@@ -49,16 +49,18 @@ solver (Context ctx (VarT x :=: VarT y) : cs) subs
4949 solver (map (cSub y (VarT x)) cs) $ Map.insert y (VarT x) subs
5050 (_, _) ->
5151 solver (map (cSub x (VarT y)) cs) $ Map.insert x (VarT y) subs
52−solver (Context ctx (VarT x :=: t) : cs) subs =
53− case Map.lookup x subs of
54− Nothing -> solver (map (cSub x t) cs) . Map.map (tSub x t) $ Map.insert x t subs
55− Just (Super ts) ->
56− let ts' = Set.intersection ts (Set.singleton t) in
57− case Set.toList ts' of
58− [] -> solver (Context ctx (t :<: Super ts) : cs) subs
59− [t'] -> solver (map (cSub x t') cs) $ Map.insert x t' subs
60− _ -> solver cs $ Map.insert x (Super ts') subs
61− Just t' -> solver (Context ctx (t' :=: t) : cs) subs
52+solver (Context ctx (VarT x :=: t) : cs) subs = do
53+ if x `occursIn` t then occursError ctx (VarT x) t else
54+ (case Map.lookup x subs of
55+ Nothing -> solver (map (cSub x t) cs) . Map.map (tSub x t) $ Map.insert x t subs
56+ Just (Super ts) ->
57+ let ts' = Set.intersection ts (Set.singleton t) in
58+ case Set.toList ts' of
59+ [] -> solver (Context ctx (t :<: Super ts) : cs) subs
60+ [t'] -> solver (map (cSub x t') cs) $ Map.insert x t' subs
61+ _ -> solver cs $ Map.insert x (Super ts') subs
62+ Just t' -> solver (Context ctx (t' :=: t) : cs) subs
63+ )
6264solver ((Context ctx (t :=: VarT x)) : cs) subs =
6365 solver ((Context ctx (VarT x :=: t)) : cs) subs
6466solver ((Context ctx (t1 :=: t2)) : cs) subs
@@ -98,6 +100,10 @@ solver (Context ctx (x :<<: s) : cs) subs
98100 prints cs'' $ solver cs'' subs
99101
100102
103+occursError ctx t1 t2 =
104+ return . Left $ "Type error: Occurs check: cannot construct the infinite type: " ++ show t1 ++
105+ " = " ++ show t2 ++
106+ " in context " ++ ctx
101107uniError ctx t1 t2 =
102108 return . Left $ "Type error: " ++ show t1 ++
103109 " is not equal to " ++ show t2 ++
@@ -109,3 +115,5 @@ unionError ctx ts ts' =
109115subtypeError ctx t s =
110116 return . Left $ concat [ "Type error: ", show t, " is not a ", show s
111117 , " in context ", ctx ]
118+
119+occursIn x t = x `elem` freeVars t