[ test ] Add test for 0 proof in elaborator script

Author: spcfox

tests/idris2/with/with012/WithProof0ElabFail.idr

@@ -0,0 +1,34 @@
+module WithProof0ElabFail
+
+import Language.Reflection
+
+%default total
+
+%language ElabReflection
+
+%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"
+  %runElab declare `[
+    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/expected

@@ -2,3 +2,4 @@
 1/1: Building WithProof1 (WithProof1.idr)
 1/1: Building WithProof0Fail (WithProof0Fail.idr)
 1/1: Building WithProof1Fail (WithProof1Fail.idr)
+1/1: Building WithProof0ElabFail (WithProof0ElabFail.idr)

tests/idris2/with/with012/run

@@ -4,3 +4,4 @@ check WithProof0.idr
 check WithProof1.idr
 check WithProof0Fail.idr
 check WithProof1Fail.idr
+check WithProof0ElabFail.idr