onlyReduceDefs should not prevent evaluation of macros

[jespercockx]

Consider the following example code:

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

make2 : Term → TC ⊤
make2 hole = bindTC (normalise (def (quote _+_) (vArg (lit (nat 1)) ∷ vArg (lit (nat 1)) ∷ []))) (unify hole)

macro
  tester : Term → TC ⊤
  tester hole = onlyReduceDefs (quote _+_ ∷ []) (make2 hole)

_ = tester

The TC action make2 hole unifies the hole with the normalization of 1 + 1, and in the macro tester this is called inside onlyReduceDefs (quote _+_ ∷ []). I would thus expect calling this macro would produce the term 2. However, we get an error instead:

Cannot unquote non-canonical type checking computation
  make2 (meta _14 [])
when checking that the expression unquote tester has type _13

What I think is happening is that the call to onlyReduceDefs prevents the call to make2 from being evaluated. This is unexpected, since onlyReduceDefs should only have an effect on calls to primitive TC operations such as reduce and normalise, not on the evaluation of the macro itself.