<div dir="ltr"><div>Let me give some context into this question because there may be easier solutions.</div><div><br></div><div>When I ask to get the definition of a function, I get a list of clauses. Each clause has a list of patterns and a term "t".</div><div>If I wanted to manipulate the term t (with functions that the reflection api provides) , I would have to introduce the context of that particular function. <br></div><div>Thus given the type of the function and the patterns of the clause, I need to compute the context. <br></div><div>Since types are dependent, for each pattern, a specific term that represents this pattern needs to substitute the variable with index 0, of the next type (in Pi a b).</div><div><br></div><div>So, instead of performing a substitution, I instead want to enclose the type with a lambda and then provide as argument the term I have created from the specific pattern.</div><div>This is the pat variable in the test. It just happens that the type does not depend in the previous variable.<br></div><div><br></div><div>Maybe there is an easier solution.</div><div><br></div><div>It is  important to note though, that neither the type system or the documentation or the error message provides any information that could help me correct any mistake I made in the above code.</div><div>Maybe this should be a github issue.<br></div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Jan 19, 2020 at 12:08 AM Apostolis Xekoukoulotakis <<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Can you find the error in this code :</div><div><br></div><div>```agda</div><div><br></div><div>module test where<br><br>open import Agda.Builtin.Reflection<br>open import Reflection<br>open import Prelude.Nat<br>open import Prelude.Bool<br>open import Prelude.Unit<br>open import Prelude.List<br><br>pat : Term<br>pat = pat-lam [ clause [ arg (arg-info visible relevant) (var "ii") ] (def (quote Bool) []) ] [ arg (arg-info visible relevant) (var 0 []) ]<br><br>macro<br>  mm : Term → TC ⊤<br>  mm hole<br>    = do<br>         inContext (arg (arg-info visible relevant) (def (quote Nat) []) ∷ [])<br>           (do<br>               t ← reduce pat<br>               typeError (termErr t ∷ termErr pat ∷ [])<br>                    )<br><br>test : ⊤<br>test = mm</div><div>```</div><div><br></div><div>Why do I get a meta instead of actually reducing :</div><div>```</div><div>.../test.agda:27,8-10<br>_22 _ (λ { ii → Bool }) _<br>when checking that the expression unquote mm has type ⊤</div><div>```<br></div></div></div></div>
</blockquote></div>