<div dir="ltr"><div>It means that evaluation got stuck without producing a primitive TC operation (i.e. a canonical value of type TC A). In your case `findAllNamesRec` didn't reduce. This is because you marked it {-# NON_TERMINATING #-}, which tells the type checker that it's not safe to unfold it. If you use {-# TERMINATING #-} instead, this tells the type checker that, although it might not look like it, it is in fact perfectly safe to unfold the function and it would never ever loop (honest!).<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 16, 2018 at 1:35 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">What is a canonical type checking computation?<br><br>My code that fails :<br><a href="https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620c8cb7d9874/test1.agda#L17" target="_blank">https://github.com/xekoukou/<wbr>Protocol/blob/<wbr>16866832963d7f495073485f0c3620<wbr>c8cb7d9874/test1.agda#L17</a><br><a href="https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620c8cb7d9874/TypeCheck.agda#L298" target="_blank">https://github.com/xekoukou/<wbr>Protocol/blob/<wbr>16866832963d7f495073485f0c3620<wbr>c8cb7d9874/TypeCheck.agda#L298</a><br><br><br>".../Protocol/test1.agda:17,9-<wbr>23<br>Cannot unquote non-canonical type checking computation<br>  findAllNamesRec .Agda.Builtin.List.List.[] (quote test)<br>when checking that the expression unquote (typeCheck (quote test))<br>has type ⊤"<br></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>