summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPhilFreeman <>2015-02-12 22:58:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2015-02-12 22:58:00 (GMT)
commit00b3c8ebb754d9948b38b7fc1a4953ac6bf8df07 (patch)
tree13862c9ba6e8cd36391d89bee5b10594bbde2459
parente4014132795a96611ae110b7a2dce5b35a7d5463 (diff)
version 0.6.70.6.7
-rw-r--r--examples/passing/Operators.purs6
-rw-r--r--examples/passing/RowPolyInstanceContext.purs20
-rw-r--r--examples/passing/ScopedTypeVariables.purs34
-rw-r--r--examples/passing/UnknownInInstance.purs8
-rw-r--r--prelude/prelude.purs17
-rw-r--r--psc-docs/Main.hs99
-rw-r--r--psci/Commands.hs2
-rw-r--r--psci/Main.hs40
-rw-r--r--psci/Parser.hs2
-rw-r--r--purescript.cabal2
-rw-r--r--src/Language/PureScript/CodeGen/JS/Common.hs44
-rw-r--r--src/Language/PureScript/Environment.hs7
-rw-r--r--src/Language/PureScript/Parser/Lexer.hs1
-rw-r--r--src/Language/PureScript/TypeChecker/Entailment.hs29
-rw-r--r--src/Language/PureScript/TypeChecker/Kinds.hs111
-rw-r--r--src/Language/PureScript/TypeChecker/Monad.hs6
-rw-r--r--src/Language/PureScript/TypeChecker/Skolems.hs1
-rw-r--r--src/Language/PureScript/TypeChecker/Types.hs31
-rw-r--r--src/Language/PureScript/TypeChecker/Unify.hs17
19 files changed, 365 insertions, 112 deletions
diff --git a/examples/passing/Operators.purs b/examples/passing/Operators.purs
index ef5f10b..d38f7ed 100644
--- a/examples/passing/Operators.purs
+++ b/examples/passing/Operators.purs
@@ -73,6 +73,11 @@ module Main where
test19 :: Number
test19 = negate $ negate (-1)
+ test20 :: Number
+ test20 = 1 @ 2
+ where
+ (@) x y = x + y * y
+
main = do
let t1 = test1 1 2 (\x y -> x + y)
let t2 = test2
@@ -93,4 +98,5 @@ module Main where
let t17 = test17
let t18 = test18
let t19 = test19
+ let t20 = test20
trace "Done"
diff --git a/examples/passing/RowPolyInstanceContext.purs b/examples/passing/RowPolyInstanceContext.purs
new file mode 100644
index 0000000..5874373
--- /dev/null
+++ b/examples/passing/RowPolyInstanceContext.purs
@@ -0,0 +1,20 @@
+module Main where
+
+class T s m where
+ state :: (s -> s) -> m Unit
+
+data S s a = S (s -> { new :: s, ret :: a })
+
+instance st :: T s (S s) where
+ state f = S $ \s -> { new: f s, ret: unit }
+
+test1 :: forall r . S { foo :: String | r } Unit
+test1 = state $ \o -> o { foo = o.foo ++ "!" }
+
+test2 :: forall m r . (T { foo :: String | r } m) => m Unit
+test2 = state $ \o -> o { foo = o.foo ++ "!" }
+
+main = do
+ let t1 = test1
+ let t2 = test2
+ Debug.Trace.trace "Done"
diff --git a/examples/passing/ScopedTypeVariables.purs b/examples/passing/ScopedTypeVariables.purs
new file mode 100644
index 0000000..b081697
--- /dev/null
+++ b/examples/passing/ScopedTypeVariables.purs
@@ -0,0 +1,34 @@
+module Main where
+
+test1 :: forall a. (a -> a) -> a -> a
+test1 f x = g (g x)
+ where
+ g :: a -> a
+ g y = f (f y)
+
+test2 :: forall a. (a -> a) -> a -> a
+test2 = h
+ where
+ h :: forall b. (b -> b) -> b -> b
+ h f x = g (g x)
+ where
+ g :: b -> b
+ g y = f (f y)
+
+test3 :: Number
+test3 = ((\b -> b :: b) :: forall b. b -> b) 0
+
+test4 :: forall a. (a -> a) -> a -> a
+test4 = h
+ where
+ h :: forall b. (b -> b) -> b -> b
+ h f x = g (g x)
+ where
+ g :: b -> b
+ g y = j (f (f y))
+ where
+ j :: forall b. b -> b
+ j x = x
+
+
+main = Debug.Trace.trace "Done"
diff --git a/examples/passing/UnknownInInstance.purs b/examples/passing/UnknownInInstance.purs
new file mode 100644
index 0000000..d19a6e8
--- /dev/null
+++ b/examples/passing/UnknownInInstance.purs
@@ -0,0 +1,8 @@
+module Main where
+
+data Proxy a = Proxy
+
+test :: forall a. (Show (Proxy a)) => String
+test = show Proxy
+
+main = Debug.Trace.trace "Done"
diff --git a/prelude/prelude.purs b/prelude/prelude.purs
index 5005cd3..1ec9679 100644
--- a/prelude/prelude.purs
+++ b/prelude/prelude.purs
@@ -24,15 +24,32 @@ module Prelude
, Unit(..), unit
) where
+ -- | An alias for `true`, which can be useful in guard clauses:
+ -- |
+ -- | E.g.
+ -- |
+ -- | max x y | x >= y = x
+ -- | | otherwise = y
otherwise :: Boolean
otherwise = true
+ -- | Flips the order of the arguments to a function of two arguments.
flip :: forall a b c. (a -> b -> c) -> b -> a -> c
flip f b a = f a b
+ -- | Returns its first argument and ignores its second.
const :: forall a b. a -> b -> a
const a _ = a
+ -- | This function returns its first argument, and can be used to assert type equalities.
+ -- | This can be useful when types are otherwise ambiguous.
+ -- |
+ -- | E.g.
+ -- |
+ -- | main = print $ [] `asTypeOf` [0]
+ -- |
+ -- | If instead, we had written `main = print []`, the type of the argument `[]` would have
+ -- | been ambiguous, resulting in a compile-time error.
asTypeOf :: forall a. a -> a -> a
asTypeOf x _ = x
diff --git a/psc-docs/Main.hs b/psc-docs/Main.hs
index 8edb75f..6ca4ec5 100644
--- a/psc-docs/Main.hs
+++ b/psc-docs/Main.hs
@@ -22,6 +22,7 @@ import Data.Function (on)
import Data.List
import Data.Maybe (fromMaybe)
import Data.Version (showVersion)
+import Data.Foldable (traverse_)
import Options.Applicative
@@ -30,13 +31,11 @@ import qualified Paths_purescript as Paths
import System.Exit (exitSuccess, exitFailure)
import System.IO (hPutStrLn, stderr)
-
data PSCDocsOptions = PSCDocsOptions
{ pscdIncludeHeir :: Bool
, pscdInputFiles :: [FilePath]
}
-
docgen :: PSCDocsOptions -> IO ()
docgen (PSCDocsOptions showHierarchy input) = do
e <- P.parseModulesFromFiles (fromMaybe "") <$> mapM (fmap (first Just) . parseFile) (nub input)
@@ -62,10 +61,16 @@ spacer = tell [""]
headerLevel :: Int -> String -> Docs
headerLevel level hdr = tell [replicate level '#' ++ ' ' : hdr]
+withIndent :: Int -> Docs -> Docs
+withIndent indent = censor (map (replicate indent ' ' ++ ))
+
atIndent :: Int -> String -> Docs
atIndent indent text =
let ls = lines text in
- forM_ ls $ \l -> tell [replicate indent ' ' ++ l]
+ withIndent indent (tell ls)
+
+ticks :: String -> String
+ticks = ("`" ++) . (++ "`")
renderModules :: Bool -> [P.Module] -> Docs
renderModules showHierarchy ms = do
@@ -109,7 +114,9 @@ renderModule showHierarchy mdl@(P.Module moduleName _ exps) =
renderTopLevel :: Maybe [P.DeclarationRef] -> [P.Declaration] -> Docs
renderTopLevel exps decls = forM_ (sortBy (compare `on` getName) decls) $ \decl -> do
- renderDeclaration 4 exps decl
+ traverse_ (headerLevel 4) (ticks `fmap` getDeclarationTitle decl)
+ spacer
+ renderDeclaration exps decl
spacer
renderTypeclassImage :: P.ModuleName -> Docs
@@ -117,53 +124,81 @@ renderTypeclassImage name =
let name' = P.runModuleName name
in tell ["![" ++ name' ++ "](images/" ++ name' ++ ".png)"]
-renderDeclaration :: Int -> Maybe [P.DeclarationRef] -> P.Declaration -> Docs
-renderDeclaration n _ (P.TypeDeclaration ident ty) =
- atIndent n $ show ident ++ " :: " ++ prettyPrintType' ty
-renderDeclaration n _ (P.ExternDeclaration _ ident _ ty) =
- atIndent n $ show ident ++ " :: " ++ prettyPrintType' ty
-renderDeclaration n exps (P.DataDeclaration dtype name args ctors) = do
+getDeclarationTitle :: P.Declaration -> Maybe String
+getDeclarationTitle (P.TypeDeclaration name _) = Just (show name)
+getDeclarationTitle (P.ExternDeclaration _ name _ _) = Just (show name)
+getDeclarationTitle (P.DataDeclaration _ name _ _) = Just (show name)
+getDeclarationTitle (P.ExternDataDeclaration name _) = Just (show name)
+getDeclarationTitle (P.TypeSynonymDeclaration name _ _) = Just (show name)
+getDeclarationTitle (P.TypeClassDeclaration name _ _ _) = Just (show name)
+getDeclarationTitle (P.TypeInstanceDeclaration name _ _ _ _) = Just (show name)
+getDeclarationTitle (P.PositionedDeclaration _ _ d) = getDeclarationTitle d
+getDeclarationTitle _ = Nothing
+
+renderDeclaration :: Maybe [P.DeclarationRef] -> P.Declaration -> Docs
+renderDeclaration _ (P.TypeDeclaration ident ty) =
+ atIndent 4 $ show ident ++ " :: " ++ prettyPrintType' ty
+renderDeclaration _ (P.ExternDeclaration _ ident _ ty) =
+ atIndent 4 $ show ident ++ " :: " ++ prettyPrintType' ty
+renderDeclaration exps (P.DataDeclaration dtype name args ctors) = do
let
typeApp = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)
typeName = prettyPrintType' typeApp
exported = filter (P.isDctorExported name exps . fst) ctors
- atIndent n $ show dtype ++ " " ++ typeName ++ (if null exported then "" else " where")
- forM_ exported $ \(ctor, tys) ->
- let ctorTy = foldr P.function typeApp tys
- in atIndent (n + 2) $ P.runProperName ctor ++ " :: " ++ prettyPrintType' ctorTy
-renderDeclaration n _ (P.ExternDataDeclaration name kind) =
- atIndent n $ "data " ++ P.runProperName name ++ " :: " ++ P.prettyPrintKind kind
-renderDeclaration n _ (P.TypeSynonymDeclaration name args ty) = do
+ atIndent 4 $ show dtype ++ " " ++ typeName
+ zipWithM_ (\isFirst (ctor, tys) ->
+ atIndent 6 $ (if isFirst then "= " else "| ") ++ P.runProperName ctor ++ " " ++ unwords (map P.prettyPrintTypeAtom tys))
+ (True : repeat False) exported
+renderDeclaration _ (P.ExternDataDeclaration name kind) =
+ atIndent 4 $ "data " ++ P.runProperName name ++ " :: " ++ P.prettyPrintKind kind
+renderDeclaration _ (P.TypeSynonymDeclaration name args ty) = do
let
typeApp = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)
typeName = prettyPrintType' typeApp
- atIndent n $ "type " ++ typeName ++ " = " ++ prettyPrintType' ty
-renderDeclaration n exps (P.TypeClassDeclaration name args implies ds) = do
+ atIndent 4 $ "type " ++ typeName ++ " = " ++ prettyPrintType' ty
+renderDeclaration _ (P.TypeClassDeclaration name args implies ds) = do
let impliesText = case implies of
[] -> ""
is -> "(" ++ intercalate ", " (map (\(pn, tys') -> show pn ++ " " ++ unwords (map P.prettyPrintTypeAtom tys')) is) ++ ") <= "
classApp = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)
className = prettyPrintType' classApp
- atIndent n $ "class " ++ impliesText ++ className ++ " where"
- mapM_ (renderDeclaration (n + 2) exps) ds
-renderDeclaration n _ (P.TypeInstanceDeclaration name constraints className tys _) = do
+ atIndent 4 $ "class " ++ impliesText ++ className ++ " where"
+ mapM_ renderClassMember ds
+ where
+ renderClassMember (P.PositionedDeclaration _ _ d) = renderClassMember d
+ renderClassMember (P.TypeDeclaration ident ty) = atIndent 6 $ show ident ++ " :: " ++ prettyPrintType' ty
+ renderClassMember _ = error "Invalid argument to renderClassMember."
+renderDeclaration _ (P.TypeInstanceDeclaration name constraints className tys _) = do
let constraintsText = case constraints of
[] -> ""
cs -> "(" ++ intercalate ", " (map (\(pn, tys') -> show pn ++ " " ++ unwords (map P.prettyPrintTypeAtom tys')) cs) ++ ") => "
- atIndent n $ "instance " ++ show name ++ " :: " ++ constraintsText ++ show className ++ " " ++ unwords (map P.prettyPrintTypeAtom tys)
-renderDeclaration n exps (P.PositionedDeclaration _ com d) = do
- renderComments n com
- spacer
- renderDeclaration n exps d
-renderDeclaration _ _ _ = return ()
-
-renderComments :: Int -> [P.Comment] -> Docs
-renderComments n cs = mapM_ (atIndent n) ls
+ atIndent 4 $ "instance " ++ show name ++ " :: " ++ constraintsText ++ show className ++ " " ++ unwords (map P.prettyPrintTypeAtom tys)
+renderDeclaration exps (P.PositionedDeclaration _ com d) = do
+ renderComments com
+ renderDeclaration exps d
+renderDeclaration _ _ = return ()
+
+renderComments :: [P.Comment] -> Docs
+renderComments cs = do
+ let raw = concatMap toLines cs
+
+ if all hasPipe raw
+ then atIndent 0 . unlines . map stripPipes $ raw
+ else atIndent 4 $ unlines raw
+
+ unless (null raw) spacer
where
- ls = concatMap toLines cs
toLines (P.LineComment s) = [s]
toLines (P.BlockComment s) = lines s
+
+ hasPipe s = case dropWhile (== ' ') s of { ('|':_) -> True; _ -> False }
+
+ stripPipes = dropPipe . dropWhile (== ' ')
+
+ dropPipe ('|':' ':s) = s
+ dropPipe ('|':s) = s
+ dropPipe s = s
toTypeVar :: (String, Maybe P.Kind) -> P.Type
toTypeVar (s, Nothing) = P.TypeVar s
diff --git a/psci/Commands.hs b/psci/Commands.hs
index 8f30b89..49bc820 100644
--- a/psci/Commands.hs
+++ b/psci/Commands.hs
@@ -52,7 +52,7 @@ data Command
-- |
-- Binds a value to a name
--
- | Let (Expr -> Expr)
+ | Let [Declaration]
-- |
-- Find the type of an expression
--
diff --git a/psci/Main.hs b/psci/Main.hs
index 49505bd..73aa302 100644
--- a/psci/Main.hs
+++ b/psci/Main.hs
@@ -69,7 +69,7 @@ data PSCiState = PSCiState
{ psciImportedFilenames :: [FilePath]
, psciImportedModuleNames :: [P.ModuleName]
, psciLoadedModules :: [(Either P.RebuildPolicy FilePath, P.Module)]
- , psciLetBindings :: [P.Expr -> P.Expr]
+ , psciLetBindings :: [P.Declaration]
}
-- State helpers
@@ -95,8 +95,8 @@ updateModules modules st = st { psciLoadedModules = psciLoadedModules st ++ modu
-- |
-- Updates the state to have more let bindings.
--
-updateLets :: (P.Expr -> P.Expr) -> PSCiState -> PSCiState
-updateLets name st = st { psciLetBindings = name : psciLetBindings st }
+updateLets :: [P.Declaration] -> PSCiState -> PSCiState
+updateLets ds st = st { psciLetBindings = ds ++ psciLetBindings st }
-- File helpers
-- |
@@ -141,6 +141,16 @@ loadAllModules files = do
return (Right filename, content)
return $ P.parseModulesFromFiles (either (const "") id) $ (Left P.RebuildNever, P.prelude) : filesAndContent
+-- |
+-- Load all modules, updating the application state
+--
+loadAllImportedModules :: PSCI ()
+loadAllImportedModules = do
+ files <- PSCI . lift $ fmap psciImportedFilenames get
+ modulesOrFirstError <- psciIO $ loadAllModules files
+ case modulesOrFirstError of
+ Left err -> psciIO $ print err
+ Right modules -> PSCI . lift . modify $ \st -> st { psciLoadedModules = modules }
-- |
-- Expands tilde in path.
@@ -348,13 +358,13 @@ createTemporaryModule exec PSCiState{psciImportedModuleNames = imports, psciLetB
importDecl m = P.ImportDeclaration m P.Unqualified Nothing
traceModule = P.ModuleName [P.ProperName "Debug", P.ProperName "Trace"]
trace = P.Var (P.Qualified (Just traceModule) (P.Ident "print"))
- itValue = foldl (\x f -> f x) val lets
mainValue = P.App trace (P.Var (P.Qualified Nothing (P.Ident "it")))
- itDecl = P.ValueDeclaration (P.Ident "it") P.Value [] $ Right itValue
+ itDecl = P.ValueDeclaration (P.Ident "it") P.Value [] $ Right val
mainDecl = P.ValueDeclaration (P.Ident "main") P.Value [] $ Right mainValue
decls = if exec then [itDecl, mainDecl] else [itDecl]
in
- P.Module moduleName ((importDecl `map` imports) ++ decls) Nothing
+ P.Module moduleName ((importDecl `map` imports) ++ lets ++ decls) Nothing
+
-- |
-- Makes a volatile module to hold a non-qualified type synonym for a fully-qualified data type declaration.
@@ -408,10 +418,10 @@ handleDeclaration val = do
-- Takes a let declaration and updates the environment, then run a make. If the declaration fails,
-- restore the pre-let environment.
--
-handleLet :: (P.Expr -> P.Expr) -> PSCI ()
-handleLet l = do
+handleLet :: [P.Declaration] -> PSCI ()
+handleLet ds = do
st <- PSCI $ lift get
- let st' = updateLets l st
+ let st' = updateLets ds st
let m = createTemporaryModule False st' (P.ObjectLiteral [])
e <- psciIO . runMake $ P.make modulesDir options (psciLoadedModules st' ++ [(Left P.RebuildAlways, m)]) []
case e of
@@ -561,10 +571,12 @@ handleCommand (LoadFile filePath) = do
PSCI . outputStrLn $ "Couldn't locate: " ++ filePath
handleCommand Reset = do
files <- psciImportedFilenames <$> PSCI (lift get)
- modulesOrFirstError <- psciIO $ loadAllModules files
- case modulesOrFirstError of
- Left err -> psciIO $ print err >> exitFailure
- Right modules -> PSCI . lift $ put (PSCiState files defaultImports modules [])
+ PSCI . lift . modify $ \st -> st
+ { psciImportedFilenames = files
+ , psciImportedModuleNames = defaultImports
+ , psciLetBindings = []
+ }
+ loadAllImportedModules
handleCommand (TypeOf val) = handleTypeOf val
handleCommand (KindOf typ) = handleKindOf typ
handleCommand (Browse moduleName) = handleBrowse moduleName
@@ -609,7 +621,7 @@ loop (PSCiOptions singleLineMode files) = do
Left err -> outputStrLn err >> go
Right Nothing -> go
Right (Just Quit) -> outputStrLn quitMessage
- Right (Just c') -> runPSCI (handleCommand c') >> go
+ Right (Just c') -> runPSCI (loadAllImportedModules >> handleCommand c') >> go
singleLineFlag :: Parser Bool
singleLineFlag = switch $
diff --git a/psci/Parser.hs b/psci/Parser.hs
index 0d5cd53..2058f9b 100644
--- a/psci/Parser.hs
+++ b/psci/Parser.hs
@@ -76,7 +76,7 @@ parseCommand cmdString =
-- we actually want the normal @let@.
--
psciLet :: P.TokenParser Command
- psciLet = Let <$> (P.Let <$> (P.reserved "let" *> P.indented *> manyDecls))
+ psciLet = Let <$> (P.reserved "let" *> P.indented *> manyDecls)
where
manyDecls :: P.TokenParser [P.Declaration]
manyDecls = C.mark (many1 (C.same *> P.parseDeclaration))
diff --git a/purescript.cabal b/purescript.cabal
index cb130d5..e70a75b 100644
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
name: purescript
-version: 0.6.6
+version: 0.6.7
cabal-version: >=1.8
build-type: Simple
license: MIT
diff --git a/src/Language/PureScript/CodeGen/JS/Common.hs b/src/Language/PureScript/CodeGen/JS/Common.hs
index 8c90813..6ba0e78 100644
--- a/src/Language/PureScript/CodeGen/JS/Common.hs
+++ b/src/Language/PureScript/CodeGen/JS/Common.hs
@@ -135,7 +135,47 @@ nameIsJsReserved name =
, "volatile"
, "while"
, "with"
- , "yield" ]
+ , "yield" ] || properNameIsJsReserved name
moduleNameToJs :: ModuleName -> String
-moduleNameToJs (ModuleName pns) = intercalate "_" (runProperName `map` pns)
+moduleNameToJs (ModuleName pns) =
+ let name = intercalate "_" (runProperName `map` pns)
+ in if properNameIsJsReserved name then "$$" ++ name else name
+
+-- |
+-- Checks whether a proper name is reserved in Javascript.
+--
+properNameIsJsReserved :: String -> Bool
+properNameIsJsReserved name =
+ name `elem` [ "Infinity"
+ , "NaN"
+ , "Object"
+ , "Function"
+ , "Boolean"
+ , "Error"
+ , "EvalError"
+ , "InternalError"
+ , "RangeError"
+ , "ReferenceError"
+ , "SyntaxError"
+ , "TypeError"
+ , "URIError"
+ , "Number"
+ , "Math"
+ , "Date"
+ , "String"
+ , "RegExp"
+ , "Array"
+ , "Int8Array"
+ , "Uint8Array"
+ , "Uint8ClampedArray"
+ , "Int16Array"
+ , "Uint16Array"
+ , "Int32Array"
+ , "Uint32Array"
+ , "Float32Array"
+ , "Float64Array"
+ , "ArrayBuffer"
+ , "DataView"
+ , "JSON"
+ , "Intl" ]
diff --git a/src/Language/PureScript/Environment.hs b/src/Language/PureScript/Environment.hs
index 347c50f..71472e3 100644
--- a/src/Language/PureScript/Environment.hs
+++ b/src/Language/PureScript/Environment.hs
@@ -136,7 +136,12 @@ data TypeKind
-- |
-- A local type variable
--
- | LocalTypeVariable deriving (Show, Eq, Data, Typeable)
+ | LocalTypeVariable
+ -- |
+ -- A scoped type variable
+ --
+ | ScopedTypeVar
+ deriving (Show, Eq, Data, Typeable)
-- |
-- The type ('data' or 'newtype') of a data type declaration
diff --git a/src/Language/PureScript/Parser/Lexer.hs b/src/Language/PureScript/Parser/Lexer.hs
index 03d771e..3aa5d83 100644
--- a/src/Language/PureScript/Parser/Lexer.hs
+++ b/src/Language/PureScript/Parser/Lexer.hs
@@ -422,6 +422,7 @@ symbol = token go P.<?> "symbol"
go (Symbol s) = Just s
go Colon = Just ":"
go LFatArrow = Just "<="
+ go At = Just "@"
go _ = Nothing
symbol' :: String -> TokenParser ()
diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index 377d3d2..d63b2f0 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -20,6 +20,7 @@ module Language.PureScript.TypeChecker.Entailment (
import Data.Function (on)
import Data.List
import Data.Maybe (maybeToList)
+import Data.Foldable (foldMap)
import qualified Data.Map as M
import Control.Applicative
@@ -199,13 +200,35 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt
-- and return a substitution from type variables to types which makes the type heads unify.
--
typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
-typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
-typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
+typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
+typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
+-- In this case, we might want type information to flow back to the typechecker.
+-- TODO: run this function in the UnifyT monad.
+typeHeadsAreEqual _ _ (TUnknown _) _ = Just []
typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
-typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2
+typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2
+ <*> typeHeadsAreEqual m e t1 t2
typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
Left _ -> Nothing
Right t1 -> typeHeadsAreEqual m e t1 t2
+typeHeadsAreEqual _ _ REmpty REmpty = Just []
+typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =
+ let (s1, r1') = rowToList r1
+ (s2, r2') = rowToList r2
+
+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
+ in (++) <$> foldMap (\(t1, t2) -> typeHeadsAreEqual m e t1 t2) int
+ <*> go sd1 r1' sd2 r2'
+ where
+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
+ go [] REmpty [] REmpty = Just []
+ go [] (TUnknown _) _ _ = Just []
+ go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = Just []
+ go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []
+ go sd r [] (TypeVar v) = Just [(v, rowFromList (sd, r))]
+ go _ _ _ _ = Nothing
typeHeadsAreEqual _ _ _ _ = Nothing
-- |
diff --git a/src/Language/PureScript/TypeChecker/Kinds.hs b/src/Language/PureScript/TypeChecker/Kinds.hs
index c83e37c..60083cc 100644
--- a/src/Language/PureScript/TypeChecker/Kinds.hs
+++ b/src/Language/PureScript/TypeChecker/Kinds.hs
@@ -14,19 +14,22 @@
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TupleSections #-}
module Language.PureScript.TypeChecker.Kinds (
kindOf,
+ kindOfWithScopedVars,
kindsOf,
kindsOfAll
) where
import Data.Maybe (fromMaybe)
import Data.Monoid ((<>))
+
import qualified Data.HashMap.Strict as H
import qualified Data.Map as M
+import Control.Arrow (second)
import Control.Applicative
import Control.Monad.Error
import Control.Monad.State
@@ -69,11 +72,19 @@ instance Unifiable Check Kind where
-- Infer the kind of a single type
--
kindOf :: ModuleName -> Type -> Check Kind
-kindOf _ ty =
+kindOf _ ty = fst <$> kindOfWithScopedVars ty
+
+-- |
+-- Infer the kind of a single type, returning the kinds of any scoped type variables
+--
+kindOfWithScopedVars :: Type -> Check (Kind, [(String, Kind)])
+kindOfWithScopedVars ty =
rethrow (mkErrorStack "Error checking kind" (Just (TypeError ty)) <>) $
- fmap (starIfUnknown . tidyUp) . liftUnify $ infer ty
+ fmap tidyUp . liftUnify $ infer ty
where
- tidyUp (k, sub) = sub $? k
+ tidyUp ((k, args), sub) = ( starIfUnknown (sub $? k)
+ , map (second (starIfUnknown . (sub $?))) args
+ )
-- |
-- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors
@@ -125,7 +136,7 @@ kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do
--
solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind
solveTypes isData ts kargs tyCon = do
- ks <- mapM infer ts
+ ks <- mapM (fmap fst . infer) ts
when isData $ do
tyCon =?= foldr FunKind Star kargs
forM_ ks $ \k -> k =?= Star
@@ -145,48 +156,64 @@ starIfUnknown k = k
-- |
-- Infer a kind for a type
--
-infer :: Type -> UnifyT Kind Check Kind
+infer :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])
infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty
-infer' :: Type -> UnifyT Kind Check Kind
-infer' TypeWildcard = fresh
-infer' (TypeVar v) = do
- Just moduleName <- checkCurrentModule <$> get
- UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
-infer' c@(TypeConstructor v) = do
- env <- liftCheck getEnv
- case M.lookup v (types env) of
- Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))
- Just (kind, _) -> return kind
-infer' (TypeApp t1 t2) = do
- k0 <- fresh
- k1 <- infer t1
- k2 <- infer t2
- k1 =?= FunKind k2 k0
- return k0
+infer' :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])
infer' (ForAll ident ty _) = do
k1 <- fresh
Just moduleName <- checkCurrentModule <$> get
- k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
+ (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
k2 =?= Star
- return Star
-infer' REmpty = do
- k <- fresh
- return $ Row k
-infer' (RCons _ ty row) = do
- k1 <- infer ty
- k2 <- infer row
- k2 =?= Row k1
- return $ Row k1
-infer' (ConstrainedType deps ty) = do
- forM_ deps $ \(className, tys) -> do
- _ <- infer $ foldl TypeApp (TypeConstructor className) tys
- return ()
- k <- infer ty
- k =?= Star
- return Star
+ return (Star, (ident, k1) : args)
infer' (KindedType ty k) = do
- k' <- infer ty
+ (k', args) <- infer ty
k =?= k'
- return k'
-infer' _ = error "Invalid argument to infer"
+ return (k', args)
+infer' other = (, []) <$> go other
+ where
+ go :: Type -> UnifyT Kind Check Kind
+ go (ForAll ident ty _) = do
+ k1 <- fresh
+ Just moduleName <- checkCurrentModule <$> get
+ k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ go ty
+ k2 =?= Star
+ return Star
+ go (KindedType ty k) = do
+ k' <- go ty
+ k =?= k'
+ return k'
+ go TypeWildcard = fresh
+ go (TypeVar v) = do
+ Just moduleName <- checkCurrentModule <$> get
+ UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
+ go (Skolem v _ _) = do
+ Just moduleName <- checkCurrentModule <$> get
+ UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
+ go c@(TypeConstructor v) = do
+ env <- liftCheck getEnv
+ case M.lookup v (types env) of
+ Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))
+ Just (kind, _) -> return kind
+ go (TypeApp t1 t2) = do
+ k0 <- fresh
+ k1 <- go t1
+ k2 <- go t2
+ k1 =?= FunKind k2 k0
+ return k0
+ go REmpty = do
+ k <- fresh
+ return $ Row k
+ go (RCons _ ty row) = do
+ k1 <- go ty
+ k2 <- go row
+ k2 =?= Row k1
+ return $ Row k1
+ go (ConstrainedType deps ty) = do
+ forM_ deps $ \(className, tys) -> do
+ _ <- go $ foldl TypeApp (TypeConstructor className) tys
+ return ()
+ k <- go ty
+ k =?= Star
+ return Star
+ go _ = error "Invalid argument to infer"
diff --git a/src/Language/PureScript/TypeChecker/Monad.hs b/src/Language/PureScript/TypeChecker/Monad.hs
index 14c04d8..b59c08a 100644
--- a/src/Language/PureScript/TypeChecker/Monad.hs
+++ b/src/Language/PureScript/TypeChecker/Monad.hs
@@ -57,6 +57,12 @@ bindTypes newNames action = do
return a
-- |
+-- Temporarily bind a collection of names to types
+--
+withScopedTypeVars :: (Functor m, MonadState CheckState m) => ModuleName -> [(String, Kind)] -> m a -> m a
+withScopedTypeVars mn ks = bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar))) ks))
+
+-- |
-- Temporarily make a collection of type class dictionaries available
--
withTypeClassDictionaries :: (MonadState CheckState m) => [TypeClassDictionaryInScope] -> m a -> m a
diff --git a/src/Language/PureScript/TypeChecker/Skolems.hs b/src/Language/PureScript/TypeChecker/Skolems.hs
index f99413c..62ee80a 100644
--- a/src/Language/PureScript/TypeChecker/Skolems.hs
+++ b/src/Language/PureScript/TypeChecker/Skolems.hs
@@ -71,6 +71,7 @@ skolemizeTypesInValue :: String -> Int -> SkolemScope -> Expr -> Expr
skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id go id in f
where
go (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)
+ go (TypedValue check val ty) = TypedValue check val (skolemize ident sko scope ty)
go other = other
-- |
diff --git a/src/Language/PureScript/TypeChecker/Types.hs b/src/Language/PureScript/TypeChecker/Types.hs
index 22476d5..49f7d0d 100644
--- a/src/Language/PureScript/TypeChecker/Types.hs
+++ b/src/Language/PureScript/TypeChecker/Types.hs
@@ -129,16 +129,16 @@ typeDictionaryForBindingGroup moduleName vals = do
return (untyped, typed, dict, untypedDict)
checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData -> UnifyT Type Check (Ident, (Expr, Type))
-checkTypedBindingGroupElement moduleName (ident, (val', ty, checkType)) dict = do
+checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do
-- Replace type wildcards
ty' <- replaceTypeWildcards ty
-- Kind check
- kind <- liftCheck $ kindOf moduleName ty
- guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty
+ checkTypeKind kind
-- Check the type with the new names in scope
ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'
val'' <- if checkType
- then bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''
+ then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''
else return (TypedValue False val' ty'')
return (ident, (val'', ty''))
@@ -183,10 +183,8 @@ replaceTypeClassDictionaries mn =
-- |
-- Check the kind of a type, failing if it is not of kind *.
--
-checkTypeKind :: ModuleName -> Type -> UnifyT t Check ()
-checkTypeKind moduleName ty = do
- kind <- liftCheck $ kindOf moduleName ty
- guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+checkTypeKind :: Kind -> UnifyT t Check ()
+checkTypeKind kind = guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
-- |
-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
@@ -293,9 +291,10 @@ infer' (SuperClassDictionary className tys) = do
return $ TypeClassDictionary False (className, tys) dicts
infer' (TypedValue checkType val ty) = do
Just moduleName <- checkCurrentModule <$> get
- checkTypeKind moduleName ty
+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty
+ checkTypeKind kind
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
- val' <- if checkType then check val ty' else return val
+ val' <- if checkType then withScopedTypeVars moduleName args (check val ty') else return val
return $ TypedValue True val' ty'
infer' (PositionedValue pos _ val) = rethrowWithPosition pos $ infer' val
infer' _ = error "Invalid argument to infer"
@@ -304,10 +303,11 @@ inferLetBinding :: [Declaration] -> [Declaration] -> Expr -> (Expr -> UnifyT Typ
inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret)
inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
Just moduleName <- checkCurrentModule <$> get
- checkTypeKind moduleName ty
+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty
+ checkTypeKind kind
let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
- TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv
+ TypedValue _ val' ty'' <- if checkType then withScopedTypeVars moduleName args (bindNames dict (check val ty')) else return tv
bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j
inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do
valTy <- fresh
@@ -507,14 +507,15 @@ check' (SuperClassDictionary className tys) _ = do
return $ TypeClassDictionary False (className, tys) dicts
check' (TypedValue checkType val ty1) ty2 = do
Just moduleName <- checkCurrentModule <$> get
- checkTypeKind moduleName ty1
+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty1
+ checkTypeKind kind
ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1
ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2
val' <- subsumes (Just val) ty1' ty2'
case val' of
Nothing -> throwError . strMsg $ "Unable to check type subsumption"
Just val'' -> do
- val''' <- if checkType then check val'' ty2' else return val''
+ val''' <- if checkType then withScopedTypeVars moduleName args (check val'' ty2') else return val''
return $ TypedValue checkType (TypedValue True val''' ty1') ty2'
check' (Case vals binders) ret = do
vals' <- mapM infer vals
@@ -562,7 +563,7 @@ check' val ty | containsTypeSynonyms ty = do
ty' <- introduceSkolemScope <=< expandAllTypeSynonyms <=< replaceTypeWildcards $ ty
check val ty'
check' val kt@(KindedType ty kind) = do
- guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+ checkTypeKind kind
val' <- check' val ty
return $ TypedValue True val' kt
check' (PositionedValue pos _ val) ty =
diff --git a/src/Language/PureScript/TypeChecker/Unify.hs b/src/Language/PureScript/TypeChecker/Unify.hs
index dcaef98..197ca9a 100644
--- a/src/Language/PureScript/TypeChecker/Unify.hs
+++ b/src/Language/PureScript/TypeChecker/Unify.hs
@@ -153,6 +153,23 @@ unifiesWith e (SaturatedTypeSynonym name args) t2 =
Left _ -> False
Right t1 -> unifiesWith e t1 t2
unifiesWith e t1 t2@(SaturatedTypeSynonym _ _) = unifiesWith e t2 t1
+unifiesWith _ REmpty REmpty = True
+unifiesWith e r1@(RCons _ _ _) r2@(RCons _ _ _) =
+ let (s1, r1') = rowToList r1
+ (s2, r2') = rowToList r2
+
+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
+ in all (\(t1, t2) -> unifiesWith e t1 t2) int && go sd1 r1' sd2 r2'
+ where
+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Bool
+ go [] REmpty [] REmpty = True
+ go [] (TypeVar v1) [] (TypeVar v2) = v1 == v2
+ go [] (Skolem _ s1 _) [] (Skolem _ s2 _) = s1 == s2
+ go _ (TUnknown _) _ _ = True
+ go _ _ _ (TUnknown _) = True
+ go _ _ _ _ = False
unifiesWith _ _ _ = False
-- |