Merge PR #12912: Fix algebraic comparison with sprop on one side

Reviewed-by: mattam82
Reviewed-by: ppedrot

2 files changed, 14 insertions, 0 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 927db9e9e6..52e93a9e22 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -142,6 +142,12 @@ let enforce_leq_alg u v g =
   | Inl x -> x
   | Inr e -> raise e
 
+let enforce_leq_alg u v g =
+  match Universe.is_sprop u, Universe.is_sprop v with
+  | true, true -> Constraint.empty, g
+  | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None))
+  | false, false -> enforce_leq_alg u v g
+
 (* sanity check wrapper *)
 let enforce_leq_alg u v g =
   let _,g as cg = enforce_leq_alg u v g in
diff --git a/test-suite/bugs/closed/bug_12909.v b/test-suite/bugs/closed/bug_12909.v
new file mode 100644
index 0000000000..fafb6a418f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12909.v
@@ -0,0 +1,8 @@
+Module Type T.
+Axiom A : Type.
+End T.
+
+Module M.
+  Axiom A : SProp.
+End M.
+Fail Module N <: T := M.