@@ -47,47 +47,7 @@ instance Unifiable Type where
47 unknown = TUnknown
47 unknown = TUnknown
48 isUnknown (TUnknown u) = Just u
48 isUnknown (TUnknown u) = Just u
49 isUnknown _ = Nothing
49 isUnknown _ = Nothing
50− TUnknown u1 ~~ TUnknown u2 | u1 == u2 = return ()
50+ (~~) = unifyTypes
51− TUnknown u ~~ t = replace u t
52− t ~~ TUnknown u = replace u t
53− SaturatedTypeSynonym name1 args1 ~~ SaturatedTypeSynonym name2 args2 | name1 == name2 =
54− zipWithM_ (~~) args1 args2
55− SaturatedTypeSynonym name args ~~ ty = do
57− modulePath <- checkModulePath `fmap` lift get
58− case M.lookup (qualify modulePath name) (typeSynonyms env) of
59− Just (synArgs, body) -> do
60− let m = M.fromList $ zip synArgs args
61− let replaced = replaceTypeVars m body
63− Nothing -> error "Type synonym was not defined"
64− ty ~~ s@(SaturatedTypeSynonym _ _) = s ~~ ty
65− ForAll ident1 ty1 ~~ ForAll ident2 ty2 = do
66− sk <- skolemize ident1 ty1
67− replaced <- replaceVarsWithUnknowns [ident2] ty2
69− ForAll ident ty1 ~~ ty2 = do
70− sk <- skolemize ident ty1
72− ty ~~ f@(ForAll _ _) = f ~~ ty
73− Number ~~ Number = return ()
74− String ~~ String = return ()
75− Boolean ~~ Boolean = return ()
76− Array s ~~ Array t = s ~~ t
77− Object row1 ~~ Object row2 = row1 ~~ row2
78− Function args1 ret1 ~~ Function args2 ret2 = do
79− guardWith "Function applied to incorrect number of args" $ length args1 == length args2
80− zipWithM_ (~~) args1 args2
82− TypeVar v1 ~~ TypeVar v2 | v1 == v2 = return ()
83− TypeConstructor c1 ~~ TypeConstructor c2 = do
84− modulePath <- checkModulePath `fmap` lift get
85− guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
86− TypeApp t1 t2 ~~ TypeApp t3 t4 = do
89− Skolem s1 ~~ Skolem s2 | s1 == s2 = return ()
90− t1 ~~ t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
91 apply s (TUnknown u) = runSubstitution s u
51 apply s (TUnknown u) = runSubstitution s u
92 apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
52 apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
93 apply s (ForAll idents ty) = ForAll idents $ apply s ty
53 apply s (ForAll idents ty) = ForAll idents $ apply s ty
@@ -140,6 +100,52 @@ instance Unifiable Row where
140 unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
100 unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
141 unknowns _ = []
101 unknowns _ = []
103+unifyTypes :: Type -> Type -> Subst Check ()
104+unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2 ++ ":\n" ++ e) $ do
107+ unifyTypes' (TUnknown u1) (TUnknown u2) | u1 == u2 = return ()
108+ unifyTypes' (TUnknown u) t = replace u t
109+ unifyTypes' t (TUnknown u) = replace u t
110+ unifyTypes' (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2)
111+ | name1 == name2 = zipWithM_ unifyTypes args1 args2
112+ unifyTypes' (SaturatedTypeSynonym name args) ty = do
114+ modulePath <- checkModulePath `fmap` lift get
115+ case M.lookup (qualify modulePath name) (typeSynonyms env) of
116+ Just (synArgs, body) -> do
117+ let m = M.fromList $ zip synArgs args
118+ let replaced = replaceTypeVars m body
119+ replaced `unifyTypes` ty
120+ Nothing -> error "Type synonym was not defined"
121+ unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty
122+ unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do
123+ sk <- skolemize ident1 ty1
124+ replaced <- replaceVarsWithUnknowns [ident2] ty2
125+ sk `unifyTypes` replaced
126+ unifyTypes' (ForAll ident ty1) ty2 = do
127+ sk <- skolemize ident ty1
129+ unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty
130+ unifyTypes' Number Number = return ()
131+ unifyTypes' String String = return ()
132+ unifyTypes' Boolean Boolean = return ()
133+ unifyTypes' (Array s) (Array t) = s `unifyTypes` t
134+ unifyTypes' (Object row1) (Object row2) = row1 ~~ row2
135+ unifyTypes' (Function args1 ret1) (Function args2 ret2) = do
136+ guardWith "Function applied to incorrect number of args" $ length args1 == length args2
137+ zipWithM_ unifyTypes args1 args2
138+ ret1 `unifyTypes` ret2
139+ unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
140+ unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
141+ modulePath <- checkModulePath `fmap` lift get
142+ guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
143+ unifyTypes' (TypeApp t1 t2) (TypeApp t3 t4) = do
146+ unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()
147+ unifyTypes' t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
143isFunction :: Value -> Bool
149isFunction :: Value -> Bool
144isFunction (Abs _ _) = True
150isFunction (Abs _ _) = True
145isFunction (TypedValue untyped _) = isFunction untyped
151isFunction (TypedValue untyped _) = isFunction untyped
@@ -486,7 +492,7 @@ inferGuardedBinder m val (GuardedBinder cond binder) = do
486 ty <- infer (m `M.union` m1) cond
492 ty <- infer (m `M.union` m1) cond
487 ty ~~ Boolean
493 ty ~~ Boolean
488 return m1
494 return m1
489−inferGuardedBinder m val b = inferBinder val b >>= return
495+inferGuardedBinder m val b = inferBinder val b
491checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()
497checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()
492checkBinders _ _ _ [] = return ()
498checkBinders _ _ _ [] = return ()