Please add some test cases showing that one cannot use this new feature to turn erased values into run-time values. Some ideas (untested):

• 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

• 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

• 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

• 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

Here are the results of trying your test cases:

1. You get an error when running the macro (as opposed to an error when defining the macro if the macro is not itself erased)
2. You get an error that A is erased, but the error location is wrong (on the binding site of A rather than on the use site).
3. Same as in 2.
4. Complains that identifier m is erased, the reason for this being that I only changed the behavior of unquote and macros but not of unquoteDef.

I've fixed the error location and added support for using unquoteDef and unquoteDecl with erased macros, so all your examples now produce the expected error during execution of the macro.

The only failed test in CI is because of this error:

E: Failed to fetch http://security.ubuntu.com/ubuntu/pool/main/g/ghostscript/libgs9-common_9.26~dfsg+0-0ubuntu0.18.04.14_all.deb  404  Not Found [IP: 52.252.75.106 80]
E: Failed to fetch http://security.ubuntu.com/ubuntu/pool/main/g/ghostscript/libgs9_9.26~dfsg+0-0ubuntu0.18.04.14_amd64.deb  404  Not Found [IP: 52.252.75.106 80]

I assume this is unrelated so I am going to merge this PR now.