-
Notifications
You must be signed in to change notification settings - Fork 172
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Replace -type-in-type
by #[local] Unset Universe Checking
in all necessary files
#1698
base: master
Are you sure you want to change the base?
Replace -type-in-type
by #[local] Unset Universe Checking
in all necessary files
#1698
Conversation
…kage [WIP, build broken]
… [WIP, build broken]
Folds, SubstitutionSystems
…T, Bicats, HomAlg
…ing it for library)
@peterlefanulumsdaine : Thanks a lot for preparing this PR!
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? |
In 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
For the other variations, an error comes up in line 406 where
This error becomes clearer when I use 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 I think that most of these files need |
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.
Somehow |
@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:
So I hope a lot of them could be prevented/fixed, but probably only by making choices/changes in |
Possibly stupidly simplistic idea: what if one replaces
with
or similar? |
Probably better to do |
If |
When I use 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:
The solution is to add
right before that file. When I change >
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
It is solved by adding I had the same errors when I tried to change all occurrences of |
You might be able to fix the errors mentioning |
I get the same errors if I add |
(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
withUnset 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 runningmake
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 inFoundations
, 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 affectingFoundations
.