f967817 · Idris-dev · git.iko.soy

src/Idris/Output.hs+35−5

compare with master

unifiedsplit

@@ -33,11 +33,12 @@ import Prelude hiding ((<$>))

33

34import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)

35import Data.List (intersperse, nub)

36−import Data.Maybe (fromMaybe)

36+import Data.Maybe (fromMaybe, fromJust, isJust, listToMaybe)

37import System.Console.Haskeline.MonadException (MonadException(controlIO),

38 RunIO(RunIO))

39import System.FilePath (replaceExtension)

40import System.IO (Handle, hPutStr, hPutStrLn)

41+import System.IO.Error (tryIOError)

41

42

42instance MonadException m => MonadException (ExceptT Err m) where

43instance MonadException m => MonadException (ExceptT Err m) where

43 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

44 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

@@ -49,15 +50,44 @@ pshow ist err = displayDecorated (consoleDecorate ist) .

49 renderPretty 1.0 80 .

50 renderPretty 1.0 80 .

50 fmap (fancifyAnnots ist True) $ pprintErr ist err

51 fmap (fancifyAnnots ist True) $ pprintErr ist err

51

52

53+formatWarning :: FC -> String -> Maybe String

54+formatWarning (FC fn (si, sj) (ei, ej)) src =

55+ if isJust sourceLine

56+ then Just (top ++ "\n" ++ formattedLine ++ "\n" ++ bottom)

57+ else Nothing

58+ where

59+ sourceLine = listToMaybe . drop (si - 1) . lines $ src

60+ formattedLine = show si ++ " | " ++ fromJust sourceLine

61+ top = take (length (show si)) (repeat ' ') ++ " |"

62+ indicator = case (si == ei, sj == ej) of

63+ (True , True ) -> "^"

64+ (True , False) -> squiggles (ej - sj + 1)

65+ (False, _ ) -> squiggles (length (fromJust sourceLine) - sj + 1) ++ " ..."

66+ bottom = top ++ " " ++ (take (sj - 1) (repeat ' ')) ++ indicator

67+ squiggles n = take n (repeat '~')

68+formatWarning _ _ = Nothing

69+

70+readSource :: FC -> Idris (Maybe String)

71+readSource (FC fn _ _) = do

72+ result <- runIO $ tryIOError (readFile fn)

73+ case result of

74+ Left _ -> pure Nothing

75+ Right v -> pure (Just v)

76+readSource _ = pure Nothing

77+

78+

52iWarn :: FC -> Doc OutputAnnotation -> Idris ()

79iWarn :: FC -> Doc OutputAnnotation -> Idris ()

53iWarn fc err =

80iWarn fc err =

54 do i <- getIState

81 do i <- getIState

55 case idris_outputmode i of

82 case idris_outputmode i of

56 RawOutput h ->

83 RawOutput h ->

84+ do maybeSource <- readSource fc

85+ let maybeFormattedSource = maybeSource >>= formatWarning fc

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

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

58− case fc of

87+ (case fc of

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

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

60− _ -> err

89+ _ -> err) <>

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

61 hWriteDoc h i err'

91 hWriteDoc h i err'

62 IdeMode n h ->

92 IdeMode n h ->

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

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

test/basic002/expected+6

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

1test006.idr:25:23-27:

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

3+ |

4+25 | Main.parity_lemma_2 = proof {

5+ | ~~~~~

3test006.idr:32:23-27:

6test006.idr:32:23-27:

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

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

8+ |

9+32 | Main.parity_lemma_1 = proof {

10+ | ~~~~~

5[False, True, False, True, False, True]

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

test/basic006/expected+3

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

6 Vect n a (Type of xs)

7 and

8 List a (Expected type)

9+ |

10+16 | foo xs = reverse xs

11+ | ~~~~~~~~~~

9[3, 2, 1]

12[3, 2, 1]

10"Number 42"

13"Number 42"

test/basic009/expected+9

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

1MAIN-PASS

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

3 Did you mean to refer to A.num?

4+ |

5+6 | fault : num = Z

6+ | ~~~

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

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

5 num = 0

8 num = 0

6

9

@@ -14,4 +17,10 @@ Specifically:

14 0

17 0

15 and

18 and

16 num

19 num

20+ |

21+7 | fault = Refl

22+ | ~~~~~~

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

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

24+ |

25+3 | import Data.Vect as X

26+ | ^

test/basic017/expected+3

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

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

2When checking an application of Main.Vect:

3 No such variable n

4+ |

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

6+ | ^

test/basic018/expected+9

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

1basic018.idr:7:12-16:

2thing is bound as an implicit

3 Did you mean to refer to Main.thing?

4+ |

5+7 | Vect thing elem

6+ | ~~~~~

4basic018.idr:12:8-12:

7basic018.idr:12:8-12:

5thing is bound as an implicit

8thing is bound as an implicit

6 Did you mean to refer to Main.thing?

9 Did you mean to refer to Main.thing?

10+ |

11+12 | test : thing = S 41

12+ | ~~~~~

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

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

8 thing = S 41

14 thing = S 41

9

15

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

17 42

23 42

18 and

24 and

19 thing

25 thing

26+ |

27+13 | test = Refl

28+ | ~~~~~~

test/directives001/expected+18

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

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

2To be replaced with `Bar`.

3+ |

4+14 | mkFoo : String -> Foo

5+ | ^

3directives001.idr:14:7:Use of deprecated name directives001.Foo

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

4To be replaced with `Bar`.

7To be replaced with `Bar`.

8+ |

9+14 | mkFoo : String -> Foo

10+ | ^

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

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

6To be replaced with `Bar`.

12To be replaced with `Bar`.

13+ |

14+15 | mkFoo = MkFoo

15+ | ~~~~~~~

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

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

8To be replaced with `Bar`.

17To be replaced with `Bar`.

18+ |

19+15 | mkFoo = MkFoo

20+ | ~~~~~~~

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

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

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

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

23+ |

24+26 | main = do

25+ | ~~~~ ...

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

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

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

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

28+ |

29+26 | main = do

30+ | ~~~~ ...

test/directives002/expected+3

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

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

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

3+ |

4+12 | main = do

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

test/effects003/expected+3

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

1hangman.idr:204:8-12:

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

3+ |

4+204 | wlen = proof search

5+ | ~~~~~

3------------

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

4

7

56 guesses left

86 guesses left

test/error001/expected+3

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

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

8 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,3 +3,6 @@ When checking right hand side of bad with expected type

3 Tm [] TUnit

4

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

6+ |

7+68 | bad = Lam (Var Here)

8+ | ~~~~~~~~~~~~~~~~

test/error004/expected+6

@@ -4,9 +4,15 @@ When checking right hand side of badCadr1 with expected type

4

5When checking argument cons2 to function FunErrTest.cadr:

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

7+ |

8+35 | badCadr1 = cadr []

9+ | ~~~~~~~

7FunErrTest.idr:38:12-19:

10FunErrTest.idr:38:12-19:

8When checking right hand side of badCadr2 with expected type

11When checking right hand side of badCadr2 with expected type

9 Int

12 Int

10

13

11When checking argument cons2 to function FunErrTest.cadr:

14When checking argument cons2 to function FunErrTest.cadr:

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

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

16+ |

17+38 | badCadr2 = cadr [1]

18+ | ~~~~~~~~

test/error005/expected+15

@@ -4,18 +4,27 @@ error005.idr:11:7:When checking right hand side of two with expected type

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

5 When using 2 as a literal for a Fin 2

6 2 is not strictly less than 2

7+ |

8+11 | two = 2

9+ | ^

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

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

8 Fin n

11 Fin n

9

12

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

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

11 When using 0 as a literal for a Fin n

14 When using 0 as a literal for a Fin n

12 0 is not strictly less than n

15 0 is not strictly less than n

16+ |

17+14 | hahaha n = 0

18+ | ^

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

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

14 Fin (plus 2 n)

20 Fin (plus 2 n)

15

21

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

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

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

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

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

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

25+ |

26+20 | notOk n = 2

27+ | ^

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

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

20 Fin 3

29 Fin 3

21

30

@@ -23,9 +32,15 @@ When checking argument prf to function Data.Fin.fromInteger:

23 When using n as a literal for a Fin 3

32 When using n as a literal for a Fin 3

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

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

25 variable instead of a constant Integer

34 variable instead of a constant Integer

35+ |

36+23 | b0rken n = fromInteger n

37+ | ~~~~~~~~~~~~~

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

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

27 Fin 4

39 Fin 4

28

40

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

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

30 When using 5 as a literal for a Fin 4

42 When using 5 as a literal for a Fin 4

31 5 is not strictly less than 4

43 5 is not strictly less than 4

44+ |

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

46+ | ^

test/error006/expected+3

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

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

2unexpected patterns outside of "with" block

3+ |

4+4 | foo 1 | 2 | 3 = True

5+ | ~~~~~~~~~~~~~

test/error007/expected+3

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

13 Bits32

14 and

15 Int

16+ |

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

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

test/error008/expected+6

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

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

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

3+ |

4+3 | s2 : x + sum Nil = x * fromInteger 0

5+ | ^

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

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

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

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

8+ |

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

10+ | ^

test/ffi002/expected+3

@@ -1 +1,4 @@

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

2+ |

3+20 | %provide (t : Type) with badProvider

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

test/interfaces008/expected+3

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

1interfaces008.idr:20:18-23:

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

3+ |

4+20 | implementation Foo2 a where

5+ | ~~~~~~

test/layout001/expected+3

@@ -63,6 +63,9 @@ mplus1.idr:13:31-17:49:When checking right hand side of term with expected type

63

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

65 No such variable f

66+ |

67+13 | term = do f <- factor

68+ | ~~~~~~~~~~~~~~~~~ ...

66./mplus2.idr:17:37:

69./mplus2.idr:17:37:

67 |

70 |

6817 | `mplus` pure f

7117 | `mplus` pure f

test/literate001/expected+3

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

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

2+ |

3+1 | Broken

4+ | ^

2'a'

5'a'

3'd'

6'd'

4zabcdefg

7zabcdefg

test/meta002/expected+9

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

1DataDef.idr:74:1-8:

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

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

4+ |

5+74 | %runElab nope

6+ | ~~~~~~~~

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

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

5When checking right hand side of testElab3 with expected type

8When checking right hand side of testElab3 with expected type

6 DPair Ty (Tm [])

9 DPair Ty (Tm [])

7

10

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

11Unifying 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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

9AgdaStyleReflection.idr:315:5-20:

15AgdaStyleReflection.idr:315:5-20:

10When checking right hand side of baz with expected type

16When checking right hand side of baz with expected type

11 (Nat, Void)

17 (Nat, Void)

12

18

13PROOF SEARCH FAILURE is not defined.

19PROOF SEARCH FAILURE is not defined.

20+ |

21+315 | baz = tactic trivial

22+ | ~~~~~~~~~~~~~~~~

test/meta003/expected+3

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

4 ()

5and

6 String

7+ |

8+14 | %runElab mkBadDef1

9+ | ~~~~~~~~

test/meta004/expected+3

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

1meta004.idr:50:1-8:

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

3Not an impossible case

4+ |

5+50 | %runElab domore

6+ | ~~~~~~~~

test/proof001/expected+6

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

1test029.idr:29:25-29:

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

3+ |

4+29 | simple.append_lemma_2 = proof {

5+ | ~~~~~

3test029.idr:36:25-29:

6test029.idr:36:25-29:

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

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

8+ |

9+36 | simple.append_lemma_1 = proof {

10+ | ~~~~~

test/proof002/expected+12

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

1Reflect.idr:175:21-25:

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

3+ |

4+175 | Reflect.appRExpr1 = proof {

5+ | ~~~~~

3Reflect.idr:184:21-25:

6Reflect.idr:184:21-25:

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

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

8+ |

9+184 | Reflect.appRExpr2 = proof {

10+ | ~~~~~

5Reflect.idr:192:15-19:

11Reflect.idr:192:15-19:

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

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

13+ |

14+192 | Reflect.bp1 = proof {

15+ | ~~~~~

7test030a.idr:12:26-37:

16test030a.idr:12:26-37:

8When checking right hand side of testReflect1 with expected type

17When checking right hand side of testReflect1 with expected type

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

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

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

19 Just x

28 Just x

20 and

29 and

21 Nothing

30 Nothing

31+ |

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

33+ | ~~~~~~~~~~~~

test/proof003/expected+18

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

1Parity.idr:17:18-22:

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

3+ |

4+17 | parity_lemma_2 = proof {

5+ | ~~~~~

3Parity.idr:24:18-22:

6Parity.idr:24:18-22:

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

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

8+ |

9+24 | parity_lemma_1 = proof {

10+ | ~~~~~

5test015.idr:88:15-19:

11test015.idr:88:15-19:

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

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

13+ |

14+88 | Main.ntbOdd = proof {

15+ | ~~~~~

7test015.idr:97:16-20:

16test015.idr:97:16-20:

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

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

18+ |

19+97 | Main.ntbEven = proof {

20+ | ~~~~~

9test015.idr:107:20-24:

21test015.idr:107:20-24:

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

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

23+ |

24+107 | Main.adc_lemma_2 = proof {

25+ | ~~~~~

11test015.idr:142:20-24:

26test015.idr:142:20-24:

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

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

28+ |

29+142 | Main.adc_lemma_1 = proof {

30+ | ~~~~~

1300101010

3100101010

1401011001

3201011001

15010000011

33010000011

test/proof007/expected+3

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

4

5When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

6 No such variable sadgjhsag

7+ |

8+9 | test = funWithBadDefArg

9+ | ~~~~~~~~~~~~~~~~~~

test/proof008/expected+3

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

1ClaimAndUnfocus.idr:8:27-31:

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

3+ |

4+8 | ClaimAndUnfocus.foo_rhs = proof

5+ | ~~~~~

test/proof011/expected+6

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

8 x ::

9 (xs ++ ys) ++

10 zs

11+ |

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

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

11proof011a.idr:14:5-37:

14proof011a.idr:14:5-37:

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

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

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

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

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

18 x ::

21 x ::

19 (xs ++ ys) ++

22 (xs ++ ys) ++

20 zs

23 zs

24+ |

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

26+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

test/quasiquote003/expected+3

@@ -2,3 +2,6 @@ NoInfer.idr:11:5-11:When checking right hand side of zzz with expected type

2 TT

3

4No such variable k

5+ |

6+11 | zzz = `(FZ)

7+ | ~~~~~~~

test/quasiquote004/expected+12

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

1Quasiquote004.idr:39:26-30:

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

3+ |

4+39 | Quasiquote004.getMeNat = proof

5+ | ~~~~~

3Quasiquote004.idr:42:28-32:

6Quasiquote004.idr:42:28-32:

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

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

8+ |

9+42 | Quasiquote004.fizzyIsAOK = proof

10+ | ~~~~~

5Quasiquote004.idr:50:27-31:

11Quasiquote004.idr:50:27-31:

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

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

13+ |

14+50 | Quasiquote004.getMeNat' = proof

15+ | ~~~~~

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

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

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

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

9 String

18 String

10

19

11Not a Nat goal

20Not a Nat goal

21+ |

22+50 | Quasiquote004.getMeNat' = proof

23+ | ~~~~~~~ ...

test/quasiquote006/expected+9

@@ -4,11 +4,17 @@ When checking right hand side of b with expected type

4

5Can't disambiguate name: ForeignEnv.Nil,

6 Prelude.List.Nil

7+ |

8+9 | b = `{Nil}

9+ | ~~~~~~~~

7quasiquote006.idr:12:3-17:

10quasiquote006.idr:12:3-17:

8When checking right hand side of c with expected type

11When checking right hand side of c with expected type

9 TTName

12 TTName

10

13

11No such variable alsdkjflkj

14No such variable alsdkjflkj

15+ |

16+12 | c = `{alsdkjflkj}

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

12quasiquote006.idr:15:3-11:

18quasiquote006.idr:15:3-11:

13When checking right hand side of d with expected type

19When checking right hand side of d with expected type

14 TTName

20 TTName

@@ -16,4 +22,7 @@ When checking right hand side of d with expected type

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

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

17 Prelude.List.::,

23 Prelude.List.::,

18 Prelude.Stream.::

24 Prelude.Stream.::

25+ |

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

27+ | ~~~~~~~~~

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

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

test/reg017/expected+6

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

1reg017.idr:5:17-23:

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

3+ |

4+5 | { default tactics { refine Refl; solve; } prfA : a = a } ->

5+ | ~~~~~~~

3reg017.idr:8:17-23:

6reg017.idr:8:17-23:

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

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

8+ |

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

10+ | ~~~~~~~

54

114

test/reg027/expected+3

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

1<<int fn>>

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

3+ |

4+9 | implementation Show (Int -> b) where

5+ | ~~~~~~~~~~~~~~~

test/regression002/expected+129

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

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

2No such variable OddList

3+ |

4+4 | ECons : Nat -> OddList -> EvenList

5+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

4No such variable EvenList

7No such variable EvenList

8+ |

9+7 | OCons : Nat -> EvenList -> OddList

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

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

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

6No such variable EvenList

12No such variable EvenList

13+ |

14+9 | test : EvenList

15+ | ^

7reg006.idr:17:1-23:

16reg006.idr:17:1-23:

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

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

18+ |

19+17 | lookup k Leaf = Nothing

20+ | ~~~~~~~~~~~~~~~~~~~~~~~

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

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

22+ |

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

24+ | ~~~~~~~~~~~

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

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

11 0 = 1

26 0 = 1

12

27

@@ -20,20 +35,44 @@ Specifically:

20 1

35 1

21 and

36 and

22 0

37 0

38+ |

39+12 | > hurrah = isSame

40+ | ~~~~~~

23reg010.idr:5:3-26:

41reg010.idr:5:3-26:

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

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

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

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

44+ |

45+5 | unsafeSubst P x x px | _ = px

46+ | ~~~~~~~~~~~~~~~~~~~~~~~~

26reg018a.idr:16:1-18:

47reg018a.idr:16:1-18:

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

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

49+ |

50+16 | minusCoNat Z n = Z

51+ | ~~~~~~~~~~~~~~~~~~

28reg018a.idr:21:1-42:

52reg018a.idr:21:1-42:

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

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

54+ |

55+21 | loopForever = minusCoNat infinity infinity

56+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

30reg018b.idr:8:1-28:

57reg018b.idr:8:1-28:

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

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

59+ |

60+8 | showB (I x) = "I" ++ showB x

61+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

32reg018b.idr:11:1-6:

62reg018b.idr:11:1-6:

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

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

64+ |

65+11 | Show B where show = showB

66+ | ~~~~~~

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

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

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

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

69+ |

70+21 | inf (x :: xs) with (hdtl xs)

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

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

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

73+ |

74+8 | pull {n=Z} _ (x :: xs) = (x, xs)

75+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

38 f Nat

77 f Nat

39

78

@@ -41,18 +80,42 @@ Type mismatch between

41 Nat (Type of 0)

80 Nat (Type of 0)

42and

81and

43 f Nat (Expected type)

82 f Nat (Expected type)

83+ |

84+7 | bad = Z

85+ | ~~~

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

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

87+ |

88+5 | bad Z = Z

89+ | ~~~~~~~~~

45reg028a.idr:17:14-18:

90reg028a.idr:17:14-18:

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

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

92+ |

93+17 | qsortLemma = proof

94+ | ~~~~~

47reg028a.idr:11:1-14:

95reg028a.idr:11:1-14:

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

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

97+ |

98+11 | qsort' [] = []

99+ | ~~~~~~~~~~~~~~

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

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

50Can't match on bar xs xs Refl

101Can't match on bar xs xs Refl

102+ |

103+6 | bar xs xs Refl = Refl

104+ | ~~~~~~~~~~~~~~

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

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

52Can't match on foo f x x Refl

106Can't match on foo f x x Refl

107+ |

108+9 | foo f x x Refl = Refl

109+ | ~~~~~~~~~~~~~~

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

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

111+ |

112+8 | fins Z = ([] ** (finZEmpty {a=_}))

113+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~

54reg044.idr:4:6-10:

114reg044.idr:4:6-10:

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

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

116+ |

117+4 | pf = proof

118+ | ~~~~~

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

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

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

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

58

121

@@ -66,12 +129,21 @@ Specifically:

66 b

129 b

67 and

130 and

68 a

131 a

132+ |

133+4 | pf = proof

134+ | ~~~~~~~ ...

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

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

70Void is not Main.Foo

136Void is not Main.Foo

137+ |

138+2 | Bogus : Void

139+ | ~~~~

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

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

72 Void

141 Void

73

142

74No such variable Bogus

143No such variable Bogus

144+ |

145+5 | uhOh = Bogus

146+ | ~~~~~~~

75./badbangop.idr:7:1:

147./badbangop.idr:7:1:

76 |

148 |

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

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

@@ -87,39 +159,87 @@ unexpected Operator without known fixity: !!

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

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

88When checking an application of constructor Main.MkInfer:

160When checking an application of constructor Main.MkInfer:

89 Attempting concrete match on polymorphic argument: 0

161 Attempting concrete match on polymorphic argument: 0

162+ |

163+18 | inf (MkInfer _ Z) = True

164+ | ~~~~~~~~~~~~~~~~~

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

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

91No explicit types on left hand side: Char

166No explicit types on left hand side: Char

167+ |

168+34 | weird {x = Char} y = '5'

169+ | ~~~~~~~~~~~~~~~~~~

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

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

93No explicit types on left hand side: Nat

171No explicit types on left hand side: Nat

172+ |

173+37 | weird' {x = Prelude.Nat.Nat} y = Z

174+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

95When checking an application of Main.tctrick:

176When checking an application of Main.tctrick:

96 Type mismatch between

177 Type mismatch between

97 Maybe a1 (Type of Just x)

178 Maybe a1 (Type of Just x)

98 and

179 and

99 a (Expected type)

180 a (Expected type)

181+ |

182+40 | tctrick (Just x) = x

183+ | ~~~~~~~

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

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

101Can't match on g (f 0)

185Can't match on g (f 0)

186+ |

187+5 | g (f Z) = 1

188+ | ~~~~~~~

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

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

103Can't match on h x x

190Can't match on h x x

191+ |

192+8 | h x x = x

193+ | ~~~~~

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

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

105When checking an application of constructor Foo.CAny:

195When checking an application of constructor Foo.CAny:

106 Attempting concrete match on polymorphic argument: Nothing

196 Attempting concrete match on polymorphic argument: Nothing

197+ |

198+8 | foo (CAny Nothing) = 42

199+ | ~~~~~~~~~~~~~~~~~~

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

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

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

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

202+ |

203+13 | apply (\x => \y => x) a = a

204+ | ~~~~~~~~~~~~~~~~~~~~~~~

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

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

206+ |

207+7 | dodgy n m Refl impossible

208+ | ~~~~~~~~~~

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

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

210+ |

211+10 | nonk Refl impossible

212+ | ~~~~~~~~~~

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

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

112This is likely to lead to problems!

214This is likely to lead to problems!

215+ |

216+1 | data nat : Type where --error

217+ | ~~~

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

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

114This is likely to lead to problems!

219This is likely to lead to problems!

220+ |

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

222+ | ~~~

115reg068.idr:2:8-10:

223reg068.idr:2:8-10:

116nat is bound as an implicit

224nat is bound as an implicit

117 Did you mean to refer to Main.nat?

225 Did you mean to refer to Main.nat?

226+ |

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

228+ | ~~~

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

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

119Type level variable nat is not Main.nat

230Type level variable nat is not Main.nat

231+ |

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

233+ | ~~~

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

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

235+ |

236+11 | natexp k = S (natfn k)

237+ | ~~~~~~~~~~~~~~~~~~~~~~

121reg070.idr:7:1-7:

238reg070.idr:7:1-7:

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

239Test_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+ |

241+7 | Show Te where

242+ | ~~~~~~~

123./reg076.idr:8:1:

243./reg076.idr:8:1:

124 |

244 |

1258 | <empty line>

2458 | <empty line>

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

147 -0.0

267 -0.0

148 and

268 and

149 0.0

269 0.0

270+ |

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

272+ | ~~~~~~~~~~~~~~~~~~~~~

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

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

274+ |

275+9 | f Nil = 0

276+ | ~~~~~~~~~

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

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

278+ |

279+12 | NaN = f (Cons 0 Nil)

280+ | ~~~~~~~~~~~~~~~~~~~~

test/sourceLocation001/expected+12

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

1SourceLoc.idr:12:19-25:

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

3+ |

4+12 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

5+ | ~~~~~~~

3SourceLoc.idr:21:19-23:

6SourceLoc.idr:21:19-23:

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

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

8+ |

9+21 | fromProofScript = proof sourceLocation

10+ | ~~~~~

5SourceLoc.idr:41:20-26:

11SourceLoc.idr:41:20-26:

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

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

13+ |

14+41 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

15+ | ~~~~~~~

7SourceLoc.idr:99:18-22:

16SourceLoc.idr:99:18-22:

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

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

18+ |

19+99 | SourceLoc.meta = proof

20+ | ~~~~~

9Testing using definition

21Testing using definition

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

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

11Testing using inline tactics

23Testing using inline tactics

test/syntax001/expected+6

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

6 String (Type of "argh")

7 and

8 Nat (Expected type)

9+ |

10+6 | foo = fnord "argh"

11+ | ~~~~~~~~~~~~

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

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

10 Nat

13 Nat

11

14

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

14 String (Type of "argh")

17 String (Type of "argh")

15 and

18 and

16 Nat (Expected type)

19 Nat (Expected type)

20+ |

21+5 | foo = fnord "argh"

22+ | ~~~~~~~~~~~~

test/totality001/expected+9

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

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

2+ |

3+15 | foo (MkBad f i) = f (MkBad' i)

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

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

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

6+ |

7+9 | bar = MkBad (\x => 3) 3

8+ | ~~~~~~~~~~~~~~~~~~~~~~~

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

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

10+ |

11+9 | bar = MkBad (\x => 3) 3

12+ | ~~~~~~~~~~~~~~~~~~~~~~~

test/totality002/expected+9

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

1test017.idr:94:26-30:

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

3+ |

4+94 | maxCommutativeStepCase = proof {

5+ | ~~~~~

3test017a.idr:7:1-24:

6test017a.idr:7:1-24:

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

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

8+ |

9+7 | vtrans [] _ = []

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

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

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

12+ |

13+4 | foo = foo

14+ | ~~~~~~~~~

test/totality003/expected+3

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

1totality003a.idr:5:1-13:

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

3+ |

4+5 | qsort [] = []

5+ | ~~~~~~~~~~~~~

test/totality004/expected+6

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

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

2totality004a.idr:13:1-44:

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

4+ |

5+13 | process (Get f) (x :: xs) = process (f x) xs

6+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

8+ |

9+24 | main = printLn (take 10 (process doubleInt (countStream 1)))

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

test/totality006/expected+9

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

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

2+ |

3+8 | prf Z Z Oh impossible

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

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

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

6+ |

7+11 | prf' (S _) (S _) Oh impossible

8+ | ~~~~~~~~~~

3totality006b.idr:10:1-34:

9totality006b.idr:10:1-34:

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

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

11+ |

12+10 | blargh [] (y :: xs) so = absurd so

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

test/totality007/expected+3

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

1Entering directory `./src'

2Totality.idr:4:1-9:

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

4+ |

5+4 | foo Z = Z

6+ | ~~~~~~~~~

4Totality.idr:4:1-9:Could not build: 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

5Leaving directory `./src'

8Leaving directory `./src'

test/totality008/expected+3

@@ -1 +1,4 @@

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

2+ |

3+7 | ElimT _ C1 = 3

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

test/totality009/expected+30

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

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

2+ |

3+9 | wrongPossible = (\Flase impossible)

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

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

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

6+ |

7+9 | wrongPossible = (\Flase impossible)

8+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

10+ |

11+12 | wrongPossible' x = case x of

12+ | ^

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

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

14+ |

15+12 | wrongPossible' x = case x of

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

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

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

18+ |

19+9 | wrongPossible = (\Flase impossible)

20+ | ~~~~~~~~~~~~~~~~~~~~~

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

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

22+ |

23+9 | wrongPossible = (\Flase impossible)

24+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

26+ |

27+12 | wrongPossible' x = case x of

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

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

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

30+ |

31+12 | wrongPossible' x = case x of

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

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

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

34+ |

35+10 | wrongPossible = (\Flase impossible)

36+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

38+ |

39+14 | wrongPossible' x = case x of

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

test/totality010/expected+6

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

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

2+ |

3+27 | evenNotS MkEven ZeroEven impossible

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

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

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

6+ |

7+30 | bad = evenNotS ZeroEven $ MkBad ZeroEven

8+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

test/totality011/expected+3

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

1totality011.lidr:22:3-57:

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

3+ |

4+22 | > weCanOnlyGetOlder {t'' = Z} {t = Z} _ _ _ = LTEZero

5+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

test/totality012/expected+6

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

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

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

3+ |

4+9 | echo2 x = if (x == "quit") then PutStr "Bye!\n"

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

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

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

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

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

8+ |

9+11 | echo = do PutStr "$ "

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

test/totality013/expected+6

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

1totality013a.idr:5:3-49:

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

3+ |

4+5 | foo order x xs y ys _ = mtot order (x :: xs) ys

5+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

7+ |

8+9 | mtot order [] right = right

9+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

test/totality014/expected+3

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

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

8 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+9

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

1totality015a.idr:52:3-53:

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

3+ |

4+52 | quiz (num1 :: num2 :: nums) score = quiz nums score

5+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

7+ |

8+42 | correct nums score

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

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

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

11+ |

12+47 | wrong nums ans score

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

test/totality016/expected+27

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

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

2+ |

3+15 | f1 (MkTP T1 x) = True

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

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

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

6+ |

7+19 | f2 (MkTP T1 x, _) = True

8+ | ~~~~~~~~~~~~~~~~~~~~~~~~

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

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

10+ |

11+23 | f3 ((MkTP T1 x, _), _) = True

12+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

14+ |

15+27 | g1 T1 x = True

16+ | ~~~~~~~~~~~~~~

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

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

18+ |

19+31 | g2 (T1, x) = True

20+ | ~~~~~~~~~~~~~~~~~

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

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

22+ |

23+35 | h1 True x = True

24+ | ~~~~~~~~~~~~~~~~

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

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

26+ |

27+39 | h2 (True, x) = True

28+ | ~~~~~~~~~~~~~~~~~~~

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

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

30+ |

31+43 | h3 (MkTP2 (T1, x)) = True

32+ | ~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

34+ |

35+47 | h4 (MkTP2 (T1, x), _) _ = True

36+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

test/totality017/expected+18

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

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

2+ |

3+19 | g1 T1 T1 = True

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

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

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

6+ |

7+25 | g2 T1' T1' = True

8+ | ~~~~~~~~~~~~~~~~~

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

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

10+ |

11+31 | g3 T1' = True

12+ | ~~~~~~~~~~~~~

4totality017.idr:37:1-36:Main.g4 is not total as there are missing cases

13totality017.idr:37:1-36:Main.g4 is not total as there are missing cases

14+ |

15+37 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True

16+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5totality017.idr:42:1-11:Main.f' is not total as there are missing cases

17totality017.idr:42:1-11:Main.f' is not total as there are missing cases

18+ |

19+42 | f' 0 = True

20+ | ~~~~~~~~~~~

6totality017.idr:47:1-17:Main.f is not total as there are missing cases

21totality017.idr:47:1-17:Main.f is not total as there are missing cases

22+ |

23+47 | f (MkPP 0) = True

24+ | ~~~~~~~~~~~~~~~~~

test/totality018/expected+3

@@ -1 +1,4 @@

1totality018.idr:12:1-10:Main.bar is not total as there are missing cases

2+ |

3+12 | bar FZ = 0

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

test/totality019/expected+6

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

1totality019.idr:8:1-36:Main.testCov is not total as there are missing cases

2+ |

3+8 | testCov False False = ?testCov_rhs_3

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

2totality019.idr:12:1-42:Main.testCov' is not total as there are missing cases

5totality019.idr:12:1-42:Main.testCov' is not total as there are missing cases

6+ |

7+12 | testCov' (False ** False) = ?testCov_rhs_3

8+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

test/totality020/expected+6

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

1totality020.idr:4:14-23:bug _ _ Refl is a valid case

2+ |

3+4 | bug _ _ Refl impossible

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

2totality020.idr:7:14-23:foo a b Refl is a valid case

5totality020.idr:7:14-23:foo a b Refl is a valid case

6+ |

7+7 | foo a b Refl impossible

8+ | ~~~~~~~~~~

test/totality021/expected+15

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

1totality021.idr:8:1-67:

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

3+ |

4+8 | sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl

5+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

3totality021.idr:12:1-66:

6totality021.idr:12:1-66:

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

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

8+ |

9+12 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl

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

5totality021.idr:18:1-26:

11totality021.idr:18:1-26:

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

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

13+ |

14+18 | v = sLevelNotSLevel l Refl

15+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~

7totality021a.idr:9:1-37:

16totality021a.idr:9:1-37:

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

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

18+ |

19+9 | noNonEmptyPointInt {n} Nil impossible

20+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

9totality021a.idr:12:1-31:

21totality021a.idr:12:1-31:

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

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

23+ |

24+12 | myVoid = noNonEmptyPointInt [2]

25+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

test/totality022/expected+3

@@ -1 +1,4 @@

1totality022.idr:7:20-29:f _ [] (RSnoc _ _) is a valid case

2+ |

3+7 | f _ [] (RSnoc _ _) impossible -- = ?wat

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

test/totality023/expected+3

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

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

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

3+ |

4+9 | run (Do x f) = do r <- x

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

test/tutorial002/expected+9

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

1tutorial002.idr:41:25-29:

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

3+ |

4+41 | Main.natToBin_lemma_1 = proof

5+ | ~~~~~

3tutorial002.idr:48:18-22:

6tutorial002.idr:48:18-22:

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

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

8+ |

9+48 | parity_lemma_1 = proof

10+ | ~~~~~

5tutorial002.idr:54:18-22:

11tutorial002.idr:54:18-22:

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

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

13+ |

14+54 | parity_lemma_2 = proof {

15+ | ~~~~~

test/tutorial004/expected+6

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

1tutorial004.idr:46:14-18:

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

3+ |

4+46 | plusredZ_S = proof {

5+ | ~~~~~

3tutorial004.idr:53:14-18:

6tutorial004.idr:53:14-18:

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

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

8+ |

9+53 | plusredZ_Z = proof {

10+ | ~~~~~

test/tutorial006/expected+6

@@ -13,6 +13,9 @@ When checking argument xs to constructor Data.Vect.:::

13 plus len len

14 and

15 plus len m

16+ |

17+5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN

18+ | ~~

16tutorial006b.idr:10:37-50:

19tutorial006b.idr:10:37-50:

17When checking right hand side of with block in Main.parity with expected type

20When checking right hand side of with block in Main.parity with expected type

18 Parity (S (S (j + j)))

21 Parity (S (S (j + j)))

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

27 plus (S j) (S j)

30 plus (S j) (S j)

28 and

31 and

29 S (S (plus j j))

32 S (S (plus j j))

33+ |

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

35+ | ~~~~~~~~~~~~~~

test/unique004/expected+30

@@ -2,25 +2,55 @@ unique001a.idr:35:14-43:50:Type mismatch between

2 Int -> String

3and

4 UniqueType (Int -> String)

5+ |

6+35 | showStuff xs = do

7+ | ~~~~ ...

5unique001a.idr:46:15-54:28:Type mismatch between

8unique001a.idr:46:15-54:28:Type mismatch between

6 Int -> String

9 Int -> String

7and

10and

8 UniqueType (Int -> String)

11 UniqueType (Int -> String)

12+ |

13+46 | showStuff' xs = do

14+ | ~~~~ ...

9unique001a.idr:57:15-62:33:Type mismatch between

15unique001a.idr:57:15-62:33:Type mismatch between

10 UniqueType (Int -> String)

16 UniqueType (Int -> String)

11and

17and

12 Int -> String

18 Int -> String

19+ |

20+57 | showThings xs = do

21+ | ~~~~ ...

13unique001b.idr:18:17-42:Borrowed name xs must not be used on RHS

22unique001b.idr:18:17-42:Borrowed name xs must not be used on RHS

23+ |

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

25+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~

14unique001c.idr:47:12-62:Unique name f is used more than once

26unique001c.idr:47:12-62:Unique name f is used more than once

27+ |

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

29+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

15unique001d.idr:4:16-18:Borrowed name x must not be used on RHS

30unique001d.idr:4:16-18:Borrowed name x must not be used on RHS

31+ |

32+4 | steal (Read x) = x

33+ | ~~~

16unique001e.idr:4:12-40:

34unique001e.idr:4:12-40:

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

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

36+ |

37+4 | Nil : {a : UniqueType} -> BadList a

38+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

18unique002.idr:17:8-20:19:Unique name xs is used more than once

39unique002.idr:17:8-20:19:Unique name xs is used more than once

40+ |

41+17 | foo xs = do -- let f = \x : Int => showU xs

42+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

19unique002a.idr:17:8-20:19:Type mismatch between

43unique002a.idr:17:8-20:19:Type mismatch between

20 Int -> String

44 Int -> String

21and

45and

22 UniqueType (Int -> String)

46 UniqueType (Int -> String)

47+ |

48+17 | foo xs = do let f = \x : Int => showU xs

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

23unique003.idr:20:8-24:19:Type mismatch between

50unique003.idr:20:8-24:19:Type mismatch between

24 Int -> String

51 Int -> String

25and

52and

26 UniqueType (Int -> String)

53 UniqueType (Int -> String)

54+ |

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

56+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

test/universes001/expected+3

@@ -7,3 +7,6 @@ universes001.idr:7:5-21:Universe inconsistency.

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

9 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+3

@@ -7,3 +7,6 @@ universes002.idr:45:9-48:Universe inconsistency.

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

9 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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~