Keep numbered existential names distinct from other existential names

Why:
    A numbered name can equal the base name of another existential, as
    $a1 for the second 'a and for 'a1, and the printer then falls back to
    internal name/stamp names. Names already given in the binding are
    now skipped.

Diagnostic modified (comparing existentials):
Example:
    type rec a2 = A2('a): a2
    type rec a1 = A1('a1): a1
    type rec a3 = A3('a): a3
    let f = (A2(y), A1(x), A3(z)) => z == x
Before (text):
    This has type: \"$a1/1011"
    But it's being compared to something of type: \"$a1/1013"
After (text):
    This has type: $a1
    But it's being compared to something of type: $a2

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kbf3gGhHjzBTXqSo8Dckpb
Signed-off-by: Christoph Knittel <ck@cca.io>

Author: cknitt

compiler/ml/ctype.ml

@@ -901,20 +901,33 @@ let instance_list env schl =
       let env = gadt_env env in
       List.map (fun t -> copy ?env t) schl)
 
-let reified_var_counter_key = Request_local.new_key (fun () -> ref Vars.empty)
+(* The next index for each base name, and the names already given *)
+let reified_var_counter_key =
+  Request_local.new_key (fun () -> ref (Vars.empty, Misc.String_set.empty))
 let reified_var_counter () = Domain.DLS.get reified_var_counter_key
-let reset_reified_var_counter () = reified_var_counter () := Vars.empty
+let reset_reified_var_counter () =
+  reified_var_counter () := (Vars.empty, Misc.String_set.empty)
 
 (* names given to new type constructors.
    Used for existential types and
-   local constraints *)
+   local constraints. A numbered name can equal a base name ending in
+   digits, as [$a1] for the second ['a] and the first ['a1], so names
+   already given are skipped. *)
 let get_new_abstract_name s =
-  let index =
-    try Vars.find s !(reified_var_counter ()) + 1 with Not_found -> 0
+  let counters, used = !(reified_var_counter ()) in
+  let name index =
+    if index = 0 && s <> "" && s.[String.length s - 1] <> '$' then s
+    else Printf.sprintf "%s%d" s index
   in
-  reified_var_counter () := Vars.add s index !(reified_var_counter ());
-  if index = 0 && s <> "" && s.[String.length s - 1] <> '$' then s
-  else Printf.sprintf "%s%d" s index
+  let rec first_free index =
+    if Misc.String_set.mem (name index) used then first_free (index + 1)
+    else index
+  in
+  let index = first_free (try Vars.find s counters + 1 with Not_found -> 0) in
+  let name = name index in
+  reified_var_counter () :=
+    (Vars.add s index counters, Misc.String_set.add name used);
+  name
 
 let new_declaration newtype manifest =
   {

tests/build_tests/super_errors/expected/gadt_existential_numbered_constructor.res.expected

@@ -0,0 +1,12 @@
+
+  We've found a bug for you!
+  /.../fixtures/gadt_existential_numbered_constructor.res:2:43
+
+  1 │ type rec t = Any(_): t | Any1(_): t
+  2 │ let f = (Any(x), Any(y), Any1(z)) => z == y
+  3 │ 
+
+  This has type: $Any1
+  But it's being compared to something of type: $Any11
+
+  You can only compare things of the same type.

tests/build_tests/super_errors/expected/gadt_existential_numbered_name.res.expected

@@ -0,0 +1,13 @@
+
+  We've found a bug for you!
+  /.../fixtures/gadt_existential_numbered_name.res:4:39
+
+  2 │ type rec a1 = A1('a1): a1
+  3 │ type rec a3 = A3('a): a3
+  4 │ let f = (A2(y), A1(x), A3(z)) => z == x
+  5 │ 
+
+  This has type: $a1
+  But it's being compared to something of type: $a2
+
+  You can only compare things of the same type.

tests/build_tests/super_errors/fixtures/gadt_existential_numbered_constructor.res

@@ -0,0 +1,2 @@
+type rec t = Any(_): t | Any1(_): t
+let f = (Any(x), Any(y), Any1(z)) => z == y

tests/build_tests/super_errors/fixtures/gadt_existential_numbered_name.res

@@ -0,0 +1,4 @@
+type rec a2 = A2('a): a2
+type rec a1 = A1('a1): a1
+type rec a3 = A3('a): a3
+let f = (A2(y), A1(x), A3(z)) => z == x