Allow running of erased macros

[jespercockx]

As discussed in #5734, macros are always executed during compile time so it should be allowed to mark them as erased.

[nad]

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

[jespercockx]

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.

[jespercockx]

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.

[jespercockx]

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.