Fix incorrectly quoted sorts (#7203)

agda · Mar 25, 2024 · 4eb7f95 · 4eb7f95
1 parent 0b2f857
commit 4eb7f95
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 2 deletions.
diff --git a/src/full/Agda/TypeChecking/Quote.hs b/src/full/Agda/TypeChecking/Quote.hs
@@ -179,8 +179,8 @@ quotingKit = do
       quoteSort PiSort{} = pure unsupportedSort
       quoteSort FunSort{} = pure unsupportedSort
       quoteSort UnivSort{}   = pure unsupportedSort
-      quoteSort (MetaS x es) = quoteTerm $ MetaV x es
-      quoteSort (DefS d es)  = quoteTerm $ Def d es
+      quoteSort (MetaS x es) = pure unsupportedSort
+      quoteSort (DefS d es)  = pure unsupportedSort
       quoteSort (DummyS s)   =__IMPOSSIBLE_VERBOSE__ s
 
       quoteType :: Type -> ReduceM Term

diff --git a/test/Succeed/Issue7187.agda b/test/Succeed/Issue7187.agda
@@ -0,0 +1,14 @@
+open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
+open import Agda.Builtin.Unit
+open import Agda.Builtin.Nat
+open import Agda.Builtin.List
+
+macro
+  `Nat : Term → TC ⊤
+  `Nat hole = do
+    ty ← inferType hole
+    _  ← debugPrint "tactic" 10 (termErr ty ∷ [])
+    unify hole (def (quote Nat) [])
+
+boom : `Nat
+boom = 1