Replace -type-in-type by #[local] Unset Universe Checking in all necessary files

[peterlefanulumsdaine]

(This is probably not intended for merging — it’s an experiment/proof-of-concept, companion to #1697.)

Following discussion in #1696 about replacing -type-in-type with Unset Universe Checking, #1697 tries one simple approach — adding #[export] Unset Universe Checking at the start of UniMath. One arguably undesirable effect of that is that it propagates the “unset” to any other development importing us.

This PR demonstrates a crude alternative #[local] Unset Universe Checking in all files that need it, determined just by running make without -type-in-type and seeing what breaks. (Thanks to @JasonGross for a quick script for this!)

Personally I don’t think this version is very nice as stands: it adds Unset Universe Checking in 382 files — over a third of our *.v files. I guess that this could be improved a lot, with some work — that fine-tuning the use of universe-checking in Foundations, and in particular adding universe polymorphism for a few core definitions, would mean most later files should then compile OK with universe checking enabled. That would take a bit more work, and would also involve making mathematically-meaningful decisions affecting Foundations.

[benediktahrens]

@peterlefanulumsdaine : Thanks a lot for preparing this PR!

This PR demonstrates a crude alternative #[local] Unset Universe Checking in all files that need it, determined just by running make without -type-in-type and seeing what breaks. (Thanks to @JasonGross for a quick script for this!)

is this approach cruder than the one proposed in #1697 ? It seems to me that it is slightly less crude than that other one, but maybe I am missing something?

[nmvdw]

In Bicategories/Core/Bicat.v, removing #[local] Unset Universe Checking. would give an error at this line:

Definition prebicat_2cell_struct (C : precategory_ob_mor)
  : UU
  := ∏ (a b: C), C⟦a, b⟧ → C⟦a, b⟧ → UU.

namely

Error:
In environment
C : precategory_ob_mor
The term "∏ a b : C, C ⟦ a, b ⟧ → C ⟦ a, b ⟧ → UU" has type "Type"
while it is expected to have type "UU" (universe inconsistency: Cannot enforce UU.u0 <
UU.u0 because UU.u0 = eqweqmap_transportb.u0 = UU.u0).

The following definitions would have been accepted:

Definition prebicat_2cell_struct (C : precategory_ob_mor)
  : Type
  := ∏ (a b: C), C⟦a, b⟧ → C⟦a, b⟧ → UU.

Definition prebicat_2cell_struct (C : precategory_ob_mor)
  : Type
  := ∏ (a b: C), C⟦a, b⟧ → C⟦a, b⟧ → Type.

Definition prebicat_2cell_struct (C : precategory_ob_mor)
  : UU
  := ∏ (a b: C), C⟦a, b⟧ → C⟦a, b⟧ → Type.

If one uses the first one, then an error comes up here:

Definition prebicat_1_id_comp_cells : UU
  := ∑ (C : precategory_data), prebicat_2cell_struct C.

namely

Error:
In environment
C : precategory_data
The term "prebicat_2cell_struct C" has type "Type" while it is expected to have type 
"UU" (universe inconsistency: Cannot enforce prebicat_2cell_struct.u0 <= UU.u0 because UU.u0
< prebicat_2cell_struct.u0).

For the other variations, an error comes up in line 406 where use tpair is used:

Error: Illegal application (Non-functional construction): 
The expression "?pr10,, ?pr22" of type "∑ y, ?P y" cannot be applied to the term
 "?y" : "?T0"

This error becomes clearer when I use simple refine (_ ,, _) instead:

Error:
In environment
ob : UU
mor : ob → ob → UU
cell : ∏ X Y : ob, mor X Y → mor X Y → UU
id₁ : ∏ X : ob, mor X X
comp : ∏ X Y Z : ob, mor X Y → mor Y Z → mor X Z
id₂ : ∏ (X Y : ob) (f : mor X Y), cell X Y f f
vcomp : ∏ (X Y : ob) (f g h : mor X Y), cell X Y f g → cell X Y g h → cell X Y f h
lwhisk : ∏ (X Y Z : ob) (f : mor X Y) (g h : mor Y Z),
         cell Y Z g h → cell X Z (comp X Y Z f g) (comp X Y Z f h)
rwhisk : ∏ (X Y Z : ob) (g h : mor X Y) (f : mor Y Z),
         cell X Y g h → cell X Z (comp X Y Z g f) (comp X Y Z h f)
lunitor : ∏ (X Y : ob) (f : mor X Y), cell X Y (comp X X Y (id₁ X) f) f
lunitor_inv : ∏ (X Y : ob) (f : mor X Y), cell X Y f (comp X X Y (id₁ X) f)
runitor : ∏ (X Y : ob) (f : mor X Y), cell X Y (comp X Y Y f (id₁ Y)) f
runitor_inv : ∏ (X Y : ob) (f : mor X Y), cell X Y f (comp X Y Y f (id₁ Y))
lassocor : ∏ (W X Y Z : ob) (f : mor W X) (g : mor X Y) (h : mor Y Z),
           cell W Z (comp W X Z f (comp X Y Z g h)) (comp W Y Z (comp W X Y f g) h)
rassocor : ∏ (W X Y Z : ob) (f : mor W X) (g : mor X Y) (h : mor Y Z),
           cell W Z (comp W Y Z (comp W X Y f g) h) (comp W X Z f (comp X Y Z g h))
The term "?pr10,, ?pr22" has type "∑ y, ?P y" while it is expected to have type
 "precategory_ob_mor" (unable to find a well-typed instantiation for 
"?T": cannot ensure that "Type" is a subtype of "UU").

If one imports UniMath in projects that do not make use of type-in-type, then one meets similar errors.

I think that most of these files need #[local] Unset Universe Checking. for similar reasons.

[nmvdw]

This is my attempt to reduce these errors to some kind of minimal example.

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Fail Definition ob_mor
  : UU
  := ∑ (ob : UU), ob → ob → UU.

Fail Definition ob_mor
  : UU
  := ∑ (ob : Type), ob → ob → UU.

Fail Definition ob_mor
  : UU
  := ∑ (ob : UU), ob → ob → Type.

Definition ob_mor
  : UU
  := ∑ (ob : Type), ob → ob → Type.

Fail Definition make_ob_mor
                (ob : UU)
                (mor : ob → ob → UU)
  : ob_mor
  := ob ,, mor.

Definition make_ob_mor
           (ob : Type)
           (mor : ob → ob → Type)
  : ob_mor
  := ob ,, mor.

#[local] Unset Universe Checking.
Definition ob_mor' : UU
  := ∑ ob : UU, ob -> ob -> UU.
#[local] Set Universe Checking.

Definition make_ob_mor'
           (ob : UU)
           (mor : ob → ob → UU)
  : ob_mor'.
Proof.
  Fail use tpair.
  #[local] Unset Universe Checking.
  use tpair.
  - exact ob.
  - exact mor.
Defined.

#[local] Unset Universe Checking is necessary if one makes use of UU in either function types or sigma types. In addition, #[local] Unset Universe Checking is inherited: if one uses such a definition in a file that uses #[local] Unset Universe Checking, then all files that depend on it, will most likely also need to use #[local] Unset Universe Checking. in order to use that definition (or suitable builders need to be provided).

Somehow UU and Type seem to behave differently with respect to universe checking.

[peterlefanulumsdaine]

@benediktahrens I find this at least as crude as #1697 (which doesn’t necessarily mean worse). Anything done 99% with a script, adding one line of code repeated in hundreds of files, surely counts as pretty crude.

@nmvdw Yes — I inspected universe errors in a few individual files (fairly haphazardly, not especially representative), and most of them came down to:

• interaction between UU and Type (which could probably often be solved by more careful+consistent choice of which to use where)
• universe-monomorphicity of total2, paths and other core definitions (which hopefully could be fixed by making just them more universe-polymorphic)
• intentional resizing, e.g. impredicative construction of prop-truncation

So I hope a lot of them could be prevented/fixed, but probably only by making choices/changes in Foundations that potentially depart from Voevodsky’s intentions.

[benediktahrens]

Possibly stupidly simplistic idea: what if one replaces

Definition UU := Type.

with

Notation "'UU'" := Type.

or similar?

[JasonGross]

Possibly stupidly simplistic idea: what if one replaces

Definition UU := Type.

with

Notation "'UU'" := Type.

or similar?

Probably better to do Polymorphic Definition UU := Type. or Notation UU := Type (only parsing). or Notation UU := Type., but surely this departs from the intention to minimize the number of universes used. (Another interesting option would be to do something like this, and then use Print Sorted Universes in one of the later files to determine how to assign smaller and larger universes throughout the files.)

[peterlefanulumsdaine]

If UU were just a notation for Type, then what motivation would remain for having UU at all?

[nmvdw]

When I use Polymorphic Definition UU := Type, compilation fails for Foundations/PartB.v. The error is

Error: Universe inconsistency. Cannot enforce Set = UniMath.Foundations.PartA.7 because
UniMath.Foundations.PartA.7 < UniMath.Foundations.PartA.7 = Set.

and it happens at this line:

Require Export UniMath.Foundations.PartA.

The solution is to add

#[local] Unset Universe Checking.

right before that file.

When I change UU to a notation, I get this error in Foundations/PartD.v:

>
Error: Universe inconsistency. Cannot enforce UniMath.Foundations.PartA.24 <=
UniMath.Foundations.UnivalenceAxiom.54 because UniMath.Foundations.UnivalenceAxiom.54
<= UniMath.Foundations.PartA.377 <= UniMath.Foundations.UnivalenceAxiom.108
<= UniMath.Foundations.UnivalenceAxiom.97 <= UniMath.Foundations.UnivalenceAxiom.95
<= UniMath.Foundations.UnivalenceAxiom.56 < UniMath.Foundations.PartA.333
= UniMath.Foundations.PartA.24.

which happens at the line

Require Export UniMath.Foundations.PartD.

It is solved by adding #[local] Unset Universe Checking before it (instead of after).

I had the same errors when I tried to change all occurrences of UU to Type.

[JasonGross]

You might be able to fix the errors mentioning Set with #[export] Unset Universe Minimization ToSet.

[nmvdw]

I get the same errors if I add #[export] Unset Universe Minimization ToSet. I tried putting it either in Preamble.v (around the definition of UU), in PartA.v (which got imported), and in PartB.v (where the error occurred).