@@ -69,7 +69,20 @@ match_unify ctxt env topx topy inj holes from =
69 return (map (renameBinders env) (trimSolutions v))
69 return (map (renameBinders env) (trimSolutions v))
70 _ -> tfail e
70 _ -> tfail e
72−
72+ -- This rule is highly dubious... it certainly produces a valid answer
73+ -- but it scares me. However, matching is never guaranteed to give a unique
74+ -- answer, merely a valid one, so perhaps we're okay.
75+ -- In other words: it may vanish without warning some day :)
76+ un names x tm@(App (P _ f (Bind fn (Pi t) sc)) a)
77+ | (P (DCon _ _) _ _, _) <- unApply x,
78+ holeIn env f || f `elem` holes
79+ = let n' = uniqueName (sMN 0 "mv") (map fst env) in
80+ checkCycle names (f, Bind n' (Lam t) x)
81+ un names tm@(App (P _ f (Bind fn (Pi t) sc)) a) x
82+ | (P (DCon _ _) _ _, _) <- unApply x,
83+ holeIn env f || f `elem` holes
84+ = let n' = uniqueName fn (map fst env) in
85+ checkCycle names (f, Bind n' (Lam t) x)
74 un names (P _ x _) tm
87 un names (P _ x _) tm
75 | holeIn env x || x `elem` holes
88 | holeIn env x || x `elem` holes