[ test ] Add failing tests for quantities of proofs

Author: spcfox

tests/idris2/with/with012/WithProof0Fail.idr

@@ -0,0 +1,28 @@
+module WithProof0Fail
+
+%default total
+
+%hide List.filter
+
+data So : Bool -> Type where
+  Oh : So True
+
+eqToSo : b = True -> So b
+eqToSo Refl = Oh
+
+data All : (0 p : a -> Type) -> List a -> Type where
+  Nil  : All p Nil
+  (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs)
+
+filter : (p : a -> Bool) -> (xs : List a) -> List a
+filter p [] = []
+filter p (x :: xs) with (p x)
+  filter p (x :: xs) | False = filter p xs
+  filter p (x :: xs) | True = x :: filter p xs
+
+failing "While processing right hand side of with block in allFilter. prf is not accessible in this context"
+  allFilter : (p : a -> Bool) -> (xs : List a) -> All (So . p) (filter p xs)
+  allFilter p [] = []
+  allFilter p (x :: xs) with (p x) proof 0 prf
+    allFilter p (x :: xs) | False = allFilter p xs
+    allFilter p (x :: xs) | True = eqToSo prf :: allFilter p xs

tests/idris2/with/with012/WithProof1Fail.idr

@@ -0,0 +1,19 @@
+module WithProof1Fail
+
+%default total
+
+%hide List.filter
+
+filter : (p : a -> Bool) -> (xs : List a) -> List a
+filter p [] = []
+filter p (x :: xs) with (p x)
+  filter p (x :: xs) | False = filter p xs
+  filter p (x :: xs) | True = x :: filter p xs
+
+failing "While processing right hand side of with block in filterSquared. There are 0 uses of linear name eq"
+  filterSquared : (p : a -> Bool) -> (xs : List a) ->
+                  filter p (filter p xs) === filter p xs
+  filterSquared p [] = Refl
+  filterSquared p (x :: xs) with (p x) proof 1 eq
+    filterSquared p (x :: xs) | False = filterSquared p xs
+    filterSquared p (x :: xs) | True = filterSquared p xs