From 980ef1b4d235af53c54525f5518b9c6001c45677 Mon Sep 17 00:00:00 2001
From: Viktor Yudov <me@spcfox.com>
Date: Mon, 18 Nov 2024 16:12:45 +0300
Subject: [PATCH] [ test ] Add failing tests for quantities of proofs

---
 tests/idris2/with/with012/WithProof0Fail.idr | 28 ++++++++++++++++++++
 tests/idris2/with/with012/WithProof1Fail.idr | 19 +++++++++++++
 tests/idris2/with/with012/expected           |  2 ++
 tests/idris2/with/with012/run                |  2 ++
 4 files changed, 51 insertions(+)
 create mode 100644 tests/idris2/with/with012/WithProof0Fail.idr
 create mode 100644 tests/idris2/with/with012/WithProof1Fail.idr

diff --git a/tests/idris2/with/with012/WithProof0Fail.idr b/tests/idris2/with/with012/WithProof0Fail.idr
new file mode 100644
index 0000000000..2cac831b57
--- /dev/null
+++ b/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
diff --git a/tests/idris2/with/with012/WithProof1Fail.idr b/tests/idris2/with/with012/WithProof1Fail.idr
new file mode 100644
index 0000000000..8d803f9c64
--- /dev/null
+++ b/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
diff --git a/tests/idris2/with/with012/expected b/tests/idris2/with/with012/expected
index 21ab08ccd7..c90e84658d 100644
--- a/tests/idris2/with/with012/expected
+++ b/tests/idris2/with/with012/expected
@@ -1,2 +1,4 @@
 1/1: Building WithProof0 (WithProof0.idr)
 1/1: Building WithProof1 (WithProof1.idr)
+1/1: Building WithProof0Fail (WithProof0Fail.idr)
+1/1: Building WithProof1Fail (WithProof1Fail.idr)
diff --git a/tests/idris2/with/with012/run b/tests/idris2/with/with012/run
index b85c518ce0..d0852365cc 100755
--- a/tests/idris2/with/with012/run
+++ b/tests/idris2/with/with012/run
@@ -2,3 +2,5 @@
 
 check WithProof0.idr
 check WithProof1.idr
+check WithProof0Fail.idr
+check WithProof1Fail.idr