@@ -66,20 +66,24 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [Fail
6666match_unify ctxt env topx topy inj holes from =
6767 case runStateT (un [] (renameBindersTm env topx)
6868 (renameBindersTm env topy)) (UI 0 []) of
69− OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
69+ OK (v, UI _ []) ->
70+ do v' <- trimSolutions topx topy from env v
71+ return (map (renameBinders env) v')
7072 res ->
7173 let topxn = renameBindersTm env (normalise ctxt env topx)
7274 topyn = renameBindersTm env (normalise ctxt env topy) in
7375 case runStateT (un [] topxn topyn)
7476 (UI 0 []) of
7577 OK (v, UI _ fails) ->
76− return (map (renameBinders env) (trimSolutions v))
78+ do v' <- trimSolutions topx topy from env v
79+ return (map (renameBinders env) v')
7780 Error e ->
7881 -- just normalise the term we're matching against
7982 case runStateT (un [] topxn topy)
8083 (UI 0 []) of
8184 OK (v, UI _ fails) ->
82− return (map (renameBinders env) (trimSolutions v))
85+ do v' <- trimSolutions topx topy from env v
86+ return (map (renameBinders env) v')
8387 _ -> tfail e
8488 where
8589 -- This rule is highly dubious... it certainly produces a valid answer
@@ -227,7 +231,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm
227231 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
228232 explicitHole t = t
229233
230−trimSolutions ns = followSols (dropPairs ns)
234+trimSolutions topx topy from env topns = followSols [] (dropPairs topns)
231235 where dropPairs [] = []
232236 dropPairs (n@(x, P _ x' _) : ns)
233237 | x == x' = dropPairs ns
@@ -238,11 +242,19 @@ trimSolutions ns = followSols (dropPairs ns)
238242 _ -> True) ns)
239243 dropPairs (n : ns) = n : dropPairs ns
240244
241− followSols [] = []
242− followSols ((n, P _ t _) : ns)
245+ followSols vs [] = return []
246+ followSols vs ((n, P _ t _) : ns)
243247 | Just t' <- lookup t ns
244− = followSols ((n, t') : ns) -- Are we guaranteed no cycles?
245− followSols (n : ns) = n : followSols ns
248+ = do vs' <- case t' of
249+ P _ tn _ ->
250+ if (n, tn) `elem` vs then -- cycle
251+ tfail (cantUnify from False topx topy
252+ (Msg "") (errEnv env) 0)
253+ else return ((n, tn) : vs)
254+ _ -> return vs
255+ followSols vs' ((n, t') : ns)
256+ followSols vs (n : ns) = do ns' <- followSols vs ns
257+ return $ n : ns'
246258
247259expandLets env (x, tm) = (x, doSubst (reverse env) tm)
248260 where
@@ -267,8 +279,8 @@ unify ctxt env topx topy inj holes usersupp from =
267279 -- don't bother if topx and topy are different at the head
268280 case runStateT (un False [] (renameBindersTm env topx)
269281 (renameBindersTm env topy)) (UI 0 []) of
270− OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),
271− [])
282+ OK (v, UI _ []) -> do v' <- trimSolutions topx topy from env v
283+ return (map (renameBinders env) v', [])
272284 res ->
273285 let topxn = renameBindersTm env (normalise ctxt env topx)
274286 topyn = renameBindersTm env (normalise ctxt env topy) in
@@ -276,8 +288,8 @@ unify ctxt env topx topy inj holes usersupp from =
276288 case runStateT (un False [] topxn topyn)
277289 (UI 0 []) of
278290 OK (v, UI _ fails) ->
279− return (map (renameBinders env) (trimSolutions v),
280− reverse fails)
291+ do v' <- trimSolutions topx topy from env v
292+ return (map (renameBinders env) v', reverse fails)
281293-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
282294 Error e -> tfail e
283295 where