e5ffbf9 · rowtype-yoga/purescript-native

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.

e5ffbf9Phil Freeman13 years ago

libraries/prelude/prelude.purs+2

compare with golang

unifiedsplit

@@ -75,6 +75,8 @@ module Prelude where

75 empty :: forall a. f a

76 (<|>) :: forall a. f a -> f a -> f a

78+ infixl 1 >>=

79+

78 class Monad m where

80 class Monad m where

79 return :: forall a. a -> m a

81 return :: forall a. a -> m a

80 (>>=) :: forall a b. m a -> (a -> m b) -> m b

82 (>>=) :: 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

143 k1 =?= FunKind k2 k0

144 return k0

145infer (ForAll ident ty _) = do

146− k <- fresh

146+ k1 <- fresh

147 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

149infer REmpty = do

151infer REmpty = do

150 k <- fresh

152 k <- fresh

151 return $ Row k

153 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

354-- |

355-- Replace named type variables with new unification variables

356--

357−replaceAllVarsWithUnknowns :: Type -> UnifyT Type Check Type

357+instantiatePolyTypeWithUnknowns :: Value -> Type -> UnifyT Type Check (Value, Type)

358+instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do

358−replaceAllVarsWithUnknowns (ForAll ident ty _) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns

359+ ty' <- replaceVarWithUnknown ident ty

359−replaceAllVarsWithUnknowns ty = return 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)

360

368

361-- |

369-- |

362-- Replace a single type variable with a new unification variable

370-- Replace a single type variable with a new unification variable

@@ -460,10 +468,10 @@ infer' (Var var) = do

460 Just moduleName <- checkCurrentModule <$> get

468 Just moduleName <- checkCurrentModule <$> get

461 ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var

469 ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var

462 case ty of

470 case ty of

463− ConstrainedType constraints _ -> do

471+ ConstrainedType constraints ty' -> do

464 env <- getEnv

472 env <- getEnv

465 dicts <- getTypeClassDictionaries

473 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'

467 _ -> return $ TypedValue True (Var var) ty

475 _ -> return $ TypedValue True (Var var) ty

468infer' (Block ss) = do

476infer' (Block ss) = do

469 ret <- fresh

477 ret <- fresh

@@ -534,7 +542,7 @@ inferBinder val (UnaryBinder ctor binder) = do

534 Just moduleName <- checkCurrentModule <$> get

542 Just moduleName <- checkCurrentModule <$> get

535 case M.lookup (qualify moduleName ctor) (dataConstructors env) of

543 case M.lookup (qualify moduleName ctor) (dataConstructors env) of

536 Just (ty, _) -> do

544 Just (ty, _) -> do

537− fn <- replaceAllVarsWithUnknowns ty

545+ (_, fn) <- instantiatePolyTypeWithUnknowns (error "Data constructor types cannot contains constraints") ty

538 case fn of

546 case fn of

539 TypeApp (TypeApp t obj) ret | t == tyFunction -> do

547 TypeApp (TypeApp t obj) ret | t == tyFunction -> do

540 _ <- subsumes Nothing val ret

548 _ <- subsumes Nothing val ret

@@ -739,9 +747,9 @@ check' val t@(SaturatedTypeSynonym name args) = do

739check' val u@(TUnknown _) = do

747check' val u@(TUnknown _) = do

740 val'@(TypedValue _ _ ty) <- infer val

748 val'@(TypedValue _ _ ty) <- infer val

741 -- Don't unify an unknown with an inferred polytype

749 -- Don't unify an unknown with an inferred polytype

742− ty' <- replaceAllVarsWithUnknowns ty

750+ (val'', ty') <- instantiatePolyTypeWithUnknowns val' ty

743 ty' =?= u

751 ty' =?= u

744− return $ TypedValue True val' ty'

752+ return $ TypedValue True val'' ty'

745check' v@(NumericLiteral _) t | t == tyNumber =

753check' v@(NumericLiteral _) t | t == tyNumber =

746 return $ TypedValue True v t

754 return $ TypedValue True v t

747check' v@(StringLiteral _) t | t == tyString =

755check' v@(StringLiteral _) t | t == tyString =

@@ -879,7 +887,8 @@ checkFunctionApplication' fn (ForAll ident ty _) arg = do

879checkFunctionApplication' fn u@(TUnknown _) arg = do

887checkFunctionApplication' fn u@(TUnknown _) arg = do

880 arg' <- do

888 arg' <- do

881 TypedValue _ v t <- infer arg

889 TypedValue _ v t <- infer arg

890+ (v', t') <- instantiatePolyTypeWithUnknowns arg t

882− TypedValue True v <$> replaceAllVarsWithUnknowns t

891+ return $ TypedValue True v' t'

883 let ty = (\(TypedValue _ _ t) -> t) arg'

892 let ty = (\(TypedValue _ _ t) -> t) arg'

884 ret <- fresh

893 ret <- fresh

885 u =?= function ty ret

894 u =?= function ty ret