Open vblot opened 3 years ago
You can probably minimize this with the bug minimizer
This kind of universe inconsistency is usually due to a template-polymorphic inductive type being partially applied somewhere. Those are not easy to find though.
Does coqbot watch this repo? @coqbot minimize
opam install coq-metacoq coq-quickchick
echo > bug.v <<EOF
From QuickChick Require Import Sets.
From MetaCoq.Template Require Import TermEquality.
EOF
coqc -q bug.v
I guess not. Trying at https://github.com/coq-community/run-coq-bug-minimizer/issues/2#issuecomment-982842826
Can metacoq do a release so that the opam package is compatible with 8.14.0?
We're working on it
This is also the incompatibility with Iris that we run into at Bedrock with @gmalecha and others; we thought it might relate to https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 but I don't have strong evidence it's related.
In our case, we just found out that we can skip importing MetaCoq.Template.Typing
— just inline MetaCoq.Template.All
minus that line, and quoting and MetaCoq Run
still work fine. (EDIT: typos).
Minimized example against coq-iris.dev.2021-01-12.0.bbaf3eaf
from git+https://gitlab.mpi-sws.org/iris/opam.git
:
From iris.algebra Require Import ofe cmra frac.
(* Imported by MetaCoq.Template.All but unneeded: *)
Fail From MetaCoq.Template Require Typing.
(* The problem is in fact introduced by: *)
Fail From MetaCoq.Template Require TermEquality.
Some partial minimizations appear in https://gist.github.com/Blaisorblade/aae837cb9b39e7693d3f2037960b0f80, but dunno if it's helpful.
On the latest commit of the coq-8.14
branch (43f4c699803d2b0e54ebfd99bb9bb5377c7d5ab9), plus coq-iris.dev.2021-12-30.0.f6beee55
, we get somewhat similar errors, and avoiding Typing
seems to still avoid those.
From iris.algebra Require Import frac.
From MetaCoq.Template Require Import Typing.
(*
Universe inconsistency. Cannot enforce Coq.Relations.Relation_Definitions.1
<= All_Forall.All.u1 because All_Forall.All.u1
< Coq.Relations.Relation_Definitions.1.
*)
From MetaCoq.Template Require Import Typing.
From iris.algebra Require Import frac.
(*
Universe inconsistency. Cannot enforce base.equivL.u0 = eq.u0 because eq.u0
<= stdpp.base.47 <= cstr_respects_variance.u0 < eq.u0 = base.equivL.u0.
*)
@gmalecha suggested dropping Typing
from MetaCoq.Template.All
since it's not needed for many metaprogramming usecases.
Other users can try replacing requires of MetaCoq.Template.All
with the following, and report whether it is sufficient for their uses.
From MetaCoq.Template Require Import
utils.MCUtils (* Utility functions *)
monad_utils (* Monadic notations *)
uGraph (* The graph of universes *)
BasicAst (* The basic AST structures *)
Ast (* The term AST *)
AstUtils (* Utilities on the AST *)
Induction (* Induction *)
LiftSubst (* Lifting and substitution for terms *)
UnivSubst (* Substitution of universe instances *)
(* Typing *) (* Typing judgment *)
TemplateMonad (* The TemplateMonad *)
Loader (* The plugin *).
I assume the partial application in QuickChick is from coq-ext-lib. Candidates include: 1) https://github.com/coq-community/coq-ext-lib/blob/73fa2d83a075adedc65c1f5888d7f688f9e31f0c/theories/Data/Monads/ListMonad.v#L7 2) https://github.com/coq-community/coq-ext-lib/blob/73fa2d83a075adedc65c1f5888d7f688f9e31f0c/theories/Data/List.v#L123
There might be more list monads in there.
If indeed this is the issue, the solution is to eta-expand list
everywhere it's used as a function, as I say at https://github.com/coq-community/coq-ext-lib/pull/123#discussion_r783590882
FWIW:
coq-metacoq.1.1+8.16
and coq-quickchick.1.6.4
, as in the platform).list
as suggested turned out to be a huge can of worms.Typing
and TermEquality
.
With the following:
I get the error:
Strangely, pasting the line
From QuickChick Require Import Sets.
on top of file https://github.com/MetaCoq/metacoq/blob/coq-8.13/template-coq/theories/TermEquality.v raises the error:Tested with Coq 8.13.2, QuickChick 1.5.0 and MetaCoq 1.0~beta2+8.13 from opam
This is related to https://github.com/smtcoq/sniper/issues/4 and https://github.com/QuickChick/QuickChick/issues/232.