MetaCoq is incompatible with QuickChick (universe inconsistency)

[vblot]

With the following:

From QuickChick Require Import Sets.
From MetaCoq.Template Require Import TermEquality.

I get the error:

Universe inconsistency. Cannot enforce
Coq.Relations.Relation_Definitions.1 <=
All_Forall.All2_All_mix_left.u1 because All_Forall.All2_All_mix_left.u1
<= All_Forall.All2.u2 <= All_Forall.All2_map.u5
< Coq.Relations.Relation_Definitions.1.

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:

No 1st non dependent hypothesis in current goal even after
head-reduction.

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.

[JasonGross]

You can probably minimize this with the bug minimizer

[mattam82]

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.

[JasonGross]

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

[JasonGross]

I guess not. Trying at https://github.com/coq-community/run-coq-bug-minimizer/issues/2#issuecomment-982842826

[JasonGross]

Can metacoq do a release so that the opam package is compatible with 8.14.0?

[mattam82]

We're working on it

[Blaisorblade]

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.

[Blaisorblade]

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

[Blaisorblade]

@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 *).

[Janno]

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.

[JasonGross]

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

[Blaisorblade]

FWIW:

• I confirmed this is still an issue as of 8.16 (with coq-metacoq.1.1+8.16 and coq-quickchick.1.6.4, as in the platform).
• Eta-expanding list as suggested turned out to be a huge can of worms.
• We're still working around this by not importing Typing and TermEquality.