The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi Matthieu,

Thank you very much for your explanation, this seems to be pretty much
exactly what is happening. I don't yet know whether that will allow me
to achieve what I was trying to do last month, but at least I now have
small example exhibiting exactly the behavior you describe.

Naturally, this leads to the question whether there are other
circumstances where the universe constraints inferred for a particular
definition are stronger than what could be inferred or can be inferred
for a convertible definition (or a slight variation).

Also, do you think it would make sense to name the universes of the most
important template polymorphic inductive types (e.g., eq, list, etc.).
That is, replace the definition of eq with:

Universe eq.
Inductive eq (A : Type@{eq}) (x : A) : A -> Prop :=  eq_refl : eq A x x.

If I understand the mechanisms correctly, this by itself should not
introduce any compatibility issues and might help understand the output
of "Print Universes".

Similarly, reusing this universe for basic lemmas might be a way to
avoid introducing unnecessary universes without introducing too many
compatibility issues, but I'm less sure about that.

Best,
Christian


On 17/10/18 12:00, Matthieu Sozeau wrote:
> Hi Christian,
> 
>   this is a bit surprising but I don't think it is a bug. I guess what
> happens is that your use 
> of @eq partially applied in foo, results in a cumulativity test of the form 
> Type@{Coq.Init.Logic.8} -> ? <= Type@{U} -> ? 
> 
> Which by default forces U = Coq.Init.Logic.8. If you enforce your
> constraint, it might force
> that assignment U = Coq.Init.Logic.8 to fail, and in that case the Coq
> typechecker will backtrack
> and eta-expand @eq to (fun A : U => @eq A) and only enforce U <=
> Coq.Init.Logic.8. You can 
> confirm this by looking at the definition of foo in the first case, it
> should have this eta expansion.
> The conclusion is that you should avoid partial applications of
> "template" polymorphic constants
> like eq, that's one of the quirks of the feature.
> 
> Best regards,
> -- Matthieu
> 
> On Tue, Sep 11, 2018 at 4:04 PM Christian Doczkal
> <christian.doczkal AT ens-lyon.fr
>  
> <mailto:christian.doczkal AT ens-lyon.fr>>
> wrote:
> 
>     Hello,
> 
>     I stumbled across another universe behavior where I am not sure whether
>     this is a bug or not.
> 
>     I have declared a bunch of Universes, say L,S,M and U and used them in a
>     bunch of definitions. This ensures that U,S <= L as can be witnessed by:
> 
>     Fail Constraint L < S.
>     Fail Constraint L < U.
> 
>     Now I can enforce S = L before some definition:
> 
>     Constraint S = L.
>     Definition foo := Foo Type@{U} ... (@eq)
>     Constraint S = L.
> 
>     In this case, everything typechecks. However, if I remove the first
>     line, then the universe constraints imposed by foo change (become
>     stronger) and the third line yields a universe inconsisteny.
> 
>     In the first case, the constraints imposed by foo are:
>       U < M and U <= Coq.Init.Logic.8 (the argument of eq)
> 
>     Without the constraint "S = L", I get
>       U < M and U = Coq.Init.Logic.8
> 
>     So S = L is consistent with foo, but ruled out by it unless enforced
>     before.
> 
>     The concrete example is again too large, but having discovered the
>     "Constraint" command, coming up with a reasonably sized example may be
>     feasible.
> 
>     Best,
>     Christian
> 
>     PS. It would be nice if the automatically generated universe names were
>     actually names in the Coq sense, so that one could use them with the
>     Constraint command.
> 
>     On 10/09/18 14:53, Matthieu Sozeau wrote:
>     > Dear Christian,
>     >
>     > There is documentation in dev/doc/universes about the changes
>     necessary.
>     > The main idea is that if your tactic produces a term with polymorphic
>     > constants in it, it must produce one fresh instance of the constant at
>     > each use. Before giving the final proof term containing those fresh
>     > instances, you can call a type inference function to gather the
>     universe
>     > constraints necessary for the whole term to typecheck automatically.
>     > Maybe a look at the OCaml code you use could help us fix this.
>     > The « cannot ensure that i <= j » error could also be because that
>     > constraint is not present in the graph you produce in a tactic I
>     believe.
>     >
>     > The order-of-Imports issue is a bug for sure. Note that if you have a
>     > module A with everything polymorphic then importing it incurs no
>     global
>     > constraints so the bug couldn’t happen in that case.
>     >
>     > Best,
>     > — Matthieu
>     > Le lun. 10 sept. 2018 à 14:28, Christian Doczkal
>     > 
> <christian.doczkal AT ens-lyon.fr
>     
> <mailto:christian.doczkal AT ens-lyon.fr>
>     
> <mailto:christian.doczkal AT ens-lyon.fr
>     
> <mailto:christian.doczkal AT ens-lyon.fr>>>
>  a
>     > écrit :
>     >
>     >     Hi,
>     >     >> - Require Import A B. succeeds
>     >     >> - Require Import B A. fails
>     >     >
>     >     > That sounds like a bug, you can open an issue on github with
>     >     > reproduction instructions and we will look into it.
>     >
>     >     Unfortunately, that's an internal repository with well over
>     10K lines,
>     >     and the problem occurs at the end. Should I manage to find a small
>     >     example, I will open an issue.
>     >
>     >     >> globalization of polymorphic reference <ID> would forget
>     universes.
>     >     >
>     >     > Unfortunately various tactics and commands do not support or
>     badly
>     >     > support universe polymorphism. This error means some
>     function hasn't
>     >     > been adapted. It should probably be an anomaly.
>     >     > Depending on what exactly is failing it may be possible for
>     us to fix
>     >     > it, or it could be beyond our current manpower.
>     >
>     >     This happens when calling one of our own tactics written in
>     OCaml. So
>     >     how does one have to adapt tactics in order to properly
>     support universe
>     >     polymorphism? (The error occurred while trying to see what
>     happens if I
>     >     make just about everything universe polymorphic, so it may or
>     may not be
>     >     necessary to fix this)
>     >
>     >     Thanks for the pointers,
>     >     Christian
>     >
>

Attachment: signature.asc
Description: OpenPGP digital signature