[ test ] Add an example revealed to be failing

Author: buzden

tests/Main.idr

@@ -251,7 +251,7 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing
        "reflection009", "reflection010", "reflection011", "reflection012",
        "reflection013", "reflection014", "reflection015", "reflection016",
        "reflection017", "reflection018", "reflection019", "reflection020",
-       "reflection021"]
+       "reflection021", "reflection022"]
 
 idrisTestsWith : TestPool
 idrisTestsWith = MkTestPool "With abstraction" [] Nothing

tests/idris2/reflection022/FailingRunElab.idr

@@ -0,0 +1,12 @@
+module FailingRunElab
+
+import ScriptDecl
+
+%default total
+
+%language ElabReflection
+
+%runElab theScript False
+
+failing "Expectedly failing"
+  %runElab theScript True

tests/idris2/reflection022/ScriptDecl.idr

@@ -0,0 +1,22 @@
+module ScriptDecl
+
+import public Language.Reflection
+import SomeNonPublicExportLib
+
+%default total
+
+f : Bool -> Elab Bool
+f x = do
+  logMsg "reflection" 0 "f \{show x}"
+  pure x
+
+export
+theScript : (shouldFail : Bool) -> Elab ()
+theScript b = do
+  b <- traverseList [b] f
+  case any id b of
+    True  => fail "Expectedly failing"
+    False => declare `[
+        x : Nat
+        x = 5
+      ]

tests/idris2/reflection022/SomeNonPublicExportLib.idr

@@ -0,0 +1,8 @@
+module SomeNonPublicExportLib
+
+%default total
+
+export
+traverseList : Applicative f => List a -> (a -> f b) -> f $ List b
+traverseList []      _ = pure []
+traverseList (x::xs) f = [| f x :: traverseList xs f |]

tests/idris2/reflection022/expected

@@ -0,0 +1,3 @@
+1/3: Building SomeNonPublicExportLib (SomeNonPublicExportLib.idr)
+2/3: Building ScriptDecl (ScriptDecl.idr)
+3/3: Building FailingRunElab (FailingRunElab.idr)

tests/idris2/reflection022/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --check FailingRunElab.idr

tests/idris2/reflection022/test.ipkg

@@ -0,0 +1 @@
+package a-test