From 5aa9c7ab0a140e66dd4a76e46d47d7b65e334b50 Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Tue, 27 Oct 2026 12:44:30 +0000 Subject: [PATCH 1/3] Show existential types as $a and name their constructor Why: An existential type of a GADT constructor is an abstract type named `$Any_'a` internally, and that name was printed as is in errors and hover. It is now printed `$a`, as in OCaml 5, and the escape error says which constructor binds it instead of calling it a type constructor. Diagnostic modified (existential escape): Example: type rec any = Any('a): any let get = (Any(x)) => x Before (diagnostic): This has type: $Any_'a But it's expected to have type: 'a The type constructor $Any_'a would escape its scope After (diagnostic): This has type: $a But it's expected to have type: 'a $a is an existential type bound by the constructor Any. It is only known in the scope of the pattern that matches Any. Review: Why decode the name instead of recording the constructor? The name already holds both parts, so printing needs no table that would have to be reset between compilations in one process. Fixes: #9068 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3 Claude-Session: https://claude.ai/code/session_01Kr4cjoUi2f5VpMvE6wT9bo Signed-off-by: Christoph Knittel --- changes/existential-type-names.polish.md | 1 + compiler/ml/printtyp.ml | 41 ++++++++++++++++--- .../tests/src/HoverExistential.res | 4 ++ .../src/expected/HoverExistential.res.txt | 5 +++ .../gadt_existential_escape.res.expected | 13 ++++++ .../fixtures/gadt_existential_escape.res | 3 ++ 6 files changed, 62 insertions(+), 5 deletions(-) create mode 100644 changes/existential-type-names.polish.md create mode 100644 tests/analysis_tests/tests/src/HoverExistential.res create mode 100644 tests/analysis_tests/tests/src/expected/HoverExistential.res.txt create mode 100644 tests/build_tests/super_errors/expected/gadt_existential_escape.res.expected create mode 100644 tests/build_tests/super_errors/fixtures/gadt_existential_escape.res diff --git a/changes/existential-type-names.polish.md b/changes/existential-type-names.polish.md new file mode 100644 index 0000000000..404d67ce55 --- /dev/null +++ b/changes/existential-type-names.polish.md @@ -0,0 +1 @@ +- Existential types of GADT constructors are shown as `$a` instead of `$Any_'a`, and an escaping one is explained by naming the constructor that binds it. diff --git a/compiler/ml/printtyp.ml b/compiler/ml/printtyp.ml index 69e77c2d17..7fa89140ab 100644 --- a/compiler/ml/printtyp.ml +++ b/compiler/ml/printtyp.ml @@ -41,8 +41,24 @@ let rec longident ppf = function let unique_names_key = Request_local.new_key (fun () -> ref Ident.empty) let unique_names () = Domain.DLS.get unique_names_key +(* [Ctype.instance_constructor] names the existential type of variable ['a] + of constructor [C] [$C_'a], followed by a number when the name is taken. + It is printed [$a], and [C] is named in the escape explanation. *) +let existential_of_name name = + match String.rindex_opt name '\'' with + | Some i when i >= 3 && name.[0] = '$' && name.[i - 1] = '_' -> + let constructor = String.sub name 1 (i - 2) in + let var = String.sub name (i + 1) (String.length name - i - 1) in + Some ("$" ^ var, constructor) + | _ -> None + let ident_name id = - try Ident.find_same id !(unique_names ()) with Not_found -> Ident.name id + try Ident.find_same id !(unique_names ()) + with Not_found -> ( + let name = Ident.name id in + match existential_of_name name with + | Some (display, _) -> display + | None -> name) let add_unique id = try ignore (Ident.find_same id !(unique_names ())) @@ -1300,16 +1316,31 @@ let rec mismatch = function | [] -> None | _ -> assert false +let escape_explanation ppf p = + match p with + | Pident id -> ( + match existential_of_name (Ident.name id) with + | Some (display, constructor) -> + fprintf ppf + "@,\ + @[%s is an existential type bound by the constructor %s.@ It is only \ + known in the scope of the pattern that matches %s.@]" + display constructor constructor + | None -> + fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]" + path p) + | _ -> + fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]" + path p + let explanation unif t3 t4 ppf = match (t3.desc, t4.desc) with | Ttuple [], Tvar _ | Tvar _, Ttuple [] -> fprintf ppf "@,Self type cannot escape its class" | Tconstr (p, _, _), Tvar _ when unif && t4.level < Path.binding_time p -> - fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]" - path p + escape_explanation ppf p | Tvar _, Tconstr (p, _, _) when unif && t3.level < Path.binding_time p -> - fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]" - path p + escape_explanation ppf p | Tvar _, Tunivar _ | Tunivar _, Tvar _ -> fprintf ppf "@,The universal variable %a would escape its scope" type_expr (if is_Tunivar t3 then t3 else t4) diff --git a/tests/analysis_tests/tests/src/HoverExistential.res b/tests/analysis_tests/tests/src/HoverExistential.res new file mode 100644 index 0000000000..6dc948f566 --- /dev/null +++ b/tests/analysis_tests/tests/src/HoverExistential.res @@ -0,0 +1,4 @@ +type rec any = Any(array<'a>, 'a => string): any + +let showAll = (Any(xs, f)) => xs->Array.map(f) +// ^hov diff --git a/tests/analysis_tests/tests/src/expected/HoverExistential.res.txt b/tests/analysis_tests/tests/src/expected/HoverExistential.res.txt new file mode 100644 index 0000000000..43bf2c3f90 --- /dev/null +++ b/tests/analysis_tests/tests/src/expected/HoverExistential.res.txt @@ -0,0 +1,5 @@ +Hover src/HoverExistential.res 2:19 +{ + "contents": { "kind": "markdown", "value": "```rescript\narray<$a>\n```" } +} + diff --git a/tests/build_tests/super_errors/expected/gadt_existential_escape.res.expected b/tests/build_tests/super_errors/expected/gadt_existential_escape.res.expected new file mode 100644 index 0000000000..3544ede550 --- /dev/null +++ b/tests/build_tests/super_errors/expected/gadt_existential_escape.res.expected @@ -0,0 +1,13 @@ + + We've found a bug for you! + /.../fixtures/gadt_existential_escape.res:3:23 + + 1 │ type rec any = Any('a): any + 2 │ + 3 │ let get = (Any(x)) => x + 4 │ + + This has type: $a + But it's expected to have type: 'a + $a is an existential type bound by the constructor Any. + It is only known in the scope of the pattern that matches Any. \ No newline at end of file diff --git a/tests/build_tests/super_errors/fixtures/gadt_existential_escape.res b/tests/build_tests/super_errors/fixtures/gadt_existential_escape.res new file mode 100644 index 0000000000..528133f82a --- /dev/null +++ b/tests/build_tests/super_errors/fixtures/gadt_existential_escape.res @@ -0,0 +1,3 @@ +type rec any = Any('a): any + +let get = (Any(x)) => x From 30a1a6a08f51e5bd6357fa72ca6141e3d17938e6 Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Tue, 27 Oct 2026 20:25:19 +0000 Subject: [PATCH 2/3] Give distinct existential types distinct names Codex review on #9080: printing `$C_'a` as `$a` made existentials of different constructors that bind the same variable print alike, so a mismatch between them read `$a` vs `$a`. Existentials are now named `$a` before the compiler makes the name unique, as OCaml 5 does, so the second one is `$a1`; the constructor binding each name is recorded for the escape explanation instead of being decoded from the name. Diagnostic modified (existentials of two constructors): Example: type rec any = First('a): any | Second('a): any let same = (First(x), Second(y)) => x == y Before (diagnostic): This has type: $a But it's being compared to something of type: $a After (diagnostic): This has type: $a1 But it's being compared to something of type: $a Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3 Claude-Session: https://claude.ai/code/session_01Kr4cjoUi2f5VpMvE6wT9bo Signed-off-by: Christoph Knittel --- compiler/ml/ctype.ml | 17 +++++++++++-- compiler/ml/ctype.mli | 4 ++++ compiler/ml/printtyp.ml | 24 ++++--------------- .../gadt_existential_same_name.res.expected | 13 ++++++++++ .../fixtures/gadt_existential_same_name.res | 3 +++ 5 files changed, 39 insertions(+), 22 deletions(-) create mode 100644 tests/build_tests/super_errors/expected/gadt_existential_same_name.res.expected create mode 100644 tests/build_tests/super_errors/fixtures/gadt_existential_same_name.res diff --git a/compiler/ml/ctype.ml b/compiler/ml/ctype.ml index b1326f398a..08d370a64f 100644 --- a/compiler/ml/ctype.ml +++ b/compiler/ml/ctype.ml @@ -932,6 +932,13 @@ let new_declaration newtype manifest = type_inlined_types = []; } +(* The constructor binding each existential type named by + [instance_constructor], for explaining an escaping one. *) +let existential_constructors_key = + Request_local.new_key (fun () -> Hashtbl.create 8) +let existential_constructor name = + Hashtbl.find_opt (Domain.DLS.get existential_constructors_key) name + let instance_constructor ?in_pattern cstr = with_copy_session (fun () -> (match in_pattern with @@ -939,12 +946,18 @@ let instance_constructor ?in_pattern cstr = | Some (env, newtype_lev) -> let process existential = let decl = new_declaration (Some (newtype_lev, newtype_lev)) None in + (* [$a] for the variable ['a], numbered when the name is taken, + so that distinct existentials print differently *) let name = match repr existential with - | {desc = Tvar (Some name)} -> "$" ^ cstr.cstr_name ^ "_'" ^ name + | {desc = Tvar (Some name)} -> "$" ^ name | _ -> "$" ^ cstr.cstr_name in - let path = Path.Pident (Ident.create (get_new_abstract_name name)) in + let name = get_new_abstract_name name in + Hashtbl.replace + (Domain.DLS.get existential_constructors_key) + name cstr.cstr_name; + let path = Path.Pident (Ident.create name) in let new_env = Env.add_local_type path decl !env in env := new_env; let to_unify = newty (Tconstr (path, [], ref Mnil)) in diff --git a/compiler/ml/ctype.mli b/compiler/ml/ctype.mli index 09bea4bbb9..4ee62e7952 100644 --- a/compiler/ml/ctype.mli +++ b/compiler/ml/ctype.mli @@ -172,6 +172,10 @@ val instance_constructor : type_expr list * type_expr (* Same, for a constructor *) +val existential_constructor : string -> string option +(* The constructor that binds the existential type of this name, given to it + by [instance_constructor] in the current request *) + val instance_parameterized_type : ?keep_names:bool -> type_expr list -> type_expr -> type_expr list * type_expr val instance_declaration : type_declaration -> type_declaration diff --git a/compiler/ml/printtyp.ml b/compiler/ml/printtyp.ml index 7fa89140ab..55d9b88aee 100644 --- a/compiler/ml/printtyp.ml +++ b/compiler/ml/printtyp.ml @@ -41,24 +41,8 @@ let rec longident ppf = function let unique_names_key = Request_local.new_key (fun () -> ref Ident.empty) let unique_names () = Domain.DLS.get unique_names_key -(* [Ctype.instance_constructor] names the existential type of variable ['a] - of constructor [C] [$C_'a], followed by a number when the name is taken. - It is printed [$a], and [C] is named in the escape explanation. *) -let existential_of_name name = - match String.rindex_opt name '\'' with - | Some i when i >= 3 && name.[0] = '$' && name.[i - 1] = '_' -> - let constructor = String.sub name 1 (i - 2) in - let var = String.sub name (i + 1) (String.length name - i - 1) in - Some ("$" ^ var, constructor) - | _ -> None - let ident_name id = - try Ident.find_same id !(unique_names ()) - with Not_found -> ( - let name = Ident.name id in - match existential_of_name name with - | Some (display, _) -> display - | None -> name) + try Ident.find_same id !(unique_names ()) with Not_found -> Ident.name id let add_unique id = try ignore (Ident.find_same id !(unique_names ())) @@ -1319,13 +1303,13 @@ let rec mismatch = function let escape_explanation ppf p = match p with | Pident id -> ( - match existential_of_name (Ident.name id) with - | Some (display, constructor) -> + match Ctype.existential_constructor (Ident.name id) with + | Some constructor -> fprintf ppf "@,\ @[%s is an existential type bound by the constructor %s.@ It is only \ known in the scope of the pattern that matches %s.@]" - display constructor constructor + (Ident.name id) constructor constructor | None -> fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]" path p) diff --git a/tests/build_tests/super_errors/expected/gadt_existential_same_name.res.expected b/tests/build_tests/super_errors/expected/gadt_existential_same_name.res.expected new file mode 100644 index 0000000000..8fdf7ec2ea --- /dev/null +++ b/tests/build_tests/super_errors/expected/gadt_existential_same_name.res.expected @@ -0,0 +1,13 @@ + + We've found a bug for you! + /.../fixtures/gadt_existential_same_name.res:3:42 + + 1 │ type rec any = First('a): any | Second('a): any + 2 │ + 3 │ let same = (First(x), Second(y)) => x == y + 4 │ + + This has type: $a1 + But it's being compared to something of type: $a + + You can only compare things of the same type. \ No newline at end of file diff --git a/tests/build_tests/super_errors/fixtures/gadt_existential_same_name.res b/tests/build_tests/super_errors/fixtures/gadt_existential_same_name.res new file mode 100644 index 0000000000..cb7f210c45 --- /dev/null +++ b/tests/build_tests/super_errors/fixtures/gadt_existential_same_name.res @@ -0,0 +1,3 @@ +type rec any = First('a): any | Second('a): any + +let same = (First(x), Second(y)) => x == y From 139986ddcc0267e571e24219fa64bc15c54bb83f Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Tue, 27 Oct 2026 20:38:34 +0000 Subject: [PATCH 3/3] Key existential constructors by identifier Codex review on #9080: the constructor of each existential was recorded by its name, but the counter that makes names unique is reset for each binding, so a nested module's `$a` could overwrite the constructor of an outer `$a`. It is recorded by the identifier's stamp now. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3 Claude-Session: https://claude.ai/code/session_01Kr4cjoUi2f5VpMvE6wT9bo Signed-off-by: Christoph Knittel --- compiler/ml/ctype.ml | 17 ++++++++++------- compiler/ml/ctype.mli | 6 +++--- compiler/ml/printtyp.ml | 2 +- ...gadt_existential_nested_binding.res.expected | 14 ++++++++++++++ .../gadt_existential_nested_binding.res | 14 ++++++++++++++ 5 files changed, 42 insertions(+), 11 deletions(-) create mode 100644 tests/build_tests/super_errors/expected/gadt_existential_nested_binding.res.expected create mode 100644 tests/build_tests/super_errors/fixtures/gadt_existential_nested_binding.res diff --git a/compiler/ml/ctype.ml b/compiler/ml/ctype.ml index 08d370a64f..0882f2c328 100644 --- a/compiler/ml/ctype.ml +++ b/compiler/ml/ctype.ml @@ -932,12 +932,15 @@ let new_declaration newtype manifest = type_inlined_types = []; } -(* The constructor binding each existential type named by - [instance_constructor], for explaining an escaping one. *) +(* The constructor binding each existential type created by + [instance_constructor], by the stamp of its identifier, for explaining an + escaping one. Names are not unique: their counter is reset per binding. *) let existential_constructors_key = Request_local.new_key (fun () -> Hashtbl.create 8) -let existential_constructor name = - Hashtbl.find_opt (Domain.DLS.get existential_constructors_key) name +let existential_constructor id = + Hashtbl.find_opt + (Domain.DLS.get existential_constructors_key) + (Ident.binding_time id) let instance_constructor ?in_pattern cstr = with_copy_session (fun () -> @@ -953,11 +956,11 @@ let instance_constructor ?in_pattern cstr = | {desc = Tvar (Some name)} -> "$" ^ name | _ -> "$" ^ cstr.cstr_name in - let name = get_new_abstract_name name in + let id = Ident.create (get_new_abstract_name name) in Hashtbl.replace (Domain.DLS.get existential_constructors_key) - name cstr.cstr_name; - let path = Path.Pident (Ident.create name) in + (Ident.binding_time id) cstr.cstr_name; + let path = Path.Pident id in let new_env = Env.add_local_type path decl !env in env := new_env; let to_unify = newty (Tconstr (path, [], ref Mnil)) in diff --git a/compiler/ml/ctype.mli b/compiler/ml/ctype.mli index 4ee62e7952..98334b37dc 100644 --- a/compiler/ml/ctype.mli +++ b/compiler/ml/ctype.mli @@ -172,9 +172,9 @@ val instance_constructor : type_expr list * type_expr (* Same, for a constructor *) -val existential_constructor : string -> string option -(* The constructor that binds the existential type of this name, given to it - by [instance_constructor] in the current request *) +val existential_constructor : Ident.t -> string option +(* The constructor that binds this existential type, created by + [instance_constructor] in the current request *) val instance_parameterized_type : ?keep_names:bool -> type_expr list -> type_expr -> type_expr list * type_expr diff --git a/compiler/ml/printtyp.ml b/compiler/ml/printtyp.ml index 55d9b88aee..5e4e891cfb 100644 --- a/compiler/ml/printtyp.ml +++ b/compiler/ml/printtyp.ml @@ -1303,7 +1303,7 @@ let rec mismatch = function let escape_explanation ppf p = match p with | Pident id -> ( - match Ctype.existential_constructor (Ident.name id) with + match Ctype.existential_constructor id with | Some constructor -> fprintf ppf "@,\ diff --git a/tests/build_tests/super_errors/expected/gadt_existential_nested_binding.res.expected b/tests/build_tests/super_errors/expected/gadt_existential_nested_binding.res.expected new file mode 100644 index 0000000000..57e1e2bee7 --- /dev/null +++ b/tests/build_tests/super_errors/expected/gadt_existential_nested_binding.res.expected @@ -0,0 +1,14 @@ + + We've found a bug for you! + /.../fixtures/gadt_existential_nested_binding.res:12:5 + + 10 ┆ } + 11 ┆ } + 12 ┆ x + 13 ┆ | Second(_) => assert(false) + 14 ┆ } + + This has type: $a + But it's expected to have type: 'a + $a is an existential type bound by the constructor First. + It is only known in the scope of the pattern that matches First. \ No newline at end of file diff --git a/tests/build_tests/super_errors/fixtures/gadt_existential_nested_binding.res b/tests/build_tests/super_errors/fixtures/gadt_existential_nested_binding.res new file mode 100644 index 0000000000..159a4c84ee --- /dev/null +++ b/tests/build_tests/super_errors/fixtures/gadt_existential_nested_binding.res @@ -0,0 +1,14 @@ +type rec any = First('a): any | Second('a): any + +let get = (v, w) => + switch v { + | First(x) => + module M = { + let inner = switch w { + | Second(y) => ignore(y) + | First(_) => () + } + } + x + | Second(_) => assert(false) + }