@@ -45,7 +45,8 @@ import Data.List
4545import Data.Maybe (maybeToList, isNothing, isJust, fromMaybe)
4646import qualified Data.Data as D
4747import Data.Generics
48− (mkM, everywhereM, everything, mkT, something, everywhere, mkQ)
48+ (everythingWithContext, mkM, everywhereM, everything, mkT,
49+ something, everywhere, mkQ)
4950
5051import Language.PureScript.Values
5152import Language.PureScript.Types
@@ -66,6 +67,7 @@ import Control.Arrow (Arrow(..))
6667
6768import qualified Data.Map as M
6869import Data.Function (on)
70+import Debug.Trace (trace)
6971
7072instance Partial Type where
7173 unknown = TUnknown
@@ -86,17 +88,23 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +
8688 unifyTypes' (TUnknown u) t = u =:= t
8789 unifyTypes' t (TUnknown u) = u =:= t
8890 unifyTypes' (SaturatedTypeSynonym name args) ty = do
89− ty1 <- expandTypeSynonym name args
91+ ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ args
9092 ty1 `unifyTypes` ty
9193 unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty
92− unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do
93− sk <- skolemize ident1 ty1
94− replaced <- replaceVarWithUnknown ident2 ty2
95− sk `unifyTypes` replaced
96− unifyTypes' (ForAll ident ty1) ty2 = do
97− sk <- skolemize ident ty1
94+ unifyTypes' (ForAll ident1 ty1 sc1) (ForAll ident2 ty2 sc2) =
95+ case (sc1, sc2) of
96+ (Just sc1', Just sc2') -> do
97+ sko <- newSkolemConstant
98+ let sk1 = skolemize ident1 sko sc1' ty1
99+ let sk2 = skolemize ident2 sko sc2' ty2
100+ sk1 `unifyTypes` sk2
101+ _ -> throwError (prettyPrintType ty1)
102+ unifyTypes' (ForAll ident ty1 (Just sc)) ty2 = do
103+ sko <- newSkolemConstant
104+ let sk = skolemize ident sko sc ty1
98105 sk `unifyTypes` ty2
99− unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty
106+ unifyTypes' (ForAll _ _ _) _ = throwError "Skolem variable scope is unspecified"
107+ unifyTypes' ty f@(ForAll _ _ _) = f `unifyTypes` ty
100108 unifyTypes' (Object row1) (Object row2) = row1 =?= row2
101109 unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
102110 unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
@@ -106,7 +114,7 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +
106114 unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do
107115 t3 `unifyTypes` t5
108116 t4 `unifyTypes` t6
109− unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()
117+ unifyTypes' (Skolem s1 _) (Skolem s2 _) | s1 == s2 = return ()
110118 unifyTypes' r1@(RCons _ _ _) r2 = unifyRows r1 r2
111119 unifyTypes' r1 r2@(RCons _ _ _) = unifyRows r1 r2
112120 unifyTypes' r1@REmpty r2 = unifyRows r1 r2
@@ -143,7 +151,7 @@ unifyRows r1 r2 =
143151 unifyRows' row r others u'
144152 unifyRows' [] REmpty [] REmpty = return ()
145153 unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()
146− unifyRows' [] (Skolem s1) [] (Skolem s2) | s1 == s2 = return ()
154+ unifyRows' [] (Skolem s1 _) [] (Skolem s2 _) | s1 == s2 = return ()
147155 unifyRows' sd3 r3 sd4 r4 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd3, r3)) ++ " with " ++ prettyPrintRow (rowFromList (sd4, r4)) ++ "."
148156
149157-- |
@@ -171,22 +179,24 @@ typesOf moduleName vals = do
171179 (ident, (val, Just (ty, checkType))) -> do
172180 kind <- liftCheck $ kindOf moduleName ty
173181 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
174− ty' <- replaceAllTypeSynonyms ty
175− val' <- bindNames dict $ if checkType then check val ty' else return val
182+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
183+ val' <- bindNames dict $ if checkType
184+ then TypedValue True <$> check val ty' <*> pure ty'
185+ else return (TypedValue False val ty')
176186 return (ident, (val', ty'))
177187 (ident, (val, Nothing)) -> do
178188 TypedValue _ val' ty <- bindNames dict $ infer val
179189 ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
180− return (ident, (val', ty))
190+ return (ident, (TypedValue True val' ty, ty))
181191 when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do
182192 [eff, a] <- replicateM 2 fresh
183193 ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a
184194 escapeCheck val ty
185195 return triple
186− forM_ tys $ skolemEscapeCheck . snd . snd
187196 forM tys $ \(ident, (val, ty)) -> do
188197 val' <- replaceTypeClassDictionaries moduleName val
189− return (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'
198+ rethrow (("Error in " ++ show ident ++ ": \n") ++) $ skolemEscapeCheck val'
199+ return $ (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'
190200 , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))
191201 where
192202 tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts
@@ -252,7 +262,7 @@ entails moduleName context goal@(className, ty) = do
252262-- and return a substitution from type variables to types which makes the type heads unify.
253263--
254264typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
255−typeHeadsAreEqual _ _ (Skolem s1) (Skolem s2) | s1 == s2 = Just []
265+typeHeadsAreEqual _ _ (Skolem s1 _) (Skolem s2 _) | s1 == s2 = Just []
256266typeHeadsAreEqual m e (TypeConstructor c1) (TypeConstructor c2) | typeConstructorsAreEqual e m c1 c2 = Just []
257267typeHeadsAreEqual m e (TypeApp h1 (TypeVar v)) (TypeApp h2 arg) = (:) (v, arg) <$> typeHeadsAreEqual m e h1 h2
258268typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1
@@ -268,7 +278,7 @@ escapeCheck value ty = do
268278 let allUnknowns = findAllTypes value
269279 forM_ allUnknowns $ \t -> do
270280 let unsolvedUnknowns = nub . unknowns $ subst $? t
271− guardWith ("Escape check fails" ++ show (subst $? ty, subst $? t)) $ null $ unsolvedUnknowns \\ visibleUnknowns
281+ guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
272282
273283-- |
274284-- Find all type annotations occuring inside a value
@@ -282,14 +292,31 @@ findAllTypes = everything (++) (mkQ [] go)
282292-- |
283293-- Ensure skolem variables do not escape their scope
284294--
285−skolemEscapeCheck :: Type -> Check ()
286−skolemEscapeCheck ty =
287− case something (mkQ Nothing findSkolems) ty of
288− Nothing -> return ()
289− Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature."
295+skolemEscapeCheck :: Value -> Check ()
296+skolemEscapeCheck (TypedValue False _ _) = return ()
297+skolemEscapeCheck root@(TypedValue _ _ _) =
298+ case everythingWithContext [] (++) (mkQ ((,) []) go) root of
299+ [] -> return ()
300+ ((binding, val) : _) -> throwError $ "Rigid/skolem type variable bound by " ++ prettyPrintValue binding ++ " has escaped at " ++ prettyPrintValue val
290301 where
291− findSkolems (Skolem _) = return ()
292− findSkolems _ = mzero
302+ go :: Value -> [(SkolemScope, Value)] -> ([(Value, Value)], [(SkolemScope, Value)])
303+ go val@(TypedValue _ _ (ForAll _ _ (Just sco))) scos = ([], (sco, val) : scos)
304+ go val@(TypedValue _ _ ty) scos = case collectSkolems ty \\ map fst scos of
305+ (sco : _) -> ([(findBindingScope sco, val)], scos)
306+ _ -> ([], scos)
307+ where
308+ collectSkolems :: Type -> [SkolemScope]
309+ collectSkolems = nub . everything (++) (mkQ [] collect)
310+ where
311+ collect (Skolem _ scope) = [scope]
312+ collect _ = []
313+ go _ scos = ([], scos)
314+ findBindingScope :: SkolemScope -> Value
315+ findBindingScope sco = fromMaybe (error "No introducing ForAll for skolem variable.") $ something (mkQ Nothing go) root
316+ where
317+ go val@(TypedValue _ _ (ForAll _ _ (Just sco'))) | sco == sco' = Just val
318+ go _ = Nothing
319+skolemEscapeCheck val = throwError $ "Untyped value passed to skolemEscapeCheck: " ++ prettyPrintValue val
293320
294321-- |
295322-- Ensure a row contains no duplicate labels
@@ -326,7 +353,7 @@ replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
326353-- Replace named type variables with new unification variables
327354--
328355replaceAllVarsWithUnknowns :: Type -> UnifyT Type Check Type
329−replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
356+replaceAllVarsWithUnknowns (ForAll ident ty _) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
330357replaceAllVarsWithUnknowns ty = return ty
331358
332359-- |
@@ -404,7 +431,8 @@ infer' (ObjectUpdate o ps) = do
404431 newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps
405432 let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals
406433 oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh
407− o' <- check o $ Object $ rowFromList (oldTys, row)
434+ let oldTy = Object $ rowFromList (oldTys, row)
435+ o' <- TypedValue True <$> check o oldTy <*> pure oldTy
408436 return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)
409437infer' (Accessor prop val) = do
410438 typed@(TypedValue _ _ objTy) <- infer val
@@ -424,19 +452,17 @@ infer' (Abs arg ret) = do
424452 return $ TypedValue True (Abs arg body) $ function ty bodyTy
425453infer' (App f arg) = do
426454 f'@(TypedValue _ _ ft) <- infer f
427− ret <- fresh
428− app <- checkFunctionApplication f' ft arg ret
455+ (ret, app) <- checkFunctionApplication f' ft arg
429456 return $ TypedValue True app ret
430457infer' (Var var) = do
431458 Just moduleName <- checkCurrentModule <$> get
432− ty <- lookupVariable moduleName var
433− ty' <- replaceAllTypeSynonyms ty
434− case ty' of
459+ ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
460+ case ty of
435461 ConstrainedType constraints _ -> do
436462 env <- getEnv
437463 dicts <- getTypeClassDictionaries
438− return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty'
439− _ -> return $ TypedValue True (Var var) ty'
464+ return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty
465+ _ -> return $ TypedValue True (Var var) ty
440466infer' (Block ss) = do
441467 ret <- fresh
442468 (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
@@ -447,7 +473,7 @@ infer' v@(Constructor c) = do
447473 Just moduleName <- checkCurrentModule <$> get
448474 case M.lookup (qualify moduleName c) (dataConstructors env) of
449475 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
450− Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty
476+ Just (ty, _) -> do ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
451477 return $ TypedValue True v ty'
452478infer' (Case vals binders) = do
453479 ts <- mapM infer vals
@@ -464,9 +490,9 @@ infer' (TypedValue checkType val ty) = do
464490 Just moduleName <- checkCurrentModule <$> get
465491 kind <- liftCheck $ kindOf moduleName ty
466492 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
467− ty' <- replaceAllTypeSynonyms ty
493+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
468494 val' <- if checkType then check val ty' else return val
469− return $ TypedValue True val' ty
495+ return $ TypedValue True val' ty'
470496infer' _ = error "Invalid argument to infer"
471497
472498-- |
@@ -477,9 +503,9 @@ inferProperty (Object row) prop = do
477503 let (props, _) = rowToList row
478504 return $ lookup prop props
479505inferProperty (SaturatedTypeSynonym name args) prop = do
480− replaced <- expandTypeSynonym name args
506+ replaced <- introduceSkolemScope <=< expandTypeSynonym name $ args
481507 inferProperty replaced prop
482−inferProperty (ForAll ident ty) prop = do
508+inferProperty (ForAll ident ty _) prop = do
483509 replaced <- replaceVarWithUnknown ident ty
484510 inferProperty replaced prop
485511inferProperty _ _ = return Nothing
@@ -551,7 +577,7 @@ checkBinders nvals ret ((binders, grd, val):bs) = do
551577 Just moduleName <- checkCurrentModule <$> get
552578 m1 <- M.unions <$> zipWithM inferBinder nvals binders
553579 r <- bindLocalVariables moduleName (M.toList m1) $ do
554− val' <- check val ret
580+ val' <- TypedValue True <$> check val ret <*> pure ret
555581 case grd of
556582 Nothing -> return (binders, Nothing, val')
557583 Just g -> do
@@ -602,7 +628,7 @@ checkStatement mass ret (For ident start end inner) = do
602628 return (allCodePathsReturn, mass, For ident start' end' inner')
603629checkStatement mass ret (Return val) = do
604630 val' <- check val ret
605− return (True, mass, Return val')
631+ return (True, mass, Return (TypedValue True val' ret))
606632
607633-- |
608634-- Check the type of an if-then-else statement
@@ -642,13 +668,32 @@ checkBlock mass ret (s:ss) = do
642668 (b, m, ss'') <- checkBlock mass1 ret ss'
643669 return (b, m, s':ss'')
644670
671+-- |
672+-- Generate a new skolem constant
673+--
674+newSkolemConstant :: UnifyT Type Check Int
675+newSkolemConstant = runUnknown <$> fresh'
676+
677+-- |
678+-- Generate a new skolem scope
679+--
680+newSkolemScope :: UnifyT Type Check SkolemScope
681+newSkolemScope = SkolemScope . runUnknown <$> fresh'
682+
645683-- |
646684-- Skolemize a type variable by replacing its instances with fresh skolem constants
647685--
648−skolemize :: String -> Type -> UnifyT Type Check Type
649−skolemize ident ty = do
650− tsk <- Skolem . runUnknown <$> fresh'
651− return $ replaceTypeVars ident tsk ty
686+skolemize :: (D.Data d) => String -> Int -> SkolemScope -> d -> d
687+skolemize ident sko scope d = replaceTypeVars ident (Skolem sko scope) d
688+
689+-- |
690+-- Introduce skolem scope at every occurence of a ForAll
691+--
692+introduceSkolemScope :: Type -> UnifyT Type Check Type
693+introduceSkolemScope = everywhereM (mkM go)
694+ where
695+ go (ForAll ident ty Nothing) = ForAll ident ty <$> (Just <$> newSkolemScope)
696+ go other = return other
652697
653698-- |
654699-- Check the type of a value, rethrowing errors to provide a better error message
@@ -668,10 +713,13 @@ check val ty = rethrow errorMessage $ check' val ty
668713-- Check the type of a value
669714--
670715check' :: Value -> Type -> UnifyT Type Check Value
671−check' val (ForAll idents ty) = do
672− sk <- skolemize idents ty
673− check val sk
674−check' val (ConstrainedType constraints ty) = do
716+check' val t@(ForAll ident ty _) = do
717+ scope <- newSkolemScope
718+ sko <- newSkolemConstant
719+ let sk = skolemize ident sko scope ty
720+ val' <- check val sk
721+ return $ TypedValue True val' (ForAll ident ty (Just scope))
722+check' val t@(ConstrainedType constraints ty) = do
675723 env <- getEnv
676724 Just moduleName <- checkCurrentModule <$> get
677725 dictNames <- flip mapM constraints $ \(Qualified _ (ProperName className), _) -> do
@@ -681,34 +729,39 @@ check' val (ConstrainedType constraints ty) = do
681729 TypeClassDictionaryInScope name className instanceTy Nothing TCDRegular) (map (Qualified Nothing) dictNames)
682730 (qualifyAllUnqualifiedNames moduleName env constraints)) $
683731 check val ty
684− return $ foldr Abs val' dictNames
732+ return $ TypedValue True (foldr Abs val' dictNames) t
685733check' val u@(TUnknown _) = do
686734 val'@(TypedValue _ _ ty) <- infer val
687735 -- Don't unify an unknown with an inferred polytype
688736 ty' <- replaceAllVarsWithUnknowns ty
689737 ty' =?= u
690− return val'
691−check' v@(NumericLiteral _) t | t == tyNumber = return v
692−check' v@(StringLiteral _) t | t == tyString = return v
693−check' v@(BooleanLiteral _) t | t == tyBoolean = return v
694−check' (ArrayLiteral vals) (TypeApp a ty) | a == tyArray = ArrayLiteral <$> forM vals (\val -> check val ty)
695−check' (Abs arg ret) (TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do
738+ return $ TypedValue True val' ty'
739+check' v@(NumericLiteral _) t | t == tyNumber =
740+ return $ TypedValue True v t
741+check' v@(StringLiteral _) t | t == tyString =
742+ return $ TypedValue True v t
743+check' v@(BooleanLiteral _) t | t == tyBoolean =
744+ return $ TypedValue True v t
745+check' (ArrayLiteral vals) t@(TypeApp a ty) | a == tyArray = do
746+ arr <- ArrayLiteral <$> forM vals (\val -> check val ty)
747+ return $ TypedValue True arr t
748+check' (Abs arg ret) ty@(TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do
696749 Just moduleName <- checkCurrentModule <$> get
697750 ret' <- bindLocalVariables moduleName [(arg, argTy)] $ check ret retTy
698− return $ Abs arg ret'
751+ return $ TypedValue True (Abs arg ret') ty
699752check' (App f arg) ret = do
700753 f'@(TypedValue _ _ ft) <- infer f
701− app <- checkFunctionApplication f' ft arg ret
702− return $ app
754+ (ret', app) <- checkFunctionApplication f' ft arg
755+ subsumes Nothing ret' ret
756+ return $ TypedValue True app ret
703757check' v@(Var var) ty = do
704758 Just moduleName <- checkCurrentModule <$> get
705− ty1 <- lookupVariable moduleName var
706− repl <- replaceAllTypeSynonyms ty1
707− ty' <- replaceAllTypeSynonyms ty
759+ repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
760+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
708761 v' <- subsumes (Just v) repl ty'
709762 case v' of
710763 Nothing -> throwError "Unable to check type subsumption"
711− Just v'' -> return v''
764+ Just v'' -> return $ TypedValue True v'' ty'
712765check' (TypedValue checkType val ty1) ty2 = do
713766 Just moduleName <- checkCurrentModule <$> get
714767 kind <- liftCheck $ kindOf moduleName ty1
@@ -718,22 +771,22 @@ check' (TypedValue checkType val ty1) ty2 = do
718771 Nothing -> throwError "Unable to check type subsumption"
719772 Just val'' -> do
720773 val''' <- if checkType then check val'' ty1 else return val''
721− return $ TypedValue True val''' ty1
774+ return $ TypedValue checkType (TypedValue True val''' ty1) ty2
722775check' (Case vals binders) ret = do
723776 vals' <- mapM infer vals
724777 let ts = map (\(TypedValue _ _ t) -> t) vals'
725778 binders' <- checkBinders ts ret binders
726− return $ Case vals' binders'
779+ return $ TypedValue True (Case vals' binders') ret
727780check' (IfThenElse cond th el) ty = do
728781 cond' <- check cond tyBoolean
729782 th' <- check th ty
730783 el' <- check el ty
731− return $ IfThenElse cond' th' el'
732−check' (ObjectLiteral ps) (Object row) = do
784+ return $ TypedValue True (IfThenElse cond' th' el') ty
785+check' (ObjectLiteral ps) t@(Object row) = do
733786 ensureNoDuplicateProperties ps
734787 ps' <- checkProperties ps row False
735− return $ ObjectLiteral ps'
736−check' (ObjectUpdate obj ps) (Object row) = do
788+ return $ TypedValue True (ObjectLiteral ps') t
789+check' (ObjectUpdate obj ps) t@(Object row) = do
737790 ensureNoDuplicateProperties ps
738791 us <- zip (map fst ps) <$> replicateM (length ps) fresh
739792 let (propsToCheck, rest) = rowToList row
@@ -741,27 +794,28 @@ check' (ObjectUpdate obj ps) (Object row) = do
741794 remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck
742795 obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))
743796 ps' <- checkProperties ps row True
744− return $ ObjectUpdate obj' ps'
797+ return $ TypedValue True (ObjectUpdate obj' ps') t
745798check' (Accessor prop val) ty = do
746799 rest <- fresh
747800 val' <- check val (Object (RCons prop ty rest))
748− return $ Accessor prop val'
801+ return $ TypedValue True (Accessor prop val') ty
749802check' (Block ss) ret = do
750803 (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
751804 guardWith "Block is missing a return statement" allCodePathsReturn
752− return $ Block ss'
805+ return $ TypedValue True (Block ss') ret
753806check' (Constructor c) ty = do
754807 env <- getEnv
755808 Just moduleName <- checkCurrentModule <$> get
756809 case M.lookup (qualify moduleName c) (dataConstructors env) of
757810 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
758811 Just (ty1, _) -> do
759− repl <- replaceAllTypeSynonyms ty1
812+ repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
760813 _ <- subsumes Nothing repl ty
761− return $ Constructor c
762−check' val (SaturatedTypeSynonym name args) = do
763− ty <- expandTypeSynonym name args
764− check val ty
814+ return $ TypedValue True (Constructor c) ty
815+check' val t@(SaturatedTypeSynonym name args) = do
816+ ty <- introduceSkolemScope <=< expandTypeSynonym name $ args
817+ val' <- check val ty
818+ return $ TypedValue True val' ty
765819check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
766820
767821-- |
@@ -774,7 +828,7 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
774828 go [] [] REmpty = return []
775829 go [] [] u@(TUnknown _) = do u =?= REmpty
776830 return []
777− go [] [] (Skolem _) | lax = return []
831+ go [] [] (Skolem _ _) | lax = return []
778832 go [] ((p, _): _) _ | lax = return []
779833 | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p
780834 go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row
@@ -801,8 +855,8 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
801855-- |
802856-- Check the type of a function application, rethrowing errors to provide a better error message
803857--
804−checkFunctionApplication :: Value -> Type -> Value -> Type -> UnifyT Type Check Value
805−checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg ret
858+checkFunctionApplication :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)
859+checkFunctionApplication fn fnTy arg = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg
806860 where
807861 errorMessage msg = "Error applying function of type "
808862 ++ prettyPrintType fnTy
@@ -812,34 +866,33 @@ checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionA
812866-- |
813867-- Check the type of a function application
814868--
815−checkFunctionApplication' :: Value -> Type -> Value -> Type -> UnifyT Type Check Value
816−checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
869+checkFunctionApplication' :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)
870+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do
817871 tyFunction' =?= tyFunction
818872 arg' <- check arg argTy
819− _ <- subsumes Nothing retTy ret
820− return $ App fn arg'
821−checkFunctionApplication' fn (ForAll ident ty) arg ret = do
873+ return (retTy, App fn arg')
874+checkFunctionApplication' fn (ForAll ident ty _) arg = do
822875 replaced <- replaceVarWithUnknown ident ty
823− checkFunctionApplication fn replaced arg ret
824−checkFunctionApplication' fn u@(TUnknown _) arg ret = do
876+ checkFunctionApplication fn replaced arg
877+checkFunctionApplication' fn u@(TUnknown _) arg = do
825878 arg' <- do
826879 TypedValue _ v t <- infer arg
827880 TypedValue True v <$> replaceAllVarsWithUnknowns t
828881 let ty = (\(TypedValue _ _ t) -> t) arg'
882+ ret <- fresh
829883 u =?= function ty ret
830− return $ App fn arg'
831−checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
832− ty <- expandTypeSynonym name tyArgs
833− checkFunctionApplication fn ty arg ret
834−checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
884+ return (ret, App fn arg')
885+checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg = do
886+ ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
887+ checkFunctionApplication fn ty arg
888+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg = do
835889 env <- getEnv
836890 dicts <- getTypeClassDictionaries
837891 Just moduleName <- checkCurrentModule <$> get
838− checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg ret
839−checkFunctionApplication' _ fnTy arg ret = throwError $ "Applying a function of type "
892+ checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg
893+checkFunctionApplication' _ fnTy arg = throwError $ "Cannot apply a function of type "
840894 ++ prettyPrintType fnTy
841− ++ " to argument(s) " ++ prettyPrintValue arg
842− ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."
895+ ++ " to argument " ++ prettyPrintValue arg
843896
844897-- |
845898-- Check whether one type subsumes another, rethrowing errors to provide a better error message
@@ -857,18 +910,25 @@ subsumes val ty1 ty2 = rethrow errorMessage $ subsumes' val ty1 ty2
857910-- Check whether one type subsumes another
858911--
859912subsumes' :: Maybe Value -> Type -> Type -> UnifyT Type Check (Maybe Value)
860−subsumes' val (ForAll ident ty1) ty2 = do
913+subsumes' val (ForAll ident ty1 _) ty2 = do
861914 replaced <- replaceVarWithUnknown ident ty1
862915 subsumes val replaced ty2
916+subsumes' val ty1 (ForAll ident ty2 sco) =
917+ case sco of
918+ Just sco' -> do
919+ sko <- newSkolemConstant
920+ let sk = skolemize ident sko sco' ty2
921+ subsumes val ty1 sk
922+ Nothing -> throwError "Skolem variable scope is unspecified"
863923subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
864924 subsumes Nothing arg2 arg1
865925 subsumes Nothing ret1 ret2
866926 return val
867927subsumes' val (SaturatedTypeSynonym name tyArgs) ty2 = do
868− ty1 <- expandTypeSynonym name tyArgs
928+ ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
869929 subsumes val ty1 ty2
870930subsumes' val ty1 (SaturatedTypeSynonym name tyArgs) = do
871− ty2 <- expandTypeSynonym name tyArgs
931+ ty2 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
872932 subsumes val ty1 ty2
873933subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do
874934 env <- getEnv