[ elab ] Add test of no escaping the zero quantity

idris-lang · Oct 18, 2021 · 76f3b3b · 76f3b3b
1 parent 3854eec
commit 76f3b3b
Show file tree

Hide file tree

Showing 4 changed files with 56 additions and 0 deletions.
diff --git a/tests/Main.idr b/tests/Main.idr
@@ -212,6 +212,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
        "reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",
        "reflection009", "reflection010", "reflection011", "reflection012",
+       "reflection013",
        -- The 'with' rule
        "with001", "with002", "with004", "with005", "with006",
        -- with-disambiguation

diff --git a/tests/idris2/reflection013/NoEscape.idr b/tests/idris2/reflection013/NoEscape.idr
@@ -0,0 +1,31 @@
+||| Check that we cannot implement function illegally escaping zero quantity using elaboration reflection
+module NoEscape
+
+import Language.Reflection
+
+%language ElabReflection
+
+escScr : Elab $ (0 _ : a) -> a
+escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x)
+
+esc : (0 _ : a) -> a
+esc = %runElab escScr
+
+escd : (0 _ : a) -> a
+
+0 escd' : (0 _ : a) -> a
+
+escDecl : Name -> Elab Unit
+escDecl name = declare [
+                 IDef EmptyFC name [
+                   PatClause EmptyFC
+                     -- lhs
+                     (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x"))
+                     -- rhs
+                     `(x)
+                 ]
+               ]
+
+%runElab escDecl `{escd'}
+
+%runElab escDecl `{escd}
diff --git a/tests/idris2/reflection013/expected b/tests/idris2/reflection013/expected
@@ -0,0 +1,21 @@
+1/1: Building NoEscape (NoEscape.idr)
+Error: While processing right hand side of esc. x is not accessible in this context.
+
+NoEscape:9:65--9:66
+ 5 | 
+ 6 | %language ElabReflection
+ 7 | 
+ 8 | escScr : Elab $ (0 _ : a) -> a
+ 9 | escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x)
+                                                                     ^
+
+Error: While processing right hand side of escd. x is not accessible in this context.
+
+NoEscape:25:24--25:25
+ 21 |                    PatClause EmptyFC
+ 22 |                      -- lhs
+ 23 |                      (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x"))
+ 24 |                      -- rhs
+ 25 |                      `(x)
+                             ^
+
diff --git a/tests/idris2/reflection013/run b/tests/idris2/reflection013/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --check NoEscape.idr