@@ -87,3 +87,274 @@ reg018b.idr:11:1-6:
8787 | ~~~~~~
8888A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
8989
90+reg018c.idr:21:1-22:21:
91+ |
92+21 | inf (x :: xs) with (hdtl xs)
93+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
94+CodataTest.inf is possibly not total due to: with block in CodataTest.inf
95+
96+reg018d.idr:8:1-39:
97+ |
98+8 | pull {n=Z} _ (x :: xs) = (x, xs)
99+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
100+Main.pull is not total as there are missing cases
101+
102+reg023.idr:7:7:
103+ |
104+7 | bad = Z
105+ | ^
106+When checking right hand side of bad with expected type
107+ f Nat
108+
109+Type mismatch between
110+ Nat (Type of 0)
111+and
112+ f Nat (Expected type)
113+
114+reg028.idr:5:1-9:
115+ |
116+5 | bad Z = Z
117+ | ~~~~~~~~~
118+tbad.bad is possibly not total due to: with block in tbad.bad
119+
120+reg028a.idr:17:14-18:
121+ |
122+17 | qsortLemma = proof
123+ | ~~~~~
124+This style of tactic proof is deprecated. See %runElab for the replacement.
125+
126+reg028a.idr:11:1-14:
127+ |
128+11 | qsort' [] = []
129+ | ~~~~~~~~~~~~~~
130+tbad.qsort' is possibly not total due to: with block in tbad.qsort'
131+
132+reg034.idr:6:1-14:
133+ |
134+6 | bar xs xs Refl = Refl
135+ | ~~~~~~~~~~~~~~
136+When checking left hand side of bar:
137+Can't match on bar xs xs Refl
138+
139+reg034.idr:9:1-14:
140+ |
141+9 | foo f x x Refl = Refl
142+ | ~~~~~~~~~~~~~~
143+When checking left hand side of foo:
144+Can't match on foo f x x Refl
145+
146+reg035b.idr:8:14-38:
147+ |
148+8 | fins Z = ([] ** (finZEmpty {a=_}))
149+ | ~~~~~~~~~~~~~~~~~~~~~~~~~
150+No such variable __pi_arg
151+
152+reg044.idr:4:6-10:
153+ |
154+4 | pf = proof
155+ | ~~~~~
156+This style of tactic proof is deprecated. See %runElab for the replacement.
157+
158+reg044.idr:4:6-6:13:
159+ |
160+4 | pf = proof
161+ | ~~~~~ ...
162+When checking right hand side of Main.pf with expected type
163+ (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
164+
165+Type mismatch between
166+ b = b (Type of Refl)
167+and
168+ a = b (Expected type)
169+
170+Specifically:
171+ Type mismatch between
172+ b
173+ and
174+ a
175+
176+reg049.idr:2:11-14:
177+ |
178+2 | Bogus : Void
179+ | ~~~~
180+When checking constructor Main.Bogus:
181+Void is not Main.Foo
182+
183+reg049.idr:5:8-12:
184+ |
185+5 | uhOh = Bogus
186+ | ~~~~~
187+When checking right hand side of uhOh with expected type
188+ Void
189+
190+No such variable Bogus
191+
192+badbangop.idr:7:1:
193+ |
194+7 | (!) : List a -> Nat -> Maybe a
195+ | ^
196+! is not a valid operator
197+
198+baddoublebang.idr:6:28:
199+ |
200+6 | doubleBang mmn = do pure !!mmn
201+ | ^
202+unexpected Operator without known fixity: !!
203+
204+reg054.idr:18:1-17:
205+ |
206+18 | inf (MkInfer _ Z) = True
207+ | ~~~~~~~~~~~~~~~~~
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
211+
212+reg054.idr:34:1-18:
213+ |
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
218+
219+reg054.idr:37:1-30:
220+ |
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
225+
226+reg054.idr:40:1-7:
227+ |
228+40 | tctrick (Just x) = x
229+ | ~~~~~~~
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)
234+ and
235+ a (Expected type)
236+
237+reg055.idr:5:1-7:
238+ |
239+5 | g (f Z) = 1
240+ | ~~~~~~~
241+When checking left hand side of g:
242+Can't match on g (f 0)
243+
244+reg055.idr:8:1-5:
245+ |
246+8 | h x x = x
247+ | ~~~~~
248+When checking left hand side of h:
249+Can't match on h x x
250+
251+reg055a.idr:8:1-18:
252+ |
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
258+
259+reg055a.idr:13:1-23:
260+ |
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
265+
266+reg056.idr:7:16-25:
267+ |
268+7 | dodgy n m Refl impossible
269+ | ~~~~~~~~~~
270+dodgy n m Refl is a valid case
271+
272+reg056.idr:10:11-20:
273+ |
274+10 | nonk Refl impossible
275+ | ~~~~~~~~~~
276+nonk Refl is a valid case
277+
278+reg068.idr:1:6-8:
279+ |
280+1 | data nat : Type where --error
281+ | ~~~
282+Main.nat has a name which may be implicitly bound.
283+This is likely to lead to problems!
284+
285+reg068.idr:2:8-10:
286+ |
287+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
288+ | ~~~
289+Main.ze has a name which may be implicitly bound.
290+This is likely to lead to problems!
291+
292+reg068.idr:2:8-10:
293+ |
294+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
295+ | ~~~
296+nat is bound as an implicit
297+ Did you mean to refer to Main.nat?
298+
299+reg068.idr:2:8-10:
300+ |
301+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
302+ | ~~~
303+When checking constructor Main.ze:
304+Type level variable nat is not Main.nat
305+
306+Mod.idr:11:1-22:
307+ |
308+11 | natexp k = S (natfn k)
309+ | ~~~~~~~~~~~~~~~~~~~~~~
310+public export Mod.natexp can't refer to export Mod.natfn
311+
312+reg070.idr:7:1-7:
313+ |
314+7 | Show Te where
315+ | ~~~~~~~
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
317+
318+reg076.idr:8:1:
319+ |
320+8 | <end of file>
321+ | ^
322+Missing fixity declaration for Main.:>
323+
324+reg077.idr:3:1:
325+ |
326+3 | <end of file>
327+ | ^
328+Missing fixity declaration for Main.:>>
329+
330+DoubleEquality.idr:4:83-103:
331+ |
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
335+ Void
336+
337+When checking argument value to function Prelude.Basics.the:
338+ Type mismatch between
339+ x = x (Type of Refl)
340+ and
341+ (-0.0) = 0.0 (Expected type)
342+
343+ Specifically:
344+ Type mismatch between
345+ -0.0
346+ and
347+ 0.0
348+
349+Canonicity.idr:9:1-9:
350+ |
351+9 | f Nil = 0
352+ | ~~~~~~~~~
353+Canonicity.f is not total as there are missing cases
354+
355+Canonicity.idr:12:1-20:
356+ |
357+12 | NaN = f (Cons 0 Nil)
358+ | ~~~~~~~~~~~~~~~~~~~~
359+Canonicity.NaN is possibly not total due to: Canonicity.f
360+