921b766 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix name propagation in error messages

Fixes #1225

commit921b766c2d2bb346d39a7f311d71aac85222b4a9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 5 Jun 2014, 15:07 (12 years ago) parent34d6f39

4 files changed+9−5

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+4 src/Idris/ElabTerm.hs+1−1 test/reg034/expected+2−2 test/tutorial006/expected+2−2

src/Idris/Core/ProofState.hs+4

@@ -823,6 +823,10 @@ updateEnv ns [] = []

823823updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env

824824

825825updateError [] err = err

826+updateError ns (At f e) = At f (updateError ns e)

827+updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

828+updateError ns (ElaboratingArg f a env e)

829+ = ElaboratingArg f a env (updateError ns e)

826830updateError ns (CantUnify b l r e xs sc)

827831 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc

828832updateError ns e = e

src/Idris/ElabTerm.hs+1−1

@@ -70,7 +70,7 @@ build ist info pattern opts fn tm

7070

7171 when (not pattern) $

7272 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++

73− "Remaining problems:\n" ++ show probs) $

73+ "Remaining problems:\n" ++ qshow probs) $

7474 do unify_all; matchProblems True; unifyProblems

7575

7676 probs <- get_probs

test/reg034/expected+2−2

@@ -1,7 +1,7 @@

11reg034.idr:6:5:When elaborating left hand side of bar:

22When elaborating an application of main.bar:

33 Can't unify

4− [95mx[0m [94m=[0m [95mx[0m

4+ [92mlength[0m [95mys[0m [94m=[0m [92mlength[0m [95mys[0m

55 with

66 [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m [95mys[0m

@@ -13,7 +13,7 @@ When elaborating an application of main.bar:

1313reg034.idr:9:5:When elaborating left hand side of foo:

1414When elaborating an application of main.foo:

1515 Can't unify

16− [95mx[0m [94m=[0m [95mx[0m

16+ [95mf[0m [95my[0m [94m=[0m [95mf[0m [95my[0m

1717 with

1818 [95mf[0m [95mx[0m [94m=[0m [95mf[0m [95my[0m

1919

test/tutorial006/expected+2−2

@@ -1,13 +1,13 @@

11tutorial006a.idr:3:23:When elaborating right hand side of vapp:

22When elaborating argument [95mxs[0m to constructor [91mPrelude.Vect.::[0m:

33 Can't unify

4− [94mVect[0m ([95mn[0m [92m+[0m [95mm[0m) [95ma[0m

4+ [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m

55 with

66 [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m

88 Specifically:

99 Can't unify

10− [92mplus[0m [95mn[0m [95mm[0m

10+ [92mplus[0m [95mn[0m [95mn[0m

1111 with

1212 [92mplus[0m [95mn[0m [95mm[0m

1313tutorial006b.idr:10:10:When elaborating right hand side of Main.parity: