Is it possible to define a cbn-able universe cast with universe checking disabled?

Using Coq
1

I was hoping to use unset universe checking to disable universes, and temporarily work in Type:Type bliss. However, occasionally my code still fails on a universe constraint even though i have disabled universe checking. I tried to minimize the problem and came up with the idea to define an identity universe cast function. And indeed it does not work; the error message “Universe constraints are not implied by the ones declared” comes up independent of whether unverse checking is set or not:

Set Universe Checking.
Fail Definition castU@{u v |}(t: Type@{u}): Type@{v} := t.
(* The command has indeed failed with message:
Universe constraints are not implied by the ones declared: u <= v *)

Unset Universe Checking.
Fail Definition castU@{u v |}(t: Type@{u}): Type@{v} := t.
(* The command has indeed failed with message:
Universe constraints are not implied by the ones declared: u <= v *)

Furthermore, if I leave all universes to be inferred, and unset universe checking Coq will nevertheless generate universe constraints, e.g., u <= u0:

Set Universe Checking.
Set Universe Polymorphism.
Definition castU(t: Type): Type := t.
Set Printing Universes.
Print castU.
(* castU@{u u0} = fun t : Type@{u} => t
        : Type@{u} -> Type@{u0}
   (* u u0 |= u <= u0 *)
*)

What am I doing wrong – or did I misunderstand the universe checking and it is still not possible to define universe casts with it disabled?

2

Indeed unsetting universe checking still tries to infer constraints, it’s just that when a constraint fails it absorbs the error.
This is done AFAIK because if you don’t infer constraints, Coq will generate humongous amounts of universes which is very slow, because there is nothing to make them unify with each other.

So for instance

Definition castU@{u v |v < u}(t: Type@{u}): Type@{v} := t.

or

Definition castU@{u v |}(t: Type@{u}): Type@{v} := ltac:(exact_no_check t).

both work

3

The @{|} making an error even with univ checking off can be considered a bug, feel free to open an issue.

4

Is it possible to work around that and still define a universe cast? I occasionally hit universe constraints in other places even though unsetting them, so I thought using a universe cast function explicitly would be a nice.

5

Not sure what you mean by cbn-able

Unset Universe Checking.
Definition castU@{u v |}(t: Type@{u}): Type@{v} := ltac:(exact_no_check t).

should work

6

Also you can report the errors you still get.

7

Thanks, I didn’t know about exact_no_check! :slight_smile:

For reference, I opened issues Error on empty constraints `@{|}` with universe checking off · Issue #17355 · coq/coq · GitHub and Unsatisfied constraints error even though Universe Checking is off · Issue #17361 · coq/coq · GitHub .

8

It’s lowering universes that’s bad, so raising universes should be safe, right?
Is it possible to raise a universe with universe checking on?
Both of these fail:

Set Universe Polymorphism.
Inductive True@{u0}: Type@{u0} := tt.

Fail Definition raise@{u0 u1 | u0 < u1} (e: True@{u0}): True@{u1} := e.
(* The term "e" has type "True@{u0}" while it is expected to have type "True@{u1}". *)

Fail Definition lower@{u0 u1 | u0 < u1} (e: True@{u1}): True@{u0} := e.
(* The term "e" has type "True@{u1}" while it is expected to have type "True@{u0}". *)
9

True is an inductive which lives in a universe, it is not itself a universe.

See also Polymorphic Universes — Coq 8.18+alpha documentation

10

(I meant ‘raise universe’ as in ‘raise the universe a term e lives in’, but maybe I’m using the terminology wrong.)

Anyway, I did not know that there are cumulativity variance annotations. I should read about them. Thanks :slight_smile: