diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 32 |
1 files changed, 23 insertions, 9 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8e9b606a58..cfca335d32 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -234,22 +234,32 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in - let sbsubst = CumulativityInfo.subtyping_susbst cumi in - let dosubst = subst_univs_level_constr sbsubst in let uctx = CumulativityInfo.univ_context cumi 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 new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in + let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) + LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels + in + let dosubst = subst_univs_level_constr lmap in + let instance_other = Instance.of_array new_levels in + let constraints_other = Univ.subst_univs_level_constraints lmap (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 env = push_context (CumulativityInfo.subtyp_context cumi) env in + let subtyp_constraints = + CumulativityInfo.leq_constraints cumi + (UContext.instance uctx) instance_other + Constraint.empty + in + let env = Environ.add_constraints subtyp_constraints env in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor env dosubst full_arity numparams true; Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc - | TemplateArity _ -> () + | TemplateArity _ -> + anomaly ~label:"check_subtyping" + Pp.(str "template polymorphism and cumulative polymorphism are not compatible") ) inds (* Type-check an inductive definition. Does not check positivity @@ -710,7 +720,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( best-effort fashion. *) let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in - let recursive = finite != Decl_kinds.BiFinite in + let recursive = finite != BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let ra_env_ar = Array.rev_to_list rc in let nparamsctxt = Context.Rel.length paramsctxt in @@ -879,9 +889,13 @@ let abstract_inductive_universes iu = match iu with | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) | Polymorphic_ind_entry ctx -> - let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx) + let (inst, auctx) = Univ.abstract_universes ctx in + let inst = Univ.make_instance_subst inst in + (inst, Polymorphic_ind auctx) | Cumulative_ind_entry cumi -> - let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi) + let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + let inst = Univ.make_instance_subst inst in + (inst, Cumulative_ind acumi) let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in |