Skip to content

Commit 4bc3193

Browse files
cknittclaude
andcommitted
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 Signed-off-by: Christoph Knittel <ck@cca.io>
1 parent cd641cb commit 4bc3193

6 files changed

Lines changed: 62 additions & 5 deletions

File tree

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
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/printtyp.ml‎

Lines changed: 36 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -41,8 +41,24 @@ let rec longident ppf = function
4141
let unique_names_key = Request_local.new_key (fun () -> ref Ident.empty)
4242
let unique_names () = Domain.DLS.get unique_names_key
4343

44+
(* [Ctype.instance_constructor] names the existential type of variable ['a]
45+
of constructor [C] [$C_'a], followed by a number when the name is taken.
46+
It is printed [$a], and [C] is named in the escape explanation. *)
47+
let existential_of_name name =
48+
match String.rindex_opt name '\'' with
49+
| Some i when i >= 3 && name.[0] = '$' && name.[i - 1] = '_' ->
50+
let constructor = String.sub name 1 (i - 2) in
51+
let var = String.sub name (i + 1) (String.length name - i - 1) in
52+
Some ("$" ^ var, constructor)
53+
| _ -> None
54+
4455
let ident_name id =
45-
try Ident.find_same id !(unique_names ()) with Not_found -> Ident.name id
56+
try Ident.find_same id !(unique_names ())
57+
with Not_found -> (
58+
let name = Ident.name id in
59+
match existential_of_name name with
60+
| Some (display, _) -> display
61+
| None -> name)
4662

4763
let add_unique id =
4864
try ignore (Ident.find_same id !(unique_names ()))
@@ -1299,16 +1315,31 @@ let rec mismatch = function
12991315
| [] -> None
13001316
| _ -> assert false
13011317

1318+
let escape_explanation ppf p =
1319+
match p with
1320+
| Pident id -> (
1321+
match existential_of_name (Ident.name id) with
1322+
| Some (display, constructor) ->
1323+
fprintf ppf
1324+
"@,\
1325+
@[%s is an existential type bound by the constructor %s.@ It is only \
1326+
known in the scope of the pattern that matches %s.@]"
1327+
display constructor constructor
1328+
| None ->
1329+
fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
1330+
path p)
1331+
| _ ->
1332+
fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
1333+
path p
1334+
13021335
let explanation unif t3 t4 ppf =
13031336
match (t3.desc, t4.desc) with
13041337
| Ttuple [], Tvar _ | Tvar _, Ttuple [] ->
13051338
fprintf ppf "@,Self type cannot escape its class"
13061339
| Tconstr (p, _, _), Tvar _ when unif && t4.level < Path.binding_time p ->
1307-
fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
1308-
path p
1340+
escape_explanation ppf p
13091341
| Tvar _, Tconstr (p, _, _) when unif && t3.level < Path.binding_time p ->
1310-
fprintf ppf "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
1311-
path p
1342+
escape_explanation ppf p
13121343
| Tvar _, Tunivar _ | Tunivar _, Tvar _ ->
13131344
fprintf ppf "@,The universal variable %a would escape its scope" type_expr
13141345
(if is_Tunivar t3 then t3 else t4)
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
type rec any = Any(array<'a>, 'a => string): any
2+
3+
let showAll = (Any(xs, f)) => xs->Array.map(f)
4+
// ^hov
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
Hover src/HoverExistential.res 2:19
2+
{
3+
"contents": { "kind": "markdown", "value": "```rescript\narray<$a>\n```" }
4+
}
5+
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
2+
We've found a bug for you!
3+
/.../fixtures/gadt_existential_escape.res:3:23
4+
5+
1 │ type rec any = Any('a): any
6+
2 │
7+
3 │ let get = (Any(x)) => x
8+
4 │
9+
10+
This has type: $a
11+
But it's expected to have type: 'a
12+
$a is an existential type bound by the constructor Any.
13+
It is only known in the scope of the pattern that matches Any.
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
type rec any = Any('a): any
2+
3+
let get = (Any(x)) => x

0 commit comments

Comments
 (0)