summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPhilFreeman <>2013-11-28 05:06:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2013-11-28 05:06:00 (GMT)
commitc3ab78e89723e634a0ce9fd8ce21e3ef5439a28a (patch)
tree9aca5cb7d35a46f8d7432652bdddd188e1d4c193
parent084bf6f0a63c09cc45a05131606bb6a883e6e57e (diff)
version 0.1.130.1.13
-rw-r--r--purescript.cabal3
-rw-r--r--src/Language/PureScript.hs4
-rw-r--r--src/Language/PureScript/CodeGen/Externs.hs4
-rw-r--r--src/Language/PureScript/CodeGen/JS.hs35
-rw-r--r--src/Language/PureScript/Declarations.hs8
-rw-r--r--src/Language/PureScript/Kinds.hs3
-rw-r--r--src/Language/PureScript/Names.hs5
-rw-r--r--src/Language/PureScript/Parser/Common.hs23
-rw-r--r--src/Language/PureScript/Parser/Declarations.hs19
-rw-r--r--src/Language/PureScript/Parser/Types.hs32
-rw-r--r--src/Language/PureScript/Parser/Values.hs16
-rw-r--r--src/Language/PureScript/Pretty/Kinds.hs3
-rw-r--r--src/Language/PureScript/Pretty/Types.hs15
-rw-r--r--src/Language/PureScript/Pretty/Values.hs10
-rw-r--r--src/Language/PureScript/TypeChecker.hs42
-rw-r--r--src/Language/PureScript/TypeChecker/Kinds.hs209
-rw-r--r--src/Language/PureScript/TypeChecker/Monad.hs98
-rw-r--r--src/Language/PureScript/TypeChecker/Types.hs1168
-rw-r--r--src/Language/PureScript/Types.hs42
-rw-r--r--src/Language/PureScript/Unknown.hs25
20 files changed, 1025 insertions, 739 deletions
diff --git a/purescript.cabal b/purescript.cabal
index ed7de6e..e70224b 100644
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
name: purescript
-version: 0.1.9
+version: 0.1.13
cabal-version: >=1.8
build-type: Simple
license: MIT
@@ -36,6 +36,7 @@ library
Language.PureScript.TypeChecker.Monad
Language.PureScript.TypeChecker.Types
Language.PureScript.TypeChecker.Synonyms
+ Language.PureScript.Unknown
exposed: True
buildable: True
hs-source-dirs: src
diff --git a/src/Language/PureScript.hs b/src/Language/PureScript.hs
index df229aa..9a40e30 100644
--- a/src/Language/PureScript.hs
+++ b/src/Language/PureScript.hs
@@ -32,7 +32,7 @@ import Data.Maybe (mapMaybe)
compile :: [Declaration] -> Either String (String, String, Environment)
compile decls = do
bracketted <- rebracket decls
- (_, env) <- check (typeCheckAll bracketted)
- let js = prettyPrintJS . map optimize . concat . mapMaybe (declToJs Nothing global) $ bracketted
+ (_, env) <- runCheck (typeCheckAll bracketted)
+ let js = prettyPrintJS . map optimize . concat . mapMaybe (\decl -> declToJs Nothing global decl env) $ bracketted
let exts = intercalate "\n" . mapMaybe (externToPs 0 global env) $ bracketted
return (js, exts, env)
diff --git a/src/Language/PureScript/CodeGen/Externs.hs b/src/Language/PureScript/CodeGen/Externs.hs
index 17a150d..eacd224 100644
--- a/src/Language/PureScript/CodeGen/Externs.hs
+++ b/src/Language/PureScript/CodeGen/Externs.hs
@@ -27,12 +27,12 @@ import Language.PureScript.Names
externToPs :: Int -> ModulePath -> Environment -> Declaration -> Maybe String
externToPs indent path env (ValueDeclaration name _) = do
(ty, _) <- M.lookup (path, name) $ names env
- return $ replicate indent ' ' ++ "foreign import " ++ show name ++ " :: " ++ prettyPrintPolyType ty
+ return $ replicate indent ' ' ++ "foreign import " ++ show name ++ " :: " ++ prettyPrintType ty
externToPs indent path env (DataDeclaration name _ _) = do
(kind, _) <- M.lookup (path, name) $ types env
return $ replicate indent ' ' ++ "foreign import data " ++ show name ++ " :: " ++ prettyPrintKind kind
externToPs indent path env (ExternMemberDeclaration member name ty) =
- return $ replicate indent ' ' ++ "foreign import member " ++ show member ++ " " ++ show name ++ " :: " ++ prettyPrintPolyType ty
+ return $ replicate indent ' ' ++ "foreign import member " ++ show member ++ " " ++ show name ++ " :: " ++ prettyPrintType ty
externToPs indent path env (ExternDataDeclaration name kind) =
return $ replicate indent ' ' ++ "foreign import data " ++ show name ++ " :: " ++ prettyPrintKind kind
externToPs indent path env (TypeSynonymDeclaration name args ty) =
diff --git a/src/Language/PureScript/CodeGen/JS.hs b/src/Language/PureScript/CodeGen/JS.hs
index f13bc29..720d197 100644
--- a/src/Language/PureScript/CodeGen/JS.hs
+++ b/src/Language/PureScript/CodeGen/JS.hs
@@ -20,11 +20,13 @@ module Language.PureScript.CodeGen.JS (
import Data.Char
import Data.Maybe (fromMaybe, mapMaybe)
import Data.List (intercalate)
+import qualified Data.Map as M
import qualified Control.Arrow as A
import Control.Arrow ((<+>), second)
import Control.Monad (forM)
import Control.Applicative
+import Language.PureScript.TypeChecker (Environment, names)
import Language.PureScript.Types
import Language.PureScript.Values
import Language.PureScript.Names
@@ -33,17 +35,17 @@ import Language.PureScript.Pretty.Common
import Language.PureScript.CodeGen.Monad
import Language.PureScript.CodeGen.JS.AST as AST
-declToJs :: Maybe Ident -> ModulePath -> Declaration -> Maybe [JS]
-declToJs mod mp (ValueDeclaration ident (Abs args ret)) =
+declToJs :: Maybe Ident -> ModulePath -> Declaration -> Environment -> Maybe [JS]
+declToJs mod mp (ValueDeclaration ident (Abs args ret)) _ =
Just $ JSFunction (Just ident) args (JSBlock [JSReturn (valueToJs mp ret)]) :
maybe [] (return . setProperty (identToJs ident) (JSVar ident)) mod
-declToJs mod mp (ValueDeclaration ident val) =
+declToJs mod mp (ValueDeclaration ident val) _ =
Just $ JSVariableIntroduction ident (Just (valueToJs mp val)) :
maybe [] (return . setProperty (identToJs ident) (JSVar ident)) mod
-declToJs mod _ (ExternMemberDeclaration member ident _) =
+declToJs mod _ (ExternMemberDeclaration member ident _) _ =
Just $ JSFunction (Just ident) [Ident "value"] (JSBlock [JSReturn (JSAccessor member (JSVar (Ident "value")))]) :
maybe [] (return . setProperty (show ident) (JSVar ident)) mod
-declToJs mod mp (DataDeclaration _ _ ctors) =
+declToJs mod mp (DataDeclaration _ _ ctors) _ =
Just $ flip concatMap ctors $ \(pn@(ProperName ctor), maybeTy) ->
let
ctorJs =
@@ -54,14 +56,21 @@ declToJs mod mp (DataDeclaration _ _ ctors) =
(JSObjectLiteral [ ("ctor", JSStringLiteral (show (Qualified mp pn)))
, ("value", JSVar (Ident "value")) ])])
in ctorJs : maybe [] (return . setProperty ctor (JSVar (Ident ctor))) mod
-declToJs mod mp (ModuleDeclaration pn@(ProperName name) decls) =
+declToJs mod mp (ModuleDeclaration pn@(ProperName name) decls) env =
Just $ [ JSVariableIntroduction (Ident name) Nothing
, JSApp (JSFunction Nothing [Ident name]
- (JSBlock (concat $ mapMaybe (declToJs (Just (Ident name)) (subModule mp pn)) decls)))
- [JSAssignment (JSAssignVariable (Ident name) )
+ (JSBlock (concat $ mapMaybe (\decl -> declToJs (Just (Ident name)) (subModule mp pn) decl env) decls)))
+ [JSAssignment (JSAssignVariable (Ident name))
(JSBinary Or (JSVar (Ident name)) (JSObjectLiteral []))]] ++
maybe [] (return . setProperty name (JSVar (Ident name))) mod
-declToJs _ _ _ = Nothing
+declToJs mod omp (ImportDeclaration mp idents) env =
+ Just $ case idents of
+ Nothing ->
+ let idents = map snd . filter ((== mp) . fst) . M.keys $ names env
+ in map mkLocal idents
+ Just idents -> map mkLocal idents
+ where mkLocal ident = JSVariableIntroduction ident (Just (qualifiedToJS identToJs (Qualified mp ident)))
+declToJs _ _ _ _ = Nothing
setProperty :: String -> JS -> Ident -> JS
setProperty prop val mod = JSAssignment (JSAssignProperty prop (JSAssignVariable mod)) val
@@ -87,10 +96,10 @@ valueToJs m (Var ident) = qualifiedToJS identToJs ident
valueToJs m (TypedValue val _) = valueToJs m val
qualifiedToJS :: (a -> String) -> Qualified a -> JS
-qualifiedToJS f (Qualified (ModulePath parts) a) = delimited (f a : reverse (map show parts))
- where
- delimited [part] = JSVar (Ident (part))
- delimited (part:parts) = JSAccessor part (delimited parts)
+qualifiedToJS f (Qualified (ModulePath parts) a) =
+ delimited (f a : reverse (map show parts))
+ where delimited [part] = JSVar (Ident (part))
+ delimited (part:parts) = JSAccessor part (delimited parts)
bindersToJs :: ModulePath -> [(Binder, Value)] -> JS -> Gen JS
bindersToJs m binders val = do
diff --git a/src/Language/PureScript/Declarations.hs b/src/Language/PureScript/Declarations.hs
index 7632a85..5457a73 100644
--- a/src/Language/PureScript/Declarations.hs
+++ b/src/Language/PureScript/Declarations.hs
@@ -30,12 +30,14 @@ data Associativity = Infixl | Infixr deriving (Show, D.Data, D.Typeable)
data Fixity = Fixity Associativity Precedence deriving (Show, D.Data, D.Typeable)
data Declaration
- = DataDeclaration ProperName [String] [(ProperName, Maybe Type)]
- | TypeSynonymDeclaration ProperName [String] Type
+ = DataDeclaration ProperName [String] [(ProperName, Maybe PolyType)]
+ | TypeSynonymDeclaration ProperName [String] PolyType
| TypeDeclaration Ident PolyType
| ValueDeclaration Ident Value
| ExternDeclaration Ident PolyType
| ExternMemberDeclaration String Ident PolyType
| ExternDataDeclaration ProperName Kind
| FixityDeclaration Fixity String
- | ModuleDeclaration ProperName [Declaration] deriving (Show, D.Data, D.Typeable)
+ | ModuleDeclaration ProperName [Declaration]
+ | ImportDeclaration ModulePath (Maybe [Ident])
+ deriving (Show, D.Data, D.Typeable)
diff --git a/src/Language/PureScript/Kinds.hs b/src/Language/PureScript/Kinds.hs
index 87786a6..222338c 100644
--- a/src/Language/PureScript/Kinds.hs
+++ b/src/Language/PureScript/Kinds.hs
@@ -17,9 +17,10 @@
module Language.PureScript.Kinds where
import Data.Data
+import Language.PureScript.Unknown
data Kind
- = KUnknown Int
+ = KUnknown (Unknown Kind)
| Star
| Row
| FunKind Kind Kind deriving (Show, Eq, Data, Typeable)
diff --git a/src/Language/PureScript/Names.hs b/src/Language/PureScript/Names.hs
index 22f8193..7bb47b3 100644
--- a/src/Language/PureScript/Names.hs
+++ b/src/Language/PureScript/Names.hs
@@ -30,7 +30,10 @@ newtype ProperName = ProperName { runProperName :: String } deriving (Eq, Ord, D
instance Show ProperName where
show = runProperName
-data ModulePath = ModulePath [ProperName] deriving (Show, Eq, Ord, Data, Typeable)
+data ModulePath = ModulePath [ProperName] deriving (Eq, Ord, Data, Typeable)
+
+instance Show ModulePath where
+ show (ModulePath segments) = intercalate "." $ map show segments
subModule :: ModulePath -> ProperName -> ModulePath
subModule (ModulePath mp) name = ModulePath (mp ++ [name])
diff --git a/src/Language/PureScript/Parser/Common.hs b/src/Language/PureScript/Parser/Common.hs
index 2bfda2b..7f202de 100644
--- a/src/Language/PureScript/Parser/Common.hs
+++ b/src/Language/PureScript/Parser/Common.hs
@@ -120,22 +120,27 @@ reservedOp = PT.reservedOp tokenParser
operator = PT.operator tokenParser
stringLiteral = PT.stringLiteral tokenParser
whiteSpace = PT.whiteSpace tokenParser
-parens = PT.parens tokenParser
-braces = PT.braces tokenParser
-angles = PT.angles tokenParser
squares = PT.squares tokenParser
semi = PT.semi tokenParser
comma = PT.comma tokenParser
colon = PT.colon tokenParser
dot = PT.dot tokenParser
-semiSep = PT.semiSep tokenParser
-semiSep1 = PT.semiSep1 tokenParser
-commaSep = PT.commaSep tokenParser
-commaSep1 = PT.commaSep1 tokenParser
natural = PT.natural tokenParser
-tick :: P.Parsec String u Char
+parens = P.between (lexeme $ P.char '(') (lexeme $ indented *> P.char ')') . (indented *>)
+braces = P.between (lexeme $ P.char '{') (lexeme $ indented *> P.char '}') . (indented *>)
+angles = P.between (lexeme $ P.char '<') (lexeme $ indented *> P.char '>') . (indented *>)
+
+sepBy p s = P.sepBy (indented *> p) (indented *> s)
+sepBy1 p s = P.sepBy1 (indented *> p) (indented *> s)
+
+semiSep = flip sepBy semi
+semiSep1 = flip sepBy1 semi
+commaSep = flip sepBy comma
+commaSep1 = flip sepBy1 comma
+
tick = lexeme $ P.char '`'
+pipe = lexeme $ P.char '|'
properName :: P.Parsec String u ProperName
properName = lexeme $ ProperName <$> P.try ((:) <$> P.upper <*> many (PT.identLetter langDef) P.<?> "name")
@@ -167,7 +172,7 @@ buildPostfixParser f x = fold x (P.choice f) (flip ($))
operatorOrBuiltIn :: P.Parsec String u String
operatorOrBuiltIn = P.try operator <|> P.choice (map (\s -> P.try (reservedOp s) >> return s) builtInOperators)
-parseIdent :: P.Parsec String u Ident
+parseIdent :: P.Parsec String ParseState Ident
parseIdent = (Ident <$> identifier) <|> (Op <$> parens operatorOrBuiltIn)
parseIdentInfix :: P.Parsec String ParseState (Qualified Ident)
diff --git a/src/Language/PureScript/Parser/Declarations.hs b/src/Language/PureScript/Parser/Declarations.hs
index a0a28ca..d8c270b 100644
--- a/src/Language/PureScript/Parser/Declarations.hs
+++ b/src/Language/PureScript/Parser/Declarations.hs
@@ -28,6 +28,7 @@ import qualified Data.Map as M
import qualified Text.Parsec as P
import qualified Text.Parsec.Pos as P
+import Language.PureScript.Names
import Language.PureScript.Values
import Language.PureScript.Types
import Language.PureScript.Parser.State
@@ -43,7 +44,7 @@ parseDataDeclaration = do
name <- indented *> properName
tyArgs <- many (indented *> identifier)
lexeme $ indented *> P.char '='
- ctors <- P.sepBy1 ((,) <$> (indented *> properName) <*> P.optionMaybe parseType) (lexeme $ indented *> P.char '|')
+ ctors <- sepBy1 ((,) <$> properName <*> P.optionMaybe (indented *> parsePolyType)) pipe
return $ DataDeclaration name tyArgs ctors
parseTypeDeclaration :: P.Parsec String ParseState Declaration
@@ -55,7 +56,7 @@ parseTypeSynonymDeclaration :: P.Parsec String ParseState Declaration
parseTypeSynonymDeclaration =
TypeSynonymDeclaration <$> (P.try (reserved "type") *> indented *> properName)
<*> many (indented *> identifier)
- <*> (lexeme (indented *> P.char '=') *> parseType)
+ <*> (lexeme (indented *> P.char '=') *> parsePolyType)
parseValueDeclaration :: P.Parsec String ParseState Declaration
parseValueDeclaration =
@@ -96,6 +97,17 @@ parseModuleDeclaration = do
decls <- mark (P.many (same *> parseDeclaration))
return $ ModuleDeclaration name decls
+parseModulePath :: P.Parsec String ParseState ModulePath
+parseModulePath = ModulePath <$> properName `sepBy1` dot
+
+parseImportDeclaration :: P.Parsec String ParseState Declaration
+parseImportDeclaration = do
+ reserved "import"
+ indented
+ modulePath <- parseModulePath
+ idents <- P.optionMaybe $ parens $ commaSep1 parseIdent
+ return $ ImportDeclaration modulePath idents
+
parseDeclaration :: P.Parsec String ParseState Declaration
parseDeclaration = P.choice
[ parseDataDeclaration
@@ -104,7 +116,8 @@ parseDeclaration = P.choice
, parseValueDeclaration
, parseExternDeclaration
, parseFixityDeclaration
- , parseModuleDeclaration ] P.<?> "declaration"
+ , parseModuleDeclaration
+ , parseImportDeclaration ] P.<?> "declaration"
parseDeclarations :: P.Parsec String ParseState [Declaration]
parseDeclarations = whiteSpace *> mark (P.many (same *> parseDeclaration)) <* P.eof
diff --git a/src/Language/PureScript/Parser/Types.hs b/src/Language/PureScript/Parser/Types.hs
index 156a9fd..6fa2ba4 100644
--- a/src/Language/PureScript/Parser/Types.hs
+++ b/src/Language/PureScript/Parser/Types.hs
@@ -25,6 +25,7 @@ import Control.Applicative
import qualified Text.Parsec as P
import qualified Text.Parsec.Expr as P
import Control.Arrow (Arrow(..))
+import Control.Monad (unless)
parseNumber :: P.Parsec String ParseState Type
parseNumber = const Number <$> reserved "Number"
@@ -43,7 +44,7 @@ parseObject = braces $ Object <$> parseRow
parseFunction :: P.Parsec String ParseState Type
parseFunction = do
- args <- lexeme $ parens $ commaSep parseType
+ args <- lexeme $ parens $ commaSep parsePolyType
lexeme $ P.string "->"
resultType <- parseType
return $ Function args resultType
@@ -54,6 +55,10 @@ parseTypeVariable = TypeVar <$> identifier
parseTypeConstructor :: P.Parsec String ParseState Type
parseTypeConstructor = TypeConstructor <$> parseQualified properName
+parseForAll :: P.Parsec String ParseState Type
+parseForAll = (mkForAll <$> (P.try (reserved "forall") *> P.many1 (indented *> identifier) <* indented <* dot)
+ <*> parseType)
+
parseTypeAtom :: P.Parsec String ParseState Type
parseTypeAtom = indented *> P.choice (map P.try
[ parseNumber
@@ -64,27 +69,36 @@ parseTypeAtom = indented *> P.choice (map P.try
, parseFunction
, parseTypeVariable
, parseTypeConstructor
+ , parseForAll
, parens parseType ])
-parsePolyType :: P.Parsec String ParseState PolyType
-parsePolyType = (PolyType <$> P.option [] (indented *> reserved "forall" *> many (indented *> identifier) <* indented <* dot)
- <*> parseType) P.<?> "polymorphic type"
-
-parseType :: P.Parsec String ParseState Type
-parseType = (P.buildExpressionParser operators . buildPostfixParser postfixTable $ parseTypeAtom) P.<?> "type"
+parseAnyType :: P.Parsec String ParseState Type
+parseAnyType = (P.buildExpressionParser operators . buildPostfixParser postfixTable $ parseTypeAtom) P.<?> "type"
where
postfixTable :: [P.Parsec String ParseState (Type -> Type)]
postfixTable = [ flip TypeApp <$> P.try (indented *> parseTypeAtom) ]
operators = [ [ P.Infix (lexeme (P.try (P.string "->")) >> return (\t1 t2 -> Function [t1] t2)) P.AssocRight ] ]
+parseType :: P.Parsec String ParseState Type
+parseType = do
+ ty <- parseAnyType
+ unless (isMonoType ty) $ P.unexpected "polymorphic type"
+ return ty
+
+parsePolyType :: P.Parsec String ParseState PolyType
+parsePolyType = do
+ ty <- parseAnyType
+ unless (isPolyType ty) $ P.unexpected "polymorphic type"
+ return ty
+
parseNameAndType :: P.Parsec String ParseState (String, Type)
-parseNameAndType = (,) <$> (indented *> identifier <* indented <* lexeme (P.string "::")) <*> parseType
+parseNameAndType = (,) <$> (indented *> identifier <* indented <* lexeme (P.string "::")) <*> parsePolyType
parseRowEnding :: P.Parsec String ParseState Row
parseRowEnding = P.option REmpty (RowVar <$> (lexeme (indented *> P.char '|') *> indented *> identifier))
parseRow :: P.Parsec String ParseState Row
-parseRow = (fromList <$> (parseNameAndType `P.sepBy` (indented *> comma)) <*> parseRowEnding) P.<?> "row"
+parseRow = (fromList <$> (commaSep parseNameAndType) <*> parseRowEnding) P.<?> "row"
where
fromList :: [(String, Type)] -> Row -> Row
fromList [] r = r
diff --git a/src/Language/PureScript/Parser/Values.hs b/src/Language/PureScript/Parser/Values.hs
index 6efb254..d1ae1a8 100644
--- a/src/Language/PureScript/Parser/Values.hs
+++ b/src/Language/PureScript/Parser/Values.hs
@@ -47,10 +47,10 @@ parseBooleanLiteral :: P.Parsec String ParseState Value
parseBooleanLiteral = BooleanLiteral <$> booleanLiteral
parseArrayLiteral :: P.Parsec String ParseState Value
-parseArrayLiteral = ArrayLiteral <$> C.squares (parseValue `P.sepBy` (C.indented *> C.comma))
+parseArrayLiteral = ArrayLiteral <$> C.squares (C.commaSep parseValue)
parseObjectLiteral :: P.Parsec String ParseState Value
-parseObjectLiteral = ObjectLiteral <$> C.braces (parseIdentifierAndValue `P.sepBy` (C.indented *> C.comma))
+parseObjectLiteral = ObjectLiteral <$> C.braces (C.commaSep parseIdentifierAndValue)
parseIdentifierAndValue :: P.Parsec String ParseState (String, Value)
parseIdentifierAndValue = (,) <$> (C.indented *> C.identifier <* C.indented <* C.colon)
@@ -66,7 +66,7 @@ parseAbs = do
where
manyArgs :: P.Parsec String ParseState (Value -> Value)
manyArgs = do
- args <- C.parens ((C.indented *> C.parseIdent) `P.sepBy` (C.indented *> C.comma))
+ args <- C.parens (C.commaSep C.parseIdent)
return $ Abs args
singleArg :: P.Parsec String ParseState (Value -> Value)
singleArg = Abs . return <$> C.parseIdent
@@ -76,7 +76,7 @@ parseAbs = do
parseApp :: P.Parsec String ParseState Value
parseApp = App <$> parseValue
- <*> (C.indented *> C.parens (parseValue `P.sepBy` (C.indented *> C.comma)))
+ <*> (C.indented *> C.parens (C.commaSep parseValue))
parseVar :: P.Parsec String ParseState Value
parseVar = Var <$> C.parseQualified C.parseIdent
@@ -134,9 +134,9 @@ parseValue =
where
indexersAndAccessors = C.buildPostfixParser postfixTable1 parseValueAtom
postfixTable1 = [ Accessor <$> (C.indented *> C.dot *> C.indented *> C.identifier)
- , P.try $ flip ObjectUpdate <$> (C.indented *> C.braces ((C.indented *> parsePropertyUpdate) `P.sepBy1` (C.indented *> C.comma))) ]
+ , P.try $ flip ObjectUpdate <$> (C.indented *> C.braces (C.commaSep1 (C.indented *> parsePropertyUpdate))) ]
postfixTable2 = [ P.try (C.indented *> indexersAndAccessors >>= \t2 -> return (\t1 -> App t1 [t2]))
- , P.try $ flip App <$> (C.indented *> C.parens (parseValue `P.sepBy` (C.indented *> C.comma)))
+ , P.try $ flip App <$> (C.indented *> C.parens (C.commaSep parseValue))
, flip TypedValue <$> (P.try (C.lexeme (C.indented *> P.string "::")) *> parsePolyType) ]
operators = [ [ Prefix $ C.lexeme (P.try $ C.indented *> C.reservedOp "!") >> return (Unary Not)
, Prefix $ C.lexeme (P.try $ C.indented *> C.reservedOp "~") >> return (Unary BitwiseNot)
@@ -221,10 +221,10 @@ parseUnaryBinder :: P.Parsec String ParseState Binder
parseUnaryBinder = UnaryBinder <$> C.lexeme (C.parseQualified C.properName) <*> (C.indented *> parseBinder)
parseObjectBinder :: P.Parsec String ParseState Binder
-parseObjectBinder = ObjectBinder <$> C.braces ((C.indented *> parseIdentifierAndBinder) `P.sepBy` (C.indented *> C.comma))
+parseObjectBinder = ObjectBinder <$> C.braces (C.commaSep (C.indented *> parseIdentifierAndBinder))
parseArrayBinder :: P.Parsec String ParseState Binder
-parseArrayBinder = C.squares $ ArrayBinder <$> ((C.indented *> parseBinder) `P.sepBy` (C.indented *> C.comma))
+parseArrayBinder = C.squares $ ArrayBinder <$> (C.commaSep (C.indented *> parseBinder))
<*> P.optionMaybe (C.indented *> C.colon *> C.indented *> parseBinder)
parseNamedBinder :: P.Parsec String ParseState Binder
diff --git a/src/Language/PureScript/Pretty/Kinds.hs b/src/Language/PureScript/Pretty/Kinds.hs
index 06dfb20..a1c9883 100644
--- a/src/Language/PureScript/Pretty/Kinds.hs
+++ b/src/Language/PureScript/Pretty/Kinds.hs
@@ -25,13 +25,14 @@ import Control.Applicative
import Language.PureScript.Kinds
import Language.PureScript.Pretty.Common
+import Language.PureScript.Unknown
typeLiterals :: Pattern () Kind String
typeLiterals = mkPattern match
where
match Star = Just "*"
match Row = Just "#"
- match (KUnknown u) = Just $ 'u' : show u
+ match (KUnknown (Unknown u)) = Just $ 'u' : show u
match _ = Nothing
funKind :: Pattern () Kind (Kind, Kind)
diff --git a/src/Language/PureScript/Pretty/Types.hs b/src/Language/PureScript/Pretty/Types.hs
index e987792..1babcc0 100644
--- a/src/Language/PureScript/Pretty/Types.hs
+++ b/src/Language/PureScript/Pretty/Types.hs
@@ -14,8 +14,7 @@
module Language.PureScript.Pretty.Types (
prettyPrintType,
- prettyPrintRow,
- prettyPrintPolyType
+ prettyPrintRow
) where
import Data.Maybe (fromMaybe)
@@ -31,6 +30,7 @@ import Language.PureScript.Names
import Language.PureScript.Declarations
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.Pretty.Common
+import Language.PureScript.Unknown
typeLiterals :: Pattern () Type String
typeLiterals = mkPattern match
@@ -42,8 +42,10 @@ typeLiterals = mkPattern match
match (Object row) = Just $ "{ " ++ prettyPrintRow row ++ " }"
match (TypeVar var) = Just var
match (TypeConstructor ctor) = Just $ show ctor
- match (TUnknown u) = Just $ 'u' : show u
+ match (TUnknown (Unknown u)) = Just $ 'u' : show u
+ match (Skolem s) = Just $ 's' : show s
match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"
+ match (ForAll ident ty) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty
match _ = Nothing
prettyPrintRow :: Row -> String
@@ -53,8 +55,9 @@ prettyPrintRow = (\(tys, tail) -> intercalate ", " (map (uncurry nameAndTypeToPs
nameAndTypeToPs name ty = name ++ " :: " ++ prettyPrintType ty
tailToPs :: Row -> String
tailToPs REmpty = ""
- tailToPs (RUnknown u) = " | " ++ show u
+ tailToPs (RUnknown (Unknown u)) = " | u" ++ show u
tailToPs (RowVar var) = " | " ++ var
+ tailToPs (RSkolem s) = " | s" ++ show s
toList :: [(String, Type)] -> Row -> ([(String, Type)], Row)
toList tys (RCons name ty row) = toList ((name, ty):tys) row
toList tys r = (tys, r)
@@ -89,7 +92,3 @@ prettyPrintType = fromMaybe (error "Incomplete pattern") . pattern matchType ()
, Wrap function $ \args ret -> "(" ++ intercalate ", " (map prettyPrintType args) ++ ") -> " ++ ret
]
]
-
-prettyPrintPolyType :: PolyType -> String
-prettyPrintPolyType (PolyType [] ty) = prettyPrintType ty
-prettyPrintPolyType (PolyType idents ty) = "forall " ++ unwords idents ++ ". " ++ prettyPrintType ty
diff --git a/src/Language/PureScript/Pretty/Values.hs b/src/Language/PureScript/Pretty/Values.hs
index 06a2f82..f37c29a 100644
--- a/src/Language/PureScript/Pretty/Values.hs
+++ b/src/Language/PureScript/Pretty/Values.hs
@@ -28,6 +28,7 @@ import Language.PureScript.Types
import Language.PureScript.Values
import Language.PureScript.Names
import Language.PureScript.Pretty.Common
+import Language.PureScript.Pretty.Types
literals :: Pattern () Value String
literals = mkPattern match
@@ -83,6 +84,12 @@ lam = mkPattern match
match (Abs args val) = Just (map show args, val)
match _ = Nothing
+typed :: Pattern () Value (PolyType, Value)
+typed = mkPattern match
+ where
+ match (TypedValue val ty) = Just (ty, val)
+ match _ = Nothing
+
unary :: UnaryOperator -> String -> Operator () Value String
unary op str = Wrap pattern (++)
where
@@ -113,6 +120,7 @@ prettyPrintValue = fromMaybe (error "Incomplete pattern") . pattern matchValue (
, [ Wrap app $ \args val -> val ++ "(" ++ args ++ ")" ]
, [ Split lam $ \args val -> "\\" ++ intercalate ", " args ++ " -> " ++ prettyPrintValue val ]
, [ Wrap ifThenElse $ \(th, el) cond -> cond ++ " ? " ++ prettyPrintValue th ++ " : " ++ prettyPrintValue el ]
+ , [ Wrap typed $ \ty val -> val ++ " :: " ++ prettyPrintType ty ]
, [ AssocR indexer (\index val -> val ++ " !! " ++ index) ]
, [ binary LessThan "<" ]
, [ binary LessThanOrEqualTo "<=" ]
@@ -147,7 +155,7 @@ prettyPrintBinder (BooleanBinder True) = "true"
prettyPrintBinder (BooleanBinder False) = "false"
prettyPrintBinder (VarBinder ident) = show ident
prettyPrintBinder (NullaryBinder ctor) = show ctor
-prettyPrintBinder (UnaryBinder ctor b) = show ctor ++ prettyPrintBinder b
+prettyPrintBinder (UnaryBinder ctor b) = show ctor ++ " " ++ prettyPrintBinder b
prettyPrintBinder (ObjectBinder bs) = "{ " ++ intercalate ", " (map (uncurry prettyPrintObjectPropertyBinder) bs) ++ " }"
prettyPrintBinder (ArrayBinder bs rest) = "[ " ++ intercalate ", " (map prettyPrintBinder bs) ++ maybe "" (("; " ++) . prettyPrintBinder) rest ++ " ]"
prettyPrintBinder (NamedBinder ident binder) = show ident ++ "@" ++ prettyPrintBinder binder
diff --git a/src/Language/PureScript/TypeChecker.hs b/src/Language/PureScript/TypeChecker.hs
index 8de9dbc..eff76f7 100644
--- a/src/Language/PureScript/TypeChecker.hs
+++ b/src/Language/PureScript/TypeChecker.hs
@@ -42,23 +42,23 @@ import Control.Monad.Error
typeCheckAll :: [Declaration] -> Check ()
typeCheckAll [] = return ()
typeCheckAll (DataDeclaration name args dctors : rest) = do
- rethrow (("Error in type constructor " ++ show name ++ ": ") ++) $ do
+ rethrow (("Error in type constructor " ++ show name ++ ":\n") ++) $ do
env <- getEnv
modulePath <- checkModulePath `fmap` get
guardWith (show name ++ " is already defined") $ not $ M.member (modulePath, name) (types env)
ctorKind <- kindsOf (Just name) args (mapMaybe snd dctors)
putEnv $ env { types = M.insert (modulePath, name) (ctorKind, Data) (types env) }
forM_ dctors $ \(dctor, maybeTy) ->
- rethrow (("Error in data constructor " ++ show name ++ ": ") ++) $ do
+ rethrow (("Error in data constructor " ++ show name ++ ":\n") ++) $ do
env' <- getEnv
guardWith (show dctor ++ " is already defined") $ not $ M.member (modulePath, dctor) (dataConstructors env')
let retTy = foldl TypeApp (TypeConstructor (Qualified modulePath name)) (map TypeVar args)
let dctorTy = maybe retTy (\ty -> Function [ty] retTy) maybeTy
- let polyType = PolyType args dctorTy
+ let polyType = mkForAll args dctorTy
putEnv $ env' { dataConstructors = M.insert (modulePath, dctor) polyType (dataConstructors env') }
typeCheckAll rest
typeCheckAll (TypeSynonymDeclaration name args ty : rest) = do
- rethrow (("Error in type synonym " ++ show name ++ ": ") ++) $ do
+ rethrow (("Error in type synonym " ++ show name ++ ":\n") ++) $ do
env <- getEnv
modulePath <- checkModulePath `fmap` get
guardWith (show name ++ " is already defined") $ not $ M.member (modulePath, name) (types env)
@@ -70,13 +70,13 @@ typeCheckAll (TypeDeclaration name ty : ValueDeclaration name' val : rest) | nam
typeCheckAll (ValueDeclaration name (TypedValue val ty) : rest)
typeCheckAll (TypeDeclaration name _ : _) = throwError $ "Orphan type declaration for " ++ show name
typeCheckAll (ValueDeclaration name val : rest) = do
- rethrow (("Error in declaration " ++ show name ++ ": ") ++) $ do
+ rethrow (("Error in declaration " ++ show name ++ ":\n") ++) $ do
env <- getEnv
modulePath <- checkModulePath `fmap` get
case M.lookup (modulePath, name) (names env) of
Just ty -> throwError $ show name ++ " is already defined"
Nothing -> do
- ty <- typeOf name val
+ ty <- typeOf (Just name) val
putEnv (env { names = M.insert (modulePath, name) (ty, Value) (names env) })
typeCheckAll rest
typeCheckAll (ExternDataDeclaration name kind : rest) = do
@@ -86,7 +86,7 @@ typeCheckAll (ExternDataDeclaration name kind : rest) = do
putEnv $ env { types = M.insert (modulePath, name) (kind, TypeSynonym) (types env) }
typeCheckAll rest
typeCheckAll (ExternMemberDeclaration member name ty : rest) = do
- rethrow (("Error in foreign import member declaration " ++ show name ++ ": ") ++) $ do
+ rethrow (("Error in foreign import member declaration " ++ show name ++ ":\n") ++) $ do
env <- getEnv
modulePath <- checkModulePath `fmap` get
kind <- kindOf ty
@@ -94,13 +94,17 @@ typeCheckAll (ExternMemberDeclaration member name ty : rest) = do
case M.lookup (modulePath, name) (names env) of
Just _ -> throwError $ show name ++ " is already defined"
Nothing -> case ty of
- (PolyType _ (Function [_] _)) -> do
+ _ | isSingleArgumentFunction ty -> do
putEnv (env { names = M.insert (modulePath, name) (ty, Extern) (names env)
, members = M.insert (modulePath, name) member (members env) })
- _ -> throwError "Foreign member declarations must have function types, with an single argument."
+ | otherwise -> throwError "Foreign member declarations must have function types, with an single argument."
typeCheckAll rest
+ where
+ isSingleArgumentFunction (Function [_] _) = True
+ isSingleArgumentFunction (ForAll _ ty) = isSingleArgumentFunction ty
+ isSingleArgumentFunction _ = False
typeCheckAll (ExternDeclaration name ty : rest) = do
- rethrow (("Error in foreign import declaration " ++ show name ++ ": ") ++) $ do
+ rethrow (("Error in foreign import declaration " ++ show name ++ ":\n") ++) $ do
env <- getEnv
modulePath <- checkModulePath `fmap` get
kind <- kindOf ty
@@ -117,3 +121,21 @@ typeCheckAll (FixityDeclaration _ name : rest) = do
typeCheckAll (ModuleDeclaration name decls : rest) = do
withModule name $ typeCheckAll decls
typeCheckAll rest
+typeCheckAll (ImportDeclaration modulePath idents : rest) = do
+ env <- getEnv
+ currentModule <- checkModulePath `fmap` get
+ rethrow errorMessage $ do
+ guardWith ("Module " ++ show modulePath ++ " does not exist") $ moduleExists env
+ case idents of
+ Nothing -> bindIdents (map snd $ filterModule env) currentModule env
+ Just idents -> bindIdents idents currentModule env
+ typeCheckAll rest
+ where errorMessage = (("Error in import declaration " ++ show modulePath ++ ":\n") ++)
+ filterModule = filter ((== modulePath) . fst) . M.keys . names
+ moduleExists env = not $ null $ filterModule env
+ bindIdents idents currentModule env =
+ forM_ idents $ \ident -> do
+ guardWith (show currentModule ++ "." ++ show ident ++ " is already defined") $ (currentModule, ident) `M.notMember` names env
+ case (modulePath, ident) `M.lookup` names env of
+ Just (pt, _) -> modifyEnv (\e -> e { names = M.insert (currentModule, ident) (pt, Alias modulePath ident) (names e) })
+ Nothing -> throwError (show modulePath ++ "." ++ show ident ++ " is undefined")
diff --git a/src/Language/PureScript/TypeChecker/Kinds.hs b/src/Language/PureScript/TypeChecker/Kinds.hs
index 92caf37..94f4600 100644
--- a/src/Language/PureScript/TypeChecker/Kinds.hs
+++ b/src/Language/PureScript/TypeChecker/Kinds.hs
@@ -15,8 +15,6 @@
{-# LANGUAGE DeriveDataTypeable #-}
module Language.PureScript.TypeChecker.Kinds (
- KindConstraint(..),
- KindSolution(..),
kindsOf,
kindOf
) where
@@ -32,6 +30,7 @@ import Language.PureScript.Names
import Language.PureScript.Declarations
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.Pretty
+import Language.PureScript.Unknown
import Control.Monad.State
import Control.Monad.Error
@@ -42,146 +41,92 @@ import qualified Control.Category as C
import qualified Data.Map as M
-data KindConstraintOrigin
- = DataDeclOrigin
- | TypeOrigin Type
- | RowOrigin Row deriving (Show, Data, Typeable)
-
-prettyPrintKindConstraintOrigin :: KindConstraintOrigin -> String
-prettyPrintKindConstraintOrigin (DataDeclOrigin) = "data declaration"
-prettyPrintKindConstraintOrigin (TypeOrigin ty) = prettyPrintType ty
-prettyPrintKindConstraintOrigin (RowOrigin row) = prettyPrintRow row
-
-data KindConstraint = KindConstraint Int Kind KindConstraintOrigin deriving (Show, Data, Typeable)
-
-newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }
-
-emptyKindSolution :: KindSolution
-emptyKindSolution = KindSolution KUnknown
-
-kindOf :: PolyType -> Check Kind
-kindOf (PolyType idents ty) = do
- ns <- replicateM (length idents) fresh
- (cs, n, m) <- kindConstraints Nothing (M.fromList (zip idents ns)) ty
- solution <- solveKindConstraints cs emptyKindSolution
- return $ starIfUnknown $ runKindSolution solution n
+instance Unifiable Kind where
+ unknown = KUnknown
+ isUnknown (KUnknown u) = Just u
+ isUnknown _ = Nothing
+ KUnknown u1 ~~ KUnknown u2 | u1 == u2 = return ()
+ KUnknown u ~~ k = replace u k
+ k ~~ KUnknown u = replace u k
+ Star ~~ Star = return ()
+ Row ~~ Row = return ()
+ FunKind k1 k2 ~~ FunKind k3 k4 = do
+ k1 ~~ k3
+ k2 ~~ k4
+ k1 ~~ k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
+ apply s (KUnknown u) = runSubstitution s u
+ apply s (FunKind k1 k2) = FunKind (apply s k1) (apply s k2)
+ apply _ k = k
+ unknowns (KUnknown (Unknown u)) = [u]
+ unknowns (FunKind k1 k2) = unknowns k1 ++ unknowns k2
+ unknowns _ = []
+
+kindOf :: Type -> Check Kind
+kindOf ty = fmap (\(k, _, _) -> k) . runSubst $ starIfUnknown <$> infer Nothing M.empty ty
kindsOf :: Maybe ProperName -> [String] -> [Type] -> Check Kind
-kindsOf name args ts = do
+kindsOf name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst $ do
tyCon <- fresh
- nargs <- replicateM (length args) fresh
- (cs, ns, m) <- kindConstraintsAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args nargs)) ts
- let extraConstraints =
- KindConstraint tyCon (foldr (FunKind . KUnknown) Star nargs) DataDeclOrigin
- : zipWith (\n arg -> KindConstraint n Star (TypeOrigin arg)) ns ts
- solution <- solveKindConstraints (extraConstraints ++ cs) emptyKindSolution
- return $ starIfUnknown $ runKindSolution solution tyCon
+ kargs <- replicateM (length args) fresh
+ ks <- inferAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args kargs)) ts
+ tyCon ~~ foldr FunKind Star kargs
+ forM_ ks $ \k -> k ~~ Star
+ return tyCon
starIfUnknown :: Kind -> Kind
starIfUnknown (KUnknown _) = Star
starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
starIfUnknown k = k
-kindConstraintsAll :: Maybe (ProperName, Int) -> M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], M.Map String Int)
-kindConstraintsAll _ m [] = return ([], [], m)
-kindConstraintsAll name m (t:ts) = do
- (cs, n1, m') <- kindConstraints name m t
- (cs', ns, m'') <- kindConstraintsAll name m' ts
- return (KindConstraint n1 Star (TypeOrigin t) : cs ++ cs', n1:ns, m'')
-
-kindConstraints :: Maybe (ProperName, Int) -> M.Map String Int -> Type -> Check ([KindConstraint], Int, M.Map String Int)
-kindConstraints name m a@(Array t) = do
- me <- fresh
- (cs, n1, m') <- kindConstraints name m t
- return (KindConstraint n1 Star (TypeOrigin t) : KindConstraint me Star (TypeOrigin a) : cs, me, m')
-kindConstraints name m o@(Object row) = do
- me <- fresh
- (cs, r, m') <- kindConstraintsForRow name m row
- return (KindConstraint me Star (TypeOrigin o) : KindConstraint r Row (RowOrigin row) : cs, me, m')
-kindConstraints name m f@(Function args ret) = do
- me <- fresh
- (cs, ns, m') <- kindConstraintsAll name m args
- (cs', retN, m'') <- kindConstraints name m' ret
- return (KindConstraint retN Star (TypeOrigin ret) : KindConstraint me Star (TypeOrigin f) : zipWith (\n arg -> KindConstraint n Star (TypeOrigin arg)) ns args ++ cs ++ cs', me, m'')
-kindConstraints _ m (TypeVar v) =
+inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst Check [Kind]
+inferAll name m = mapM (infer name m)
+
+infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Check Kind
+infer name m (Array t) = do
+ k <- infer name m t
+ k ~~ Star
+ return Star
+infer name m (Object row) = do
+ k <- inferRow name m row
+ k ~~ Row
+ return Star
+infer name m (Function args ret) = do
+ ks <- inferAll name m args
+ k <- infer name m ret
+ k ~~ Star
+ forM ks $ \k -> k ~~ Star
+ return Star
+infer _ m (TypeVar v) =
case M.lookup v m of
- Just u -> return ([], u, m)
+ Just k -> return k
Nothing -> throwError $ "Unbound type variable " ++ v
-kindConstraints (Just (name, u)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = do
- env <- getEnv
- me <- fresh
- modulePath <- checkModulePath `fmap` get
- return ([KindConstraint me (KUnknown u) (TypeOrigin c)], me, m)
-kindConstraints name m c@(TypeConstructor v) = do
- env <- getEnv
- me <- fresh
- modulePath <- checkModulePath `fmap` get
+infer (Just (name, k)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = return k
+infer name m (TypeConstructor v) = do
+ env <- lift getEnv
+ modulePath <- checkModulePath `fmap` lift get
case M.lookup (qualify modulePath v) (types env) of
Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"
- Just (kind, _) -> return ([KindConstraint me kind (TypeOrigin c)], me, m)
-kindConstraints name m a@(TypeApp t1 t2) = do
- me <- fresh
- (cs1, n1, m1) <- kindConstraints name m t1
- (cs2, n2, m2) <- kindConstraints name m1 t2
- return (KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me)) (TypeOrigin a) : cs1 ++ cs2, me, m2)
-kindConstraints _ m t = do
- me <- fresh
- return ([KindConstraint me Star (TypeOrigin t)], me, m)
-
-kindConstraintsForRow :: Maybe (ProperName, Int) -> M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
-kindConstraintsForRow _ m r@(RowVar v) = do
- me <- case M.lookup v m of
- Just u -> return u
- Nothing -> fresh
- return ([KindConstraint me Row (RowOrigin r)], me, M.insert v me m)
-kindConstraintsForRow _ m r@REmpty = do
- me <- fresh
- return ([KindConstraint me Row (RowOrigin r)], me, m)
-kindConstraintsForRow name m r@(RCons _ ty row) = do
- me <- fresh
- (cs1, n1, m1) <- kindConstraints name m ty
- (cs2, n2, m2) <- kindConstraintsForRow name m1 row
- return (KindConstraint me Row (RowOrigin r) : KindConstraint n1 Star (TypeOrigin ty) : KindConstraint n2 Row (RowOrigin r) : cs1 ++ cs2, me, m2)
-
-solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
-solveKindConstraints [] s = return s
-solveKindConstraints all@(KindConstraint n k t : cs) s = do
- (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintKindConstraintOrigin t ++ ": " ++ err) $ do
- guardWith "Occurs check failed" $ not $ kindOccursCheck False n k
- let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
- cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
- return (cs', s')
- solveKindConstraints cs' s'
-
-substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
-substituteKindConstraint n k (KindConstraint m l t)
- | n == m = unifyKinds t k l
- | otherwise = return [KindConstraint m (replaceUnknownKind n k l) t]
-
-replaceUnknownKind :: Int -> Kind -> Kind -> Kind
-replaceUnknownKind n k = f
- where
- f (KUnknown m) | m == n = k
- f (FunKind k1 k2) = FunKind (f k2) (f k2)
- f other = other
-
-unifyKinds :: KindConstraintOrigin -> Kind -> Kind -> Check [KindConstraint]
-unifyKinds _ (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
-unifyKinds t (KUnknown u) k = do
- guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
- return [KindConstraint u k t]
-unifyKinds t k (KUnknown u) = do
- guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
- return [KindConstraint u k t]
-unifyKinds _ Star Star = return []
-unifyKinds _ Row Row = return []
-unifyKinds t (FunKind k1 k2) (FunKind k3 k4) = do
- cs1 <- unifyKinds t k1 k3
- cs2 <- unifyKinds t k2 k4
- return $ cs1 ++ cs2
-unifyKinds _ k1 k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
-
-kindOccursCheck :: Bool -> Int -> Kind -> Bool
-kindOccursCheck b u (KUnknown u') | u == u' = b
-kindOccursCheck _ u (FunKind k1 k2) = kindOccursCheck True u k1 || kindOccursCheck True u k2
-kindOccursCheck _ _ _ = False
+ Just (kind, _) -> return kind
+infer name m (TypeApp t1 t2) = do
+ k0 <- fresh
+ k1 <- infer name m t1
+ k2 <- infer name m t2
+ k1 ~~ FunKind k2 k0
+ return k0
+infer name m (ForAll ident ty) = do
+ k <- fresh
+ infer name (M.insert ident k m) ty
+infer _ m t = return Star
+
+inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Check Kind
+inferRow _ m (RowVar v) = do
+ case M.lookup v m of
+ Just k -> return k
+ Nothing -> throwError $ "Unbound row variable " ++ v
+inferRow _ m r@REmpty = return Row
+inferRow name m r@(RCons _ ty row) = do
+ k1 <- infer name m ty
+ k2 <- inferRow name m row
+ k1 ~~ Star
+ k2 ~~ Row
+ return Row
diff --git a/src/Language/PureScript/TypeChecker/Monad.hs b/src/Language/PureScript/TypeChecker/Monad.hs
index 7d57bc6..213708b 100644
--- a/src/Language/PureScript/TypeChecker/Monad.hs
+++ b/src/Language/PureScript/TypeChecker/Monad.hs
@@ -12,14 +12,20 @@
--
-----------------------------------------------------------------------------
-{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances, RankNTypes, DeriveDataTypeable,
+ GADTs, StandaloneDeriving, MultiParamTypeClasses, FlexibleContexts #-}
module Language.PureScript.TypeChecker.Monad where
import Language.PureScript.Types
import Language.PureScript.Kinds
import Language.PureScript.Names
+import Language.PureScript.Unknown
+import Data.Data
+import Data.Maybe
+import Data.Monoid
+import Data.Typeable
import Control.Applicative
import Control.Monad.State
import Control.Monad.Error
@@ -28,14 +34,14 @@ import Control.Arrow ((***), first, second)
import qualified Data.Map as M
-data NameKind = Value | Extern deriving Show
+data NameKind = Value | Extern | Alias ModulePath Ident deriving Show
data TypeDeclarationKind = Data | ExternData | TypeSynonym deriving Show
data Environment = Environment
- { names :: M.Map (ModulePath, Ident) (PolyType, NameKind)
+ { names :: M.Map (ModulePath, Ident) (Type, NameKind)
, types :: M.Map (ModulePath, ProperName) (Kind, TypeDeclarationKind)
- , dataConstructors :: M.Map (ModulePath, ProperName) PolyType
+ , dataConstructors :: M.Map (ModulePath, ProperName) Type
, typeSynonyms :: M.Map (ModulePath, ProperName) ([String], Type)
, members :: M.Map (ModulePath, Ident) String
} deriving (Show)
@@ -43,10 +49,13 @@ data Environment = Environment
emptyEnvironment :: Environment
emptyEnvironment = Environment M.empty M.empty M.empty M.empty M.empty
+data AnyUnifiable where
+ AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable
+
data CheckState = CheckState { checkEnv :: Environment
, checkNextVar :: Int
, checkModulePath :: ModulePath
- } deriving (Show)
+ }
newtype Check a = Check { unCheck :: StateT CheckState (Either String) a }
deriving (Functor, Monad, Applicative, MonadPlus, MonadState CheckState, MonadError String)
@@ -57,14 +66,13 @@ getEnv = fmap checkEnv get
putEnv :: Environment -> Check ()
putEnv env = modify (\s -> s { checkEnv = env })
-fresh :: Check Int
-fresh = do
- st <- get
- put $ st { checkNextVar = checkNextVar st + 1 }
- return $ checkNextVar st
+modifyEnv :: (Environment -> Environment) -> Check ()
+modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })
-check :: Check a -> Either String (a, Environment)
-check = fmap (second checkEnv) . flip runStateT (CheckState emptyEnvironment 0 global) . unCheck
+runCheck :: Check a -> Either String (a, Environment)
+runCheck c = do
+ (a, s) <- flip runStateT (CheckState emptyEnvironment 0 global) $ unCheck c
+ return (a, checkEnv s)
guardWith :: (MonadError e m) => e -> Bool -> m ()
guardWith _ True = return ()
@@ -80,3 +88,69 @@ withModule name act = do
a <- act
modify $ \s -> s { checkModulePath = original }
return a
+
+newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }
+
+instance Monoid Substitution where
+ mempty = Substitution unknown
+ s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))
+
+data SubstState = SubstState { substSubst :: Substitution
+ , substFutureEscapeChecks :: [AnyUnifiable] }
+
+newtype Subst m a = Subst { unSubst :: StateT SubstState m a }
+ deriving (Functor, Monad, Applicative, MonadPlus, MonadTrans)
+
+deriving instance (MonadError String m) => MonadError String (Subst m)
+
+runSubst :: (Unifiable a, Monad m) => Subst m a -> m (a, Substitution, [AnyUnifiable])
+runSubst subst = do
+ (a, s) <- flip runStateT (SubstState mempty []) . unSubst $ subst
+ return (apply (substSubst s) a, substSubst s, substFutureEscapeChecks s)
+
+substituteWith :: (Typeable t) => (Unknown t -> t) -> Substitution
+substituteWith f = Substitution $ \u -> fromMaybe (unknown u) $ do
+ u1 <- cast u
+ cast (f u1)
+
+substituteOne :: (Unifiable t) => Unknown t -> t -> Substitution
+substituteOne u t = substituteWith $ \u1 ->
+ case u1 of
+ u2 | u2 == u -> t
+ | otherwise -> unknown u2
+
+replace :: (Unifiable t) => Unknown t -> t -> Subst Check ()
+replace u t' = do
+ sub <- substSubst <$> Subst get
+ let t = apply sub t'
+ occursCheck u t
+ let current = apply sub $ unknown u
+ case isUnknown current of
+ Just u1 | u1 == u -> return ()
+ _ -> current ~~ t
+ Subst . modify $ \s -> s { substSubst = substituteOne u t <> substSubst s }
+
+class (Typeable t, Data t, Show t) => Unifiable t where
+ unknown :: Unknown t -> t
+ (~~) :: t -> t -> Subst Check ()
+ isUnknown :: t -> Maybe (Unknown t)
+ apply :: Substitution -> t -> t
+ unknowns :: t -> [Int]
+
+occursCheck :: (Unifiable t) => Unknown s -> t -> Subst Check ()
+occursCheck (Unknown u) t =
+ case isUnknown t of
+ Nothing -> guardWith "Occurs check fails" (u `notElem` unknowns t)
+ _ -> return ()
+
+fresh' :: Subst Check Int
+fresh' = do
+ n <- lift $ checkNextVar <$> get
+ lift . modify $ \s -> s { checkNextVar = succ (checkNextVar s) }
+ return n
+
+fresh :: (Unifiable t) => Subst Check t
+fresh = unknown . Unknown <$> fresh'
+
+escapeCheckLater :: (Unifiable t) => t -> Subst Check ()
+escapeCheckLater t = Subst . modify $ \s -> s { substFutureEscapeChecks = AnyUnifiable t : substFutureEscapeChecks s }
diff --git a/src/Language/PureScript/TypeChecker/Types.hs b/src/Language/PureScript/TypeChecker/Types.hs
index fcd8c01..b814d2c 100644
--- a/src/Language/PureScript/TypeChecker/Types.hs
+++ b/src/Language/PureScript/TypeChecker/Types.hs
@@ -15,17 +15,16 @@
{-# LANGUAGE DeriveDataTypeable #-}
module Language.PureScript.TypeChecker.Types (
- TypeConstraint(..),
- TypeSolution(..),
typeOf
) where
-import Debug.Trace
-
import Data.List
+import Data.Maybe (isJust, fromMaybe)
import Data.Function
import qualified Data.Data as D
-import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
+import Data.Generics
+ (extT, something, everywhere, everywhereM, everything,
+ everywhereBut, mkT, mkM, mkQ, extM, extQ)
import Language.PureScript.Values
import Language.PureScript.Types
@@ -35,72 +34,160 @@ import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Kinds
import Language.PureScript.TypeChecker.Synonyms
import Language.PureScript.Pretty
+import Language.PureScript.Unknown
import Control.Monad.State
import Control.Monad.Error
import Control.Applicative
-import Control.Arrow (Kleisli(..), (***), (&&&), first)
+import Control.Arrow (Arrow(..), Kleisli(..), (***), (&&&), second)
import qualified Control.Category as C
import qualified Data.Map as M
-data TypeConstraintOrigin
- = ValueOrigin Value
- | BinderOrigin Binder
- | AssignmentTargetOrigin Ident deriving (Show, D.Data, D.Typeable)
-
-prettyPrintOrigin :: TypeConstraintOrigin -> String
-prettyPrintOrigin (ValueOrigin val) = prettyPrintValue val
-prettyPrintOrigin (BinderOrigin binder) = prettyPrintBinder binder
-prettyPrintOrigin (AssignmentTargetOrigin ident) = show ident
-
-data TypeConstraint
- = TypeConstraint Int Type TypeConstraintOrigin
- | RowConstraint Int Row TypeConstraintOrigin deriving (Show, D.Data, D.Typeable)
-
-newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
-
-emptyTypeSolution :: TypeSolution
-emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
+instance Unifiable Type where
+ unknown = TUnknown
+ isUnknown (TUnknown u) = Just u
+ isUnknown _ = Nothing
+ (~~) = unifyTypes
+ apply s (TUnknown u) = runSubstitution s u
+ apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
+ apply s (ForAll idents ty) = ForAll idents $ apply s ty
+ apply s (Array t) = Array (apply s t)
+ apply s (Object r) = Object (apply s r)
+ apply s (Function args ret) = Function (map (apply s) args) (apply s ret)
+ apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)
+ apply _ t = t
+ unknowns (TUnknown (Unknown u)) = [u]
+ unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys
+ unknowns (ForAll idents ty) = unknowns ty
+ unknowns (Array t) = unknowns t
+ unknowns (Object r) = unknowns r
+ unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret
+ unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2
+ unknowns _ = []
+
+instance Unifiable Row where
+ unknown = RUnknown
+ isUnknown (RUnknown u) = Just u
+ isUnknown _ = Nothing
+ r1 ~~ r2 =
+ 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 do
+ forM_ int (uncurry (~~))
+ unifyRows sd1 r1' sd2 r2'
+ where
+ unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst Check ()
+ unifyRows [] (RUnknown u) sd r = replace u (rowFromList (sd, r))
+ unifyRows sd r [] (RUnknown u) = replace u (rowFromList (sd, r))
+ unifyRows ns@((name, ty):row) r others u@(RUnknown un) = do
+ occursCheck un ty
+ forM row $ \(_, ty) -> occursCheck un ty
+ u' <- fresh
+ u ~~ RCons name ty u'
+ unifyRows row r others u'
+ unifyRows [] REmpty [] REmpty = return ()
+ unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()
+ unifyRows [] (RSkolem s1) [] (RSkolem s2) | s1 == s2 = return ()
+ unifyRows sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
+ apply s (RUnknown u) = runSubstitution s u
+ apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)
+ apply _ r = r
+ unknowns (RUnknown (Unknown u)) = [u]
+ unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
+ unknowns _ = []
+
+unifyTypes :: Type -> Type -> Subst Check ()
+unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2 ++ ":\n" ++ e) $ do
+ unifyTypes' t1 t2
+ where
+ unifyTypes' (TUnknown u1) (TUnknown u2) | u1 == u2 = return ()
+ unifyTypes' (TUnknown u) t = replace u t
+ unifyTypes' t (TUnknown u) = replace u t
+ unifyTypes' (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2)
+ | name1 == name2 = zipWithM_ unifyTypes args1 args2
+ unifyTypes' (SaturatedTypeSynonym name args) ty = do
+ ty1 <- expandTypeSynonym name args
+ ty1 `unifyTypes` ty
+ unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty
+ unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do
+ sk <- skolemize ident1 ty1
+ replaced <- replaceVarWithUnknown ident2 ty2
+ sk `unifyTypes` replaced
+ unifyTypes' (ForAll ident ty1) ty2 = do
+ sk <- skolemize ident ty1
+ sk `unifyTypes` ty2
+ unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty
+ unifyTypes' Number Number = return ()
+ unifyTypes' String String = return ()
+ unifyTypes' Boolean Boolean = return ()
+ unifyTypes' (Array s) (Array t) = s `unifyTypes` t
+ unifyTypes' (Object row1) (Object row2) = row1 ~~ row2
+ unifyTypes' (Function args1 ret1) (Function args2 ret2) = do
+ guardWith "Function applied to incorrect number of args" $ length args1 == length args2
+ zipWithM_ unifyTypes args1 args2
+ ret1 `unifyTypes` ret2
+ unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
+ unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
+ modulePath <- checkModulePath `fmap` lift get
+ guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
+ unifyTypes' (TypeApp t1 t2) (TypeApp t3 t4) = do
+ t1 `unifyTypes` t3
+ t2 `unifyTypes` t4
+ unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()
+ unifyTypes' t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
isFunction :: Value -> Bool
isFunction (Abs _ _) = True
isFunction (TypedValue untyped _) = isFunction untyped
isFunction _ = False
-allConstraints :: Ident -> Value -> Check ([TypeConstraint], Int)
-allConstraints name val | isFunction val = do
- me <- fresh
- (cs, n) <- typeConstraints (M.singleton name me) val
- return (TypeConstraint me (TUnknown n) (ValueOrigin val): cs, n)
-allConstraints _ val = typeConstraints M.empty val
-
-typeOf :: Ident -> Value -> Check PolyType
+typeOf :: Maybe Ident -> Value -> Check Type
typeOf name val = do
- (cs, n) <- allConstraints name val
- desugared <- replaceAllTypeSynonyms cs
- solution <- solveTypeConstraints desugared emptyTypeSolution
- let ty = fst (runTypeSolution solution) n
- allUnknownsBecameQuantified desugared solution ty
+ (ty, sub, checks) <- runSubst $ case name of
+ Just ident | isFunction val ->
+ case val of
+ TypedValue val ty -> do
+ kind <- lift $ kindOf ty
+ guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+ ty' <- lift $ replaceAllTypeSynonyms ty
+ check (M.singleton ident ty) val ty'
+ return ty'
+ _ -> do
+ me <- fresh
+ ty <- infer (M.singleton ident me) val
+ ty ~~ me
+ return ty
+ _ -> infer M.empty val
+ escapeCheck checks ty sub
+ skolemEscapeCheck ty
return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
-allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
-allUnknownsBecameQuantified cs solution ty = do
+escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
+escapeCheck checks ty sub =
let
- typesMentioned = findUnknownTypes ty
- unknownTypes = nub $ flip concatMap cs $ \c -> case c of
- TypeConstraint u t _ -> u : findUnknownTypes t
- RowConstraint _ r _ -> findUnknownTypes r
- unsolvedTypes = filter (\n -> TUnknown n == fst (runTypeSolution solution) n) unknownTypes
- guardWith "Unsolved type variable" $ null $ unsolvedTypes \\ typesMentioned
- let
- rowsMentioned = findUnknownRows ty
- unknownRows = nub $ flip concatMap cs $ \c -> case c of
- TypeConstraint _ t _ -> findUnknownRows t
- RowConstraint u r _ -> u : findUnknownRows r
- unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
- guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
+ visibleUnknowns = nub $ unknowns ty
+ in
+ forM_ checks $ \check -> case check of
+ AnyUnifiable t -> do
+ let unsolvedUnknowns = nub . unknowns $ apply sub t
+ guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
+
+skolemEscapeCheck :: Type -> Check ()
+skolemEscapeCheck ty =
+ case something (extQ (mkQ Nothing findSkolems) findRSkolems) ty of
+ Nothing -> return ()
+ Just _ -> throwError "Skolem variables cannot escape. Consider adding a type signature."
+ where
+ findSkolems (Skolem _) = return ()
+ findSkolems _ = mzero
+ findRSkolems (RSkolem _) = return ()
+ findRSkolems _ = mzero
setify :: Row -> Row
setify = rowFromList . first (M.toList . M.fromList) . rowToList
@@ -108,86 +195,45 @@ setify = rowFromList . first (M.toList . M.fromList) . rowToList
setifyAll :: (D.Data d) => d -> d
setifyAll = everywhere (mkT setify)
-findUnknownTypes :: (D.Data d) => d -> [Int]
-findUnknownTypes = everything (++) (mkQ [] f)
- where
- f :: Type -> [Int]
- f (TUnknown n) = [n]
- f _ = []
-
-findTypeVars :: (D.Data d) => d -> [String]
-findTypeVars = everything (++) (mkQ [] f)
- where
- f :: Type -> [String]
- f (TypeVar v) = [v]
- f _ = []
-
-findUnknownRows :: (D.Data d) => d -> [Int]
-findUnknownRows = everything (++) (mkQ [] f)
- where
- f :: Row -> [Int]
- f (RUnknown n) = [n]
- f _ = []
-
-varIfUnknown :: Type -> PolyType
+varIfUnknown :: Type -> Type
varIfUnknown ty =
- let
- (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
- in
- PolyType (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
+ let unks = nub $ unknowns ty
+ toName = (:) 't' . show
+ ty' = everywhere (mkT rowToVar) . everywhere (mkT typeToVar) $ ty
+ typeToVar :: Type -> Type
+ typeToVar (TUnknown (Unknown u)) = TypeVar (toName u)
+ typeToVar t = t
+ rowToVar :: Row -> Row
+ rowToVar (RUnknown (Unknown u)) = RowVar (toName u)
+ rowToVar t = t
+ in mkForAll (sort . map toName $ unks) ty'
+
+replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
+replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
+
+replaceTypeVars :: (D.Data d) => String -> Type -> d -> d
+replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replace)
where
- f :: Type -> State (M.Map Int String) Type
- f (TUnknown n) = do
- m <- get
- case M.lookup n m of
- Nothing -> do
- let name = 't' : show (M.size m)
- put $ M.insert n name m
- return $ TypeVar name
- Just name -> return $ TypeVar name
- f t = return t
- g :: Row -> State (M.Map Int String) Row
- g (RUnknown n) = do
- m <- get
- case M.lookup n m of
- Nothing -> do
- let name = 'r' : show (M.size m)
- put $ M.insert n name m
- return $ RowVar name
- Just name -> return $ RowVar name
- g r = return r
-
-replaceTypeVars :: M.Map String Type -> Type -> Type
-replaceTypeVars m = everywhere (mkT replace)
- where
- replace (TypeVar v) = case M.lookup v m of
- Just ty -> ty
- _ -> TypeVar v
+ replace (TypeVar v) | v == name = t
replace t = t
+ isShadowed (ForAll v _) | v == name = True
+ isShadowed _ = False
-replaceVarsWithUnknowns :: [String] -> Type -> Check Type
-replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
+replaceRowVars :: (D.Data d) => String -> Row -> d -> d
+replaceRowVars name r = everywhere (mkT replace)
where
- f :: Type -> StateT (M.Map String Int) Check Type
- f (TypeVar var) | var `elem` idents = do
- m <- get
- n <- lift fresh
- case M.lookup var m of
- Nothing -> do
- put (M.insert var n m)
- return $ TUnknown n
- Just u -> return $ TUnknown u
- f t = return t
- g :: Row -> StateT (M.Map String Int) Check Row
- g (RowVar var) | var `elem` idents = do
- m <- get
- n <- lift fresh
- case M.lookup var m of
- Nothing -> do
- put (M.insert var n m)
- return $ RUnknown n
- Just u -> return $ RUnknown u
- g r = return r
+ replace (RowVar v) | v == name = r
+ replace t = t
+
+replaceAllVarsWithUnknowns :: Type -> Subst Check Type
+replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
+replaceAllVarsWithUnknowns ty = return ty
+
+replaceVarWithUnknown :: String -> Type -> Subst Check Type
+replaceVarWithUnknown ident ty = do
+ tu <- fresh
+ ru <- fresh
+ return $ replaceRowVars ident ru . replaceTypeVars ident tu $ ty
replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
replaceAllTypeSynonyms d = do
@@ -201,440 +247,532 @@ desaturateAllTypeSynonyms = everywhere (mkT replace)
replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
replace t = t
-replaceType :: (D.Data d) => Int -> Type -> d -> d
-replaceType n t = everywhere (mkT go)
- where
- go (TUnknown m) | m == n = t
- go t = t
-
-replaceRow :: (D.Data d) => Int -> Row -> d -> d
-replaceRow n r = everywhere (mkT go)
- where
- go (RUnknown m) | m == n = r
- go r = r
-
-typeOccursCheck :: Int -> Type -> Check ()
-typeOccursCheck u (TUnknown _) = return ()
-typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
-
-rowOccursCheck :: Int -> Row -> Check ()
-rowOccursCheck u (RUnknown _) = return ()
-rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
-
-occursCheck :: (D.Data d) => Int -> d -> Bool
-occursCheck u = everything (||) $ flip extQ g $ mkQ False f
- where
- f (TUnknown u') | u' == u = True
- f _ = False
- g (RUnknown u') | u' == u = True
- g _ = False
-
-typesToRow :: [(String, Type)] -> Row
-typesToRow [] = REmpty
-typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
+expandAllTypeSynonyms :: Type -> Subst Check Type
+expandAllTypeSynonyms (SaturatedTypeSynonym name args) = expandTypeSynonym name args >>= expandAllTypeSynonyms
+expandAllTypeSynonyms ty = return ty
-rowToList :: Row -> ([(String, Type)], Row)
-rowToList (RCons name ty row) = let (tys, rest) = rowToList row
- in ((name, ty):tys, rest)
-rowToList r = ([], r)
-
-rowFromList :: ([(String, Type)], Row) -> Row
-rowFromList ([], r) = r
-rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
+expandTypeSynonym :: Qualified ProperName -> [Type] -> Subst Check Type
+expandTypeSynonym name args = do
+ env <- lift getEnv
+ modulePath <- checkModulePath `fmap` lift get
+ case M.lookup (qualify modulePath name) (typeSynonyms env) of
+ Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body
+ Nothing -> error "Type synonym was not defined"
ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
-typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
-typeConstraints _ v@(NumericLiteral _) = do
- me <- fresh
- return ([TypeConstraint me Number (ValueOrigin v)], me)
-typeConstraints _ v@(StringLiteral _) = do
- me <- fresh
- return ([TypeConstraint me String (ValueOrigin v)], me)
-typeConstraints _ v@(BooleanLiteral _) = do
- me <- fresh
- return ([TypeConstraint me Boolean (ValueOrigin v)], me)
-typeConstraints m v@(ArrayLiteral vals) = do
- all <- mapM (typeConstraints m) vals
- let (cs, ns) = (concatMap fst &&& map snd) all
- me <- fresh
- return (cs ++ zipWith (\n el -> TypeConstraint me (Array $ TUnknown n) (ValueOrigin el)) ns vals, me)
-typeConstraints m u@(Unary op val) = do
- (cs, n1) <- typeConstraints m val
- me <- fresh
- return (cs ++ unaryOperatorConstraints u op n1 me, me)
-typeConstraints m b@(Binary op left right) = do
- (cs1, n1) <- typeConstraints m left
- (cs2, n2) <- typeConstraints m right
- me <- fresh
- return (cs1 ++ cs2 ++ binaryOperatorConstraints b op n1 n2 me, me)
-typeConstraints m v@(ObjectLiteral ps) = do
- ensureNoDuplicateProperties ps
- all <- mapM (typeConstraints m . snd) ps
- let (cs, ns) = (concatMap fst &&& map snd) all
- me <- fresh
- let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
- return (TypeConstraint me (Object (typesToRow tys)) (ValueOrigin v) : cs, me)
-typeConstraints m v@(ObjectUpdate o ps) = do
- ensureNoDuplicateProperties ps
- (cs1, n1) <- typeConstraints m o
- all <- mapM (typeConstraints m . snd) ps
- let (cs2, ns) = (concatMap fst &&& map snd) all
+infer :: M.Map Ident Type -> Value -> Subst Check Type
+infer m val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ do
+ ty <- infer' m val
+ escapeCheckLater ty
+ return ty
+
+infer' _ (NumericLiteral _) = return Number
+infer' _ (StringLiteral _) = return String
+infer' _ (BooleanLiteral _) = return Boolean
+infer' m (ArrayLiteral vals) = do
+ ts <- mapM (infer m) vals
+ arr <- fresh
+ forM_ ts $ \t -> arr ~~ Array t
+ return arr
+infer' m (Unary op val) = do
+ t <- infer m val
+ inferUnary op t
+infer' m (Binary op left right) = do
+ t1 <- infer m left
+ t2 <- infer m right
+ inferBinary op t1 t2
+infer' m (ObjectLiteral ps) = do
+ lift $ ensureNoDuplicateProperties ps
+ ts <- mapM (infer m . snd) ps
+ let fields = zipWith (\(name, _) t -> (name, t)) ps ts
+ return $ Object $ rowFromList (fields, REmpty)
+infer' m (ObjectUpdate o ps) = do
+ lift $ ensureNoDuplicateProperties ps
row <- fresh
- let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
- return (TypeConstraint n1 (Object (rowFromList (tys, RUnknown row))) (ValueOrigin v) : cs1 ++ cs2, n1)
-typeConstraints m v@(Indexer index val) = do
- (cs1, n1) <- typeConstraints m index
- (cs2, n2) <- typeConstraints m val
- me <- fresh
- return (TypeConstraint n1 Number (ValueOrigin index) : TypeConstraint n2 (Array (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
-typeConstraints m v@(Accessor prop val) = do
- (cs, n1) <- typeConstraints m val
- me <- fresh
- rest <- fresh
- return (TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest))) (ValueOrigin v) : cs, me)
-typeConstraints m v@(Abs args ret) = do
- ns <- replicateM (length args) fresh
- let m' = m `M.union` M.fromList (zip args ns)
- (cs, n') <- typeConstraints m' ret
- me <- fresh
- return (TypeConstraint me (Function (map TUnknown ns) (TUnknown n')) (ValueOrigin v) : cs, me)
-typeConstraints m v@(App f xs) = do
- (cs1, n1) <- typeConstraints m f
- all <- mapM (typeConstraints m) xs
- let (cs2, ns) = (concatMap fst &&& map snd) all
- me <- fresh
- return (TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
-typeConstraints m v@(Var var@(Qualified mp name)) = do
+ newTys <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer m . snd) ps
+ oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh
+ check m o $ Object $ rowFromList (oldTys, row)
+ return $ Object $ rowFromList (newTys, row)
+infer' m (Indexer index val) = do
+ el <- fresh
+ check m index Number
+ check m val (Array el)
+ return el
+infer' m (Accessor prop val) = do
+ obj <- infer m val
+ propTy <- inferProperty obj prop
+ case propTy of
+ Nothing -> do
+ field <- fresh
+ rest <- fresh
+ obj `subsumes` Object (RCons prop field rest)
+ return field
+ Just ty -> return ty
+infer' m (Abs args ret) = do
+ ts <- replicateM (length args) fresh
+ let m' = m `M.union` M.fromList (zip args ts)
+ body <- infer m' ret
+ return $ Function ts body
+infer' m app@(App _ _) = do
+ let (f, argss) = unfoldApplication app
+ ft <- infer m f
+ ret <- fresh
+ checkFunctionApplications m ft argss ret
+ return ret
+infer' m (Var var@(Qualified mp name)) = do
case mp of
ModulePath [] ->
case M.lookup name m of
- Just u -> do
- me <- fresh
- return ([TypeConstraint u (TUnknown me) (ValueOrigin v)], me)
+ Just ty -> lift $ replaceAllTypeSynonyms ty
Nothing -> lookupGlobal
_ -> lookupGlobal
where
lookupGlobal = do
- env <- getEnv
- modulePath <- checkModulePath `fmap` get
+ env <- lift getEnv
+ modulePath <- checkModulePath `fmap` lift get
case M.lookup (qualify modulePath var) (names env) of
Nothing -> throwError $ show var ++ " is undefined"
- Just (PolyType idents ty, _) -> do
- me <- fresh
- replaced <- replaceVarsWithUnknowns idents ty
- return ([TypeConstraint me replaced (ValueOrigin v)], me)
-typeConstraints m (Block ss) = do
+ Just (ty, _) -> lift $ replaceAllTypeSynonyms ty
+infer' m (Block ss) = do
ret <- fresh
- (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
+ (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
guardWith "Block is missing a return statement" allCodePathsReturn
- return (cs, ret)
-typeConstraints m v@(Constructor c) = do
- env <- getEnv
- modulePath <- checkModulePath `fmap` get
+ return ret
+infer' m (Constructor c) = do
+ env <- lift getEnv
+ modulePath <- checkModulePath `fmap` lift get
case M.lookup (qualify modulePath c) (dataConstructors env) of
Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
- Just (PolyType idents ty) -> do
- me <- fresh
- replaced <- replaceVarsWithUnknowns idents ty
- return ([TypeConstraint me replaced (ValueOrigin v)], me)
-typeConstraints m (Case val binders) = do
- (cs1, n1) <- typeConstraints m val
+ Just ty -> lift $ replaceAllTypeSynonyms ty
+infer' m (Case val binders) = do
+ t1 <- infer m val
ret <- fresh
- cs2 <- typeConstraintsForBinders m n1 ret binders
- return (cs1 ++ cs2, ret)
-typeConstraints m v@(IfThenElse cond th el) = do
- (cs1, n1) <- typeConstraints m cond
- (cs2, n2) <- typeConstraints m th
- (cs3, n3) <- typeConstraints m el
- return (TypeConstraint n1 Boolean (ValueOrigin cond) : TypeConstraint n2 (TUnknown n3) (ValueOrigin v) : cs1 ++ cs2 ++ cs3, n2)
-typeConstraints m v@(TypedValue val poly@(PolyType idents ty)) = do
- kind <- kindOf poly
+ checkBinders m t1 ret binders
+ return ret
+infer' m (IfThenElse cond th el) = do
+ check m cond Boolean
+ t2 <- infer m th
+ t3 <- infer m el
+ t2 ~~ t3
+ return t2
+infer' m (TypedValue val ty) = do
+ kind <- lift $ kindOf ty
guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
- (cs, n1) <- typeConstraints m val
- return (TypeConstraint n1 ty (ValueOrigin v) : cs, n1)
-
-unaryOperatorConstraints :: Value -> UnaryOperator -> Int -> Int -> [TypeConstraint]
-unaryOperatorConstraints v Negate val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
-unaryOperatorConstraints v Not val result = [TypeConstraint val Boolean (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
-unaryOperatorConstraints v BitwiseNot val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
-
-binaryOperatorConstraints :: Value -> BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
-binaryOperatorConstraints v Add = symBinOpConstraints v Number
-binaryOperatorConstraints v Subtract = symBinOpConstraints v Number
-binaryOperatorConstraints v Multiply = symBinOpConstraints v Number
-binaryOperatorConstraints v Divide = symBinOpConstraints v Number
-binaryOperatorConstraints v Modulus = symBinOpConstraints v Number
-binaryOperatorConstraints v LessThan = asymBinOpConstraints v Number Boolean
-binaryOperatorConstraints v LessThanOrEqualTo = asymBinOpConstraints v Number Boolean
-binaryOperatorConstraints v GreaterThan = asymBinOpConstraints v Number Boolean
-binaryOperatorConstraints v GreaterThanOrEqualTo = asymBinOpConstraints v Number Boolean
-binaryOperatorConstraints v BitwiseAnd = symBinOpConstraints v Number
-binaryOperatorConstraints v BitwiseOr = symBinOpConstraints v Number
-binaryOperatorConstraints v BitwiseXor = symBinOpConstraints v Number
-binaryOperatorConstraints v ShiftLeft = symBinOpConstraints v Number
-binaryOperatorConstraints v ShiftRight = symBinOpConstraints v Number
-binaryOperatorConstraints v ZeroFillShiftRight = symBinOpConstraints v Number
-binaryOperatorConstraints v EqualTo = equalityBinOpConstraints v
-binaryOperatorConstraints v NotEqualTo = equalityBinOpConstraints v
-binaryOperatorConstraints v And = symBinOpConstraints v Boolean
-binaryOperatorConstraints v Or = symBinOpConstraints v Boolean
-binaryOperatorConstraints v Concat = symBinOpConstraints v String
-
-equalityBinOpConstraints :: Value -> Int -> Int -> Int -> [TypeConstraint]
-equalityBinOpConstraints v left right result = [TypeConstraint left (TUnknown right) (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
-
-symBinOpConstraints :: Value -> Type -> Int -> Int -> Int -> [TypeConstraint]
-symBinOpConstraints v ty = asymBinOpConstraints v ty ty
-
-asymBinOpConstraints :: Value -> Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
-asymBinOpConstraints v ty res left right result = [TypeConstraint left ty (ValueOrigin v), TypeConstraint right ty (ValueOrigin v), TypeConstraint result res (ValueOrigin v)]
-
-typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
-typeConstraintsForBinder _ NullBinder = return ([], M.empty)
-typeConstraintsForBinder val b@(StringBinder _) = constantBinder b val String
-typeConstraintsForBinder val b@(NumberBinder _) = constantBinder b val Number
-typeConstraintsForBinder val b@(BooleanBinder _) = constantBinder b val Boolean
-typeConstraintsForBinder val b@(VarBinder name) = do
- me <- fresh
- return ([TypeConstraint me (TUnknown val) (BinderOrigin b)], M.singleton name me)
-typeConstraintsForBinder val b@(NullaryBinder ctor) = do
- env <- getEnv
- modulePath <- checkModulePath `fmap` get
+ ty' <- lift $ replaceAllTypeSynonyms ty
+ check m val ty'
+ return ty'
+
+inferProperty :: Type -> String -> Subst Check (Maybe Type)
+inferProperty (Object row) prop = do
+ let (props, _) = rowToList row
+ return $ lookup prop props
+inferProperty (SaturatedTypeSynonym name args) prop = do
+ replaced <- expandTypeSynonym name args
+ inferProperty replaced prop
+inferProperty (ForAll ident ty) prop = do
+ replaced <- replaceVarWithUnknown ident ty
+ inferProperty replaced prop
+inferProperty _ prop = return Nothing
+
+inferUnary :: UnaryOperator -> Type -> Subst Check Type
+inferUnary op val =
+ case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
+ (valTy, resTy) -> do
+ val ~~ valTy
+ return resTy
+
+checkUnary :: M.Map Ident Type -> UnaryOperator -> Value -> Type -> Subst Check ()
+checkUnary m op val res =
+ case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
+ (valTy, resTy) -> do
+ res ~~ resTy
+ check m val valTy
+
+unaryOps :: [(UnaryOperator, (Type, Type))]
+unaryOps = [ (Negate, (Number, Number))
+ , (Not, (Boolean, Boolean))
+ , (BitwiseNot, (Number, Number))
+ ]
+
+inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type
+inferBinary op left right | isEqualityTest op = do
+ left ~~ right
+ return Boolean
+inferBinary op left right =
+ case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
+ (valTy, resTy) -> do
+ left ~~ valTy
+ right ~~ valTy
+ return resTy
+
+checkBinary :: M.Map Ident Type -> BinaryOperator -> Value -> Value -> Type -> Subst Check ()
+checkBinary m op left right res | isEqualityTest op = do
+ res ~~ Boolean
+ t1 <- infer m left
+ t2 <- infer m right
+ t1 ~~ t2
+checkBinary m op left right res =
+ case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
+ (valTy, resTy) -> do
+ res ~~ resTy
+ check m left valTy
+ check m right valTy
+
+isEqualityTest :: BinaryOperator -> Bool
+isEqualityTest EqualTo = True
+isEqualityTest NotEqualTo = True
+isEqualityTest _ = False
+
+binaryOps :: [(BinaryOperator, (Type, Type))]
+binaryOps = [ (Add, (Number, Number))
+ , (Subtract, (Number, Number))
+ , (Multiply, (Number, Number))
+ , (Divide, (Number, Number))
+ , (Modulus, (Number, Number))
+ , (BitwiseAnd, (Number, Number))
+ , (BitwiseOr, (Number, Number))
+ , (BitwiseXor, (Number, Number))
+ , (ShiftRight, (Number, Number))
+ , (ZeroFillShiftRight, (Number, Number))
+ , (And, (Boolean, Boolean))
+ , (Or, (Boolean, Boolean))
+ , (Concat, (String, String))
+ , (Modulus, (Number, Number))
+ , (LessThan, (Number, Boolean))
+ , (LessThanOrEqualTo, (Number, Boolean))
+ , (GreaterThan, (Number, Boolean))
+ , (GreaterThanOrEqualTo, (Number, Boolean))
+ ]
+
+inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)
+inferBinder _ NullBinder = return M.empty
+inferBinder val (StringBinder _) = val ~~ String >> return M.empty
+inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty
+inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty
+inferBinder val (VarBinder name) = return $ M.singleton name val
+inferBinder val (NullaryBinder ctor) = do
+ env <- lift getEnv
+ modulePath <- checkModulePath `fmap` lift get
case M.lookup (qualify modulePath ctor) (dataConstructors env) of
- Just (PolyType args ret) -> do
- ret' <- replaceVarsWithUnknowns args ret
- return ([TypeConstraint val ret' (BinderOrigin b)], M.empty)
+ Just ty -> do
+ ty `subsumes` val
+ return M.empty
_ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
-typeConstraintsForBinder val b@(UnaryBinder ctor binder) = do
- env <- getEnv
- modulePath <- checkModulePath `fmap` get
+inferBinder val (UnaryBinder ctor binder) = do
+ env <- lift getEnv
+ modulePath <- checkModulePath `fmap` lift get
case M.lookup (qualify modulePath ctor) (dataConstructors env) of
- Just (PolyType idents f@(Function [_] _)) -> do
- obj <- fresh
- (Function [ty] ret) <- replaceVarsWithUnknowns idents f
- (cs, m1) <- typeConstraintsForBinder obj binder
- return (TypeConstraint val ret (BinderOrigin b) : TypeConstraint obj ty (BinderOrigin b) : cs, m1)
- Just _ -> throwError $ show ctor ++ " is not a unary constructor"
+ Just ty -> do
+ Function [obj] ret <- replaceAllVarsWithUnknowns ty
+ val `subsumes` ret
+ inferBinder obj binder
_ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
-typeConstraintsForBinder val b@(ObjectBinder props) = do
+inferBinder val (ObjectBinder props) = do
row <- fresh
rest <- fresh
- (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
- return (TypeConstraint val (Object (RUnknown row)) (BinderOrigin b) : cs, m1)
+ m1 <- inferRowProperties row rest props
+ val ~~ Object row
+ return m1
where
- typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
- typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row (BinderOrigin b)], M.empty)
- typeConstraintsForProperties nrow row ((name, binder):binders) = do
+ inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst Check (M.Map Ident Type)
+ inferRowProperties nrow row [] = nrow ~~ row >> return M.empty
+ inferRowProperties nrow row ((name, binder):binders) = do
propTy <- fresh
- (cs1, m1) <- typeConstraintsForBinder propTy binder
- (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
- return (cs1 ++ cs2, m1 `M.union` m2)
-typeConstraintsForBinder val b@(ArrayBinder binders rest) = do
+ m1 <- inferBinder propTy binder
+ m2 <- inferRowProperties nrow (RCons name propTy row) binders
+ return $ m1 `M.union` m2
+inferBinder val (ArrayBinder binders rest) = do
el <- fresh
- all <- mapM (typeConstraintsForBinder el) binders
- let (cs1, m1) = (concatMap fst &&& M.unions . map snd) all
- let arrayConstraint = TypeConstraint val (Array (TUnknown el)) (BinderOrigin b)
+ m1 <- M.unions <$> mapM (inferBinder el) binders
+ val ~~ Array el
case rest of
- Nothing -> return (arrayConstraint : cs1, m1)
+ Nothing -> return m1
Just binder -> do
- (cs2, m2) <- typeConstraintsForBinder val binder
- return (arrayConstraint : cs1 ++ cs2, m1 `M.union` m2)
-typeConstraintsForBinder val b@(NamedBinder name binder) = do
- me <- fresh
- (cs, m) <- typeConstraintsForBinder val binder
- return (TypeConstraint me (TUnknown val) (BinderOrigin b) : cs, M.insert name me m)
-
-typeConstraintsForGuardedBinder :: M.Map Ident Int -> Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
-typeConstraintsForGuardedBinder m val b@(GuardedBinder cond binder) = do
- (cs1, m1) <- typeConstraintsForBinder val binder
- (cs2, n) <- typeConstraints (m `M.union` m1) cond
- return (TypeConstraint n Boolean (ValueOrigin cond) : cs1 ++ cs2, m1)
-typeConstraintsForGuardedBinder m val b = typeConstraintsForBinder val b >>= return
-
-constantBinder :: Binder -> Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
-constantBinder b val ty = return ([TypeConstraint val ty (BinderOrigin b)], M.empty)
-
-typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
-typeConstraintsForBinders _ _ _ [] = return []
-typeConstraintsForBinders m nval ret ((binder, val):bs) = do
- (cs1, m1) <- typeConstraintsForGuardedBinder m nval binder
- (cs2, n2) <- typeConstraints (m `M.union` m1) val
- cs3 <- typeConstraintsForBinders m nval ret bs
- return (TypeConstraint n2 (TUnknown ret) (BinderOrigin binder) : cs1 ++ cs2 ++ cs3)
-
-assignVariable :: Ident -> M.Map Ident Int -> Check ()
+ m2 <- inferBinder val binder
+ return $ m1 `M.union` m2
+inferBinder val (NamedBinder name binder) = do
+ m <- inferBinder val binder
+ return $ M.insert name val m
+
+inferGuardedBinder :: M.Map Ident Type -> Type -> Binder -> Subst Check (M.Map Ident Type)
+inferGuardedBinder m val (GuardedBinder cond binder) = do
+ m1 <- inferBinder val binder
+ check (m1 `M.union` m) cond Boolean
+ return m1
+inferGuardedBinder m val b = inferBinder val b
+
+checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()
+checkBinders _ _ _ [] = return ()
+checkBinders m nval ret ((binder, val):bs) = do
+ m1 <- inferGuardedBinder m nval binder
+ check (m1 `M.union` m) val ret
+ checkBinders m nval ret bs
+
+assignVariable :: Ident -> M.Map Ident Type -> Subst Check ()
assignVariable name m =
case M.lookup name m of
Nothing -> return ()
Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
-typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
-typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
+checkStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> Statement -> Subst Check (Bool, M.Map Ident Type)
+checkStatement m mass ret (VariableIntroduction name val) = do
assignVariable name (m `M.union` mass)
- (cs1, n1) <- typeConstraints m val
- return (cs1, False, M.insert name n1 mass)
-typeConstraintsForStatement m mass ret (Assignment ident val) = do
- (cs1, n1) <- typeConstraints m val
+ t <- infer m val
+ return (False, M.insert name t mass)
+checkStatement m mass ret (Assignment ident val) = do
+ t <- infer m val
case M.lookup ident mass of
Nothing -> throwError $ "No local variable with name " ++ show ident
- Just ty ->
- return (TypeConstraint n1 (TUnknown ty) (AssignmentTargetOrigin ident) : cs1, False, mass)
-typeConstraintsForStatement m mass ret (While val inner) = do
- (cs1, n1) <- typeConstraints m val
- (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
- return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, allCodePathsReturn, mass)
-typeConstraintsForStatement m mass ret (If ifst) = do
- (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
- return (cs, allCodePathsReturn, mass)
-typeConstraintsForStatement m mass ret (For ident start end inner) = do
+ Just ty -> do t ~~ ty
+ return (False, mass)
+checkStatement m mass ret (While val inner) = do
+ check m val Boolean
+ (allCodePathsReturn, _) <- checkBlock m mass ret inner
+ return (allCodePathsReturn, mass)
+checkStatement m mass ret (If ifst) = do
+ allCodePathsReturn <- checkIfStatement m mass ret ifst
+ return (allCodePathsReturn, mass)
+checkStatement m mass ret (For ident start end inner) = do
assignVariable ident (m `M.union` mass)
- (cs1, n1) <- typeConstraints (m `M.union` mass) start
- (cs2, n2) <- typeConstraints (m `M.union` mass) end
- let mass1 = M.insert ident n1 mass
- (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
- return (TypeConstraint n1 Number (ValueOrigin start) : TypeConstraint n2 Number (ValueOrigin end) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
-typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
+ check (m `M.union` mass) start Number
+ check (m `M.union` mass) end Number
+ let mass1 = M.insert ident Number mass
+ (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
+ return (allCodePathsReturn, mass)
+checkStatement m mass ret (ForEach ident vals inner) = do
assignVariable ident (m `M.union` mass)
val <- fresh
- (cs1, n1) <- typeConstraints (m `M.union` mass) vals
+ check (m `M.union` mass) vals (Array val)
let mass1 = M.insert ident val mass
- (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
+ (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
- return (TypeConstraint n1 (Array (TUnknown val)) (ValueOrigin vals) : cs1 ++ cs2, False, mass)
-typeConstraintsForStatement m mass ret (Return val) = do
- (cs1, n1) <- typeConstraints (m `M.union` mass) val
- return (TypeConstraint n1 (TUnknown ret) (ValueOrigin val) : cs1, True, mass)
-
-typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
-typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
- (cs1, n1) <- typeConstraints m val
- (cs2, _, _) <- typeConstraintsForBlock m mass ret thens
- return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, False)
-typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
- (cs1, n1) <- typeConstraints m val
- (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
- (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
- return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
-
-typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
-typeConstraintsForElseStatement m mass ret (Else elses) = do
- (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
- return (cs, allCodePathsReturn)
-typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
- (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
- return (cs, allCodePathsReturn)
-
-typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
-typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
-typeConstraintsForBlock m mass ret (s:ss) = do
- (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
+ return (False, mass)
+checkStatement m mass ret (Return val) = do
+ check (m `M.union` mass) val ret
+ return (True, mass)
+
+checkIfStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> IfStatement -> Subst Check Bool
+checkIfStatement m mass ret (IfStatement val thens Nothing) = do
+ check m val Boolean
+ _ <- checkBlock m mass ret thens
+ return False
+checkIfStatement m mass ret (IfStatement val thens (Just elses)) = do
+ check m val Boolean
+ (allCodePathsReturn1, _) <- checkBlock m mass ret thens
+ allCodePathsReturn2 <- checkElseStatement m mass ret elses
+ return $ allCodePathsReturn1 && allCodePathsReturn2
+
+checkElseStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> ElseStatement -> Subst Check Bool
+checkElseStatement m mass ret (Else elses) = fst <$> checkBlock m mass ret elses
+checkElseStatement m mass ret (ElseIf ifst) = checkIfStatement m mass ret ifst
+
+checkBlock :: M.Map Ident Type -> M.Map Ident Type -> Type -> [Statement] -> Subst Check (Bool, M.Map Ident Type)
+checkBlock _ mass _ [] = return (False, mass)
+checkBlock m mass ret (s:ss) = do
+ (b1, mass1) <- checkStatement (m `M.union` mass) mass ret s
case (b1, ss) of
- (True, []) -> return (cs1, True, mass1)
+ (True, []) -> return (True, mass1)
(True, _) -> throwError "Unreachable code"
(False, ss) -> do
- (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
- return (cs1 ++ cs2, b2, mass2)
-
-solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
-solveTypeConstraints [] s = return s
-solveTypeConstraints all@(TypeConstraint n t o:cs) s = do
- (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
- typeOccursCheck n t
- let s' = let (f, g) = runTypeSolution s
- in TypeSolution (replaceType n t . f, replaceType n t . g)
- cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
- return (cs', s')
- solveTypeConstraints cs' s'
-solveTypeConstraints (RowConstraint n r o:cs) s = do
- (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
- rowOccursCheck n r
- let s' = let (f, g) = runTypeSolution s
- in TypeSolution (replaceRow n r . f, replaceRow n r . g)
- cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
- return (cs', s')
- solveTypeConstraints cs' s'
-
-substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
-substituteTypeInConstraint n s (TypeConstraint m t v)
- | n == m = unifyTypes v s t
- | otherwise = return [TypeConstraint m (replaceType n s t) v]
-substituteTypeInConstraint n s (RowConstraint m r v)
- = return [RowConstraint m (replaceType n s r) v]
-
-substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
-substituteRowInConstraint n r (TypeConstraint m t v)
- = return [TypeConstraint m (replaceRow n r t) v]
-substituteRowInConstraint n r (RowConstraint m r1 v)
- | m == n = unifyRows v r r1
- | otherwise = return [RowConstraint m (replaceRow n r r1) v]
-
-unifyTypes :: TypeConstraintOrigin -> Type -> Type -> Check [TypeConstraint]
-unifyTypes _ (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
-unifyTypes o (TUnknown u) t = do
- typeOccursCheck u t
- return [TypeConstraint u t o]
-unifyTypes o t (TUnknown u) = do
- typeOccursCheck u t
- return [TypeConstraint u t o]
-unifyTypes o (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2) | name1 == name2 =
- fmap concat $ zipWithM (unifyTypes o) args1 args2
-unifyTypes o (SaturatedTypeSynonym name args) ty = do
- env <- getEnv
- modulePath <- checkModulePath `fmap` get
- case M.lookup (qualify modulePath name) (typeSynonyms env) of
- Just (synArgs, body) -> do
- let m = M.fromList $ zip synArgs args
- let replaced = replaceTypeVars m body
- unifyTypes o replaced ty
- Nothing -> error "Type synonym was not defined"
-unifyTypes o ty s@(SaturatedTypeSynonym _ _) = unifyTypes o s ty
-unifyTypes _ Number Number = return []
-unifyTypes _ String String = return []
-unifyTypes _ Boolean Boolean = return []
-unifyTypes o (Array s) (Array t) = unifyTypes o s t
-unifyTypes o (Object row1) (Object row2) = unifyRows o row1 row2
-unifyTypes o (Function args1 ret1) (Function args2 ret2) = do
- guardWith "Function applied to incorrect number of args" $ length args1 == length args2
- cs1 <- fmap concat $ zipWithM (unifyTypes o) args1 args2
- cs2 <- unifyTypes o ret1 ret2
- return $ cs1 ++ cs2
-unifyTypes _ (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
-unifyTypes _ (TypeConstructor c1) (TypeConstructor c2) = do
- modulePath <- checkModulePath `fmap` get
- guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
- return []
-unifyTypes o (TypeApp t1 t2) (TypeApp t3 t4) = do
- cs1 <- unifyTypes o t1 t3
- cs2 <- unifyTypes o t2 t4
- return $ cs1 ++ cs2
-unifyTypes _ t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
-
-unifyRows :: TypeConstraintOrigin -> Row -> Row -> Check [TypeConstraint]
-unifyRows o r1 r2 =
- 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 do
- cs1 <- fmap concat $ mapM (uncurry $ unifyTypes o) int
- cs2 <- unifyRows' o sd1 r1' sd2 r2'
- return $ cs1 ++ cs2
+ (b2, mass2) <- checkBlock m mass1 ret ss
+ return (b2, mass2)
+
+skolemize :: String -> Type -> Subst Check Type
+skolemize ident ty = do
+ tsk <- Skolem <$> fresh'
+ rsk <- RSkolem <$> fresh'
+ return $ replaceRowVars ident rsk $ replaceTypeVars ident tsk ty
+
+check :: M.Map Ident Type -> Value -> Type -> Subst Check ()
+check m val ty = rethrow errorMessage $ check' m val ty
+ where
+ errorMessage msg =
+ "Error checking type of term " ++
+ prettyPrintValue val ++
+ " against type " ++
+ prettyPrintType ty ++
+ ":\n" ++
+ msg
+
+check' :: M.Map Ident Type -> Value -> Type -> Subst Check ()
+check' m val (ForAll idents ty) = do
+ sk <- skolemize idents ty
+ check m val sk
+check' m val u@(TUnknown _) = do
+ ty <- infer m val
+ -- Don't unify an unknown with an inferred polytype
+ ty' <- replaceAllVarsWithUnknowns ty
+ ty' ~~ u
+check' m (NumericLiteral _) Number = return ()
+check' m (StringLiteral _) String = return ()
+check' m (BooleanLiteral _) Boolean = return ()
+check' m (Unary op val) ty = checkUnary m op val ty
+check' m (Binary op left right) ty = checkBinary m op left right ty
+check' m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)
+check' m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)
+check' m (Abs args ret) (Function argTys retTy) = do
+ guardWith "Incorrect number of function arguments" (length args == length argTys)
+ let bindings = M.fromList (zip args argTys)
+ check (bindings `M.union` m) ret retTy
+check' m app@(App _ _) ret = do
+ let (f, argss) = unfoldApplication app
+ ft <- infer m f
+ checkFunctionApplications m ft argss ret
+check' m v@(Var var@(Qualified mp name)) ty = do
+ case mp of
+ ModulePath [] ->
+ case M.lookup name m of
+ Just ty1 -> do
+ repl <- lift $ replaceAllTypeSynonyms ty1
+ repl `subsumes` ty
+ Nothing -> lookupGlobal
+ _ -> lookupGlobal
where
- unifyRows' :: TypeConstraintOrigin -> [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
- unifyRows' o [] (RUnknown u) sd r = do
- rowOccursCheck u r
- return [RowConstraint u (rowFromList (sd, r)) o]
- unifyRows' o sd r [] (RUnknown u) = do
- rowOccursCheck u r
- return [RowConstraint u (rowFromList (sd, r)) o]
- unifyRows' o ns@((name, ty):row) r others (RUnknown u) | not (occursCheck u (ty, row)) = do
- u' <- fresh
- cs <- unifyRows' o row r others (RUnknown u')
- return (RowConstraint u (RCons name ty (RUnknown u')) o : cs)
- unifyRows' _ [] REmpty [] REmpty = return []
- unifyRows' _ [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return []
- unifyRows' _ sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
+ lookupGlobal = do
+ env <- lift getEnv
+ modulePath <- checkModulePath `fmap` lift get
+ case M.lookup (qualify modulePath var) (names env) of
+ Nothing -> throwError $ show var ++ " is undefined"
+ Just (ty1, _) -> do
+ repl <- lift $ replaceAllTypeSynonyms ty1
+ repl `subsumes` ty
+check' m (TypedValue val ty1) ty2 = do
+ kind <- lift $ kindOf ty1
+ guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+ ty1 `subsumes` ty2
+ check m val ty1
+check' m (Case val binders) ret = do
+ t1 <- infer m val
+ checkBinders m t1 ret binders
+check' m (IfThenElse cond th el) ty = do
+ check m cond Boolean
+ check m th ty
+ check m el ty
+check' m (ObjectLiteral ps) (Object row) = do
+ lift $ ensureNoDuplicateProperties ps
+ checkProperties m ps row False
+check' m (ObjectUpdate obj ps) (Object row) = do
+ lift $ ensureNoDuplicateProperties ps
+ us <- zip (map fst ps) <$> replicateM (length ps) fresh
+ let (propsToCheck, rest) = rowToList row
+ propsToRemove = map fst ps
+ remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck
+ check m obj (Object (rowFromList (us ++ remainingProps, rest)))
+ checkProperties m ps row True
+check' m (Accessor prop val) ty = do
+ rest <- fresh
+ check m val (Object (RCons prop ty rest))
+check' m (Block ss) ret = do
+ (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
+ guardWith "Block is missing a return statement" allCodePathsReturn
+check' m (Constructor c) ty = do
+ env <- lift getEnv
+ modulePath <- checkModulePath `fmap` lift get
+ case M.lookup (qualify modulePath c) (dataConstructors env) of
+ Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
+ Just ty1 -> do
+ repl <- lift $ replaceAllTypeSynonyms ty1
+ repl `subsumes` ty
+check' m val (SaturatedTypeSynonym name args) = do
+ ty <- expandTypeSynonym name args
+ check m val ty
+check' _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
+
+checkProperties :: M.Map Ident Type -> [(String, Value)] -> Row -> Bool -> Subst Check ()
+checkProperties m ps row lax = let (ts, r') = rowToList row in go ps ts r' where
+ go [] [] REmpty = return ()
+ go [] [] u@(RUnknown _) = u ~~ REmpty
+ go [] [] (RSkolem _) | lax = return ()
+ go [] ((p, _): _) _ | lax = return ()
+ | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p
+ go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row
+ go ((p,v):ps) [] u@(RUnknown _) = do
+ ty <- infer m v
+ rest <- fresh
+ u ~~ RCons p ty rest
+ go ps [] rest
+ go ((p,v):ps) ts r =
+ case lookup p ts of
+ Nothing -> do
+ ty <- infer m v
+ rest <- fresh
+ r ~~ RCons p ty rest
+ go ps ts rest
+ Just ty -> do
+ check m v ty
+ go ps (delete (p, ty) ts) r
+ go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)
+
+unfoldApplication :: Value -> (Value, [[Value]])
+unfoldApplication = go []
+ where
+ go argss (App f args) = go (args:argss) f
+ go argss f = (f, argss)
+
+checkFunctionApplications :: M.Map Ident Type -> Type -> [[Value]] -> Type -> Subst Check ()
+checkFunctionApplications _ _ [] _ = error "Nullary function application"
+checkFunctionApplications m fnTy [args] ret = checkFunctionApplication m fnTy args ret
+checkFunctionApplications m fnTy (args:argss) ret = do
+ argTys <- mapM (infer m) args
+ f <- inferFunctionApplication m fnTy argTys
+ checkFunctionApplications m f argss ret
+
+checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
+checkFunctionApplication m fnTy args ret = rethrow errorMessage $ checkFunctionApplication' m fnTy args ret
+ where
+ errorMessage msg = "Error applying function of type "
+ ++ prettyPrintType fnTy
+ ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
+ ++ ", expecting value of type "
+ ++ prettyPrintType ret ++ ":\n" ++ msg
+
+inferFunctionApplication :: M.Map Ident Type -> Type -> [Type] -> Subst Check Type
+inferFunctionApplication m (Function argTys retTy) args = do
+ guardWith "Incorrect number of function arguments" (length args == length argTys)
+ zipWithM subsumes args argTys
+ return retTy
+inferFunctionApplication m (ForAll ident ty) args = do
+ replaced <- replaceVarWithUnknown ident ty
+ inferFunctionApplication m replaced args
+inferFunctionApplication m u@(TUnknown _) args = do
+ ret <- fresh
+ args' <- mapM replaceAllVarsWithUnknowns args
+ u ~~ Function args' ret
+ return ret
+inferFunctionApplication m (SaturatedTypeSynonym name tyArgs) args = do
+ ty <- expandTypeSynonym name tyArgs
+ inferFunctionApplication m ty args
+inferFunctionApplication _ fnTy args = throwError $ "Cannot apply function of type "
+ ++ prettyPrintType fnTy
+ ++ " to argument(s) of type(s) " ++ intercalate ", " (map prettyPrintType args)
+
+checkFunctionApplication' :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
+checkFunctionApplication' m (Function argTys retTy) args ret = do
+ guardWith "Incorrect number of function arguments" (length args == length argTys)
+ zipWithM (check m) args argTys
+ retTy `subsumes` ret
+checkFunctionApplication' m (ForAll ident ty) args ret = do
+ replaced <- replaceVarWithUnknown ident ty
+ checkFunctionApplication m replaced args ret
+checkFunctionApplication' m u@(TUnknown _) args ret = do
+ tyArgs <- mapM (\arg -> infer m arg >>= replaceAllVarsWithUnknowns) args
+ u ~~ Function tyArgs ret
+checkFunctionApplication' m (SaturatedTypeSynonym name tyArgs) args ret = do
+ ty <- expandTypeSynonym name tyArgs
+ checkFunctionApplication' m ty args ret
+checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "
+ ++ prettyPrintType fnTy
+ ++ " to argument(s) " ++ intercalate ", " (map prettyPrintValue args)
+ ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."
+
+subsumes :: Type -> Type -> Subst Check ()
+subsumes (ForAll ident ty1) ty2 = do
+ replaced <- replaceVarWithUnknown ident ty1
+ replaced `subsumes` ty2
+subsumes (Function args1 ret1) (Function args2 ret2) = do
+ zipWithM subsumes args2 args1
+ ret1 `subsumes` ret2
+subsumes ty1 ty2 = ty1 ~~ ty2
+
diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs
index 79042a7..d3af5f1 100644
--- a/src/Language/PureScript/Types.hs
+++ b/src/Language/PureScript/Types.hs
@@ -18,27 +18,53 @@ module Language.PureScript.Types where
import Data.Data
import Language.PureScript.Names
+import Language.PureScript.Unknown (Unknown(..))
data Type
- = TUnknown Int
+ = TUnknown (Unknown Type)
| Number
| String
| Boolean
| Array Type
| Object Row
- | Function [Type] Type
+ | Function [PolyType] Type
| TypeVar String
| TypeConstructor (Qualified ProperName)
| TypeApp Type Type
- | SaturatedTypeSynonym (Qualified ProperName) [Type] deriving (Show, Eq, Data, Typeable)
+ | SaturatedTypeSynonym (Qualified ProperName) [Type]
+ | ForAll String Type
+ | Skolem Int deriving (Show, Eq, Data, Typeable)
-data PolyType = PolyType [String] Type deriving (Show, Eq, Data, Typeable)
+type PolyType = Type
data Row
- = RUnknown Int
+ = RUnknown (Unknown Row)
| RowVar String
| REmpty
- | RCons String Type Row deriving (Show, Eq, Data, Typeable)
+ | RCons String Type Row
+ | RSkolem Int deriving (Show, Eq, Data, Typeable)
-monoType :: Type -> PolyType
-monoType = PolyType []
+rowToList :: Row -> ([(String, Type)], Row)
+rowToList (RCons name ty row) = let (tys, rest) = rowToList row
+ in ((name, ty):tys, rest)
+rowToList r = ([], r)
+
+rowFromList :: ([(String, Type)], Row) -> Row
+rowFromList ([], r) = r
+rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
+
+isMonoType :: Type -> Bool
+isMonoType (ForAll _ _) = False
+isMonoType ty = isPolyType ty
+
+isPolyType :: Type -> Bool
+isPolyType (Array ty) = isMonoType ty
+isPolyType (Object ps) = all isPolyType (map snd . fst $ rowToList ps)
+isPolyType (Function args ret) = all isPolyType args && isPolyType ret
+isPolyType (TypeApp t1 t2) = isMonoType t1 && isMonoType t2
+isPolyType (SaturatedTypeSynonym _ args) = all isPolyType args
+isPolyType (ForAll idents ty) = isPolyType ty
+isPolyType _ = True
+
+mkForAll :: [String] -> Type -> Type
+mkForAll = flip . foldl . flip $ ForAll
diff --git a/src/Language/PureScript/Unknown.hs b/src/Language/PureScript/Unknown.hs
new file mode 100644
index 0000000..9f40ab9
--- /dev/null
+++ b/src/Language/PureScript/Unknown.hs
@@ -0,0 +1,25 @@
+-----------------------------------------------------------------------------
+--
+-- Module : Language.PureScript.Unknown
+-- Copyright : (c) Phil Freeman 2013
+-- License : MIT
+--
+-- Maintainer : Phil Freeman <paf31@cantab.net>
+-- Stability : experimental
+-- Portability :
+--
+-- |
+--
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DeriveDataTypeable #-}
+
+module Language.PureScript.Unknown where
+
+import Data.Data
+import Data.Typeable
+
+newtype Unknown t = Unknown { runUnknown :: Int } deriving (Show, Eq, Ord, Data, Typeable)
+
+
+