feat: Remove Type eliminates to any sort by default

doc/changelog/01-kernel/21453-remove-type-to-sorts-Changed.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  `Type` does not eliminate to every sort by default
+  (`#21453 <https://github.com/rocq-prover/rocq/pull/21453>`_,
+  by Tomas Diaz).

kernel/indTyping.ml

@@ -135,7 +135,13 @@ let compute_elim_squash ?(is_real_arg=false) env u info =
     | QSort (q, _), (SProp | Prop) ->
         if Environ.Internal.is_above_prop env q then info
         else add_squash (Sorts.quality u) info
-    | _, _ -> { info with ind_squashed = Some AlwaysSquashed }
+    | (Type _ | Set), QSort (q, _) -> add_squash (QVar q) info
+    | SProp, (Prop | Type _ | Set) ->
+        { info with ind_squashed = Some AlwaysSquashed }
+    | Prop, (Type _ | Set) -> { info with ind_squashed = Some AlwaysSquashed }
+    (* These cases should not happen because `eliminates_to` above should be true,
+      * e.g., Type -> (S)Prop, SProp -> SProp, etc. *)
+    | (Type _ | Set | SProp | Prop), _ -> assert false
 
 let check_context_univs ~ctor env info ctx =
   let check_one d (info,env) =

kernel/qGraph.ml

@@ -21,7 +21,6 @@ module ElimTable = struct
 
   let eliminates_to q q' =
     match q, q' with
-    | QConstant QType, _ -> true
     | QConstant q, QConstant q' -> const_eliminates_to q q'
     | QVar q, QVar q' -> QVar.equal q q'
     | (QConstant _ | QVar _), _ -> false
@@ -159,11 +158,31 @@ let rec update_dominance g q qv =
     | Some q' -> update_dominant_if_related g qv q' q in
   match QMap.find_opt qv g.delayed_check with
   | None -> g'
-  | Some qs ->
-     let g' = QSet.fold (fun v g -> Option.bind g (fun g -> update_dominance g q v)) qs g' in
-     match g' with
-     | Some graph -> Some { graph with delayed_check = QMap.set qv QSet.empty g.delayed_check }
-     | None -> None
+  | Some delayed_qs ->
+    (* When two sort variables are `set` to each other, e.g. uState, (q1 <-> q2), without being
+       dominated, then both delay the domination check of each other:
+       delayed_check[q1] = {q2}
+       delayed_check[q2] = {q1}
+
+       When one of them becomes dominated, e.g. q1 dominated by Type, then we need to clear up
+       any occurrence of it in the delayed check of the other, e.g. remove q1 from delayed_check[q2].
+       Otherwise, we end up in a loop. *)
+    let remove_qv_from_delayed delayed_q delayed_check =
+      match QMap.find_opt delayed_q delayed_check with
+      | None -> delayed_check
+      | Some dqs ->
+        QMap.set delayed_q (QSet.remove qv dqs) delayed_check
+    in
+    let clearup_cyclic_delay graph =
+      QSet.fold (fun delayed_q acc_graph ->
+        { acc_graph with delayed_check = remove_qv_from_delayed delayed_q acc_graph.delayed_check })
+        delayed_qs graph
+    in
+    let g' = Option.map clearup_cyclic_delay g' in
+    let g' = QSet.fold (fun v g -> Option.bind g (fun g -> update_dominance g q v)) delayed_qs g' in
+    match g' with
+    | Some graph -> Some { graph with delayed_check = QMap.set qv QSet.empty g.delayed_check }
+    | None -> None
 
 let update_dominance_if_valid g (q1,k,q2) =
   match k with
@@ -173,6 +192,8 @@ let update_dominance_if_valid g (q1,k,q2) =
      else
        match q1, q2 with
        | (Quality.QConstant _ | Quality.QVar _), Quality.QConstant _ -> assert false
+       | Quality.QVar qv1, Quality.QVar qv2 when QVar.equal qv1 qv2 -> assert false
+        (* It makes no sense to update or delay the dominance of a sort variable when it eliminates to itself *)
        | Quality.QVar qv1, Quality.QVar qv2 ->
           (* 3 cases:
              - if [qv1] is a global, treat as constants.
@@ -183,7 +204,7 @@ let update_dominance_if_valid g (q1,k,q2) =
             (match QMap.find_opt qv1 g.dominant with
             | None ->
                let add_delayed qs =
-                 Some { g with delayed_check = QMap.set qv1 (QSet.add qv2 qs) g.delayed_check }
+                 Some { g with delayed_check = QMap.add qv1 (QSet.add qv2 qs) g.delayed_check }
                in
                (match QMap.find_opt qv1 g.delayed_check with
                | None -> add_delayed QSet.empty
@@ -232,8 +253,9 @@ let enforce_constraint (q1, k, q2) g =
      if ignore_constraints g then g else
      let e = lazy (G.get_explanation (q1,to_graph_cstr k,q2) g.graph) in
      raise @@ EliminationError (QualityInconsistency (None, (k, q1, q2, Some (Path e))))
-  | Some g ->
-    dominance_check g (q1, k, q2)
+  | Some graph ->
+    if Quality.equal q1 q2 then graph
+    else dominance_check graph (q1, k, q2)
 
 let merge_constraints csts g = ElimConstraints.fold enforce_constraint csts g
 
@@ -248,16 +270,11 @@ exception AlreadyDeclared = G.AlreadyDeclared
 
 let add_quality q g =
   let graph = G.add q g.graph in
-  let g = enforce_constraint (Quality.qtype, ElimConstraint.ElimTo, q) { g with graph } in
-  let (paths,ground_and_global_sorts) =
+  let ground_and_global_sorts =
     if Quality.is_qglobal q
-    then (RigidPaths.add_elim_to Quality.qtype q g.rigid_paths, Quality.Set.add q g.ground_and_global_sorts)
-    else (g.rigid_paths,g.ground_and_global_sorts) in
-  (* As Type ~> s, set Type to be the dominant sort of q if q is a variable. *)
-  let dominant = match q with
-    | Quality.QVar qv -> QMap.add qv Quality.qtype g.dominant
-    | Quality.QConstant _ -> g.dominant in
-  { g with rigid_paths = paths; ground_and_global_sorts; dominant }
+    then Quality.Set.add q g.ground_and_global_sorts
+    else g.ground_and_global_sorts in
+  { g with graph; ground_and_global_sorts }
 
 let enforce_eliminates_to s1 s2 g =
   enforce_constraint (s1, ElimConstraint.ElimTo, s2) g
@@ -307,9 +324,10 @@ let merge g g' =
              (fun q acc -> try add_quality q acc with _ -> acc) qs g in
   Quality.Set.fold
     (fun q -> Quality.Set.fold
-             (fun q' acc -> if eliminates_to g' q q'
-                         then enforce_eliminates_to q q' acc
-                         else acc) qs) qs g
+      (fun q' acc -> if Quality.equal q q' then acc
+        else if eliminates_to g' q q'
+        then enforce_eliminates_to q q' acc
+        else acc) qs) qs g
 
 let is_empty g = QVar.Set.is_empty (qvar_domain g)
 

test-suite/output/sort_poly_elab.v

@@ -440,6 +440,13 @@ Module Inductives.
   (* α α0 ; u |= α -> SProp *)
   About list_idS.
 
+  Fixpoint list_idTS {A : Type} (l : list@{_ Type;_} A) : list A :=
+    match l with
+    | nil => nil
+    | cons x l => cons x (list_idTS l)
+    end.
+  About list_idTS.
+
   Fixpoint map A B f (l : list A) : list B :=
     match l with
     | nil => nil
@@ -496,6 +503,13 @@ Module Inductives.
   (* α ;  |= α -> Type *)
   About bool_to_Prop'.
 
+  Definition bool_idTS (b : bool@{Type;}) : bool :=
+    match b with
+    | true => true
+    | false => false
+    end.
+  About bool_idTS.
+
   #[universes(polymorphic=no)]
   Sort Test.
   (* Sort variables not instantiated *)

test-suite/success/sort_poly.v

@@ -213,7 +213,9 @@ Module Inductives.
   Definition R5f1_sprop (A:SProp) (r:R5 A) : A := let (f) := r in f.
   Fail Definition R5f1_prop (A:Prop) (r:R5 A) : A := let (f) := r in f.
 
-  Record R6@{s; |} (A:Type@{s;Set}) := { R6f1 : A; R6f2 : nat }.
+  (* This is now invalid since Type does not eliminate to arbitrary sorts by default *)
+  Fail Record R6@{s; |} (A:Type@{s;Set}) := { R6f1 : A; R6f2 : nat }.
+  Record R6@{s; |Type->s} (A:Type@{s;Set}) := { R6f1 : A; R6f2 : nat }.
   Check fun (A:SProp) (x y : R6 A) =>
           eq_refl : Conversion.box _ x.(R6f1 _) = Conversion.box _ y.(R6f1 _).
   Fail Check fun (A:Prop) (x y : R6 A) =>
@@ -286,7 +288,10 @@ Module Inductives.
 
   Arguments exist3 {_ _}.
 
-  Definition π1@{s s';u v|} {A:Type@{s;u}} {P:A -> Type@{s';v}} (p : sigma3@{_ _ Type;_ _} A P) : A :=
+  (* This is now invalid since Type does not eliminate to arbitrary sorts by default *)
+  Fail Definition π1@{s s';u v|} {A:Type@{s;u}} {P:A -> Type@{s';v}} (p : sigma3@{_ _ Type;_ _} A P) : A :=
     match p return A with exist3 a _ => a end.
-
+  Definition π1@{s s';u v|Type -> s} {A:Type@{s;u}} {P:A -> Type@{s';v}} (p : sigma3@{_ _ Type;_ _} A P) : A :=
+    match p return A with exist3 a _ => a end.
+  (* s s' ; u v |= Type -> s *)
 End Inductives.

test-suite/success/sort_poly_elim_csts.v

@@ -192,3 +192,17 @@ Fixpoint list'_idV@{s s0 s';l l'|l <= l', s0 -> s'} {A : Type@{s;l}} (l : List'@
   | nil' => nil'
   | cons' x l => cons' x (list'_idV l)
   end.
+
+Inductive bool@{s;} : Type@{s;Set} := true | false.
+
+Fail Definition bool_idTS@{s;} (b : bool@{Type;}) : bool@{s;} :=
+  match b with
+  | true => true
+  | false => false
+  end.
+
+Definition bool_idTS@{s;| Type -> s} (b : bool@{Type;}) : bool@{s;} :=
+  match b with
+  | true => true
+  | false => false
+  end.