[Agda] Cannot unquote non-canonical type checking computation

[Ulf Norell]

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!).

/ Ulf

On Fri, Mar 16, 2018 at 1:35 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> What is a canonical type checking computation?
>
> My code that fails :
> https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620
> c8cb7d9874/test1.agda#L17
> https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620
> c8cb7d9874/TypeCheck.agda#L298
>
>
> ".../Protocol/test1.agda:17,9-23
> Cannot unquote non-canonical type checking computation
>   findAllNamesRec .Agda.Builtin.List.List.[] (quote test)
> when checking that the expression unquote (typeCheck (quote test))
> has type ⊤"
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180316/867a8e80/attachment.html>