7d0c06b · Idris-dev · git.iko.soy

src/Idris/Output.hs+11−5

compare with master

unifiedsplit

@@ -82,18 +82,24 @@ iWarn fc err =

82 case idris_outputmode i of

83 RawOutput h ->

84 do maybeSource <- readSource fc

85− let maybeFormattedSource = maybeSource >>= formatWarning fc

85+ let maybeFormattedSource = (maybeSource >>= formatWarning fc)

86 err' <- iRender . fmap (fancifyAnnots i True) $

87− (case fc of

88− FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err

89− _ -> err) <>

90− string (maybe "" ("\n" ++) maybeFormattedSource)

87+ layoutError (formatFC fc) (fmap string maybeFormattedSource) err

91 hWriteDoc h i err'

88 hWriteDoc h i err'

92 IdeMode n h ->

89 IdeMode n h ->

93 do err' <- iRender . fmap (fancifyAnnots i True) $ err

90 do err' <- iRender . fmap (fancifyAnnots i True) $ err

94 let (str, spans) = displaySpans err'

91 let (str, spans) = displaySpans err'

95 runIO . hPutStrLn h $

92 runIO . hPutStrLn h $

96 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

93 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

94+ where

95+ formatFC :: FC -> Doc OutputAnnotation

96+ formatFC (FC fn _ _) | fn /= "" = text (show fc) <> colon

97+ formatFC _ = empty

98+

99+ layoutError :: Doc OutputAnnotation -> Maybe (Doc OutputAnnotation) -> Doc OutputAnnotation -> Doc OutputAnnotation

100+ layoutError loc (Just src) err = loc <$$> src <$$> err

101+ layoutError loc Nothing err = loc </> err

102+

97

103

98iRender :: Doc a -> Idris (SimpleDoc a)

104iRender :: Doc a -> Idris (SimpleDoc a)

99iRender d = do w <- getWidth

105iRender d = do w <- getWidth

test/basic002/expected+2−2

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

1test006.idr:25:23-27:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

425 | Main.parity_lemma_2 = proof {

325 | Main.parity_lemma_2 = proof {

5 | ~~~~~

4 | ~~~~~

6−test006.idr:32:23-27:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+test006.idr:32:23-27:

8 |

7 |

932 | Main.parity_lemma_1 = proof {

832 | Main.parity_lemma_1 = proof {

10 | ~~~~~

9 | ~~~~~

10+This style of tactic proof is deprecated. See %runElab for the replacement.

11[False, True, False, True, False, True]

test/basic006/expected+5−4

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

1+test020a.idr:16:10-19:

2+ |

3+16 | foo xs = reverse xs

4+ | ~~~~~~~~~~

1−test020a.idr:16:10-19:When checking right hand side of foo with expected type

5+When checking right hand side of foo with expected type

2 List a

6 List a

3

7

4When checking an application of function Prelude.List.reverse:

8When checking an application of function Prelude.List.reverse:

@@ -6,8 +10,5 @@ When checking an application of function Prelude.List.reverse:

6 Vect n a (Type of xs)

10 Vect n a (Type of xs)

7 and

11 and

8 List a (Expected type)

12 List a (Expected type)

9− |

10−16 | foo xs = reverse xs

11− | ~~~~~~~~~~

12[3, 2, 1]

13[3, 2, 1]

13"Number 42"

14"Number 42"

test/basic009/expected+10−7

@@ -1,10 +1,15 @@

1MAIN-PASS

2−Faulty.idr:6:9-11:num is bound as an implicit

2+Faulty.idr:6:9-11:

3− Did you mean to refer to A.num?

4 |

3 |

56 | fault : num = Z

46 | fault : num = Z

6 | ~~~

5 | ~~~

6+num is bound as an implicit

7+ Did you mean to refer to A.num?

8+Faulty.idr:7:7-12:

9+ |

10+7 | fault = Refl

11+ | ~~~~~~

7−Faulty.idr:7:7-12:When checking right hand side of fault with expected type

12+When checking right hand side of fault with expected type

8 num = 0

13 num = 0

9

14

10Type mismatch between

15Type mismatch between

@@ -17,10 +22,8 @@ Specifically:

17 0

22 0

18 and

23 and

19 num

24 num

20− |

21−7 | fault = Refl

22− | ~~~~~~

23−Multiple.idr:3:21:import alias not unique: "X"

25+Multiple.idr:3:21:

24 |

26 |

253 | import Data.Vect as X

273 | import Data.Vect as X

26 | ^

28 | ^

29+import alias not unique: "X"

test/basic016/expected+1−1

@@ -1 +1 @@

1−Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB

1+ Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB

test/basic017/expected+4−3

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

1−basic017a.idr:11:8:When checking type of Main.append:

1+basic017a.idr:11:8:

2−When checking an application of Main.Vect:

3− No such variable n

4 |

2 |

511 | append : Vect n a -> Vect m a -> Vect (n + m) a

311 | append : Vect n a -> Vect m a -> Vect (n + m) a

6 | ^

4 | ^

5+When checking type of Main.append:

6+When checking an application of Main.Vect:

7+ No such variable n

test/basic018/expected+8−7

@@ -1,16 +1,20 @@

1basic018.idr:7:12-16:

2−thing is bound as an implicit

3− Did you mean to refer to Main.thing?

4 |

2 |

57 | Vect thing elem

37 | Vect thing elem

6 | ~~~~~

4 | ~~~~~

7−basic018.idr:12:8-12:

8thing is bound as an implicit

5thing is bound as an implicit

9 Did you mean to refer to Main.thing?

6 Did you mean to refer to Main.thing?

7+basic018.idr:12:8-12:

10 |

8 |

1112 | test : thing = S 41

912 | test : thing = S 41

12 | ~~~~~

10 | ~~~~~

11+thing is bound as an implicit

12+ Did you mean to refer to Main.thing?

13+basic018.idr:13:6-11:

14+ |

15+13 | test = Refl

16+ | ~~~~~~

13−basic018.idr:13:6-11:When checking right hand side of test with expected type

17+When checking right hand side of test with expected type

14 thing = S 41

18 thing = S 41

15

19

16Type mismatch between

20Type mismatch between

@@ -23,6 +27,3 @@ Specifically:

23 42

27 42

24 and

28 and

25 thing

29 thing

26− |

27−13 | test = Refl

28− | ~~~~~~

test/directives001/expected+14−8

@@ -1,30 +1,36 @@

1−directives001.idr:14:7:Use of deprecated name directives001.Foo

1+directives001.idr:14:7:

2−To be replaced with `Bar`.

3 |

2 |

414 | mkFoo : String -> Foo

314 | mkFoo : String -> Foo

5 | ^

4 | ^

6−directives001.idr:14:7:Use of deprecated name directives001.Foo

5+Use of deprecated name directives001.Foo

7To be replaced with `Bar`.

6To be replaced with `Bar`.

7+directives001.idr:14:7:

8 |

914 | mkFoo : String -> Foo

10 | ^

11−directives001.idr:15:7-13:Use of deprecated name directives001.Foo

11+Use of deprecated name directives001.Foo

12To be replaced with `Bar`.

13+directives001.idr:15:7-13:

13 |

14 |

1415 | mkFoo = MkFoo

1515 | mkFoo = MkFoo

15 | ~~~~~~~

16 | ~~~~~~~

16−directives001.idr:15:7-13:Use of deprecated name directives001.Foo

17+Use of deprecated name directives001.Foo

17To be replaced with `Bar`.

18To be replaced with `Bar`.

19+directives001.idr:15:7-13:

18 |

20 |

1915 | mkFoo = MkFoo

2115 | mkFoo = MkFoo

20 | ~~~~~~~

22 | ~~~~~~~

23+Use of deprecated name directives001.Foo

24+To be replaced with `Bar`.

21−directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar

25+directives001.idr:26:8-28:28:

22−How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

23 |

26 |

2426 | main = do

2726 | main = do

25 | ~~~~ ...

28 | ~~~~ ...

26−directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar

29+Use of a fragile construct directives001.mkBar

27How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

30How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

31+directives001.idr:26:8-28:28:

28 |

32 |

2926 | main = do

3326 | main = do

30 | ~~~~ ...

34 | ~~~~ ...

35+Use of a fragile construct directives001.mkBar

36+How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

test/directives002/expected+1−1

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

1directives002.idr:12:3-14:28:

2−directives002.Main.main is possibly not total due to: directives002.loop

3 |

2 |

412 | main = do

312 | main = do

5 | ~~~~~~~~~ ...

4 | ~~~~~~~~~ ...

5+directives002.Main.main is possibly not total due to: directives002.loop

test/effects003/expected+1−1

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

1hangman.idr:204:8-12:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

4204 | wlen = proof search

3204 | wlen = proof search

5 | ~~~~~

4 | ~~~~~

5+This style of tactic proof is deprecated. See %runElab for the replacement.

6------------

7

86 guesses left

test/error001/expected+5−4

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

1+test002.idr:1:6:

2+ |

3+1 | myid : (a : Type) -> a -> a

4+ | ^

1−test002.idr:1:6:Universe inconsistency.

5+Universe inconsistency.

2 Working on: ./test002.idr.z

6 Working on: ./test002.idr.z

3 Old domain: (6,6)

7 Old domain: (6,6)

4 New domain: (6,5)

8 New domain: (6,5)

@@ -6,6 +10,3 @@ test002.idr:1:6:Universe inconsistency.

6 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

10 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

7 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}

11 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}

8 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

12 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

9− |

10−1 | myid : (a : Type) -> a -> a

11− | ^

test/error003/expected+3−3

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

1ErrorReflection.idr:68:5-20:

2+ |

3+68 | bad = Lam (Var Here)

4+ | ~~~~~~~~~~~~~~~~

2When checking right hand side of bad with expected type

5When checking right hand side of bad with expected type

3 Tm [] TUnit

6 Tm [] TUnit

4

7

5DSL type error: (t(504) => t'(503)) doesn't match ()

8DSL type error: (t(504) => t'(503)) doesn't match ()

6− |

7−68 | bad = Lam (Var Here)

8− | ~~~~~~~~~~~~~~~~

test/error004/expected+6−6

@@ -1,18 +1,18 @@

1FunErrTest.idr:35:12-18:

2+ |

3+35 | badCadr1 = cadr []

4+ | ~~~~~~~

2When checking right hand side of badCadr1 with expected type

5When checking right hand side of badCadr1 with expected type

3 Int

6 Int

4

7

5When checking argument cons2 to function FunErrTest.cadr:

8When checking argument cons2 to function FunErrTest.cadr:

6 Could not prove that [] has at least two elements.

9 Could not prove that [] has at least two elements.

7− |

8−35 | badCadr1 = cadr []

9− | ~~~~~~~

10FunErrTest.idr:38:12-19:

11+ |

12+38 | badCadr2 = cadr [1]

13+ | ~~~~~~~~

11When checking right hand side of badCadr2 with expected type

14When checking right hand side of badCadr2 with expected type

12 Int

15 Int

13

16

14When checking argument cons2 to function FunErrTest.cadr:

17When checking argument cons2 to function FunErrTest.cadr:

15 Could not prove that [] has at least two elements.

18 Could not prove that [] has at least two elements.

16− |

17−38 | badCadr2 = cadr [1]

18− | ~~~~~~~~

test/error005/expected+21−16

@@ -1,46 +1,51 @@

1+error005.idr:11:7:

2+ |

3+11 | two = 2

4+ | ^

1−error005.idr:11:7:When checking right hand side of two with expected type

5+When checking right hand side of two with expected type

2 Fin 2

6 Fin 2

3

7

4When checking argument prf to function Data.Fin.fromInteger:

8When checking argument prf to function Data.Fin.fromInteger:

5 When using 2 as a literal for a Fin 2

9 When using 2 as a literal for a Fin 2

6 2 is not strictly less than 2

10 2 is not strictly less than 2

11+error005.idr:14:12:

7 |

12 |

8−11 | two = 2

13+14 | hahaha n = 0

9− | ^

14+ | ^

10−error005.idr:14:12:When checking right hand side of hahaha with expected type

15+When checking right hand side of hahaha with expected type

11 Fin n

16 Fin n

12

17

13When checking argument prf to function Data.Fin.fromInteger:

18When checking argument prf to function Data.Fin.fromInteger:

14 When using 0 as a literal for a Fin n

19 When using 0 as a literal for a Fin n

15 0 is not strictly less than n

20 0 is not strictly less than n

21+error005.idr:20:11:

16 |

22 |

17−14 | hahaha n = 0

23+20 | notOk n = 2

18− | ^

24+ | ^

19−error005.idr:20:11:When checking right hand side of notOk with expected type

25+When checking right hand side of notOk with expected type

20 Fin (plus 2 n)

26 Fin (plus 2 n)

21

27

22When checking argument prf to function Data.Fin.fromInteger:

28When checking argument prf to function Data.Fin.fromInteger:

23 When using 2 as a literal for a Fin (S (S n))

29 When using 2 as a literal for a Fin (S (S n))

24 2 is not strictly less than S (S n)

30 2 is not strictly less than S (S n)

31+error005.idr:23:12-24:

25 |

32 |

26−20 | notOk n = 2

33+23 | b0rken n = fromInteger n

27− | ^

34+ | ~~~~~~~~~~~~~

28−error005.idr:23:12-24:When checking right hand side of b0rken with expected type

35+When checking right hand side of b0rken with expected type

29 Fin 3

36 Fin 3

30

37

31When checking argument prf to function Data.Fin.fromInteger:

38When checking argument prf to function Data.Fin.fromInteger:

32 When using n as a literal for a Fin 3

39 When using n as a literal for a Fin 3

33 Could not show that n is less than 3 because n is a bound

40 Could not show that n is less than 3 because n is a bound

34 variable instead of a constant Integer

41 variable instead of a constant Integer

42+error005.idr:26:17:

35 |

43 |

36−23 | b0rken n = fromInteger n

44+26 | x = the (Fin 4) 5

37− | ~~~~~~~~~~~~~

45+ | ^

38−error005.idr:26:17:When checking right hand side of x with expected type

46+When checking right hand side of x with expected type

39 Fin 4

47 Fin 4

40

48

41When checking argument prf to function Data.Fin.fromInteger:

49When checking argument prf to function Data.Fin.fromInteger:

42 When using 5 as a literal for a Fin 4

50 When using 5 as a literal for a Fin 4

43 5 is not strictly less than 4

51 5 is not strictly less than 4

44− |

45−26 | x = the (Fin 4) 5

46− | ^

test/error006/expected+3−2

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

1−WithPatsNoWith.idr:4:1-13:When checking left hand side of foo:

1+WithPatsNoWith.idr:4:1-13:

2−unexpected patterns outside of "with" block

3 |

2 |

44 | foo 1 | 2 | 3 = True

34 | foo 1 | 2 | 3 = True

5 | ~~~~~~~~~~~~~

4 | ~~~~~~~~~~~~~

5+When checking left hand side of foo:

6+unexpected patterns outside of "with" block

test/error007/expected+3−3

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

1error007.idr:26:7-29:

2+ |

3+26 | send_page conn str code -- (prim__zextB32_Int code)

4+ | ~~~~~~~~~~~~~~~~~~~~~~~

2When checking right hand side of answer_to_connection with expected type

5When checking right hand side of answer_to_connection with expected type

3 IO Int

6 IO Int

4

7

@@ -13,6 +16,3 @@ When checking argument code to function Main.send_page:

13 Bits32

16 Bits32

14 and

17 and

15 Int

18 Int

16− |

17−26 | send_page conn str code -- (prim__zextB32_Int code)

18− | ~~~~~~~~~~~~~~~~~~~~~~~

test/error008/expected+5−3

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

1−error008.idr:3:4:When checking type of Main.s2:

1+error008.idr:3:4:

2−Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil

3 |

2 |

43 | s2 : x + sum Nil = x * fromInteger 0

33 | s2 : x + sum Nil = x * fromInteger 0

5 | ^

4 | ^

6−error008a.idr:3:4:When checking type of Main.s1:

5+When checking type of Main.s2:

7Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil

6Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil

7+error008a.idr:3:4:

8 |

93 | s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0

10 | ^

11+When checking type of Main.s1:

12+Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil

test/ffi002/expected+2−1

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

1−test023.idr:20:26-36:Type provider error: Always fails

1+test023.idr:20:26-36:

2 |

320 | %provide (t : Type) with badProvider

4 | ~~~~~~~~~~~

5+Type provider error: Always fails

test/interfaces008/expected+1−1

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

1interfaces008.idr:20:18-23:

2−Default implementations must be for a super interface constraint on the containing interface.

3 |

2 |

420 | implementation Foo2 a where

320 | implementation Foo2 a where

5 | ~~~~~~

4 | ~~~~~~

5+Default implementations must be for a super interface constraint on the containing interface.

test/layout001/expected+5−4

@@ -58,14 +58,15 @@ Wrong indention: should be greater than context indentation

58 | ^

59Wrong indention: should be greater than context indentation

60

61+mplus1.idr:13:31-17:49:

62+ |

63+13 | term = do f <- factor

64+ | ~~~~~~~~~~~~~~~~~ ...

61−mplus1.idr:13:31-17:49:When checking right hand side of term with expected type

65+When checking right hand side of term with expected type

62 Maybe Int

66 Maybe Int

63

67

64When checking an application of function Prelude.Applicative.pure:

68When checking an application of function Prelude.Applicative.pure:

65 No such variable f

69 No such variable f

66− |

67−13 | term = do f <- factor

68− | ~~~~~~~~~~~~~~~~~ ...

69./mplus2.idr:17:37:

70./mplus2.idr:17:37:

70 |

71 |

7117 | `mplus` pure f

7217 | `mplus` pure f

test/literate001/expected+2−1

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

1−./test003a.lidr:1:0:Program line next to comment

1+./test003a.lidr:1:0:

2 |

31 | Broken

4 | ^

5+Program line next to comment

5'a'

6'a'

6'd'

7'd'

7zabcdefg

8zabcdefg

test/meta002/expected+8−8

@@ -1,22 +1,22 @@

1DataDef.idr:74:1-8:

2−While running an elaboration script, the following error occurred:

3−Prelude.Either.Either is already defined as a datatype.

4 |

2 |

574 | %runElab nope

374 | %runElab nope

6 | ~~~~~~~~

4 | ~~~~~~~~

5+While running an elaboration script, the following error occurred:

6+Prelude.Either.Either is already defined as a datatype.

7Tacs.idr:299:15-300:78:

8+ |

9+299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))

10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

8When checking right hand side of testElab3 with expected type

11When checking right hand side of testElab3 with expected type

9 DPair Ty (Tm [])

12 DPair Ty (Tm [])

10

13

11Unifying ty and ARR ty t would lead to infinite value

14Unifying ty and ARR ty t would lead to infinite value

12− |

13−299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))

14− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

15AgdaStyleReflection.idr:315:5-20:

16+ |

17+315 | baz = tactic trivial

18+ | ~~~~~~~~~~~~~~~~

16When checking right hand side of baz with expected type

19When checking right hand side of baz with expected type

17 (Nat, Void)

20 (Nat, Void)

18

21

19PROOF SEARCH FAILURE is not defined.

22PROOF SEARCH FAILURE is not defined.

20− |

21−315 | baz = tactic trivial

22− | ~~~~~~~~~~~~~~~~

test/meta003/expected+3−3

@@ -1,9 +1,9 @@

1BadDef.idr:14:1-8:

2+ |

3+14 | %runElab mkBadDef1

4+ | ~~~~~~~~

2While running an elaboration script, the following error occurred:

5While running an elaboration script, the following error occurred:

3Type mismatch between

6Type mismatch between

4 ()

7 ()

5and

8and

6 String

9 String

7− |

8−14 | %runElab mkBadDef1

9− | ~~~~~~~~

test/meta004/expected+2−2

@@ -1,6 +1,6 @@

1meta004.idr:50:1-8:

2−While running an elaboration script, the following error occurred:

3−Not an impossible case

4 |

2 |

550 | %runElab domore

350 | %runElab domore

6 | ~~~~~~~~

4 | ~~~~~~~~

5+While running an elaboration script, the following error occurred:

6+Not an impossible case

test/proof001/expected+2−2

@@ -1,10 +1,10 @@

1test029.idr:29:25-29:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

429 | simple.append_lemma_2 = proof {

329 | simple.append_lemma_2 = proof {

5 | ~~~~~

4 | ~~~~~

6−test029.idr:36:25-29:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+test029.idr:36:25-29:

8 |

7 |

936 | simple.append_lemma_1 = proof {

836 | simple.append_lemma_1 = proof {

10 | ~~~~~

9 | ~~~~~

10+This style of tactic proof is deprecated. See %runElab for the replacement.

test/proof002/expected+6−6

@@ -1,19 +1,22 @@

1Reflect.idr:175:21-25:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

4175 | Reflect.appRExpr1 = proof {

3175 | Reflect.appRExpr1 = proof {

5 | ~~~~~

4 | ~~~~~

6−Reflect.idr:184:21-25:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+Reflect.idr:184:21-25:

8 |

7 |

9184 | Reflect.appRExpr2 = proof {

8184 | Reflect.appRExpr2 = proof {

10 | ~~~~~

9 | ~~~~~

11−Reflect.idr:192:15-19:

12This style of tactic proof is deprecated. See %runElab for the replacement.

10This style of tactic proof is deprecated. See %runElab for the replacement.

11+Reflect.idr:192:15-19:

13 |

12 |

14192 | Reflect.bp1 = proof {

13192 | Reflect.bp1 = proof {

15 | ~~~~~

14 | ~~~~~

15+This style of tactic proof is deprecated. See %runElab for the replacement.

16test030a.idr:12:26-37:

17+ |

18+12 | testReflect1 {a} xs ys = AssocProof a

19+ | ~~~~~~~~~~~~

17When checking right hand side of testReflect1 with expected type

20When checking right hand side of testReflect1 with expected type

18 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs

21 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs

19

22

@@ -28,6 +31,3 @@ When checking an application of function Reflect.getJust:

28 Just x

31 Just x

29 and

32 and

30 Nothing

33 Nothing

31− |

32−12 | testReflect1 {a} xs ys = AssocProof a

33− | ~~~~~~~~~~~~

test/proof003/expected+6−6

@@ -1,33 +1,33 @@

1Parity.idr:17:18-22:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

417 | parity_lemma_2 = proof {

317 | parity_lemma_2 = proof {

5 | ~~~~~

4 | ~~~~~

6−Parity.idr:24:18-22:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+Parity.idr:24:18-22:

8 |

7 |

924 | parity_lemma_1 = proof {

824 | parity_lemma_1 = proof {

10 | ~~~~~

9 | ~~~~~

11−test015.idr:88:15-19:

12This style of tactic proof is deprecated. See %runElab for the replacement.

10This style of tactic proof is deprecated. See %runElab for the replacement.

11+test015.idr:88:15-19:

13 |

12 |

1488 | Main.ntbOdd = proof {

1388 | Main.ntbOdd = proof {

15 | ~~~~~

14 | ~~~~~

16−test015.idr:97:16-20:

17This style of tactic proof is deprecated. See %runElab for the replacement.

15This style of tactic proof is deprecated. See %runElab for the replacement.

16+test015.idr:97:16-20:

18 |

17 |

1997 | Main.ntbEven = proof {

1897 | Main.ntbEven = proof {

20 | ~~~~~

19 | ~~~~~

21−test015.idr:107:20-24:

22This style of tactic proof is deprecated. See %runElab for the replacement.

20This style of tactic proof is deprecated. See %runElab for the replacement.

21+test015.idr:107:20-24:

23 |

22 |

24107 | Main.adc_lemma_2 = proof {

23107 | Main.adc_lemma_2 = proof {

25 | ~~~~~

24 | ~~~~~

26−test015.idr:142:20-24:

27This style of tactic proof is deprecated. See %runElab for the replacement.

25This style of tactic proof is deprecated. See %runElab for the replacement.

26+test015.idr:142:20-24:

28 |

27 |

29142 | Main.adc_lemma_1 = proof {

28142 | Main.adc_lemma_1 = proof {

30 | ~~~~~

29 | ~~~~~

30+This style of tactic proof is deprecated. See %runElab for the replacement.

3100101010

3201011001

33010000011

test/proof007/expected+3−3

@@ -1,9 +1,9 @@

1DefaultArgUnknownName.idr:9:6-23:

2+ |

3+9 | test = funWithBadDefArg

4+ | ~~~~~~~~~~~~~~~~~~

2When checking right hand side of test with expected type

5When checking right hand side of test with expected type

3 ()

6 ()

4

7

5When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

8When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

6 No such variable sadgjhsag

9 No such variable sadgjhsag

7− |

8−9 | test = funWithBadDefArg

9− | ~~~~~~~~~~~~~~~~~~

test/proof008/expected+1−1

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

1ClaimAndUnfocus.idr:8:27-31:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

48 | ClaimAndUnfocus.foo_rhs = proof

38 | ClaimAndUnfocus.foo_rhs = proof

5 | ~~~~~

4 | ~~~~~

5+This style of tactic proof is deprecated. See %runElab for the replacement.

test/proof011/expected+6−6

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

1proof011.idr:20:5-21:18:

2+ |

3+20 | = rewrite vassoc xs ys xs using vreplace in

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

2When checking right hand side of vassoc' with expected type

5When checking right hand side of vassoc' with expected type

3 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

6 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

4

7

@@ -8,10 +11,10 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

8 x ::

11 x ::

9 (xs ++ ys) ++

12 (xs ++ ys) ++

10 zs

13 zs

11− |

12−20 | = rewrite vassoc xs ys xs using vreplace in

13− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

14proof011a.idr:14:5-37:

15+ |

16+14 | = rewrite vassoc xs ys xs in Refl

17+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

15When checking right hand side of vassoc' with expected type

18When checking right hand side of vassoc' with expected type

16 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

19 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

17

20

@@ -21,6 +24,3 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

21 x ::

24 x ::

22 (xs ++ ys) ++

25 (xs ++ ys) ++

23 zs

26 zs

24− |

25−14 | = rewrite vassoc xs ys xs in Refl

26− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

test/quasiquote003/expected+5−4

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

1−NoInfer.idr:11:5-11:When checking right hand side of zzz with expected type

1+NoInfer.idr:11:5-11:

2− TT

3−

4−No such variable k

5 |

2 |

611 | zzz = `(FZ)

311 | zzz = `(FZ)

7 | ~~~~~~~

4 | ~~~~~~~

5+When checking right hand side of zzz with expected type

6+ TT

7+

8+No such variable k

test/quasiquote004/expected+6−6

@@ -1,23 +1,23 @@

1Quasiquote004.idr:39:26-30:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

439 | Quasiquote004.getMeNat = proof

339 | Quasiquote004.getMeNat = proof

5 | ~~~~~

4 | ~~~~~

6−Quasiquote004.idr:42:28-32:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+Quasiquote004.idr:42:28-32:

8 |

7 |

942 | Quasiquote004.fizzyIsAOK = proof

842 | Quasiquote004.fizzyIsAOK = proof

10 | ~~~~~

9 | ~~~~~

11−Quasiquote004.idr:50:27-31:

12This style of tactic proof is deprecated. See %runElab for the replacement.

10This style of tactic proof is deprecated. See %runElab for the replacement.

11+Quasiquote004.idr:50:27-31:

13 |

12 |

1450 | Quasiquote004.getMeNat' = proof

1350 | Quasiquote004.getMeNat' = proof

15 | ~~~~~

14 | ~~~~~

15+This style of tactic proof is deprecated. See %runElab for the replacement.

16Quasiquote004.idr:50:25-51:18:

17+ |

18+50 | Quasiquote004.getMeNat' = proof

19+ | ~~~~~~~ ...

17When checking right hand side of Quasiquote004.getMeNat' with expected type

20When checking right hand side of Quasiquote004.getMeNat' with expected type

18 String

21 String

19

22

20Not a Nat goal

23Not a Nat goal

21− |

22−50 | Quasiquote004.getMeNat' = proof

23− | ~~~~~~~ ...

test/quasiquote006/expected+10−10

@@ -1,28 +1,28 @@

1quasiquote006.idr:9:3-10:

2+ |

3+9 | b = `{Nil}

4+ | ~~~~~~~~

2When checking right hand side of b with expected type

5When checking right hand side of b with expected type

3 TTName

6 TTName

4

7

5Can't disambiguate name: ForeignEnv.Nil,

8Can't disambiguate name: ForeignEnv.Nil,

6 Prelude.List.Nil

9 Prelude.List.Nil

7− |

8−9 | b = `{Nil}

9− | ~~~~~~~~

10quasiquote006.idr:12:3-17:

11+ |

12+12 | c = `{alsdkjflkj}

13+ | ~~~~~~~~~~~~~~~

11When checking right hand side of c with expected type

14When checking right hand side of c with expected type

12 TTName

15 TTName

13

16

14No such variable alsdkjflkj

17No such variable alsdkjflkj

15− |

16−12 | c = `{alsdkjflkj}

17− | ~~~~~~~~~~~~~~~

18quasiquote006.idr:15:3-11:

19+ |

20+15 | d = `{(::)}

21+ | ~~~~~~~~~

19When checking right hand side of d with expected type

22When checking right hand side of d with expected type

20 TTName

23 TTName

21

24

22Can't disambiguate name: ForeignEnv.::,

25Can't disambiguate name: ForeignEnv.::,

23 Prelude.List.::,

26 Prelude.List.::,

24 Prelude.Stream.::

27 Prelude.Stream.::

25− |

26−15 | d = `{(::)}

27− | ~~~~~~~~~

28−quasiquote006.idr:17:3:Main.d already defined

28+ quasiquote006.idr:17:3:Main.d already defined

test/reg017/expected+2−2

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

1reg017.idr:5:17-23:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

45 | { default tactics { refine Refl; solve; } prfA : a = a } ->

35 | { default tactics { refine Refl; solve; } prfA : a = a } ->

5 | ~~~~~~~

4 | ~~~~~~~

6−reg017.idr:8:17-23:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+reg017.idr:8:17-23:

8 |

7 |

98 | { default tactics { refine Refl; solve; } prfBC : b = c } ->

88 | { default tactics { refine Refl; solve; } prfBC : b = c } ->

10 | ~~~~~~~

9 | ~~~~~~~

10+This style of tactic proof is deprecated. See %runElab for the replacement.

114

test/reg027/expected+2−1

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

1<<int fn>>

2−reg027a.idr:9:16-30:Overlapping implementation: Show (Int -> a) already defined

2+reg027a.idr:9:16-30:

3 |

49 | implementation Show (Int -> b) where

5 | ~~~~~~~~~~~~~~~

6+Overlapping implementation: Show (Int -> a) already defined

test/regression002/expected+108−78

@@ -1,28 +1,36 @@

1−reg003a.idr:4:13-38:When checking type of Main.ECons:

1+reg003a.idr:4:13-38:

2−No such variable OddList

3 |

2 |

44 | ECons : Nat -> OddList -> EvenList

34 | ECons : Nat -> OddList -> EvenList

5 | ~~~~~~~~~~~~~~~~~~~~~~~~~~

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~

6−reg003a.idr:7:13-38:When checking type of Main.OCons:

5+When checking type of Main.ECons:

7−No such variable EvenList

6+No such variable OddList

7+reg003a.idr:7:13-38:

8 |

97 | OCons : Nat -> EvenList -> OddList

10 | ~~~~~~~~~~~~~~~~~~~~~~~~~~

11−reg003a.idr:9:6:When checking type of Main.test:

11+When checking type of Main.OCons:

12No such variable EvenList

13+reg003a.idr:9:6:

13 |

14 |

149 | test : EvenList

159 | test : EvenList

15 | ^

16 | ^

17+When checking type of Main.test:

18+No such variable EvenList

16reg006.idr:17:1-23:

19reg006.idr:17:1-23:

17−RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

18 |

20 |

1917 | lookup k Leaf = Nothing

2117 | lookup k Leaf = Nothing

20 | ~~~~~~~~~~~~~~~~~~~~~~~

22 | ~~~~~~~~~~~~~~~~~~~~~~~

23+RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

21−reg007.lidr:8:3-13:A.n is already defined

24+reg007.lidr:8:3-13:

22 |

25 |

238 | > A.n = Z -- This is where it's at!

268 | > A.n = Z -- This is where it's at!

24 | ~~~~~~~~~~~

27 | ~~~~~~~~~~~

28+A.n is already defined

29+reg007.lidr:12:13-18:

30+ |

31+12 | > hurrah = isSame

32+ | ~~~~~~

25−reg007.lidr:12:13-18:When checking right hand side of hurrah with expected type

33+When checking right hand side of hurrah with expected type

26 0 = 1

34 0 = 1

27

35

28Type mismatch between

36Type mismatch between

@@ -35,88 +43,95 @@ Specifically:

35 1

43 1

36 and

44 and

37 0

45 0

38− |

39−12 | > hurrah = isSame

40− | ~~~~~~

41reg010.idr:5:3-26:

46reg010.idr:5:3-26:

42−When checking left hand side of with block in usubst.unsafeSubst:

43−Can't match on with block in usubst.unsafeSubst warg a P x x px

44 |

47 |

455 | unsafeSubst P x x px | _ = px

485 | unsafeSubst P x x px | _ = px

46 | ~~~~~~~~~~~~~~~~~~~~~~~~

49 | ~~~~~~~~~~~~~~~~~~~~~~~~

50+When checking left hand side of with block in usubst.unsafeSubst:

51+Can't match on with block in usubst.unsafeSubst warg a P x x px

47reg018a.idr:16:1-18:

52reg018a.idr:16:1-18:

48−conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat

49 |

53 |

5016 | minusCoNat Z n = Z

5416 | minusCoNat Z n = Z

51 | ~~~~~~~~~~~~~~~~~~

55 | ~~~~~~~~~~~~~~~~~~

56+conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat

52reg018a.idr:21:1-42:

57reg018a.idr:21:1-42:

53−conat.loopForever is possibly not total due to: conat.minusCoNat

54 |

58 |

5521 | loopForever = minusCoNat infinity infinity

5921 | loopForever = minusCoNat infinity infinity

56 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

60 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

61+conat.loopForever is possibly not total due to: conat.minusCoNat

57reg018b.idr:8:1-28:

62reg018b.idr:8:1-28:

58−A.showB is possibly not total due to recursive path A.showB --> A.showB

59 |

63 |

608 | showB (I x) = "I" ++ showB x

648 | showB (I x) = "I" ++ showB x

61 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

65 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

66+A.showB is possibly not total due to recursive path A.showB --> A.showB

62reg018b.idr:11:1-6:

67reg018b.idr:11:1-6:

63−A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB

64 |

68 |

6511 | Show B where show = showB

6911 | Show B where show = showB

66 | ~~~~~~

70 | ~~~~~~

71+A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB

67reg018c.idr:21:1-22:21:

72reg018c.idr:21:1-22:21:

68−CodataTest.inf is possibly not total due to: with block in CodataTest.inf

69 |

73 |

7021 | inf (x :: xs) with (hdtl xs)

7421 | inf (x :: xs) with (hdtl xs)

71 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

75 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

76+CodataTest.inf is possibly not total due to: with block in CodataTest.inf

72−reg018d.idr:8:1-39:Main.pull is not total as there are missing cases

77+reg018d.idr:8:1-39:

73 |

78 |

748 | pull {n=Z} _ (x :: xs) = (x, xs)

798 | pull {n=Z} _ (x :: xs) = (x, xs)

75 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

80 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

81+Main.pull is not total as there are missing cases

82+reg023.idr:7:5-7:

83+ |

84+7 | bad = Z

85+ | ~~~

76−reg023.idr:7:5-7:When checking right hand side of bad with expected type

86+When checking right hand side of bad with expected type

77 f Nat

87 f Nat

78

88

79Type mismatch between

89Type mismatch between

80 Nat (Type of 0)

90 Nat (Type of 0)

81and

91and

82 f Nat (Expected type)

92 f Nat (Expected type)

83− |

93+reg028.idr:5:1-9:

84−7 | bad = Z

85− | ~~~

86−reg028.idr:5:1-9:tbad.bad is possibly not total due to: with block in tbad.bad

87 |

94 |

885 | bad Z = Z

955 | bad Z = Z

89 | ~~~~~~~~~

96 | ~~~~~~~~~

97+tbad.bad is possibly not total due to: with block in tbad.bad

90reg028a.idr:17:14-18:

98reg028a.idr:17:14-18:

91−This style of tactic proof is deprecated. See %runElab for the replacement.

92 |

99 |

9317 | qsortLemma = proof

10017 | qsortLemma = proof

94 | ~~~~~

101 | ~~~~~

102+This style of tactic proof is deprecated. See %runElab for the replacement.

95reg028a.idr:11:1-14:

103reg028a.idr:11:1-14:

96−tbad.qsort' is possibly not total due to: with block in tbad.qsort'

97 |

104 |

9811 | qsort' [] = []

10511 | qsort' [] = []

99 | ~~~~~~~~~~~~~~

106 | ~~~~~~~~~~~~~~

107+tbad.qsort' is possibly not total due to: with block in tbad.qsort'

100−reg034.idr:6:1-14:When checking left hand side of bar:

108+reg034.idr:6:1-14:

101−Can't match on bar xs xs Refl

102 |

109 |

1036 | bar xs xs Refl = Refl

1106 | bar xs xs Refl = Refl

104 | ~~~~~~~~~~~~~~

111 | ~~~~~~~~~~~~~~

105−reg034.idr:9:1-14:When checking left hand side of foo:

112+When checking left hand side of bar:

106−Can't match on foo f x x Refl

113+Can't match on bar xs xs Refl

114+reg034.idr:9:1-14:

107 |

115 |

1089 | foo f x x Refl = Refl

1169 | foo f x x Refl = Refl

109 | ~~~~~~~~~~~~~~

117 | ~~~~~~~~~~~~~~

118+When checking left hand side of foo:

119+Can't match on foo f x x Refl

110−reg035b.idr:8:12-38:No such variable __pi_arg

120+reg035b.idr:8:12-38:

111 |

121 |

1128 | fins Z = ([] ** (finZEmpty {a=_}))

1228 | fins Z = ([] ** (finZEmpty {a=_}))

113 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~

123 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~

124+No such variable __pi_arg

114reg044.idr:4:6-10:

125reg044.idr:4:6-10:

115−This style of tactic proof is deprecated. See %runElab for the replacement.

116 |

126 |

1174 | pf = proof

1274 | pf = proof

118 | ~~~~~

128 | ~~~~~

129+This style of tactic proof is deprecated. See %runElab for the replacement.

130+reg044.idr:4:4-6:13:

131+ |

132+4 | pf = proof

133+ | ~~~~~~~ ...

119−reg044.idr:4:4-6:13:When checking right hand side of Main.pf with expected type

134+When checking right hand side of Main.pf with expected type

120 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

135 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

121

136

122Type mismatch between

137Type mismatch between

@@ -129,21 +144,20 @@ Specifically:

129 b

144 b

130 and

145 and

131 a

146 a

132− |

133−4 | pf = proof

134− | ~~~~~~~ ...

135−reg049.idr:2:11-14:When checking constructor Main.Bogus:

147+reg049.idr:2:11-14:

136−Void is not Main.Foo

137 |

148 |

1382 | Bogus : Void

1492 | Bogus : Void

139 | ~~~~

150 | ~~~~

140−reg049.idr:5:6-12:When checking right hand side of uhOh with expected type

151+When checking constructor Main.Bogus:

141− Void

152+Void is not Main.Foo

142−

153+reg049.idr:5:6-12:

143−No such variable Bogus

144 |

154 |

1455 | uhOh = Bogus

1555 | uhOh = Bogus

146 | ~~~~~~~

156 | ~~~~~~~

157+When checking right hand side of uhOh with expected type

158+ Void

159+

160+No such variable Bogus

147./badbangop.idr:7:1:

161./badbangop.idr:7:1:

148 |

162 |

1497 | (!) : List a -> Nat -> Maybe a

1637 | (!) : List a -> Nat -> Maybe a

@@ -156,90 +170,104 @@ No such variable Bogus

156 | ^

170 | ^

157unexpected Operator without known fixity: !!

171unexpected Operator without known fixity: !!

158

172

159−reg054.idr:18:1-17:When checking left hand side of inf:

173+reg054.idr:18:1-17:

160−When checking an application of constructor Main.MkInfer:

161− Attempting concrete match on polymorphic argument: 0

162 |

174 |

16318 | inf (MkInfer _ Z) = True

17518 | inf (MkInfer _ Z) = True

164 | ~~~~~~~~~~~~~~~~~

176 | ~~~~~~~~~~~~~~~~~

177+When checking left hand side of inf:

178+When checking an application of constructor Main.MkInfer:

179+ Attempting concrete match on polymorphic argument: 0

165−reg054.idr:34:1-18:When checking left hand side of weird:

180+reg054.idr:34:1-18:

166−No explicit types on left hand side: Char

167 |

181 |

16834 | weird {x = Char} y = '5'

18234 | weird {x = Char} y = '5'

169 | ~~~~~~~~~~~~~~~~~~

183 | ~~~~~~~~~~~~~~~~~~

170−reg054.idr:37:1-30:When checking left hand side of weird':

184+When checking left hand side of weird:

171−No explicit types on left hand side: Nat

185+No explicit types on left hand side: Char

186+reg054.idr:37:1-30:

172 |

187 |

17337 | weird' {x = Prelude.Nat.Nat} y = Z

18837 | weird' {x = Prelude.Nat.Nat} y = Z

174 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

189 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

190+When checking left hand side of weird':

191+No explicit types on left hand side: Nat

192+reg054.idr:40:1-7:

193+ |

194+40 | tctrick (Just x) = x

195+ | ~~~~~~~

175−reg054.idr:40:1-7:When checking left hand side of tctrick:

196+When checking left hand side of tctrick:

176When checking an application of Main.tctrick:

197When checking an application of Main.tctrick:

177 Type mismatch between

198 Type mismatch between

178 Maybe a1 (Type of Just x)

199 Maybe a1 (Type of Just x)

179 and

200 and

180 a (Expected type)

201 a (Expected type)

181− |

182−40 | tctrick (Just x) = x

183− | ~~~~~~~

184−reg055.idr:5:1-7:When checking left hand side of g:

202+reg055.idr:5:1-7:

185−Can't match on g (f 0)

186 |

203 |

1875 | g (f Z) = 1

2045 | g (f Z) = 1

188 | ~~~~~~~

205 | ~~~~~~~

189−reg055.idr:8:1-5:When checking left hand side of h:

206+When checking left hand side of g:

190−Can't match on h x x

207+Can't match on g (f 0)

208+reg055.idr:8:1-5:

191 |

209 |

1928 | h x x = x

2108 | h x x = x

193 | ~~~~~

211 | ~~~~~

212+When checking left hand side of h:

213+Can't match on h x x

194−reg055a.idr:8:1-18:When checking left hand side of foo:

214+reg055a.idr:8:1-18:

195−When checking an application of constructor Foo.CAny:

196− Attempting concrete match on polymorphic argument: Nothing

197 |

215 |

1988 | foo (CAny Nothing) = 42

2168 | foo (CAny Nothing) = 42

199 | ~~~~~~~~~~~~~~~~~~

217 | ~~~~~~~~~~~~~~~~~~

200−reg055a.idr:13:1-23:When checking left hand side of Foo.apply:

218+When checking left hand side of foo:

201−Can't match on apply (\x, y => x) a

219+When checking an application of constructor Foo.CAny:

220+ Attempting concrete match on polymorphic argument: Nothing

221+reg055a.idr:13:1-23:

202 |

222 |

20313 | apply (\x => \y => x) a = a

22313 | apply (\x => \y => x) a = a

204 | ~~~~~~~~~~~~~~~~~~~~~~~

224 | ~~~~~~~~~~~~~~~~~~~~~~~

225+When checking left hand side of Foo.apply:

226+Can't match on apply (\x, y => x) a

205−reg056.idr:7:16-25:dodgy n m Refl is a valid case

227+reg056.idr:7:16-25:

206 |

228 |

2077 | dodgy n m Refl impossible

2297 | dodgy n m Refl impossible

208 | ~~~~~~~~~~

230 | ~~~~~~~~~~

231+dodgy n m Refl is a valid case

209−reg056.idr:10:11-20:nonk Refl is a valid case

232+reg056.idr:10:11-20:

210 |

233 |

21110 | nonk Refl impossible

23410 | nonk Refl impossible

212 | ~~~~~~~~~~

235 | ~~~~~~~~~~

213−reg068.idr:1:6-8:Main.nat has a name which may be implicitly bound.

236+nonk Refl is a valid case

214−This is likely to lead to problems!

237+reg068.idr:1:6-8:

215 |

238 |

2161 | data nat : Type where --error

2391 | data nat : Type where --error

217 | ~~~

240 | ~~~

218−reg068.idr:2:8-10:Main.ze has a name which may be implicitly bound.

241+Main.nat has a name which may be implicitly bound.

219This is likely to lead to problems!

242This is likely to lead to problems!

243+reg068.idr:2:8-10:

220 |

244 |

2212 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

2452 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

222 | ~~~

246 | ~~~

247+Main.ze has a name which may be implicitly bound.

248+This is likely to lead to problems!

223reg068.idr:2:8-10:

249reg068.idr:2:8-10:

224−nat is bound as an implicit

225− Did you mean to refer to Main.nat?

226 |

250 |

2272 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

2512 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

228 | ~~~

252 | ~~~

253+nat is bound as an implicit

254+ Did you mean to refer to Main.nat?

229−reg068.idr:2:8-10:When checking constructor Main.ze:

255+reg068.idr:2:8-10:

230−Type level variable nat is not Main.nat

231 |

256 |

2322 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

2572 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

233 | ~~~

258 | ~~~

234−Mod.idr:11:1-22:public export Mod.natexp can't refer to export Mod.natfn

259+When checking constructor Main.ze:

260+Type level variable nat is not Main.nat

261+Mod.idr:11:1-22:

235 |

262 |

23611 | natexp k = S (natfn k)

26311 | natexp k = S (natfn k)

237 | ~~~~~~~~~~~~~~~~~~~~~~

264 | ~~~~~~~~~~~~~~~~~~~~~~

265+public export Mod.natexp can't refer to export Mod.natfn

238reg070.idr:7:1-7:

266reg070.idr:7:1-7:

239−Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

240 |

267 |

2417 | Show Te where

2687 | Show Te where

242 | ~~~~~~~

269 | ~~~~~~~

270+Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

243./reg076.idr:8:1:

271./reg076.idr:8:1:

244 |

272 |

2458 | <empty line>

2738 | <empty line>

@@ -253,6 +281,9 @@ Missing fixity declaration for Main.:>

253Missing fixity declaration for Main.:>>

281Missing fixity declaration for Main.:>>

254

282

255DoubleEquality.idr:4:83-103:

283DoubleEquality.idr:4:83-103:

284+ |

285+4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl

286+ | ~~~~~~~~~~~~~~~~~~~~~

256When checking right hand side of oops with expected type

287When checking right hand side of oops with expected type

257 Void

288 Void

258

289

@@ -267,14 +298,13 @@ When checking argument value to function Prelude.Basics.the:

267 -0.0

298 -0.0

268 and

299 and

269 0.0

300 0.0

270− |

271−4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl

272− | ~~~~~~~~~~~~~~~~~~~~~

273−Canonicity.idr:9:1-9:Canonicity.f is not total as there are missing cases

301+Canonicity.idr:9:1-9:

274 |

302 |

2759 | f Nil = 0

3039 | f Nil = 0

276 | ~~~~~~~~~

304 | ~~~~~~~~~

277−Canonicity.idr:12:1-20:Canonicity.NaN is possibly not total due to: Canonicity.f

305+Canonicity.f is not total as there are missing cases

306+Canonicity.idr:12:1-20:

278 |

307 |

27912 | NaN = f (Cons 0 Nil)

30812 | NaN = f (Cons 0 Nil)

280 | ~~~~~~~~~~~~~~~~~~~~

309 | ~~~~~~~~~~~~~~~~~~~~

310+Canonicity.NaN is possibly not total due to: Canonicity.f

test/sourceLocation001/expected+4−4

@@ -1,23 +1,23 @@

1SourceLoc.idr:12:19-25:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

412 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

312 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

5 | ~~~~~~~

4 | ~~~~~~~

6−SourceLoc.idr:21:19-23:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+SourceLoc.idr:21:19-23:

8 |

7 |

921 | fromProofScript = proof sourceLocation

821 | fromProofScript = proof sourceLocation

10 | ~~~~~

9 | ~~~~~

11−SourceLoc.idr:41:20-26:

12This style of tactic proof is deprecated. See %runElab for the replacement.

10This style of tactic proof is deprecated. See %runElab for the replacement.

11+SourceLoc.idr:41:20-26:

13 |

12 |

1441 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

1341 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

15 | ~~~~~~~

14 | ~~~~~~~

16−SourceLoc.idr:99:18-22:

17This style of tactic proof is deprecated. See %runElab for the replacement.

15This style of tactic proof is deprecated. See %runElab for the replacement.

16+SourceLoc.idr:99:18-22:

18 |

17 |

1999 | SourceLoc.meta = proof

1899 | SourceLoc.meta = proof

20 | ~~~~~

19 | ~~~~~

20+This style of tactic proof is deprecated. See %runElab for the replacement.

21Testing using definition

22FileLoc "SourceLoc.idr" (17, 11) (17, 16)

23Testing using inline tactics

test/syntax001/expected+8−6

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

1+Syntax.idr:6:7-18:

2+ |

3+6 | foo = fnord "argh"

4+ | ~~~~~~~~~~~~

1−Syntax.idr:6:7-18:When checking right hand side of foo with expected type

5+When checking right hand side of foo with expected type

2 Nat

6 Nat

3

7

4When checking an application of function Prelude.Interfaces.+:

8When checking an application of function Prelude.Interfaces.+:

@@ -6,10 +10,11 @@ When checking an application of function Prelude.Interfaces.+:

6 String (Type of "argh")

10 String (Type of "argh")

7 and

11 and

8 Nat (Expected type)

12 Nat (Expected type)

13+SyntaxTest.idr:5:7-18:

9 |

14 |

10−6 | foo = fnord "argh"

15+5 | foo = fnord "argh"

11 | ~~~~~~~~~~~~

16 | ~~~~~~~~~~~~

12−SyntaxTest.idr:5:7-18:When checking right hand side of foo with expected type

17+When checking right hand side of foo with expected type

13 Nat

18 Nat

14

19

15When checking an application of function Prelude.Interfaces.+:

20When checking an application of function Prelude.Interfaces.+:

@@ -17,6 +22,3 @@ When checking an application of function Prelude.Interfaces.+:

17 String (Type of "argh")

22 String (Type of "argh")

18 and

23 and

19 Nat (Expected type)

24 Nat (Expected type)

20− |

21−5 | foo = fnord "argh"

22− | ~~~~~~~~~~~~

test/totality001/expected+6−3

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

1−test010.idr:15:1-30:Main.foo is possibly not total due to: Main.MkBad

1+test010.idr:15:1-30:

2 |

315 | foo (MkBad f i) = f (MkBad' i)

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5−test010a.idr:9:1-23:main.bar is possibly not total due to: main.MkBad

5+Main.foo is possibly not total due to: Main.MkBad

6+test010a.idr:9:1-23:

6 |

7 |

79 | bar = MkBad (\x => 3) 3

89 | bar = MkBad (\x => 3) 3

8 | ~~~~~~~~~~~~~~~~~~~~~~~

9 | ~~~~~~~~~~~~~~~~~~~~~~~

9−test010b.idr:9:1-23:main.bar is possibly not total due to: main.MkBad

10+main.bar is possibly not total due to: main.MkBad

11+test010b.idr:9:1-23:

10 |

12 |

119 | bar = MkBad (\x => 3) 3

139 | bar = MkBad (\x => 3) 3

12 | ~~~~~~~~~~~~~~~~~~~~~~~

14 | ~~~~~~~~~~~~~~~~~~~~~~~

15+main.bar is possibly not total due to: main.MkBad

test/totality002/expected+4−3

@@ -1,14 +1,15 @@

1test017.idr:94:26-30:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

494 | maxCommutativeStepCase = proof {

394 | maxCommutativeStepCase = proof {

5 | ~~~~~

4 | ~~~~~

5+This style of tactic proof is deprecated. See %runElab for the replacement.

6test017a.idr:7:1-24:

7−scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

8 |

7 |

97 | vtrans [] _ = []

87 | vtrans [] _ = []

10 | ~~~~~~~~~~~~~~~~~~~~~~~~

9 | ~~~~~~~~~~~~~~~~~~~~~~~~

11−test017b.idr:4:1-9:foo.foo is possibly not total due to recursive path foo.foo

10+scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

11+test017b.idr:4:1-9:

12 |

134 | foo = foo

14 | ~~~~~~~~~

15+foo.foo is possibly not total due to recursive path foo.foo

test/totality003/expected+1−1

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

1totality003a.idr:5:1-13:

2−smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort

3 |

2 |

45 | qsort [] = []

35 | qsort [] = []

5 | ~~~~~~~~~~~~~

4 | ~~~~~~~~~~~~~

5+smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort

test/totality004/expected+3−2

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

1[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

2totality004a.idr:13:1-44:

3−Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

4 |

3 |

513 | process (Get f) (x :: xs) = process (f x) xs

413 | process (Get f) (x :: xs) = process (f x) xs

6 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

7−totality004a.idr:24:1-60:Main.main is possibly not total due to: Main.process

6+Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

7+totality004a.idr:24:1-60:

8 |

924 | main = printLn (take 10 (process doubleInt (countStream 1)))

10 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

11+Main.main is possibly not total due to: Main.process

test/totality006/expected+5−3

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

1−totality006.idr:8:1-29:Main.prf is not total as there are missing cases

1+totality006.idr:8:1-29:

2 |

38 | prf Z Z Oh impossible

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.prf is not total as there are missing cases

5−totality006a.idr:11:21-30:prf' (S _) (S _) Oh is a valid case

6+totality006a.idr:11:21-30:

6 |

7 |

711 | prf' (S _) (S _) Oh impossible

811 | prf' (S _) (S _) Oh impossible

8 | ~~~~~~~~~~

9 | ~~~~~~~~~~

10+prf' (S _) (S _) Oh is a valid case

9totality006b.idr:10:1-34:

11totality006b.idr:10:1-34:

10−totality006b.blargh is not total as there are missing cases

11 |

12 |

1210 | blargh [] (y :: xs) so = absurd so

1310 | blargh [] (y :: xs) so = absurd so

13 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

14 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

15+totality006b.blargh is not total as there are missing cases

test/totality007/expected+1−1

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

1Entering directory `./src'

2Totality.idr:4:1-9:

3−Totality.foo is not total as there are missing cases

4 |

3 |

54 | foo Z = Z

44 | foo Z = Z

6 | ~~~~~~~~~

5 | ~~~~~~~~~

6+Totality.foo is not total as there are missing cases

7Totality.idr:4:1-9:Could not build: Totality.foo is not total as there are missing cases

8Leaving directory `./src'

test/totality008/expected+2−1

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

1−totality008.idr:7:1-14:Main.ElimT is possibly not total due to: Main.C2

1+totality008.idr:7:1-14:

2 |

37 | ElimT _ C1 = 3

4 | ~~~~~~~~~~~~~~

5+Main.ElimT is possibly not total due to: Main.C2

test/totality009/expected+20−10

@@ -1,40 +1,50 @@

1−TestLambdaPossible.idr:9:25-34:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

1+TestLambdaPossible.idr:9:25-34:

2 |

39 | wrongPossible = (\Flase impossible)

4 | ~~~~~~~~~~

5−TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

5+Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

6+TestLambdaPossible.idr:9:1-35:

6 |

7 |

79 | wrongPossible = (\Flase impossible)

89 | wrongPossible = (\Flase impossible)

8 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

9 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

9−TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

10+Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

11+TestLambdaPossible.idr:12:25:

10 |

12 |

1112 | wrongPossible' x = case x of

1312 | wrongPossible' x = case x of

12 | ^

14 | ^

13−TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

15+Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

16+TestLambdaPossible.idr:12:1-13:40:

14 |

17 |

1512 | wrongPossible' x = case x of

1812 | wrongPossible' x = case x of

16 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

19 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

17−TestLambdaPossible.idr:9:15-35:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

20+Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

21+TestLambdaPossible.idr:9:15-35:

18 |

22 |

199 | wrongPossible = (\Flase impossible)

239 | wrongPossible = (\Flase impossible)

20 | ~~~~~~~~~~~~~~~~~~~~~

24 | ~~~~~~~~~~~~~~~~~~~~~

21−TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

25+Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

26+TestLambdaPossible.idr:9:1-35:

22 |

27 |

239 | wrongPossible = (\Flase impossible)

289 | wrongPossible = (\Flase impossible)

24 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

29 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

25−TestLambdaPossible.idr:12:18-13:40:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

30+Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

31+TestLambdaPossible.idr:12:18-13:40:

26 |

32 |

2712 | wrongPossible' x = case x of

3312 | wrongPossible' x = case x of

28 | ~~~~~~~~~~~ ...

34 | ~~~~~~~~~~~ ...

29−TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

35+Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

36+TestLambdaPossible.idr:12:1-13:40:

30 |

37 |

3112 | wrongPossible' x = case x of

3812 | wrongPossible' x = case x of

32 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

39 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

33−TestLambdaPossible2.idr:10:1-35:TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34

40+Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

41+TestLambdaPossible2.idr:10:1-35:

34 |

42 |

3510 | wrongPossible = (\Flase impossible)

4310 | wrongPossible = (\Flase impossible)

36 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

44 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

37−TestLambdaPossible2.idr:14:1-15:40:TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25

45+TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34

46+TestLambdaPossible2.idr:14:1-15:40:

38 |

47 |

3914 | wrongPossible' x = case x of

4814 | wrongPossible' x = case x of

40 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

49 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

50+TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25

test/totality010/expected+4−2

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

1−totality010.idr:27:1-35:Main.evenNotS is not total as there are missing cases

1+totality010.idr:27:1-35:

2 |

327 | evenNotS MkEven ZeroEven impossible

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.evenNotS is not total as there are missing cases

5−totality010.idr:30:1-40:Main.bad is possibly not total due to: Main.evenNotS

6+totality010.idr:30:1-40:

6 |

7 |

730 | bad = evenNotS ZeroEven $ MkBad ZeroEven

830 | bad = evenNotS ZeroEven $ MkBad ZeroEven

8 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

9 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

10+Main.bad is possibly not total due to: Main.evenNotS

test/totality011/expected+1−1

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

1totality011.lidr:22:3-57:

2−Main.weCanOnlyGetOlder is not total as there are missing cases

3 |

2 |

422 | > weCanOnlyGetOlder {t'' = Z} {t = Z} _ _ _ = LTEZero

322 | > weCanOnlyGetOlder {t'' = Z} {t = Z} _ _ _ = LTEZero

5 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.weCanOnlyGetOlder is not total as there are missing cases

test/totality012/expected+2−2

@@ -1,10 +1,10 @@

1totality012a.idr:9:1-10:27:

2−Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2

3 |

2 |

49 | echo2 x = if (x == "quit") then PutStr "Bye!\n"

39 | echo2 x = if (x == "quit") then PutStr "Bye!\n"

5 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

5+Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2

6totality012b.idr:11:1-17:33:

7−Main.echo is possibly not total due to recursive path Main.echo

8 |

7 |

911 | echo = do PutStr "$ "

811 | echo = do PutStr "$ "

10 | ~~~~~~~~~~~~~~~~~~~~~ ...

9 | ~~~~~~~~~~~~~~~~~~~~~ ...

10+Main.echo is possibly not total due to recursive path Main.echo

test/totality013/expected+3−2

@@ -1,9 +1,10 @@

1totality013a.idr:5:3-49:

2−Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot

3 |

2 |

45 | foo order x xs y ys _ = mtot order (x :: xs) ys

35 | foo order x xs y ys _ = mtot order (x :: xs) ys

5 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

6−totality013a.idr:9:3-36:Main.mtot is possibly not total due to: Main.foo

5+Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot

6+totality013a.idr:9:3-36:

7 |

89 | mtot order [] right = right

9 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

10+Main.mtot is possibly not total due to: Main.foo

test/totality014/expected+5−4

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

1+totality014.idr:1:6-9:

2+ |

3+1 | data Con2 : Type where

4+ | ~~~~

1−totality014.idr:1:6-9:Universe inconsistency.

5+Universe inconsistency.

2 Working on: ./totality014.idr.w

6 Working on: ./totality014.idr.w

3 Old domain: (5,5)

7 Old domain: (5,5)

4 New domain: (5,4)

8 New domain: (5,4)

@@ -6,6 +10,3 @@ totality014.idr:1:6-9:Universe inconsistency.

6 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}

10 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}

7 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}

11 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}

8 ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:27-29}

12 ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:27-29}

9− |

10−1 | data Con2 : Type where

11− | ~~~~

test/totality015/expected+5−3

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

1totality015a.idr:52:3-53:

2−Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz

3 |

2 |

452 | quiz (num1 :: num2 :: nums) score = quiz nums score

352 | quiz (num1 :: num2 :: nums) score = quiz nums score

5 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz

6−totality015a.idr:42:3-44:36:Main.correct is possibly not total due to: Main.quiz

6+totality015a.idr:42:3-44:36:

7 |

842 | correct nums score

9 | ~~~~~~~~~~~~~~~~~~ ...

10−totality015a.idr:47:3-49:28:Main.wrong is possibly not total due to: Main.quiz

10+Main.correct is possibly not total due to: Main.quiz

11+totality015a.idr:47:3-49:28:

11 |

12 |

1247 | wrong nums ans score

1347 | wrong nums ans score

13 | ~~~~~~~~~~~~~~~~~~~~ ...

14 | ~~~~~~~~~~~~~~~~~~~~ ...

15+Main.wrong is possibly not total due to: Main.quiz

test/totality016/expected+18−9

@@ -1,36 +1,45 @@

1−totality016.idr:15:1-21:Main.f1 is not total as there are missing cases

1+totality016.idr:15:1-21:

2 |

315 | f1 (MkTP T1 x) = True

4 | ~~~~~~~~~~~~~~~~~~~~~

5−totality016.idr:19:1-24:Main.f2 is not total as there are missing cases

5+Main.f1 is not total as there are missing cases

6+totality016.idr:19:1-24:

6 |

7 |

719 | f2 (MkTP T1 x, _) = True

819 | f2 (MkTP T1 x, _) = True

8 | ~~~~~~~~~~~~~~~~~~~~~~~~

9 | ~~~~~~~~~~~~~~~~~~~~~~~~

9−totality016.idr:23:1-29:Main.f3 is not total as there are missing cases

10+Main.f2 is not total as there are missing cases

11+totality016.idr:23:1-29:

10 |

12 |

1123 | f3 ((MkTP T1 x, _), _) = True

1323 | f3 ((MkTP T1 x, _), _) = True

12 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

14 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

13−totality016.idr:27:1-14:Main.g1 is not total as there are missing cases

15+Main.f3 is not total as there are missing cases

16+totality016.idr:27:1-14:

14 |

17 |

1527 | g1 T1 x = True

1827 | g1 T1 x = True

16 | ~~~~~~~~~~~~~~

19 | ~~~~~~~~~~~~~~

17−totality016.idr:31:1-17:Main.g2 is not total as there are missing cases

20+Main.g1 is not total as there are missing cases

21+totality016.idr:31:1-17:

18 |

22 |

1931 | g2 (T1, x) = True

2331 | g2 (T1, x) = True

20 | ~~~~~~~~~~~~~~~~~

24 | ~~~~~~~~~~~~~~~~~

21−totality016.idr:35:1-16:Main.h1 is not total as there are missing cases

25+Main.g2 is not total as there are missing cases

26+totality016.idr:35:1-16:

22 |

27 |

2335 | h1 True x = True

2835 | h1 True x = True

24 | ~~~~~~~~~~~~~~~~

29 | ~~~~~~~~~~~~~~~~

25−totality016.idr:39:1-19:Main.h2 is not total as there are missing cases

30+Main.h1 is not total as there are missing cases

31+totality016.idr:39:1-19:

26 |

32 |

2739 | h2 (True, x) = True

3339 | h2 (True, x) = True

28 | ~~~~~~~~~~~~~~~~~~~

34 | ~~~~~~~~~~~~~~~~~~~

29−totality016.idr:43:1-25:Main.h3 is not total as there are missing cases

35+Main.h2 is not total as there are missing cases

36+totality016.idr:43:1-25:

30 |

37 |

3143 | h3 (MkTP2 (T1, x)) = True

3843 | h3 (MkTP2 (T1, x)) = True

32 | ~~~~~~~~~~~~~~~~~~~~~~~~~

39 | ~~~~~~~~~~~~~~~~~~~~~~~~~

33−totality016.idr:47:1-30:Main.h4 is not total as there are missing cases

40+Main.h3 is not total as there are missing cases

41+totality016.idr:47:1-30:

34 |

42 |

3547 | h4 (MkTP2 (T1, x), _) _ = True

4347 | h4 (MkTP2 (T1, x), _) _ = True

36 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

44 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

45+Main.h4 is not total as there are missing cases

test/totality017/expected+12−6

@@ -1,24 +1,30 @@

1−totality017.idr:19:1-15:Main.g1 is not total as there are missing cases

1+totality017.idr:19:1-15:

2 |

319 | g1 T1 T1 = True

4 | ~~~~~~~~~~~~~~~

5−totality017.idr:25:1-17:Main.g2 is not total as there are missing cases

5+Main.g1 is not total as there are missing cases

6+totality017.idr:25:1-17:

6 |

7 |

725 | g2 T1' T1' = True

825 | g2 T1' T1' = True

8 | ~~~~~~~~~~~~~~~~~

9 | ~~~~~~~~~~~~~~~~~

9−totality017.idr:31:1-13:Main.g3 is not total as there are missing cases

10+Main.g2 is not total as there are missing cases

11+totality017.idr:31:1-13:

10 |

12 |

1131 | g3 T1' = True

1331 | g3 T1' = True

12 | ~~~~~~~~~~~~~

14 | ~~~~~~~~~~~~~

13−totality017.idr:37:1-36:Main.g4 is not total as there are missing cases

15+Main.g3 is not total as there are missing cases

16+totality017.idr:37:1-36:

14 |

17 |

1537 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True

1837 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True

16 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

19 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

17−totality017.idr:42:1-11:Main.f' is not total as there are missing cases

20+Main.g4 is not total as there are missing cases

21+totality017.idr:42:1-11:

18 |

22 |

1942 | f' 0 = True

2342 | f' 0 = True

20 | ~~~~~~~~~~~

24 | ~~~~~~~~~~~

21−totality017.idr:47:1-17:Main.f is not total as there are missing cases

25+Main.f' is not total as there are missing cases

26+totality017.idr:47:1-17:

22 |

27 |

2347 | f (MkPP 0) = True

2847 | f (MkPP 0) = True

24 | ~~~~~~~~~~~~~~~~~

29 | ~~~~~~~~~~~~~~~~~

30+Main.f is not total as there are missing cases

test/totality018/expected+2−1

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

1−totality018.idr:12:1-10:Main.bar is not total as there are missing cases

1+totality018.idr:12:1-10:

2 |

312 | bar FZ = 0

4 | ~~~~~~~~~~

5+Main.bar is not total as there are missing cases

test/totality019/expected+4−2

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

1−totality019.idr:8:1-36:Main.testCov is not total as there are missing cases

1+totality019.idr:8:1-36:

2 |

38 | testCov False False = ?testCov_rhs_3

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5−totality019.idr:12:1-42:Main.testCov' is not total as there are missing cases

5+Main.testCov is not total as there are missing cases

6+totality019.idr:12:1-42:

6 |

7 |

712 | testCov' (False ** False) = ?testCov_rhs_3

812 | testCov' (False ** False) = ?testCov_rhs_3

8 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

9 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

10+Main.testCov' is not total as there are missing cases

test/totality020/expected+4−2

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

1−totality020.idr:4:14-23:bug _ _ Refl is a valid case

1+totality020.idr:4:14-23:

2 |

34 | bug _ _ Refl impossible

4 | ~~~~~~~~~~

5+bug _ _ Refl is a valid case

5−totality020.idr:7:14-23:foo a b Refl is a valid case

6+totality020.idr:7:14-23:

6 |

7 |

77 | foo a b Refl impossible

87 | foo a b Refl impossible

8 | ~~~~~~~~~~

9 | ~~~~~~~~~~

10+foo a b Refl is a valid case

test/totality021/expected+5−5

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

1totality021.idr:8:1-67:

2−Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'

3 |

2 |

48 | sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl

38 | sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl

5 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'

6totality021.idr:12:1-66:

7−Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'

8 |

7 |

912 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl

812 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl

10 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

9 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

10+Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'

11totality021.idr:18:1-26:

12−Main.v is possibly not total due to: Main.sLevelNotSLevel

13 |

12 |

1418 | v = sLevelNotSLevel l Refl

1318 | v = sLevelNotSLevel l Refl

15 | ~~~~~~~~~~~~~~~~~~~~~~~~~~

14 | ~~~~~~~~~~~~~~~~~~~~~~~~~~

15+Main.v is possibly not total due to: Main.sLevelNotSLevel

16totality021a.idr:9:1-37:

17−Main.noNonEmptyPointInt is not total as there are missing cases

18 |

17 |

199 | noNonEmptyPointInt {n} Nil impossible

189 | noNonEmptyPointInt {n} Nil impossible

20 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

19 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

20+Main.noNonEmptyPointInt is not total as there are missing cases

21totality021a.idr:12:1-31:

22−Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt

23 |

22 |

2412 | myVoid = noNonEmptyPointInt [2]

2312 | myVoid = noNonEmptyPointInt [2]

25 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

24 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

25+Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt

test/totality022/expected+2−1

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

1−totality022.idr:7:20-29:f _ [] (RSnoc _ _) is a valid case

1+totality022.idr:7:20-29:

2 |

37 | f _ [] (RSnoc _ _) impossible -- = ?wat

4 | ~~~~~~~~~~

5+f _ [] (RSnoc _ _) is a valid case

test/totality023/expected+1−1

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

1totality023.idr:9:1-10:27:

2−Main.run is possibly not total due to recursive path Main.run --> Main.run

3 |

2 |

49 | run (Do x f) = do r <- x

39 | run (Do x f) = do r <- x

5 | ~~~~~~~~~~~~~~~~~~~~~~~~ ...

4 | ~~~~~~~~~~~~~~~~~~~~~~~~ ...

5+Main.run is possibly not total due to recursive path Main.run --> Main.run

test/tutorial002/expected+3−3

@@ -1,15 +1,15 @@

1tutorial002.idr:41:25-29:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

441 | Main.natToBin_lemma_1 = proof

341 | Main.natToBin_lemma_1 = proof

5 | ~~~~~

4 | ~~~~~

6−tutorial002.idr:48:18-22:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+tutorial002.idr:48:18-22:

8 |

7 |

948 | parity_lemma_1 = proof

848 | parity_lemma_1 = proof

10 | ~~~~~

9 | ~~~~~

11−tutorial002.idr:54:18-22:

12This style of tactic proof is deprecated. See %runElab for the replacement.

10This style of tactic proof is deprecated. See %runElab for the replacement.

11+tutorial002.idr:54:18-22:

13 |

12 |

1454 | parity_lemma_2 = proof {

1354 | parity_lemma_2 = proof {

15 | ~~~~~

14 | ~~~~~

15+This style of tactic proof is deprecated. See %runElab for the replacement.

test/tutorial004/expected+2−2

@@ -1,10 +1,10 @@

1tutorial004.idr:46:14-18:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3 |

2 |

446 | plusredZ_S = proof {

346 | plusredZ_S = proof {

5 | ~~~~~

4 | ~~~~~

6−tutorial004.idr:53:14-18:

7This style of tactic proof is deprecated. See %runElab for the replacement.

5This style of tactic proof is deprecated. See %runElab for the replacement.

6+tutorial004.idr:53:14-18:

8 |

7 |

953 | plusredZ_Z = proof {

853 | plusredZ_Z = proof {

10 | ~~~~~

9 | ~~~~~

10+This style of tactic proof is deprecated. See %runElab for the replacement.

test/tutorial006/expected+6−6

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

1tutorial006a.idr:5:23-24:

2+ |

3+5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN

4+ | ~~

2When checking right hand side of vapp with expected type

5When checking right hand side of vapp with expected type

3 Vect (S len + m) a

6 Vect (S len + m) a

4

7

@@ -13,10 +16,10 @@ When checking argument xs to constructor Data.Vect.:::

13 plus len len

16 plus len len

14 and

17 and

15 plus len m

18 plus len m

16− |

17−5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN

18− | ~~

19tutorial006b.idr:10:37-50:

20+ |

21+10 | parity (S (S (j + j))) | Even = Even {n=S j}

22+ | ~~~~~~~~~~~~~~

20When checking right hand side of with block in Main.parity with expected type

23When checking right hand side of with block in Main.parity with expected type

21 Parity (S (S (j + j)))

24 Parity (S (S (j + j)))

22

25

@@ -30,6 +33,3 @@ Specifically:

30 plus (S j) (S j)

33 plus (S j) (S j)

31 and

34 and

32 S (S (plus j j))

35 S (S (plus j j))

33− |

34−10 | parity (S (S (j + j))) | Even = Even {n=S j}

35− | ~~~~~~~~~~~~~~

test/unique004/expected+27−18

@@ -1,56 +1,65 @@

1−unique001a.idr:35:14-43:50:Type mismatch between

1+unique001a.idr:35:14-43:50:

2− Int -> String

3−and

4− UniqueType (Int -> String)

5 |

2 |

635 | showStuff xs = do

335 | showStuff xs = do

7 | ~~~~ ...

4 | ~~~~ ...

8−unique001a.idr:46:15-54:28:Type mismatch between

5+Type mismatch between

9 Int -> String

6 Int -> String

10and

7and

11 UniqueType (Int -> String)

8 UniqueType (Int -> String)

9+unique001a.idr:46:15-54:28:

12 |

10 |

1346 | showStuff' xs = do

1146 | showStuff' xs = do

14 | ~~~~ ...

12 | ~~~~ ...

15−unique001a.idr:57:15-62:33:Type mismatch between

13+Type mismatch between

16− UniqueType (Int -> String)

17−and

18 Int -> String

14 Int -> String

15+and

16+ UniqueType (Int -> String)

17+unique001a.idr:57:15-62:33:

19 |

18 |

2057 | showThings xs = do

1957 | showThings xs = do

21 | ~~~~ ...

20 | ~~~~ ...

21+Type mismatch between

22+ UniqueType (Int -> String)

23+and

24+ Int -> String

22−unique001b.idr:18:17-42:Borrowed name xs must not be used on RHS

25+unique001b.idr:18:17-42:

23 |

26 |

2418 | showU (x :: xs) = show x ++ "," ++ free xs

2718 | showU (x :: xs) = show x ++ "," ++ free xs

25 | ~~~~~~~~~~~~~~~~~~~~~~~~~~

28 | ~~~~~~~~~~~~~~~~~~~~~~~~~~

29+Borrowed name xs must not be used on RHS

26−unique001c.idr:47:12-62:Unique name f is used more than once

30+unique001c.idr:47:12-62:

27 |

31 |

2847 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)

3247 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)

29 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

33 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

34+Unique name f is used more than once

30−unique001d.idr:4:16-18:Borrowed name x must not be used on RHS

35+unique001d.idr:4:16-18:

31 |

36 |

324 | steal (Read x) = x

374 | steal (Read x) = x

33 | ~~~

38 | ~~~

39+Borrowed name x must not be used on RHS

34unique001e.idr:4:12-40:

40unique001e.idr:4:12-40:

35−Constructor Main.Nil has a UniqueType, but the data type does not

36 |

41 |

374 | Nil : {a : UniqueType} -> BadList a

424 | Nil : {a : UniqueType} -> BadList a

38 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

43 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

44+Constructor Main.Nil has a UniqueType, but the data type does not

39−unique002.idr:17:8-20:19:Unique name xs is used more than once

45+unique002.idr:17:8-20:19:

40 |

46 |

4117 | foo xs = do -- let f = \x : Int => showU xs

4717 | foo xs = do -- let f = \x : Int => showU xs

42 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

48 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

49+Unique name xs is used more than once

43−unique002a.idr:17:8-20:19:Type mismatch between

50+unique002a.idr:17:8-20:19:

44− Int -> String

45−and

46− UniqueType (Int -> String)

47 |

51 |

4817 | foo xs = do let f = \x : Int => showU xs

5217 | foo xs = do let f = \x : Int => showU xs

49 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

53 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

50−unique003.idr:20:8-24:19:Type mismatch between

54+Type mismatch between

51 Int -> String

55 Int -> String

52and

56and

53 UniqueType (Int -> String)

57 UniqueType (Int -> String)

58+unique003.idr:20:8-24:19:

54 |

59 |

5520 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context

6020 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context

56 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

61 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

62+Type mismatch between

63+ Int -> String

64+and

65+ UniqueType (Int -> String)

test/universes001/expected+5−4

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

1+universes001.idr:7:5-21:

2+ |

3+7 | foo = Const (Const 0)

4+ | ~~~~~~~~~~~~~~~~~

1−universes001.idr:7:5-21:Universe inconsistency.

5+Universe inconsistency.

2 Working on: ./universes001.idr.x

6 Working on: ./universes001.idr.x

3 Old domain: (5,5)

7 Old domain: (5,5)

4 New domain: (5,4)

8 New domain: (5,4)

@@ -7,6 +11,3 @@ universes001.idr:7:5-21:Universe inconsistency.

7 ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}

11 ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}

8 ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}

12 ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}

9 ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}

13 ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}

10− |

11−7 | foo = Const (Const 0)

12− | ~~~~~~~~~~~~~~~~~

test/universes002/expected+5−4

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

1+universes002.idr:45:9-48:

2+ |

3+45 | russell = lemma (MkMPair (MkMPair R lemma) REFL)

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1−universes002.idr:45:9-48:Universe inconsistency.

5+Universe inconsistency.

2 Working on: ./universes002.idr.b1

6 Working on: ./universes002.idr.b1

3 Old domain: (5,5)

7 Old domain: (5,5)

4 New domain: (5,4)

8 New domain: (5,4)

@@ -7,6 +11,3 @@ universes002.idr:45:9-48:Universe inconsistency.

7 ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}

11 ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}

8 ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}

12 ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}

9 ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}

13 ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}

10− |

11−45 | russell = lemma (MkMPair (MkMPair R lemma) REFL)

12− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~