@@ -90,14 +90,12 @@ solver aliases subs (C txt span c : cs) =
90 let ctx = C txt span
90 let ctx = C txt span
91 eq t1 t2 = ctx (t1 :=: t2)
91 eq t1 t2 = ctx (t1 :=: t2)
92 solv = solver aliases subs
92 solv = solver aliases subs
93+ uniError' = uniError (\t1 t2 -> solv (eq t1 t2 : cs)) aliases txt span
93 in case c of
94 in case c of
94 -- Destruct Type-constructors
95 -- Destruct Type-constructors
95 t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2) ->
96 t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2) ->
96 if n1 == n2 then solv (zipWith eq ts1 ts2 ++ cs)
97 if n1 == n2 then solv (zipWith eq ts1 ts2 ++ cs)
97− else let t1' = dealias aliases t1
98+ else uniError' t1 t2
98− t2' = dealias aliases t2
99− in if t1 == t1' && t2 == t2' then uniError txt span t1 t2
100− else solv (ctx (t1' :=: t2') : cs)
102 LambdaT t1 t2 :=: LambdaT t1' t2' ->
100 LambdaT t1 t2 :=: LambdaT t1' t2' ->
103 solv ([ eq t1 t1', eq t2 t2' ] ++ cs)
101 solv ([ eq t1 t1', eq t2 t2' ] ++ cs)
@@ -146,7 +144,7 @@ solver aliases subs (C txt span c : cs) =
146 t :=: VarT x -> solv ((ctx (VarT x :=: t)) : cs)
144 t :=: VarT x -> solv ((ctx (VarT x :=: t)) : cs)
148 t1 :=: t2 | t1 == t2 -> solv cs
146 t1 :=: t2 | t1 == t2 -> solv cs
149− | otherwise -> uniError txt span t1 t2
147+ | otherwise -> uniError' t1 t2
151 -- subtypes
149 -- subtypes
152 VarT x :<: Super ts ->
150 VarT x :<: Super ts ->
@@ -190,10 +188,14 @@ occursError msg span t1 t2 =
190 , "Occurs check: cannot construct the infinite type:\n"
188 , "Occurs check: cannot construct the infinite type:\n"
191 , show t1, " = ", show t2, showMsg msg ]
189 , show t1, " = ", show t2, showMsg msg ]
193−uniError msg span t1 t2 =
191+uniError solveWith aliases msg span t1 t2 =
192+ let t1' = dealias aliases t1
193+ t2' = dealias aliases t2
194+ in if t1 /= t1' || t2 /= t2'
195+ then solveWith t1' t2'
194− return . Left $ concat
196+ else return . Left $ concat
195− [ "Type error (" ++ show span ++ "):\n"
197+ [ "Type error (" ++ show span ++ "):\n"
196− , show t1, " is not equal to ", show t2, showMsg msg ]
198+ , show t1, " is not equal to ", show t2, showMsg msg ]
198unionError msg span ts ts' =
200unionError msg span ts ts' =
199 return . Left $ concat
201 return . Left $ concat