@@ -164,14 +164,15 @@ pprintErr' i (InternalMsg s) =
164164 text "This is probably a bug, or a missing error message.",
165165 text ("Please consider reporting at " ++ bugaddr)
166166 ]
167−pprintErr' i (CantUnify _ x y e sc s) =
168− text "Can't unify" <> indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x))) <$>
169− text "with" <> indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y))) <>
170− case e of
171− Msg "" -> empty
172− _ -> line <> line <> text "Specifically:" <>
173− indented (pprintErr' i e) <>
174− if (opt_errContext (idris_options i)) then showSc i sc else empty
167+pprintErr' i (CantUnify _ x_in y_in e sc s) =
168+ let (x, y) = addImplicitDiffs (delab i x_in) (delab i y_in) in
169+ text "Can't unify" <> indented (annTm x_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) x)) <$>
170+ text "with" <> indented (annTm y_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) y)) <>
171+ case e of
172+ Msg "" -> empty
173+ _ -> line <> line <> text "Specifically:" <>
174+ indented (pprintErr' i e) <>
175+ if (opt_errContext (idris_options i)) then showSc i sc else empty
175176pprintErr' i (CantConvert x y env) =
176177 text "Can't convert" <>
177178 indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <$>
@@ -262,6 +263,68 @@ pprintErr' i (ReflectionFailed msg err) =
262263 indented (pprintErr' i err) <>
263264 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
264265
266+-- If the two terms only differ in their implicits, mark the implicits which
267+-- differ as AlwaysShow so that they appear in errors
268+addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)
269+addImplicitDiffs x y
270+ = if (x `expLike` y) then addI x y else (x, y)
271+ where
272+ addI :: PTerm -> PTerm -> (PTerm, PTerm)
273+ addI (PApp fc f as) (PApp gc g bs)
274+ = let (as', bs') = addShows as bs in
275+ (PApp fc f as', PApp gc g bs')
276+ where addShows [] [] = ([], [])
277+ addShows (a:as) (b:bs)
278+ = let (as', bs') = addShows as bs
279+ (a', b') = addI (getTm a) (getTm b) in
280+ if (not (a' `expLike` b'))
281+ then (a { argopts = AlwaysShow : argopts a,
282+ getTm = a' } : as',
283+ b { argopts = AlwaysShow : argopts b,
284+ getTm = b' } : bs')
285+ else (a { getTm = a' } : as',
286+ b { getTm = b' } : bs')
287+ addI (PLam n a b) (PLam n' c d)
288+ = let (a', c') = addI a c
289+ (b', d') = addI b d in
290+ (PLam n a' b', PLam n' c' d')
291+ addI (PPi p n a b) (PPi p' n' c d)
292+ = let (a', c') = addI a c
293+ (b', d') = addI b d in
294+ (PPi p n a' b', PPi p' n' c' d')
295+ addI (PRefl fc a) (PRefl fc' b)
296+ = let (a', b') = addI a b in
297+ (PRefl fc a', PRefl fc' b')
298+ addI (PEq fc a b) (PEq fc' c d)
299+ = let (a', c') = addI a c
300+ (b', d') = addI b d in
301+ (PEq fc a' b', PEq fc' c' d')
302+ addI (PPair fc pi a b) (PPair fc' pi' c d)
303+ = let (a', c') = addI a c
304+ (b', d') = addI b d in
305+ (PPair fc pi a' b', PPair fc' pi' c' d')
306+ addI (PDPair fc pi a t b) (PDPair fc' pi' c u d)
307+ = let (a', c') = addI a c
308+ (t', u') = addI t u
309+ (b', d') = addI b d in
310+ (PDPair fc pi a' t' b', PDPair fc' pi' c' u' d')
311+ addI x y = (x, y)
312+
313+ -- Just the ones which appear desugared in errors
314+ expLike (PRef _ n) (PRef _ n') = n == n'
315+ expLike (PApp _ f as) (PApp _ f' as')
316+ = expLike f f' && length as == length as' &&
317+ and (zipWith expLike (getExps as) (getExps as'))
318+ expLike (PPi _ n s t) (PPi _ n' s' t')
319+ = n == n' && expLike s s' && expLike t t'
320+ expLike (PLam n s t) (PLam n' s' t')
321+ = n == n' && expLike s s' && expLike t t'
322+ expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'
323+ expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'
324+ expLike (PEq _ x y) (PEq _ x' y') = expLike x x' && expLike y y'
325+ expLike (PRefl _ x) (PRefl _ x') = expLike x x'
326+ expLike x y = x == y
327+
265328isUN :: Name -> Bool
266329isUN (UN n) = not $ T.isPrefixOf (T.pack "__") n -- TODO figure out why MNs are getting rewritte to UNs for top-level pattern-matching functions
267330isUN (NS n _) = isUN n