<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">https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620c8cb7d9874/test1.agda#L17</a><br><a href="https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620c8cb7d9874/TypeCheck.agda#L298">https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620c8cb7d9874/TypeCheck.agda#L298</a><br><br><br>".../Protocol/test1.agda:17,9-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>