[Agda] Cannot unquote non-canonical type checking computation

[Apostolis Xekoukoulotakis]

Ok, I removed NON_TERMINATING with TERMINATING and it does not produce that
error. I was honest.

I now have another issue which is probably related to this issue :
https://github.com/agda/agda/issues/2119

Is there a way to work with functions that have universe vars? I could
remove the vars if it is not possible.

I get this error (in another test function):

"
Setω is not a valid type
when checking that the expression
{ℓ : .Agda.Primitive.Level} {A : Set ℓ} → A has type _317
"

agda debug :
"
term _315 r :DirEq .Agda.Primitive.lzero
term _315 r :DirEq .Agda.Primitive.lzero
solving _315 := λ r ⦃ f ⦄ ⦃ g₁ ⦄ ⦃ e₁ ⦄ → .Agda.Primitive.lzero
compareTerm
  Set =< Set
  : Set (.Agda.Primitive.lsuc .Agda.Primitive.lzero)
Solving awake constraints. 0 remaining.
}
coerce term      v  = (r : RoleA) ⦃ f : PF ar ⊤ (λ z → Nat) tm r ⦄
                      ⦃ g = g₁ : PF br ⊤ (λ z → Nat) tm r ⦄
                      ⦃ e = e₁ : PF cr (Nat × Nat × Nat) (λ z → Nat) tm r ⦄
→
                      PF cr Nat (λ z → Nat) tm r
       from type t1 = Set
       to type   t2 = _310
term _309 :DirEq .Agda.Primitive.lsuc .Agda.Primitive.lzero
term _309 :DirEq .Agda.Primitive.lsuc .Agda.Primitive.lzero
solving _309 := .Agda.Primitive.lsuc .Agda.Primitive.lzero
compareTerm Set =< _310 : Set₁
term _310 :DirGeq Set
term _310 :DirGeq Set
solving _310 := Set
Solving awake constraints. 0 remaining.
}
{ checkExpr
{ checkExpr
inferred def  .Agda.Primitive.Level
   :  Set
   -->  .Agda.Primitive.Level
term _318 :DirEq .Agda.Primitive.lzero
term _318 :DirEq .Agda.Primitive.lzero
solving _318 := .Agda.Primitive.lzero
compareTerm Set =< Set : Set₁
Solving awake constraints. 0 remaining.
}
{ checkExpr
coerce term      v  = ℓ
       from type t1 = .Agda.Primitive.Level
       to type   t2 = .Agda.Primitive.Level
compareTerm .Agda.Primitive.Level =< .Agda.Primitive.Level : Set
Solving awake constraints. 0 remaining.
}
{ checkExpr
term _319 :DirEq ℓ
term _319 :DirEq ℓ
solving _319 := λ {ℓ} {A} → ℓ
compareTerm Set ℓ =< Set ℓ : Set (.Agda.Primitive.lsuc ℓ)
Solving awake constraints. 0 remaining.
}
coerce term      v  = {ℓ : .Agda.Primitive.Level} {A : Set ℓ} → A
       from type t1 = Setω
       to type   t2 = _317
term _316 :DirEq Setω
term _316 :DirEq Setω
solving _316 := Setω
compareTerm Setω =< _317 : Setω
term _317 :DirGeq Setω
term _317 :DirGeq Setω
term _317 :DirGeq Setω
term _317 :DirGeq Setω
}
}
}
cacheCurrentTypeCheckLog

"


On Fri, Mar 16, 2018 at 2:51 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/16866832963d7f4950
>> 73485f0c3620c8cb7d9874/test1.agda#L17
>> https://github.com/xekoukou/Protocol/blob/16866832963d7f4950
>> 73485f0c3620c8cb7d9874/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/20180317/9fa64649/attachment.html>