Merge PR #9918: Fix #9294: critical bug with template polymorphism

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot

17 files changed, 211 insertions, 25 deletions

diff --git a/test-suite/bugs/closed/bug_9294.v b/test-suite/bugs/closed/bug_9294.v
new file mode 100644
index 0000000000..a079d672d3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9294.v
@@ -0,0 +1,29 @@
+Set Printing Universes.
+
+Inductive Foo@{i} (A:Type@{i}) : Type := foo : (Set:Type@{i}) -> Foo A.
+Arguments foo {_} _.
+Print Universes Subgraph (Foo.i).
+Definition bar : Foo True -> Set := fun '(foo x) => x.
+
+Definition foo_bar (n : Foo True) : foo (bar n) = n.
+Proof. destruct n;reflexivity. Qed.
+
+Definition bar_foo (n : Set) : bar (foo n) = n.
+Proof. reflexivity. Qed.
+
+Require Import Hurkens.
+
+Inductive box (A : Set) : Prop := Box : A -> box A.
+
+Definition Paradox : False.
+Proof.
+Fail unshelve refine (
+  NoRetractFromSmallPropositionToProp.paradox
+  (Foo True)
+  (fun A => foo A)
+  (fun A => box (bar A))
+  _
+  _
+  False
+).
+Abort.
diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v
index bc5cd0fb68..4b6916af55 100644
--- a/test-suite/coqchk/inductive_functor_template.v
+++ b/test-suite/coqchk/inductive_functor_template.v
@@ -2,7 +2,7 @@
 Module Type E. Parameter T : Type. End E.
 
 Module F (X:E).
-  #[universes(template)] Inductive foo := box : X.T -> foo.
+  Inductive foo := box : X.T -> foo.
 End F.
 
 Module ME. Definition T := nat. End ME.
diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
new file mode 100644
index 0000000000..75b2a56169
--- /dev/null
+++ b/test-suite/failure/Template.v
@@ -0,0 +1,32 @@
+(*
+Module TestUnsetTemplateCheck.
+  Unset Template Check.
+
+  Section Foo.
+
+    Context (A : Type).
+
+    Definition cstr := nat : ltac:(let ty := type of A in exact ty).
+
+    Inductive myind :=
+    | cons : A -> myind.
+  End Foo.
+
+  (* Can only succeed if no template check is performed *)
+  Check myind True : Prop.
+
+  Print Assumptions myind.
+  (*
+  Axioms:
+  myind is template polymorphic on all its universe parameters.
+   *)
+  About myind.
+(*
+myind : Type@{Top.60} -> Type@{Top.60}
+
+myind is assumed template universe polymorphic on Top.60
+Argument scope is [type_scope]
+Expands to: Inductive Top.TestUnsetTemplateCheck.myind
+*)
+End TestUnsetTemplateCheck.
+*)
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4e949dcb04..a040b69b44 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -84,7 +84,6 @@ Print f.
 (* Was enhancement request #5142 (error message reported on the most
    general return clause heuristic) *)
 
-#[universes(template)]
 Inductive gadt : Type -> Type :=
 | gadtNat : nat -> gadt nat
 | gadtTy : forall T, T -> gadt T.
diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v
index 6976f35a88..0e84bf3966 100644
--- a/test-suite/output/Coercions.v
+++ b/test-suite/output/Coercions.v
@@ -1,7 +1,7 @@
 (* Submitted by Randy Pollack *)
 
-#[universes(template)] Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
-#[universes(template)] Record rel (S : Set) : Type :=  {sr_rel :> S -> S -> Prop}.
+Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
+Record rel (S : Set) : Type :=  {sr_rel :> S -> S -> Prop}.
 
 Section testSection.
 Variables (S : Set) (P : pred S) (R : rel S) (x : S).
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index f9398fdca9..1ecd9771eb 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -101,7 +101,7 @@ Section decoder_result.
 
  Variable inst : Type.
 
- #[universes(template)] Inductive decoder_result : Type :=
+ Inductive decoder_result : Type :=
  | DecUndefined : decoder_result
  | DecUnpredictable : decoder_result
  | DecInst : inst -> decoder_result
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 9b25c2dbd3..61ae4edbd1 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
   omega.
 Qed.
 
-#[universes(template)] CoInductive Inf := S { projS : Inf }.
+CoInductive Inf := S { projS : Inf }.
 Definition expand_Inf (x : Inf) := S (projS x).
 CoFixpoint inf := S inf.
 Eval compute in inf.
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 29614c032a..aeebc0f98b 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
 (**********************************************************************)
 (* Test printing of #4932                                             *)
 
-#[universes(template)] Inductive ftele : Type :=
+Inductive ftele : Type :=
 | fb {T:Type} : T -> ftele
 | fr {T} : (T -> ftele) -> ftele.
 
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 0c1b08f5a3..d671053c07 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -53,7 +53,7 @@ Module Suboptimal.
 (** This test shows an example which exposes the [let] introduced by
     the pattern notation in binders. *)
 
-#[universes(template)] Inductive Fin (n:nat) := Z : Fin n.
+Inductive Fin (n:nat) := Z : Fin n.
 Definition F '(n,p) : Type := (Fin n * Fin p)%type.
 Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
 Print both_z.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ab4172711e..e788977fb7 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,6 +1,6 @@
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
-existT is template universe polymorphic
+existT is template universe polymorphic on sigT.u0 sigT.u1
 Argument A is implicit
 Argument scopes are [type_scope function_scope _ _]
 Expands to: Constructor Coq.Init.Specif.existT
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 35f36e87d7..14d63d39c4 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -6,7 +6,7 @@ Class HostFunction := host_func : Type.
 
 Section store.
   Context `{HostFunction}.
-  #[universes(template)] Record store := { store_funcs : host_func }.
+  Record store := { store_funcs : host_func }.
 End store.
 
 Check (fun (S:@store nat) => S.(store_funcs)).
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 4fe7b051f8..d9a649fadc 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,12 +20,12 @@ Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
 
-#[universes(template)] Record N := C { T : Type; _ : True }.
+Record N := C { T : Type; _ : True }.
 Check fun x:N => let 'C _ p := x in p.
 Check fun x:N => let 'C T _ := x in T.
 Check fun x:N => let 'C T p := x in (T,p).
 
-#[universes(template)] Record M := D { U : Type; a := 0; q : True }.
+Record M := D { U : Type; a := 0; q : True }.
 Check fun x:M => let 'D T _ p := x in p.
 Check fun x:M => let 'D T _ p := x in T.
 Check fun x:M => let 'D T p := x in (T,p).
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
index 99183f2064..9cf6ad35b8 100644
--- a/test-suite/output/ShowMatch.v
+++ b/test-suite/output/ShowMatch.v
@@ -3,12 +3,12 @@
 *)
 
 Module A.
-  #[universes(template)] Inductive foo := f.
+  Inductive foo := f.
   Show Match foo. (* no need to disambiguate *)
 End A. 
 
 Module B.
-  #[universes(template)] Inductive foo := f.
+  Inductive foo := f.
   (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
   Show Match A.foo. 
 End B.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 222a808768..a89fd64999 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -68,9 +68,9 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 bobmorane = 
-let tt := Type@{UnivBinders.32} in
-let ff := Type@{UnivBinders.34} in tt -> ff
-     : Type@{max(UnivBinders.31,UnivBinders.33)}
+let tt := Type@{UnivBinders.33} in
+let ff := Type@{UnivBinders.35} in tt -> ff
+     : Type@{max(UnivBinders.32,UnivBinders.34)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
@@ -143,16 +143,16 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.56 UnivBinders.57} :
-Type@{UnivBinders.56} -> Type@{i}
-(* i UnivBinders.56 UnivBinders.57 |=  *)
+axfoo@{i UnivBinders.57 UnivBinders.58} :
+Type@{UnivBinders.57} -> Type@{i}
+(* i UnivBinders.57 UnivBinders.58 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.56 UnivBinders.57} :
-Type@{UnivBinders.57} -> Type@{i}
-(* i UnivBinders.56 UnivBinders.57 |=  *)
+axbar@{i UnivBinders.57 UnivBinders.58} :
+Type@{UnivBinders.58} -> Type@{i}
+(* i UnivBinders.57 UnivBinders.58 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
index 0eb5db1733..7465442cab 100644
--- a/test-suite/output/Warnings.v
+++ b/test-suite/output/Warnings.v
@@ -1,5 +1,5 @@
 (* Term in warning was not printed in the right environment at some time *)
-#[universes(template)] Record A := { B:Type; b:B->B }.
+Record A := { B:Type; b:B->B }.
 Definition a B := {| B:=B; b:=fun x => x |}.
 Canonical Structure a.
 
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 209fedc343..57a4739e9f 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -21,6 +21,6 @@ Print P.
 
 (* Note: exact numbers of evars are not important... *)
 
-#[universes(template)] Inductive T (n:nat) : Type := A : T n.
+Inductive T (n:nat) : Type := A : T n.
 Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index cfc25c3346..656362b8fc 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -46,3 +46,129 @@ Module No.
   Definition j_lebox (A:Type@{j}) := Box A.
   Fail Definition box_lti A := Box A : Type@{i}.
 End No.
+
+Module DefaultProp.
+  Inductive identity (A : Type) (a : A) : A -> Type := id_refl : identity A a a.
+
+  (* By default template polymorphism does not interact with inductives
+     which naturally fall in Prop *)
+  Check (identity nat 0 0 : Prop).
+End DefaultProp.
+
+Module ExplicitTemplate.
+  #[universes(template)]
+  Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a.
+
+  (* Weird interaction of template polymorphism and inductive types
+     which naturally fall in Prop: this one is template polymorphic but not on i:
+     it just lives in any universe *)
+  Check (identity Type nat nat : Prop).
+End ExplicitTemplate.
+
+Polymorphic Definition f@{i} : Type@{i} := nat.
+Polymorphic Definition baz@{i} : Type@{i} -> Type@{i} := fun x => x.
+
+Section Foo.
+  Universe u.
+  Context (A : Type@{u}).
+
+  Inductive Bar :=
+  | bar : A -> Bar.
+
+  Set Universe Minimization ToSet.
+  Inductive Baz :=
+  | cbaz : A -> baz Baz -> Baz.
+
+  Inductive Baz' :=
+  | cbaz' : A -> baz@{Set} nat -> Baz'.
+
+  (* 2 constructors, at least in Set *)
+  Inductive Bazset@{v} :=
+  | cbaz1 : A -> baz@{v} Bazset -> Bazset
+  | cbaz2 : Bazset.
+
+  Eval compute in ltac:(let T := type of A in exact T).
+
+  Inductive Foo : Type :=
+  | foo : A -> f -> Foo.
+
+End Foo.
+
+Set Printing Universes.
+(* Cannot fall back to Prop or Set anymore as baz is no longer template-polymorphic *)
+Fail Check Bar True : Prop.
+Fail Check Bar nat : Set.
+About Baz.
+
+Check cbaz True I.
+
+(** Neither can it be Set *)
+Fail Check Baz nat : Set.
+
+(** No longer possible for Baz' which contains a type in Set *)
+Fail Check Baz' True : Prop.
+Fail Check Baz' nat : Set.
+
+Fail Check Bazset True : Prop.
+Fail Check Bazset True : Set.
+
+(** We can force the universe instantiated in [baz Bazset] to be [u], so Bazset lives in max(Set, u). *)
+Constraint u = Bazset.v.
+(** As u is global it is already > Set, so: *)
+Definition bazsetex@{i | i < u} : Type@{u} := Bazset Type@{i}.
+
+(* Bazset is closed for universes u = u0, cannot be instantiated with Prop *)
+Definition bazseetpar (X : Type@{u}) : Type@{u} := Bazset X.
+
+(** Would otherwise break singleton elimination and extraction. *)
+Fail Check Foo True : Prop.
+Fail Check Foo True : Set.
+
+Definition foo_proj {A} (f : Foo A) : nat :=
+  match f with foo _ _ n => n end.
+
+Definition ex : Foo True := foo _ I 0.
+Check foo_proj ex.
+
+(** See failure/Template.v for a test of the unsafe Unset Template Check usage *)
+
+Module AutoTemplateTest.
+Set Warnings "+auto-template".
+Section Foo.
+  Universe u'.
+  Context (A : Type@{u'}).
+
+  (* Not failing as Bar cannot be made template polymorphic at all *)
+  Inductive Bar :=
+  | bar : A -> Bar.
+End Foo.
+End AutoTemplateTest.
+
+Module TestTemplateAttribute.
+  Section Foo.
+    Universe u.
+    Context (A : Type@{u}).
+
+    (* Failing as Bar cannot be made template polymorphic at all *)
+    Fail #[universes(template)] Inductive Bar :=
+    | bar : A -> Bar.
+
+  End Foo.
+End TestTemplateAttribute.
+
+Module SharingWithoutSection.
+Inductive Foo A (S:= fun _ => Set : ltac:(let ty := type of A in exact ty))
+  := foo : S A -> Foo A.
+Fail Check Foo True : Prop.
+End SharingWithoutSection.
+
+Module OkNotCovered.
+(* Here it happens that box is safe but we don't see it *)
+Section S.
+Universe u.
+Variable A : Type@{u}.
+Inductive box (A:Type@{u}) := Box : A -> box A.
+Definition B := Set : Type@{u}.
+End S.
+Fail Check box True : Prop.
+End OkNotCovered.