reg001.idr:2:1-9: | 2 | foo a a x = x | ~~~~~~~~~ When checking left hand side of foo: Can't match on foo a a x reg002.idr:3:1-19: | 3 | append (X :: XS) ys = X :: append XS ys | ~~~~~~~~~~~~~~~~~~~ When checking left hand side of append: When checking argument x to constructor Prelude.List.::: X is not a valid name for a pattern variable reg003a.idr:4:13-38: | 4 | ECons : Nat -> OddList -> EvenList | ~~~~~~~~~~~~~~~~~~~~~~~~~~ When checking type of Main.ECons: No such variable OddList reg003a.idr:7:13-38: | 7 | OCons : Nat -> EvenList -> OddList | ~~~~~~~~~~~~~~~~~~~~~~~~~~ When checking type of Main.OCons: No such variable EvenList reg003a.idr:9:6: | 9 | test : EvenList | ^ When checking type of Main.test: No such variable EvenList reg006.idr:17:1-23: | 17 | lookup k Leaf = Nothing | ~~~~~~~~~~~~~~~~~~~~~~~ RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup reg007.lidr:8:3-13: | 8 | > A.n = Z -- This is where it's at! | ~~~~~~~~~~~ A.n is already defined reg007.lidr:12:13-18: | 12 | > hurrah = isSame | ~~~~~~ When checking right hand side of hurrah with expected type 0 = 1 Type mismatch between n = lala (Type of isSame) and 0 = 1 (Expected type) Specifically: Type mismatch between 1 and 0 reg010.idr:5:3-26: | 5 | unsafeSubst P x x px | _ = px | ~~~~~~~~~~~~~~~~~~~~~~~~ When checking left hand side of with block in usubst.unsafeSubst: Can't match on with block in usubst.unsafeSubst warg a P x x px reg018a.idr:16:1-18: | 16 | minusCoNat Z n = Z | ~~~~~~~~~~~~~~~~~~ conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat reg018a.idr:21:1-42: | 21 | loopForever = minusCoNat infinity infinity | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ conat.loopForever is possibly not total due to: conat.minusCoNat reg018b.idr:8:1-28: | 8 | showB (I x) = "I" ++ showB x | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A.showB is possibly not total due to recursive path A.showB --> A.showB reg018b.idr:11:1-6: | 11 | Show B where show = showB | ~~~~~~ A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB reg018c.idr:21:1-22:21: | 21 | inf (x :: xs) with (hdtl xs) | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ... CodataTest.inf is possibly not total due to: with block in CodataTest.inf reg018d.idr:8:1-39: | 8 | pull {n=Z} _ (x :: xs) = (x, xs) | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Main.pull is not total as there are missing cases reg023.idr:7:7: | 7 | bad = Z | ^ When checking right hand side of bad with expected type f Nat Type mismatch between Nat (Type of 0) and f Nat (Expected type) reg028.idr:5:1-9: | 5 | bad Z = Z | ~~~~~~~~~ tbad.bad is possibly not total due to: with block in tbad.bad reg028a.idr:17:14-18: | 17 | qsortLemma = proof | ~~~~~ This style of tactic proof is deprecated. See %runElab for the replacement. reg028a.idr:11:1-14: | 11 | qsort' [] = [] | ~~~~~~~~~~~~~~ tbad.qsort' is possibly not total due to: with block in tbad.qsort' reg034.idr:6:1-14: | 6 | bar xs xs Refl = Refl | ~~~~~~~~~~~~~~ When checking left hand side of bar: Can't match on bar xs xs Refl reg034.idr:9:1-14: | 9 | foo f x x Refl = Refl | ~~~~~~~~~~~~~~ When checking left hand side of foo: Can't match on foo f x x Refl reg035b.idr:8:14-38: | 8 | fins Z = ([] ** (finZEmpty {a=_})) | ~~~~~~~~~~~~~~~~~~~~~~~~~ No such variable __pi_arg reg044.idr:4:6-10: | 4 | pf = proof | ~~~~~ This style of tactic proof is deprecated. See %runElab for the replacement. reg044.idr:4:6-6:13: | 4 | pf = proof | ~~~~~ ... When checking right hand side of Main.pf with expected type (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b Type mismatch between b = b (Type of Refl) and a = b (Expected type) Specifically: Type mismatch between b and a reg049.idr:2:11-14: | 2 | Bogus : Void | ~~~~ When checking constructor Main.Bogus: Void is not Main.Foo reg049.idr:5:8-12: | 5 | uhOh = Bogus | ~~~~~ When checking right hand side of uhOh with expected type Void No such variable Bogus badbangop.idr:7:1: | 7 | (!) : List a -> Nat -> Maybe a | ^ ! is not a valid operator baddoublebang.idr:6:28: | 6 | doubleBang mmn = do pure !!mmn | ^ unexpected Operator without known fixity: !! reg054.idr:18:1-17: | 18 | inf (MkInfer _ Z) = True | ~~~~~~~~~~~~~~~~~ When checking left hand side of inf: When checking an application of constructor Main.MkInfer: Attempting concrete match on polymorphic argument: 0 reg054.idr:34:1-18: | 34 | weird {x = Char} y = '5' | ~~~~~~~~~~~~~~~~~~ When checking left hand side of weird: No explicit types on left hand side: Char reg054.idr:37:1-30: | 37 | weird' {x = Prelude.Nat.Nat} y = Z | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When checking left hand side of weird': No explicit types on left hand side: Nat reg054.idr:40:1-7: | 40 | tctrick (Just x) = x | ~~~~~~~ When checking left hand side of tctrick: When checking an application of Main.tctrick: Type mismatch between Maybe a1 (Type of Just x) and a (Expected type) reg055.idr:5:1-7: | 5 | g (f Z) = 1 | ~~~~~~~ When checking left hand side of g: Can't match on g (f 0) reg055.idr:8:1-5: | 8 | h x x = x | ~~~~~ When checking left hand side of h: Can't match on h x x reg055a.idr:8:1-18: | 8 | foo (CAny Nothing) = 42 | ~~~~~~~~~~~~~~~~~~ When checking left hand side of foo: When checking an application of constructor Foo.CAny: Attempting concrete match on polymorphic argument: Nothing reg055a.idr:13:1-23: | 13 | apply (\x => \y => x) a = a | ~~~~~~~~~~~~~~~~~~~~~~~ When checking left hand side of Foo.apply: Can't match on apply (\x, y => x) a reg056.idr:7:16-25: | 7 | dodgy n m Refl impossible | ~~~~~~~~~~ dodgy n m Refl is a valid case reg056.idr:10:11-20: | 10 | nonk Refl impossible | ~~~~~~~~~~ nonk Refl is a valid case reg068.idr:1:6-8: | 1 | data nat : Type where --error | ~~~ Main.nat has a name which may be implicitly bound. This is likely to lead to problems! reg068.idr:2:8-10: | 2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat | ~~~ Main.ze has a name which may be implicitly bound. This is likely to lead to problems! reg068.idr:2:8-10: | 2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat | ~~~ nat is bound as an implicit Did you mean to refer to Main.nat? reg068.idr:2:8-10: | 2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat | ~~~ When checking constructor Main.ze: Type level variable nat is not Main.nat Mod.idr:11:1-22: | 11 | natexp k = S (natfn k) | ~~~~~~~~~~~~~~~~~~~~~~ public export Mod.natexp can't refer to export Mod.natfn reg070.idr:7:1-7: | 7 | Show Te where | ~~~~~~~ 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 reg076.idr:8:1: | 8 | | ^ Missing fixity declaration for Main.:> reg077.idr:3:1: | 3 | | ^ Missing fixity declaration for Main.:>> DoubleEquality.idr:4:83-103: | 4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl | ~~~~~~~~~~~~~~~~~~~~~ When checking right hand side of oops with expected type Void When checking argument value to function Prelude.Basics.the: Type mismatch between x = x (Type of Refl) and (-0.0) = 0.0 (Expected type) Specifically: Type mismatch between -0.0 and 0.0 Canonicity.idr:9:1-9: | 9 | f Nil = 0 | ~~~~~~~~~ Canonicity.f is not total as there are missing cases Canonicity.idr:12:1-20: | 12 | NaN = f (Cons 0 Nil) | ~~~~~~~~~~~~~~~~~~~~ Canonicity.NaN is possibly not total due to: Canonicity.f