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