Check @notUndefined of an interface against the implementation

changes/not-undefined-inclusion.fix.md

@@ -0,0 +1 @@
+- Reject an implementation that can hold `undefined` for a type its interface declares `@notUndefined`, which made `Some(None)` of the type `None` in clients.

compiler/ml/UntaggedVariants.md

@@ -409,14 +409,24 @@ values are never `undefined`. It affects only rule 12: `option` of the type,
 and of an untagged variant with a payload of the type, is unboxed. It does not
 make the type a recognized payload kind (rule 4). On any other type
 declaration it is an error, "@notUndefined can only be used on abstract
-types". Interface inclusion does not compare it. `@instanceOf` and `@typeOf`
-(rule 5) imply it.
+types". `@instanceOf` and `@typeOf` (rule 5) imply it.
+
+When an interface declares a type `@notUndefined`, its implementation must be
+a type that cannot hold `undefined` either, or an abstract type, which has no
+representation to contradict it. `type t = option<int>` under
+`@notUndefined type t` is an error: "Their runtime representations
+differ: the second declaration is @notUndefined, but the first declaration
+can hold undefined". The same holds
+for functor arguments and `with type` constraints.
 
 - Implementation: `typedecl.ml:transl_declaration`, `is_not_undefined_attr`;
-  `typeopt.ml:type_cannot_contain_undefined`.
-- Tests: `spec_test` rule 13; fixture `invalid_attribute_not_undefined.res`;
+  `typeopt.ml:type_cannot_contain_undefined`;
+  `includemod.ml:not_undefined_mismatch`.
+- Tests: `spec_test` rule 13; fixtures `invalid_attribute_not_undefined.res`,
+  `not_undefined_functor_argument.res`;
+  `tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation`;
   `tests/build_tests/not_undefined_attribute`.
-- Shaped by #7458, #7464.
+- Shaped by #7458, #7464, #8964.
 
 ### 14. `@tag` and interfaces
 
@@ -527,8 +537,8 @@ had to answer, and the answers of rule 5:
 4. **The unchecked branch** stays the contract (rule 10).
 5. **Realms.** Recognition is local to a realm (rule 10).
 6. **Interfaces and functors** compare declared classes and kinds, and the
-   payload kinds of untagged cases (rule 14). They still do not compare
-   `@notUndefined`.
+   payload kinds of untagged cases (rule 14), and `@notUndefined` against
+   the implementation (rule 13).
 7. **Implied `@notUndefined`.** A declared class or kind implies it, and
    rule 5 rejects annotations on abbreviations of types that can hold
    `undefined`.

compiler/ml/includecore.ml

@@ -185,6 +185,7 @@ type type_mismatch =
   | Tag_name
   | Variant_representation of Ident.t
   | Runtime_annotation of string * string
+  | Not_undefined
 
 let report_type_mismatch0 first second decl ppf err =
   let pr fmt = Format.fprintf ppf fmt in
@@ -217,6 +218,11 @@ let report_type_mismatch0 first second decl ppf err =
   | Tag_name -> pr "Their @tag annotations differ"
   | Variant_representation s ->
     pr "The internal representations for case %s are not equal" (Ident.name s)
+  | Not_undefined ->
+    pr
+      "Their runtime representations differ:@ %s %s is @notUndefined,@ but %s \
+       %s can hold undefined"
+      second decl first decl
   | Runtime_annotation (declared1, declared2) ->
     pr
       "Their runtime representations differ:@ %s %s states %s,@ %s %s states %s"

compiler/ml/includecore.mli

@@ -39,6 +39,7 @@ type type_mismatch =
   | Tag_name
   | Variant_representation of Ident.t
   | Runtime_annotation of string * string
+  | Not_undefined
 
 val value_descriptions :
   loc:Location.t ->

compiler/ml/includemod.ml

@@ -62,12 +62,35 @@ let value_descriptions ~loc env cxt subst id vd1 vd2 =
 
 (* Inclusion between type declarations *)
 
+(* [@notUndefined] lets clients unbox [option] of the type, so the
+   implementation must be a type that cannot hold [undefined] either. An
+   abstract implementation has no representation to contradict it. *)
+let not_undefined_mismatch env id (decl1 : Types.type_declaration)
+    (decl2 : Types.type_declaration) =
+  let is_abstract =
+    decl1.type_kind = Type_abstract && decl1.type_manifest = None
+  in
+  if
+    (not is_abstract)
+    && List.exists Typedecl.is_not_undefined_attr decl2.type_attributes
+  then
+    let env = Env.add_type ~check:false id decl1 env in
+    let ty =
+      Btype.newgenty (Tconstr (Pident id, decl1.type_params, ref Mnil))
+    in
+    if Typeopt.type_cannot_contain_undefined ty env then []
+    else [Includecore.Not_undefined]
+  else []
+
 let type_declarations ~loc env ?(old_env = env) cxt subst id decl1 decl2 =
   Env.mark_type_used env (Ident.name id) decl1;
   let decl2 = Subst.type_declaration subst decl2 in
   let err =
     Includecore.type_declarations ~loc env (Ident.name id) decl1 id decl2
   in
+  let err =
+    if err <> [] then err else not_undefined_mismatch env id decl1 decl2
+  in
   if err <> [] then
     raise (Error [(cxt, old_env, Type_declarations (id, decl1, decl2, err))])
 

tests/build_tests/super_errors/expected/not_undefined_functor_argument.res.expected

@@ -0,0 +1,31 @@
+
+  We've found a bug for you!
+  /.../fixtures/not_undefined_functor_argument.res:9:23-11:1
+
+   7 │ }
+   8 │ 
+   9 │ module Applied = Make({
+  10 │   type t = option<int>
+  11 │ })
+  12 │ 
+
+  Signature mismatch:
+  Modules do not match:
+    {
+  type t = option<int>
+}
+  is not included in
+    {
+  type t
+}
+  Type declarations do not match:
+    type t = option<int>
+  is not included in
+    type t
+  /.../fixtures/not_undefined_functor_argument.res:3:19-24:
+    Expected declaration
+  /.../fixtures/not_undefined_functor_argument.res:10:3-22:
+    Actual declaration
+  Their runtime representations differ:
+  the second declaration is @notUndefined,
+  but the first declaration can hold undefined.

tests/build_tests/super_errors/fixtures/not_undefined_functor_argument.res

@@ -0,0 +1,11 @@
+module Make = (
+  X: {
+    @notUndefined type t
+  },
+) => {
+  type u = X.t
+}
+
+module Applied = Make({
+  type t = option<int>
+})

tests/build_tests/super_errors_multi/expected/Cross_not_undefined_option_implementation.expected

@@ -0,0 +1,22 @@
+===== Hidden.res =====
+
+  We've found a bug for you!
+  /.../fixtures/Cross_not_undefined_option_implementation/Hidden.res:1:1-20
+
+  1 │ type t = option<int>
+  2 │ let none: t = None
+  3 │ 
+
+  The implementation /.../fixtures/Cross_not_undefined_option_implementation/Hidden.res
+  does not match the interface /.../fixtures/Cross_not_undefined_option_implementation/hidden.cmi:
+  Type declarations do not match:
+    type t = option<int>
+  is not included in
+    type t
+  /.../fixtures/Cross_not_undefined_option_implementation/Hidden.resi:1:15-20:
+    Expected declaration
+  /.../fixtures/Cross_not_undefined_option_implementation/Hidden.res:1:1-20:
+    Actual declaration
+  Their runtime representations differ:
+  the second declaration is @notUndefined,
+  but the first declaration can hold undefined.

tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.res

@@ -0,0 +1,2 @@
+type t = option<int>
+let none: t = None

tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.resi

@@ -0,0 +1,2 @@
+@notUndefined type t
+let none: t