@@ -167,10 +167,14 @@ pprintErr' i (InternalMsg s) =
167167 text ("Please consider reporting at " ++ bugaddr)
168168 ]
169169pprintErr' i (CantUnify _ x_in y_in e sc s) =
170− let (x_ns, y_ns) = renameMNs x_in y_in
170+ let (x_ns, y_ns, nms) = renameMNs x_in y_in
171171 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in
172− text "Can't unify" <> indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) x)) <$>
173− text "with" <> indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) y)) <>
172+ text "Can't unify" <> indented (annTm x_ns
173+ (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
174+ ++ zip nms (repeat False)) x)) <$>
175+ text "with" <> indented (annTm y_ns
176+ (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
177+ ++ zip nms (repeat False)) y)) <>
174178 case e of
175179 Msg "" -> empty
176180 _ -> line <> line <> text "Specifically:" <>
@@ -269,26 +273,19 @@ pprintErr' i (ReflectionFailed msg err) =
269273-- Make sure the machine invented names are shown helpfully to the user, so
270274-- that any names which differ internally also differ visibly
271275-- FIXME: I can't actually contrive an error to test this! Will revisit later...
272−renameMNs :: Term -> Term -> (Term, Term)
276+renameMNs :: Term -> Term -> (Term, Term, [Name])
273277renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y
274− newnames = execState getRenames (zip ns ns) in
275− (rename newnames x, rename newnames y)
278+ newnames = evalState (getRenames [] ns) 1 in
279+ (rename newnames x, rename newnames y, map snd newnames)
276280 where
277− getRenames :: State [(Name, Name)] ()
278− getRenames = do getRs x; getRs y
279−
280− getRs :: Term -> State [(Name, Name)] ()
281− getRs (P _ n@(MN i x) _) = do
282− nmap <- get
283− when (n `notElem` map fst nmap) $
284− put $ (n, uniqueName n (map fst nmap)) : nmap
285− getRs (App f a) = do getRs f; getRs a
286− getRs (Bind n b sc) = do
287− nmap <- get
288− when (n `notElem` map fst nmap) $
289− put $ (n, uniqueName n (map fst nmap)) : nmap
290− getRs sc
291− getRs t = return ()
281+ getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
282+ getRenames acc [] = return acc
283+ getRenames acc (n@(MN i x) : xs) | UN x `elem` xs
284+ = do idx <- get
285+ put (idx + 1)
286+ let x' = sUN (str x ++ show idx)
287+ getRenames ((n, x') : acc) xs
288+ getRenames acc (x : xs) = getRenames acc xs
292289
293290 rename :: [(Name, Name)] -> Term -> Term
294291 rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t