The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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.
>