Add elaboration of qualities

dev/ci/user-overlays/21450-TDiazT-elab-sorts.sh

@@ -0,0 +1 @@
+overlay equations https://github.com/TDiazT/Coq-Equations elab-sorts 21450

doc/changelog/02-specification-language/21450-elab-sorts-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  elaboration of implicit sort qualities, controlled by the flag :flag:`Collapse Sorts ToType`
+  (`#21450 <https://github.com/rocq-prover/rocq/pull/21450>`_,
+  by Tomas Diaz).

doc/sphinx/addendum/universe-polymorphism.rst

@@ -800,8 +800,6 @@ To be able to instantiate a sort with `Prop` or `SProp`, we must
 quantify over :gdef:`sort qualities`. Definitions which quantify over
 sort qualities are called :gdef:`sort polymorphic`.
 
-All sort quality variables must be explicitly bound.
-
 .. rocqtop:: all
 
    Polymorphic Definition sort@{s ; u} := Type@{s;u}.
@@ -855,6 +853,29 @@ witness these temporary variables.
 Sort polymorphic inductives may be declared when every instantiation
 is valid.
 
+.. flag:: Collapse Sorts ToType
+
+   When set, unbound sort variables are collapsed to `Type` during minimization of universes.
+   Unsetting this flag will preserve sort variables during implicit elaboration of sort-polymorphic terms,
+   if :flag:`Universe Polymorphism` is set.
+   The flag is set by default.
+
+   For instance, defining the `list` type, without explicit sorts, should elaborate two implicit ones:
+   One for the type of parameter `A`, and one for the `list` type itself.
+
+   .. rocqtop:: all
+
+      Unset Collapse Sorts ToType.
+
+      Inductive list (A : Type) : Type :=
+      | nil : list A
+      | cons : A -> list A -> list A.
+
+      Set Printing Universes.
+      About list.
+
+      Set Collapse Sorts ToType.
+
 .. _elim-constraints:
 
 Elimination of Sort-Polymorphic Inductives
@@ -953,7 +974,10 @@ It means that `s` and `s'` can respectively be instantiated to e.g., `Type` and
 
    As with universe level constraints, elimination constraints can be elaborated
    automatically if the constraints are denoted extensible with `+` **or** if they
-   are totally omitted. For instance, the two following definitions are legal.
+   are totally omitted. In addition, when unsetting :flag:`Collapse Sorts ToType`,
+   the definition may be left completely implicit, elaborating both sort variables and
+   elimination constraints.
+   For instance, the three following definitions are legal.
 
    .. rocqtop:: all
 
@@ -975,6 +999,16 @@ It means that `s` and `s'` can respectively be instantiated to e.g., `Type` and
                 | inr y => fr y
                 end.
 
+      Unset Collapse Sorts ToType.
+
+      Definition sum_elim_implicit (A B : Type) (P : sum A B -> Type)
+        (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+        (v : sum A B) : P v :=
+            match v with
+                | inl x => fl x
+                | inr y => fr y
+                end.
+
 .. note::
 
     These restrictions ignore :flag:`Definitional UIP`.

engine/evarutil.ml

@@ -32,8 +32,8 @@ let create_clos_infos env sigma flags =
 (* Expanding/testing/exposing existential variables *)
 (****************************************************)
 
-let finalize ?abort_on_undefined_evars sigma f =
-  let sigma = minimize_universes sigma in
+let finalize ?abort_on_undefined_evars ?(to_type = true) sigma f =
+  let sigma = minimize_universes ~to_type sigma in
   let uvars = ref Univ.Level.Set.empty in
   let nf_constr c =
     let _, varsc = EConstr.universes_of_constr sigma c in

engine/evarutil.mli

@@ -150,7 +150,7 @@ val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
 
     Note that the normalizer passed to [f] holds some imperative state
    in its closure. *)
-val finalize : ?abort_on_undefined_evars:bool -> evar_map ->
+val finalize : ?abort_on_undefined_evars:bool -> ?to_type:bool -> evar_map ->
   ((EConstr.t -> Constr.t) -> 'a) ->
   evar_map * 'a
 

engine/evd.ml

@@ -1031,7 +1031,7 @@ let check_univ_decl_early ~poly ~with_obls sigma udecl terms =
   in
   let vars = List.fold_left (fun acc b -> Univ.Level.Set.union acc (Vars.universes_of_constr b)) Univ.Level.Set.empty terms in
   let uctx = ustate sigma in
-  let uctx = UState.collapse_sort_variables uctx in
+  let uctx = UState.collapse_sort_variables ~to_type:(PolyFlags.collapse_sort_variables poly) uctx in
   let uctx = UState.restrict uctx vars in
   ignore (UState.check_univ_decl ~poly uctx udecl)
 
@@ -1216,13 +1216,13 @@ let nf_univ_variables evd =
   let uctx = UState.normalize_variables evd.universes in
   {evd with universes = uctx}
 
-let collapse_sort_variables ?except evd =
-  let universes = UState.collapse_sort_variables ?except evd.universes in
+let collapse_sort_variables ?except ?(to_type = true) evd =
+  let universes = UState.collapse_sort_variables ?except ~to_type evd.universes in
   { evd with universes }
 
-let minimize_universes ?(collapse_sort_variables=true) evd =
+let minimize_universes ?(collapse_sort_variables=true) ?(to_type = true) evd =
   let uctx' = if collapse_sort_variables
-    then UState.collapse_sort_variables evd.universes
+    then UState.collapse_sort_variables ~to_type evd.universes
     else evd.universes
   in
   let uctx' = UState.normalize_variables uctx' in

engine/evd.mli

@@ -643,12 +643,12 @@ val with_sort_context_set : ?loc:Loc.t -> ?sort_rigid:bool -> ?src:UState.constr
 
 val nf_univ_variables : evar_map -> evar_map
 
-val collapse_sort_variables : ?except:Sorts.QVar.Set.t -> evar_map -> evar_map
+val collapse_sort_variables : ?except:Sorts.QVar.Set.t -> ?to_type:bool -> evar_map -> evar_map
 
 val fix_undefined_variables : evar_map -> evar_map
 
 (** Universe minimization (collapse_sort_variables is true by default) *)
-val minimize_universes : ?collapse_sort_variables:bool -> evar_map -> evar_map
+val minimize_universes : ?collapse_sort_variables:bool -> ?to_type:bool -> evar_map -> evar_map
 
 (** Lift [UState.update_sigma_univs] *)
 val update_sigma_univs : UGraph.t -> evar_map -> evar_map

engine/uState.ml

@@ -95,7 +95,7 @@ module QState : sig
   val unify_quality : fail:(unit -> t) -> Conversion.conv_pb -> Quality.t -> Quality.t -> t -> t
   val undefined : t -> QVar.Set.t
   val collapse_above_prop : to_prop:bool -> t -> t
-  val collapse : ?except:QVar.Set.t -> t -> t
+  val collapse : ?except:QVar.Set.t -> ?to_type:bool -> t -> t
   val pr : (QVar.t -> Libnames.qualid option) -> t -> Pp.t
   val of_elims : QGraph.t -> t
   val elims : t -> QGraph.t
@@ -158,18 +158,19 @@ let set q qv m =
   let q, rigid = match q with ReprVar (q, rigid) -> q, rigid | ReprConstant _ -> assert false in
   let qv = match qv with QVar qv -> repr_node qv m | QConstant qc -> ReprConstant qc in
   let enforce_eq q1 q2 g = QGraph.enforce_eliminates_to q1 q2 (QGraph.enforce_eliminates_to q2 q1 g) in
-  match q, qv with
-  | q, ReprVar (qv, _qvrigd) ->
+  match qv with
+  | ReprVar (qv, _qvrigd) ->
     if QVar.equal q qv then Some m
     else if rigid then None
     else
       let above_prop =
         if is_above_prop m q
         then QSet.add qv (QSet.remove q m.above_prop)
         else m.above_prop in
-      Some { qmap = QMap.add q (Equiv (QVar qv)) m.qmap; above_prop;
-             elims = enforce_eq (QVar qv) (QVar q) m.elims; initial_elims = m.initial_elims }
-  | q, ReprConstant qc ->
+      Some { m with
+             qmap = QMap.add q (Equiv (QVar qv)) m.qmap; above_prop;
+             elims = enforce_eq (QVar qv) (QVar q) m.elims; }
+  | ReprConstant qc ->
     if qc == QSProp && (is_above_prop m q || eliminates_to_prop m q) then None
     else if rigid then None
     else
@@ -299,13 +300,40 @@ let collapse_above_prop ~to_prop m =
          )
          m.qmap m
 
-let collapse ?(except=QSet.empty) m =
+let collapse ?(except=QSet.empty) ?(to_type = true) m =
+  let free_qualities = QMap.fold (fun q v fqs ->
+      match v with
+      | Equiv _ -> fqs
+      | Canonical _ -> QSet.add q fqs)
+      m.qmap QSet.empty
+  in
+  let dominates_above_prop q q' =
+    not (QVar.equal q q') && QGraph.eliminates_to m.elims (QVar q) (QVar q') && not (QSet.mem q m.above_prop)
+  in
   QMap.fold (fun q v m ->
-           match v with
-           | Equiv _ -> m
-           | Canonical { rigid } -> if rigid || QSet.mem q except then m
-                    else Option.get (set q qtype m))
-         m.qmap m
+      match v with
+      | Equiv _ -> m
+      | Canonical { rigid } ->
+        if rigid || QSet.mem q except then m
+        (* This check is necessary because there is a particular scenario where we could end up
+           with an unsatisfied elimination constraint or an unnecessary elaborated elimination constraint to Type
+           (or some inexistent sort variable); if we simply defaulted sort variables to Type, as before.
+           This comes from a weird interaction with "above Prop". The scenario is:
+           - An unbound sort variable β might be set to be above Prop during unification, which in practice
+             should be equal to Prop.
+           - A rigid sort s eliminates to Prop explicitly (and β, since they are supposed to be equal)
+           - Collapsing β to Type means that now sort s eliminates to Type, but this is an undeclared constraint,
+             and therefore the declaration fails.
+
+           This check is therefore simply finding if the sort variable above Prop is dominated by another one.
+           If so, the sort variable collapses to Prop, otherwise to Type (if collapsing is enabled), or we keep it.
+        *)
+        else if QSet.mem q m.above_prop then
+          if QSet.exists (fun q' -> dominates_above_prop q' q) free_qualities then
+            Option.get (set q qprop m)
+          else Option.get (set q qtype m)
+        else if to_type then Option.get (set q qtype m) else m)
+    m.qmap m
 
 let pr prqvar_opt ({ qmap; elims } as m) =
   let open Pp in
@@ -352,7 +380,8 @@ let normalize_elim_constraints m cstrs =
   let can_drop (q1,_,q2) = not (is_instantiated q1 && is_instantiated q2) in
   let subst_cst (q1,c,q2) = (subst q1,c,subst q2) in
   let cstrs = ElimConstraints.map subst_cst cstrs in
-  ElimConstraints.filter can_drop cstrs
+  let cstrs = ElimConstraints.filter can_drop cstrs in
+  ElimConstraints.filter (fun (q1, _, q2) -> not @@ Quality.equal q1 q2) cstrs
 end
 
 module UPairSet = UnivMinim.UPairSet
@@ -1492,8 +1521,8 @@ let collapse_above_prop_sort_variables ~to_prop uctx =
   let sorts = QState.collapse_above_prop ~to_prop uctx.sort_variables in
   normalize_quality_variables { uctx with sort_variables = sorts }
 
-let collapse_sort_variables ?except uctx =
-  let sorts = QState.collapse ?except uctx.sort_variables in
+let collapse_sort_variables ?except ?(to_type = true) uctx =
+  let sorts = QState.collapse ?except ~to_type uctx.sort_variables in
   normalize_quality_variables { uctx with sort_variables = sorts }
 
 let minimize uctx =

engine/uState.mli

@@ -243,7 +243,7 @@ val minimize : t -> t
 
 val collapse_above_prop_sort_variables : to_prop:bool -> t -> t
 
-val collapse_sort_variables : ?except:QVar.Set.t -> t -> t
+val collapse_sort_variables : ?except:QVar.Set.t -> ?to_type:bool -> t -> t
 
 type ('a, 'b, 'c, 'd) gen_universe_decl = {
   univdecl_qualities : 'a;

kernel/inductive.ml

@@ -1626,7 +1626,14 @@ let check_one_fix cache ?evars renv recpos trees def =
   | NeedReduce (env,err) -> raise (FixGuardError (env,err))
   | NoNeedReduce -> ()
 
-let inductive_of_mutfix ?evars ?elim_to env ((nvect,bodynum),(names,types,bodies as recdef)) =
+let raise_fix_guard_err_fn env recdef names =
+  let fixenv = push_rec_types recdef env in
+  let vdefj = judgment_of_fixpoint recdef in
+  let raise_err env i err =
+    error_ill_formed_rec_body env (Type_errors.FixGuardError err) names i fixenv vdefj in
+  raise_err
+
+let inductive_of_mutfix ?evars env ((nvect, bodynum), (names, types, bodies as recdef)) =
   let nbfix = Array.length bodies in
   if Int.equal nbfix 0
     || not (Int.equal (Array.length nvect) nbfix)
@@ -1636,9 +1643,7 @@ let inductive_of_mutfix ?evars ?elim_to env ((nvect,bodynum),(names,types,bodies
     || bodynum >= nbfix
   then anomaly (Pp.str "Ill-formed fix term.");
   let fixenv = push_rec_types recdef env in
-  let vdefj = judgment_of_fixpoint recdef in
-  let raise_err env i err =
-    error_ill_formed_rec_body env (Type_errors.FixGuardError err) names i fixenv vdefj in
+  let raise_err = raise_fix_guard_err_fn env recdef names in
   (* Check the i-th definition with recarg k *)
   let find_ind i k def =
     (* check fi does not appear in the k+1 first abstractions,
@@ -1662,55 +1667,69 @@ let inductive_of_mutfix ?evars ?elim_to env ((nvect,bodynum),(names,types,bodies
             else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
         | _ -> raise_err env i (NotEnoughAbstractionInFixBody k)
     in
-    let ((ind, inst), _) as res = check_occur fixenv 1 def in
-    let _, mip = lookup_mind_specif env ind in
-    (* recursive sprop means non record with projections -> squashed *)
-    let () =
-      if Environ.is_type_in_type env (GlobRef.IndRef ind) then ()
-      else
-        let sind = UVars.subst_instance_sort inst mip.mind_sort in
-        let u = Sorts.univ_of_sort sind in
+    check_occur fixenv 1 def
+  in
+  (* Do it on every fixpoint *)
+  let rv = Array.map2_i find_ind nvect bodies in
+  (Array.map fst rv, Array.map snd rv)
+
+(* Returns the pairs of (inductive sort * output sort) or None if Type in Type *)
+let sorts_of_mutfix env minds names =
+  let check_type_in_type (ind, _) = Environ.is_type_in_type env (GlobRef.IndRef ind) in
+  (* recursive sprop means non record with projections -> squashed *)
+  if Array.exists check_type_in_type minds then None
+  else
+    Some (Array.fold_left_i (fun i sorts (ind, inst) ->
+        let _, mip = lookup_mind_specif env ind in
+        let ind_sort = UVars.subst_instance_sort inst mip.mind_sort in
+        let u = Sorts.univ_of_sort ind_sort in
         (* This is an approximation: a [Relevant] variable might be of sort [Prop]
            or [Type]. As we only care about the quality, we have to be conservative
            here, i.e., every relevant sort (so, [Prop] or above) can be eliminated
            into any other relevant sort. *)
-        let bsort = match names.(i).Context.binder_relevance with
+        let out_sort = match names.(i).Context.binder_relevance with
           | Irrelevant -> Sorts.sprop
           | Relevant -> Sorts.prop
           | RelevanceVar q -> Sorts.qsort q u in
-        let elim_to = match elim_to with
-          | Some f -> f
-          | None -> eliminates_to (Environ.qualities env) in
-        if not (is_allowed_fixpoint elim_to sind bsort) then
-          raise_err env i @@ FixpointOnNonEliminable (sind, bsort)
-    in
-    res
-  in
-  (* Do it on every fixpoint *)
-  let rv = Array.map2_i find_ind nvect bodies in
-  (Array.map fst rv, Array.map snd rv)
+        (ind_sort, out_sort) :: sorts
+      ) [] minds)
 
 
-let check_fix ?evars ?elim_to env ((nvect,_),(names,_,bodies as recdef) as fix) =
+let check_fix_pre_sorts ?evars env ((nvect, _), (names, _, bodies as recdef) as fix) =
   let cache = Cache.create () in
-  let (minds, rdef) = inductive_of_mutfix ?evars ?elim_to env fix in
+(* For elaboration of elimination constraints, we need to update the evar_map with
+   the possibly new constraints (see e.g. [esearch_guard] (Pretyping)). We expose this
+   function to be used for this purpose, while check_fix performs the normal check,
+   failing when elimination constraints are not satisfied. *)
+  let minds, rdef = inductive_of_mutfix ?evars env fix in
+  let sorts_opt = sorts_of_mutfix env minds names in
+  let inds = Array.map fst minds in
   let flags = Environ.typing_flags env in
-  if flags.check_guarded then
-    let get_tree (kn,i) =
-      let mib = Environ.lookup_mind kn env in
-      mib.mind_packets.(i).mind_recargs
-    in
-    let trees = Array.map (fun (mind,_) -> get_tree mind) minds in
-    for i = 0 to Array.length bodies - 1 do
-      let (fenv,body) = rdef.(i) in
-      let renv = make_renv fenv nvect.(i) trees.(i) in
-      try check_one_fix cache ?evars renv nvect trees body
-      with FixGuardError (fixenv,err) ->
-        error_ill_formed_rec_body fixenv (Type_errors.FixGuardError err) names i
-          (push_rec_types recdef env) (judgment_of_fixpoint recdef)
-    done
-  else
-    ()
+  let raise_err = raise_fix_guard_err_fn env recdef names in
+  let () =
+    if flags.check_guarded then
+      let get_tree (kn,i) =
+        let mib = Environ.lookup_mind kn env in
+        mib.mind_packets.(i).mind_recargs
+      in
+      let trees = Array.map get_tree inds in
+      for i = 0 to Array.length bodies - 1 do
+        let (fenv, body) = rdef.(i) in
+        let renv = make_renv fenv nvect.(i) trees.(i) in
+        try check_one_fix cache ?evars renv nvect trees body
+        with FixGuardError (err_env, err) -> raise_err err_env i err
+      done
+  in
+  sorts_opt
+
+let check_fix ?evars env (_, (names, _, _ as recdef) as fix) =
+  let sorts_opts = check_fix_pre_sorts ?evars env fix in
+  let raise_err = raise_fix_guard_err_fn env recdef names in
+  let elim_to = eliminates_to (Environ.qualities env) in
+  Option.iter (List.iteri (fun i (ind_sort, out_sort) ->
+      if not (is_allowed_fixpoint elim_to ind_sort out_sort) then
+        raise_err env i @@ FixpointOnNonEliminable (ind_sort, out_sort)
+    )) sorts_opts
 
 (************************************************************************)
 (* Co-fixpoints. *)