[Agda] When I try to reduce, I get a meta. (Reflection).

[Apostolis Xekoukoulotakis]

Can you find the error in this code :

```agda

module test where

open import Agda.Builtin.Reflection
open import Reflection
open import Prelude.Nat
open import Prelude.Bool
open import Prelude.Unit
open import Prelude.List

pat : Term
pat = pat-lam [ clause [ arg (arg-info visible relevant) (var "ii") ] (def
(quote Bool) []) ] [ arg (arg-info visible relevant) (var 0 []) ]

macro
  mm : Term → TC ⊤
  mm hole
    = do
         inContext (arg (arg-info visible relevant) (def (quote Nat) []) ∷
[])
           (do
               t ← reduce pat
               typeError (termErr t ∷ termErr pat ∷ [])
                    )

test : ⊤
test = mm
```

Why do I get a meta instead of actually reducing :
```
.../test.agda:27,8-10
_22 _ (λ { ii → Bool }) _
when checking that the expression unquote mm has type ⊤
```
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200119/5ccbf2c6/attachment.html>