The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Definition T1 := Type.
Definition T2 := Type.
Definition T3 := Type.

Definition T1_le_T2 : T1 -> T2 := fun x => x.
Definition T2_le_T3 : T2 -> T3 := fun x => x.

Fail Definition T3_lt_T1 : T1 := T3.
(* The term "T3" has type "Type" while it is expected to have type "T1" 
(universe inconsistency). *)

Set Printing Universes.
Fail Definition T3_lt_T1 : T1 := T3.
(* The term "T3" has type "Type@{Top.3+1}" while it is expected to have 
type
"T1" (universe inconsistency: Cannot enforce Top.3 < Top.1 because Top.1 
<= Top.2 <= Top.3).
*)


Linking constraints to specific definitions is currently not something 
Coq helps you with.

Gaëtan Gilbert

On 06/09/2018 11:18, Christian Doczkal wrote:
> Hello,
>
> I already had used "Set Printing Universes". As far as I can tell, the
> only thing "Set Printing Universes" does is cause "Print/Check term." to
> print the universe levels of all occurrences of "Type" occurring in a
> particular definition as well as the constraints enforced by a
> particular definition.
>
> I have a constraint system with thousands of constraints arising from
> hundreds of definitions and I would like to know which constraints
> contribute to the inconsistency and which definitions/lemmas give rise
> to a given constraint.
>
> For instance, Print Universes might mention
> "Coq.Relations.Relation_Definitions.1" which I could correctly guess is
> the first argument of "relation":
>
> relation =
> fun A : Type@{Coq.Relations.Relation_Definitions.1} => A -> A -> Prop
>       : Type@{Coq.Relations.Relation_Definitions.1} ->
>         Type@{max(Coq.Relations.Relation_Definitions.1,Set+1)}
>
> But its not always that easy to guess the definitions introducing a
> particular universe index and even harder to guess which definition or
> lemma enforces a given constraint.
>
> Best,
> Christian
>
>
>
>
> On 05/09/18 20:42, Gaëtan Gilbert wrote:
> > 1) yes
> >
> > 2) and 3)
> > if you enable printing of universes (Set Printing Universes. in
> > coqtop/proof general/etc, some GUI toggle in coqide) universe
> > inconsistencies should print that information
> >
> > Gaëtan Gilbert
> >
> > On 05/09/2018 17:57, Christian Doczkal wrote:
> > > Hello everyone,
> > >
> > > We have a large development where we have generic structures and some
> > > concrete instances for them. One of these is for relations (X -> Y ->
> > > Prop) with (X,Y : Set).
> > >
> > > Now I was trying to generalize this to all instances with (X,Y : Type).
> > > This leads to a universe inconsistency thousands of lines down the road.
> > > I would hope that this is merely a problem of making certain things
> > > universe polymorphic, but I don't manage to come up with a minimal
> > > example reproducing the problem.
> > >
> > > At first, I only got the rather uninformative "Universe Inconsistency"
> > > error when trying to load two separately compiled parts of the library.
> > >
> > > With some trial and error I got to the point where I have statement that
> > > type checks before the generalized instances are imported and fails to
> > > type check afterwards. This gives me an Error of the form:
> > >
> > > "... cannot ensure that "Type@{foo.2}" is a subtype of Type@{bar.3}"
> > >
> > > I can use "Print Universes" before and after the Import, but that yields
> > > thousands of constraints and even the diff is not too enlightening.
> > >
> > > If I understand the universe mechanism and the error message correctly,
> > > this actually means that assuming "foo.2 <= bar.3" is inconsistent with
> > > the current collection of universe constraints. So here are some
> > > questions:
> > >
> > > 1) Is my understanding correct?
> > >
> > > 2) If yes, is there a way to obtain a minimal (or at least sufficiently
> > > small) subset of the current collection of constraints, proving that
> > > "foo.2 <= bar.3" cannot be consistently added.
> > >
> > > 3) What other things can I do to shed some light onto what is happening?
> > >
> > > Any help would be appreciated.
> > >
> > > Best,
> > > Christian