Complex squash API in declarations.mli (not yet used)

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.

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

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

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,57 +94,56 @@ 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 ->
     if UGraph.check_leq (universes env) Universe.type0 indu
     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

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

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,_) =

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

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

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)

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
 

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