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