From 34fe539e616f0bda33a49e373fb2929a55c9f003 Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Thu, 22 Oct 2026 19:04:09 +0000 Subject: [PATCH 1/2] Check @notUndefined of an interface against the implementation Why: Interface inclusion ignored `@notUndefined`. An interface could declare `@notUndefined type t` over `type t = option`, and clients then unboxed `option`, so `Some(M.none)` was `None` (#8964). When the second declaration of an inclusion is `@notUndefined`, the first must be a type that cannot hold `undefined`, by the rule `option` unboxing uses, or an abstract type, which has no representation to contradict it. This covers `.resi` files, functor arguments and `with type` constraints. The check runs in `Includemod`, since `Typeopt` depends on `Includecore` through `Typedecl`. Diagnostic added: Example: // Hidden.resi @notUndefined type t // Hidden.res type t = option After (diagnostic): Type declarations do not match: type t = option is not included in type t Their runtime representations differ: the second declaration is @notUndefined, but the first declaration can hold undefined. Review: Why accept an abstract implementation without the attribute? The stdlib's `Lazy.res` declares `type t<+'a>` under `@notUndefined` in its interface, and so may bindings; such a type has no representation that could hold `undefined`, so requiring the attribute twice would only break them. Fixes: #8964 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Fc7LEuyEfynjaKCVEBPmTF Signed-off-by: Christoph Knittel --- changes/not-undefined-inclusion.fix.md | 1 + compiler/ml/UntaggedVariants.md | 24 +++++++++----- compiler/ml/includecore.ml | 6 ++++ compiler/ml/includecore.mli | 1 + compiler/ml/includemod.ml | 20 ++++++++++++ ...ot_undefined_functor_argument.res.expected | 31 +++++++++++++++++++ .../not_undefined_functor_argument.res | 11 +++++++ ...t_undefined_option_implementation.expected | 22 +++++++++++++ .../Hidden.res | 2 ++ .../Hidden.resi | 2 ++ 10 files changed, 113 insertions(+), 7 deletions(-) create mode 100644 changes/not-undefined-inclusion.fix.md create mode 100644 tests/build_tests/super_errors/expected/not_undefined_functor_argument.res.expected create mode 100644 tests/build_tests/super_errors/fixtures/not_undefined_functor_argument.res create mode 100644 tests/build_tests/super_errors_multi/expected/Cross_not_undefined_option_implementation.expected create mode 100644 tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.res create mode 100644 tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.resi diff --git a/changes/not-undefined-inclusion.fix.md b/changes/not-undefined-inclusion.fix.md new file mode 100644 index 0000000000..4b76474e9d --- /dev/null +++ b/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. diff --git a/compiler/ml/UntaggedVariants.md b/compiler/ml/UntaggedVariants.md index c8ad0586c9..42e9674039 100644 --- a/compiler/ml/UntaggedVariants.md +++ b/compiler/ml/UntaggedVariants.md @@ -430,16 +430,26 @@ 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` 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`; `ast_untagged_variants.ml:has_not_undefined`; `variant_layout.ml:declaration_shape`; - `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 @@ -538,8 +548,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`. diff --git a/compiler/ml/includecore.ml b/compiler/ml/includecore.ml index 635298bd37..1d5e574bba 100644 --- a/compiler/ml/includecore.ml +++ b/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" diff --git a/compiler/ml/includecore.mli b/compiler/ml/includecore.mli index 6edd3bf32b..eec47e1f2f 100644 --- a/compiler/ml/includecore.mli +++ b/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 -> diff --git a/compiler/ml/includemod.ml b/compiler/ml/includemod.ml index 890c6c97de..164e07fe28 100644 --- a/compiler/ml/includemod.ml +++ b/compiler/ml/includemod.ml @@ -62,12 +62,32 @@ 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) && decl2.type_shape = Never_undefined 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))]) diff --git a/tests/build_tests/super_errors/expected/not_undefined_functor_argument.res.expected b/tests/build_tests/super_errors/expected/not_undefined_functor_argument.res.expected new file mode 100644 index 0000000000..d3c478fff7 --- /dev/null +++ b/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 + 11 │ }) + 12 │ + + Signature mismatch: + Modules do not match: + { + type t = option +} + is not included in + { + type t +} + Type declarations do not match: + type t = option + 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. \ No newline at end of file diff --git a/tests/build_tests/super_errors/fixtures/not_undefined_functor_argument.res b/tests/build_tests/super_errors/fixtures/not_undefined_functor_argument.res new file mode 100644 index 0000000000..bd1ed144d5 --- /dev/null +++ b/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 +}) diff --git a/tests/build_tests/super_errors_multi/expected/Cross_not_undefined_option_implementation.expected b/tests/build_tests/super_errors_multi/expected/Cross_not_undefined_option_implementation.expected new file mode 100644 index 0000000000..efc27a4df3 --- /dev/null +++ b/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 + 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 + 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. \ No newline at end of file diff --git a/tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.res b/tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.res new file mode 100644 index 0000000000..5474e4e6d4 --- /dev/null +++ b/tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.res @@ -0,0 +1,2 @@ +type t = option +let none: t = None diff --git a/tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.resi b/tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.resi new file mode 100644 index 0000000000..4d843da27a --- /dev/null +++ b/tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation/Hidden.resi @@ -0,0 +1,2 @@ +@notUndefined type t +let none: t From b19d240d781f1714b3fa5d4b1900013727c3467c Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Fri, 23 Oct 2026 11:34:59 +0000 Subject: [PATCH 2/2] Accept @notUndefined over implementations the compiler cannot see into Why: The check rejected bindings that are fine: an interface's `@notUndefined type t` over `type t = Dom.element`, an abbreviation of an abstract type, or over a JavaScript object type, which is never undefined. An implementation whose representation the compiler does not see has none that contradicts the interface: an abstract type, also reached through an abbreviation, or a JavaScript object type. A functor parameter's or a locally abstract type stands for any type and does not count as abstract. Diagnostic removed (an abbreviation of an abstract type): Example: // A.resi @notUndefined type t // A.res type t = Dom.element Before (diagnostic): Their runtime representations differ: the second declaration is @notUndefined, but the first declaration can hold undefined. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01CMkrYaktctdKc4M41WF36t Signed-off-by: Christoph Knittel --- compiler/ml/UntaggedVariants.md | 10 ++++-- compiler/ml/includemod.ml | 31 ++++++++++++++----- ...t_undefined_functor_parameter.res.expected | 26 ++++++++++++++++ .../not_undefined_functor_parameter.res | 11 +++++++ .../src/not_undefined_interface_test.mjs | 26 ++++++++++++++++ .../src/not_undefined_interface_test.res | 16 ++++++++++ .../src/not_undefined_interface_test.resi | 4 +++ 7 files changed, 113 insertions(+), 11 deletions(-) create mode 100644 tests/build_tests/super_errors/expected/not_undefined_functor_parameter.res.expected create mode 100644 tests/build_tests/super_errors/fixtures/not_undefined_functor_parameter.res create mode 100644 tests/tests/src/not_undefined_interface_test.mjs create mode 100644 tests/tests/src/not_undefined_interface_test.res create mode 100644 tests/tests/src/not_undefined_interface_test.resi diff --git a/compiler/ml/UntaggedVariants.md b/compiler/ml/UntaggedVariants.md index 42e9674039..5d6919242e 100644 --- a/compiler/ml/UntaggedVariants.md +++ b/compiler/ml/UntaggedVariants.md @@ -433,8 +433,11 @@ declaration it is an error, "@notUndefined can only be used on abstract 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` under +a type that cannot hold `undefined` either, or a type whose representation +the compiler does not see, which has none to contradict it: an abstract type, +also through an abbreviation such as `type t = Dom.element`, or a JavaScript +object type. The type of a functor parameter or a locally abstract type +stands for another type and does not count as abstract. `type t = option` 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 @@ -446,7 +449,8 @@ for functor arguments and `with type` constraints. `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`; + `not_undefined_functor_argument.res`, `not_undefined_functor_parameter.res`; + `tests/tests/src/not_undefined_interface_test.res`; `tests/build_tests/super_errors_multi/fixtures/Cross_not_undefined_option_implementation`; `tests/build_tests/not_undefined_attribute`. - Shaped by #7458, #7464, #8964. diff --git a/compiler/ml/includemod.ml b/compiler/ml/includemod.ml index 164e07fe28..08d7fd4a2c 100644 --- a/compiler/ml/includemod.ml +++ b/compiler/ml/includemod.ml @@ -63,21 +63,36 @@ 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. *) + implementation must be a type that cannot hold [undefined] either. A type + whose representation the compiler does not see, an abstract type (also + through an abbreviation) or a JavaScript object type, has none that + contradicts it. A functor parameter's or a locally abstract type stands + for any type, so it does not count as abstract. *) 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) && decl2.type_shape = Never_undefined then + match decl2.type_shape with + | Unstated | Recognized_as _ -> [] + | Never_undefined -> 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 [] + let opaque = + match (Ctype.expand_head_opt env ty).desc with + | Tconstr (path, _, _) -> ( + match Env.find_type path env with + | {type_kind = Type_abstract; type_manifest = None; type_newtype_level} + -> + Predef.type_is_builtin_path_but_option path = Predef.NA + && type_newtype_level = None + && not (Env.is_functor_arg path env) + | _ -> false + | exception Not_found -> false) + | Tobject _ -> true + | _ -> false + in + if opaque || 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; diff --git a/tests/build_tests/super_errors/expected/not_undefined_functor_parameter.res.expected b/tests/build_tests/super_errors/expected/not_undefined_functor_parameter.res.expected new file mode 100644 index 0000000000..f8595c3662 --- /dev/null +++ b/tests/build_tests/super_errors/expected/not_undefined_functor_parameter.res.expected @@ -0,0 +1,26 @@ + + We've found a bug for you! + /.../fixtures/not_undefined_functor_parameter.res:8:7-10:3 + + 6 │ module Checked: { + 7 │ @notUndefined type t + 8 │ } = { + 9 │  type t = X.t + 10 │  } + 11 │ } + 12 │ + + Signature mismatch: + Modules do not match: { + type t = X.t +} is not included in { + type t +} + Type declarations do not match: type t = X.t is not included in type t + /.../fixtures/not_undefined_functor_parameter.res:7:19-24: + Expected declaration + /.../fixtures/not_undefined_functor_parameter.res:9:5-16: + Actual declaration + Their runtime representations differ: + the second declaration is @notUndefined, + but the first declaration can hold undefined. \ No newline at end of file diff --git a/tests/build_tests/super_errors/fixtures/not_undefined_functor_parameter.res b/tests/build_tests/super_errors/fixtures/not_undefined_functor_parameter.res new file mode 100644 index 0000000000..00f85f1bbf --- /dev/null +++ b/tests/build_tests/super_errors/fixtures/not_undefined_functor_parameter.res @@ -0,0 +1,11 @@ +module Make = ( + X: { + type t + }, +) => { + module Checked: { + @notUndefined type t + } = { + type t = X.t + } +} diff --git a/tests/tests/src/not_undefined_interface_test.mjs b/tests/tests/src/not_undefined_interface_test.mjs new file mode 100644 index 0000000000..6f03b6875c --- /dev/null +++ b/tests/tests/src/not_undefined_interface_test.mjs @@ -0,0 +1,26 @@ +// Generated by ReScript, PLEASE EDIT WITH CARE + +import * as Mocha from "mocha"; +import * as Test_utils from "./test_utils.mjs"; +import * as Primitive_option from "@rescript/runtime/lib/es6/Primitive_option.mjs"; + +let makeElement = (() => ({})); + +function makeRecord() { + return { + name: "a" + }; +} + +Mocha.describe("Not_undefined_interface_test", () => { + Mocha.test("option of the types is unboxed", () => { + let element = makeElement(); + Test_utils.ok("File \"not_undefined_interface_test.res\", line 14, characters 18-25", Primitive_option.some(element) === element); + }); +}); + +export { + makeElement, + makeRecord, +} +/* Not a pure module */ diff --git a/tests/tests/src/not_undefined_interface_test.res b/tests/tests/src/not_undefined_interface_test.res new file mode 100644 index 0000000000..e0359f933e --- /dev/null +++ b/tests/tests/src/not_undefined_interface_test.res @@ -0,0 +1,16 @@ +// Implementations whose representation the compiler does not see, an +// abstract type through an abbreviation and a JavaScript object type, agree +// with @notUndefined in the interface +type opaque +type element = opaque +type record = {"name": string} + +let makeElement: unit => element = %raw(`() => ({})`) +let makeRecord = () => {"name": "a"} + +Mocha.describe(__MODULE__, () => { + Mocha.test("option of the types is unboxed", () => { + let element = makeElement() + Test_utils.ok(__LOC__, Obj.magic(Some(element)) === element) + }) +}) diff --git a/tests/tests/src/not_undefined_interface_test.resi b/tests/tests/src/not_undefined_interface_test.resi new file mode 100644 index 0000000000..2fe3908cd4 --- /dev/null +++ b/tests/tests/src/not_undefined_interface_test.resi @@ -0,0 +1,4 @@ +@notUndefined type element +@notUndefined type record +let makeElement: unit => element +let makeRecord: unit => record