Merge PR #18331: Fully sort polymorphic inductives

Reviewed-by: ppedrot
Ack-by: tabareau
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

checker/checkInductive.ml

@@ -98,7 +98,26 @@ 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 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 ->
+      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.
@@ -122,7 +141,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 +153,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

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|]
@@ -282,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 [|[|v_set v_quality|]|]
+
 let v_one_ind = v_tuple "one_inductive_body"
   [|v_id;
     v_rctxt;
@@ -290,7 +291,7 @@ let v_one_ind = v_tuple "one_inductive_body"
     Array v_constr;
     Int;
     Int;
-    v_sortfam;
+    Opt v_squash_info;
     Array (v_pair v_rctxt v_constr);
     Array Int;
     Array Int;

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

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 <https://github.com/coq/coq/pull/17836>`_,
+  `#18331 <https://github.com/coq/coq/pull/18331>`_,
   by Gaëtan Gilbert).

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

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

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

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.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].
+
+      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 = {
 (** {8 Primitive datas } *)
@@ -198,7 +207,8 @@ 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 : 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
@@ -209,7 +219,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. *)
 

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;

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;

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 }

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;
 }

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))