@@ -87,3 +87,274 @@ reg018b.idr:11:1-6:
88A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
88A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
90+reg018c.idr:21:1-22:21:
92+21 | inf (x :: xs) with (hdtl xs)
93+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
94+CodataTest.inf is possibly not total due to: with block in CodataTest.inf
98+8 | pull {n=Z} _ (x :: xs) = (x, xs)
99+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
100+Main.pull is not total as there are missing cases
106+When checking right hand side of bad with expected type
109+Type mismatch between
112+ f Nat (Expected type)
118+tbad.bad is possibly not total due to: with block in tbad.bad
120+reg028a.idr:17:14-18:
122+17 | qsortLemma = proof
124+This style of tactic proof is deprecated. See %runElab for the replacement.
130+tbad.qsort' is possibly not total due to: with block in tbad.qsort'
134+6 | bar xs xs Refl = Refl
136+When checking left hand side of bar:
137+Can't match on bar xs xs Refl
141+9 | foo f x x Refl = Refl
143+When checking left hand side of foo:
144+Can't match on foo f x x Refl
148+8 | fins Z = ([] ** (finZEmpty {a=_}))
149+ | ~~~~~~~~~~~~~~~~~~~~~~~~~
150+No such variable __pi_arg
156+This style of tactic proof is deprecated. See %runElab for the replacement.
162+When checking right hand side of Main.pf with expected type
163+ (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
165+Type mismatch between
166+ b = b (Type of Refl)
168+ a = b (Expected type)
171+ Type mismatch between
180+When checking constructor Main.Bogus:
187+When checking right hand side of uhOh with expected type
190+No such variable Bogus
194+7 | (!) : List a -> Nat -> Maybe a
196+! is not a valid operator
198+baddoublebang.idr:6:28:
200+6 | doubleBang mmn = do pure !!mmn
202+unexpected Operator without known fixity: !!
206+18 | inf (MkInfer _ Z) = True
208+When checking left hand side of inf:
209+When checking an application of constructor Main.MkInfer:
210+ Attempting concrete match on polymorphic argument: 0
214+34 | weird {x = Char} y = '5'
215+ | ~~~~~~~~~~~~~~~~~~
216+When checking left hand side of weird:
217+No explicit types on left hand side: Char
221+37 | weird' {x = Prelude.Nat.Nat} y = Z
222+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
223+When checking left hand side of weird':
224+No explicit types on left hand side: Nat
228+40 | tctrick (Just x) = x
230+When checking left hand side of tctrick:
231+When checking an application of Main.tctrick:
232+ Type mismatch between
233+ Maybe a1 (Type of Just x)
241+When checking left hand side of g:
242+Can't match on g (f 0)
248+When checking left hand side of h:
253+8 | foo (CAny Nothing) = 42
254+ | ~~~~~~~~~~~~~~~~~~
255+When checking left hand side of foo:
256+When checking an application of constructor Foo.CAny:
257+ Attempting concrete match on polymorphic argument: Nothing
261+13 | apply (\x => \y => x) a = a
262+ | ~~~~~~~~~~~~~~~~~~~~~~~
263+When checking left hand side of Foo.apply:
264+Can't match on apply (\x, y => x) a
268+7 | dodgy n m Refl impossible
270+dodgy n m Refl is a valid case
274+10 | nonk Refl impossible
276+nonk Refl is a valid case
280+1 | data nat : Type where --error
282+Main.nat has a name which may be implicitly bound.
283+This is likely to lead to problems!
287+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
289+Main.ze has a name which may be implicitly bound.
290+This is likely to lead to problems!
294+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
296+nat is bound as an implicit
297+ Did you mean to refer to Main.nat?
301+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
303+When checking constructor Main.ze:
304+Type level variable nat is not Main.nat
308+11 | natexp k = S (natfn k)
309+ | ~~~~~~~~~~~~~~~~~~~~~~
310+public export Mod.natexp can't refer to export Mod.natfn
316+Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show
322+Missing fixity declaration for Main.:>
328+Missing fixity declaration for Main.:>>
330+DoubleEquality.idr:4:83-103:
332+4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
333+ | ~~~~~~~~~~~~~~~~~~~~~
334+When checking right hand side of oops with expected type
337+When checking argument value to function Prelude.Basics.the:
338+ Type mismatch between
339+ x = x (Type of Refl)
341+ (-0.0) = 0.0 (Expected type)
344+ Type mismatch between
349+Canonicity.idr:9:1-9:
353+Canonicity.f is not total as there are missing cases
355+Canonicity.idr:12:1-20:
357+12 | NaN = f (Cons 0 Nil)
358+ | ~~~~~~~~~~~~~~~~~~~~
359+Canonicity.NaN is possibly not total due to: Canonicity.f