@@ -28,15 +28,15 @@ unify ctxt env topx topy
28 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
28 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
29 -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
29 -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
31− -- trace ("Unifying " ++ show (topx, topy)) $
31+-- trace ("Unifying " ++ show (topx, topy)) $
32 let topxn = normalise ctxt env topx
32 let topxn = normalise ctxt env topx
33− topyn = normalise ctxt env topy in
33+ topyn = normalise ctxt env topy in
34-- trace ("Unifying " ++ show (topxn, topyn)) $
34-- trace ("Unifying " ++ show (topxn, topyn)) $
35− case runStateT (un' False [] topxn topyn)
35+ case runStateT (un' False [] topxn topyn)
36− (UI 0 [] []) of
36+ (UI 0 [] []) of
37− OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
37+ OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
38-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s
38-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s
39− Error e -> tfail e
39+ Error e -> tfail e
41 notTrivial (x, P _ x' _) = x /= x'
41 notTrivial (x, P _ x' _) = x /= x'
42 notTrivial _ = True
42 notTrivial _ = True
@@ -174,9 +174,11 @@ unify ctxt env topx topy
174 combine bnames as ((n, t) : bs)
174 combine bnames as ((n, t) : bs)
175 = case lookup n as of
175 = case lookup n as of
176 Nothing -> combine bnames (as ++ [(n,t)]) bs
176 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
179− combine bnames as bs
181+ combine bnames as (ns' ++ bs)
181 -- If there are any clashes of constructors, deem it unrecoverable, otherwise some
183 -- If there are any clashes of constructors, deem it unrecoverable, otherwise some
182 -- more work may help.
184 -- more work may help.