c44a35c · Idris-dev · git.iko.soy

src/Idris/Delaborate.hs+3

compare with master

unifiedsplit

@@ -205,6 +205,9 @@ pprintErr' i (CantUnify _ x_in y_in e sc s) =

205 ++ zip nms (repeat False)) y)) <>

206 case e of

207 Msg "" -> empty

208+ -- if the specific error is the same as the one we just printed,

209+ -- there's no need to print it

210+ CantUnify _ x_in' y_in' _ _ _ | x_in == x_in' && y_in == y_in' -> empty

208 _ -> line <> line <> text "Specifically:" <>

211 _ -> line <> line <> text "Specifically:" <>

209 indented (pprintErr' i e) <>

212 indented (pprintErr' i e) <>

210 if (opt_errContext (idris_options i)) then showSc i sc else empty

213 if (opt_errContext (idris_options i)) then showSc i sc else empty

test/basic006/expected−6

@@ -4,11 +4,5 @@ When elaborating an application of function Prelude.List.reverse:

4 Vect n a

5 with

6 List a

7−

8− Specifically:

9− Can't unify

10− Vect n a

11− with

12− List a

13[3, 2, 1]

7[3, 2, 1]

14"Number 42"

8"Number 42"

test/reg010/expected−6

@@ -3,9 +3,3 @@ Can't unify

3 P x

4with

5 P y

6−

7−Specifically:

8− Can't unify

9− P x

10− with

11− P y

test/reg023/expected−6

@@ -3,9 +3,3 @@ Can't unify

3 [94mNat[0m

4with

5 [92mf[0m [94mNat[0m

6−

7−Specifically:

8− Can't unify

9− [94mNat[0m

10− with

11− [92mf[0m [94mNat[0m