Show existential types as $a and name their constructor (#9080)

* 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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3
Claude-Session: https://claude.ai/code/session_01Kr4cjoUi2f5VpMvE6wT9bo
Signed-off-by: Christoph Knittel <ck@cca.io>

* 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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3
Claude-Session: https://claude.ai/code/session_01Kr4cjoUi2f5VpMvE6wT9bo
Signed-off-by: Christoph Knittel <ck@cca.io>

* 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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3
Claude-Session: https://claude.ai/code/session_01Kr4cjoUi2f5VpMvE6wT9bo
Signed-off-by: Christoph Knittel <ck@cca.io>

---------

Signed-off-by: Christoph Knittel <ck@cca.io>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: cknitt

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.

compiler/ml/ctype.ml

@@ -933,19 +933,35 @@ let new_declaration newtype manifest =
     type_inlined_types = [];
   }
 
+(* 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 id =
+  Hashtbl.find_opt
+    (Domain.DLS.get existential_constructors_key)
+    (Ident.binding_time id)
+
 let instance_constructor ?in_pattern cstr =
   with_copy_session (fun () ->
       (match in_pattern with
       | None -> ()
       | 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 id = Ident.create (get_new_abstract_name name) in
+          Hashtbl.replace
+            (Domain.DLS.get existential_constructors_key)
+            (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

compiler/ml/ctype.mli

@@ -175,6 +175,10 @@ val instance_constructor :
   type_expr list * type_expr
 (* Same, for a constructor *)
 
+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
 val instance_declaration : type_declaration -> type_declaration

compiler/ml/printtyp.ml

@@ -1300,16 +1300,31 @@ let rec mismatch = function
   | [] -> None
   | _ -> assert false
 
+let escape_explanation ppf p =
+  match p with
+  | Pident id -> (
+    match Ctype.existential_constructor 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.@]"
+        (Ident.name id) 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)

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

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```" }
+}
+

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.

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.

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.

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