<div dir="ltr"><div><div>Ok, I removed NON_TERMINATING with TERMINATING and it does not produce that error. I was honest.<br><br></div><div>I now have another issue which is probably related to this issue :<br><a href="https://github.com/agda/agda/issues/2119">https://github.com/agda/agda/issues/2119</a><br></div><div><br></div><div>Is there a way to work with functions that have universe vars? I could remove the vars if it is not possible.<br></div><div><br></div>I get this error (in another test function): <br><br>"<br>Setω is not a valid type<br>when checking that the expression<br>{ℓ : .Agda.Primitive.Level} {A : Set ℓ} → A has type _317<br>"<br><br></div>agda debug :<br><div>"<br>term _315 r :DirEq .Agda.Primitive.lzero<br>term _315 r :DirEq .Agda.Primitive.lzero<br>solving _315 := λ r ⦃ f ⦄ ⦃ g₁ ⦄ ⦃ e₁ ⦄ → .Agda.Primitive.lzero<br>compareTerm<br> Set =< Set<br> : Set (.Agda.Primitive.lsuc .Agda.Primitive.lzero)<br>Solving awake constraints. 0 remaining.<br>}<br>coerce term v = (r : RoleA) ⦃ f : PF ar ⊤ (λ z → Nat) tm r ⦄<br> ⦃ g = g₁ : PF br ⊤ (λ z → Nat) tm r ⦄<br> ⦃ e = e₁ : PF cr (Nat × Nat × Nat) (λ z → Nat) tm r ⦄ →<br> PF cr Nat (λ z → Nat) tm r<br> from type t1 = Set<br> to type t2 = _310<br>term _309 :DirEq .Agda.Primitive.lsuc .Agda.Primitive.lzero<br>term _309 :DirEq .Agda.Primitive.lsuc .Agda.Primitive.lzero<br>solving _309 := .Agda.Primitive.lsuc .Agda.Primitive.lzero<br>compareTerm Set =< _310 : Set₁<br>term _310 :DirGeq Set<br>term _310 :DirGeq Set<br>solving _310 := Set<br>Solving awake constraints. 0 remaining.<br>}<br>{ checkExpr<br>{ checkExpr<br>inferred def .Agda.Primitive.Level<br> : Set<br> --> .Agda.Primitive.Level<br>term _318 :DirEq .Agda.Primitive.lzero<br>term _318 :DirEq .Agda.Primitive.lzero<br>solving _318 := .Agda.Primitive.lzero<br>compareTerm Set =< Set : Set₁<br>Solving awake constraints. 0 remaining.<br>}<br>{ checkExpr<br>coerce term v = ℓ<br> from type t1 = .Agda.Primitive.Level<br> to type t2 = .Agda.Primitive.Level<br>compareTerm .Agda.Primitive.Level =< .Agda.Primitive.Level : Set<br>Solving awake constraints. 0 remaining.<br>}<br>{ checkExpr<br>term _319 :DirEq ℓ<br>term _319 :DirEq ℓ<br>solving _319 := λ {ℓ} {A} → ℓ<br>compareTerm Set ℓ =< Set ℓ : Set (.Agda.Primitive.lsuc ℓ)<br>Solving awake constraints. 0 remaining.<br>}<br>coerce term v = {ℓ : .Agda.Primitive.Level} {A : Set ℓ} → A<br> from type t1 = Setω<br> to type t2 = _317<br>term _316 :DirEq Setω<br>term _316 :DirEq Setω<br>solving _316 := Setω<br>compareTerm Setω =< _317 : Setω<br>term _317 :DirGeq Setω<br>term _317 :DirGeq Setω<br>term _317 :DirGeq Setω<br>term _317 :DirGeq Setω<br>}<br>}<br>}<br>cacheCurrentTypeCheckLog<br><br>"<br><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 16, 2018 at 2:51 PM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@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"><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"><div><div class="h5">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@<wbr>gmail.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><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/Pr<wbr>otocol/blob/16866832963d7f4950<wbr>73485f0c3620c8cb7d9874/test1.<wbr>agda#L17</a><br><a href="https://github.com/xekoukou/Protocol/blob/16866832963d7f495073485f0c3620c8cb7d9874/TypeCheck.agda#L298" target="_blank">https://github.com/xekoukou/Pr<wbr>otocol/blob/16866832963d7f4950<wbr>73485f0c3620c8cb7d9874/<wbr>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></div></div>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>