The Coq mailing list

[Nathanaël Courant <nathanael.courant AT ens.fr>]

Hi,

The issue is reported at
https://github.com/coq/coq/issues/7875 ; I included as many details as 
possible. It looks like it was not map's second parameter that was 
constrained, but the parameter of eq itself (!).

Thanks,
Nathanaël

On 20/06/2018 14:55, Matthieu Sozeau wrote:
> Hi,
>
> This looks like a bug, probably linked to template polymorphism, could you
> report it at github.com/coq/coq/issues please? Those are rather hard to
> debug, but not impossible. If you Print Universes, it’s likely that the
> stdlib universe for map’s second parameter (...List.270 I believe) is
> constrained from above by one of Vpl’s universes, and this should not
> happen. One has to find the definition in Vpl that forces that and fix it,
> certainly by fixing a tactic.
>
> Best regards,
> — Matthieu
> Le mer. 20 juin 2018 à 12:25, Nathanaël Courant 
> <nathanael.courant AT ens.fr>
> a écrit :
>
> > Looking through the code, it looks like the problem is caused by the use
> > of setoid_rewrite in multiple places. For instance, trying to put the
> > snippet below at the end of Map_poly.v produces an universe inconsistency.
> >
> > Require Import ImpureConfig.
> > Require Import List.
> > Definition f (x : unit) : imp unit := pure x.
> > Definition g l := map f l
> >
> > However, changing the proof of mapsto_add_compat in the same file to
> > avoid using "rewrite ... at 1", which does a setoid_rewrite with the
> > equality relation, is enough to make the inconsistency error disappear.
> > I am a bit clueless as to why setoid_rewrite poses such problems though,
> > and why map is specifically affected.
> >
> > Thanks,
> > Nathanaël
> >
> > On 20/06/2018 10:59, Sylvain Boulmé wrote:
> > > Hi Nathanaël,
> > >
> > > I am not an expert on universe issues. But this is very strange, because
> > > it seems somehow specific to "map". I do not understand why.
> > >
> > > Here is a little variant of your code that is accepted by Coq: it uses
> > > "fold_right" instead of "map".
> > >
> > > Require Import Vpl.ImpureConfig.
> > > Require Import Vpl.PedraQ.
> > > Require Import List.
> > > Definition f (x : unit) : imp unit := pure x.
> > >
> > > Definition g := fold_right (fun x l => (f x)::l).
> > >
> > > A variant with "fold_left" also works !
> > >
> > > Moreover, the VPL already uses some higher-order iterator, see
> > > "swithAll" in
> > >     https://github.com/VERIMAG-Polyhedra/VPL/blob/master/coq/AssignD.v
> > >
> > > So, I do not understand where this issue comes from. I am also
> > > interested in any hint about this...
> > >
> > > Thanks,
> > >
> > > Sylvain.
> > >
> > >
> > > Le 20/06/2018 à 10:09, Nathanaël Courant a écrit :
> > > > Require Import ImpureConfig.
> > > > Require Import PedraQ.
> > > > Require Import List.
> > > > Definition f (x : unit) : imp unit := pure x.
> > > > Definition g l := map f l.