Fix #11360: discharge of template inductive with param only use of var

3 files changed, 26 insertions, 8 deletions

diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst
new file mode 100644
index 0000000000..8c84648aa7
--- /dev/null
+++ b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst
@@ -0,0 +1,4 @@
+- **Fixed:** `#11360 <https://github.com/issues/11360>`_
+  Broken section closing when a template polymorphic inductive type depends on
+  a section variable through its parameters (`#11361
+  <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert).
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 750ac86908..ab915e2b8d 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -379,17 +379,25 @@ let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds =
 (************************************************************************)
 (* Build the inductive packet *)
 
-let repair_arity indices = function
-  | RegularArity ar -> ar.mind_user_arity
-  | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level)
+let fold_arity f acc params arity indices = match arity with
+  | RegularArity ar -> f acc ar.mind_user_arity
+  | TemplateArity _ ->
+    let fold_ctx acc ctx =
+      List.fold_left (fun acc d ->
+          Context.Rel.Declaration.fold_constr (fun c acc -> f acc c) d acc)
+        acc
+        ctx
+    in
+    fold_ctx (fold_ctx acc params) indices
 
-let fold_inductive_blocks f =
+let fold_inductive_blocks f acc params inds =
   Array.fold_left (fun acc ((arity,lc),(indices,_),_) ->
-    f (Array.fold_left f acc lc) (repair_arity indices arity))
+      fold_arity f (Array.fold_left f acc lc) params arity indices)
+    acc inds
 
-let used_section_variables env inds =
+let used_section_variables env params inds =
   let fold l c = Id.Set.union (Environ.global_vars_set env c) l in
-  let ids = fold_inductive_blocks fold Id.Set.empty inds in
+  let ids = fold_inductive_blocks fold Id.Set.empty params inds in
   keep_hyps env ids
 
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
@@ -461,7 +469,7 @@ let compute_projections (kn, i as ind) mib =
 let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
-  let hyps = used_section_variables env inds in
+  let hyps = used_section_variables env paramsctxt inds in
   let nparamargs = Context.Rel.nhyps paramsctxt in
   (* Check one inductive *)
   let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg =
diff --git a/test-suite/bugs/closed/bug_11360.v b/test-suite/bugs/closed/bug_11360.v
new file mode 100644
index 0000000000..d8bc4a9f02
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11360.v
@@ -0,0 +1,6 @@
+Section S.
+  Variable (A:Type).
+  #[universes(template)]
+  Inductive bar (d:A) := .
+End S.
+Check bar nat 0.