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

**URL:** <https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899>\
**Category:** Using Rocq\
**Created:** [March 7, 2023, 6:40pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899 "2023-03-07T18:40:51Z")\
**Posts on this page:** 10\
**Page:** 1

<div class="post-metadata">

**Author:** ![drcicero](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/drcicero/32/601_2.png) [@drcicero](https://discourse.rocq-prover.org/u/drcicero)\
**Post date:** [March 7, 2023, 6:40pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/1 "2023-03-07T18:40:51Z")

</div>

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:

```coq
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`:

```auto
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?

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [March 7, 2023, 9:08pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/2 "2023-03-07T21:08:34Z")

</div>

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

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

```

or

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

```

both work

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [March 7, 2023, 9:09pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/3 "2023-03-07T21:09:30Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![drcicero](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/drcicero/32/601_2.png) [@drcicero](https://discourse.rocq-prover.org/u/drcicero)\
**Post date:** [March 8, 2023, 4:32pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/4 "2023-03-08T16:32:03Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [March 8, 2023, 4:49pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/5 "2023-03-08T16:49:55Z")

</div>

Not sure what you mean by cbn-able

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

```

should work

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [March 8, 2023, 4:50pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/6 "2023-03-08T16:50:18Z")

</div>

Also you can report the errors you still get.

---

<div class="post-metadata">

**Author:** ![drcicero](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/drcicero/32/601_2.png) [@drcicero](https://discourse.rocq-prover.org/u/drcicero)\
**Post date:** [March 8, 2023, 6:07pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/7 "2023-03-08T18:07:34Z")

</div>

Thanks, I didn’t know about exact\_no\_check! 🙂

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

---

<div class="post-metadata">

**Author:** ![drcicero](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/drcicero/32/601_2.png) [@drcicero](https://discourse.rocq-prover.org/u/drcicero)\
**Post date:** [March 8, 2023, 10:05pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/8 "2023-03-08T22:05:37Z")

</div>

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:

```coq
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}". *)

```

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [March 8, 2023, 10:17pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/9 "2023-03-08T22:17:49Z")

</div>

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

See also [Polymorphic Universes — Coq 8.18+alpha documentation](https://coq.github.io/doc/master/refman/addendum/universe-polymorphism.html#cumulative-noncumulative)

---

<div class="post-metadata">

**Author:** ![drcicero](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/drcicero/32/601_2.png) [@drcicero](https://discourse.rocq-prover.org/u/drcicero)\
**Post date:** [March 8, 2023, 11:00pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/10 "2023-03-08T23:00:40Z")

</div>

(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 🙂