[ re #5744 ] Also allow unquoting at top-level with erased macros

agda · Mar 14, 2022 · 3dbfa03 · 3dbfa03
1 parent 276b384
commit 3dbfa03
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 1 deletion.
diff --git a/src/full/Agda/TypeChecking/Rules/Decl.hs b/src/full/Agda/TypeChecking/Rules/Decl.hs
@@ -336,7 +336,8 @@ unquoteTop xs e = do
   lzero <- primLevelZero
   let vArg = defaultArg
       hArg = setHiding Hidden . vArg
-  m    <- checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit]
+  m    <- applyQuantityToContext zeroQuantity $
+            checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit]
   res  <- runUnquoteM $ tell xs >> evalTCM m
   case res of
     Left err      -> typeError $ UnquoteFailed err

diff --git a/test/Succeed/ErasedMacro.agda b/test/Succeed/ErasedMacro.agda
@@ -3,10 +3,26 @@ open import Agda.Builtin.List
 open import Agda.Builtin.Nat
 open import Agda.Builtin.Equality
 open import Agda.Builtin.Reflection
+open import Agda.Builtin.Sigma
 
 macro
   @0 trivial : Term → TC ⊤
   trivial = unify (con (quote refl) [])
 
 test : 42 ≡ 42
 test = trivial
+
+@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 : Set → Set
+unquoteDef F = m F