[ re #5744 ] Add some failing test cases

agda · Jan 18, 2022 · 382861b · 382861b
1 parent b2689af
commit 382861b
Show file tree

Hide file tree

Showing 8 changed files with 70 additions and 0 deletions.
diff --git a/test/Fail/ErasedMacro1.agda b/test/Fail/ErasedMacro1.agda
@@ -0,0 +1,15 @@
+open import Agda.Builtin.Reflection
+open import Agda.Builtin.Unit
+
+@0 A : Set₁
+A = Set
+
+macro
+
+  @0 m : Term → TC ⊤
+  m B =
+    bindTC (quoteTC A) λ A →
+    unify A B
+
+B : Set₁
+B = m
diff --git a/test/Fail/ErasedMacro1.err b/test/Fail/ErasedMacro1.err
@@ -0,0 +1,3 @@
+ErasedMacro1.agda:15,5-6
+Identifier A is declared erased, so it cannot be used here
+when inferring the type of A
diff --git a/test/Fail/ErasedMacro2.agda b/test/Fail/ErasedMacro2.agda
@@ -0,0 +1,12 @@
+open import Agda.Builtin.Reflection
+open import Agda.Builtin.Unit
+
+macro
+
+  @0 m : @0 Set → Term → TC ⊤
+  m A B =
+    bindTC (quoteTC A) λ A →
+    unify A B
+
+F : @0 Set → Set
+F A = m A
diff --git a/test/Fail/ErasedMacro2.err b/test/Fail/ErasedMacro2.err
@@ -0,0 +1,3 @@
+ErasedMacro2.agda:12,7-10
+Variable A is declared erased, so it cannot be used here
+when inferring the type of A
diff --git a/test/Fail/ErasedMacro3.agda b/test/Fail/ErasedMacro3.agda
@@ -0,0 +1,12 @@
+open import Agda.Builtin.Reflection
+open import Agda.Builtin.Unit
+
+macro
+
+  @0 m : Set → Term → TC ⊤
+  m A B =
+    bindTC (quoteTC A) λ A →
+    unify A B
+
+F : @0 Set → Set
+F A = m A
diff --git a/test/Fail/ErasedMacro3.err b/test/Fail/ErasedMacro3.err
@@ -0,0 +1,3 @@
+ErasedMacro3.agda:12,7-10
+Variable A is declared erased, so it cannot be used here
+when inferring the type of A
diff --git a/test/Fail/ErasedMacro4.agda b/test/Fail/ErasedMacro4.agda
@@ -0,0 +1,19 @@
+open import Agda.Builtin.List
+open import Agda.Builtin.Reflection
+open import Agda.Builtin.Sigma
+open import Agda.Builtin.Unit
+
+@0 m : Name → TC ⊤
+m F = defineFun F
+  (clause
+     (( "A"
+      , arg (arg-info visible (modality relevant quantity-0))
+          (agda-sort (lit 0))) ∷
+      [])
+     (arg (arg-info visible (modality relevant quantity-0)) (var 0) ∷
+      [])
+     (var 0 []) ∷
+   [])
+
+F : @0 Set → Set
+unquoteDef F = m F
diff --git a/test/Fail/ErasedMacro4.err b/test/Fail/ErasedMacro4.err
@@ -0,0 +1,3 @@
+ErasedMacro4.agda:19,1-19
+Variable A is declared erased, so it cannot be used here
+when checking that the expression A has type Set