`False` inductive sensitive to universe polymorphism, resulting in `admit`ed definitions being sensitive to universe polymorphism setting

[JasonGross]

This is responsible for https://github.com/coq/coq/pull/14733#issuecomment-892772832 and https://github.com/coq/coq/pull/14748#issuecomment-898896082

Consider: In Foo.v:

(* -*- coq-prog-args: ("-emacs" "-noinit") -*- *)
Global Set Universe Polymorphism.
Definition foo@{i} := Type@{i}.

In ex.v:

(* -*- coq-prog-args: ("-emacs" "-noinit" "-Q" "." "Top") -*- *)
Require Import Top.Foo.
Require Import Coq.Init.Ltac.
Monomorphic Inductive True := I.
Monomorphic Inductive eq {A} (x : A) : forall _ : A, Prop := eq_refl : eq x x.
Arguments eq_refl {A x} , [A] x.
Definition foo@{} : Set. Proof. refine True. Defined.
Check let f := (fun _ : foo => (eq_refl Set : eq Foo.foo@{Set} Set)) in f : forall _ : Set, _.

When minimizing this file, we add the code

Inductive False := .
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.

to the top. We then replace refine True with admit. This is fine, but we can now no longer inline Foo.v, because that will Set Universe Polymorphism giving False and therefore proof_admitted one universe, which is not valid. In particular, the file

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option" "-noinit" "-R" "." "Top" "-top" "example_48" "-native-compiler" "ondemand") -*- *)
(* File reduced by coq-bug-finder from original input, then from 24 lines to 15 lines *)
(* coqc version 8.13.1 (April 2021) compiled on Apr 11 2021 23:42:08 with OCaml 4.11.2
   coqtop version 8.13.1 (April 2021)
   Expected coqc runtime on this file: 0.036 sec *)
Declare ML Module "ltac_plugin".
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False := .
End LocalFalse.
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Module Export Top_DOT_Foo.
Module Export Top.
Module Foo.
(* -*- coq-prog-args: ("-emacs" "-noinit") -*- *)
Global Set Universe Polymorphism.
Definition foo@{i} := Type@{i}.

End Foo.

End Top.

End Top_DOT_Foo.
Require Coq.Init.Ltac.

Inductive False := .
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Require Top.Foo.
Require Coq.Init.Ltac.
Import Coq.Init.Ltac.
Monomorphic Inductive eq {A} (x : A) : forall _ : A, Prop := eq_refl : eq x x.
Arguments eq_refl {A x} , [A] x.
Definition foo@{} : Set.
admit.
Defined.
Check let f := (fun _ : foo => (eq_refl Set : eq Foo.foo@{Set} Set)) in f : forall _ : Set, _.

The solution is to false Inductive False to be in Prop.

[JasonGross]

This was a bit harder to debug than it should have been, due to https://github.com/coq/coq/issues/15073

[Alizter]

Good job on finding the culprit! That's a nasty error message from universes though, hopefully we can take a look at that this week.

[JasonGross]

The error message isn't actually that nasty, it's just that if you explicitly annotate a definition with universes, you can't then use a polymorphic constant to admit the definition.