From 131236fafdc2208e509b110d203d4b26cd4a98ac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 14 Nov 2023 15:55:25 +0100 Subject: [PATCH 01/10] Be compatible with variable relevance inductives --- interp/impargs.ml | 2 +- kernel/cClosure.ml | 17 ++++++++++------- kernel/environ.ml | 8 ++++---- kernel/environ.mli | 7 +++++-- kernel/indtypes.ml | 2 +- kernel/inductive.ml | 29 +++++++++++++++++------------ kernel/inductive.mli | 4 +++- kernel/relevanceops.ml | 6 ++---- pretyping/cases.ml | 4 ++-- pretyping/inductiveops.ml | 6 +++--- tactics/eqschemes.ml | 16 ++++++++-------- tactics/tactics.ml | 2 +- vernac/record.ml | 2 +- 13 files changed, 58 insertions(+), 47 deletions(-) diff --git a/interp/impargs.ml b/interp/impargs.ml index 976c16eda9f6..83804729397d 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -472,7 +472,7 @@ let compute_mib_implicits flags kn = (fun i mip -> (* No need to care about constraints here *) let ty, _ = Typeops.type_of_global_in_context env (GlobRef.IndRef (kn,i)) in - let r = Inductive.relevance_of_inductive env (kn,i) in + let r = (snd @@ Inductive.lookup_mind_specif env (kn,i)).mind_relevance in Context.Rel.Declaration.LocalAssum (Context.make_annot (Name mip.mind_typename) r, ty)) mib.mind_packets) in let env_ar = Environ.push_rel_context ar env in diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 8ee97da5a111..37a286cfa230 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -799,7 +799,7 @@ let inductive_subst mib u pms = mk_pms (Array.length pms - 1) mib.mind_params_ctxt, u (* Iota-reduction: feed the arguments of the constructor to the branch *) -let get_branch infos depth ci u pms (ind, c) br e args = +let get_branch infos depth ci pms ((ind, c), u) br e args = let i = c - 1 in let args = drop_parameters depth ci.ci_npar args in let (_nas, br) = br.(i) in @@ -1240,9 +1240,11 @@ let rec skip_irrelevant_stack info stk = match stk with let () = update m mk_irrelevant.mark mk_irrelevant.term in skip_irrelevant_stack info s -let is_irrelevant_constructor infos (ind,_) = match infos.i_cache.i_mode with -| Conversion -> Indset_env.mem ind infos.i_cache.i_env.irr_inds -| Reduction -> false +let is_irrelevant_constructor infos ((ind,_),u) = + match Indmap_env.find_opt ind (info_env infos).Environ.irr_inds with + | None -> false + | Some r -> + is_irrelevant infos @@ UVars.subst_instance_relevance u r (*********************************************************************) (* A machine that inspects the head of a term until it finds an @@ -1361,14 +1363,15 @@ let rec knr info tab m stk = (* Similarly to fix, partially applied primitives are not Ntrl! *) (m, stk) | Undef _ | OpaqueDef _ -> (set_ntrl m; (m,stk))) - | FConstruct(c,_u) -> + | FConstruct c -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in if use_match || use_fix then (match [@ocaml.warning "-4"] strip_update_shift_app m stk with - | (depth, args, ZcaseT(ci,u,pms,_,br,e)::s) when use_match -> + | (depth, args, ZcaseT(ci,_,pms,_,br,e)::s) when use_match -> assert (ci.ci_npar>=0); - let (br, e) = get_branch info depth ci u pms c br e args in + (* instance on the case and instance on the constructor are compatible by typing *) + let (br, e) = get_branch info depth ci pms c br e args in knit info tab e br s | (_, cargs, Zfix(fx,par)::s) when use_fix -> let rarg = fapp_stack(m,cargs) in diff --git a/kernel/environ.ml b/kernel/environ.ml index 1885f0e2256b..067aa7f75fc9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -83,7 +83,7 @@ type env = { env_universes_lbound : UGraph.Bound.t; env_qualities : Sorts.QVar.Set.t; irr_constants : Sorts.relevance Cmap_env.t; - irr_inds : Indset_env.t; + irr_inds : Sorts.relevance Indmap_env.t; env_typing_flags : typing_flags; retroknowledge : Retroknowledge.retroknowledge; } @@ -113,7 +113,7 @@ let empty_env = { env_universes_lbound = UGraph.Bound.Set; env_qualities = Sorts.QVar.Set.empty; irr_constants = Cmap_env.empty; - irr_inds = Indset_env.empty; + irr_inds = Indmap_env.empty; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; } @@ -644,8 +644,8 @@ let add_mind_key kn (mind, _ as mind_key) env = Globals.inductives = new_inds; } in let irr_inds = Array.fold_left_i (fun i irr_inds mip -> - if mip.mind_relevance == Sorts.Irrelevant - then Indset_env.add (kn, i) irr_inds + if mip.mind_relevance != Sorts.Relevant + then Indmap_env.add (kn, i) mip.mind_relevance irr_inds else irr_inds) env.irr_inds mind.mind_packets in { env with irr_inds; env_globals = new_globals } diff --git a/kernel/environ.mli b/kernel/environ.mli index 5ed491d30686..b7a8ef4bc404 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -74,8 +74,11 @@ type env = private { env_universes : UGraph.t; env_universes_lbound : UGraph.Bound.t; env_qualities : Sorts.QVar.Set.t; - irr_constants : Sorts.relevance Cmap_env.t; - irr_inds : Indset_env.t; + irr_constants : Sorts.relevance Cmap_env.t +(** [irr_constants] is a cache of the relevances which are not Relevant. + In other words, [const_relevance == Option.default Relevant (find_opt con irr_constants)]. *); + irr_inds : Sorts.relevance Indmap_env.t +(** [irr_inds] is a cache of the relevances which are not Relevant. cf [irr_constants]. *); env_typing_flags : typing_flags; retroknowledge : Retroknowledge.retroknowledge; } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 182d433fa96b..9627f607044e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -160,7 +160,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let specif = (lookup_mind_specif env mi, u) in let ty = type_of_inductive specif in let env' = - let r = (snd (fst specif)).mind_relevance in + let r = Inductive.relevance_of_ind_body (snd (fst specif)) u in let anon = Context.make_annot Anonymous r in let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in push_rel decl env in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f6c9d3b490ae..43bb8dd71f21 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -216,9 +216,12 @@ let instantiate_universes ctx (templ, ar) args = (* Type of an inductive type *) -let relevance_of_inductive env ind = +let relevance_of_ind_body mip u = + UVars.subst_instance_relevance u mip.mind_relevance + +let relevance_of_inductive env (ind,u) = let _, mip = lookup_mind_specif env ind in - mip.mind_relevance + relevance_of_ind_body mip u let check_instance mib u = if not (match mib.mind_universes with @@ -352,7 +355,7 @@ let expand_arity (mib, mip) (ind, u) params nas = let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in mkApp (mkIndU (ind, u), args) in - let na = Context.make_annot Anonymous mip.mind_relevance in + let na = Context.make_annot Anonymous (relevance_of_ind_body mip u) in let realdecls = LocalAssum (na, self) :: realdecls in instantiate_context u params nas realdecls @@ -722,7 +725,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind mip env = - let r = mip.mind_relevance in + let r = relevance_of_ind_body mip u in let anon = Context.make_annot Anonymous r in let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive ((mib,mip),u)) lpar) in push_rel decl env @@ -1430,16 +1433,18 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") | _ -> raise_err env i NotEnoughAbstractionInFixBody in - let ((ind, _), _) as res = check_occur fixenv 1 def in + let ((ind, u), _) as res = check_occur fixenv 1 def in let _, mip = lookup_mind_specif env ind in (* recursive sprop means non record with projections -> squashed *) - if mip.mind_relevance == Sorts.Irrelevant && - not (Environ.is_type_in_type env (GlobRef.IndRef ind)) - then - begin - if not (names.(i).Context.binder_relevance == Sorts.Irrelevant) - then raise_err env i FixpointOnIrrelevantInductive - end; + let () = + if Environ.is_type_in_type env (GlobRef.IndRef ind) then () + else match relevance_of_ind_body mip u with + | Sorts.Irrelevant | Sorts.RelevanceVar _ -> + (* XXX if RelevanceVar also allow binder_relevance = the same var? *) + if not (names.(i).Context.binder_relevance == Sorts.Irrelevant) + then raise_err env i FixpointOnIrrelevantInductive + | Sorts.Relevant -> () + in res in (* Do it on every fixpoint *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 4a17b5f6f956..6ab1fbefc308 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -55,7 +55,9 @@ val constrained_type_of_inductive : mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : mind_specif puniverses -> param_univs -> types constrained -val relevance_of_inductive : env -> inductive -> Sorts.relevance +val relevance_of_ind_body : one_inductive_body -> UVars.Instance.t -> Sorts.relevance + +val relevance_of_inductive : env -> pinductive -> Sorts.relevance val type_of_inductive : mind_specif puniverses -> types diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml index 36517e877c5a..e4a4342bee7b 100644 --- a/kernel/relevanceops.ml +++ b/kernel/relevanceops.ml @@ -28,10 +28,8 @@ let relevance_of_constant env (c,u) = let decl = lookup_constant c env in UVars.subst_instance_relevance u decl.const_relevance -let relevance_of_constructor env (((mi,i),_),u) = - let decl = lookup_mind mi env in - let packet = decl.mind_packets.(i) in - UVars.subst_instance_relevance u packet.mind_relevance +let relevance_of_constructor env ((ind,_),u) = + Inductive.relevance_of_inductive env (ind,u) let relevance_of_projection_repr env (p, u) = let mib = lookup_mind (Names.Projection.Repr.mind p) env in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 687950171b13..0f83314d922b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1979,7 +1979,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = (str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in - let ((ind,u),_) = dest_ind_family indf' in + let ((ind,_ as indu),_) = dest_ind_family indf' in let nrealargs_ctxt = inductive_nrealdecls env0 ind in let arsign = get_arity env0 indf' in let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in @@ -1993,7 +1993,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in - let r = Inductive.relevance_of_inductive env0 ind in + let r = Inductive.relevance_of_inductive env0 indu in let t = EConstr.of_constr (build_dependent_inductive env0 indf') in LocalAssum (make_annot na r, t) :: List.map2 RelDecl.set_name realnal arsign in let rec buildrec n = function diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 5dc8a8294a1b..ea2dda6330c5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -74,7 +74,7 @@ let lift_inductive_family n = liftn_inductive_family n 1 let substnl_ind_family l n = map_ind_family (substnl l n) -let relevance_of_inductive_family env ((ind,_),_ : inductive_family) = +let relevance_of_inductive_family env (ind,_ : inductive_family) = Inductive.relevance_of_inductive env ind type inductive_type = IndType of inductive_family * EConstr.constr list @@ -430,7 +430,7 @@ let build_dependent_inductive env ((ind, params) as indf) = (* builds the arity of an elimination predicate in sort [s] *) -let make_arity_signature env sigma dep ((ind,_), _ as indf) = +let make_arity_signature env sigma dep (ind, _ as indf) = let arsign = get_arity env indf in let r = Inductive.relevance_of_inductive env ind in let anon = make_annot Anonymous r in @@ -577,7 +577,7 @@ let find_coinductive env sigma c = (* Type of Case predicates *) let arity_of_case_predicate env (ind,params) dep k = let arsign = get_arity env (ind,params) in - let r = Inductive.relevance_of_inductive env (fst ind) in + let r = Inductive.relevance_of_inductive env ind in let mind = build_dependent_inductive env (ind,params) in let concl = if dep then mkArrow mind r (mkSort k) else mkSort k in Term.it_mkProd_or_LetIn concl arsign diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index d35b60e6b12b..dbc1939be465 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -204,10 +204,10 @@ let build_sym_scheme env _handle ind = get_sym_eq_data env indu in let cstr n = mkApp (mkConstructUi(indu,1),Context.Rel.instance mkRel n mib.mind_params_ctxt) in - let inds = snd (mind_arity mip) in + let inds = inductive_sort_family mip in let varH,_ = fresh env (default_id_of_sort inds) Id.Set.empty in let applied_ind = build_dependent_inductive indu specif in - let indr = Sorts.relevance_of_sort_family inds in + let indr = UVars.subst_instance_relevance u mip.mind_relevance in let realsign_ind = name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in let rci = Sorts.Relevant in (* TODO relevance *) @@ -267,8 +267,8 @@ let build_sym_involutive_scheme env handle ind = let eq,eqrefl,ctx = get_coq_eq env ctx in let sym, ctx = const_of_scheme sym_scheme_kind env handle ind ctx in let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.instance mkRel n paramsctxt) in - let inds = snd (mind_arity mip) in - let indr = Sorts.relevance_of_sort_family inds in + let inds = inductive_sort_family mip in + let indr = UVars.subst_instance_relevance u mip.mind_relevance in let varH,_ = fresh env (default_id_of_sort inds) Id.Set.empty in let applied_ind = build_dependent_inductive indu specif in let applied_ind_C = @@ -383,8 +383,8 @@ let build_l2r_rew_scheme dep env handle ind kind = mkApp (mkConstructUi(indu,1), Array.concat [Context.Rel.instance mkRel n paramsctxt1; rel_vect p nrealargs]) in - let inds = snd (mind_arity mip) in - let indr = Sorts.relevance_of_sort_family inds in + let inds = inductive_sort_family mip in + let indr = UVars.subst_instance_relevance u mip.mind_relevance in let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in let varHC,avoid = fresh env (Id.of_string "HC") avoid in let varP,_ = fresh env (Id.of_string "P") avoid in @@ -501,8 +501,8 @@ let build_l2r_forward_rew_scheme dep env ind kind = mkApp (mkConstructUi(indu,1), Array.concat [Context.Rel.instance mkRel n paramsctxt1; rel_vect p nrealargs]) in - let inds = snd (mind_arity mip) in - let indr = Sorts.relevance_of_sort_family inds in + let inds = inductive_sort_family mip in + let indr = UVars.subst_instance_relevance u mip.mind_relevance in let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in let varHC,avoid = fresh env (Id.of_string "HC") avoid in let varP,_ = fresh env (Id.of_string "P") avoid in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index eb4b6ef3ae8b..ca2e8fea18bc 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1716,7 +1716,7 @@ let make_projection env sigma params cstr sign elim i n c (ind, u) = let ci = Inductiveops.make_case_info env ind RegularStyle in let br = [| mknas cs_args, b |] in let args = Context.Rel.instance mkRel 0 sign in - let pnas = Array.append (mknas arity) [|make_annot Anonymous mip.mind_relevance|] in + let pnas = Array.append (mknas arity) [|make_annot Anonymous (Inductive.relevance_of_ind_body mip (EConstr.Unsafe.to_instance u))|] in let p = (pnas, lift (Array.length pnas) t) in let c = mkCase (ci, u, Array.of_list params, (p, get_relevance decl), NoInvert, mkApp (c, args), br) in Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign) diff --git a/vernac/record.ml b/vernac/record.ml index f0cb29feb7b0..130e5de0e857 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -476,7 +476,7 @@ let declare_projections indsp univs ?(kind=Decls.StructureComponent) inhabitant_ let r = mkIndU (indsp,uinstance) in let rp = applist (r, Context.Rel.instance_list mkRel 0 paramdecls) in let paramargs = Context.Rel.instance_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*) - let x = make_annot (Name inhabitant_id) mip.mind_relevance in + let x = make_annot (Name inhabitant_id) (Inductive.relevance_of_ind_body mip uinstance) in let fields = instantiate_possibly_recursive_type (fst indsp) uinstance mib.mind_ntypes paramdecls fields in let lifted_fields = Vars.lift_rel_context 1 fields in let primitive = From 82ff8a4f4ae00f6cc58d9bf847badb4ba4a17c0f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 14 Nov 2023 17:30:24 +0100 Subject: [PATCH 02/10] Fix tiny typo in comments --- kernel/declarations.mli | 2 +- vernac/comInductive.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 496a988579cb..bbd8c9512137 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -209,7 +209,7 @@ type one_inductive_body = { (possibly with let-ins). This context is internally represented as a list [[cstrdecl_ij{q_ij};...;cstrdecl_ij1;paramdecl_m;...;paramdecl_1]] such that the constructor in fine has type [forall paramdecls, - forall cstrdecls_ij, Ii params realargs_ij]] with [params] referring to + forall cstrdecls_ij, Ii params realargs_ij] with [params] referring to the assumptions of [paramdecls] and [realargs_ij] being the "indices" specific to the constructor. *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7fa830dd260f..eda9c9e4d33c 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -299,7 +299,7 @@ let inductive_levels env evd arities ctors = else ind) inds in - (* Add constraints from constructor arguments and indices.Q + (* Add constraints from constructor arguments and indices. We must do this after Prop lowering as otherwise we risk unifying sorts eg on "Box (A:Type)" we risk unifying the parameter sort and the output sort then ESorts.equal would make us believe that the constructor argument is a lowering candidate. From 16ae249adb28ef7ec0143aa833afab43ca101c66 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 14 Nov 2023 17:37:48 +0100 Subject: [PATCH 03/10] Remove Inductive.mind_arity (returning rel_context * Sorts.family) --- kernel/inductive.ml | 3 --- kernel/inductive.mli | 2 -- tactics/eqschemes.ml | 2 +- 3 files changed, 1 insertion(+), 6 deletions(-) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 43bb8dd71f21..54d1718d8014 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -309,9 +309,6 @@ let inductive_sort_family mip = | RegularArity s -> Sorts.family s.mind_sort | TemplateArity _ -> Sorts.InType -let mind_arity mip = - mip.mind_arity_ctxt, inductive_sort_family mip - let elim_sort (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 6ab1fbefc308..bd7bca786ef5 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -124,8 +124,6 @@ val build_branches_type : constr list -> constr -> types array (** Return the arity of an inductive type *) -val mind_arity : one_inductive_body -> Constr.rel_context * Sorts.family - val inductive_sort_family : one_inductive_body -> Sorts.family (** Check a [case_info] actually correspond to a Case expression on the diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index dbc1939be465..08d1383f655a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -596,7 +596,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let cstr n = mkApp (mkConstructUi(indu,1),Context.Rel.instance mkRel n mib.mind_params_ctxt) in let constrargs_cstr = constrargs@[cstr 0] in - let inds = snd (mind_arity mip) in + let inds = inductive_sort_family mip in let indr = Sorts.relevance_of_sort_family inds in let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in let varHC,avoid = fresh env (Id.of_string "HC") avoid in From f0cbec627ff0f1ccd9cc5e22cab9fc9e7b68d5f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 14 Nov 2023 17:49:37 +0100 Subject: [PATCH 04/10] Declarations.mind_kelim : family ==> mind_squashed : bool The family is redundant with the sort info in mind_arity. --- checker/checkInductive.ml | 7 ++++--- checker/values.ml | 3 +-- kernel/declarations.mli | 2 +- kernel/declareops.ml | 2 +- kernel/discharge.ml | 2 +- kernel/indTyping.ml | 17 +---------------- kernel/indTyping.mli | 2 +- kernel/indtypes.ml | 4 ++-- kernel/inductive.ml | 4 +++- kernel/subtyping.ml | 2 +- kernel/type_errors.ml | 4 ++-- kernel/type_errors.mli | 4 ++-- kernel/typeops.ml | 6 +++--- pretyping/inductiveops.ml | 4 ++-- pretyping/pretype_errors.mli | 2 +- pretyping/typing.ml | 3 +-- tactics/tactics.ml | 4 ++-- vernac/assumptions.ml | 2 +- vernac/himsg.ml | 4 ++-- vernac/record.ml | 4 ++-- 20 files changed, 34 insertions(+), 48 deletions(-) diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 9bca850c2a0a..aa4a602525d8 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -98,7 +98,8 @@ let check_template ar1 ar2 = match ar1, ar2 with ContextSet.equal template_context ar.template_context | None, Some _ | Some _, None -> false -let check_kelim k1 k2 = Sorts.family_leq k1 k2 +(* if the generated inductive is squashed the original one must be squashed *) +let check_squashed k1 k2 = if k2 then k1 else true (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. @@ -122,7 +123,7 @@ let eq_in_context (ctx1, t1) (ctx2, t2) = let check_packet env mind ind { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc; - mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc; + mind_nrealargs; mind_nrealdecls; mind_squashed; mind_nf_lc; mind_consnrealargs; mind_consnrealdecls; mind_recargs; mind_relevance; mind_nb_constant; mind_nb_args; mind_reloc_tbl } = let check = check mind in @@ -134,7 +135,7 @@ let check_packet env mind ind check "mind_user_lc" (Array.equal Constr.equal ind.mind_user_lc mind_user_lc); check "mind_nrealargs" Int.(equal ind.mind_nrealargs mind_nrealargs); check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); - check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim); + check "mind_squashed" (check_squashed ind.mind_squashed mind_squashed); check "mind_nf_lc" (Array.equal eq_in_context ind.mind_nf_lc mind_nf_lc); (* NB: here syntactic equality is not just an optimisation, we also diff --git a/checker/values.ml b/checker/values.ml index 79fed03c992e..fc2c07af825d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -116,7 +116,6 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|];[|v_qvar;v_univ(*QSort*)|]|] -let v_sortfam = v_enum "sorts_family" 4 let v_relevance = v_sum "relevance" 2 [|[|v_qvar|]|] let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|] @@ -290,7 +289,7 @@ let v_one_ind = v_tuple "one_inductive_body" Array v_constr; Int; Int; - v_sortfam; + v_bool; Array (v_pair v_rctxt v_constr); Array Int; Array Int; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index bbd8c9512137..e41348530fdf 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -198,7 +198,7 @@ type one_inductive_body = { mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) - mind_kelim : Sorts.family; (** Highest allowed elimination sort *) + mind_squashed : bool; (** Is elimination restricted to the inductive's sort? *) mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 6cbda4ae677d..97f69213a7f8 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -247,7 +247,7 @@ let subst_mind_packet subst mbp = mind_user_lc = Array.Smart.map (subst_mps subst) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealdecls = mbp.mind_nrealdecls; - mind_kelim = mbp.mind_kelim; + mind_squashed = mbp.mind_squashed; mind_recargs = subst_wf_paths subst mbp.mind_recargs (*wf_paths*); mind_relevance = mbp.mind_relevance; mind_nb_constant = mbp.mind_nb_constant; diff --git a/kernel/discharge.ml b/kernel/discharge.ml index 9d4758a1e9b3..7c2c552d5a76 100644 --- a/kernel/discharge.ml +++ b/kernel/discharge.ml @@ -136,7 +136,7 @@ let cook_one_ind cache ~ntypes mip = mind_user_lc; mind_nrealargs = mip.mind_nrealargs; mind_nrealdecls = mip.mind_nrealdecls; - mind_kelim = mip.mind_kelim; + mind_squashed = mip.mind_squashed; mind_nf_lc; mind_consnrealargs = mip.mind_consnrealargs; mind_consnrealdecls = mip.mind_consnrealdecls; diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 928f4d0e1d36..946abd625589 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -242,20 +242,6 @@ let check_record data = | _ -> false)) data -(* Allowed eliminations *) - -(* Previous comment: *) -(* Unitary/empty Prop: elimination to all sorts are realizable *) -(* unless the type is large. If it is large, forbids large elimination *) -(* which otherwise allows simulating the inconsistent system Type:Type. *) -(* -> this is now handled by is_smashed: *) -(* - 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_template=_;record_arg_info=_;missing=_} = - if not ind_squashed then InType - else Sorts.family ind_univ - (* For a level to be template polymorphic, it must be introduced by the definition (so have no constraint except lbound <= l) and not to be constrained from below, so any universe l' <= l @@ -340,8 +326,7 @@ let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) = RegularArity {mind_user_arity = arity; mind_sort = ind_univ} in - let kelim = allowed_sorts univ_info in - (arity,lc), (indices,splayed_lc), kelim + (arity,lc), (indices,splayed_lc), univ_info.ind_squashed let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 426d8c76ec94..0603feca0f4d 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -35,5 +35,5 @@ val typecheck_inductive : env -> sec_univs:UVars.Instance.t option * Constr.rel_context * ((inductive_arity * Constr.types array) * (Constr.rel_context * (Constr.rel_context * Constr.types) array) * - Sorts.family) + bool (* squashed *)) array diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9627f607044e..52902e5588f6 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -483,7 +483,7 @@ let build_inductive env ~sec_univs names prv univs template variance let u = UVars.make_abstract_instance (universes_context univs) in let subst = List.init ntypes (fun i -> mkIndU ((kn, ntypes - i - 1), u)) in (* Check one inductive *) - let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg = + let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),squashed) recarg = let lc = Array.map (substl subst) lc in (* Type of constructors in normal form *) let nf_lc = @@ -519,7 +519,7 @@ let build_inductive env ~sec_univs names prv univs template variance mind_arity_ctxt = indices @ paramsctxt; mind_nrealargs = Context.Rel.nhyps indices; mind_nrealdecls = Context.Rel.length indices; - mind_kelim = kelim; + mind_squashed = squashed; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealdecls; mind_consnrealargs = consnrealargs; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 54d1718d8014..6e569c1bd85a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -309,7 +309,9 @@ let inductive_sort_family mip = | RegularArity s -> Sorts.family s.mind_sort | TemplateArity _ -> Sorts.InType -let elim_sort (_,mip) = mip.mind_kelim +let elim_sort (_,mip) = + if not mip.mind_squashed then Sorts.InType + else inductive_sort_family mip let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 0b19c8e8c4f8..de5133fbc4a3 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -139,7 +139,7 @@ let check_inductive (cst, ustate) trace env mp1 l info1 mp2 mib2 subst1 subst2 r let check f test why = if not (test (f p1) (f p2)) then error why in check (fun p -> p.mind_consnames) (Array.equal Id.equal) NotSameConstructorNamesField; check (fun p -> p.mind_typename) Id.equal NotSameInductiveNameInBlockField; - check (fun p -> p.mind_kelim) Sorts.family_equal (NotConvertibleInductiveField p2.mind_typename); + check (fun p -> p.mind_squashed) Bool.equal (NotConvertibleInductiveField p2.mind_typename); (* nf_lc later *) (* nf_arity later *) (* user_lc ignored *) diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 93985c5a2d6f..88542fb935ed 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -56,7 +56,7 @@ type ('constr, 'types) ptype_error = | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * - (('constr, 'types) punsafe_judgment * Sorts.family * Sorts.family * Sorts.family) option + (('constr, 'types) punsafe_judgment * Sorts.family * Sorts.family) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | CaseOnPrivateInd of inductive | WrongCaseInfo of pinductive * case_info @@ -214,7 +214,7 @@ let map_ptype_error f = function | NotAType j -> NotAType (on_judgment f j) | BadAssumption j -> BadAssumption (on_judgment f j) | ElimArity (pi, c, ar) -> - ElimArity (pi, f c, Option.map (fun (j, s1, s2, s3) -> (on_judgment f j, s1, s2, s3)) ar) + ElimArity (pi, f c, Option.map (fun (j, s1, s2) -> (on_judgment f j, s1, s2)) ar) | CaseNotInductive j -> CaseNotInductive (on_judgment f j) | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci) | NumberBranches (j, n) -> NumberBranches (on_judgment f j, n) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 9e6dabe455c8..e28f5c328546 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -58,7 +58,7 @@ type ('constr, 'types) ptype_error = | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * - (('constr, 'types) punsafe_judgment * Sorts.family * Sorts.family * Sorts.family) option + (('constr, 'types) punsafe_judgment * Sorts.family * Sorts.family) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | CaseOnPrivateInd of inductive | WrongCaseInfo of pinductive * case_info @@ -120,7 +120,7 @@ val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a val error_elim_arity : env -> pinductive -> constr -> - (unsafe_judgment * Sorts.family * Sorts.family * Sorts.family) option -> 'a + (unsafe_judgment * Sorts.family * Sorts.family) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index a54322eb53a5..30e218f11e03 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -552,10 +552,10 @@ let type_of_case env (mib, mip as specif) ci u pms (pctx, pnas, p, rp, pt) iv c in let () = let ksort = Sorts.family sp in - if not (Sorts.family_leq ksort mip.mind_kelim) then - let s = inductive_sort_family mip in + let s = elim_sort specif in + if not (Sorts.family_leq ksort s) then let pj = make_judge (it_mkLambda_or_LetIn p pctx) (it_mkProd_or_LetIn pt pctx) in - let kinds = Some (pj, mip.mind_kelim, ksort, s) in + let kinds = Some (pj, ksort, s) in error_elim_arity env (ind, u') c kinds in (* Check that the scrutinee has the right type *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ea2dda6330c5..c3395038ab5b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -231,8 +231,8 @@ let inductive_has_local_defs env ind = not (Int.equal l1 l2) let top_allowed_sort env (kn,i as ind) = - let (mib,mip) = Inductive.lookup_mind_specif env ind in - mip.mind_kelim + let specif = Inductive.lookup_mind_specif env ind in + Inductive.elim_sort specif let sorts_below top = List.filter (fun s -> Sorts.family_leq s top) Sorts.[InSProp;InProp;InSet;InType] diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 89968c052f83..69a3bfef0b33 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -116,7 +116,7 @@ val error_ill_typed_rec_body : val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> pinductive -> constr -> - (unsafe_judgment * Sorts.family * Sorts.family * Sorts.family) option -> 'b + (unsafe_judgment * Sorts.family * Sorts.family) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 846672d6d0f0..66dad388ad80 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -270,8 +270,7 @@ let check_allowed_sort env sigma ind c p = | InQSort -> InType (* FIXME *) in if not (Sorts.family_leq ksort sorts) then - let s = inductive_sort_family (snd specif) in - error_elim_arity env sigma ind c (Some (pj, sorts, ksort, s)) + error_elim_arity env sigma ind c (Some (pj, ksort, sorts)) else Sorts.relevance_of_sort sort diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ca2e8fea18bc..1ce6e55c6328 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1707,10 +1707,10 @@ let make_projection env sigma params cstr sign elim i n c (ind, u) = && not (isEvar sigma (fst (whd_betaiota_stack env sigma t))) && (not (isRel sigma t)) then - let (_, mip) = Inductive.lookup_mind_specif env ind in + let (_, mip) as specif = Inductive.lookup_mind_specif env ind in let t = lift (i + 1 - n) t in let ksort = Retyping.get_sort_family_of (push_rel_context sign env) sigma t in - if Sorts.family_leq ksort mip.mind_kelim then + if Sorts.family_leq ksort (Inductive.elim_sort specif) then let arity = List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt in let mknas ctx = Array.of_list (List.rev_map get_annot ctx) in let ci = Inductiveops.make_case_info env ind RegularStyle in diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 24158e38ae6f..b0ed95748273 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -334,7 +334,7 @@ let type_of_constant cb = cb.Declarations.const_type let uses_uip mib = Array.exists (fun mip -> - mip.mind_kelim == InType + not mip.mind_squashed && mip.mind_relevance == Sorts.Irrelevant && Array.length mip.mind_nf_lc = 1 && List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5f34b0a265ad..b09cb762fca5 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -236,9 +236,9 @@ let explain_elim_arity env sigma ind c okinds = let pi = pr_inductive env (fst ind) in let pc = pr_leconstr_env env sigma c in let msg = match okinds with - | Some (pj, sorts, kp, ki) -> + | Some (pj, kp, ki) -> let explanation = error_elim_explain kp ki in - let sorts = Inductiveops.sorts_below sorts in + let sorts = Inductiveops.sorts_below ki in let pki = Sorts.pr_sort_family ki in let pkp = Sorts.pr_sort_family kp in let explanation = match explanation with diff --git a/vernac/record.ml b/vernac/record.ml index 130e5de0e857..cd06859fec06 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -295,12 +295,12 @@ let warning_or_error ~info flags indsp err = strbrk " not defined.") | BadTypedProj (fi,_ctx,te) -> match te with - | ElimArity (_, _, Some (_, _, (InType | InSet), InProp)) -> + | ElimArity (_, _, Some (_, (InType | InSet), InProp)) -> (Id.print fi ++ strbrk" cannot be defined because it is informative and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") - | ElimArity (_, _, Some (_, _, InType, InSet)) -> + | ElimArity (_, _, Some (_, InType, InSet)) -> (Id.print fi ++ strbrk" cannot be defined because it is large and " ++ Printer.pr_inductive (Global.env()) indsp ++ From 1e741c2777f149ada4624ab970c7fa6312126873 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 17 Nov 2023 17:00:57 +0100 Subject: [PATCH 05/10] Complex squash API in declarations.mli (not yet used) --- checker/checkInductive.ml | 20 +++++++++++- checker/values.ml | 4 ++- kernel/declarations.mli | 11 ++++++- kernel/genlambda.ml | 10 +++--- kernel/indTyping.ml | 44 ++++++++++++++----------- kernel/indTyping.mli | 2 +- kernel/inductive.ml | 57 +++++++++++++++++++++++++++++++-- kernel/inductive.mli | 9 +++++- kernel/subtyping.ml | 8 ++++- kernel/type_errors.ml | 4 +-- kernel/type_errors.mli | 4 +-- kernel/typeops.ml | 12 +++---- kernel/uVars.ml | 17 ++++++---- kernel/uVars.mli | 3 ++ pretyping/cases.ml | 2 +- pretyping/inductiveops.ml | 62 ++++++++++++++++++++++++++++++++++-- pretyping/inductiveops.mli | 6 ++++ pretyping/pretype_errors.ml | 2 ++ pretyping/pretype_errors.mli | 2 +- pretyping/typing.ml | 13 +++----- tactics/tactics.ml | 2 +- vernac/assumptions.ml | 2 +- vernac/auto_ind_decl.ml | 4 +-- vernac/himsg.ml | 4 ++- vernac/himsg.mli | 9 ++++++ vernac/indschemes.ml | 4 +-- vernac/record.ml | 14 +++++--- 27 files changed, 258 insertions(+), 73 deletions(-) diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index aa4a602525d8..466675027dec 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -99,7 +99,25 @@ let check_template ar1 ar2 = match ar1, ar2 with | None, Some _ | Some _, None -> false (* if the generated inductive is squashed the original one must be squashed *) -let check_squashed k1 k2 = if k2 then k1 else true +let check_squashed orig generated = match orig, generated with + | None, None -> true + | Some _, None -> + (* the inductive is from functor instantiation which removed the need for squash *) + true + | None, Some _ -> + (* missing squash *) + false + | Some s1, Some s2 -> + (* functor instantiation can change sort qualities + (from Type -> Prop) + Condition: every quality which can make the generated inductive + squashed must also make the original inductive squashed *) + match s1, s2 with + | AlwaysSquashed, AlwaysSquashed -> true + | AlwaysSquashed, SometimesSquashed _ -> true + | SometimesSquashed _, AlwaysSquashed -> false + | SometimesSquashed s1, SometimesSquashed s2 -> + List.for_all (fun s2 -> List.exists (fun s1 -> Sorts.Quality.equal s1 s2) s1) s2 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. diff --git a/checker/values.ml b/checker/values.ml index fc2c07af825d..dfcaf20d6754 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -281,6 +281,8 @@ let v_mono_ind_arity = let v_ind_arity = v_sum "inductive_arity" 0 [|[|v_mono_ind_arity|];[|v_template_arity|]|] +let v_squash_info = v_sum "squash_info" 1 [|[|List v_quality|]|] + let v_one_ind = v_tuple "one_inductive_body" [|v_id; v_rctxt; @@ -289,7 +291,7 @@ let v_one_ind = v_tuple "one_inductive_body" Array v_constr; Int; Int; - v_bool; + Opt v_squash_info; Array (v_pair v_rctxt v_constr); Array Int; Array Int; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index e41348530fdf..72d0ee47a500 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -164,6 +164,15 @@ type regular_inductive_arity = { type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity +type squash_info = + | AlwaysSquashed + | SometimesSquashed of Sorts.Quality.t list + (** A sort polymorphic inductive [I@{...|...|...} : ... -> Type@{ s|...}] + is squashed at a given instantiation if the qualities in the list are not smaller than [s]. + + NB: if [s] is sort poly and the inductive has >0 constructors + SometimesSquashed contains Prop ie the SProp instantiation is squashed. *) + (** {7 Datas specific to a single type of a block of mutually inductive type } *) type one_inductive_body = { (** {8 Primitive datas } *) @@ -198,7 +207,7 @@ type one_inductive_body = { mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) - mind_squashed : bool; (** Is elimination restricted to the inductive's sort? *) + mind_squashed : squash_info option; (** Is elimination restricted to the inductive's sort? *) mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion diff --git a/kernel/genlambda.ml b/kernel/genlambda.ml index ef6f7ebf7135..274f073b16b5 100644 --- a/kernel/genlambda.ml +++ b/kernel/genlambda.ml @@ -69,11 +69,11 @@ let pp_rel name n = Name.print name ++ str "##" ++ int n let pp_sort s = - match Sorts.family s with - | Sorts.InSet -> str "Set" - | Sorts.InProp -> str "Prop" - | Sorts.InSProp -> str "SProp" - | Sorts.InType | Sorts.InQSort -> str "Type" + match s with + | Sorts.Set -> str "Set" + | Sorts.Prop -> str "Prop" + | Sorts.SProp -> str "SProp" + | Sorts.Type _ | Sorts.QSort _ -> str "Type" let pr_con sp = str(Names.Label.to_string (Constant.label sp)) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 946abd625589..d39735b7decb 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -74,7 +74,7 @@ type record_arg_info = | HasRelevantArg type univ_info = - { ind_squashed : bool + { ind_squashed : squash_info option ; record_arg_info : record_arg_info ; ind_template : bool ; ind_univ : Sorts.t @@ -94,22 +94,21 @@ let check_univ_leq ?(is_real_arg=false) env u info = | Sorts.SProp | QSort _ -> info | Prop | Set | Type _ -> { info with record_arg_info = HasRelevantArg } in - (* If we would squash (eg Prop, SProp case) we still need to check the type in type flag. *) - let ind_squashed = not (Environ.type_in_type env) in - match u, info.ind_univ with + if (Environ.type_in_type env) then info + else match u, info.ind_univ with | SProp, (SProp | Prop | Set | QSort _ | Type _) -> (* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *) info - | Prop, SProp -> { info with ind_squashed } - | Prop, QSort _ -> { info with ind_squashed } (* imprecise *) + | Prop, SProp -> { info with ind_squashed = Some AlwaysSquashed } + | Prop, QSort _ -> { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) | Prop, (Prop | Set | Type _) -> info - | Set, (SProp | Prop) -> { info with ind_squashed } + | Set, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed } | Set, QSort (_, indu) -> if UGraph.check_leq (universes env) Universe.type0 indu - then { info with ind_squashed } (* imprecise *) + then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) else { info with missing = u :: info.missing } | Set, Set -> info | Set, Type indu -> @@ -117,34 +116,34 @@ let check_univ_leq ?(is_real_arg=false) env u info = then info else { info with missing = u :: info.missing } - | QSort _, (SProp | Prop) -> { info with ind_squashed } (* imprecise *) + | QSort _, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) | QSort (cq, uu), QSort (indq, indu) -> if UGraph.check_leq (universes env) uu indu then begin if Sorts.QVar.equal cq indq then info - else { info with ind_squashed } (* imprecise *) + else { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) end else { info with missing = u :: info.missing } | QSort (_, uu), Set -> if UGraph.check_leq (universes env) uu Universe.type0 then info else if is_impredicative_set env - then { info with ind_squashed } (* imprecise *) + then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) else { info with missing = u :: info.missing } | QSort (_,uu), Type indu -> if UGraph.check_leq (universes env) uu indu then info else { info with missing = u :: info.missing } - | Type _, (SProp | Prop) -> { info with ind_squashed } + | Type _, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed } | Type uu, Set -> if UGraph.check_leq (universes env) uu Universe.type0 then info else if is_impredicative_set env - then { info with ind_squashed } + then { info with ind_squashed = Some AlwaysSquashed } else { info with missing = u :: info.missing } | Type uu, QSort (_, indu) -> if UGraph.check_leq (universes env) uu indu - then { info with ind_squashed } (* imprecise *) + then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) else { info with missing = u :: info.missing } | Type uu, Type indu -> if UGraph.check_leq (universes env) uu indu @@ -173,7 +172,7 @@ let check_arity ~template env_params env_ar ind = let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in let indices, ind_sort = Reduction.dest_arity env_params arity in let univ_info = { - ind_squashed=false; + ind_squashed=None; record_arg_info=NoRelevantArg; ind_template = template; ind_univ=ind_sort; @@ -205,10 +204,12 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) = (* SProp primitive records are OK, if we squash and become fakerecord also OK *) if isrecord then univ_info (* 1 constructor with no arguments also OK in SProp (to make - things easier on ourselves when reducing we forbid letins) *) + things easier on ourselves when reducing we forbid letins) + unless ind_univ is sort polymorphic (for ease of implementation) *) else if (Environ.typing_flags env_ar_par).allow_uip && fst (splayed_lc.(0)) = [] && List.for_all Context.Rel.Declaration.is_local_assum params + && Sorts.is_sprop univ_info.ind_univ then univ_info (* 1 constructor with arguments must squash if SProp (we could allow arguments in SProp but the reduction rule is a pain) *) @@ -225,7 +226,7 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) = let check_record data = List.for_all (fun (_,(_,splayed_lc),info) -> (* records must have all projections definable -> equivalent to not being squashed *) - not info.ind_squashed + Option.is_empty info.ind_squashed (* relevant records must have at least 1 relevant argument, and we don't yet support variable relevance projections *) && (match info.record_arg_info with @@ -326,7 +327,14 @@ let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) = RegularArity {mind_user_arity = arity; mind_sort = ind_univ} in - (arity,lc), (indices,splayed_lc), univ_info.ind_squashed + let squashed = Option.map (function + | AlwaysSquashed -> AlwaysSquashed + | SometimesSquashed qs -> + SometimesSquashed (List.map (UVars.subst_sort_level_quality usubst) qs)) + univ_info.ind_squashed + in + + (arity,lc), (indices,splayed_lc), squashed let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 0603feca0f4d..9a05a9352fd6 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -35,5 +35,5 @@ val typecheck_inductive : env -> sec_univs:UVars.Instance.t option * Constr.rel_context * ((inductive_arity * Constr.types array) * (Constr.rel_context * (Constr.rel_context * Constr.types) array) * - bool (* squashed *)) + squash_info option) array diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6e569c1bd85a..2640c3bd6c7d 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -304,14 +304,65 @@ let abstract_constructor_type_relatively_to_inductive_types_context ntyps mind t (* Get type of inductive, with parameters instantiated *) +(* XXX questionable for sort poly inductives *) let inductive_sort_family mip = match mip.mind_arity with | RegularArity s -> Sorts.family s.mind_sort | TemplateArity _ -> Sorts.InType -let elim_sort (_,mip) = - if not mip.mind_squashed then Sorts.InType - else inductive_sort_family mip +let quality_leq q q' = + let open Sorts.Quality in + match q, q' with + | QVar q, QVar q' -> Sorts.QVar.equal q q' + | QConstant QSProp, _ + | _, QConstant QType + | QConstant QProp, QConstant QProp + -> true + + | (QVar _ | QConstant (QProp | QType)), _ -> false + +let is_squashed ((_,mip),u) = + match mip.mind_squashed with + | None -> None + | Some squash -> + let inds = match mip.mind_arity with + | TemplateArity _ -> assert false (* template is never squashed *) + | RegularArity a -> a.mind_sort + in + let inds = UVars.subst_instance_sort u inds in + match squash with + | AlwaysSquashed -> Some inds + | SometimesSquashed squash -> + match inds with + | Sorts.Set -> + (* impredicative set squashes are always AlwaysSquashed *) + assert false + | Sorts.Type _ -> None + | _ -> + let squash = List.map (UVars.subst_instance_quality u) squash in + if List.for_all (fun q -> quality_leq q (Sorts.quality inds)) squash then None + else Some inds + +let is_allowed_elimination specifu s = + match is_squashed specifu with + | None -> true + | Some inds -> + let open Sorts in + match s, inds with + (* impredicative set squash *) + | (SProp|Prop|Set), Set -> true + | (QSort _|Type _), Set -> false + + (* we never squash to Type *) + | _, Type _ -> assert false + + (* other squashes *) + | SProp, (SProp|Prop|QSort _) | Prop, Prop -> true + | QSort (q,_), QSort (indq,_) -> Sorts.QVar.equal q indq + | (Set|Type _), (SProp|Prop|QSort _) -> false + | Prop, SProp + | Prop, QSort _ + | QSort _, (Prop|SProp) -> false let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = diff --git a/kernel/inductive.mli b/kernel/inductive.mli index bd7bca786ef5..a8fb8ebf6bfb 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -64,7 +64,14 @@ val type_of_inductive : mind_specif puniverses -> types val type_of_inductive_knowing_parameters : ?polyprop:bool -> mind_specif puniverses -> param_univs -> types -val elim_sort : mind_specif -> Sorts.family +val quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool +(** For squashing. *) + +val is_squashed : mind_specif puniverses -> Sorts.t option +(** Returns the sort to which the inductive is squashed (i.e. the sort + of the inductive) if it is squashed. *) + +val is_allowed_elimination : mind_specif puniverses -> Sorts.t -> bool val is_private : mind_specif -> bool val is_primitive_record : mind_specif -> bool diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index de5133fbc4a3..35087e493858 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -114,6 +114,11 @@ let check_variance error v1 v2 = | None, Some _ -> error (CumulativeStatusExpected true) | Some _, None -> error (CumulativeStatusExpected false) +let squash_info_equal s1 s2 = match s1, s2 with + | AlwaysSquashed, AlwaysSquashed -> true + | SometimesSquashed s1, SometimesSquashed s2 -> List.equal Sorts.Quality.equal s1 s2 + | (AlwaysSquashed | SometimesSquashed _), _ -> false + (* for now we do not allow reorderings *) let check_inductive (cst, ustate) trace env mp1 l info1 mp2 mib2 subst1 subst2 reso1 reso2= @@ -139,7 +144,8 @@ let check_inductive (cst, ustate) trace env mp1 l info1 mp2 mib2 subst1 subst2 r let check f test why = if not (test (f p1) (f p2)) then error why in check (fun p -> p.mind_consnames) (Array.equal Id.equal) NotSameConstructorNamesField; check (fun p -> p.mind_typename) Id.equal NotSameInductiveNameInBlockField; - check (fun p -> p.mind_squashed) Bool.equal (NotConvertibleInductiveField p2.mind_typename); + check (fun p -> p.mind_squashed) (Option.equal squash_info_equal) + (NotConvertibleInductiveField p2.mind_typename); (* nf_lc later *) (* nf_arity later *) (* user_lc ignored *) diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 88542fb935ed..1290b4f738c0 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -56,7 +56,7 @@ type ('constr, 'types) ptype_error = | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * - (('constr, 'types) punsafe_judgment * Sorts.family * Sorts.family) option + (('constr, 'types) punsafe_judgment * Sorts.t) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | CaseOnPrivateInd of inductive | WrongCaseInfo of pinductive * case_info @@ -214,7 +214,7 @@ let map_ptype_error f = function | NotAType j -> NotAType (on_judgment f j) | BadAssumption j -> BadAssumption (on_judgment f j) | ElimArity (pi, c, ar) -> - ElimArity (pi, f c, Option.map (fun (j, s1, s2) -> (on_judgment f j, s1, s2)) ar) + ElimArity (pi, f c, Option.map (fun (j, s1) -> (on_judgment f j, s1)) ar) | CaseNotInductive j -> CaseNotInductive (on_judgment f j) | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci) | NumberBranches (j, n) -> NumberBranches (on_judgment f j, n) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index e28f5c328546..b4c99bebf66b 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -58,7 +58,7 @@ type ('constr, 'types) ptype_error = | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * - (('constr, 'types) punsafe_judgment * Sorts.family * Sorts.family) option + (('constr, 'types) punsafe_judgment * Sorts.t) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | CaseOnPrivateInd of inductive | WrongCaseInfo of pinductive * case_info @@ -120,7 +120,7 @@ val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a val error_elim_arity : env -> pinductive -> constr -> - (unsafe_judgment * Sorts.family * Sorts.family) option -> 'a + (unsafe_judgment * Sorts.t) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 30e218f11e03..642473faa4ac 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -550,13 +550,11 @@ let type_of_case env (mib, mip as specif) ci u pms (pctx, pnas, p, rp, pt) iv c if not (is_inversion = should_invert_case env rp ci) then error_bad_invert env in - let () = - let ksort = Sorts.family sp in - let s = elim_sort specif in - if not (Sorts.family_leq ksort s) then - let pj = make_judge (it_mkLambda_or_LetIn p pctx) (it_mkProd_or_LetIn pt pctx) in - let kinds = Some (pj, ksort, s) in - error_elim_arity env (ind, u') c kinds + let () = if not (is_allowed_elimination (specif,u) sp) then begin + let pj = make_judge (it_mkLambda_or_LetIn p pctx) (it_mkProd_or_LetIn pt pctx) in + let kinds = Some (pj, sp) in + error_elim_arity env (ind, u') c kinds + end in (* Check that the scrutinee has the right type *) let rslty = type_case_scrutinee env (mib, mip) (u', largs) u pms (pctx, p) c in diff --git a/kernel/uVars.ml b/kernel/uVars.ml index 5f03a1596d20..c52f3e0a68d7 100644 --- a/kernel/uVars.ml +++ b/kernel/uVars.ml @@ -237,7 +237,7 @@ let subst_instance_quality s l = | Some n -> (fst (Instance.to_array s)).(n) | None -> l end - | _ -> l + | Quality.QConstant _ -> l let subst_instance_instance s i = let qs, us = Instance.to_array i in @@ -412,18 +412,23 @@ let subst_sort_level_instance (qsubst,usubst) i = let subst_univs_level_abstract_universe_context subst (inst, csts) = inst, subst_univs_level_constraints subst csts -let subst_fn_of_qsubst qsubst qv = +let subst_sort_level_qvar (qsubst,_) qv = match Sorts.QVar.Map.find_opt qv qsubst with | None -> Quality.QVar qv | Some q -> q -let subst_sort_level_sort (qsubst,usubst) s = - let fq qv = subst_fn_of_qsubst qsubst qv in +let subst_sort_level_quality subst = function + | Sorts.Quality.QConstant _ as q -> q + | Sorts.Quality.QVar q -> + subst_sort_level_qvar subst q + +let subst_sort_level_sort (_,usubst as subst) s = + let fq qv = subst_sort_level_qvar subst qv in let fu u = subst_univs_level_universe usubst u in Sorts.subst_fn (fq,fu) s -let subst_sort_level_relevance (qsubst,_) r = - Sorts.relevance_subst_fn (subst_fn_of_qsubst qsubst) r +let subst_sort_level_relevance subst r = + Sorts.relevance_subst_fn (subst_sort_level_qvar subst) r let make_instance_subst i = let qarr, uarr = Instance.to_array i in diff --git a/kernel/uVars.mli b/kernel/uVars.mli index afb2e6d5475d..043a74edad18 100644 --- a/kernel/uVars.mli +++ b/kernel/uVars.mli @@ -206,6 +206,8 @@ val subst_univs_level_abstract_universe_context : val subst_sort_level_instance : sort_level_subst -> Instance.t -> Instance.t (** Level to universe substitutions. *) +val subst_sort_level_quality : sort_level_subst -> Sorts.Quality.t -> Sorts.Quality.t + val subst_sort_level_sort : sort_level_subst -> Sorts.t -> Sorts.t val subst_sort_level_relevance : sort_level_subst -> Sorts.relevance -> Sorts.relevance @@ -213,6 +215,7 @@ val subst_sort_level_relevance : sort_level_subst -> Sorts.relevance -> Sorts.re (** Substitution of instances *) val subst_instance_instance : Instance.t -> Instance.t -> Instance.t val subst_instance_universe : Instance.t -> Universe.t -> Universe.t +val subst_instance_quality : Instance.t -> Sorts.Quality.t -> Sorts.Quality.t val subst_instance_sort : Instance.t -> Sorts.t -> Sorts.t val subst_instance_relevance : Instance.t -> Sorts.relevance -> Sorts.relevance diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0f83314d922b..744fb558f477 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2093,7 +2093,7 @@ let expected_elimination_sort env tomatchl = match tm with | IsInd (_,IndType(indf,_),_) -> (* Not a degenerated line, see coerce_to_indtype *) - let s' = Inductive.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in + let s' = Inductiveops.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in if Sorts.family_leq s s' then s else s' | NotInd _ -> s) tomatchl Sorts.InType diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c3395038ab5b..7cd5eb730080 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -230,12 +230,70 @@ let inductive_has_local_defs env ind = let l2 = mib.mind_nparams + mip.mind_nrealargs in not (Int.equal l1 l2) +let is_squashed sigma ((_,mip),u) = + match mip.mind_squashed with + | None -> None + | Some squash -> + let inds = match mip.mind_arity with + | TemplateArity _ -> assert false (* template is never squashed *) + | RegularArity a -> a.mind_sort + in + let inds = UVars.subst_instance_sort u inds in + match squash with + | AlwaysSquashed -> Some (EConstr.ESorts.make inds) + | SometimesSquashed squash -> + match inds with + | Sorts.Set -> + (* impredicative set squashes are always AlwaysSquashed *) + assert false + | Sorts.Type _ -> None + | _ -> + let squash = List.map (UVars.subst_instance_quality u) squash in + let nfq q = UState.nf_quality (Evd.evar_universe_context sigma) q in + let indq = nfq (Sorts.quality inds) in + if List.for_all (fun q -> Inductive.quality_leq (nfq q) indq) squash then None + else Some (EConstr.ESorts.make inds) + +let is_allowed_elimination sigma specifu s = + match is_squashed sigma specifu with + | None -> true + | Some inds -> + match EConstr.ESorts.kind sigma s, EConstr.ESorts.kind sigma inds with + (* impredicative set squash *) + | (SProp|Prop|Set), Set -> true + | (QSort _|Type _), Set -> false + + (* we never squash to Type *) + | _, Type _ -> assert false + + (* other squashes *) + | SProp, (SProp|Prop|QSort _) | Prop, Prop -> true + | QSort (q,_), QSort (indq,_) -> Sorts.QVar.equal q indq + | (Set|Type _), (SProp|Prop|QSort _) -> false + | Prop, QSort _ (* XXX check above_prop in the ustate? *) + | Prop, SProp + | QSort _, (Prop|SProp) -> false + +let elim_sort (_,mip) = + if Option.is_empty mip.mind_squashed then Sorts.InType + else Inductive.inductive_sort_family mip + let top_allowed_sort env (kn,i as ind) = let specif = Inductive.lookup_mind_specif env ind in - Inductive.elim_sort specif + elim_sort specif let sorts_below top = - List.filter (fun s -> Sorts.family_leq s top) Sorts.[InSProp;InProp;InSet;InType] + List.filter (fun s -> + Sorts.family_equal s top + || match s, top with + | InSProp, _ -> true + | InProp, InSet -> true + | _, InType -> true + | (InProp|InSet|InType|InQSort), _ -> false) + Sorts.[InSProp;InProp;InSet;InType] + +let sorts_for_schemes specif = + sorts_below (elim_sort specif) let has_dependent_elim (mib,mip) = match mib.mind_record with diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 4668ee495554..cde51223981d 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -123,6 +123,12 @@ val inductive_has_local_defs : env -> inductive -> bool val sorts_below : Sorts.family -> Sorts.family list +val sorts_for_schemes : mind_specif -> Sorts.family list + +val is_allowed_elimination : evar_map -> (mind_specif * UVars.Instance.t) -> EConstr.ESorts.t -> bool + +val elim_sort : mind_specif -> Sorts.family + val top_allowed_sort : env -> inductive -> Sorts.family (** (Co)Inductive records with primitive projections do not have eta-conversion, diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index e984644492eb..9244fff1577a 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -119,6 +119,8 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys = (env, sigma, IllTypedRecBody (i, na, jl, tys)) let error_elim_arity ?loc env sigma pi c a = + (* XXX type_errors should have a 'sort type parameter *) + let a = Option.map (fun (x,s) -> x, EConstr.Unsafe.to_sorts s) a in raise_type_error ?loc (env, sigma, ElimArity (pi, c, a)) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 69a3bfef0b33..374d86bf092f 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -116,7 +116,7 @@ val error_ill_typed_rec_body : val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> pinductive -> constr -> - (unsafe_judgment * Sorts.family * Sorts.family) option -> 'b + (unsafe_judgment * ESorts.t) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 66dad388ad80..b75cd80efe3e 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -258,21 +258,16 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let specif = lookup_mind_specif env (fst ind) in - let sorts = elim_sort specif in let pj = Retyping.get_judgment_of env sigma p in let _, s = whd_decompose_prod env sigma pj.uj_type in let sort = match EConstr.kind sigma s with - | Sort s -> EConstr.ESorts.kind sigma s + | Sort s -> s | _ -> error_elim_arity env sigma ind c None in - let ksort = match Sorts.family sort with - | InType | InSProp | InSet | InProp as f -> f - | InQSort -> InType (* FIXME *) - in - if not (Sorts.family_leq ksort sorts) then - error_elim_arity env sigma ind c (Some (pj, ksort, sorts)) + if Inductiveops.is_allowed_elimination sigma (specif,(snd ind)) sort then + ESorts.relevance_of_sort sigma sort else - Sorts.relevance_of_sort sort + error_elim_arity env sigma ind c (Some (pj, sort)) let check_actual_type env sigma cj t = try Evarconv.unify_leq_delay env sigma cj.uj_type t diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1ce6e55c6328..051bf3e3d8ae 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1710,7 +1710,7 @@ let make_projection env sigma params cstr sign elim i n c (ind, u) = let (_, mip) as specif = Inductive.lookup_mind_specif env ind in let t = lift (i + 1 - n) t in let ksort = Retyping.get_sort_family_of (push_rel_context sign env) sigma t in - if Sorts.family_leq ksort (Inductive.elim_sort specif) then + if Sorts.family_leq ksort (Inductiveops.elim_sort specif) then let arity = List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt in let mknas ctx = Array.of_list (List.rev_map get_annot ctx) in let ci = Inductiveops.make_case_info env ind RegularStyle in diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index b0ed95748273..8198074fcd78 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -334,7 +334,7 @@ let type_of_constant cb = cb.Declarations.const_type let uses_uip mib = Array.exists (fun mip -> - not mip.mind_squashed + Option.is_empty mip.mind_squashed && mip.mind_relevance == Sorts.Irrelevant && Array.length mip.mind_nf_lc = 1 && List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 367f94db6ccf..a63ff4d6fab0 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -835,7 +835,7 @@ let build_beq_scheme env handle kn = | Finite when truly_recursive || nb_ind > 1 (* Hum... *) -> let cores = Array.init nb_ind make_one_eq in Array.init nb_ind (fun i -> - let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in + let kelim = Inductiveops.elim_sort (mib,mib.mind_packets.(i)) in if not (Sorts.family_leq InSet kelim) then raise (NonSingletonProp (kn,i)); let decrArg = Context.Rel.length nonrecparams_ctx_with_eqs in @@ -845,7 +845,7 @@ let build_beq_scheme env handle kn = assert (Int.equal nb_ind 1); (* If the inductive type is not recursive, the fixpoint is not used, so let's replace it with garbage *) - let kelim = Inductive.elim_sort (mib,mib.mind_packets.(0)) in + let kelim = Inductiveops.elim_sort (mib,mib.mind_packets.(0)) in if not (Sorts.family_leq InSet kelim) then raise (NonSingletonProp (kn,0)); [|Term.it_mkLambda_or_LetIn (make_one_eq 0) recparams_ctx_with_eqs|] in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index b09cb762fca5..9a56b03bd276 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -236,7 +236,9 @@ let explain_elim_arity env sigma ind c okinds = let pi = pr_inductive env (fst ind) in let pc = pr_leconstr_env env sigma c in let msg = match okinds with - | Some (pj, kp, ki) -> + | Some (pj, sp) -> + let kp = Sorts.family sp in + let ki = Inductiveops.elim_sort (Inductive.lookup_mind_specif env (fst ind)) in let explanation = error_elim_explain kp ki in let sorts = Inductiveops.sorts_below ki in let pki = Sorts.pr_sort_family ki in diff --git a/vernac/himsg.mli b/vernac/himsg.mli index f0aa50f22764..9d271b3dbf66 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -16,3 +16,12 @@ val explain_type_error : Environ.env -> Evd.evar_map -> Pretype_errors.type_erro val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t + +(* XXX add cases for SProp (and sort poly?) *) +type arity_error = + | NonInformativeToInformative + | StrongEliminationOnNonSmallType + | WrongArity + +val error_elim_explain : Sorts.family -> Sorts.family -> arity_error +(** Second argument is the familty of the inductive. *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index db5f87063009..fa7f8574b8fb 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -204,7 +204,7 @@ let declare_one_case_analysis_scheme ?loc ind = else if not (Inductiveops.has_dependent_elim specif) then case_scheme_kind_from_type else case_dep_scheme_kind_from_type in - let kelim = Inductive.elim_sort (mib,mip) in + let kelim = Inductiveops.elim_sort (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the appropriate type *) @@ -236,7 +236,7 @@ let declare_one_induction_scheme ?loc ind = let kind = Inductive.inductive_sort_family mip in let from_prop = kind == InProp in let depelim = Inductiveops.has_dependent_elim specif in - let kelim = Inductiveops.sorts_below (Inductive.elim_sort (mib,mip)) in + let kelim = Inductiveops.sorts_below (Inductiveops.elim_sort (mib,mip)) in let kelim = if Global.sprop_allowed () then kelim else List.filter (fun s -> s <> InSProp) kelim in diff --git a/vernac/record.ml b/vernac/record.ml index cd06859fec06..2c5bf718f249 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -294,18 +294,24 @@ let warning_or_error ~info flags indsp err = prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++ strbrk " not defined.") | BadTypedProj (fi,_ctx,te) -> - match te with - | ElimArity (_, _, Some (_, (InType | InSet), InProp)) -> + let err = match te with + | ElimArity (_, _, Some (_, s)) -> + Himsg.error_elim_explain (Sorts.family s) + (Inductiveops.elim_sort (Global.lookup_inductive indsp)) + | _ -> WrongArity + in + match err with + | NonInformativeToInformative -> (Id.print fi ++ strbrk" cannot be defined because it is informative and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") - | ElimArity (_, _, Some (_, InType, InSet)) -> + | StrongEliminationOnNonSmallType -> (Id.print fi ++ strbrk" cannot be defined because it is large and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") - | _ -> + | WrongArity -> (Id.print fi ++ strbrk " cannot be defined because it is not typable.") in if flags.Data.pf_coercion || flags.Data.pf_instance then user_err ~info st; From 76e189595d46c97c814b210a6ac97a4152bcefbb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 17 Nov 2023 17:18:03 +0100 Subject: [PATCH 06/10] Produce precise squashing --- kernel/indTyping.ml | 29 +++++++++++++++++------------ test-suite/success/sort_poly.v | 8 +++++++- 2 files changed, 24 insertions(+), 13 deletions(-) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index d39735b7decb..811db22a99c5 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -81,13 +81,17 @@ type univ_info = ; missing : Sorts.t list (* missing u <= ind_univ constraints *) } -(* TODO squash depending on the instance - (so eg in the "QSort(q, _), Prop" case, "@{q:=Prop|}" is not squashed - but "@{q:=Type|}" does need squashing) - Cases which will be modified are annotated with "imprecise". - - This code can probably be simplified but I can't quite see how right now. *) +let add_squash q info = + match info.ind_squashed with + | None -> { info with ind_squashed = Some (SometimesSquashed [q]) } + | Some AlwaysSquashed -> info + | Some (SometimesSquashed qs) -> + (* XXX dedup insertion *) + { info with ind_squashed = Some (SometimesSquashed (q::qs)) } + +(* This code can probably be simplified but I can't quite see how right now. *) let check_univ_leq ?(is_real_arg=false) env u info = + let open Sorts.Quality in let info = if not is_real_arg then info else match info.record_arg_info with | NoRelevantArg | HasRelevantArg -> match u with @@ -102,13 +106,13 @@ let check_univ_leq ?(is_real_arg=false) env u info = info | Prop, SProp -> { info with ind_squashed = Some AlwaysSquashed } - | Prop, QSort _ -> { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) + | Prop, QSort _ -> add_squash qprop info | Prop, (Prop | Set | Type _) -> info | Set, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed } | Set, QSort (_, indu) -> if UGraph.check_leq (universes env) Universe.type0 indu - then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) + then add_squash qtype info else { info with missing = u :: info.missing } | Set, Set -> info | Set, Type indu -> @@ -116,18 +120,19 @@ let check_univ_leq ?(is_real_arg=false) env u info = then info else { info with missing = u :: info.missing } - | QSort _, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) + | QSort (q,_), (SProp | Prop) -> add_squash (QVar q) info | QSort (cq, uu), QSort (indq, indu) -> if UGraph.check_leq (universes env) uu indu then begin if Sorts.QVar.equal cq indq then info - else { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) + else add_squash (QVar cq) info end else { info with missing = u :: info.missing } | QSort (_, uu), Set -> if UGraph.check_leq (universes env) uu Universe.type0 then info else if is_impredicative_set env - then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) + then (* imprecise but we don't handle complex impredicative set squashings *) + { info with ind_squashed = Some AlwaysSquashed } else { info with missing = u :: info.missing } | QSort (_,uu), Type indu -> if UGraph.check_leq (universes env) uu indu @@ -143,7 +148,7 @@ let check_univ_leq ?(is_real_arg=false) env u info = else { info with missing = u :: info.missing } | Type uu, QSort (_, indu) -> if UGraph.check_leq (universes env) uu indu - then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *) + then add_squash qtype info else { info with missing = u :: info.missing } | Type uu, Type indu -> if UGraph.check_leq (universes env) uu indu diff --git a/test-suite/success/sort_poly.v b/test-suite/success/sort_poly.v index a06926fa7258..9879c608149e 100644 --- a/test-suite/success/sort_poly.v +++ b/test-suite/success/sort_poly.v @@ -113,13 +113,19 @@ Module Inductives. Definition foo5_ind'@{s| |} : forall (A : Type@{s|Set}) (P : Prop), (A -> P) -> foo5 A -> P := foo5_ind. - (* TODO more precise squashing *) + (* TODO unify sort variable instead of failing *) Fail Definition foo5_Prop_rect (A:Prop) (P:foo5 A -> Type) (H : forall a, P (Foo5 A a)) (f : foo5 A) : P f := match f with Foo5 _ a => H a end. + Definition foo5_Prop_rect (A:Prop) (P:foo5 A -> Type) + (H : forall a, P (Foo5 A a)) + (f : foo5@{Prop|} A) + : P f + := match f with Foo5 _ a => H a end. + Set Primitive Projections. Set Warnings "+records". From 96c66202d0881aa304151af4db0d2f63e4e9155b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 17 Nov 2023 17:28:07 +0100 Subject: [PATCH 07/10] Fully sort polymorphic inductives --- kernel/declarations.mli | 9 +- kernel/indTyping.ml | 33 +++--- kernel/inductive.ml | 82 +++++++-------- kernel/inductive.mli | 4 - pretyping/cases.ml | 45 +++++---- pretyping/inductiveops.ml | 101 +++++++++++-------- pretyping/inductiveops.mli | 4 + test-suite/success/sort_poly.v | 117 +++++++++++++++++++++- test-suite/success/sort_poly_extraction.v | 13 ++- vernac/comInductive.ml | 3 +- vernac/himsg.ml | 5 +- 11 files changed, 276 insertions(+), 140 deletions(-) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 72d0ee47a500..2f22d8d11c72 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -168,10 +168,10 @@ type squash_info = | AlwaysSquashed | SometimesSquashed of Sorts.Quality.t list (** A sort polymorphic inductive [I@{...|...|...} : ... -> Type@{ s|...}] - is squashed at a given instantiation if the qualities in the list are not smaller than [s]. + is squashed at a given instantiation if any quality in the list is not smaller than [s]. - NB: if [s] is sort poly and the inductive has >0 constructors - SometimesSquashed contains Prop ie the SProp instantiation is squashed. *) + NB: if [s] is a variable SometimesSquashed contains SProp + ie non ground instantiations are squashed. *) (** {7 Datas specific to a single type of a block of mutually inductive type } *) type one_inductive_body = { @@ -207,7 +207,8 @@ type one_inductive_body = { mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) - mind_squashed : squash_info option; (** Is elimination restricted to the inductive's sort? *) + mind_squashed : squash_info option; + (** Is elimination restricted to the inductive's sort? *) mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 811db22a99c5..29b022dd0920 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -66,12 +66,11 @@ let mind_check_names mie = (************************************************************************) -let no_sort_variable () = - CErrors.user_err (Pp.str "Sort variables not yet supported for the inductive's sort.") - type record_arg_info = | NoRelevantArg | HasRelevantArg + (** HasRelevantArg means when the record is relevant at least one arg is relevant. + When the record is in a polymorphic sort this can mean one arg is in the same sort. *) type univ_info = { ind_squashed : squash_info option @@ -94,19 +93,23 @@ let check_univ_leq ?(is_real_arg=false) env u info = let open Sorts.Quality in let info = if not is_real_arg then info else match info.record_arg_info with - | NoRelevantArg | HasRelevantArg -> match u with - | Sorts.SProp | QSort _ -> info - | Prop | Set | Type _ -> { info with record_arg_info = HasRelevantArg } + | HasRelevantArg -> info + | NoRelevantArg -> match u with + | Sorts.SProp -> info + | QSort (q,_) -> if Sorts.Quality.equal (QVar q) (Sorts.quality info.ind_univ) + then { info with record_arg_info = HasRelevantArg } + else info + | Prop | Set | Type _ -> { info with record_arg_info = HasRelevantArg } in if (Environ.type_in_type env) then info else match u, info.ind_univ with - | SProp, (SProp | Prop | Set | QSort _ | Type _) -> + | SProp, (SProp | Prop | Set | Type _) -> (* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *) info | Prop, SProp -> { info with ind_squashed = Some AlwaysSquashed } - | Prop, QSort _ -> add_squash qprop info + | (SProp|Prop), QSort _ -> add_squash (Sorts.quality u) info | Prop, (Prop | Set | Type _) -> info | Set, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed } @@ -202,11 +205,11 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) = let lc = Array.map_of_list (fun c -> (Typeops.infer_type env_ar_par c).utj_val) lc in let splayed_lc = Array.map (Reduction.whd_decompose_prod_decls env_ar_par) lc in let univ_info = match Array.length lc with - (* Empty type: all OK *) - | 0 -> univ_info + (* Empty type: sort poly must squash *) + | 0 -> check_univ_leq env_ar_par Sorts.sprop univ_info | 1 -> - (* SProp primitive records are OK, if we squash and become fakerecord also OK *) + (* SProp and sort poly primitive records are OK, if we squash and become fakerecord also OK *) if isrecord then univ_info (* 1 constructor with no arguments also OK in SProp (to make things easier on ourselves when reducing we forbid letins) @@ -216,7 +219,7 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) = && List.for_all Context.Rel.Declaration.is_local_assum params && Sorts.is_sprop univ_info.ind_univ then univ_info - (* 1 constructor with arguments must squash if SProp + (* 1 constructor with arguments must squash if SProp / sort poly (we could allow arguments in SProp but the reduction rule is a pain) *) else check_univ_leq env_ar_par Sorts.prop univ_info @@ -319,11 +322,7 @@ let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) = args,out) splayed_lc in - let ind_univ = match univ_info.ind_univ with - | QSort _ -> no_sort_variable () - | _ -> - UVars.subst_sort_level_sort usubst univ_info.ind_univ - in + let ind_univ = UVars.subst_sort_level_sort usubst univ_info.ind_univ in let arity = if univ_info.ind_template then diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2640c3bd6c7d..a9ab4bf5e23b 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -314,55 +314,50 @@ let quality_leq q q' = let open Sorts.Quality in match q, q' with | QVar q, QVar q' -> Sorts.QVar.equal q q' - | QConstant QSProp, _ - | _, QConstant QType - | QConstant QProp, QConstant QProp - -> true + | QConstant q, QConstant q' -> + begin match q, q' with + | QSProp, _ + | _, QType + | QProp, QProp + -> true + | (QProp|QType), _ -> false + end + | (QVar _|QConstant _), _ -> false - | (QVar _ | QConstant (QProp | QType)), _ -> false +type squash = SquashToSet | SquashToQuality of Sorts.Quality.t let is_squashed ((_,mip),u) = - match mip.mind_squashed with - | None -> None - | Some squash -> - let inds = match mip.mind_arity with - | TemplateArity _ -> assert false (* template is never squashed *) - | RegularArity a -> a.mind_sort - in - let inds = UVars.subst_instance_sort u inds in - match squash with - | AlwaysSquashed -> Some inds - | SometimesSquashed squash -> - match inds with - | Sorts.Set -> - (* impredicative set squashes are always AlwaysSquashed *) - assert false - | Sorts.Type _ -> None - | _ -> + match mip.mind_arity with + | TemplateArity _ -> None (* template is never squashed *) + | RegularArity a -> + match mip.mind_squashed with + | None -> None + | Some squash -> + let indq = Sorts.quality (UVars.subst_instance_sort u a.mind_sort) in + match squash with + | AlwaysSquashed -> begin match a.mind_sort with + | Sorts.Set -> Some SquashToSet + | _ -> Some (SquashToQuality indq) + end + | SometimesSquashed squash -> + (* impredicative set squashes are always AlwaysSquashed, + so here if inds=Set it is a sort poly squash (see "foo6" in test sort_poly.v) *) let squash = List.map (UVars.subst_instance_quality u) squash in - if List.for_all (fun q -> quality_leq q (Sorts.quality inds)) squash then None - else Some inds + if List.for_all (fun q -> quality_leq q indq) squash then None + else Some (SquashToQuality indq) let is_allowed_elimination specifu s = + let open Sorts in match is_squashed specifu with | None -> true - | Some inds -> - let open Sorts in - match s, inds with - (* impredicative set squash *) - | (SProp|Prop|Set), Set -> true - | (QSort _|Type _), Set -> false - - (* we never squash to Type *) - | _, Type _ -> assert false - - (* other squashes *) - | SProp, (SProp|Prop|QSort _) | Prop, Prop -> true - | QSort (q,_), QSort (indq,_) -> Sorts.QVar.equal q indq - | (Set|Type _), (SProp|Prop|QSort _) -> false - | Prop, SProp - | Prop, QSort _ - | QSort _, (Prop|SProp) -> false + | Some SquashToSet -> + begin match s with + | SProp|Prop|Set -> true + | QSort _ | Type _ -> + (* XXX in [Type u] case, should we check [u == set] in the ugraph? *) + false + end + | Some (SquashToQuality indq) -> quality_leq (Sorts.quality s) indq let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = @@ -1489,9 +1484,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let () = if Environ.is_type_in_type env (GlobRef.IndRef ind) then () else match relevance_of_ind_body mip u with - | Sorts.Irrelevant | Sorts.RelevanceVar _ -> - (* XXX if RelevanceVar also allow binder_relevance = the same var? *) - if not (names.(i).Context.binder_relevance == Sorts.Irrelevant) + | Sorts.Irrelevant | Sorts.RelevanceVar _ as rind -> + if not (Sorts.relevance_equal names.(i).Context.binder_relevance rind) then raise_err env i FixpointOnIrrelevantInductive | Sorts.Relevant -> () in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a8fb8ebf6bfb..a8a830b448ee 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -67,10 +67,6 @@ val type_of_inductive_knowing_parameters : val quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool (** For squashing. *) -val is_squashed : mind_specif puniverses -> Sorts.t option -(** Returns the sort to which the inductive is squashed (i.e. the sort - of the inductive) if it is squashed. *) - val is_allowed_elimination : mind_specif puniverses -> Sorts.t -> bool val is_private : mind_specif -> bool diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 744fb558f477..ad51c0d205f3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2088,14 +2088,13 @@ let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs ars Some (sigma', p, arsign) with e when precatchable_exception e -> None -let expected_elimination_sort env tomatchl = - List.fold_right (fun (_,tm) s -> - match tm with +let expected_elimination_sorts env sigma tomatchl = + List.map_filter (fun (_,tm) -> match tm with + | NotInd _ -> None | IsInd (_,IndType(indf,_),_) -> - (* Not a degenerated line, see coerce_to_indtype *) - let s' = Inductiveops.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in - if Sorts.family_leq s s' then s else s' - | NotInd _ -> s) tomatchl Sorts.InType + let (ind, u), _ = dest_ind_family indf in + Inductiveops.is_squashed sigma (Inductive.lookup_mind_specif env ind, u)) + tomatchl (* Builds the predicate. If the predicate is dependent, its context is * made of 1+nrealargs assumptions for each matched term in an inductive @@ -2155,32 +2154,36 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty underspecified, i.e. a QSort, we make a non-canonical choice for the return type. Incompatible constraints are ignored and handled later when typing the pattern-matching. *) - let sigma = match expected_elimination_sort !!env tomatchs with - | InType -> - (* Not squashed, no constraints *) - sigma - | InProp -> + let check_elim_sort sigma = function + | SquashToSet -> + (* Squashed inductive in Set, only happens with impredicative Set *) + begin match ESorts.kind sigma rtnsort with + | Sorts.QSort _ -> + Evd.set_eq_sort !!env sigma rtnsort ESorts.set + | Sorts.Type _ | Sorts.Set | Sorts.SProp | Sorts.Prop -> sigma + end + | SquashToQuality (QConstant QProp) -> (* Squashed inductive in Prop, return sort must be Prop or SProp *) begin match ESorts.kind sigma rtnsort with | Sorts.QSort _ -> Evd.set_eq_sort !!env sigma rtnsort ESorts.prop | Sorts.Type _ | Sorts.Set | Sorts.SProp | Sorts.Prop -> sigma end - | InSProp -> + | SquashToQuality (QConstant QSProp) -> (* Squashed inductive in SProp, return sort must be SProp. *) begin match ESorts.kind sigma rtnsort with | Sorts.QSort _ -> Evd.set_eq_sort !!env sigma rtnsort ESorts.sprop | Sorts.Type _ | Sorts.Set | Sorts.Prop | Sorts.SProp -> sigma end - | InSet -> - (* Squashed inductive in Set, only happens with impredicative Set *) - begin match ESorts.kind sigma rtnsort with - | Sorts.QSort _ -> - Evd.set_eq_sort !!env sigma rtnsort ESorts.set - | Sorts.Type _ | Sorts.Set | Sorts.SProp | Sorts.Prop -> sigma - end - | InQSort -> assert false + | SquashToQuality (QConstant QType) -> + (* Sort poly squash to type *) + Evd.set_leq_sort !!env sigma ESorts.set rtnsort + | SquashToQuality (QVar q) -> + Evd.set_leq_sort !!env sigma (ESorts.make (Sorts.qsort q Univ.Universe.type0)) rtnsort + in + let sigma = List.fold_left check_elim_sort sigma + (expected_elimination_sorts !!env sigma tomatchs) in let predccl = nf_evar sigma predcclj.uj_val in [sigma, predccl, building_arsign] diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 7cd5eb730080..f4774f112c87 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -230,49 +230,62 @@ let inductive_has_local_defs env ind = let l2 = mib.mind_nparams + mip.mind_nrealargs in not (Int.equal l1 l2) +(* XXX use above_prop from the ustate *) +let quality_leq q q' = + let open Sorts.Quality in + match q, q' with + | QVar q, QVar q' -> Sorts.QVar.equal q q' + | QConstant q, QConstant q' -> + begin match q, q' with + | QSProp, _ + | _, QType + | QProp, QProp + -> true + | (QProp|QType), _ -> false + end + | (QVar _|QConstant _), _ -> false + +type squash = SquashToSet | SquashToQuality of Sorts.Quality.t + let is_squashed sigma ((_,mip),u) = - match mip.mind_squashed with - | None -> None - | Some squash -> - let inds = match mip.mind_arity with - | TemplateArity _ -> assert false (* template is never squashed *) - | RegularArity a -> a.mind_sort - in - let inds = UVars.subst_instance_sort u inds in - match squash with - | AlwaysSquashed -> Some (EConstr.ESorts.make inds) - | SometimesSquashed squash -> - match inds with - | Sorts.Set -> - (* impredicative set squashes are always AlwaysSquashed *) - assert false - | Sorts.Type _ -> None - | _ -> - let squash = List.map (UVars.subst_instance_quality u) squash in - let nfq q = UState.nf_quality (Evd.evar_universe_context sigma) q in - let indq = nfq (Sorts.quality inds) in - if List.for_all (fun q -> Inductive.quality_leq (nfq q) indq) squash then None - else Some (EConstr.ESorts.make inds) - -let is_allowed_elimination sigma specifu s = - match is_squashed sigma specifu with - | None -> true - | Some inds -> - match EConstr.ESorts.kind sigma s, EConstr.ESorts.kind sigma inds with - (* impredicative set squash *) - | (SProp|Prop|Set), Set -> true - | (QSort _|Type _), Set -> false - - (* we never squash to Type *) - | _, Type _ -> assert false - - (* other squashes *) - | SProp, (SProp|Prop|QSort _) | Prop, Prop -> true - | QSort (q,_), QSort (indq,_) -> Sorts.QVar.equal q indq - | (Set|Type _), (SProp|Prop|QSort _) -> false - | Prop, QSort _ (* XXX check above_prop in the ustate? *) - | Prop, SProp - | QSort _, (Prop|SProp) -> false + match mip.mind_arity with + | TemplateArity _ -> None (* template is never squashed *) + | RegularArity a -> + match mip.mind_squashed with + | None -> None + | Some squash -> + let indq = EConstr.ESorts.quality sigma + (EConstr.ESorts.make @@ UVars.subst_instance_sort u a.mind_sort) + in + match squash with + | AlwaysSquashed -> begin match a.mind_sort with + | Sorts.Set -> Some SquashToSet + | _ -> Some (SquashToQuality indq) + end + | SometimesSquashed squash -> + (* impredicative set squashes are always AlwaysSquashed, + so here if inds=Set it is a sort poly squash (see "foo6" in test sort_poly.v) *) + if List.for_all (fun q -> + let q = UVars.subst_instance_quality u q in + let q = UState.nf_quality (Evd.evar_universe_context sigma) q in + quality_leq q indq) squash then None + else Some (SquashToQuality indq) + +let is_allowed_elimination sigma ((mib,_),_ as specifu) s = + let open Sorts in + match mib.mind_record with + | PrimRecord _ -> true + | NotRecord | FakeRecord -> + match is_squashed sigma specifu with + | None -> true + | Some SquashToSet -> + begin match EConstr.ESorts.kind sigma s with + | SProp|Prop|Set -> true + | QSort _ | Type _ -> + (* XXX in [Type u] case, should we check [u == set] in the ugraph? *) + false + end + | Some (SquashToQuality indq) -> quality_leq (EConstr.ESorts.quality sigma s) indq let elim_sort (_,mip) = if Option.is_empty mip.mind_squashed then Sorts.InType @@ -286,10 +299,12 @@ let sorts_below top = List.filter (fun s -> Sorts.family_equal s top || match s, top with + | InQSort, _ -> assert false + | _, InQSort -> false | InSProp, _ -> true | InProp, InSet -> true | _, InType -> true - | (InProp|InSet|InType|InQSort), _ -> false) + | (InProp|InSet|InType), _ -> false) Sorts.[InSProp;InProp;InSet;InType] let sorts_for_schemes specif = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cde51223981d..a3c59709d5cf 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -125,6 +125,10 @@ val sorts_below : Sorts.family -> Sorts.family list val sorts_for_schemes : mind_specif -> Sorts.family list +type squash = SquashToSet | SquashToQuality of Sorts.Quality.t + +val is_squashed : evar_map -> (mind_specif * UVars.Instance.t) -> squash option + val is_allowed_elimination : evar_map -> (mind_specif * UVars.Instance.t) -> EConstr.ESorts.t -> bool val elim_sort : mind_specif -> Sorts.family diff --git a/test-suite/success/sort_poly.v b/test-suite/success/sort_poly.v index 9879c608149e..ceb90105c4bc 100644 --- a/test-suite/success/sort_poly.v +++ b/test-suite/success/sort_poly.v @@ -100,12 +100,17 @@ Module Inference. End Inference. Module Inductives. - (* TODO sort variable in the output sort *) - Fail Inductive foo1@{s| |} : Type@{s|Set} := . + Inductive foo1@{s| |} : Type@{s|Set} := . + Fail Check foo1_sind. + + Fail Definition foo1_False@{s|+|+} (x:foo1@{s|}) : False := match x return False with end. + (* XXX error message is bad *) Inductive foo2@{s| |} := Foo2 : Type@{s|Set} -> foo2. + Check foo2_rect. Inductive foo3@{s| |} (A:Type@{s|Set}) := Foo3 : A -> foo3 A. + Check foo3_rect. Fail Inductive foo4@{s|u v|v < u} : Type@{v} := C (_:Type@{s|u}). @@ -126,6 +131,57 @@ Module Inductives. : P f := match f with Foo5 _ a => H a end. + (* all sort poly output with nonzero contructors are squashed (avoid interfering with uip) *) + Inductive foo6@{s| |} : Type@{s|Set} := Foo6. + Fail Check foo6_sind. + + Fail Definition foo6_rect (P:foo6 -> Type) + (H : P Foo6) + (f : foo6) + : P f + := match f with Foo6 => H end. + (* XXX error message is pretty bad *) + + Definition foo6_prop_rect (P:foo6 -> Type) + (H : P Foo6) + (f : foo6@{Prop|}) + : P f + := match f with Foo6 => H end. + + Definition foo6_type_rect (P:foo6 -> Type) + (H : P Foo6) + (f : foo6@{Type|}) + : P f + := match f with Foo6 => H end. + + Definition foo6_qsort_rect@{s|u|} (P:foo6 -> Type@{s|u}) + (H : P Foo6) + (f : foo6@{s|}) + : P f + := match f with Foo6 => H end. + + Fail Definition foo6_2qsort_rect@{s s'|u|} (P:foo6 -> Type@{s|u}) + (H : P Foo6) + (f : foo6@{s'|}) + : P f + := match f with Foo6 => H end. + + Inductive foo7@{s| |} : Type@{s|Set} := Foo7_1 | Foo7_2. + Fail Check foo7_sind. + Fail Check foo7_ind. + + Definition foo7_prop_ind (P:foo7 -> Prop) + (H : P Foo7_1) (H' : P Foo7_2) + (f : foo7@{Prop|}) + : P f + := match f with Foo7_1 => H | Foo7_2 => H' end. + + Fail Definition foo7_prop_rect (P:foo7 -> Type) + (H : P Foo7_1) (H' : P Foo7_2) + (f : foo7@{Prop|}) + : P f + := match f with Foo7_1 => H | Foo7_2 => H' end. + Set Primitive Projections. Set Warnings "+records". @@ -138,8 +194,7 @@ Module Inductives. (* R3@{SProp Type|} may not be primitive *) Fail Record R3@{s s'| |} (A:Type@{s|Set}) : Type@{s'|Set} := { R3f1 : A }. - (* TODO sort variable in output sort *) - Fail Record R4@{s| |} (A:Type@{s|Set}) : Type@{s|Set} := { R4f1 : A}. + Record R4@{s| |} (A:Type@{s|Set}) : Type@{s|Set} := { R4f1 : A}. (* non SProp instantiation must be squashed *) Fail Record R5@{s| |} (A:Type@{s|Set}) : SProp := { R5f1 : A}. @@ -163,4 +218,58 @@ Module Inductives. Check R7@{SProp|} : SProp -> Set. Check R7@{Type|} : Set -> Set. + Inductive sigma@{s|u v|} (A:Type@{s|u}) (B:A -> Type@{s|v}) : Type@{s|max(u,v)} + := pair : forall x : A, B x -> sigma A B. + + Definition sigma_srect@{s|k +|} A B + (P : sigma@{s|_ _} A B -> Type@{s|k}) + (H : forall x b, P (pair _ _ x b)) + (s:sigma A B) + : P s + := match s with pair _ _ x b => H x b end. + + (* squashed because positive type with >0 constructors *) + Fail Definition sigma_srect'@{s sk|k +|} A B + (P : sigma@{s|_ _} A B -> Type@{sk|k}) + (H : forall x b, P (pair _ _ x b)) + (s:sigma A B) + : P s + := match s with pair _ _ x b => H x b end. + + (* even though it's squashed, we can still define the projections *) + Definition pr1@{s|+|} {A B} (s:sigma@{s|_ _} A B) : A + := match s with pair _ _ x _ => x end. + + Definition pr2@{s|+|} {A B} (s:sigma@{s|_ _} A B) : B (pr1 s) + := match s with pair _ _ _ y => y end. + + (* but we can't prove eta *) + Inductive seq@{s|u|} (A:Type@{s|u}) (a:A) : A -> Prop := seq_refl : seq A a a. + Arguments seq_refl {_ _}. + + Definition eta@{s|+|+} A B (s:sigma@{s|_ _} A B) : seq _ s (pair A B (pr1 s) (pr2 s)). + Proof. + Fail destruct s. + Abort. + + (* sigma as a primitive record works better *) + Record Rsigma@{s|u v|} (A:Type@{s|u}) (B:A -> Type@{s|v}) : Type@{s|max(u,v)} + := Rpair { Rpr1 : A; Rpr2 : B Rpr1 }. + + (* match desugared to primitive projections using definitional eta *) + Definition Rsigma_srect@{s sk|k +|} A B + (P : Rsigma@{s|_ _} A B -> Type@{sk|k}) + (H : forall x b, P (Rpair _ _ x b)) + (s:Rsigma A B) + : P s + := match s with Rpair _ _ x b => H x b end. + + (* sort polymorphic exists (we could also make B sort poly) + can't be a primitive record since the first projection isn't defined at all sorts *) + Inductive sexists@{s|u|} (A:Type@{s|u}) (B:A -> Prop) : Prop + := sexist : forall a:A, B a -> sexists A B. + + (* we can eliminate to Prop *) + Check sexists_ind. + End Inductives. diff --git a/test-suite/success/sort_poly_extraction.v b/test-suite/success/sort_poly_extraction.v index 09c111ded087..8d3b2b40cdea 100644 --- a/test-suite/success/sort_poly_extraction.v +++ b/test-suite/success/sort_poly_extraction.v @@ -7,4 +7,15 @@ Definition bar := foo@{Prop|}. Fail Extraction bar. -(* the actual problem only appears once we have inductives with sort poly output *) +(* the actual problem only appears once we have inductives with sort poly output: *) + +Inductive Pair@{s|u|} (A:Type@{s|u}) : Type@{s|u} := pair : A -> A -> Pair A. + +Definition use_pair@{s|+|} A (k:A->nat) (x:Pair@{s|_} A) := + k (match x with pair _ x _ => x end). + +Definition make_pair := pair@{Prop|_} _ I I. + +Definition hell := use_pair True (fun _ => 0) make_pair. + +Fail Recursive Extraction hell. diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index eda9c9e4d33c..61c8308b40c9 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -233,7 +233,8 @@ let inductive_levels env evd arities ctors = let less_than_2 = function [] | [_] -> true | _ :: _ :: _ -> false in let evd = List.fold_left (fun evd (raw_arity,(_,s),ctors) -> if less_than_2 ctors || is_impredicative_sort evd s then evd - else Evd.set_leq_sort env evd ESorts.set s) + else (* >=2 constructors is like having a bool argument *) + include_constructor_argument env evd ~ctor_sort:ESorts.set ~inductive_sort:s) evd inds in (* If indices_matter, the index telescope acts like an extra diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 9a56b03bd276..207d1764641f 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -250,7 +250,10 @@ let explain_elim_arity env sigma ind c okinds = "strong elimination on non-small inductive types leads to paradoxes" | WrongArity -> "wrong arity" in - let ppar = pr_disjunction (fun s -> quote (Sorts.pr_sort_family s)) sorts in + let ppar = match sorts with + | [] -> str "at some variable quality" + | _ -> pr_disjunction (fun s -> quote (Sorts.pr_sort_family s)) sorts + in let ppt = pr_leconstr_env env sigma (snd (decompose_prod_decls sigma pj.uj_type)) in hov 0 (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++ From f256442e39a535771eaa4a423c7c855efeeae50e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 20 Nov 2023 15:37:26 +0100 Subject: [PATCH 08/10] Overlays for sort poly inductives --- dev/ci/user-overlays/18331-SkySkimmer-sort-poly-ind.sh | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 dev/ci/user-overlays/18331-SkySkimmer-sort-poly-ind.sh diff --git a/dev/ci/user-overlays/18331-SkySkimmer-sort-poly-ind.sh b/dev/ci/user-overlays/18331-SkySkimmer-sort-poly-ind.sh new file mode 100644 index 000000000000..4cc0776e3f6a --- /dev/null +++ b/dev/ci/user-overlays/18331-SkySkimmer-sort-poly-ind.sh @@ -0,0 +1,7 @@ +overlay elpi https://github.com/SkySkimmer/coq-elpi sort-poly-ind 18331 + +overlay lean_importer https://github.com/SkySkimmer/coq-lean-import sort-poly-ind 18331 + +overlay metacoq https://github.com/SkySkimmer/metacoq sort-poly-ind 18331 + +overlay serapi https://github.com/SkySkimmer/coq-serapi sort-poly-ind 18331 From 0d4a00c8354c884baea177b32050e58ee9ea18d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 20 Nov 2023 15:55:01 +0100 Subject: [PATCH 09/10] Doc for sort poly inductives --- doc/changelog/01-kernel/17836-sort-poly.rst | 1 + doc/sphinx/addendum/universe-polymorphism.rst | 52 +++++++++++++++++++ 2 files changed, 53 insertions(+) diff --git a/doc/changelog/01-kernel/17836-sort-poly.rst b/doc/changelog/01-kernel/17836-sort-poly.rst index d34ac26360ef..94ad484cd937 100644 --- a/doc/changelog/01-kernel/17836-sort-poly.rst +++ b/doc/changelog/01-kernel/17836-sort-poly.rst @@ -2,4 +2,5 @@ :ref:`sort-polymorphism` makes it possible to share common constructs over `Type` `Prop` and `SProp` (`#17836 `_, + `#18331 `_, by Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 8d791d02a918..c432895bcd24 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -803,6 +803,58 @@ witness these temporary variables. `α` followed by a number as printing will not distinguish between your bound variables and temporary variables. +Sort polymorphic inductives may be declared when every instantiation +is valid. + +Elimination at a given universe instance requires that elimination is +allowed at every ground instantiation of the sort variables in the +instance. Additionally if the output sort at the given universe +instance is sort polymorphic, the return type of the elimination must +be at the same quality. These restrictions ignore :flag:`Definitional +UIP`. + +For instance + +.. coqtop:: all reset + + Set Universe Polymorphism. + + Inductive Squash@{s|u|} (A:Type@{s|u}) : Prop := squash (_:A). + +Elimination to `Prop` and `SProp` is always allowed, so `Squash_ind` +and `Squash_sind` are automatically defined. + +Elimination to `Type` is not allowed with variable `s`, because the +instantiation `s := Type` does not allow elimination to `Type`. + +However elimination to `Type` or to a polymorphic sort with `s := Prop` is allowed: + +.. coqtop:: all + + Definition Squash_Prop_rect A (P:Squash@{Prop|_} A -> Type) + (H:forall x, P (squash _ x)) + : forall s, P s + := fun s => match s with squash _ x => H x end. + + Definition Squash_Prop_srect@{s|u +|} A (P:Squash@{Prop|_} A -> Type@{s|u}) + (H:forall x, P (squash _ x)) + : forall s, P s + := fun s => match s with squash _ x => H x end. + +.. note:: + + Since inductive types with sort polymorphic output may only be + polymorphically eliminated to the same sort quality, containers + such as sigma types may be better defined as primitive records (which + do not have this restriction) when possible. + + .. coqtop:: all + + Set Primitive Projections. + Record sigma@{s|u v|} (A:Type@{s|u}) (B:A -> Type@{s|v}) + : Type@{s|max(u,v)} + := pair { pr1 : A; pr2 : B pr1 }. + .. _universe-polymorphism-in-sections: Universe polymorphism and sections From 676365916eb26f889d97623b9078a1d35f58af42 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 24 Nov 2023 15:35:02 +0100 Subject: [PATCH 10/10] SometimesSquashed of quality set instead of list --- checker/checkInductive.ml | 2 +- checker/values.ml | 2 +- kernel/declarations.mli | 2 +- kernel/indTyping.ml | 11 ++++++++--- kernel/inductive.ml | 7 +++++-- kernel/subtyping.ml | 2 +- pretyping/inductiveops.ml | 5 +++-- 7 files changed, 20 insertions(+), 11 deletions(-) diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 466675027dec..dda19cb95f39 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -117,7 +117,7 @@ let check_squashed orig generated = match orig, generated with | AlwaysSquashed, SometimesSquashed _ -> true | SometimesSquashed _, AlwaysSquashed -> false | SometimesSquashed s1, SometimesSquashed s2 -> - List.for_all (fun s2 -> List.exists (fun s1 -> Sorts.Quality.equal s1 s2) s1) s2 + Sorts.Quality.Set.subset s2 s1 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. diff --git a/checker/values.ml b/checker/values.ml index dfcaf20d6754..bd0c935d387b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -281,7 +281,7 @@ let v_mono_ind_arity = let v_ind_arity = v_sum "inductive_arity" 0 [|[|v_mono_ind_arity|];[|v_template_arity|]|] -let v_squash_info = v_sum "squash_info" 1 [|[|List v_quality|]|] +let v_squash_info = v_sum "squash_info" 1 [|[|v_set v_quality|]|] let v_one_ind = v_tuple "one_inductive_body" [|v_id; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 2f22d8d11c72..434c70ed1474 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -166,7 +166,7 @@ type inductive_arity = (regular_inductive_arity, template_arity) declaration_ari type squash_info = | AlwaysSquashed - | SometimesSquashed of Sorts.Quality.t list + | SometimesSquashed of Sorts.Quality.Set.t (** A sort polymorphic inductive [I@{...|...|...} : ... -> Type@{ s|...}] is squashed at a given instantiation if any quality in the list is not smaller than [s]. diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 29b022dd0920..1c874e1999ed 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -82,11 +82,11 @@ type univ_info = let add_squash q info = match info.ind_squashed with - | None -> { info with ind_squashed = Some (SometimesSquashed [q]) } + | None -> { info with ind_squashed = Some (SometimesSquashed (Sorts.Quality.Set.singleton q)) } | Some AlwaysSquashed -> info | Some (SometimesSquashed qs) -> (* XXX dedup insertion *) - { info with ind_squashed = Some (SometimesSquashed (q::qs)) } + { info with ind_squashed = Some (SometimesSquashed (Sorts.Quality.Set.add q qs)) } (* This code can probably be simplified but I can't quite see how right now. *) let check_univ_leq ?(is_real_arg=false) env u info = @@ -334,7 +334,12 @@ let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) = let squashed = Option.map (function | AlwaysSquashed -> AlwaysSquashed | SometimesSquashed qs -> - SometimesSquashed (List.map (UVars.subst_sort_level_quality usubst) qs)) + let qs = Sorts.Quality.Set.fold (fun q qs -> + Sorts.Quality.Set.add (UVars.subst_sort_level_quality usubst q) qs) + qs + Sorts.Quality.Set.empty + in + SometimesSquashed qs) univ_info.ind_squashed in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index a9ab4bf5e23b..af4cd20a0f71 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -342,8 +342,11 @@ let is_squashed ((_,mip),u) = | SometimesSquashed squash -> (* impredicative set squashes are always AlwaysSquashed, so here if inds=Set it is a sort poly squash (see "foo6" in test sort_poly.v) *) - let squash = List.map (UVars.subst_instance_quality u) squash in - if List.for_all (fun q -> quality_leq q indq) squash then None + if Sorts.Quality.Set.for_all (fun q -> + let q = UVars.subst_instance_quality u q in + quality_leq q indq) + squash + then None else Some (SquashToQuality indq) let is_allowed_elimination specifu s = diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 35087e493858..9cf8c723c77d 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -116,7 +116,7 @@ let check_variance error v1 v2 = let squash_info_equal s1 s2 = match s1, s2 with | AlwaysSquashed, AlwaysSquashed -> true - | SometimesSquashed s1, SometimesSquashed s2 -> List.equal Sorts.Quality.equal s1 s2 + | SometimesSquashed s1, SometimesSquashed s2 -> Sorts.Quality.Set.equal s1 s2 | (AlwaysSquashed | SometimesSquashed _), _ -> false (* for now we do not allow reorderings *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index f4774f112c87..7ffe4cec7d86 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -265,10 +265,11 @@ let is_squashed sigma ((_,mip),u) = | SometimesSquashed squash -> (* impredicative set squashes are always AlwaysSquashed, so here if inds=Set it is a sort poly squash (see "foo6" in test sort_poly.v) *) - if List.for_all (fun q -> + if Sorts.Quality.Set.for_all (fun q -> let q = UVars.subst_instance_quality u q in let q = UState.nf_quality (Evd.evar_universe_context sigma) q in - quality_leq q indq) squash then None + quality_leq q indq) squash + then None else Some (SquashToQuality indq) let is_allowed_elimination sigma ((mib,_),_ as specifu) s =