Stream: Coq users

Topic: stdpp universe inconistency with ID and fin_maps

Karl Palmskog (Nov 16 2023 at 11:46):

I'm using stdpp 1.9.0 and have the following file called inclsys.v:

From stdpp Require Import base.
Class InclSys
  `(A : index -> Type)
  (IS : forall (ifrom ito : index), option (A ifrom -> A ito))
  : Prop :=
incl_sys_id : forall i, IS i i = Some id.

I then compile the file and do the following in another file test.v:

From stdpp Require Import fin_maps.
Require Import inclsys.

However, I then get the following error on the second statement:

File "./test.v", line 2, characters 0-19:
Error: Universe inconsistency. Cannot enforce ID.u0 <= option.u0 because
option.u0 <= MapFold.u2 < Coq.Relations.Relation_Definitions.1 <= ID.u0.

Any hints what could be the problem here? Are fin_maps in Stdpp 1.9.0 using fancy universe tricks that act at a distance?

Gaëtan Gilbert (Nov 16 2023 at 11:50):

if you make the class universe polymorphic, Set Printing Universes, what does About InclSys say? (in its own file)
like

Polymorphic Definition foo : Type := Type.
Set Printing Universes.
About foo.
(* ...
(* u u0 |= u0 < u *)
...
*)

Karl Palmskog (Nov 16 2023 at 11:53):

I assume you mean like this:

From stdpp Require Import base.
Polymorphic Class InclSys
  `(A : index -> Type)
  (IS : forall (ifrom ito : index), option (A ifrom -> A ito))
  : Prop :=
incl_sys_id : forall i, IS i i = Some id.
Set Printing Universes.
About InclSys.
(*
InclSys@{u u0} :
∀ {index : Type@{u}} (A : index → Type@{u0}),
  (∀ ifrom ito : index, option (A ifrom → A ito)) → Prop
(* u u0 |= ID.u0 <= option.u0
           u0 <= eq.u0
           u0 <= option.u0
           u0 <= ID.u0 *)

InclSys is universe polymorphic
Arguments InclSys {index}%type_scope (A IS)%function_scope
InclSys is transparent
*)

Karl Palmskog (Nov 16 2023 at 11:56):

if it matters to anyone, the error only happens when using stdpp 1.9.0, not 1.8.0. The root cause may be introduction of fancy maps as described here

Gaëtan Gilbert (Nov 16 2023 at 11:56):

what is index? just a generalized variable?

Karl Palmskog (Nov 16 2023 at 11:57):

yes, stdpp base does the following: Global Generalizable All Variables.

Gaëtan Gilbert (Nov 16 2023 at 12:01):

it may help to eta expand id:

Global Generalizable All Variables.
Arguments id {_}.

Polymorphic Class InclSys
  `(A : index -> Type)
  (IS : forall (ifrom ito : index), option (A ifrom -> A ito))
  : Prop :=
  incl_sys_id : forall i, IS i i = Some id.

Polymorphic Class InclSys'
  `(A : index -> Type)
  (IS : forall (ifrom ito : index), option (A ifrom -> A ito))
  : Prop :=
  incl_sys_id' : forall i, IS i i = Some (fun x => id x).

Set Printing Universes.
About InclSys.
(* u u0 |= ID.u0 <= option.u0
           u0 <= eq.u0
           u0 <= option.u0
           u0 <= ID.u0 *)

About InclSys'.
(* u u0 |= u0 <= eq.u0
           u0 <= option.u0
           u0 <= ID.u0 *)

Karl Palmskog (Nov 16 2023 at 12:06):

Here is an example of the error that only depends on stdpp's fin_maps and Stdlib, inclsys.v:

From Coq Require Import Morphisms.
Global Generalizable All Variables.
Class InclSys
  `(A : index -> Type)
  (IS : forall (ifrom ito : index), option (A ifrom -> A ito))
  : Prop :=
incl_sys_id : forall i, IS i i = Some id.

and in test.v:

From stdpp Require Import fin_maps.
Require Import inclsys.

and we get:

File "./test.v", line 2, characters 0-19:
Error: Universe inconsistency. Cannot enforce ID.u0 <= option.u0 because
option.u0 <= MapFold.u2 < Coq.Relations.Relation_Definitions.1 <= ID.u0.

Karl Palmskog (Nov 16 2023 at 12:07):

if I do Polymorphic Class InclSys, I don't get the error, but that was maybe already assumed above.

Gaëtan Gilbert (Nov 16 2023 at 12:08):

do you even need to import Morphisms? I guess it just sets the implicit argument of id to be maximal
through Program.Basics

if I do Polymorphic Class InclSys, I don't get the error, but that was maybe already assumed above.

yes, it's only to get it the print the univs associated to it (monomorphics don't have a proper concept of "univ associated to it")

Karl Palmskog (Nov 16 2023 at 12:09):

you're right, this suffices:

Arguments id {_}.
Global Generalizable All Variables.

Karl Palmskog (Nov 16 2023 at 12:10):

am testing the fun x => id x thing now

Gaëtan Gilbert (Nov 16 2023 at 12:10):

you can try doing Constraint ID.u0 <= option.u0 at the top of fin_maps and see if it makes an error (then the error may be at a problem location more precise than the whole file)
it's possible that it will silently eta expand something instead though

Gaëtan Gilbert (Nov 16 2023 at 12:15):

if it silently eta expand you can instead binary search to find the first command after which adding the constraint errors but this takes more effort

Karl Palmskog (Nov 16 2023 at 12:15):

in the much larger example this was extracted from, replacing id with fun x => id x everywhere makes the problem go away

Karl Palmskog (Nov 16 2023 at 12:16):

will try to do the Constraint thing in stdpp now

Gaëtan Gilbert (Nov 16 2023 at 12:16):

I guess if you do that you start wondering why not do fun x => x instead though ;)

Karl Palmskog (Nov 16 2023 at 12:23):

I guess the following is what one might call the stdpp bug report:

From stdpp Require Import fin_maps.
Constraint ID.u0 <= option.u0.
(* Error: Universe inconsistency. Cannot enforce ID.u0 <= option.u0 because option.u0
<= MapFold.u2 < Coq.Relations.Relation_Definitions.1 <= ID.u0. *)

I couldn't easily find any place inside fin_maps.v that the constraint fails though, the file is 4500+ LOC long...

Karl Palmskog (Nov 16 2023 at 12:24):

will keep looking for a while

Karl Palmskog (Nov 16 2023 at 12:30):

from what I can tell (not exhaustively tested), Constraint ID.u0 <= option.u0. doesn't fail anywhere inside fin_maps.v...

Gaëtan Gilbert (Nov 16 2023 at 12:35):

even at the end? weird

Karl Palmskog (Nov 16 2023 at 12:36):

nope, not even at the end.

Karl Palmskog (Nov 16 2023 at 12:38):

I was going to write a stdpp issue, how could I summarize this? "It's not very nice to clients to add universe constraints in a module"?

Gaëtan Gilbert (Nov 16 2023 at 12:40):

you say it makes stdpp incompatible with writing Some id

Karl Palmskog (Nov 16 2023 at 12:49):

https://gitlab.mpi-sws.org/iris/stdpp/-/issues/201

Karl Palmskog (Nov 16 2023 at 13:09):

based on the discussion in the Stdpp issue report, this may be an issue with Coq, should I report?

Gaëtan Gilbert (Nov 16 2023 at 13:12):

no

Ralf Jung (Nov 16 2023 at 13:53):

I think this is a new instance of an old issue: https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80

Ralf Jung (Nov 16 2023 at 13:54):

this pinning of template universes regularly prevents combining independently developed coq libraries

Ralf Jung (Nov 16 2023 at 13:55):

sadly there's little that Coq libraries can do here (other than "don't add instances for typeclasses like Monad for standard coq types", which obviously is a bad outcome), as far as I can tell. the only proper fix is transitioning coq standard types like list and option to proper universe polymorphism.

Karl Palmskog (Nov 16 2023 at 13:57):

as stdpp users, we ended up with the following workaround:

#[local] Notation id := (fun x => id x).

Last updated: Oct 13 2024 at 01:02 UTC