The Coq mailing list

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

If someone is touching the naming of universes it would be nice if the 
automatically generated names were actually Coq-identifiers. This would allow 
using them with the "Constraint" command. 

In the same vein, it would be nice if there were also commands like 
"Consistent Constraint U <= V" that checks whether "U <= V" is consistent but 
does not add it and "Implied Constraint U < V" that checks whether "U < V" is 
implied by the current universe constraint. 

Best,
Christian

On 10/17/2018 06:18 PM, Gaëtan Gilbert wrote:
> 
>> 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:
> 
> In https://github.com/coq/coq/issues/2829#issuecomment-350265818 I talk 
> about a branch of mine which tries to do this automatically, such that for 
> instance the universe on eq is called eq.0
> In it I mention some issues but the universe naming system has changed some 
> since so maybe it can be made to work reliably (also those issues were not 
> that bad in the first place).
> 
> I'll look into updating it and getting it into Coq.
> 
> Gaëtan Gilbert
> 
> On 17/10/2018 17:41, Christian Doczkal wrote:
>> 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