From a5d124dd7c3d43a5ead81cfac30c7d1448002d56 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Nov 2019 15:53:48 +0100
Subject: 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.
---
 vernac/comInductive.ml | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

(limited to 'vernac/comInductive.ml')

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
-- 
cgit v1.2.3


From 1db8720bf624c202dcc4f1eecdcde803fed4efc2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 19 Nov 2019 14:28:37 +0100
Subject: indTyping: error instead of anomaly for ill-formed template

and do not run template_candidate in the upper layers when the
template attribute is given.

This means we can use an over-approximation in the upper layer
implementation of template_candidate (returning false even in cases
which the kernel may accept) if we ever want to.
---
 vernac/comInductive.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index d9201e54af..2aee9bd47f 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -396,9 +396,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
         | Some template ->
           if poly && template then user_err
               Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.");
-          if template && not (template_candidate ()) then
-            user_err Pp.(strbrk "Inductive " ++ Id.print indname ++
-                         str" cannot be made template polymorphic.");
           template
         | None ->
           should_auto_template indname (template_candidate ())
-- 
cgit v1.2.3