[ fix agda#5700 ] Give proper scope to metas created by reflection

src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs

@@ -190,9 +190,16 @@ instance ToAbstract Term where
       return $ A.Pi exprNoRange (singleton a) b
     R.Sort s   -> toAbstract s
     R.Lit l    -> toAbstract l
-    R.Meta x es    -> toAbstract (A.Underscore info, es)
-      where info = emptyMetaInfo{ metaNumber = Just x }
-    R.Unknown      -> return $ Underscore emptyMetaInfo
+    R.Meta x es    -> do
+      info <- mkMetaInfo
+      let info' = info{ metaNumber = Just x }
+      toAbstract (A.Underscore info', es)
+    R.Unknown      -> Underscore <$> mkMetaInfo
+
+mkMetaInfo :: ReadTCState m => m MetaInfo
+mkMetaInfo = do
+  scope <- getScope
+  return $ emptyMetaInfo { metaScope = scope }
 
 mkDef :: HasConstInfo m => QName -> m A.Expr
 mkDef f =
@@ -231,7 +238,7 @@ instance ToAbstract Sort where
       PropS x -> mkApp (A.Def propName) <$> toAbstract x
       PropLitS x -> return $ A.Def' propName $ A.Suffix x
       InfS x -> return $ A.Def' infName $ A.Suffix x
-      UnknownS -> return $ mkApp (A.Def setName) $ Underscore emptyMetaInfo
+      UnknownS -> mkApp (A.Def setName) . Underscore <$> mkMetaInfo
 
 instance ToAbstract R.Pattern where
   type AbsOfRef R.Pattern = A.Pattern

test/interaction/Issue5700.agda

@@ -0,0 +1,13 @@
+open import Agda.Builtin.List
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Unit
+open import Agda.Builtin.Reflection
+
+pattern vArg x = arg (arg-info visible (modality relevant quantity-ω)) x
+
+macro
+  macaroo : Term → TC ⊤
+  macaroo hole = unify hole (con (quote suc) (vArg unknown ∷ []))
+
+test : Nat
+test = macaroo

test/interaction/Issue5700.in

@@ -0,0 +1 @@
+top_command (cmd_load currentFile [])

test/interaction/Issue5700.out

@@ -0,0 +1,6 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "_n_7 : Nat [ at Issue5700.agda:13,8-15 ] " nil)
+((last . 1) . (agda2-goals-action '()))