purescript 0.1.9 → 0.1.11

raw patch · 20 files changed

+1119/−844 lines, 20 files

Files

• purescript.cabal +2/−1
• src/Language/PureScript.hs +2/−2
• src/Language/PureScript/CodeGen/Externs.hs +2/−2
• src/Language/PureScript/CodeGen/JS.hs +22/−13
• src/Language/PureScript/Declarations.hs +5/−3
• src/Language/PureScript/Kinds.hs +2/−1
• src/Language/PureScript/Names.hs +4/−1
• src/Language/PureScript/Parser/Common.hs +14/−9
• src/Language/PureScript/Parser/Declarations.hs +16/−3
• src/Language/PureScript/Parser/Types.hs +23/−9
• src/Language/PureScript/Parser/Values.hs +8/−8
• src/Language/PureScript/Pretty/Kinds.hs +2/−1
• src/Language/PureScript/Pretty/Types.hs +7/−8
• src/Language/PureScript/Pretty/Values.hs +9/−1
• src/Language/PureScript/TypeChecker.hs +32/−10
• src/Language/PureScript/TypeChecker/Kinds.hs +74/−129
• src/Language/PureScript/TypeChecker/Monad.hs +86/−12
• src/Language/PureScript/TypeChecker/Types.hs +746/−623
• src/Language/PureScript/Types.hs +38/−8
• src/Language/PureScript/Unknown.hs +25/−0

@@ -1,5 +1,5 @@ name: purescript-version: 0.1.9+version: 0.1.11 cabal-version: >=1.8 build-type: Simple license: MIT@@ -36,6 +36,7 @@                      Language.PureScript.TypeChecker.Monad                      Language.PureScript.TypeChecker.Types                      Language.PureScript.TypeChecker.Synonyms+                     Language.PureScript.Unknown     exposed: True     buildable: True     hs-source-dirs: src

@@ -32,7 +32,7 @@ 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)

@@ -27,12 +27,12 @@ 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) =

@@ -20,11 +20,13 @@ 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.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 @@                         (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 (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

@@ -30,12 +30,14 @@ 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)

@@ -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)

@@ -30,7 +30,10 @@ 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])

@@ -120,22 +120,27 @@ 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 @@ 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)

@@ -28,6 +28,7 @@ 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 @@   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 =   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 @@   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 @@                    , 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

@@ -25,6 +25,7 @@ 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 @@  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 @@ 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 @@             , 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

@@ -47,10 +47,10 @@ 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 @@   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 @@  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 @@   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 = 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

@@ -25,13 +25,14 @@  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)

@@ -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.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 @@   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 @@   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 @@                     , 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

@@ -28,6 +28,7 @@ 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 @@   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 @@                   , [ 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 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

@@ -42,23 +42,23 @@ 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 (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 @@   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 @@     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 (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")

@@ -15,8 +15,6 @@ {-# LANGUAGE DeriveDataTypeable #-}  module Language.PureScript.TypeChecker.Kinds (-    KindConstraint(..),-    KindSolution(..),     kindsOf,     kindOf ) where@@ -32,6 +30,7 @@ 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 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+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 :: 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+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'')+inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst Check [Kind]+inferAll name m = mapM (infer name 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) =+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 ++ "."+    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 -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+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

@@ -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 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 @@ 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 @@ 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 @@   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  }

@@ -15,626 +15,749 @@ {-# LANGUAGE DeriveDataTypeable #-}  module Language.PureScript.TypeChecker.Types (-    TypeConstraint(..),-    TypeSolution(..),-    typeOf-) where--import Debug.Trace--import Data.List-import Data.Function-import qualified Data.Data as D-import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)--import Language.PureScript.Values-import Language.PureScript.Types-import Language.PureScript.Kinds-import Language.PureScript.Names-import Language.PureScript.TypeChecker.Monad-import Language.PureScript.TypeChecker.Kinds-import Language.PureScript.TypeChecker.Synonyms-import Language.PureScript.Pretty--import Control.Monad.State-import Control.Monad.Error--import Control.Applicative-import Control.Arrow (Kleisli(..), (***), (&&&), first)-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)--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 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-  return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty--allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()-allUnknownsBecameQuantified cs solution ty = do-  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--setify :: Row -> Row-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 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'-  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 t = t--replaceVarsWithUnknowns :: [String] -> Type -> Check Type-replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)-  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--replaceAllTypeSynonyms :: (D.Data d) => d -> Check d-replaceAllTypeSynonyms d = do-  env <- getEnv-  let syns = map (\((path, name), (args, _)) -> (Qualified path name, length args)) . M.toList $ typeSynonyms env-  either throwError return $ saturateAllTypeSynonyms syns d--desaturateAllTypeSynonyms :: (D.Data d) => d -> d-desaturateAllTypeSynonyms = everywhere (mkT replace)-  where-  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)--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))--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-  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-  case mp of-    ModulePath [] ->-      case M.lookup name m of-        Just u -> do-          me <- fresh-          return ([TypeConstraint u (TUnknown me) (ValueOrigin v)], me)-        Nothing -> lookupGlobal-    _ -> lookupGlobal-  where-  lookupGlobal = do-    env <- getEnv-    modulePath <- checkModulePath `fmap` 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-  ret <- fresh-  (cs, allCodePathsReturn, _) <- typeConstraintsForBlock 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-  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-  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-  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-  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)-    _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"-typeConstraintsForBinder val b@(UnaryBinder ctor binder) = do-  env <- getEnv-  modulePath <- checkModulePath `fmap` 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"-    _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"-typeConstraintsForBinder val b@(ObjectBinder props) = do-  row <- fresh-  rest <- fresh-  (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props-  return (TypeConstraint val (Object (RUnknown row)) (BinderOrigin b) : cs, 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-    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-  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)-  case rest of-    Nothing -> return (arrayConstraint : cs1, 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 ()-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-  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-  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-  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-  assignVariable ident (m `M.union` mass)-  val <- fresh-  (cs1, n1) <- typeConstraints (m `M.union` mass) vals-  let mass1 = M.insert ident val mass-  (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (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-  case (b1, ss) of-    (True, []) -> return (cs1, 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-  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)) ++ "."+    typeOf+) where++import Data.List+import Data.Maybe (isJust, fromMaybe)+import Data.Function+import qualified Data.Data as D+import Data.Generics+       (something, everywhere, everywhereM, everything, everywhereBut,+        mkT, mkM, mkQ, extM, extQ)++import Language.PureScript.Values+import Language.PureScript.Types+import Language.PureScript.Kinds+import Language.PureScript.Names+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 (Arrow(..), Kleisli(..), (***), (&&&), second)+import qualified Control.Category as C++import qualified Data.Map as M++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 <- replaceVarsWithUnknowns [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++typeOf :: Maybe Ident -> Value -> Check Type+typeOf name val = do+  (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++escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()+escapeCheck checks ty sub =+  let+    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++setifyAll :: (D.Data d) => d -> d+setifyAll = everywhere (mkT setify)++varIfUnknown :: Type -> Type+varIfUnknown ty = mkForAll (sort . map ((:) 'u' . show) . nub $ unknowns ty) 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+  replace (TypeVar v) | v == name = t+  replace t = t+  isShadowed (ForAll v _) | v == name = True+  isShadowed _ = False++replaceRowVars :: (D.Data d) => String -> Row -> d -> d+replaceRowVars name r = everywhere (mkT replace)+  where+  replace (RowVar v) | v == name = r+  replace t = t++replaceAllVarsWithUnknowns :: Type -> Subst Check Type+replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [ident] ty >>= replaceAllVarsWithUnknowns+replaceAllVarsWithUnknowns ty = return ty++replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type+replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)+  where+  f :: Type -> StateT (M.Map String Int) (Subst 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 (Unknown n)+      Just u -> return $ TUnknown (Unknown u)+  f t = return t+  g :: Row -> StateT (M.Map String Int) (Subst 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 (Unknown n)+      Just u -> return $ RUnknown (Unknown u)+  g r = return r++replaceAllTypeSynonyms :: (D.Data d) => d -> Check d+replaceAllTypeSynonyms d = do+  env <- getEnv+  let syns = map (\((path, name), (args, _)) -> (Qualified path name, length args)) . M.toList $ typeSynonyms env+  either throwError return $ saturateAllTypeSynonyms syns d++desaturateAllTypeSynonyms :: (D.Data d) => d -> d+desaturateAllTypeSynonyms = everywhere (mkT replace)+  where+  replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args+  replace t = t++expandAllTypeSynonyms :: Type -> Subst Check Type+expandAllTypeSynonyms (SaturatedTypeSynonym name args) = expandTypeSynonym name args >>= expandAllTypeSynonyms+expandAllTypeSynonyms ty = return ty++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++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 $ typesToRow fields+infer' m (ObjectUpdate o ps) = do+  lift $ ensureNoDuplicateProperties ps+  obj <- infer m o+  row <- fresh+  ts <- mapM (infer m . snd) ps+  let tys = zipWith (\(name, _) t -> (name, t)) ps ts+  obj ~~ Object (rowFromList (tys, row))+  return obj+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 ty -> lift $ replaceAllTypeSynonyms ty+        Nothing -> lookupGlobal+    _ -> lookupGlobal+  where+  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 (ty, _) -> lift $ replaceAllTypeSynonyms ty+infer' m (Block ss) = do+  ret <- fresh+  (allCodePathsReturn, _) <- checkBlock m M.empty ret ss+  guardWith "Block is missing a return statement" allCodePathsReturn+  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 ty -> lift $ replaceAllTypeSynonyms ty+infer' m (Case val binders) = do+  t1 <- infer m val+  ret <- fresh+  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+  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 <- replaceVarsWithUnknowns [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 ty -> do+      ty `subsumes` val+      return M.empty+    _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"+inferBinder val (UnaryBinder ctor binder) = do+  env <- lift getEnv+  modulePath <- checkModulePath `fmap` lift get+  case M.lookup (qualify modulePath ctor) (dataConstructors env) of+    Just ty -> do+      Function [obj] ret <- replaceAllVarsWithUnknowns ty+      val `subsumes` ret+      inferBinder obj binder+    _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"+inferBinder val (ObjectBinder props) = do+  row <- fresh+  rest <- fresh+  m1 <- inferRowProperties row rest props+  val ~~ Object row+  return m1+  where+  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+    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+  m1 <- M.unions <$> mapM (inferBinder el) binders+  val ~~ Array el+  case rest of+    Nothing -> return m1+    Just binder -> do+      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."++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)+  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 -> 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)+  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+  check (m `M.union` mass) vals (Array val)+  let mass1 = M.insert ident val mass+  (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner+  guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn+  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 (True, mass1)+    (True, _) -> throwError "Unreachable code"+    (False, ss) -> do+      (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+  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) objTy@(Object row) = do+  lift $ ensureNoDuplicateProperties ps+  check m obj objTy+  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+  f <- fresh+  checkFunctionApplication m fnTy args f+  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++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 <- replaceVarsWithUnknowns [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 $ "Cannot apply function of type "+  ++ prettyPrintType fnTy+  ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)+  ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."++subsumes :: Type -> Type -> Subst Check ()+subsumes (ForAll ident ty1) ty2 = do+  replaced <- replaceVarsWithUnknowns [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+

@@ -18,27 +18,57 @@  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 []+typesToRow :: [(String, Type)] -> Row+typesToRow [] = REmpty+typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)++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

@@ -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)+++