@@ -22,8 +22,7 @@ module Language.PureScript.TypeChecker.Types (
2222import Data.List
2323import Data.Maybe (isNothing, isJust, fromMaybe)
2424import qualified Data.Data as D
25−import Data.Generics
26− (mkT, something, everywhere, mkQ)
25+import Data.Generics (everything, mkT, something, everywhere, mkQ)
2726
2827import Language.PureScript.Values
2928import Language.PureScript.Types
@@ -129,7 +128,7 @@ unifyRows r1 r2 =
129128 unifyRows' sd r [] (TUnknown u) = replace u (rowFromList (sd, r))
130129 unifyRows' ((name, ty):row) r others u@(TUnknown un) = do
131130 occursCheck un ty
132− forM row $ \(_, t) -> occursCheck un t
131+ forM_ row $ \(_, t) -> occursCheck un t
133132 u' <- fresh
134133 u ~~ RCons name ty u'
135134 unifyRows' row r others u'
@@ -143,7 +142,7 @@ typeConstructorsAreEqual env moduleName = (==) `on` canonicalizeType moduleName
143142
144143typesOf :: ModuleName -> [(Ident, Value)] -> Check [Type]
145144typesOf moduleName vals = do
146− (tys, sub) <- runSubst (SubstContext moduleName) $ do
145+ (tys, _) <- runSubst (SubstContext moduleName) $ do
147146 let es = map isTyped vals
148147 typed = filter (isJust . snd . snd) es
149148 untyped = filter (isNothing . snd . snd) es
@@ -152,46 +151,50 @@ typesOf moduleName vals = do
152151 let untypedDict = zip (map fst untyped) untypedNames
153152 dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ typedDict ++ untypedDict)
154153 tys <- forM es $ \e -> do
155− ty <- case e of
154+ (val, ty) <- case e of
156155 (_, (val, Just ty)) -> do
157156 kind <- liftCheck $ kindOf moduleName ty
158157 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
159158 ty' <- replaceAllTypeSynonyms ty
160− bindNames dict $ check val ty'
161− return ty'
159+ val' <- bindNames dict $ check val ty'
160+ return (val', ty')
162161 (ident, (val, Nothing)) -> do
163− TypedValue _ ty <- bindNames dict $ infer val
162+ TypedValue val' ty <- bindNames dict $ infer val
164163 ty ~~ fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
165− return ty
164+ return (val', ty)
166165 when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do
167166 [eff, a] <- replicateM 2 fresh
168167 ty ~~ TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a
168+ escapeCheck val ty
169169 return ty
170170 return tys
171− --forM tys $ flip (escapeCheck checks) sub
172− forM tys $ skolemEscapeCheck
171+ forM_ tys $ skolemEscapeCheck
173172 return $ map (varIfUnknown . desaturateAllTypeSynonyms . setifyAll) tys
174173
175174isTyped :: (Ident, Value) -> (Ident, (Value, Maybe Type))
176175isTyped (name, TypedValue value ty) = (name, (value, Just ty))
177176isTyped (name, value) = (name, (value, Nothing))
178177
179−{-escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
180−escapeCheck checks ty sub =
181− let
182− visibleUnknowns = nub $ unknowns ty
183− in
184− forM_ checks $ \c -> case c of
185− AnyUnifiable t -> do
186− let unsolvedUnknowns = nub . unknowns $ apply sub t
187− guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
188−-}
178+escapeCheck :: Value -> Type -> Subst ()
179+escapeCheck value ty = do
180+ subst <- substSubst <$> getSubstState
181+ let visibleUnknowns = nub $ unknowns $ apply subst ty
182+ let allUnknowns = findAllTypes value
183+ forM_ allUnknowns $ \t -> do
184+ let unsolvedUnknowns = nub . unknowns $ apply subst t
185+ guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
186+
187+findAllTypes :: Value -> [Type]
188+findAllTypes = everything (++) (mkQ [] go)
189+ where
190+ go (TypedValue _ ty) = [ty]
191+ go _ = []
189192
190193skolemEscapeCheck :: Type -> Check ()
191194skolemEscapeCheck ty =
192195 case something (mkQ Nothing findSkolems) ty of
193196 Nothing -> return ()
194− Just _ -> throwError "Skolem variables cannot escape. Consider adding a type signature."
197+ Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature." ++ show ty
195198 where
196199 findSkolems (Skolem _) = return ()
197200 findSkolems _ = mzero
@@ -283,9 +286,9 @@ infer' (ObjectUpdate o ps) = do
283286 return $ TypedValue (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)
284287infer' (Indexer index val) = do
285288 el <- fresh
286− check index Number
287− check val (Array el)
288− return $ TypedValue (Indexer (TypedValue index Number) (TypedValue val (Array el))) el
289+ index' <- check index Number
290+ val' <- check val (Array el)
291+ return $ TypedValue (Indexer (TypedValue index' Number) (TypedValue val' (Array el))) el
289292infer' (Accessor prop val) = do
290293 typed@(TypedValue _ objTy) <- infer val
291294 propTy <- inferProperty objTy prop
@@ -330,11 +333,11 @@ infer' (Case vals binders) = do
330333 binders' <- checkBinders (map (\(TypedValue _ t) -> t) ts) ret binders
331334 return $ TypedValue (Case ts binders') ret
332335infer' (IfThenElse cond th el) = do
333− check cond Boolean
334− TypedValue v2 t2 <- infer th
335− TypedValue v3 t3 <- infer el
336+ cond' <- check cond Boolean
337+ v2@(TypedValue _ t2) <- infer th
338+ v3@(TypedValue _ t3) <- infer el
336339 t2 ~~ t3
337− return $ TypedValue (IfThenElse cond v2 v3) t2
340+ return $ TypedValue (IfThenElse cond' v2 v3) t2
338341infer' (TypedValue val ty) = do
339342 moduleName <- substCurrentModule <$> ask
340343 kind <- liftCheck $ kindOf moduleName ty
@@ -368,7 +371,8 @@ checkUnary op val res =
368371 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
369372 (valTy, resTy) -> do
370373 res ~~ resTy
371− check val valTy
374+ val' <- check val valTy
375+ return $ Unary op val'
372376
373377unaryOps :: [(UnaryOperator, (Type, Type))]
374378unaryOps = [ (Negate, (Number, Number))
@@ -391,17 +395,17 @@ inferBinary _ _ _ = error "Invalid arguments to inferBinary"
391395checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst Value
392396checkBinary op left right res | isEqualityTest op = do
393397 res ~~ Boolean
394− TypedValue v1 t1 <- infer left
395− TypedValue v2 t2 <- infer right
398+ left'@(TypedValue _ t1) <- infer left
399+ right'@(TypedValue _ t2) <- infer right
396400 t1 ~~ t2
397− return $ TypedValue (Binary op v1 v2) $ res
401+ return $ Binary op left' right'
398402checkBinary op left right res =
399403 case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
400404 (valTy, resTy) -> do
401405 res ~~ resTy
402− v1 <- check left valTy
403− v2 <- check right valTy
404− return $ TypedValue (Binary op v1 v2) $ res
406+ left' <- check left valTy
407+ right' <- check right valTy
408+ return $ Binary op left' right'
405409
406410isEqualityTest :: BinaryOperator -> Bool
407411isEqualityTest EqualTo = True
@@ -591,48 +595,53 @@ check' val u@(TUnknown _) = do
591595 ty' <- replaceAllVarsWithUnknowns ty
592596 ty' ~~ u
593597 return val'
594−check' v@(NumericLiteral _) Number = return $ TypedValue v Number
595−check' v@(StringLiteral _) String = return $ TypedValue v String
596−check' v@(BooleanLiteral _) Boolean = return $ TypedValue v Boolean
598+check' v@(NumericLiteral _) Number = return v
599+check' v@(StringLiteral _) String = return v
600+check' v@(BooleanLiteral _) Boolean = return v
597601check' (Unary op val) ty = checkUnary op val ty
598602check' (Binary op left right) ty = checkBinary op left right ty
599−check' (ArrayLiteral vals) (Array ty) = TypedValue <$> (ArrayLiteral <$> forM vals (\val -> check val ty)) <*> pure (Array ty)
600−check' (Indexer index vals) ty = check index Number >> check vals (Array ty)
603+check' (ArrayLiteral vals) (Array ty) = ArrayLiteral <$> forM vals (\val -> check val ty)
604+check' (Indexer index vals) ty = do
605+ index' <- check index Number
606+ vals' <- check vals (Array ty)
607+ return $ Indexer index' vals'
601608check' (Abs args ret) (Function argTys retTy) = do
602609 moduleName <- substCurrentModule <$> ask
603610 guardWith "Incorrect number of function arguments" (length args == length argTys)
604− bindLocalVariables moduleName (zip args argTys) $ check ret retTy
611+ ret' <- bindLocalVariables moduleName (zip args argTys) $ check ret retTy
612+ return $ Abs args ret'
605613check' (App f args) ret = do
606614 f'@(TypedValue _ ft) <- infer f
607615 args' <- checkFunctionApplication ft args ret
608− return $ TypedValue (App f' args') ret
616+ return $ App f' args'
609617check' (Var var) ty = do
610618 moduleName <- substCurrentModule <$> ask
611619 ty1 <- lookupVariable moduleName var
612620 repl <- replaceAllTypeSynonyms ty1
613621 repl `subsumes` ty
614− return $ TypedValue (Var var) ty
615−check' v@(TypedValue val ty1) ty2 = do
622+ return $ Var var
623+check' (TypedValue val ty1) ty2 = do
616624 moduleName <- substCurrentModule <$> ask
617625 kind <- liftCheck $ kindOf moduleName ty1
618626 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
619627 ty1 `subsumes` ty2
620− check val ty1
621− return v
628+ val' <- check val ty1
629+ return $ TypedValue val' ty1
622630check' (Case vals binders) ret = do
623631 vals' <- mapM infer vals
624632 let ts = map (\(TypedValue _ t) -> t) vals'
625633 binders' <- checkBinders ts ret binders
626− return $ TypedValue (Case vals' binders') ret
634+ return $ Case vals' binders'
627635check' (IfThenElse cond th el) ty = do
628− check cond Boolean
629− check th ty
630− check el ty
631−check' (ObjectLiteral ps) t@(Object row) = do
636+ cond' <- check cond Boolean
637+ th' <- check th ty
638+ el' <- check el ty
639+ return $ IfThenElse cond' th' el'
640+check' (ObjectLiteral ps) (Object row) = do
632641 ensureNoDuplicateProperties ps
633642 ps' <- checkProperties ps row False
634− return $ TypedValue (ObjectLiteral ps') t
635−check' (ObjectUpdate obj ps) t@(Object row) = do
643+ return $ ObjectLiteral ps'
644+check' (ObjectUpdate obj ps) (Object row) = do
636645 ensureNoDuplicateProperties ps
637646 us <- zip (map fst ps) <$> replicateM (length ps) fresh
638647 let (propsToCheck, rest) = rowToList row
@@ -640,14 +649,15 @@ check' (ObjectUpdate obj ps) t@(Object row) = do
640649 remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck
641650 obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))
642651 ps' <- checkProperties ps row True
643− return $ TypedValue (ObjectUpdate obj' ps') t
652+ return $ ObjectUpdate obj' ps'
644653check' (Accessor prop val) ty = do
645654 rest <- fresh
646− check val (Object (RCons prop ty rest))
655+ val' <- check val (Object (RCons prop ty rest))
656+ return $ Accessor prop val'
647657check' (Block ss) ret = do
648658 (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
649659 guardWith "Block is missing a return statement" allCodePathsReturn
650− return $ TypedValue (Block ss') ret
660+ return $ Block ss'
651661check' (Constructor c) ty = do
652662 env <- getEnv
653663 moduleName <- substCurrentModule <$> ask
@@ -656,7 +666,7 @@ check' (Constructor c) ty = do
656666 Just (ty1, _) -> do
657667 repl <- replaceAllTypeSynonyms ty1
658668 repl `subsumes` ty
659− return $ TypedValue (Constructor c) ty
669+ return $ Constructor c
660670check' val (SaturatedTypeSynonym name args) = do
661671 ty <- expandTypeSynonym name args
662672 check val ty
@@ -700,26 +710,6 @@ checkFunctionApplication fnTy args ret = rethrow errorMessage $ checkFunctionApp
700710 ++ ", expecting value of type "
701711 ++ prettyPrintType ret ++ ":\n" ++ msg
702712
703−inferFunctionApplication :: Type -> [Type] -> Subst Type
704−inferFunctionApplication (Function argTys retTy) args = do
705− guardWith "Incorrect number of function arguments" (length args == length argTys)
706− zipWithM subsumes args argTys
707− return retTy
708−inferFunctionApplication (ForAll ident ty) args = do
709− replaced <- replaceVarWithUnknown ident ty
710− inferFunctionApplication replaced args
711−inferFunctionApplication u@(TUnknown _) args = do
712− ret <- fresh
713− args' <- mapM replaceAllVarsWithUnknowns args
714− u ~~ Function args' ret
715− return ret
716−inferFunctionApplication (SaturatedTypeSynonym name tyArgs) args = do
717− ty <- expandTypeSynonym name tyArgs
718− inferFunctionApplication ty args
719−inferFunctionApplication fnTy args = throwError $ "Cannot apply function of type "
720− ++ prettyPrintType fnTy
721− ++ " to argument(s) of type(s) " ++ intercalate ", " (map prettyPrintType args)
722−
723713checkFunctionApplication' :: Type -> [Value] -> Type -> Subst [Value]
724714checkFunctionApplication' (Function argTys retTy) args ret = do
725715 guardWith "Incorrect number of function arguments" (length args == length argTys)
@@ -747,7 +737,7 @@ subsumes (ForAll ident ty1) ty2 = do
747737 replaced <- replaceVarWithUnknown ident ty1
748738 replaced `subsumes` ty2
749739subsumes (Function args1 ret1) (Function args2 ret2) = do
750− zipWithM subsumes args2 args1
740+ zipWithM_ subsumes args2 args1
751741 ret1 `subsumes` ret2
752742subsumes ty1 ty2 = ty1 ~~ ty2
753743