@@ -28,14 +28,14 @@ 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
3333 topyn = normalise ctxt env topy in
3434-- trace ("Unifying " ++ show (topxn, topyn)) $
3535 case runStateT (un' False [] topxn topyn)
3636 (UI 0 [] []) of
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
37+ OK (v, UI _ inj fails) ->
38+ return (filter notTrivial v, inj, reverse fails)
3939 Error e -> tfail e
4040 where
4141 notTrivial (x, P _ x' _) = x /= x'
@@ -75,12 +75,18 @@ unify ctxt env topx topy
7575 | (x,y) `elem` bnames = do sc 1; return []
7676 un' fn bnames (P Bound x _) tm
7777 | holeIn env x = do UI s i f <- get
78− when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)
78+ -- injectivity check
79+ when (notP tm && fn) $
80+-- trace (show (x, tm, normalise ctxt env tm)) $
81+ put (UI s ((tm, topx, topy) : i) f)
7982 sc 1
8083 checkCycle (x, tm)
8184 un' fn bnames tm (P Bound y _)
8285 | holeIn env y = do UI s i f <- get
83− when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)
86+ -- injectivity check
87+ when (notP tm && fn) $
88+-- trace (show (y, tm, normalise ctxt env tm)) $
89+ put (UI s ((tm, topx, topy) : i) f)
8490 sc 1
8591 checkCycle (y, tm)
8692 un' fn bnames (V i) (P Bound x _)