Add elaboration of qualities #21450

SkySkimmer · 2026-01-28T16:19:31Z

this API seems a bit awkward (to_type is ignored when collapse = false) but IDK what would be better

Yeah, I agree. The only use I've seen for collapse is for template I think.

SkySkimmer · 2026-01-28T16:22:46Z

not sure what "possible sorts" means, is it "for each fixpoint the pair of structural argument's sort and output's sort"?
also since type in type isn't per-fixpoint it should be _ array option not _ option array

I'll edit it, don't actually remember.

Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		overlay equations https://github.com/TDiazT/Coq-Equations elab-sorts 21450

-Original file line number
+Diff line change
@@ -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).

-Original file line number
+Diff line change
@@ Expand Up @@
     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}.
@@ Expand Down Expand Up / @@ -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
@@ Expand Down Expand Up @@
        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
@@ Expand All @@
                     | 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`.
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -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
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up @@
         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
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add elaboration of qualities #21450

Diff view

Diff view

There are no files selected for viewing

SkySkimmer Jan 28, 2026

Uh oh!

TDiazT Jan 29, 2026

Uh oh!

Uh oh!

SkySkimmer Jan 28, 2026

Uh oh!

TDiazT Jan 29, 2026

Uh oh!

Uh oh!

Uh oh!

-Original file line number
+Diff line change
@@ Expand Up @@
       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)
@@ Expand Down Expand Up / @@ -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
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up @@
     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
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -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
@@ Expand Down Expand Up / @@ -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
@@ Expand Down Expand Up / @@ -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
@@ Expand Down Expand Up / @@ -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
@@ Expand Down Expand Up / @@ -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 =
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -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;
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -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)
@@ Expand All @@
         || 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,
@@ Expand All @@
                 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
+        let ((ind, inst), bs) = check_occur fixenv 1 def in
         (* recursive sprop means non record with projections -> squashed *)
-        let () =
-          if Environ.is_type_in_type env (GlobRef.IndRef ind) then ()
+        let sorts_opt =
+          if Environ.is_type_in_type env (GlobRef.IndRef ind) then None
           else
+            let _, mip = lookup_mind_specif env ind in
             let sind = UVars.subst_instance_sort inst mip.mind_sort in
             let u = Sorts.univ_of_sort sind in
             (* This is an approximation: a [Relevant] variable might be of sort [Prop]
@@ Expand All @@
               | 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)
+            Some (sind, bsort)
         in
-        res
+        ind, bs, sorts_opt
       in
       (* Do it on every fixpoint *)
       let rv = Array.map2_i find_ind nvect bodies in
-      (Array.map fst rv, Array.map snd rv)
+      (Array.map (fun (minds, _, _) -> minds) rv,
+       Array.map (fun (_, rdef, _) -> rdef) rv,
+       Array.map (fun (_, _, sorts_opt) -> sorts_opt) rv)
-    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, sorts_opt) = inductive_of_mutfix ?evars env fix in
       let flags = Environ.typing_flags env in
+      let raise_err = raise_fix_guard_err_fn env recdef names 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
+        let trees = Array.map get_tree minds in
+        let () =
+          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
       else
-        ()
+        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
+      Array.iteri (fun i sort_opt ->
+          match sort_opt with
+          | None -> ()
+          | Some (ind_sort, binder_sort) ->
+            if not (is_allowed_fixpoint elim_to ind_sort binder_sort) then
+              raise_err env i @@ FixpointOnNonEliminable (ind_sort, binder_sort)
+        ) sorts_opts
     (************************************************************************)
     (* Co-fixpoints. *)
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up @@
         in these containers. *)
     val is_primitive_positive_container : env -> Constant.t -> bool
-    (** When [chk] is false, the guard condition is not actually
-        checked. *)
-    val check_fix : ?evars:evar_handler -> ?elim_to:(Sorts.Quality.t -> Sorts.Quality.t -> bool) -> env -> fixpoint -> unit
+    val check_fix_pre_sorts : ?evars:evar_handler -> env -> fixpoint -> (Sorts.t * Sorts.t) option array
+    (** Checks fixpoint without checking sort elimination constraints.
+       Returns an array of possible sorts (None if Type in Type) *)
+    val check_fix : ?evars:evar_handler -> env -> fixpoint -> unit
+    (** Checks fixpoint, along with sort elimination constraints. *)
     val check_cofix : ?evars:evar_handler -> env -> cofixpoint -> unit
     val abstract_mind_lc : int -> int -> MutInd.t -> (rel_context * constr) array -> constr array
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up @@
       end in
       let avoid = ref Id.Set.empty in
       let Proof.{sigma} = Proof.data pf in
-      let sigma = Evd.minimize_universes sigma in
+      let sigma = Evd.minimize_universes ~to_type:(PolyFlags.collapse_sort_variables poly) sigma in
       let rec fill_holes c =
         match EConstr.kind sigma c with
         | Evar (e,args) ->
@@ Expand Down @@

Add elaboration of qualities #21450

Are you sure you want to change the base?

Add elaboration of qualities #21450

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

SkySkimmer Jan 28, 2026

Choose a reason for hiding this comment

Uh oh!

TDiazT Jan 29, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

SkySkimmer Jan 28, 2026

Choose a reason for hiding this comment

Uh oh!

TDiazT Jan 29, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!