feat: Remove default elim constraints Type -> s

feat: Remove elim constraint Type->s by default

fix: Update to have dominance check not be done on same quality

Notably, dominance updates between sort variables were not checking
if the variables were the same. If both were the same and they were
not dominated (e.g. when removing the default Type->s constraint),
then it would loop because it would postpone the dominance check.
It really doesn't make sense though to update the dominance of a
sort variable when adding the reflexive elimination constraint.
The dominant will be the same in both cases, and if there is none,
then it will be dominated eventually when checking with other sorts.

fix: Cleanup delayed_check with sort variables

fix: Add Type->s to MaybeSquashed

fix: Add elim constraints for projections in non-primitive records

chore: Add changelog entry

refactor: Use Cmap_env to keep elim constraints from projs

Author: TDiazT

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/success/sort_poly.v

@@ -112,7 +112,7 @@ Module Inductives.
   Inductive foo2@{s; |} := Foo2 : Type@{s;Set} -> foo2.
   Check foo2_rect.
 
-  Inductive foo3@{s; |} (A:Type@{s;Set}) := Foo3 : A -> foo3 A.
+  Inductive foo3@{s;|} (A:Type@{s;Set}) : Type := Foo3 : A -> foo3 A.
   Check foo3_rect.
 
   Fail Inductive foo4@{s;u v|v < u} : Type@{v} := C (_:Type@{s;u}).
@@ -210,10 +210,13 @@ Module Inductives.
   Fail Record R5@{s; |} (A:Type@{s;Set}) : SProp := { R5f1 : A}.
   #[warnings="-non-primitive-record"]
     Record R5@{s; |} (A:Type@{s;Set}) : SProp := { R5f1 : A}.
+  Fail Check R5f1.
   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 +289,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_extraction.v

@@ -31,7 +31,7 @@ Definition foo1 := foo@{Type SProp|}.
 
 Inductive T@{s| |} : Type@{s|Set} := O : T | S : T -> T.
 
-Inductive box@{s1 s2| |} (A : Type@{s1|Set}) (B : Type@{s2|Set}) : Type@{Set} := Box : A -> B -> box A B.
+Inductive box@{s1 s2; |Type->s1, Type->s2} (A : Type@{s1;Set}) (B : Type@{s2;Set}) : Type@{Set} := Box : A -> B -> box A B.
 
 Definition bar (A : Type) (x : A) := 0.
 
@@ -44,11 +44,11 @@ Extraction TestCompile Foo.
 (* Check module subtyping *)
 
 Module Type S.
-Inductive box@{s1 s2| |} (A : Type@{s1|Set}) (B : Type@{s2|Set}) : Type@{Set} := Box : A -> B -> box A B.
+Inductive box@{s1 s2; |Type->s1, Type->s2} (A : Type@{s1;Set}) (B : Type@{s2;Set}) : Type@{Set} := Box : A -> B -> box A B.
 End S.
 
 Module Bar : S.
-Inductive box@{s1 s2| |} (A : Type@{s1|Set}) (B : Type@{s2|Set}) : Type@{Set} := Box : A -> B -> box A B.
+Inductive box@{s1 s2; |Type->s1, Type->s2} (A : Type@{s1;Set}) (B : Type@{s2;Set}) : Type@{Set} := Box : A -> B -> box A B.
 End Bar.
 
 Extraction TestCompile Bar.