[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 ⊀"

[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 <

Post by Apostolis Xekoukoulotakis
What is a canonical type checking computation?
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

"

Post by 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 <

Post by Apostolis Xekoukoulotakis
What is a canonical type checking computation?
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
https://lists.chalmers.se/mailman/listinfo/agda