Metas created during macro execution use the wrong scope

[jespercockx]

Here's a small example:

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

When loading this file, you get this:

_n_7 : Agda.Builtin.Nat.Nat  [ at ...:14,8-15 ]

Note that the type of the meta is Agda.Builtin.Nat.Nat, while if you give the term suc _ by hand the type you get is Nat.