61870cb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change wording in unification errors

"Can't unify" and "Can't convert" are terrible error messages for programmers, and particularly confusing to explain to beginners, because programmers don't need to know that implementation detail. Changed to "type mismatch" and updated docs accordingly.

commit61870cb9b28319cf5aad447fbbf99508c6dc4f88 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 24 May 2015, 23:21 (11 years ago) parentf75980a

14 files changed+50−50

compare with master

unifiedsplit

docs/proofs/pluscomm.rst+2−2 docs/tutorial/provisional.rst+4−4 docs/tutorial/typesfuns.rst+4−4 src/Idris/Delaborate.hs+4−4 test/basic006/expected+2−2 test/proof002/expected+4−4 test/reg007/expected+4−4 test/reg023/expected+2−2 test/reg044/expected+4−4 test/reg054/expected+2−2 test/tutorial006/expected+8−8 test/unique001/expected+6−6 test/unique002/expected+2−2 test/unique003/expected+2−2

docs/proofs/pluscomm.rst+2−2

@@ -88,9 +88,9 @@ error:

8888::

8989

9090 When elaborating right hand side of four_eq_five:

91− Can't unify

91+ Type mismatch between

9292 x = x (Type of Refl)

93− with

93+ and

9494 4 = 5 (Expected type)

9595

9696Type checking equality proofs

docs/tutorial/provisional.rst+4−4

@@ -35,15 +35,15 @@ Unfortunately, the type checker rejects this:

3535::

3636

3737 viewsbroken.idr:12:10:When elaborating right hand side of ViewsBroken.parity:

38− Can't unify

38+ Type mismatch between

3939 Parity (plus (S j) (S j))

40− with

40+ and

4141 Parity (S (S (plus j j)))

4242

4343 Specifically:

44− Can't unify

44+ Type mismatch between

4545 plus (S j) (S j)

46− with

46+ and

4747 S (S (plus j j))

4848

4949The type checker is telling us that ``(j+1)+(j+1)`` and ``2+j+j`` do not

docs/tutorial/typesfuns.rst+4−4

@@ -309,15 +309,15 @@ following:

309309 $ idris vbroken.idr --check

310310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:

311311 When elaborating an application of constructor Vect.:::

312− Can't unify

312+ Type mismatch between

313313 Vect (k + k) a (Type of xs ++ xs)

314− with

314+ and

315315 Vect (plus k m) a (Expected type)

316316

317317 Specifically:

318− Can't unify

318+ Type mismatch between

319319 plus k k

320− with

320+ and

321321 plus k m

322322

323323

src/Idris/Delaborate.hs+4−4

@@ -231,14 +231,14 @@ pprintErr' i (InternalMsg s) =

231231pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

232232 let (x_ns, y_ns, nms) = renameMNs x_in y_in

233233 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

234− text "Can't unify" <> indented (annTm x_ns

234+ text "Type mismatch between" <> indented (annTm x_ns

235235 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

236236 ++ zip nms (repeat False)) x))

237237 <> case xprov of

238238 Nothing -> empty

239239 Just t -> text " (" <> pprintProv i sc t <> text ")"

240240 <$>

241− text "with" <> indented (annTm y_ns

241+ text "and" <> indented (annTm y_ns

242242 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

243243 ++ zip nms (repeat False)) y))

244244 <> case yprov of

@@ -257,10 +257,10 @@ pprintErr' i (CantConvert x_in y_in env) =

257257 let (x_ns, y_ns, nms) = renameMNs x_in y_in

258258 (x, y) = addImplicitDiffs (delab i (flagUnique x_ns))

259259 (delab i (flagUnique y_ns)) in

260− text "Can't convert" <>

260+ text "Type mismatch between" <>

261261 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

262262 x)) <$>

263− text "with" <>

263+ text "and" <>

264264 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

265265 y)) <>

266266 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

test/basic006/expected+2−2

@@ -1,8 +1,8 @@

11test020a.idr:16:18:When elaborating right hand side of foo:

22When elaborating an application of function Prelude.List.reverse:

3− Can't unify

3+ Type mismatch between

44 Vect n a (Type of xs)

5− with

5+ and

66 List a (Expected type)

77[3, 2, 1]

88"Number 42"

test/proof002/expected+4−4

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

11Reflect.idr:208:38:

22When elaborating right hand side of testReflect1:

33When elaborating an application of function Reflect.getJust:

4− Can't unify

4+ Type mismatch between

55 IsJust (Just x1) (Type of ItIsJust)

6− with

6+ and

77 IsJust (prove (getProof x)) (Expected type)

99 Specifically:

10− Can't unify

10+ Type mismatch between

1111 Just x

12− with

12+ and

1313 Nothing

test/reg007/expected+4−4

@@ -1,12 +1,12 @@

11reg007.lidr:8:1:A.n is already defined

22reg007.lidr:12:11-17:When elaborating right hand side of hurrah:

3−Can't unify

3+Type mismatch between

44 n = lala (Type of isSame)

5−with

5+and

66 0 = 1 (Expected type)

88Specifically:

9− Can't unify

9+ Type mismatch between

1010 1

11− with

11+ and

1212 0

test/reg023/expected+2−2

@@ -1,5 +1,5 @@

11reg023.idr:7:5:When elaborating right hand side of bad:

2−Can't unify

2+Type mismatch between

33 Nat (Type of 0)

4−with

4+and

55 f Nat (Expected type)

test/reg044/expected+4−4

@@ -1,11 +1,11 @@

11reg044.idr:4:4:When elaborating right hand side of Main.pf:

2−Can't unify

2+Type mismatch between

33 b = b (Type of Refl)

4−with

4+and

55 a = b (Expected type)

77Specifically:

8− Can't unify

8+ Type mismatch between

99 b

10− with

10+ and

1111 a

test/reg054/expected+2−2

@@ -6,7 +6,7 @@ When elaborating argument x to Main.weird:

66 No explicit types on left hand side: Char

77reg054.idr:37:1-8:When elaborating left hand side of tctrick:

88When elaborating an application of Main.tctrick:

9− Can't unify

9+ Type mismatch between

1010 Maybe a1 (Type of Just x)

11− with

11+ and

1212 a (Expected type)

test/tutorial006/expected+8−8

@@ -1,25 +1,25 @@

11tutorial006a.idr:5:23-25:

22When elaborating right hand side of vapp:

33When elaborating argument xs to constructor Data.VectType.Vect.:::

4− Can't unify

4+ Type mismatch between

55 Vect (n + n) a (Type of vapp xs xs)

6− with

6+ and

77 Vect (plus n m) a (Expected type)

99 Specifically:

10− Can't unify

10+ Type mismatch between

1111 plus n n

12− with

12+ and

1313 plus n m

1414tutorial006b.idr:10:10:

1515When elaborating right hand side of with block in Main.parity:

16−Can't unify

16+Type mismatch between

1717 Parity (plus (S j) (S j)) (Type of even)

18−with

18+and

1919 Parity (S (S (plus j j))) (Expected type)

2020

2121Specifically:

22− Can't unify

22+ Type mismatch between

2323 plus (S j) (S j)

24− with

24+ and

2525 S (S (plus j j))

test/unique001/expected+6−6

@@ -2,17 +2,17 @@

2219,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END

3338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

4438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

5−unique001a.idr:33:11:Can't convert

5+unique001a.idr:33:11:Type mismatch between

66 Int -> String

7−with

7+and

88 UniqueType (Int -> String)

9−unique001a.idr:44:12:Can't convert

9+unique001a.idr:44:12:Type mismatch between

1010 Int -> String

11−with

11+and

1212 UniqueType (Int -> String)

13−unique001a.idr:55:12:Can't convert

13+unique001a.idr:55:12:Type mismatch between

1414 UniqueType (Int -> String)

15−with

15+and

1616 Int -> String

1717unique001b.idr:16:7:Borrowed name xs must not be used on RHS

1818unique001c.idr:46:6:Unique name f is used more than once

test/unique002/expected+2−2

@@ -1,5 +1,5 @@

11unique002.idr:15:5:Unique name xs is used more than once

2−unique002a.idr:15:5:Can't convert

2+unique002a.idr:15:5:Type mismatch between

33 Int -> String

4−with

4+and

55 UniqueType (Int -> String)

test/unique003/expected+2−2

@@ -1,4 +1,4 @@

1−unique003.idr:18:5:Can't convert

1+unique003.idr:18:5:Type mismatch between

22 Int -> String

3−with

3+and

44 UniqueType (Int -> String)