Module subtyping: primitive fields cannot be implemented

Fix coq#18503

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

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

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
+*)
+*)