Merge PR #11478: Nicer kernel universe error for inductives

Reviewed-by: ppedrot

4 files changed, 27 insertions, 16 deletions

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 591cd050a5..719eb276df 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -66,7 +66,9 @@ let mind_check_names mie =
 
 type univ_info = { ind_squashed : bool; ind_has_relevant_arg : bool;
                    ind_min_univ : Universe.t option; (* Some for template *)
-                   ind_univ : Universe.t }
+                   ind_univ : Universe.t;
+                   missing : Universe.Set.t; (* missing u <= ind_univ constraints *)
+                 }
 
 let check_univ_leq ?(is_real_arg=false) env u info =
   let ind_univ = info.ind_univ in
@@ -78,9 +80,8 @@ let check_univ_leq ?(is_real_arg=false) env u info =
   if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
   then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
   else if is_impredicative_univ env ind_univ
-  then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
-    else raise (InductiveError BadUnivs)
-  else raise (InductiveError BadUnivs)
+       && Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
+  else {info with missing = Universe.Set.add u info.missing}
 
 let check_context_univs ~ctor env info ctx =
   let check_one d (info,env) =
@@ -109,6 +110,7 @@ let check_arity env_params env_ar ind =
     ind_has_relevant_arg=false;
     ind_min_univ;
     ind_univ=Sorts.univ_of_sort ind_sort;
+    missing=Universe.Set.empty;
   }
   in
   let univ_info = check_indices_matter env_params univ_info indices in
@@ -174,7 +176,7 @@ let check_record data =
 (* - all_sorts in case of small, unitary Prop (not smashed) *)
 (* - logical_sorts in case of large, unitary Prop (smashed) *)
 
-let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} =
+let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_;missing=_} =
   if not ind_squashed then InType
   else Sorts.family (Sorts.sort_of_univ ind_univ)
 
@@ -224,6 +226,8 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc
   params, univs
 
 let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+  if not (Universe.Set.is_empty univ_info.missing)
+  then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
   let arity = Vars.subst_univs_level_constr usubst arity in
   let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
   let indices = Vars.subst_univs_level_context usubst indices in
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f221ac7a4f..c2cdf98ee8 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -12,6 +12,7 @@ open Names
 open Constr
 open Environ
 open Reduction
+open Univ
 
 (* Type errors. *)
 
@@ -63,8 +64,8 @@ type ('constr, 'types) ptype_error =
   | IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
       int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
-  | UnsatisfiedConstraints of Univ.Constraint.t
-  | UndeclaredUniverse of Univ.Level.t
+  | UnsatisfiedConstraints of Constraint.t
+  | UndeclaredUniverse of Level.t
   | DisallowedSProp
   | BadRelevance
 
@@ -83,7 +84,7 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
-  | BadUnivs
+  | MissingConstraints of (Universe.Set.t * Universe.t)
 
 exception InductiveError of inductive_error
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index ae6fd31762..0f29717f12 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -11,6 +11,7 @@
 open Names
 open Constr
 open Environ
+open Univ
 
 (** Type errors. {% \label{typeerrors} %} *)
 
@@ -64,8 +65,8 @@ type ('constr, 'types) ptype_error =
   | IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
       int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
-  | UnsatisfiedConstraints of Univ.Constraint.t
-  | UndeclaredUniverse of Univ.Level.t
+  | UnsatisfiedConstraints of Constraint.t
+  | UndeclaredUniverse of Level.t
   | DisallowedSProp
   | BadRelevance
 
@@ -86,7 +87,8 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
-  | BadUnivs
+  | MissingConstraints of (Universe.Set.t * Universe.t)
+  (* each universe in the set should have been <= the other one *)
 
 exception InductiveError of inductive_error
 
@@ -133,9 +135,9 @@ val error_ill_typed_rec_body  :
 
 val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
 
-val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
+val error_unsatisfied_constraints : env -> Constraint.t -> 'a
 
-val error_undeclared_universe : env -> Univ.Level.t -> 'a
+val error_undeclared_universe : env -> Level.t -> 'a
 
 val error_disallowed_sprop : env -> 'a
 
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index eb39564fed..17c3e0395a 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1216,8 +1216,12 @@ let error_bad_entry () =
 let error_large_non_prop_inductive_not_in_type () =
   str "Large non-propositional inductive types must be in Type."
 
-let error_inductive_bad_univs () =
-  str "Incorrect universe constraints declared for inductive type."
+let error_inductive_missing_constraints (us,ind_univ) =
+  let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes in
+  str "Missing universe constraint declared for inductive type:" ++ spc()
+  ++ v 0 (prlist_with_sep spc (fun u ->
+      hov 0 (pr_u u ++ str " <= " ++ pr_u ind_univ))
+      (Univ.Universe.Set.elements us))
 
 (* Recursion schemes errors *)
 
@@ -1256,7 +1260,7 @@ let explain_inductive_error = function
   | BadEntry -> error_bad_entry ()
   | LargeNonPropInductiveNotInType ->
     error_large_non_prop_inductive_not_in_type ()
-  | BadUnivs -> error_inductive_bad_univs ()
+  | MissingConstraints csts -> error_inductive_missing_constraints csts
 
 (* Recursion schemes errors *)