839d3e2 · elk · git.iko.soy

git.iko.soy/elk

on master help sign in

Add occurs check to unification.

839d3e2evancz14 years ago

elm/src/Types/Substitutions.hs+1

compare with master

unifiedsplit

@@ -3,6 +3,7 @@ module Types.Substitutions (cSub

3 ,tSub

4 ,cSubNoContext

5 ,cFreeVars

6+ ,freeVars

6 ,schemeSub

7 ,schemeSub

7 ,concretize

8 ,concretize

8 ,rescheme

9 ,rescheme

elm/src/Types/Unify.hs+18−10

@@ -49,16 +49,18 @@ solver (Context ctx (VarT x :=: VarT y) : cs) subs

49 solver (map (cSub y (VarT x)) cs) $ Map.insert y (VarT x) subs

50 (_, _) ->

51 solver (map (cSub x (VarT y)) cs) $ Map.insert x (VarT y) subs

52−solver (Context ctx (VarT x :=: 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

53− case Map.lookup x subs of

54+ (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+ Nothing -> solver (map (cSub x t) cs) . Map.map (tSub x t) $ Map.insert x t subs

55− Just (Super ts) ->

56+ Just (Super ts) ->

56− let ts' = Set.intersection ts (Set.singleton t) in

57+ let ts' = Set.intersection ts (Set.singleton t) in

57− case Set.toList ts' of

58+ case Set.toList ts' of

58− [] -> solver (Context ctx (t :<: Super ts) : cs) subs

59+ [] -> solver (Context ctx (t :<: Super ts) : cs) subs

59− [t'] -> solver (map (cSub x t') cs) $ Map.insert x t' subs

60+ [t'] -> solver (map (cSub x t') cs) $ Map.insert x t' subs

60− _ -> solver cs $ Map.insert x (Super ts') subs

61+ _ -> solver cs $ Map.insert x (Super ts') subs

61− Just t' -> solver (Context ctx (t' :=: t) : cs) subs

62+ Just t' -> solver (Context ctx (t' :=: t) : cs) subs

63+ )

62solver ((Context ctx (t :=: VarT x)) : cs) subs =

64solver ((Context ctx (t :=: VarT x)) : cs) subs =

63 solver ((Context ctx (VarT x :=: t)) : cs) subs

65 solver ((Context ctx (VarT x :=: t)) : cs) subs

64solver ((Context ctx (t1 :=: t2)) : cs) subs

66solver ((Context ctx (t1 :=: t2)) : cs) subs

@@ -98,6 +100,10 @@ solver (Context ctx (x :<<: s) : cs) subs

98 prints cs'' $ solver cs'' subs

100 prints cs'' $ solver cs'' subs

101

100

102

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

101uniError ctx t1 t2 =

107uniError ctx t1 t2 =

102 return . Left $ "Type error: " ++ show t1 ++

108 return . Left $ "Type error: " ++ show t1 ++

103 " is not equal to " ++ show t2 ++

109 " is not equal to " ++ show t2 ++

@@ -109,3 +115,5 @@ unionError ctx ts ts' =

109subtypeError ctx t s =

115subtypeError ctx t s =

110 return . Left $ concat [ "Type error: ", show t, " is not a ", show s

116 return . Left $ concat [ "Type error: ", show t, " is not a ", show s

111 , " in context ", ctx ]

117 , " in context ", ctx ]

118+

119+occursIn x t = x `elem` freeVars t