feat: Remove elim constraint Type->s by default

Author: TDiazT

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
@@ -234,16 +233,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

test-suite/success/sort_poly.v

@@ -109,7 +109,9 @@ Module Inductives.
   Inductive foo2@{s; |} := Foo2 : Type@{s;Set} -> foo2.
   Check foo2_rect.
 
-  Inductive foo3@{s; |} (A:Type@{s;Set}) := Foo3 : A -> foo3 A.
+  (* This is now invalid since Type does not eliminate to arbitrary sorts by default *)
+  Fail Inductive foo3@{s; |} (A:Type@{s;Set}) := Foo3 : A -> foo3 A.
+  Inductive foo3@{s; |Type->s} (A:Type@{s;Set}) := Foo3 : A -> foo3 A.
   Check foo3_rect.
 
   Fail Inductive foo4@{s;u v|v < u} : Type@{v} := C (_:Type@{s;u}).
@@ -212,17 +214,25 @@ 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) =>
           eq_refl : Conversion.box _ x.(R6f1 _) = Conversion.box _ y.(R6f1 _).
   Fail Check fun (A:SProp) (x y : R6 A) =>
           eq_refl : Conversion.box _ x.(R6f2 _) = Conversion.box _ y.(R6f2 _).
 
-  #[projections(primitive=no)] Record R7@{s; |} (A:Type@{s;Set}) := { R7f1 : A; R7f2 : nat }.
+  (* This is now invalid since Type does not eliminate to arbitrary sorts by default *)
+  Fail #[projections(primitive=no)] Record R7@{s; |} (A:Type@{s;Set}) := { R7f1 : A; R7f2 : nat }.
+  #[projections(primitive=no)] Record R7@{s; |Type -> s} (A:Type@{s;Set}) := { R7f1 : A; R7f2 : nat }.
   Check R7@{SProp;} : SProp -> Set.
   Check R7@{Type;} : Set -> Set.
+  #[universes(polymorphic=no)]
+  Sort s7.
+  Fail Check R7@{s7;} : 𝒰@{s7;0} -> Set.
+  (* This expression would enforce a non-declared elimination constraint between Type and s7 *)
 
   Inductive sigma@{s;u v|} (A:Type@{s;u}) (B:A -> Type@{s;v}) : Type@{s;max(u,v)}
     := pair : forall x : A, B x -> sigma A B.
@@ -284,7 +294,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.