Fix #11039: proof of False with template poly and nonlinear universes

Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.

A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.

Also fixes #10504.

10 files changed, 145 insertions, 19 deletions

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 0631b3ad59..67becb251a 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -120,7 +120,17 @@ Universes
   risk: unlikely to be activated by chance (requires a plugin)
 
   component: template polymorphism
-  summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though)
+  summary: template polymorphism not collecting side constrains on the
+  universe level of a parameter; this is a general form of the
+  previous issue about template polymorphism exploiting other ways to
+  generate untracked constraints
+  introduced: morally at the introduction of template polymorphism, 23
+  May 2006, 9c2d70b, r8845, Herbelin
+  impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3,
+  V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory
+  also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found
+  there yet (an exploit using a plugin to force sharing of universe
+  level is in principle possible though)
   impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found
   impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit)
   fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau)
@@ -129,6 +139,22 @@ Universes
   GH issue number: #9294
   risk: moderate risk to be activated by chance
 
+  component: template polymorphism
+  summary: using the same universe in the parameters and the
+  constructor arguments of a template polymorphic inductive (using
+  named universes in modern Coq, or unification tricks in older Coq)
+  produces implicit equality constraints not caught by the previous
+  template polymorphism fix.
+  introduced: same as the previous template polymorphism bug, morally
+  from V8.1, first verified impacted version V8.5 (the universe
+  unification is sufficiently different in V8.4 to prevent our trick
+  from working)
+  fixed in: expected in 8.10.2, 8.11+beta, master (#11128, Nov 2019, Gilbert)
+  found by: Gilbert
+  exploit: test-suite/bugs/closed/bug_11039.v
+  GH issue number: #11039
+  risk: moderate risk (found by investigating #10504)
+
   component: universe polymorphism, asynchronous proofs
   summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
   introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 06d2e1bb21..2b5409c1ab 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -253,10 +253,11 @@ let unbounded_from_below u cstrs =
    (starting from the most recent and ignoring let-definitions) is not
    contributing to the inductive type's sort or is Some u_k if its level
    is u_k and is contributing. *)
-let template_polymorphic_univs ~template_check uctx paramsctxt concl =
+let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl =
   let check_level l =
     if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
-       unbounded_from_below l (Univ.ContextSet.constraints uctx) then
+       unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
+       not (Univ.LSet.mem l ctor_levels) then
       Some l
     else None
   in
@@ -302,7 +303,28 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
           | Polymorphic _ ->
             CErrors.anomaly ~label:"polymorphic_template_ind"
               Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
-      let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in
+      let ctor_levels =
+        let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+        let param_levels =
+          List.fold_left (fun levels d -> match d with
+              | LocalAssum _ -> levels
+              | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+            Univ.LSet.empty params
+        in
+        Array.fold_left
+          (fun levels (d,c) ->
+             let levels =
+               List.fold_left (fun levels d ->
+                   Context.Rel.Declaration.fold_constr add_levels d levels)
+                 levels d
+             in
+             add_levels c levels)
+          param_levels
+          splayed_lc
+      in
+      let param_levels, concl_levels =
+        template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ
+      in
       if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
          && Univ.LSet.is_empty concl_levels then
         CErrors.anomaly ~label:"polymorphic_template_ind"
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8da4e2885c..5c04e860a2 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -38,6 +38,7 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
    of a template polymorphic inductive *)
 val template_polymorphic_univs :
   template_check:bool ->
+  ctor_levels:Univ.LSet.t ->
   Univ.ContextSet.t ->
   Constr.rel_context ->
   Univ.Universe.t ->
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index f6b192c226..475859fcc2 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -1184,7 +1184,6 @@ Notation xpreim := (fun f (p : pred _) x => p (f x)).
 
 (** The packed class interface for pred-like types. **)
 
-#[universes(template)]
 Structure predType T :=
    PredType {pred_sort :> Type; topred : pred_sort -> pred T}.
 
diff --git a/test-suite/bugs/closed/bug_10504.v b/test-suite/bugs/closed/bug_10504.v
new file mode 100644
index 0000000000..6e66a6a90a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10504.v
@@ -0,0 +1,14 @@
+Inductive any_list {A} :=
+| nil : @any_list A
+| cons : forall X, A -> @any_list X -> @any_list A.
+
+Arguments nil {A}.
+Arguments cons {A X}.
+
+Notation "[]" := (@nil Type).
+Notation "hd :: tl" := (cons hd tl).
+
+Definition xs := true :: 2137 :: false :: 0 :: [].
+Fail Definition ys := xs :: xs.
+
+(* Goal ys = ys. produced an anomaly "Unable to handle arbitrary u+k <= v constraints" *)
diff --git a/test-suite/bugs/closed/bug_11039.v b/test-suite/bugs/closed/bug_11039.v
new file mode 100644
index 0000000000..f02a3ef177
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11039.v
@@ -0,0 +1,26 @@
+(* this bug was a proof of False *)
+
+(* when we require template poly Coq recognizes that it's not allowed *)
+Fail #[universes(template)]
+  Inductive foo@{i} (A:Type@{i}) : Type@{i+1} := bar (X:Type@{i}) : foo A.
+
+(* variants with letin *)
+Fail #[universes(template)]
+ Inductive foo@{i}  (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar (X:T) : foo A.
+
+Fail #[universes(template)]
+ Record foo@{i}  (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar { X:T }.
+
+
+(* no implicit template poly, no explicit universe annotations *)
+Inductive foo (A:Type) := bar X : foo X -> foo A | nonempty.
+Arguments nonempty {_}.
+
+Fail Check foo nat : Type@{foo.u0}.
+(* template poly didn't activate *)
+
+Definition U := Type.
+Definition A : U := foo nat.
+
+Fail Definition down : U -> A := fun u => bar nat u nonempty.
+(* this is the one where it's important that it fails *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index b09a7d3264..c5165662e5 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -257,7 +257,6 @@ Ltac blocked t := block_goal ; t ; unblock_goal.
    be used by the [equations] resolver. It is especially useful to register the dependent elimination
    principles for things in [Prop] which are not automatically generated. *)
 
-#[universes(template)]
 Class DependentEliminationPackage (A : Type) :=
   { elim_type : Type ; elim : elim_type }.
 
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 80fcb7bc45..d9201e54af 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -323,7 +323,7 @@ let check_named {CAst.loc;v=na} = match na with
   let msg = str "Parameters must be named." in
   user_err ?loc  msg
 
-let template_polymorphism_candidate env uctx params concl =
+let template_polymorphism_candidate env ~ctor_levels uctx params concl =
   match uctx with
   | Entries.Monomorphic_entry uctx ->
     let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
@@ -331,7 +331,9 @@ let template_polymorphism_candidate env uctx params concl =
     else
       let template_check = Environ.check_template env in
       let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
-      let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in
+      let params, conclunivs =
+        IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu
+      in
       not (template_check && Univ.LSet.is_empty conclunivs)
   | Entries.Polymorphic_entry _ -> false
 
@@ -376,7 +378,20 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
   (* Build the inductive entries *)
   let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) ->
       let template_candidate () =
-        templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in
+        templatearity ||
+        let ctor_levels =
+          let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+          let param_levels =
+            List.fold_left (fun levels d -> match d with
+                | LocalAssum _ -> levels
+                | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+              Univ.LSet.empty ctx_params
+          in
+          List.fold_left (fun levels c -> add_levels c levels)
+            param_levels ctypes
+        in
+        template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl
+      in
       let template = match template with
         | Some template ->
           if poly && template then user_err
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 45e539b1e4..ef05b213d8 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -77,12 +77,18 @@ val should_auto_template : Id.t -> bool -> bool
    automatically use template polymorphism. [x] is the name of the
    inductive under consideration. *)
 
-val template_polymorphism_candidate :
-  Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool
-(** [template_polymorphism_candidate env uctx params conclsort] is
-   [true] iff an inductive with params [params] and conclusion
-   [conclsort] would be definable as template polymorphic.  It should
-   have at least one universe in its monomorphic universe context that
-   can be made parametric in its conclusion sort, if one is given.
-   If the [Template Check] flag is false we just check that the conclusion sort
-   is not small. *)
+val template_polymorphism_candidate
+  : Environ.env
+  -> ctor_levels:Univ.LSet.t
+  -> Entries.universes_entry
+  -> Constr.rel_context
+  -> Sorts.t option
+  -> bool
+(** [template_polymorphism_candidate env ~ctor_levels uctx params
+   conclsort] is [true] iff an inductive with params [params],
+   conclusion [conclsort] and universe levels appearing in the
+   constructor arguments [ctor_levels] would be definable as template
+   polymorphic. It should have at least one universe in its
+   monomorphic universe context that can be made parametric in its
+   conclusion sort, if one is given. If the [Template Check] flag is
+   false we just check that the conclusion sort is not small. *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 49a73271f0..c4254d11fb 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -429,7 +429,25 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
     let type_constructor = it_mkProd_or_LetIn ind fields in
     let template =
       let template_candidate () =
-        ComInductive.template_polymorphism_candidate (Global.env ()) univs params
+        (* we use some dummy values for the arities in the rel_context
+           as univs_of_constr doesn't care about localassums and
+           getting the real values is too annoying *)
+        let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+        let param_levels =
+          List.fold_left (fun levels d -> match d with
+              | LocalAssum _ -> levels
+              | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+            Univ.LSet.empty params
+        in
+        let ctor_levels = List.fold_left
+            (fun univs d ->
+               let univs =
+                 RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs
+               in
+               univs)
+            param_levels fields
+        in
+        ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params
           (Some (Sorts.sort_of_univ min_univ))
       in
       match template with