@@ -28,15 +28,15 @@ unify ctxt env topx topy
2828 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
2929 -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
3030 -- _ ->
31− -- trace ("Unifying " ++ show (topx, topy)) $
31+-- trace ("Unifying " ++ show (topx, topy)) $
3232 let topxn = normalise ctxt env topx
33− topyn = normalise ctxt env topy in
33+ topyn = normalise ctxt env topy in
3434-- trace ("Unifying " ++ show (topxn, topyn)) $
35− case runStateT (un' False [] topxn topyn)
36− (UI 0 [] []) of
37− OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
35+ case runStateT (un' False [] topxn topyn)
36+ (UI 0 [] []) of
37+ OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
3838-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s
39− Error e -> tfail e
39+ Error e -> tfail e
4040 where
4141 notTrivial (x, P _ x' _) = x /= x'
4242 notTrivial _ = True
@@ -174,9 +174,11 @@ unify ctxt env topx topy
174174 combine bnames as ((n, t) : bs)
175175 = case lookup n as of
176176 Nothing -> combine bnames (as ++ [(n,t)]) bs
177− Just t' -> do un' False bnames t t'
177+ Just t' -> do ns <- un' False bnames t t'
178+ -- make sure there's n mapping from n in ns
179+ let ns' = filter (\ (x, _) -> x/=n) ns
178180 sc 1
179− combine bnames as bs
181+ combine bnames as (ns' ++ bs)
180182
181183 -- If there are any clashes of constructors, deem it unrecoverable, otherwise some
182184 -- more work may help.