From 594ff2811c0644ae54f41bd3d9bdae2b51bbc8e4 Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Sun, 25 Oct 2026 06:54:59 +0000 Subject: [PATCH] Compare constructor representations in interfaces and coercions alike Why: An interface or a coercion accepted a tagged constructor for an `@unboxed` one: inclusion compared only the tags of tagged constructors, and the coercion check only the declared `@as` (#9038). The coercion error also said that the wrong variant was unboxed. `Variant_runtime.same_representation` compares two constructors: constant with the same literal, tagged with the same tag, or both untagged. Interface inclusion and the coercion check use it. Type declarations in messages print the `@unboxed` of an untagged constructor of a type that is not `@unboxed` itself, and an interface mismatch names the constructor that is `@unboxed` in only one declaration. The predefined `unknown`, an `@unboxed` variant, now has the untagged layout a declaration of it gets, so `@unboxed type rec t = unknown = Unknown(_): t` still agrees with it. Diagnostic added (interface with an @unboxed constructor): Example: module M: { type t = | @unboxed A(int) | B({x: int}) } = { type t = | A(int) | B({x: int}) } Before (diagnostic): none; clients read {TAG: "A", _0: 3} as B After (diagnostic): Type declarations do not match: type t = A(int) | B({x: int}) is not included in type t = @unboxed A(int) | B({x: int}) Their internal representations differ: case A is @unboxed only in the second declaration. Diagnostic added (coercion between representations): Example: type a = | @unboxed A(int) | B({x: int}) type b = | A(int) | B({x: int}) | C let x: b = (A(3): a :> b) Before (diagnostic): none; the coerced 3 matches C After (diagnostic): Type a is not a subtype of b Diagnostic modified (unboxed configurations): Example: @unboxed type x = One(bool) | Two type y = One(bool) | Two Before (diagnostic): - Variant x is not unboxed. - Variant y is unboxed. After (diagnostic): - Variant x is unboxed. - Variant y is not unboxed. Fixes #9038 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01CMkrYaktctdKc4M41WF36t Signed-off-by: Christoph Knittel --- .../per-constructor-unboxed-inclusion.fix.md | 1 + compiler/ml/ctype.ml | 12 +++--- compiler/ml/includecore.ml | 40 +++++++++++-------- compiler/ml/includecore.mli | 3 ++ compiler/ml/predef.ml | 37 ++++++++++++----- compiler/ml/printtyp.ml | 7 +++- compiler/ml/variant_coercion.ml | 6 --- compiler/ml/variant_runtime.ml | 8 ++++ compiler/ml/variant_runtime.mli | 6 +++ ...constructor_coercion_mismatch.res.expected | 10 +++++ ...onstructor_interface_mismatch.res.expected | 23 +++++++++++ ...t_to_variant_coercion_unboxed.res.expected | 4 +- ...untagged_constructor_coercion_mismatch.res | 3 ++ ...ntagged_constructor_interface_mismatch.res | 5 +++ 14 files changed, 121 insertions(+), 44 deletions(-) create mode 100644 changes/per-constructor-unboxed-inclusion.fix.md create mode 100644 tests/build_tests/super_errors/expected/untagged_constructor_coercion_mismatch.res.expected create mode 100644 tests/build_tests/super_errors/expected/untagged_constructor_interface_mismatch.res.expected create mode 100644 tests/build_tests/super_errors/fixtures/untagged_constructor_coercion_mismatch.res create mode 100644 tests/build_tests/super_errors/fixtures/untagged_constructor_interface_mismatch.res diff --git a/changes/per-constructor-unboxed-inclusion.fix.md b/changes/per-constructor-unboxed-inclusion.fix.md new file mode 100644 index 00000000000..0759ec7326e --- /dev/null +++ b/changes/per-constructor-unboxed-inclusion.fix.md @@ -0,0 +1 @@ +- Reject interfaces and coercions in which an `@unboxed` constructor meets a tagged one, and name the unboxed variant correctly in the coercion error. diff --git a/compiler/ml/ctype.ml b/compiler/ml/ctype.ml index 3d79e206612..4e01d269a6e 100644 --- a/compiler/ml/ctype.ml +++ b/compiler/ml/ctype.ml @@ -3727,9 +3727,9 @@ let rec subtype_rec env trace t1 t2 cstrs = ({Types.cd_args = Cstr_record fields2}, position2) ) -> if - Variant_coercion.variant_representation_matches - (Variant_runtime.constructor_tag layout1 position1) - (Variant_runtime.constructor_tag layout2 position2) + Variant_runtime.same_representation + (Variant_runtime.constructor_at layout1 position1) + (Variant_runtime.constructor_at layout2 position2) then let violations, tl1, tl2 = Record_coercion.check_record_fields fields1 fields2 @@ -3754,9 +3754,9 @@ let rec subtype_rec env trace t1 t2 cstrs = Some ({Types.cd_args = Cstr_tuple tl2}, position2) ) -> if - Variant_coercion.variant_representation_matches - (Variant_runtime.constructor_tag layout1 position1) - (Variant_runtime.constructor_tag layout2 position2) + Variant_runtime.same_representation + (Variant_runtime.constructor_at layout1 position1) + (Variant_runtime.constructor_at layout2 position2) then try let lst = subtype_list env trace tl1 tl2 cstrs in diff --git a/compiler/ml/includecore.ml b/compiler/ml/includecore.ml index d775bfdd747..cdfff58a34c 100644 --- a/compiler/ml/includecore.ml +++ b/compiler/ml/includecore.ml @@ -184,6 +184,9 @@ type type_mismatch = | Immediate | Tag_name | Variant_representation of Ident.t + | Constructor_unboxed of Ident.t * bool + (** The case is untagged in only one declaration; [true] means the + second *) let report_type_mismatch0 first second decl ppf err = let pr fmt = Format.fprintf ppf fmt in @@ -216,6 +219,13 @@ 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) + | Constructor_unboxed (s, b) -> + pr + "Their internal representations differ:@ case %s is @@unboxed only in %s \ + %s" + (Ident.name s) + (if b then second else first) + decl let report_type_mismatch first second decl ppf = List.iter (fun err -> @@ -265,23 +275,19 @@ and compare_variants ~loc env params1 params2 ~layout1 ~layout2 n let r = if r <> [] then r else - match Ast_untagged_variants.is_nullary_variant cd1.cd_args with - | true -> - let tag_type1 = Variant_runtime.constructor_tag layout1 (n - 1) in - let tag_type2 = Variant_runtime.constructor_tag layout2 (n - 1) in - if tag_type1 <> tag_type2 then [Variant_representation cd1.cd_id] - else [] - | false -> ( - (* A tagged case with a payload carries its tag in the object; - an untagged one is its payload, whatever its [@as] *) - match - ( Variant_runtime.constructor_at layout1 (n - 1), - Variant_runtime.constructor_at layout2 (n - 1) ) - with - | Block (Tagged {tag = tag1}), Block (Tagged {tag = tag2}) - when tag1.literal <> tag2.literal -> - [Variant_representation cd1.cd_id] - | _ -> r) + (* A tagged case with a payload carries its tag in the object; an + untagged one is its payload, whatever its [@as], also when only + some constructors are [@unboxed] *) + let case1 = Variant_runtime.constructor_at layout1 (n - 1) + and case2 = Variant_runtime.constructor_at layout2 (n - 1) in + if Variant_runtime.same_representation case1 case2 then r + else + match (case1, case2) with + | Block (Tagged _), Block (Untagged _) -> + [Constructor_unboxed (cd1.cd_id, true)] + | Block (Untagged _), Block (Tagged _) -> + [Constructor_unboxed (cd1.cd_id, false)] + | _ -> [Variant_representation cd1.cd_id] in if r <> [] then r else diff --git a/compiler/ml/includecore.mli b/compiler/ml/includecore.mli index ab6aebf6c06..c46d8bd97ec 100644 --- a/compiler/ml/includecore.mli +++ b/compiler/ml/includecore.mli @@ -38,6 +38,9 @@ type type_mismatch = | Immediate | Tag_name | Variant_representation of Ident.t + | Constructor_unboxed of Ident.t * bool + (** The case is untagged in only one declaration; [true] means the + second *) val value_descriptions : loc:Location.t -> diff --git a/compiler/ml/predef.ml b/compiler/ml/predef.ml index de6f65ee624..71048854008 100644 --- a/compiler/ml/predef.ml +++ b/compiler/ml/predef.ml @@ -340,17 +340,32 @@ let common_initial_env add_type add_extension empty_env = type_params = []; type_arity = 0; type_kind = - plain_variant - [ - { - cd_id = ident_ctor_unknown; - cd_runtime_tag = None; - cd_args = Cstr_tuple [tvar]; - cd_res = Some (type_unknown ()); - cd_loc = Location.none; - cd_attributes = []; - }; - ]; + (* An [@unboxed] variant whose only case is its payload *) + (let layout = Variant_runtime.pending_layout () in + Variant_runtime.complete_layout layout + (Variant_runtime.make_layout + ~configuration:{unboxed = true; tag_name = None} + [| + Block + (Untagged + { + tag = + {name = Ident.name ident_ctor_unknown; literal = None}; + block_type = UnknownType; + }); + |]); + Type_variant + ( [ + { + cd_id = ident_ctor_unknown; + cd_runtime_tag = None; + cd_args = Cstr_tuple [tvar]; + cd_res = Some (type_unknown ()); + cd_loc = Location.none; + cd_attributes = []; + }; + ], + layout )); type_representation = Types.Unboxed; } and decl_promise = diff --git a/compiler/ml/printtyp.ml b/compiler/ml/printtyp.ml index a271e464b41..6290e110a8e 100644 --- a/compiler/ml/printtyp.ml +++ b/compiler/ml/printtyp.ml @@ -919,7 +919,10 @@ and tree_of_constructor ?printing_context ~layout ~position cd = | Block (Untagged _) | Constant _ -> false in let repr = - if not tagged then None + if not tagged then + (* An untagged case of a type that is not [@unboxed] as a whole *) + if (Variant_runtime.configuration layout).unboxed then None + else Some "@unboxed" else let as_annotation = function | Variant_runtime.Null -> "@as(null)" @@ -1604,7 +1607,7 @@ let print_variant_configuration_issue ppf let print_unboxed_status ppf unboxed name = fprintf ppf "@ - Variant @{%s@} is @{%s@}unboxed." (Path.name name) - (if unboxed then "not " else "") + (if unboxed then "" else "not ") in print_unboxed_status ppf left_unboxed left_variant_name; print_unboxed_status ppf right_unboxed right_variant_name; diff --git a/compiler/ml/variant_coercion.ml b/compiler/ml/variant_coercion.ml index 0bd95ddbfd0..88d14822bbe 100644 --- a/compiler/ml/variant_coercion.ml +++ b/compiler/ml/variant_coercion.ml @@ -140,12 +140,6 @@ let can_try_coerce_variant_to_primitive_opt p = | None -> None | Some p -> can_try_coerce_variant_to_primitive p -let variant_representation_matches tag1 tag2 = - match (tag1, tag2) with - | None, None -> true - | Some s1, Some s2 when s1 = s2 -> true - | _ -> false - type variant_configuration_error = | Untagged of {left_is_unboxed: bool} | TagName of {left_tag: string option; right_tag: string option} diff --git a/compiler/ml/variant_runtime.ml b/compiler/ml/variant_runtime.ml index e5db19f22ae..d5e418cc3d9 100644 --- a/compiler/ml/variant_runtime.ml +++ b/compiler/ml/variant_runtime.ml @@ -184,6 +184,14 @@ let constructor_tag layout position = | Constant tag -> tag.literal | Block (Tagged {tag} | Untagged {tag}) -> tag.literal +let same_representation (case1 : constructor_case) (case2 : constructor_case) = + match (case1, case2) with + | Constant tag1, Constant tag2 -> tag1.literal = tag2.literal + | Block (Tagged {tag = tag1}), Block (Tagged {tag = tag2}) -> + tag1.literal = tag2.literal + | Block (Untagged _), Block (Untagged _) -> true + | (Constant _ | Block (Tagged _ | Untagged _)), _ -> false + let representation ({variant; position} : constructor_reference) = constructor_at (get_layout variant) position diff --git a/compiler/ml/variant_runtime.mli b/compiler/ml/variant_runtime.mli index c8555da8c61..a4c1d9bce2c 100644 --- a/compiler/ml/variant_runtime.mli +++ b/compiler/ml/variant_runtime.mli @@ -116,6 +116,12 @@ val matching_facts : layout -> matching_facts val configuration : layout -> configuration val constructor_at : layout -> int -> constructor_case val constructor_tag : layout -> int -> literal_tag option + +val same_representation : constructor_case -> constructor_case -> bool +(** Whether two constructors are represented alike at run time: both constant + with the same literal, both tagged with the same tag, or both untagged, + whose payloads are compared by their types *) + val representation : constructor_reference -> constructor_case val length : layout -> int val num_constants : layout -> int diff --git a/tests/build_tests/super_errors/expected/untagged_constructor_coercion_mismatch.res.expected b/tests/build_tests/super_errors/expected/untagged_constructor_coercion_mismatch.res.expected new file mode 100644 index 00000000000..51671dbe486 --- /dev/null +++ b/tests/build_tests/super_errors/expected/untagged_constructor_coercion_mismatch.res.expected @@ -0,0 +1,10 @@ + + We've found a bug for you! + /.../fixtures/untagged_constructor_coercion_mismatch.res:3:14-26 + + 1 │ type a = | @unboxed A(int) | B({x: int}) + 2 │ type b = A(int) | B({x: int}) | C + 3 │ let x: b = ((A(3): a) :> b) + 4 │ + + Type a is not a subtype of b \ No newline at end of file diff --git a/tests/build_tests/super_errors/expected/untagged_constructor_interface_mismatch.res.expected b/tests/build_tests/super_errors/expected/untagged_constructor_interface_mismatch.res.expected new file mode 100644 index 00000000000..51373d30844 --- /dev/null +++ b/tests/build_tests/super_errors/expected/untagged_constructor_interface_mismatch.res.expected @@ -0,0 +1,23 @@ + + We've found a bug for you! + /.../fixtures/untagged_constructor_interface_mismatch.res:3:5-5:1 + + 1 │ module M: { + 2 │ type t = | @unboxed A(int) | B({x: int}) + 3 │ } = { + 4 │  type t = A(int) | B({x: int}) + 5 │ } + 6 │ + + Signature mismatch: + ... + Type declarations do not match: + type t = A(int) | B({x: int}) + is not included in + type t = @unboxed A(int) | B({x: int}) + /.../fixtures/untagged_constructor_interface_mismatch.res:2:3-42: + Expected declaration + /.../fixtures/untagged_constructor_interface_mismatch.res:4:3-31: + Actual declaration + Their internal representations differ: + case A is @unboxed only in the second declaration. \ No newline at end of file diff --git a/tests/build_tests/super_errors/expected/variant_to_variant_coercion_unboxed.res.expected b/tests/build_tests/super_errors/expected/variant_to_variant_coercion_unboxed.res.expected index 399af95df07..848a05c80c0 100644 --- a/tests/build_tests/super_errors/expected/variant_to_variant_coercion_unboxed.res.expected +++ b/tests/build_tests/super_errors/expected/variant_to_variant_coercion_unboxed.res.expected @@ -10,7 +10,7 @@ Type x is not a subtype of y The variants have different @unboxed configurations. - - Variant x is not unboxed. - - Variant y is unboxed. + - Variant x is unboxed. + - Variant y is not unboxed. Fix this by making sure the variants either both have, or don't have, the @unboxed attribute. \ No newline at end of file diff --git a/tests/build_tests/super_errors/fixtures/untagged_constructor_coercion_mismatch.res b/tests/build_tests/super_errors/fixtures/untagged_constructor_coercion_mismatch.res new file mode 100644 index 00000000000..483f63a1e51 --- /dev/null +++ b/tests/build_tests/super_errors/fixtures/untagged_constructor_coercion_mismatch.res @@ -0,0 +1,3 @@ +type a = | @unboxed A(int) | B({x: int}) +type b = A(int) | B({x: int}) | C +let x: b = ((A(3): a) :> b) diff --git a/tests/build_tests/super_errors/fixtures/untagged_constructor_interface_mismatch.res b/tests/build_tests/super_errors/fixtures/untagged_constructor_interface_mismatch.res new file mode 100644 index 00000000000..1cd995328c2 --- /dev/null +++ b/tests/build_tests/super_errors/fixtures/untagged_constructor_interface_mismatch.res @@ -0,0 +1,5 @@ +module M: { + type t = | @unboxed A(int) | B({x: int}) +} = { + type t = A(int) | B({x: int}) +}