git.iko.soy/Idris-dev
on master help sign in
Make warnings, non-parse errors pretty
commitf967817d5b8281ea4c7ff261efc68c9b3753915a authorJason Felice <jason.m.felice@gmail.com> dateTue 5 Dec 2017, 14:32 (9 years ago) parent5218727
65 files changed+626−5
compare with master
unifiedsplit
src/Idris/Output.hs+35−5 test/basic002/expected+6 test/basic006/expected+3 test/basic009/expected+9 test/basic017/expected+3 test/basic018/expected+9 test/directives001/expected+18 test/directives002/expected+3 test/effects003/expected+3 test/error001/expected+3 test/error003/expected+3 test/error004/expected+6 test/error005/expected+15 test/error006/expected+3 test/error007/expected+3 test/error008/expected+6 test/ffi002/expected+3 test/interfaces008/expected+3 test/layout001/expected+3 test/literate001/expected+3 test/meta002/expected+9 test/meta003/expected+3 test/meta004/expected+3 test/proof001/expected+6 test/proof002/expected+12 test/proof003/expected+18 test/proof007/expected+3 test/proof008/expected+3 test/proof011/expected+6 test/quasiquote003/expected+3 test/quasiquote004/expected+12 test/quasiquote006/expected+9 test/reg017/expected+6 test/reg027/expected+3 test/regression002/expected+129 test/sourceLocation001/expected+12 test/syntax001/expected+6 test/totality001/expected+9 test/totality002/expected+9 test/totality003/expected+3 test/totality004/expected+6 test/totality006/expected+9 test/totality007/expected+3 test/totality008/expected+3 test/totality009/expected+30 test/totality010/expected+6 test/totality011/expected+3 test/totality012/expected+6 test/totality013/expected+6 test/totality014/expected+3 test/totality015/expected+9 test/totality016/expected+27 test/totality017/expected+18 test/totality018/expected+3 test/totality019/expected+6 test/totality020/expected+6 test/totality021/expected+15 test/totality022/expected+3 test/totality023/expected+3 test/tutorial002/expected+9 test/tutorial004/expected+6 test/tutorial006/expected+6 test/unique004/expected+30 test/universes001/expected+3 test/universes002/expected+3
src/Idris/Output.hs+35−5
@@ -33,11 +33,12 @@ import Prelude hiding ((<$>))
3333
3434import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
3535import Data.List (intersperse, nub)
36−import Data.Maybe (fromMaybe)
36+import Data.Maybe (fromMaybe, fromJust, isJust, listToMaybe)
3737import System.Console.Haskeline.MonadException (MonadException(controlIO),
3838 RunIO(RunIO))
3939import System.FilePath (replaceExtension)
4040import System.IO (Handle, hPutStr, hPutStrLn)
41+import System.IO.Error (tryIOError)
4142
4243instance MonadException m => MonadException (ExceptT Err m) where
4344 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
@@ -49,15 +50,44 @@ pshow ist err = displayDecorated (consoleDecorate ist) .
4950 renderPretty 1.0 80 .
5051 fmap (fancifyAnnots ist True) $ pprintErr ist err
5152
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+
5279iWarn :: FC -> Doc OutputAnnotation -> Idris ()
5380iWarn fc err =
5481 do i <- getIState
5582 case idris_outputmode i of
5683 RawOutput h ->
57− do err' <- iRender . fmap (fancifyAnnots i True) $
58− case fc of
59− FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err
60− _ -> err
84+ do maybeSource <- readSource fc
85+ let maybeFormattedSource = maybeSource >>= formatWarning fc
86+ err' <- iRender . fmap (fancifyAnnots i True) $
87+ (case fc of
88+ FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err
89+ _ -> err) <>
90+ string (maybe "" ("\n" ++) maybeFormattedSource)
6191 hWriteDoc h i err'
6292 IdeMode n h ->
6393 do err' <- iRender . fmap (fancifyAnnots i True) $ err
test/basic002/expected+6
@@ -1,5 +1,11 @@
11test006.idr:25:23-27:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+25 | Main.parity_lemma_2 = proof {
5+ | ~~~~~
36test006.idr:32:23-27:
47This style of tactic proof is deprecated. See %runElab for the replacement.
8+ |
9+32 | Main.parity_lemma_1 = proof {
10+ | ~~~~~
511[False, True, False, True, False, True]
test/basic006/expected+3
@@ -6,5 +6,8 @@ When checking an application of function Prelude.List.reverse:
66 Vect n a (Type of xs)
77 and
88 List a (Expected type)
9+ |
10+16 | foo xs = reverse xs
11+ | ~~~~~~~~~~
912[3, 2, 1]
1013"Number 42"
test/basic009/expected+9
@@ -1,6 +1,9 @@
11MAIN-PASS
22Faulty.idr:6:9-11:num is bound as an implicit
33 Did you mean to refer to A.num?
4+ |
5+6 | fault : num = Z
6+ | ~~~
47Faulty.idr:7:7-12:When checking right hand side of fault with expected type
58 num = 0
69
@@ -14,4 +17,10 @@ Specifically:
1417 0
1518 and
1619 num
20+ |
21+7 | fault = Refl
22+ | ~~~~~~
1723Multiple.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 @@
11basic017a.idr:11:8:When checking type of Main.append:
22When checking an application of Main.Vect:
33 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 @@
11basic018.idr:7:12-16:
22thing is bound as an implicit
33 Did you mean to refer to Main.thing?
4+ |
5+7 | Vect thing elem
6+ | ~~~~~
47basic018.idr:12:8-12:
58thing is bound as an implicit
69 Did you mean to refer to Main.thing?
10+ |
11+12 | test : thing = S 41
12+ | ~~~~~
713basic018.idr:13:6-11:When checking right hand side of test with expected type
814 thing = S 41
915
@@ -17,3 +23,6 @@ Specifically:
1723 42
1824 and
1925 thing
26+ |
27+13 | test = Refl
28+ | ~~~~~~
test/directives001/expected+18
@@ -1,12 +1,30 @@
11directives001.idr:14:7:Use of deprecated name directives001.Foo
22To be replaced with `Bar`.
3+ |
4+14 | mkFoo : String -> Foo
5+ | ^
36directives001.idr:14:7:Use of deprecated name directives001.Foo
47To be replaced with `Bar`.
8+ |
9+14 | mkFoo : String -> Foo
10+ | ^
511directives001.idr:15:7-13:Use of deprecated name directives001.Foo
612To be replaced with `Bar`.
13+ |
14+15 | mkFoo = MkFoo
15+ | ~~~~~~~
716directives001.idr:15:7-13:Use of deprecated name directives001.Foo
817To be replaced with `Bar`.
18+ |
19+15 | mkFoo = MkFoo
20+ | ~~~~~~~
921directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar
1022How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
23+ |
24+26 | main = do
25+ | ~~~~ ...
1126directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar
1227How `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 @@
11directives002.idr:12:3-14:28:
22directives002.Main.main is possibly not total due to: directives002.loop
3+ |
4+12 | main = do
5+ | ~~~~~~~~~ ...
test/effects003/expected+3
@@ -1,5 +1,8 @@
11hangman.idr:204:8-12:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+204 | wlen = proof search
5+ | ~~~~~
36------------
47
586 guesses left
test/error001/expected+3
@@ -6,3 +6,6 @@ test002.idr:1:6:Universe inconsistency.
66 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
77 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}
88 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
33 Tm [] TUnit
44
55DSL 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
44
55When checking argument cons2 to function FunErrTest.cadr:
66 Could not prove that [] has at least two elements.
7+ |
8+35 | badCadr1 = cadr []
9+ | ~~~~~~~
710FunErrTest.idr:38:12-19:
811When checking right hand side of badCadr2 with expected type
912 Int
1013
1114When checking argument cons2 to function FunErrTest.cadr:
1215 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
44When checking argument prf to function Data.Fin.fromInteger:
55 When using 2 as a literal for a Fin 2
66 2 is not strictly less than 2
7+ |
8+11 | two = 2
9+ | ^
710error005.idr:14:12:When checking right hand side of hahaha with expected type
811 Fin n
912
1013When checking argument prf to function Data.Fin.fromInteger:
1114 When using 0 as a literal for a Fin n
1215 0 is not strictly less than n
16+ |
17+14 | hahaha n = 0
18+ | ^
1319error005.idr:20:11:When checking right hand side of notOk with expected type
1420 Fin (plus 2 n)
1521
1622When checking argument prf to function Data.Fin.fromInteger:
1723 When using 2 as a literal for a Fin (S (S n))
1824 2 is not strictly less than S (S n)
25+ |
26+20 | notOk n = 2
27+ | ^
1928error005.idr:23:12-24:When checking right hand side of b0rken with expected type
2029 Fin 3
2130
@@ -23,9 +32,15 @@ When checking argument prf to function Data.Fin.fromInteger:
2332 When using n as a literal for a Fin 3
2433 Could not show that n is less than 3 because n is a bound
2534 variable instead of a constant Integer
35+ |
36+23 | b0rken n = fromInteger n
37+ | ~~~~~~~~~~~~~
2638error005.idr:26:17:When checking right hand side of x with expected type
2739 Fin 4
2840
2941When checking argument prf to function Data.Fin.fromInteger:
3042 When using 5 as a literal for a Fin 4
3143 5 is not strictly less than 4
44+ |
45+26 | x = the (Fin 4) 5
46+ | ^
test/error006/expected+3
@@ -1,2 +1,5 @@
11WithPatsNoWith.idr:4:1-13:When checking left hand side of foo:
22unexpected 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:
1313 Bits32
1414 and
1515 Int
16+ |
17+26 | send_page conn str code -- (prim__zextB32_Int code)
18+ | ~~~~~~~~~~~~~~~~~~~~~~~
test/error008/expected+6
@@ -1,4 +1,10 @@
11error008.idr:3:4:When checking type of Main.s2:
22Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
3+ |
4+3 | s2 : x + sum Nil = x * fromInteger 0
5+ | ^
36error008a.idr:3:4:When checking type of Main.s1:
47Can'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 @@
11test023.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 @@
11interfaces008.idr:20:18-23:
22Default 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
6363
6464When checking an application of function Prelude.Applicative.pure:
6565 No such variable f
66+ |
67+13 | term = do f <- factor
68+ | ~~~~~~~~~~~~~~~~~ ...
6669./mplus2.idr:17:37:
6770 |
687117 | `mplus` pure f
test/literate001/expected+3
@@ -1,4 +1,7 @@
11./test003a.lidr:1:0:Program line next to comment
2+ |
3+1 | Broken
4+ | ^
25'a'
36'd'
47zabcdefg
test/meta002/expected+9
@@ -1,13 +1,22 @@
11DataDef.idr:74:1-8:
22While running an elaboration script, the following error occurred:
33Prelude.Either.Either is already defined as a datatype.
4+ |
5+74 | %runElab nope
6+ | ~~~~~~~~
47Tacs.idr:299:15-300:78:
58When checking right hand side of testElab3 with expected type
69 DPair Ty (Tm [])
710
811Unifying 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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
915AgdaStyleReflection.idr:315:5-20:
1016When checking right hand side of baz with expected type
1117 (Nat, Void)
1218
1319PROOF SEARCH FAILURE is not defined.
20+ |
21+315 | baz = tactic trivial
22+ | ~~~~~~~~~~~~~~~~
test/meta003/expected+3
@@ -4,3 +4,6 @@ Type mismatch between
44 ()
55and
66 String
7+ |
8+14 | %runElab mkBadDef1
9+ | ~~~~~~~~
test/meta004/expected+3
@@ -1,3 +1,6 @@
11meta004.idr:50:1-8:
22While running an elaboration script, the following error occurred:
33Not an impossible case
4+ |
5+50 | %runElab domore
6+ | ~~~~~~~~
test/proof001/expected+6
@@ -1,4 +1,10 @@
11test029.idr:29:25-29:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+29 | simple.append_lemma_2 = proof {
5+ | ~~~~~
36test029.idr:36:25-29:
47This 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 @@
11Reflect.idr:175:21-25:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+175 | Reflect.appRExpr1 = proof {
5+ | ~~~~~
36Reflect.idr:184:21-25:
47This style of tactic proof is deprecated. See %runElab for the replacement.
8+ |
9+184 | Reflect.appRExpr2 = proof {
10+ | ~~~~~
511Reflect.idr:192:15-19:
612This style of tactic proof is deprecated. See %runElab for the replacement.
13+ |
14+192 | Reflect.bp1 = proof {
15+ | ~~~~~
716test030a.idr:12:26-37:
817When checking right hand side of testReflect1 with expected type
918 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs
@@ -19,3 +28,6 @@ When checking an application of function Reflect.getJust:
1928 Just x
2029 and
2130 Nothing
31+ |
32+12 | testReflect1 {a} xs ys = AssocProof a
33+ | ~~~~~~~~~~~~
test/proof003/expected+18
@@ -1,15 +1,33 @@
11Parity.idr:17:18-22:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+17 | parity_lemma_2 = proof {
5+ | ~~~~~
36Parity.idr:24:18-22:
47This style of tactic proof is deprecated. See %runElab for the replacement.
8+ |
9+24 | parity_lemma_1 = proof {
10+ | ~~~~~
511test015.idr:88:15-19:
612This style of tactic proof is deprecated. See %runElab for the replacement.
13+ |
14+88 | Main.ntbOdd = proof {
15+ | ~~~~~
716test015.idr:97:16-20:
817This style of tactic proof is deprecated. See %runElab for the replacement.
18+ |
19+97 | Main.ntbEven = proof {
20+ | ~~~~~
921test015.idr:107:20-24:
1022This style of tactic proof is deprecated. See %runElab for the replacement.
23+ |
24+107 | Main.adc_lemma_2 = proof {
25+ | ~~~~~
1126test015.idr:142:20-24:
1227This style of tactic proof is deprecated. See %runElab for the replacement.
28+ |
29+142 | Main.adc_lemma_1 = proof {
30+ | ~~~~~
133100101010
143201011001
1533010000011
test/proof007/expected+3
@@ -4,3 +4,6 @@ When checking right hand side of test with expected type
44
55When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:
66 No such variable sadgjhsag
7+ |
8+9 | test = funWithBadDefArg
9+ | ~~~~~~~~~~~~~~~~~~
test/proof008/expected+3
@@ -1,2 +1,5 @@
11ClaimAndUnfocus.idr:8:27-31:
22This 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 ::
88 x ::
99 (xs ++ ys) ++
1010 zs
11+ |
12+20 | = rewrite vassoc xs ys xs using vreplace in
13+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
1114proof011a.idr:14:5-37:
1215When checking right hand side of vassoc' with expected type
1316 (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 ::
1821 x ::
1922 (xs ++ ys) ++
2023 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
22 TT
33
44No such variable k
5+ |
6+11 | zzz = `(FZ)
7+ | ~~~~~~~
test/quasiquote004/expected+12
@@ -1,11 +1,23 @@
11Quasiquote004.idr:39:26-30:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+39 | Quasiquote004.getMeNat = proof
5+ | ~~~~~
36Quasiquote004.idr:42:28-32:
47This style of tactic proof is deprecated. See %runElab for the replacement.
8+ |
9+42 | Quasiquote004.fizzyIsAOK = proof
10+ | ~~~~~
511Quasiquote004.idr:50:27-31:
612This style of tactic proof is deprecated. See %runElab for the replacement.
13+ |
14+50 | Quasiquote004.getMeNat' = proof
15+ | ~~~~~
716Quasiquote004.idr:50:25-51:18:
817When checking right hand side of Quasiquote004.getMeNat' with expected type
918 String
1019
1120Not 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
44
55Can't disambiguate name: ForeignEnv.Nil,
66 Prelude.List.Nil
7+ |
8+9 | b = `{Nil}
9+ | ~~~~~~~~
710quasiquote006.idr:12:3-17:
811When checking right hand side of c with expected type
912 TTName
1013
1114No such variable alsdkjflkj
15+ |
16+12 | c = `{alsdkjflkj}
17+ | ~~~~~~~~~~~~~~~
1218quasiquote006.idr:15:3-11:
1319When checking right hand side of d with expected type
1420 TTName
@@ -16,4 +22,7 @@ When checking right hand side of d with expected type
1622Can't disambiguate name: ForeignEnv.::,
1723 Prelude.List.::,
1824 Prelude.Stream.::
25+ |
26+15 | d = `{(::)}
27+ | ~~~~~~~~~
1928quasiquote006.idr:17:3:Main.d already defined
test/reg017/expected+6
@@ -1,5 +1,11 @@
11reg017.idr:5:17-23:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+5 | { default tactics { refine Refl; solve; } prfA : a = a } ->
5+ | ~~~~~~~
36reg017.idr:8:17-23:
47This style of tactic proof is deprecated. See %runElab for the replacement.
8+ |
9+8 | { default tactics { refine Refl; solve; } prfBC : b = c } ->
10+ | ~~~~~~~
5114
test/reg027/expected+3
@@ -1,2 +1,5 @@
11<<int fn>>
22reg027a.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 @@
11reg003a.idr:4:13-38:When checking type of Main.ECons:
22No such variable OddList
3+ |
4+4 | ECons : Nat -> OddList -> EvenList
5+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~
36reg003a.idr:7:13-38:When checking type of Main.OCons:
47No such variable EvenList
8+ |
9+7 | OCons : Nat -> EvenList -> OddList
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~
511reg003a.idr:9:6:When checking type of Main.test:
612No such variable EvenList
13+ |
14+9 | test : EvenList
15+ | ^
716reg006.idr:17:1-23:
817RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
18+ |
19+17 | lookup k Leaf = Nothing
20+ | ~~~~~~~~~~~~~~~~~~~~~~~
921reg007.lidr:8:3-13:A.n is already defined
22+ |
23+8 | > A.n = Z -- This is where it's at!
24+ | ~~~~~~~~~~~
1025reg007.lidr:12:13-18:When checking right hand side of hurrah with expected type
1126 0 = 1
1227
@@ -20,20 +35,44 @@ Specifically:
2035 1
2136 and
2237 0
38+ |
39+12 | > hurrah = isSame
40+ | ~~~~~~
2341reg010.idr:5:3-26:
2442When checking left hand side of with block in usubst.unsafeSubst:
2543Can't match on with block in usubst.unsafeSubst warg a P x x px
44+ |
45+5 | unsafeSubst P x x px | _ = px
46+ | ~~~~~~~~~~~~~~~~~~~~~~~~
2647reg018a.idr:16:1-18:
2748conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
49+ |
50+16 | minusCoNat Z n = Z
51+ | ~~~~~~~~~~~~~~~~~~
2852reg018a.idr:21:1-42:
2953conat.loopForever is possibly not total due to: conat.minusCoNat
54+ |
55+21 | loopForever = minusCoNat infinity infinity
56+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3057reg018b.idr:8:1-28:
3158A.showB is possibly not total due to recursive path A.showB --> A.showB
59+ |
60+8 | showB (I x) = "I" ++ showB x
61+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3262reg018b.idr:11:1-6:
3363A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
64+ |
65+11 | Show B where show = showB
66+ | ~~~~~~
3467reg018c.idr:21:1-22:21:
3568CodataTest.inf is possibly not total due to: with block in CodataTest.inf
69+ |
70+21 | inf (x :: xs) with (hdtl xs)
71+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
3672reg018d.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3776reg023.idr:7:5-7:When checking right hand side of bad with expected type
3877 f Nat
3978
@@ -41,18 +80,42 @@ Type mismatch between
4180 Nat (Type of 0)
4281and
4382 f Nat (Expected type)
83+ |
84+7 | bad = Z
85+ | ~~~
4486reg028.idr:5:1-9:tbad.bad is possibly not total due to: with block in tbad.bad
87+ |
88+5 | bad Z = Z
89+ | ~~~~~~~~~
4590reg028a.idr:17:14-18:
4691This style of tactic proof is deprecated. See %runElab for the replacement.
92+ |
93+17 | qsortLemma = proof
94+ | ~~~~~
4795reg028a.idr:11:1-14:
4896tbad.qsort' is possibly not total due to: with block in tbad.qsort'
97+ |
98+11 | qsort' [] = []
99+ | ~~~~~~~~~~~~~~
49100reg034.idr:6:1-14:When checking left hand side of bar:
50101Can't match on bar xs xs Refl
102+ |
103+6 | bar xs xs Refl = Refl
104+ | ~~~~~~~~~~~~~~
51105reg034.idr:9:1-14:When checking left hand side of foo:
52106Can't match on foo f x x Refl
107+ |
108+9 | foo f x x Refl = Refl
109+ | ~~~~~~~~~~~~~~
53110reg035b.idr:8:12-38:No such variable __pi_arg
111+ |
112+8 | fins Z = ([] ** (finZEmpty {a=_}))
113+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~
54114reg044.idr:4:6-10:
55115This style of tactic proof is deprecated. See %runElab for the replacement.
116+ |
117+4 | pf = proof
118+ | ~~~~~
56119reg044.idr:4:4-6:13:When checking right hand side of Main.pf with expected type
57120 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
58121
@@ -66,12 +129,21 @@ Specifically:
66129 b
67130 and
68131 a
132+ |
133+4 | pf = proof
134+ | ~~~~~~~ ...
69135reg049.idr:2:11-14:When checking constructor Main.Bogus:
70136Void is not Main.Foo
137+ |
138+2 | Bogus : Void
139+ | ~~~~
71140reg049.idr:5:6-12:When checking right hand side of uhOh with expected type
72141 Void
73142
74143No such variable Bogus
144+ |
145+5 | uhOh = Bogus
146+ | ~~~~~~~
75147./badbangop.idr:7:1:
76148 |
771497 | (!) : List a -> Nat -> Maybe a
@@ -87,39 +159,87 @@ unexpected Operator without known fixity: !!
87159reg054.idr:18:1-17:When checking left hand side of inf:
88160When checking an application of constructor Main.MkInfer:
89161 Attempting concrete match on polymorphic argument: 0
162+ |
163+18 | inf (MkInfer _ Z) = True
164+ | ~~~~~~~~~~~~~~~~~
90165reg054.idr:34:1-18:When checking left hand side of weird:
91166No explicit types on left hand side: Char
167+ |
168+34 | weird {x = Char} y = '5'
169+ | ~~~~~~~~~~~~~~~~~~
92170reg054.idr:37:1-30:When checking left hand side of weird':
93171No explicit types on left hand side: Nat
172+ |
173+37 | weird' {x = Prelude.Nat.Nat} y = Z
174+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
94175reg054.idr:40:1-7:When checking left hand side of tctrick:
95176When checking an application of Main.tctrick:
96177 Type mismatch between
97178 Maybe a1 (Type of Just x)
98179 and
99180 a (Expected type)
181+ |
182+40 | tctrick (Just x) = x
183+ | ~~~~~~~
100184reg055.idr:5:1-7:When checking left hand side of g:
101185Can't match on g (f 0)
186+ |
187+5 | g (f Z) = 1
188+ | ~~~~~~~
102189reg055.idr:8:1-5:When checking left hand side of h:
103190Can't match on h x x
191+ |
192+8 | h x x = x
193+ | ~~~~~
104194reg055a.idr:8:1-18:When checking left hand side of foo:
105195When checking an application of constructor Foo.CAny:
106196 Attempting concrete match on polymorphic argument: Nothing
197+ |
198+8 | foo (CAny Nothing) = 42
199+ | ~~~~~~~~~~~~~~~~~~
107200reg055a.idr:13:1-23:When checking left hand side of Foo.apply:
108201Can't match on apply (\x, y => x) a
202+ |
203+13 | apply (\x => \y => x) a = a
204+ | ~~~~~~~~~~~~~~~~~~~~~~~
109205reg056.idr:7:16-25:dodgy n m Refl is a valid case
206+ |
207+7 | dodgy n m Refl impossible
208+ | ~~~~~~~~~~
110209reg056.idr:10:11-20:nonk Refl is a valid case
210+ |
211+10 | nonk Refl impossible
212+ | ~~~~~~~~~~
111213reg068.idr:1:6-8:Main.nat has a name which may be implicitly bound.
112214This is likely to lead to problems!
215+ |
216+1 | data nat : Type where --error
217+ | ~~~
113218reg068.idr:2:8-10:Main.ze has a name which may be implicitly bound.
114219This 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+ | ~~~
115223reg068.idr:2:8-10:
116224nat is bound as an implicit
117225 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+ | ~~~
118229reg068.idr:2:8-10:When checking constructor Main.ze:
119230Type 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+ | ~~~
120234Mod.idr:11:1-22:public export Mod.natexp can't refer to export Mod.natfn
235+ |
236+11 | natexp k = S (natfn k)
237+ | ~~~~~~~~~~~~~~~~~~~~~~
121238reg070.idr:7:1-7:
122239Test_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+ | ~~~~~~~
123243./reg076.idr:8:1:
124244 |
1252458 | <empty line>
@@ -147,5 +267,14 @@ When checking argument value to function Prelude.Basics.the:
147267 -0.0
148268 and
149269 0.0
270+ |
271+4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
272+ | ~~~~~~~~~~~~~~~~~~~~~
150273Canonicity.idr:9:1-9:Canonicity.f is not total as there are missing cases
274+ |
275+9 | f Nil = 0
276+ | ~~~~~~~~~
151277Canonicity.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 @@
11SourceLoc.idr:12:19-25:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+12 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation
5+ | ~~~~~~~
36SourceLoc.idr:21:19-23:
47This style of tactic proof is deprecated. See %runElab for the replacement.
8+ |
9+21 | fromProofScript = proof sourceLocation
10+ | ~~~~~
511SourceLoc.idr:41:20-26:
612This style of tactic proof is deprecated. See %runElab for the replacement.
13+ |
14+41 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t
15+ | ~~~~~~~
716SourceLoc.idr:99:18-22:
817This style of tactic proof is deprecated. See %runElab for the replacement.
18+ |
19+99 | SourceLoc.meta = proof
20+ | ~~~~~
921Testing using definition
1022FileLoc "SourceLoc.idr" (17, 11) (17, 16)
1123Testing using inline tactics
test/syntax001/expected+6
@@ -6,6 +6,9 @@ When checking an application of function Prelude.Interfaces.+:
66 String (Type of "argh")
77 and
88 Nat (Expected type)
9+ |
10+6 | foo = fnord "argh"
11+ | ~~~~~~~~~~~~
912SyntaxTest.idr:5:7-18:When checking right hand side of foo with expected type
1013 Nat
1114
@@ -14,3 +17,6 @@ When checking an application of function Prelude.Interfaces.+:
1417 String (Type of "argh")
1518 and
1619 Nat (Expected type)
20+ |
21+5 | foo = fnord "argh"
22+ | ~~~~~~~~~~~~
test/totality001/expected+9
@@ -1,3 +1,12 @@
11test010.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
25test010a.idr:9:1-23:main.bar is possibly not total due to: main.MkBad
6+ |
7+9 | bar = MkBad (\x => 3) 3
8+ | ~~~~~~~~~~~~~~~~~~~~~~~
39test010b.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 @@
11test017.idr:94:26-30:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+94 | maxCommutativeStepCase = proof {
5+ | ~~~~~
36test017a.idr:7:1-24:
47scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
8+ |
9+7 | vtrans [] _ = []
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~
511test017b.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 @@
11totality003a.idr:5:1-13:
22smaller.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 @@
11[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
22totality004a.idr:13:1-44:
33Main.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
47totality004a.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 @@
11totality006.idr:8:1-29:Main.prf is not total as there are missing cases
2+ |
3+8 | prf Z Z Oh impossible
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
25totality006a.idr:11:21-30:prf' (S _) (S _) Oh is a valid case
6+ |
7+11 | prf' (S _) (S _) Oh impossible
8+ | ~~~~~~~~~~
39totality006b.idr:10:1-34:
410totality006b.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 @@
11Entering directory `./src'
22Totality.idr:4:1-9:
33Totality.foo is not total as there are missing cases
4+ |
5+4 | foo Z = Z
6+ | ~~~~~~~~~
47Totality.idr:4:1-9:Could not build: Totality.foo is not total as there are missing cases
58Leaving directory `./src'
test/totality008/expected+3
@@ -1 +1,4 @@
11totality008.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 @@
11TestLambdaPossible.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+ | ~~~~~~~~~~
25TestLambdaPossible.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
39TestLambdaPossible.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+ | ^
413TestLambdaPossible.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
517TestLambdaPossible.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+ | ~~~~~~~~~~~~~~~~~~~~~
621TestLambdaPossible.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
725TestLambdaPossible.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+ | ~~~~~~~~~~~ ...
829TestLambdaPossible.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
933TestLambdaPossible2.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1037TestLambdaPossible2.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 @@
11totality010.idr:27:1-35:Main.evenNotS is not total as there are missing cases
2+ |
3+27 | evenNotS MkEven ZeroEven impossible
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
25totality010.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 @@
11totality011.lidr:22:3-57:
22Main.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 @@
11totality012a.idr:9:1-10:27:
22Main.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
36totality012b.idr:11:1-17:33:
47Main.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 @@
11totality013a.idr:5:3-49:
22Main.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
36totality013a.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.
66 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
77 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
88 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 @@
11totality015a.idr:52:3-53:
22Main.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
36totality015a.idr:42:3-44:36:Main.correct is possibly not total due to: Main.quiz
7+ |
8+42 | correct nums score
9+ | ~~~~~~~~~~~~~~~~~~ ...
410totality015a.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 @@
11totality016.idr:15:1-21:Main.f1 is not total as there are missing cases
2+ |
3+15 | f1 (MkTP T1 x) = True
4+ | ~~~~~~~~~~~~~~~~~~~~~
25totality016.idr:19:1-24:Main.f2 is not total as there are missing cases
6+ |
7+19 | f2 (MkTP T1 x, _) = True
8+ | ~~~~~~~~~~~~~~~~~~~~~~~~
39totality016.idr:23:1-29:Main.f3 is not total as there are missing cases
10+ |
11+23 | f3 ((MkTP T1 x, _), _) = True
12+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
413totality016.idr:27:1-14:Main.g1 is not total as there are missing cases
14+ |
15+27 | g1 T1 x = True
16+ | ~~~~~~~~~~~~~~
517totality016.idr:31:1-17:Main.g2 is not total as there are missing cases
18+ |
19+31 | g2 (T1, x) = True
20+ | ~~~~~~~~~~~~~~~~~
621totality016.idr:35:1-16:Main.h1 is not total as there are missing cases
22+ |
23+35 | h1 True x = True
24+ | ~~~~~~~~~~~~~~~~
725totality016.idr:39:1-19:Main.h2 is not total as there are missing cases
26+ |
27+39 | h2 (True, x) = True
28+ | ~~~~~~~~~~~~~~~~~~~
829totality016.idr:43:1-25:Main.h3 is not total as there are missing cases
30+ |
31+43 | h3 (MkTP2 (T1, x)) = True
32+ | ~~~~~~~~~~~~~~~~~~~~~~~~~
933totality016.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 @@
11totality017.idr:19:1-15:Main.g1 is not total as there are missing cases
2+ |
3+19 | g1 T1 T1 = True
4+ | ~~~~~~~~~~~~~~~
25totality017.idr:25:1-17:Main.g2 is not total as there are missing cases
6+ |
7+25 | g2 T1' T1' = True
8+ | ~~~~~~~~~~~~~~~~~
39totality017.idr:31:1-13:Main.g3 is not total as there are missing cases
10+ |
11+31 | g3 T1' = True
12+ | ~~~~~~~~~~~~~
413totality017.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
517totality017.idr:42:1-11:Main.f' is not total as there are missing cases
18+ |
19+42 | f' 0 = True
20+ | ~~~~~~~~~~~
621totality017.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 @@
11totality018.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 @@
11totality019.idr:8:1-36:Main.testCov is not total as there are missing cases
2+ |
3+8 | testCov False False = ?testCov_rhs_3
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
25totality019.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 @@
11totality020.idr:4:14-23:bug _ _ Refl is a valid case
2+ |
3+4 | bug _ _ Refl impossible
4+ | ~~~~~~~~~~
25totality020.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 @@
11totality021.idr:8:1-67:
22Main.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
36totality021.idr:12:1-66:
47Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'
8+ |
9+12 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
511totality021.idr:18:1-26:
612Main.v is possibly not total due to: Main.sLevelNotSLevel
13+ |
14+18 | v = sLevelNotSLevel l Refl
15+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~
716totality021a.idr:9:1-37:
817Main.noNonEmptyPointInt is not total as there are missing cases
18+ |
19+9 | noNonEmptyPointInt {n} Nil impossible
20+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
921totality021a.idr:12:1-31:
1022Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt
23+ |
24+12 | myVoid = noNonEmptyPointInt [2]
25+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
test/totality022/expected+3
@@ -1 +1,4 @@
11totality022.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 @@
11totality023.idr:9:1-10:27:
22Main.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 @@
11tutorial002.idr:41:25-29:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+41 | Main.natToBin_lemma_1 = proof
5+ | ~~~~~
36tutorial002.idr:48:18-22:
47This style of tactic proof is deprecated. See %runElab for the replacement.
8+ |
9+48 | parity_lemma_1 = proof
10+ | ~~~~~
511tutorial002.idr:54:18-22:
612This 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 @@
11tutorial004.idr:46:14-18:
22This style of tactic proof is deprecated. See %runElab for the replacement.
3+ |
4+46 | plusredZ_S = proof {
5+ | ~~~~~
36tutorial004.idr:53:14-18:
47This 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.:::
1313 plus len len
1414 and
1515 plus len m
16+ |
17+5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN
18+ | ~~
1619tutorial006b.idr:10:37-50:
1720When checking right hand side of with block in Main.parity with expected type
1821 Parity (S (S (j + j)))
@@ -27,3 +30,6 @@ Specifically:
2730 plus (S j) (S j)
2831 and
2932 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
22 Int -> String
33and
44 UniqueType (Int -> String)
5+ |
6+35 | showStuff xs = do
7+ | ~~~~ ...
58unique001a.idr:46:15-54:28:Type mismatch between
69 Int -> String
710and
811 UniqueType (Int -> String)
12+ |
13+46 | showStuff' xs = do
14+ | ~~~~ ...
915unique001a.idr:57:15-62:33:Type mismatch between
1016 UniqueType (Int -> String)
1117and
1218 Int -> String
19+ |
20+57 | showThings xs = do
21+ | ~~~~ ...
1322unique001b.idr:18:17-42:Borrowed name xs must not be used on RHS
23+ |
24+18 | showU (x :: xs) = show x ++ "," ++ free xs
25+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~
1426unique001c.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1530unique001d.idr:4:16-18:Borrowed name x must not be used on RHS
31+ |
32+4 | steal (Read x) = x
33+ | ~~~
1634unique001e.idr:4:12-40:
1735Constructor Main.Nil has a UniqueType, but the data type does not
36+ |
37+4 | Nil : {a : UniqueType} -> BadList a
38+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1839unique002.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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
1943unique002a.idr:17:8-20:19:Type mismatch between
2044 Int -> String
2145and
2246 UniqueType (Int -> String)
47+ |
48+17 | foo xs = do let f = \x : Int => showU xs
49+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
2350unique003.idr:20:8-24:19:Type mismatch between
2451 Int -> String
2552and
2653 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.
77 ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}
88 ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}
99 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.
77 ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}
88 ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}
99 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+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~