<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hi all, <div><br></div><div>Based on Language Reference, I expect that the following fragment </div><div><br></div></div></div></div></div></div></div><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px"><div><div><div><div><div><div><div><div><font face="monospace, monospace">macro</font></div></div></div></div></div></div></div></div><div><div><div><div><div><div><div><font face="monospace, monospace">  showGoal : Term → TC ⊤</font></div></div></div></div></div></div></div><div><div><div><div><div><div><div><font face="monospace, monospace">  showGoal hole =</font></div></div></div></div></div></div></div><div><div><div><div><div><div><div><font face="monospace, monospace">    (inferType hole) >>= λ goal → typeError [ termErr goal ]</font></div></div></div></div></div></div></div></blockquote><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>binds the reflected goal to `goal`, but I always get a meta-variable instead even if the goal is simply ℕ. Is this the expected behaviour? </div><div><br></div></div></div></div></div></div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Best regards,<br></div>Liang-Ting</div></div></div></div></div></div></div></div></div></div></div></div></div>