79351ee · Idris-dev · git.iko.soy

src/Idris/Output.hs+1−1

compare with master

unifiedsplit

@@ -98,7 +98,7 @@ iWarn fc err =

98 layoutSource _ _ = Nothing

99

100 layoutWarning :: OutputDoc -> Maybe OutputDoc -> OutputDoc -> OutputDoc

101− layoutWarning loc (Just src) err = loc <$$> src <$$> err

101+ layoutWarning loc (Just src) err = loc <$$> src <$$> err <$$> empty

102 layoutWarning loc Nothing err = loc </> err

103

104

test/basic002/expected+2

@@ -3,9 +3,11 @@ test006.idr:25:23-27:

325 | Main.parity_lemma_2 = proof {

4 | ~~~~~

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

6+

6test006.idr:32:23-27:

7test006.idr:32:23-27:

7 |

8 |

832 | Main.parity_lemma_1 = proof {

932 | Main.parity_lemma_1 = proof {

9 | ~~~~~

10 | ~~~~~

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

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

12+

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

13[False, True, False, True, False, True]

test/basic006/expected+1

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

10 Vect n a (Type of xs)

11 and

12 List a (Expected type)

13+

13[3, 2, 1]

14[3, 2, 1]

14"Number 42"

15"Number 42"

test/basic009/expected+3

@@ -5,6 +5,7 @@ Faulty.idr:6:9-11:

5 | ~~~

6num is bound as an implicit

7 Did you mean to refer to A.num?

8+

8Faulty.idr:7:7-12:

9Faulty.idr:7:7-12:

9 |

10 |

107 | fault = Refl

117 | fault = Refl

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

22 0

23 0

23 and

24 and

24 num

25 num

26+

25Multiple.idr:3:21:

27Multiple.idr:3:21:

26 |

28 |

273 | import Data.Vect as X

293 | import Data.Vect as X

28 | ^

30 | ^

29import alias not unique: "X"

31import alias not unique: "X"

32+

test/basic017/expected+1

@@ -5,3 +5,4 @@ basic017a.idr:11:8:

5When checking type of Main.append:

6When checking an application of Main.Vect:

7 No such variable n

8+

test/basic018/expected+3

@@ -4,12 +4,14 @@ basic018.idr:7:12-16:

4 | ~~~~~

5thing is bound as an implicit

6 Did you mean to refer to Main.thing?

7+

7basic018.idr:12:8-12:

8basic018.idr:12:8-12:

8 |

9 |

912 | test : thing = S 41

1012 | test : thing = S 41

10 | ~~~~~

11 | ~~~~~

11thing is bound as an implicit

12thing is bound as an implicit

12 Did you mean to refer to Main.thing?

13 Did you mean to refer to Main.thing?

14+

13basic018.idr:13:6-11:

15basic018.idr:13:6-11:

14 |

16 |

1513 | test = Refl

1713 | test = Refl

@@ -27,3 +29,4 @@ Specifically:

27 42

29 42

28 and

30 and

29 thing

31 thing

32+

test/directives001/expected+6

@@ -4,33 +4,39 @@ directives001.idr:14:7:

4 | ^

5Use of deprecated name directives001.Foo

6To be replaced with `Bar`.

7+

7directives001.idr:14:7:

8directives001.idr:14:7:

8 |

9 |

914 | mkFoo : String -> Foo

1014 | mkFoo : String -> Foo

10 | ^

11 | ^

11Use of deprecated name directives001.Foo

12Use of deprecated name directives001.Foo

12To be replaced with `Bar`.

13To be replaced with `Bar`.

14+

13directives001.idr:15:7-13:

15directives001.idr:15:7-13:

14 |

16 |

1515 | mkFoo = MkFoo

1715 | mkFoo = MkFoo

16 | ~~~~~~~

18 | ~~~~~~~

17Use of deprecated name directives001.Foo

19Use of deprecated name directives001.Foo

18To be replaced with `Bar`.

20To be replaced with `Bar`.

21+

19directives001.idr:15:7-13:

22directives001.idr:15:7-13:

20 |

23 |

2115 | mkFoo = MkFoo

2415 | mkFoo = MkFoo

22 | ~~~~~~~

25 | ~~~~~~~

23Use of deprecated name directives001.Foo

26Use of deprecated name directives001.Foo

24To be replaced with `Bar`.

27To be replaced with `Bar`.

28+

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

29directives001.idr:26:8-28:28:

26 |

30 |

2726 | main = do

3126 | main = do

28 | ~~~~ ...

32 | ~~~~ ...

29Use of a fragile construct directives001.mkBar

33Use of a fragile construct directives001.mkBar

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

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

35+

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

36directives001.idr:26:8-28:28:

32 |

37 |

3326 | main = do

3826 | main = do

34 | ~~~~ ...

39 | ~~~~ ...

35Use of a fragile construct directives001.mkBar

40Use of a fragile construct directives001.mkBar

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

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

42+

test/directives002/expected+1

@@ -3,3 +3,4 @@ directives002.idr:12:3-14:28:

312 | main = do

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

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

6+

test/effects003/expected+1

@@ -3,6 +3,7 @@ hangman.idr:204:8-12:

3204 | wlen = proof search

4 | ~~~~~

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

6+

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

7------------

7

8

86 guesses left

96 guesses left

test/error001/expected+1

@@ -10,3 +10,4 @@ Universe inconsistency.

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

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

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

13+

test/error003/expected+1

@@ -6,3 +6,4 @@ When checking right hand side of bad with expected type

6 Tm [] TUnit

7

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

9+

test/error004/expected+2

@@ -7,6 +7,7 @@ When checking right hand side of badCadr1 with expected type

7

8When checking argument cons2 to function FunErrTest.cadr:

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

10+

10FunErrTest.idr:38:12-19:

11FunErrTest.idr:38:12-19:

11 |

12 |

1238 | badCadr2 = cadr [1]

1338 | badCadr2 = cadr [1]

@@ -16,3 +17,4 @@ When checking right hand side of badCadr2 with expected type

16

17

17When checking argument cons2 to function FunErrTest.cadr:

18When checking argument cons2 to function FunErrTest.cadr:

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

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

20+

test/error005/expected+5

@@ -8,6 +8,7 @@ When checking right hand side of two with expected type

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

9 When using 2 as a literal for a Fin 2

10 2 is not strictly less than 2

11+

11error005.idr:14:12:

12error005.idr:14:12:

12 |

13 |

1314 | hahaha n = 0

1414 | hahaha n = 0

@@ -18,6 +19,7 @@ When checking right hand side of hahaha with expected type

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

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

19 When using 0 as a literal for a Fin n

20 When using 0 as a literal for a Fin n

20 0 is not strictly less than n

21 0 is not strictly less than n

22+

21error005.idr:20:11:

23error005.idr:20:11:

22 |

24 |

2320 | notOk n = 2

2520 | notOk n = 2

@@ -28,6 +30,7 @@ When checking right hand side of notOk with expected type

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

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

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

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

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

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

33+

31error005.idr:23:12-24:

34error005.idr:23:12-24:

32 |

35 |

3323 | b0rken n = fromInteger n

3623 | b0rken n = fromInteger n

@@ -39,6 +42,7 @@ When checking argument prf to function Data.Fin.fromInteger:

39 When using n as a literal for a Fin 3

42 When using n as a literal for a Fin 3

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

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

41 variable instead of a constant Integer

44 variable instead of a constant Integer

45+

42error005.idr:26:17:

46error005.idr:26:17:

43 |

47 |

4426 | x = the (Fin 4) 5

4826 | x = the (Fin 4) 5

@@ -49,3 +53,4 @@ When checking right hand side of x with expected type

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

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

50 When using 5 as a literal for a Fin 4

54 When using 5 as a literal for a Fin 4

51 5 is not strictly less than 4

55 5 is not strictly less than 4

56+

test/error006/expected+1

@@ -4,3 +4,4 @@ WithPatsNoWith.idr:4:1-13:

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

5When checking left hand side of foo:

6unexpected patterns outside of "with" block

7+

test/error007/expected+1

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

16 Bits32

17 and

18 Int

19+

test/error008/expected+2

@@ -4,9 +4,11 @@ error008.idr:3:4:

4 | ^

5When checking type of Main.s2:

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

7+

7error008a.idr:3:4:

8error008a.idr:3:4:

8 |

9 |

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

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

10 | ^

11 | ^

11When checking type of Main.s1:

12When checking type of Main.s1:

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

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

14+

test/ffi002/expected+1

@@ -3,3 +3,4 @@ test023.idr:20:26-36:

320 | %provide (t : Type) with badProvider

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

5Type provider error: Always fails

6+

test/interfaces008/expected+1

@@ -3,3 +3,4 @@ interfaces008.idr:20:18-23:

320 | implementation Foo2 a where

4 | ~~~~~~

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

6+

test/layout001/expected+1

@@ -67,6 +67,7 @@ When checking right hand side of term with expected type

67

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

69 No such variable f

70+

70./mplus2.idr:17:37:

71./mplus2.idr:17:37:

71 |

72 |

7217 | `mplus` pure f

7317 | `mplus` pure f

test/literate001/expected+1

@@ -3,6 +3,7 @@

31 | Broken

4 | ^

5Program line next to comment

6+

6'a'

7'a'

7'd'

8'd'

8zabcdefg

9zabcdefg

test/meta002/expected+3

@@ -4,6 +4,7 @@ DataDef.idr:74:1-8:

4 | ~~~~~~~~

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

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

7+

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

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

8 |

9 |

9299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))

10299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))

@@ -12,6 +13,7 @@ When checking right hand side of testElab3 with expected type

12 DPair Ty (Tm [])

13 DPair Ty (Tm [])

13

14

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

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

16+

15AgdaStyleReflection.idr:315:5-20:

17AgdaStyleReflection.idr:315:5-20:

16 |

18 |

17315 | baz = tactic trivial

19315 | baz = tactic trivial

@@ -20,3 +22,4 @@ When checking right hand side of baz with expected type

20 (Nat, Void)

22 (Nat, Void)

21

23

22PROOF SEARCH FAILURE is not defined.

24PROOF SEARCH FAILURE is not defined.

25+

test/meta003/expected+1

@@ -7,3 +7,4 @@ Type mismatch between

7 ()

8and

9 String

10+

test/meta004/expected+1

@@ -4,3 +4,4 @@ meta004.idr:50:1-8:

4 | ~~~~~~~~

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

6Not an impossible case

7+

test/proof001/expected+2

@@ -3,8 +3,10 @@ test029.idr:29:25-29:

329 | simple.append_lemma_2 = proof {

4 | ~~~~~

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

6+

6test029.idr:36:25-29:

7test029.idr:36:25-29:

7 |

8 |

836 | simple.append_lemma_1 = proof {

936 | simple.append_lemma_1 = proof {

9 | ~~~~~

10 | ~~~~~

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

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

12+

test/proof002/expected+4

@@ -3,16 +3,19 @@ Reflect.idr:175:21-25:

3175 | Reflect.appRExpr1 = proof {

4 | ~~~~~

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

6+

6Reflect.idr:184:21-25:

7Reflect.idr:184:21-25:

7 |

8 |

8184 | Reflect.appRExpr2 = proof {

9184 | Reflect.appRExpr2 = proof {

9 | ~~~~~

10 | ~~~~~

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

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

12+

11Reflect.idr:192:15-19:

13Reflect.idr:192:15-19:

12 |

14 |

13192 | Reflect.bp1 = proof {

15192 | Reflect.bp1 = proof {

14 | ~~~~~

16 | ~~~~~

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

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

18+

16test030a.idr:12:26-37:

19test030a.idr:12:26-37:

17 |

20 |

1812 | testReflect1 {a} xs ys = AssocProof a

2112 | testReflect1 {a} xs ys = AssocProof a

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

31 Just x

34 Just x

32 and

35 and

33 Nothing

36 Nothing

37+

test/proof003/expected+6

@@ -3,31 +3,37 @@ Parity.idr:17:18-22:

317 | parity_lemma_2 = proof {

4 | ~~~~~

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

6+

6Parity.idr:24:18-22:

7Parity.idr:24:18-22:

7 |

8 |

824 | parity_lemma_1 = proof {

924 | parity_lemma_1 = proof {

9 | ~~~~~

10 | ~~~~~

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

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

12+

11test015.idr:88:15-19:

13test015.idr:88:15-19:

12 |

14 |

1388 | Main.ntbOdd = proof {

1588 | Main.ntbOdd = proof {

14 | ~~~~~

16 | ~~~~~

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

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

18+

16test015.idr:97:16-20:

19test015.idr:97:16-20:

17 |

20 |

1897 | Main.ntbEven = proof {

2197 | Main.ntbEven = proof {

19 | ~~~~~

22 | ~~~~~

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

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

24+

21test015.idr:107:20-24:

25test015.idr:107:20-24:

22 |

26 |

23107 | Main.adc_lemma_2 = proof {

27107 | Main.adc_lemma_2 = proof {

24 | ~~~~~

28 | ~~~~~

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

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

30+

26test015.idr:142:20-24:

31test015.idr:142:20-24:

27 |

32 |

28142 | Main.adc_lemma_1 = proof {

33142 | Main.adc_lemma_1 = proof {

29 | ~~~~~

34 | ~~~~~

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

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

36+

3100101010

3700101010

3201011001

3801011001

33010000011

39010000011

test/proof007/expected+1

@@ -7,3 +7,4 @@ When checking right hand side of test with expected type

7

8When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

9 No such variable sadgjhsag

10+

test/proof008/expected+1

@@ -3,3 +3,4 @@ ClaimAndUnfocus.idr:8:27-31:

38 | ClaimAndUnfocus.foo_rhs = proof

4 | ~~~~~

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

6+

test/proof011/expected+2

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

11 x ::

12 (xs ++ ys) ++

13 zs

14+

14proof011a.idr:14:5-37:

15proof011a.idr:14:5-37:

15 |

16 |

1614 | = rewrite vassoc xs ys xs in Refl

1714 | = rewrite vassoc xs ys xs in Refl

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

24 x ::

25 x ::

25 (xs ++ ys) ++

26 (xs ++ ys) ++

26 zs

27 zs

28+

test/quasiquote003/expected+1

@@ -6,3 +6,4 @@ When checking right hand side of zzz with expected type

6 TT

7

8No such variable k

9+

test/quasiquote004/expected+4

@@ -3,16 +3,19 @@ Quasiquote004.idr:39:26-30:

339 | Quasiquote004.getMeNat = proof

4 | ~~~~~

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

6+

6Quasiquote004.idr:42:28-32:

7Quasiquote004.idr:42:28-32:

7 |

8 |

842 | Quasiquote004.fizzyIsAOK = proof

942 | Quasiquote004.fizzyIsAOK = proof

9 | ~~~~~

10 | ~~~~~

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

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

12+

11Quasiquote004.idr:50:27-31:

13Quasiquote004.idr:50:27-31:

12 |

14 |

1350 | Quasiquote004.getMeNat' = proof

1550 | Quasiquote004.getMeNat' = proof

14 | ~~~~~

16 | ~~~~~

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

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

18+

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

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

17 |

20 |

1850 | Quasiquote004.getMeNat' = proof

2150 | Quasiquote004.getMeNat' = proof

@@ -21,3 +24,4 @@ When checking right hand side of Quasiquote004.getMeNat' with expected type

21 String

24 String

22

25

23Not a Nat goal

26Not a Nat goal

27+

test/quasiquote006/expected+3

@@ -7,6 +7,7 @@ When checking right hand side of b with expected type

7

8Can't disambiguate name: ForeignEnv.Nil,

9 Prelude.List.Nil

10+

10quasiquote006.idr:12:3-17:

11quasiquote006.idr:12:3-17:

11 |

12 |

1212 | c = `{alsdkjflkj}

1312 | c = `{alsdkjflkj}

@@ -15,6 +16,7 @@ When checking right hand side of c with expected type

15 TTName

16 TTName

16

17

17No such variable alsdkjflkj

18No such variable alsdkjflkj

19+

18quasiquote006.idr:15:3-11:

20quasiquote006.idr:15:3-11:

19 |

21 |

2015 | d = `{(::)}

2215 | d = `{(::)}

@@ -25,4 +27,5 @@ When checking right hand side of d with expected type

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

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

26 Prelude.List.::,

28 Prelude.List.::,

27 Prelude.Stream.::

29 Prelude.Stream.::

30+

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

31 quasiquote006.idr:17:3:Main.d already defined

test/reg017/expected+2

@@ -3,9 +3,11 @@ reg017.idr:5:17-23:

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

4 | ~~~~~~~

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

6+

6reg017.idr:8:17-23:

7reg017.idr:8:17-23:

7 |

8 |

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

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

9 | ~~~~~~~

10 | ~~~~~~~

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

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

12+

114

134

test/reg027/expected+1

@@ -4,3 +4,4 @@ reg027a.idr:9:16-30:

49 | implementation Show (Int -> b) where

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

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

7+

test/regression002/expected+43

@@ -4,28 +4,33 @@ reg003a.idr:4:13-38:

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

5When checking type of Main.ECons:

6No such variable OddList

7+

7reg003a.idr:7:13-38:

8reg003a.idr:7:13-38:

8 |

9 |

97 | OCons : Nat -> EvenList -> OddList

107 | OCons : Nat -> EvenList -> OddList

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

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

11When checking type of Main.OCons:

12When checking type of Main.OCons:

12No such variable EvenList

13No such variable EvenList

14+

13reg003a.idr:9:6:

15reg003a.idr:9:6:

14 |

16 |

159 | test : EvenList

179 | test : EvenList

16 | ^

18 | ^

17When checking type of Main.test:

19When checking type of Main.test:

18No such variable EvenList

20No such variable EvenList

21+

19reg006.idr:17:1-23:

22reg006.idr:17:1-23:

20 |

23 |

2117 | lookup k Leaf = Nothing

2417 | lookup k Leaf = Nothing

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

25 | ~~~~~~~~~~~~~~~~~~~~~~~

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

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

27+

24reg007.lidr:8:3-13:

28reg007.lidr:8:3-13:

25 |

29 |

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

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

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

31 | ~~~~~~~~~~~

28A.n is already defined

32A.n is already defined

33+

29reg007.lidr:12:13-18:

34reg007.lidr:12:13-18:

30 |

35 |

3112 | > hurrah = isSame

3612 | > hurrah = isSame

@@ -43,42 +48,50 @@ Specifically:

43 1

48 1

44 and

49 and

45 0

50 0

51+

46reg010.idr:5:3-26:

52reg010.idr:5:3-26:

47 |

53 |

485 | unsafeSubst P x x px | _ = px

545 | unsafeSubst P x x px | _ = px

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

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

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

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

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

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

58+

52reg018a.idr:16:1-18:

59reg018a.idr:16:1-18:

53 |

60 |

5416 | minusCoNat Z n = Z

6116 | minusCoNat Z n = Z

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

62 | ~~~~~~~~~~~~~~~~~~

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

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

64+

57reg018a.idr:21:1-42:

65reg018a.idr:21:1-42:

58 |

66 |

5921 | loopForever = minusCoNat infinity infinity

6721 | loopForever = minusCoNat infinity infinity

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

68 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

69conat.loopForever is possibly not total due to: conat.minusCoNat

70+

62reg018b.idr:8:1-28:

71reg018b.idr:8:1-28:

63 |

72 |

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

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

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

74 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

76+

67reg018b.idr:11:1-6:

77reg018b.idr:11:1-6:

68 |

78 |

6911 | Show B where show = showB

7911 | Show B where show = showB

70 | ~~~~~~

80 | ~~~~~~

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

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

82+

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

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

73 |

84 |

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

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

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

86 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

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

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

88+

77reg018d.idr:8:1-39:

89reg018d.idr:8:1-39:

78 |

90 |

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

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

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

92 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

93Main.pull is not total as there are missing cases

94+

82reg023.idr:7:5-7:

95reg023.idr:7:5-7:

83 |

96 |

847 | bad = Z

977 | bad = Z

@@ -90,43 +103,51 @@ Type mismatch between

90 Nat (Type of 0)

103 Nat (Type of 0)

91and

104and

92 f Nat (Expected type)

105 f Nat (Expected type)

106+

93reg028.idr:5:1-9:

107reg028.idr:5:1-9:

94 |

108 |

955 | bad Z = Z

1095 | bad Z = Z

96 | ~~~~~~~~~

110 | ~~~~~~~~~

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

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

112+

98reg028a.idr:17:14-18:

113reg028a.idr:17:14-18:

99 |

114 |

10017 | qsortLemma = proof

11517 | qsortLemma = proof

101 | ~~~~~

116 | ~~~~~

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

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

118+

103reg028a.idr:11:1-14:

119reg028a.idr:11:1-14:

104 |

120 |

10511 | qsort' [] = []

12111 | qsort' [] = []

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

122 | ~~~~~~~~~~~~~~

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

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

124+

108reg034.idr:6:1-14:

125reg034.idr:6:1-14:

109 |

126 |

1106 | bar xs xs Refl = Refl

1276 | bar xs xs Refl = Refl

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

128 | ~~~~~~~~~~~~~~

112When checking left hand side of bar:

129When checking left hand side of bar:

113Can't match on bar xs xs Refl

130Can't match on bar xs xs Refl

131+

114reg034.idr:9:1-14:

132reg034.idr:9:1-14:

115 |

133 |

1169 | foo f x x Refl = Refl

1349 | foo f x x Refl = Refl

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

135 | ~~~~~~~~~~~~~~

118When checking left hand side of foo:

136When checking left hand side of foo:

119Can't match on foo f x x Refl

137Can't match on foo f x x Refl

138+

120reg035b.idr:8:12-38:

139reg035b.idr:8:12-38:

121 |

140 |

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

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

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

142 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~

124No such variable __pi_arg

143No such variable __pi_arg

144+

125reg044.idr:4:6-10:

145reg044.idr:4:6-10:

126 |

146 |

1274 | pf = proof

1474 | pf = proof

128 | ~~~~~

148 | ~~~~~

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

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

150+

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

151reg044.idr:4:4-6:13:

131 |

152 |

1324 | pf = proof

1534 | pf = proof

@@ -144,12 +165,14 @@ Specifically:

144 b

165 b

145 and

166 and

146 a

167 a

168+

147reg049.idr:2:11-14:

169reg049.idr:2:11-14:

148 |

170 |

1492 | Bogus : Void

1712 | Bogus : Void

150 | ~~~~

172 | ~~~~

151When checking constructor Main.Bogus:

173When checking constructor Main.Bogus:

152Void is not Main.Foo

174Void is not Main.Foo

175+

153reg049.idr:5:6-12:

176reg049.idr:5:6-12:

154 |

177 |

1555 | uhOh = Bogus

1785 | uhOh = Bogus

@@ -158,6 +181,7 @@ When checking right hand side of uhOh with expected type

158 Void

181 Void

159

182

160No such variable Bogus

183No such variable Bogus

184+

161./badbangop.idr:7:1:

185./badbangop.idr:7:1:

162 |

186 |

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

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

@@ -177,18 +201,21 @@ reg054.idr:18:1-17:

177When checking left hand side of inf:

201When checking left hand side of inf:

178When checking an application of constructor Main.MkInfer:

202When checking an application of constructor Main.MkInfer:

179 Attempting concrete match on polymorphic argument: 0

203 Attempting concrete match on polymorphic argument: 0

204+

180reg054.idr:34:1-18:

205reg054.idr:34:1-18:

181 |

206 |

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

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

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

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

184When checking left hand side of weird:

209When checking left hand side of weird:

185No explicit types on left hand side: Char

210No explicit types on left hand side: Char

211+

186reg054.idr:37:1-30:

212reg054.idr:37:1-30:

187 |

213 |

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

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

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

215 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

190When checking left hand side of weird':

216When checking left hand side of weird':

191No explicit types on left hand side: Nat

217No explicit types on left hand side: Nat

218+

192reg054.idr:40:1-7:

219reg054.idr:40:1-7:

193 |

220 |

19440 | tctrick (Just x) = x

22140 | tctrick (Just x) = x

@@ -199,18 +226,21 @@ When checking an application of Main.tctrick:

199 Maybe a1 (Type of Just x)

226 Maybe a1 (Type of Just x)

200 and

227 and

201 a (Expected type)

228 a (Expected type)

229+

202reg055.idr:5:1-7:

230reg055.idr:5:1-7:

203 |

231 |

2045 | g (f Z) = 1

2325 | g (f Z) = 1

205 | ~~~~~~~

233 | ~~~~~~~

206When checking left hand side of g:

234When checking left hand side of g:

207Can't match on g (f 0)

235Can't match on g (f 0)

236+

208reg055.idr:8:1-5:

237reg055.idr:8:1-5:

209 |

238 |

2108 | h x x = x

2398 | h x x = x

211 | ~~~~~

240 | ~~~~~

212When checking left hand side of h:

241When checking left hand side of h:

213Can't match on h x x

242Can't match on h x x

243+

214reg055a.idr:8:1-18:

244reg055a.idr:8:1-18:

215 |

245 |

2168 | foo (CAny Nothing) = 42

2468 | foo (CAny Nothing) = 42

@@ -218,56 +248,66 @@ reg055a.idr:8:1-18:

218When checking left hand side of foo:

248When checking left hand side of foo:

219When checking an application of constructor Foo.CAny:

249When checking an application of constructor Foo.CAny:

220 Attempting concrete match on polymorphic argument: Nothing

250 Attempting concrete match on polymorphic argument: Nothing

251+

221reg055a.idr:13:1-23:

252reg055a.idr:13:1-23:

222 |

253 |

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

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

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

255 | ~~~~~~~~~~~~~~~~~~~~~~~

225When checking left hand side of Foo.apply:

256When checking left hand side of Foo.apply:

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

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

258+

227reg056.idr:7:16-25:

259reg056.idr:7:16-25:

228 |

260 |

2297 | dodgy n m Refl impossible

2617 | dodgy n m Refl impossible

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

262 | ~~~~~~~~~~

231dodgy n m Refl is a valid case

263dodgy n m Refl is a valid case

264+

232reg056.idr:10:11-20:

265reg056.idr:10:11-20:

233 |

266 |

23410 | nonk Refl impossible

26710 | nonk Refl impossible

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

268 | ~~~~~~~~~~

236nonk Refl is a valid case

269nonk Refl is a valid case

270+

237reg068.idr:1:6-8:

271reg068.idr:1:6-8:

238 |

272 |

2391 | data nat : Type where --error

2731 | data nat : Type where --error

240 | ~~~

274 | ~~~

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

275Main.nat has a name which may be implicitly bound.

242This is likely to lead to problems!

276This is likely to lead to problems!

277+

243reg068.idr:2:8-10:

278reg068.idr:2:8-10:

244 |

279 |

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

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

246 | ~~~

281 | ~~~

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

282Main.ze has a name which may be implicitly bound.

248This is likely to lead to problems!

283This is likely to lead to problems!

284+

249reg068.idr:2:8-10:

285reg068.idr:2:8-10:

250 |

286 |

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

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

252 | ~~~

288 | ~~~

253nat is bound as an implicit

289nat is bound as an implicit

254 Did you mean to refer to Main.nat?

290 Did you mean to refer to Main.nat?

291+

255reg068.idr:2:8-10:

292reg068.idr:2:8-10:

256 |

293 |

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

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

258 | ~~~

295 | ~~~

259When checking constructor Main.ze:

296When checking constructor Main.ze:

260Type level variable nat is not Main.nat

297Type level variable nat is not Main.nat

298+

261Mod.idr:11:1-22:

299Mod.idr:11:1-22:

262 |

300 |

26311 | natexp k = S (natfn k)

30111 | natexp k = S (natfn k)

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

302 | ~~~~~~~~~~~~~~~~~~~~~~

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

303public export Mod.natexp can't refer to export Mod.natfn

304+

266reg070.idr:7:1-7:

305reg070.idr:7:1-7:

267 |

306 |

2687 | Show Te where

3077 | Show Te where

269 | ~~~~~~~

308 | ~~~~~~~

270Test_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

309Test_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

310+

271./reg076.idr:8:1:

311./reg076.idr:8:1:

272 |

312 |

2738 | <empty line>

3138 | <empty line>

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

298 -0.0

338 -0.0

299 and

339 and

300 0.0

340 0.0

341+

301Canonicity.idr:9:1-9:

342Canonicity.idr:9:1-9:

302 |

343 |

3039 | f Nil = 0

3449 | f Nil = 0

304 | ~~~~~~~~~

345 | ~~~~~~~~~

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

346Canonicity.f is not total as there are missing cases

347+

306Canonicity.idr:12:1-20:

348Canonicity.idr:12:1-20:

307 |

349 |

30812 | NaN = f (Cons 0 Nil)

35012 | NaN = f (Cons 0 Nil)

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

351 | ~~~~~~~~~~~~~~~~~~~~

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

352Canonicity.NaN is possibly not total due to: Canonicity.f

353+

test/sourceLocation001/expected+4

@@ -3,21 +3,25 @@ SourceLoc.idr:12:19-25:

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

4 | ~~~~~~~

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

6+

6SourceLoc.idr:21:19-23:

7SourceLoc.idr:21:19-23:

7 |

8 |

821 | fromProofScript = proof sourceLocation

921 | fromProofScript = proof sourceLocation

9 | ~~~~~

10 | ~~~~~

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

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

12+

11SourceLoc.idr:41:20-26:

13SourceLoc.idr:41:20-26:

12 |

14 |

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

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

14 | ~~~~~~~

16 | ~~~~~~~

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

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

18+

16SourceLoc.idr:99:18-22:

19SourceLoc.idr:99:18-22:

17 |

20 |

1899 | SourceLoc.meta = proof

2199 | SourceLoc.meta = proof

19 | ~~~~~

22 | ~~~~~

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

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

24+

21Testing using definition

25Testing using definition

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

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

23Testing using inline tactics

27Testing using inline tactics

test/syntax001/expected+2

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

10 String (Type of "argh")

11 and

12 Nat (Expected type)

13+

13SyntaxTest.idr:5:7-18:

14SyntaxTest.idr:5:7-18:

14 |

15 |

155 | foo = fnord "argh"

165 | foo = fnord "argh"

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

22 String (Type of "argh")

23 String (Type of "argh")

23 and

24 and

24 Nat (Expected type)

25 Nat (Expected type)

26+

test/totality001/expected+3

@@ -3,13 +3,16 @@ test010.idr:15:1-30:

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

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

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

6+

6test010a.idr:9:1-23:

7test010a.idr:9:1-23:

7 |

8 |

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

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

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

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

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

11main.bar is possibly not total due to: main.MkBad

12+

11test010b.idr:9:1-23:

13test010b.idr:9:1-23:

12 |

14 |

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

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

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

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

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

17main.bar is possibly not total due to: main.MkBad

18+

test/totality002/expected+3

@@ -3,13 +3,16 @@ test017.idr:94:26-30:

394 | maxCommutativeStepCase = proof {

4 | ~~~~~

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

6+

6test017a.idr:7:1-24:

7test017a.idr:7:1-24:

7 |

8 |

87 | vtrans [] _ = []

97 | vtrans [] _ = []

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

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

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

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

12+

11test017b.idr:4:1-9:

13test017b.idr:4:1-9:

12 |

14 |

134 | foo = foo

154 | foo = foo

14 | ~~~~~~~~~

16 | ~~~~~~~~~

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

17foo.foo is possibly not total due to recursive path foo.foo

18+

test/totality003/expected+1

@@ -3,3 +3,4 @@ totality003a.idr:5:1-13:

35 | qsort [] = []

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

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

6+

test/totality004/expected+2

@@ -4,8 +4,10 @@ totality004a.idr:13:1-44:

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

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

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

7+

7totality004a.idr:24:1-60:

8totality004a.idr:24:1-60:

8 |

9 |

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

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

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

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

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

12Main.main is possibly not total due to: Main.process

13+

test/totality006/expected+3

@@ -3,13 +3,16 @@ totality006.idr:8:1-29:

38 | prf Z Z Oh impossible

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

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

6+

6totality006a.idr:11:21-30:

7totality006a.idr:11:21-30:

7 |

8 |

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

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

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

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

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

11prf' (S _) (S _) Oh is a valid case

12+

11totality006b.idr:10:1-34:

13totality006b.idr:10:1-34:

12 |

14 |

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

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

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

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

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

17totality006b.blargh is not total as there are missing cases

18+

test/totality007/expected+1

@@ -4,5 +4,6 @@ Totality.idr:4:1-9:

44 | foo Z = Z

5 | ~~~~~~~~~

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

7+

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

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

8Leaving directory `./src'

9Leaving directory `./src'

test/totality008/expected+1

@@ -3,3 +3,4 @@ totality008.idr:7:1-14:

37 | ElimT _ C1 = 3

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

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

6+

test/totality009/expected+10

@@ -3,48 +3,58 @@ TestLambdaPossible.idr:9:25-34:

39 | wrongPossible = (\Flase impossible)

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

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

6+

6TestLambdaPossible.idr:9:1-35:

7TestLambdaPossible.idr:9:1-35:

7 |

8 |

89 | wrongPossible = (\Flase impossible)

99 | wrongPossible = (\Flase impossible)

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

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

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

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

12+

11TestLambdaPossible.idr:12:25:

13TestLambdaPossible.idr:12:25:

12 |

14 |

1312 | wrongPossible' x = case x of

1512 | wrongPossible' x = case x of

14 | ^

16 | ^

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

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

18+

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

19TestLambdaPossible.idr:12:1-13:40:

17 |

20 |

1812 | wrongPossible' x = case x of

2112 | wrongPossible' x = case x of

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

22 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

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

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

24+

21TestLambdaPossible.idr:9:15-35:

25TestLambdaPossible.idr:9:15-35:

22 |

26 |

239 | wrongPossible = (\Flase impossible)

279 | wrongPossible = (\Flase impossible)

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

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

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

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

30+

26TestLambdaPossible.idr:9:1-35:

31TestLambdaPossible.idr:9:1-35:

27 |

32 |

289 | wrongPossible = (\Flase impossible)

339 | wrongPossible = (\Flase impossible)

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

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

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

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

36+

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

37TestLambdaPossible.idr:12:18-13:40:

32 |

38 |

3312 | wrongPossible' x = case x of

3912 | wrongPossible' x = case x of

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

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

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

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

42+

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

43TestLambdaPossible.idr:12:1-13:40:

37 |

44 |

3812 | wrongPossible' x = case x of

4512 | wrongPossible' x = case x of

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

46 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

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

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

48+

41TestLambdaPossible2.idr:10:1-35:

49TestLambdaPossible2.idr:10:1-35:

42 |

50 |

4310 | wrongPossible = (\Flase impossible)

5110 | wrongPossible = (\Flase impossible)

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

52 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

54+

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

55TestLambdaPossible2.idr:14:1-15:40:

47 |

56 |

4814 | wrongPossible' x = case x of

5714 | wrongPossible' x = case x of

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

58 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

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

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

60+

test/totality010/expected+2

@@ -3,8 +3,10 @@ totality010.idr:27:1-35:

327 | evenNotS MkEven ZeroEven impossible

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

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

6+

6totality010.idr:30:1-40:

7totality010.idr:30:1-40:

7 |

8 |

830 | bad = evenNotS ZeroEven $ MkBad ZeroEven

930 | bad = evenNotS ZeroEven $ MkBad ZeroEven

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

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

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

11Main.bad is possibly not total due to: Main.evenNotS

12+

test/totality011/expected+1

@@ -3,3 +3,4 @@ totality011.lidr:22:3-57:

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

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

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

6+

test/totality012/expected+2

@@ -3,8 +3,10 @@ totality012a.idr:9:1-10:27:

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

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

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

6+

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

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

7 |

8 |

811 | echo = do PutStr "$ "

911 | echo = do PutStr "$ "

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

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

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

11Main.echo is possibly not total due to recursive path Main.echo

12+

test/totality013/expected+2

@@ -3,8 +3,10 @@ totality013a.idr:5:3-49:

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

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

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

6+

6totality013a.idr:9:3-36:

7totality013a.idr:9:3-36:

7 |

8 |

89 | mtot order [] right = right

99 | mtot order [] right = right

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

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

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

11Main.mtot is possibly not total due to: Main.foo

12+

test/totality014/expected+1

@@ -10,3 +10,4 @@ Universe inconsistency.

10 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}

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

13+

test/totality015/expected+3

@@ -3,13 +3,16 @@ totality015a.idr:52:3-53:

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

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

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

6+

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

7totality015a.idr:42:3-44:36:

7 |

8 |

842 | correct nums score

942 | correct nums score

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

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

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

11Main.correct is possibly not total due to: Main.quiz

12+

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

13totality015a.idr:47:3-49:28:

12 |

14 |

1347 | wrong nums ans score

1547 | wrong nums ans score

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

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

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

17Main.wrong is possibly not total due to: Main.quiz

18+

test/totality016/expected+9

@@ -3,43 +3,52 @@ totality016.idr:15:1-21:

315 | f1 (MkTP T1 x) = True

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

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

6+

6totality016.idr:19:1-24:

7totality016.idr:19:1-24:

7 |

8 |

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

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

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

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

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

11Main.f2 is not total as there are missing cases

12+

11totality016.idr:23:1-29:

13totality016.idr:23:1-29:

12 |

14 |

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

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

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

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

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

17Main.f3 is not total as there are missing cases

18+

16totality016.idr:27:1-14:

19totality016.idr:27:1-14:

17 |

20 |

1827 | g1 T1 x = True

2127 | g1 T1 x = True

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

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

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

23Main.g1 is not total as there are missing cases

24+

21totality016.idr:31:1-17:

25totality016.idr:31:1-17:

22 |

26 |

2331 | g2 (T1, x) = True

2731 | g2 (T1, x) = True

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

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

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

29Main.g2 is not total as there are missing cases

30+

26totality016.idr:35:1-16:

31totality016.idr:35:1-16:

27 |

32 |

2835 | h1 True x = True

3335 | h1 True x = True

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

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

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

35Main.h1 is not total as there are missing cases

36+

31totality016.idr:39:1-19:

37totality016.idr:39:1-19:

32 |

38 |

3339 | h2 (True, x) = True

3939 | h2 (True, x) = True

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

40 | ~~~~~~~~~~~~~~~~~~~

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

41Main.h2 is not total as there are missing cases

42+

36totality016.idr:43:1-25:

43totality016.idr:43:1-25:

37 |

44 |

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

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

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

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

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

47Main.h3 is not total as there are missing cases

48+

41totality016.idr:47:1-30:

49totality016.idr:47:1-30:

42 |

50 |

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

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

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

52 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

53Main.h4 is not total as there are missing cases

54+

test/totality017/expected+6

@@ -3,28 +3,34 @@ totality017.idr:19:1-15:

319 | g1 T1 T1 = True

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

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

6+

6totality017.idr:25:1-17:

7totality017.idr:25:1-17:

7 |

8 |

825 | g2 T1' T1' = True

925 | g2 T1' T1' = True

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

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

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

11Main.g2 is not total as there are missing cases

12+

11totality017.idr:31:1-13:

13totality017.idr:31:1-13:

12 |

14 |

1331 | g3 T1' = True

1531 | g3 T1' = True

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

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

15Main.g3 is not total as there are missing cases

17Main.g3 is not total as there are missing cases

18+

16totality017.idr:37:1-36:

19totality017.idr:37:1-36:

17 |

20 |

1837 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True

2137 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True

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

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

20Main.g4 is not total as there are missing cases

23Main.g4 is not total as there are missing cases

24+

21totality017.idr:42:1-11:

25totality017.idr:42:1-11:

22 |

26 |

2342 | f' 0 = True

2742 | f' 0 = True

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

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

25Main.f' is not total as there are missing cases

29Main.f' is not total as there are missing cases

30+

26totality017.idr:47:1-17:

31totality017.idr:47:1-17:

27 |

32 |

2847 | f (MkPP 0) = True

3347 | f (MkPP 0) = True

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

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

30Main.f is not total as there are missing cases

35Main.f is not total as there are missing cases

36+

test/totality018/expected+1

@@ -3,3 +3,4 @@ totality018.idr:12:1-10:

312 | bar FZ = 0

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

5Main.bar is not total as there are missing cases

6+

test/totality019/expected+2

@@ -3,8 +3,10 @@ totality019.idr:8:1-36:

38 | testCov False False = ?testCov_rhs_3

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

5Main.testCov is not total as there are missing cases

6+

6totality019.idr:12:1-42:

7totality019.idr:12:1-42:

7 |

8 |

812 | testCov' (False ** False) = ?testCov_rhs_3

912 | testCov' (False ** False) = ?testCov_rhs_3

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

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

10Main.testCov' is not total as there are missing cases

11Main.testCov' is not total as there are missing cases

12+

test/totality020/expected+2

@@ -3,8 +3,10 @@ totality020.idr:4:14-23:

34 | bug _ _ Refl impossible

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

5bug _ _ Refl is a valid case

6+

6totality020.idr:7:14-23:

7totality020.idr:7:14-23:

7 |

8 |

87 | foo a b Refl impossible

97 | foo a b Refl impossible

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

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

10foo a b Refl is a valid case

11foo a b Refl is a valid case

12+

test/totality021/expected+5

@@ -3,23 +3,28 @@ totality021.idr:8:1-67:

38 | sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl

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

5Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'

6+

6totality021.idr:12:1-66:

7totality021.idr:12:1-66:

7 |

8 |

812 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl

912 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl

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

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

10Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'

11Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'

12+

11totality021.idr:18:1-26:

13totality021.idr:18:1-26:

12 |

14 |

1318 | v = sLevelNotSLevel l Refl

1518 | v = sLevelNotSLevel l Refl

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

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

15Main.v is possibly not total due to: Main.sLevelNotSLevel

17Main.v is possibly not total due to: Main.sLevelNotSLevel

18+

16totality021a.idr:9:1-37:

19totality021a.idr:9:1-37:

17 |

20 |

189 | noNonEmptyPointInt {n} Nil impossible

219 | noNonEmptyPointInt {n} Nil impossible

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

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

20Main.noNonEmptyPointInt is not total as there are missing cases

23Main.noNonEmptyPointInt is not total as there are missing cases

24+

21totality021a.idr:12:1-31:

25totality021a.idr:12:1-31:

22 |

26 |

2312 | myVoid = noNonEmptyPointInt [2]

2712 | myVoid = noNonEmptyPointInt [2]

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

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

25Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt

29Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt

30+

test/totality022/expected+1

@@ -3,3 +3,4 @@ totality022.idr:7:20-29:

37 | f _ [] (RSnoc _ _) impossible -- = ?wat

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

5f _ [] (RSnoc _ _) is a valid case

6+

test/totality023/expected+1

@@ -3,3 +3,4 @@ totality023.idr:9:1-10:27:

39 | run (Do x f) = do r <- x

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

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

6+

test/tutorial002/expected+3

@@ -3,13 +3,16 @@ tutorial002.idr:41:25-29:

341 | Main.natToBin_lemma_1 = proof

4 | ~~~~~

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

6+

6tutorial002.idr:48:18-22:

7tutorial002.idr:48:18-22:

7 |

8 |

848 | parity_lemma_1 = proof

948 | parity_lemma_1 = proof

9 | ~~~~~

10 | ~~~~~

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

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

12+

11tutorial002.idr:54:18-22:

13tutorial002.idr:54:18-22:

12 |

14 |

1354 | parity_lemma_2 = proof {

1554 | parity_lemma_2 = proof {

14 | ~~~~~

16 | ~~~~~

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

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

18+

test/tutorial004/expected+2

@@ -3,8 +3,10 @@ tutorial004.idr:46:14-18:

346 | plusredZ_S = proof {

4 | ~~~~~

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

6+

6tutorial004.idr:53:14-18:

7tutorial004.idr:53:14-18:

7 |

8 |

853 | plusredZ_Z = proof {

953 | plusredZ_Z = proof {

9 | ~~~~~

10 | ~~~~~

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

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

12+

test/tutorial006/expected+2

@@ -16,6 +16,7 @@ When checking argument xs to constructor Data.Vect.:::

16 plus len len

17 and

18 plus len m

19+

19tutorial006b.idr:10:37-50:

20tutorial006b.idr:10:37-50:

20 |

21 |

2110 | parity (S (S (j + j))) | Even = Even {n=S j}

2210 | parity (S (S (j + j))) | Even = Even {n=S j}

@@ -33,3 +34,4 @@ Specifically:

33 plus (S j) (S j)

34 plus (S j) (S j)

34 and

35 and

35 S (S (plus j j))

36 S (S (plus j j))

37+

test/unique004/expected+10

@@ -6,6 +6,7 @@ Type mismatch between

6 Int -> String

7and

8 UniqueType (Int -> String)

9+

9unique001a.idr:46:15-54:28:

10unique001a.idr:46:15-54:28:

10 |

11 |

1146 | showStuff' xs = do

1246 | showStuff' xs = do

@@ -14,6 +15,7 @@ Type mismatch between

14 Int -> String

15 Int -> String

15and

16and

16 UniqueType (Int -> String)

17 UniqueType (Int -> String)

18+

17unique001a.idr:57:15-62:33:

19unique001a.idr:57:15-62:33:

18 |

20 |

1957 | showThings xs = do

2157 | showThings xs = do

@@ -22,31 +24,37 @@ Type mismatch between

22 UniqueType (Int -> String)

24 UniqueType (Int -> String)

23and

25and

24 Int -> String

26 Int -> String

27+

25unique001b.idr:18:17-42:

28unique001b.idr:18:17-42:

26 |

29 |

2718 | showU (x :: xs) = show x ++ "," ++ free xs

3018 | showU (x :: xs) = show x ++ "," ++ free xs

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

31 | ~~~~~~~~~~~~~~~~~~~~~~~~~~

29Borrowed name xs must not be used on RHS

32Borrowed name xs must not be used on RHS

33+

30unique001c.idr:47:12-62:

34unique001c.idr:47:12-62:

31 |

35 |

3247 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)

3647 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)

33 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

37 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

34Unique name f is used more than once

38Unique name f is used more than once

39+

35unique001d.idr:4:16-18:

40unique001d.idr:4:16-18:

36 |

41 |

374 | steal (Read x) = x

424 | steal (Read x) = x

38 | ~~~

43 | ~~~

39Borrowed name x must not be used on RHS

44Borrowed name x must not be used on RHS

45+

40unique001e.idr:4:12-40:

46unique001e.idr:4:12-40:

41 |

47 |

424 | Nil : {a : UniqueType} -> BadList a

484 | Nil : {a : UniqueType} -> BadList a

43 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

44Constructor Main.Nil has a UniqueType, but the data type does not

50Constructor Main.Nil has a UniqueType, but the data type does not

51+

45unique002.idr:17:8-20:19:

52unique002.idr:17:8-20:19:

46 |

53 |

4717 | foo xs = do -- let f = \x : Int => showU xs

5417 | foo xs = do -- let f = \x : Int => showU xs

48 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

55 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

49Unique name xs is used more than once

56Unique name xs is used more than once

57+

50unique002a.idr:17:8-20:19:

58unique002a.idr:17:8-20:19:

51 |

59 |

5217 | foo xs = do let f = \x : Int => showU xs

6017 | foo xs = do let f = \x : Int => showU xs

@@ -55,6 +63,7 @@ Type mismatch between

55 Int -> String

63 Int -> String

56and

64and

57 UniqueType (Int -> String)

65 UniqueType (Int -> String)

66+

58unique003.idr:20:8-24:19:

67unique003.idr:20:8-24:19:

59 |

68 |

6020 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context

6920 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context

@@ -63,3 +72,4 @@ Type mismatch between

63 Int -> String

72 Int -> String

64and

73and

65 UniqueType (Int -> String)

74 UniqueType (Int -> String)

75+

test/universes001/expected+1

@@ -11,3 +11,4 @@ Universe inconsistency.

11 ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}

12 ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}

13 ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}

14+

test/universes002/expected+1

@@ -11,3 +11,4 @@ Universe inconsistency.

11 ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}

12 ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}

13 ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}

14+