The Coq mailing list

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

Hi all,

I am encountering universe inconsistencies while trying to write Coq 
code that depends on the VPL ( https://github.com/VERIMAG-Polyhedra/VPL ).

Once the VPL is compiled, the following code triggers an universe 
inconsistency:

Require Import ImpureConfig.
Require Import PedraQ.
Require Import List.
Definition f (x : unit) : imp unit := pure x.
Definition g l := map f l.

The error message is the following:

The term "f" has type "unit -> imp unit" while it is expected to have type
 "unit -> ?B" (unable to find a well-typed instantiation for
"?B": cannot ensure that "Type@{Vpl.Impure.2}" is a subtype of
"Type@{Coq.Lists.List.170}").

In that code, the "Require Import PedraQ." conflicts with the 
application of "map" to a function returning "imp unit" (this file 
compiles fine without PedraQ).

Thus, I have two questions:
- how can I find in the code what causes the universe inconsistency? By 
that, I mean not only the specific line shown in the error message, but 
all the lines causing constraints in the cycle of the inconsistency.
- is there anything I could do to be able to use map with types such as 
"imp unit" that cause the universe inconsistency?

Thanks,

Nathanaël Courant