From 7b929640a052c9ccfa1685fd28fb901b44ecf0f2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 17 Jan 2024 14:20:10 +0100
Subject: [PATCH] Module subtyping: primitive fields cannot be implemented

Fix #18503
---
 dev/doc/critical-bugs       | 13 ++++++++++--
 kernel/subtyping.ml         | 21 +++++++++++--------
 test-suite/bugs/bug_18503.v | 41 +++++++++++++++++++++++++++++++++++++
 3 files changed, 65 insertions(+), 10 deletions(-)
 create mode 100644 test-suite/bugs/bug_18503.v

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 1eabba3de90cd..d418165eb2311 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -151,8 +151,6 @@ Module system
   GH issue number: #4294
   risk: ?
 
-Module system
-
   component: modules, universes
   summary: universe constraints for module subtyping not stored in vo files
   introduced: presumably 8.2 (b3d3b56)
@@ -187,6 +185,17 @@ Module system
   exploit: see issue
   risk: medium
 
+  component: modules, primitive types
+  summary: Primitives are incorrectly considered convertible to anything by module subtyping
+  introduced: 8.11
+  impacted released versions: V8.11.0-V8.18.0
+  impacted coqchk versions: same
+  fixed in: V8.19.0
+  found by: Gaëtan Gilbert
+  GH issue number: #18503
+  exploit: see issue
+  risk: high if there is a Primitive in a Module Type, otherwise low
+
 Universes
 
   component: template polymorphism
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 9cf8c723c77d9..b33be580811ee 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -246,18 +246,23 @@ let check_constant (cst, ustate) trace env l info1 cb2 subst1 subst2 =
       (* Now we check the bodies:
          - A transparent constant can only be implemented by a compatible
            transparent constant.
+         - A primitive cannot be implemented.
+           (We could try to allow implementing with the same primitive,
+            but for some reason we get cb1.const_body = Def,
+            without some use case there is no motivation to solve this.)
          - In the signature, an opaque is handled just as a parameter:
            anything of the right type can implement it, even if bodies differ.
       *)
       (match cb2.const_body with
-        | Primitive _ | Undef _ | OpaqueDef _ -> cst
-        | Def c2 ->
-          (match cb1.const_body with
-            | Primitive _ | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField
-            | Def c1 ->
-              (* NB: cb1 might have been strengthened and appear as transparent.
-                 Anyway [check_conv] will handle that afterwards. *)
-              check_conv NotConvertibleBodyField cst poly CONV env c1 c2))
+       | Undef _ | OpaqueDef _ -> cst
+       | Primitive _ -> error NotConvertibleBodyField
+       | Def c2 ->
+         (match cb1.const_body with
+          | Primitive _ | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField
+          | Def c1 ->
+            (* NB: cb1 might have been strengthened and appear as transparent.
+               Anyway [check_conv] will handle that afterwards. *)
+            check_conv NotConvertibleBodyField cst poly CONV env c1 c2))
 
 let rec check_modules state trace env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module msb1 in
diff --git a/test-suite/bugs/bug_18503.v b/test-suite/bugs/bug_18503.v
new file mode 100644
index 0000000000000..4d6a10027d277
--- /dev/null
+++ b/test-suite/bugs/bug_18503.v
@@ -0,0 +1,41 @@
+Require Import PrimInt63.
+Open Scope int63_scope.
+
+Module Type T.
+  Primitive bar := #int63_sub.
+
+  Axiom bar_land : bar = land.
+End T.
+
+Module F(X:T).
+  Definition foo : X.bar 1 1 = 0 := eq_refl.
+End F.
+
+Module M.
+  Definition bar := land.
+  Definition bar_land : bar = land := eq_refl.
+End M.
+
+Fail Module N : T := M.
+
+(*
+Module A := F N.
+
+Lemma bad : False.
+Proof.
+  pose (f := fun x => eqb x 1).
+  assert (H:f 1 = f 0).
+  { f_equal. change 1 with (land 1 1).
+    rewrite <-N.bar_land.
+    exact A.foo. }
+  change (true = false) in H.
+  inversion H.
+Qed.
+
+Print Assumptions bad.
+(* Axioms:
+land : int -> int -> int
+int : Set
+eqb : int -> int -> bool
+*)
+*)