[subst] fails with bogus error message about universe polymorphism

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5341 From: @tchajed Reported version: trunk CC: @tchajed

[coqbot]

Comment author: @tchajed

The following code triggers a subst bug:

(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fscq" "-top" "Mem") -*- *)
(* File reduced by coq-bug-finder from original input, then from 213 linesCoq.Logic.FunctionalExtensionalityunk (February 2017) compiled on Feb 6 2017 16:8:54 with OCaml 4.02.3
   coqtop version 26-5-163.dynamic.csail.mit.edu:/Users/tchajed/code/sw/coq,trunk (e61e83758e129d455d664b65a1fe15ecac793186), then from 40 lines to 26 lines *)
(* coqc version trunk (February 2017) compiled on Feb 6 2017 16:8:54 with OCaml 4.02.3
   coqtop version 26-5-163.dynamic.csail.mit.edu:/Users/tchajed/code/sw/coq,trunk (e61e83758e129d455d664b65a1fe15ecac793186) *)

Set Universe Polymorphism.

Section GenMem.
  Variable A : Type.

  Theorem upd_nop:  forall (a : A) (x : A) (e : a = x),
      e = e ->
      True.
  Proof.
    intros.
    subst.
(* Ltac call to "subst" failed.
Error: Cannot mix universe polymorphic and monomorphic declarations in sections. *)
  Abort.
End GenMem.

[coqbot]

Comment author: @tchajed

Interestingly, this works:

(also, thanks to Jason for debugging this!)

(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top" "-top" "subst_def_bug") -*- *)
(* File reduced by coq-bug-finder from original input, then from 490 lines to 38 lines, then from 52 lines to 38 lines *)
(* coqc version trunk (February 2017) compiled on Feb 6 2017 16:8:54 with OCaml 4.02.3
   coqtop version 26-5-163.dynamic.csail.mit.edu:/Users/tchajed/code/sw/coq,trunk (e61e83758e129d455d664b65a1fe15ecac793186) *)

Set Universe Polymorphism.

Theorem upd_nop:  forall A (a : A) (x : A) (e : a = x),
    e = e -> True.
Proof.
  intros ? ? ? ->.
  auto.
Qed.

Section GenMem.
  Variable A : Type.

  Theorem upd_nop':  forall (a : A) (x : A) (e : a = x),
      e = e -> True.
  Proof.
    intros.
    subst. (* interestingly, this works, but only if upd_nop's proof uses the ->
    intro pattern (not even <-) *)

[coqbot]

Comment author: @JasonGross

What's happening here is that "subst" apparently generates (monomorphic) dependent rewriting lemmas on the fly if they do not exist, and having them be monomorphic in a section with polymorphic variables is not allowed.

You can also get this error message with [rewrite]:

Inductive eq {A} (x : A) : A -> Prop := eq_refl : eq x x.

Set Universe Polymorphism.
Section a.
  Variable a : Type.
  Goal forall (x y : a) (e h : eq x y), eq e e.
  Proof.
    intros ?? e h.
    rewrite e in h.

It's not clear to me what the right fix is. I think the best thing to do is to relax "Cannot mix universe polymorphic and monomorphic declarations in sections" so that mixtures are allowed when they are entirely disjoint (i.e., a monomorphic definition cannot mention a polymorphic variable, nor any polymorphic universes, and a polymorphic definition cannot mention any monomorphic variables).

[SkySkimmer]

We would need to check monomorphic stuff in an environment without all the polymorphic stuff, so it's a bit tricky currently.

[SkySkimmer]

See also https://github.com/coq/coq/issues/16330