[Agda] Cannot unquote non-canonical type checking computation

[Apostolis Xekoukoulotakis]

What is a canonical type checking computation?

My code that fails :
https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620c8cb7d9874/test1.agda#L17
https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620c8cb7d9874/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 ⊤"
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180316/6f809ce8/attachment.html>