Merge PR #11424: Check instance length in type_of_{inductive,constructor}

Reviewed-by: ppedrot

4 files changed, 37 insertions, 2 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca4fea45c5..5d8e1f0fdb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -198,7 +198,14 @@ let relevance_of_inductive env ind =
   let _, mip = lookup_mind_specif env ind in
   mip.mind_relevance
 
-let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps =
+let check_instance mib u =
+  if not (match mib.mind_universes with
+      | Monomorphic _ -> Instance.is_empty u
+      | Polymorphic uctx -> Instance.length u = AUContext.size uctx)
+  then CErrors.anomaly Pp.(str "bad instance length on mutind.")
+
+let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+  check_instance mib u;
   match mip.mind_arity with
   | RegularArity a -> subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
@@ -244,6 +251,7 @@ let max_inductive_sort =
 (* Type of a constructor *)
 
 let type_of_constructor (cstr, u) (mib,mip) =
+  check_instance mib u;
   let ind = inductive_of_constructor cstr in
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 3f4d5ef58c..190c34262f 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -3,6 +3,10 @@ foo : nat
 Axioms:
 foo : nat
 Axioms:
+bli : Type
+Axioms:
+bli : Type
+Axioms:
 extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
 Axioms:
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index 3d4dfe603d..4c980fddba 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -30,6 +30,21 @@ Module P := N M.
 Print Assumptions M.bar. (* Should answer: foo *)
 Print Assumptions P.bar. (* Should answer: foo *)
 
+(* Print Assumptions used empty instances on polymorphic inductives *)
+Module Poly.
+
+  Set Universe Polymorphism.
+  Axiom bli : Type.
+
+  Definition bla := bli -> bli.
+
+  Inductive blo : bli -> Type := .
+
+  Print Assumptions bla.
+  Print Assumptions blo.
+
+End Poly.
+
 
 (* The original test-case of the bug-report *)
 
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 9f92eba729..fb61a1089f 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -240,8 +240,16 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
      (* Build the context of all arities *)
      let arities_ctx =
        let global_env = Global.env () in
+       let instance =
+         let open Univ in
+         Instance.of_array
+           (Array.init
+              (AUContext.size
+                 (Declareops.inductive_polymorphic_context mib))
+              Level.var)
+       in
        Array.fold_left (fun accu oib ->
-          let pspecif = Univ.in_punivs (mib, oib) in
+          let pspecif = ((mib, oib), instance) in
           let ind_type = Inductive.type_of_inductive global_env pspecif in
           let indr = oib.mind_relevance in
           let ind_name = Name oib.mind_typename in