git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Instantiate constrained types as well as universally quantified types when unifying with a unification variable.
commite5ffbf9e7548da4c4e242a30c6eaeeb92b70961b authorPhil Freeman <paf31@cantab.net> dateFri 7 Feb 2014, 14:44 (13 years ago) parent554c9a0
3 files changed+24−11
compare with golang
unifiedsplit
libraries/prelude/prelude.purs+2 src/Language/PureScript/TypeChecker/Kinds.hs+4−2 src/Language/PureScript/TypeChecker/Types.hs+18−9
libraries/prelude/prelude.purs+2
@@ -75,6 +75,8 @@ module Prelude where
7575 empty :: forall a. f a
7676 (<|>) :: forall a. f a -> f a -> f a
7777
78+ infixl 1 >>=
79+
7880 class Monad m where
7981 return :: forall a. a -> m a
8082 (>>=) :: forall a b. m a -> (a -> m b) -> m b
src/Language/PureScript/TypeChecker/Kinds.hs+4−2
@@ -143,9 +143,11 @@ infer (TypeApp t1 t2) = do
143143 k1 =?= FunKind k2 k0
144144 return k0
145145infer (ForAll ident ty _) = do
146− k <- fresh
146+ k1 <- fresh
147147 Just moduleName <- checkCurrentModule <$> get
148− bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty
148+ k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
149+ k2 =?= Star
150+ return Star
149151infer REmpty = do
150152 k <- fresh
151153 return $ Row k
src/Language/PureScript/TypeChecker/Types.hs+18−9
@@ -354,9 +354,17 @@ replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
354354-- |
355355-- Replace named type variables with new unification variables
356356--
357−replaceAllVarsWithUnknowns :: Type -> UnifyT Type Check Type
358−replaceAllVarsWithUnknowns (ForAll ident ty _) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
359−replaceAllVarsWithUnknowns ty = return ty
357+instantiatePolyTypeWithUnknowns :: Value -> Type -> UnifyT Type Check (Value, Type)
358+instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
359+ ty' <- replaceVarWithUnknown ident ty
360+ instantiatePolyTypeWithUnknowns val ty'
361+instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do
362+ env <- getEnv
363+ Just moduleName <- checkCurrentModule <$> get
364+ dicts <- getTypeClassDictionaries
365+ (_, ty') <- instantiatePolyTypeWithUnknowns (error "Types under a constraint cannot themselves be constrained") ty
366+ return (foldl App val (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints)), ty')
367+instantiatePolyTypeWithUnknowns val ty = return (val, ty)
360368
361369-- |
362370-- Replace a single type variable with a new unification variable
@@ -460,10 +468,10 @@ infer' (Var var) = do
460468 Just moduleName <- checkCurrentModule <$> get
461469 ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
462470 case ty of
463− ConstrainedType constraints _ -> do
471+ ConstrainedType constraints ty' -> do
464472 env <- getEnv
465473 dicts <- getTypeClassDictionaries
466− return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty
474+ return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty'
467475 _ -> return $ TypedValue True (Var var) ty
468476infer' (Block ss) = do
469477 ret <- fresh
@@ -534,7 +542,7 @@ inferBinder val (UnaryBinder ctor binder) = do
534542 Just moduleName <- checkCurrentModule <$> get
535543 case M.lookup (qualify moduleName ctor) (dataConstructors env) of
536544 Just (ty, _) -> do
537− fn <- replaceAllVarsWithUnknowns ty
545+ (_, fn) <- instantiatePolyTypeWithUnknowns (error "Data constructor types cannot contains constraints") ty
538546 case fn of
539547 TypeApp (TypeApp t obj) ret | t == tyFunction -> do
540548 _ <- subsumes Nothing val ret
@@ -739,9 +747,9 @@ check' val t@(SaturatedTypeSynonym name args) = do
739747check' val u@(TUnknown _) = do
740748 val'@(TypedValue _ _ ty) <- infer val
741749 -- Don't unify an unknown with an inferred polytype
742− ty' <- replaceAllVarsWithUnknowns ty
750+ (val'', ty') <- instantiatePolyTypeWithUnknowns val' ty
743751 ty' =?= u
744− return $ TypedValue True val' ty'
752+ return $ TypedValue True val'' ty'
745753check' v@(NumericLiteral _) t | t == tyNumber =
746754 return $ TypedValue True v t
747755check' v@(StringLiteral _) t | t == tyString =
@@ -879,7 +887,8 @@ checkFunctionApplication' fn (ForAll ident ty _) arg = do
879887checkFunctionApplication' fn u@(TUnknown _) arg = do
880888 arg' <- do
881889 TypedValue _ v t <- infer arg
882− TypedValue True v <$> replaceAllVarsWithUnknowns t
890+ (v', t') <- instantiatePolyTypeWithUnknowns arg t
891+ return $ TypedValue True v' t'
883892 let ty = (\(TypedValue _ _ t) -> t) arg'
884893 ret <- fresh
885894 u =?= function ty ret