diff options
| -rw-r--r-- | kernel/indTyping.ml | 14 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 7 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 12 | ||||
| -rw-r--r-- | vernac/himsg.ml | 10 |
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 *) |