aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/indtypes.ml61
-rw-r--r--kernel/indtypes.mli11
-rw-r--r--kernel/reduction.ml4
-rw-r--r--library/declare.ml6
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/inductiveops.ml41
-rw-r--r--pretyping/inductiveops.mli4
-rw-r--r--test-suite/success/polymorphism.v20
-rw-r--r--vernac/command.ml2
-rw-r--r--vernac/record.ml6
10 files changed, 106 insertions, 55 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 15fe90835..a4c7a0573 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -215,20 +215,42 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter
numchecked := !numchecked + 1
in
let check_typ typ typ_env =
- match typ with
- | LocalAssum (_, typ') ->
- begin
- try
- basic_check env typ'; Environ.push_rel typ typ_env
- with NotConvertible ->
- anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
- end
- | _ -> anomaly (Pp.str "")
+ match typ with
+ | LocalAssum (_, typ') ->
+ begin
+ try
+ basic_check typ_env typ'; Environ.push_rel typ typ_env
+ with NotConvertible ->
+ anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
+ end
+ | _ -> anomaly (Pp.str "")
in
let typs, codom = dest_prod env arcn in
let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
if not is_arity then basic_check last_env codom else ()
+(* Check that the subtyping information inferred for inductive types in the block is correct. *)
+(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
+let check_subtyping mie paramsctxt env_ar inds =
+ let numparams = Context.Rel.nhyps paramsctxt in
+ let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in
+ let dosubst = subst_univs_level_constr sbsubst in
+ let uctx = UInfoInd.univ_context mie.mind_entry_universes in
+ let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
+ let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+ let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+ let env' = Environ.push_context uctx env_ar in
+ let env'' = Environ.push_context uctx_other env' in
+ let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in
+ (* process individual inductive types: *)
+ Array.iter (fun (id,cn,lc,(sign,arity)) ->
+ match arity with
+ | RegularArity (_, full_arity, _) ->
+ check_subtyping_arity_constructor envsb dosubst full_arity numparams true;
+ Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
+ | TemplateArity _ -> ()
+ ) inds
+
(* Type-check an inductive definition. Does not check positivity
conditions. *)
(* TODO check that we don't overgeneralize construcors/inductive arities with
@@ -370,26 +392,7 @@ let typecheck_inductive env mie =
in
(* Check that the subtyping information inferred for inductive types in the block is correct. *)
(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
- let () =
- let numparams = List.length paramsctxt in
- let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in
- let dosubst = subst_univs_level_constr sbsubst in
- let uctx = UInfoInd.univ_context mie.mind_entry_universes in
- let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
- let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
- let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
- let env' = Environ.push_context uctx env_ar_par in
- let env'' = Environ.push_context uctx_other env' in
- let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in
- (* process individual inductive types: *)
- Array.iter (fun (id,cn,lc,(sign,arity)) ->
- match arity with
- | RegularArity (_, full_arity, _) ->
- check_subtyping_arity_constructor envsb dosubst full_arity numparams true;
- Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
- | TemplateArity _ -> ()
- (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *)
- ) inds
+ let () = check_subtyping mie paramsctxt env_arities inds
in (env_arities, env_ar_par, paramsctxt, inds)
(************************************************************************)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5b4615399..7b0f01794 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -32,6 +32,17 @@ type inductive_error =
exception InductiveError of inductive_error
+val check_subtyping_arity_constructor : Environ.env ->
+(Term.constr -> Term.constr) -> Term.types -> int -> bool -> unit
+
+(* This needs not be exposed. Exposing for debugging purposes! *)
+val check_subtyping : Entries.mutual_inductive_entry ->
+Context.Rel.t ->
+Environ.env ->
+('b * 'c * Term.types array *
+ ('d * ('e * Term.types * 'f, 'g) Declarations.declaration_arity))
+array -> unit
+
(** The following function does checks on inductive declarations. *)
val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a872a103a..33dd53a5b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -500,7 +500,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if mind.Declarations.mind_polymorphic then
begin
let num_param_arity =
- Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
+ mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_nrealargs
in
if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
fall_back ()
@@ -535,7 +535,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then
fall_back ()
else
- begin (* we don't consider subtyping for constructors. *)
+ begin (* we consider subtyping for constructors. *)
let uinfind = mind.Declarations.mind_universes in
let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in
diff --git a/library/declare.ml b/library/declare.ml
index fcaadaa6e..bf5313545 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -364,9 +364,9 @@ let infer_inductive_subtyping (pth, mind_ent) =
let env' =
Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env
in
- let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in
- let evd = Evd.from_env env'' in
- (pth, Inductiveops.infer_inductive_subtyping env'' evd mind_ent)
+ (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
+ let evd = Evd.from_env env' in
+ (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
end
else (pth, mind_ent)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index eb8a0c85a..ea22c3708 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -494,7 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
if mind.Declarations.mind_polymorphic then
begin
let num_param_arity =
- Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt)
+ mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
in
if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
UnifFailure (evd, NotSameHead)
@@ -520,7 +520,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
if mind.Declarations.mind_polymorphic then
begin
let num_cnstr_args =
- let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in
+ let nparamsctxt =
+ mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+ in
nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1)
in
if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1f8600dc2..ebfb1f8a7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -659,14 +659,22 @@ let control_only_guard env c =
(* inference of subtyping condition for inductive types *)
let infer_inductive_subtyping_arity_constructor
- (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity =
+ (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) =
+ let numchecked = ref 0 in
+ let numparams = Context.Rel.nhyps params in
let update_contexts (env, evd, csts) csts' =
(Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
in
let basic_check (env, evd, csts) tp =
- let csts' =
- Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
- in update_contexts (env, evd, csts) csts'
+ let result =
+ if !numchecked >= numparams then
+ let csts' =
+ Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
+ in update_contexts (env, evd, csts) csts'
+ else
+ (env, evd, csts)
+ in
+ numchecked := !numchecked + 1; result
in
let infer_typ typ ctxs =
match typ with
@@ -680,12 +688,14 @@ let infer_inductive_subtyping_arity_constructor
end
| _ -> anomaly (Pp.str "")
in
- let typs, codom = Reduction.dest_prod env arcn in
+ let arcn' = Term.it_mkProd_or_LetIn arcn params in
+ let typs, codom = Reduction.dest_prod env arcn' in
let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
if not is_arity then basic_check last_contexts codom else last_contexts
let infer_inductive_subtyping env evd mind_ent =
- let { Entries.mind_entry_inds = entries;
+ let { Entries.mind_entry_params = params;
+ Entries.mind_entry_inds = entries;
Entries.mind_entry_polymorphic = poly;
Entries.mind_entry_universes = ground_uinfind;
} = mind_ent
@@ -704,15 +714,16 @@ let infer_inductive_subtyping env evd mind_ent =
let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in
let (_, _, subtyp_constraints) =
List.fold_left
- (fun ctxs indentry ->
- let ctxs' = infer_inductive_subtyping_arity_constructor
- ctxs dosubst indentry.Entries.mind_entry_arity true
- in
- List.fold_left
- (fun ctxs cons ->
- infer_inductive_subtyping_arity_constructor ctxs dosubst cons false)
- ctxs' indentry.Entries.mind_entry_lc
- ) (env', evd', Univ.Constraint.empty) entries
+ (fun ctxs indentry ->
+ let _, params = Typeops.infer_local_decls env params in
+ let ctxs' = infer_inductive_subtyping_arity_constructor
+ ctxs dosubst indentry.Entries.mind_entry_arity true params
+ in
+ List.fold_left
+ (fun ctxs cons ->
+ infer_inductive_subtyping_arity_constructor ctxs dosubst cons false params)
+ ctxs' indentry.Entries.mind_entry_lc
+ ) (env', evd', Univ.Constraint.empty) entries
in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
Univ.UContext.make
(Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7d89b1b2b..811f47f39 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -201,6 +201,10 @@ val type_of_inductive_knowing_conclusion :
val control_only_guard : env -> types -> unit
(* inference of subtyping condition for inductive types *)
+(* for debugging purposes only to be removed *)
+val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t ->
+(Term.constr -> Term.constr) ->
+Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
Entries.mutual_inductive_entry
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 66ff55edc..3e90825ab 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -316,6 +316,26 @@ Module Hurkens'.
Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+Section test_letin_subtyping.
+ Universe i j k i' j' k'.
+ Constraint j < j'.
+
+ Context (W : Type) (X : box@{i j k} W).
+ Definition Y := X : box@{i' j' k'} W.
+
+ Universe i1 j1 k1 i2 j2 k2.
+ Constraint i1 < i2, k2 < k1.
+ Definition Z : box@{i1 j1 k1} W := {| unwrap := W |}.
+ Definition Z' : box@{i2 j2 k2} W := {| unwrap := W |}.
+ Lemma ZZ' : @eq (box@{i2 j2 k2} W) Z Z'.
+ Proof.
+ Set Printing All. Set Printing Universes.
+ cbv.
+ reflexivity.
+ Qed.
+
+End test_letin_subtyping.
+
Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
diff --git a/vernac/command.ml b/vernac/command.ml
index 116a7aee1..6c5997623 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -662,7 +662,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
}
in
(if poly then
- Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent
+ Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
else mind_ent), pl, impls
(* Very syntactical equality *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 84312594d..093a31c19 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -410,9 +410,9 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
begin
let env = Global.env () in
let env' = Environ.push_context (Univ.UInfoInd.univ_context ctx) env in
- let env'' = Environ.push_rel_context params env' in
- let evd = Evd.from_env env'' in
- Inductiveops.infer_inductive_subtyping env'' evd mie
+ (* let env'' = Environ.push_rel_context params env' in *)
+ let evd = Evd.from_env env' in
+ Inductiveops.infer_inductive_subtyping env' evd mie
end
else
mie
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 06:07:26 +0000