Semantic Diff

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

3 commits

beb423d9411b3e39f7c07cd8bed109d485f33339..pr-9080

bff79a6ee · cknitt + Claude · Oct 27, 2026, 12:44 UTC

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.

modifiedDiagnostic existential escape

type rec any = Any('a): any let get = (Any(x)) => x
diagnostic
Before
After
This has type: $Any_'aThis has type: $aBut it's expected to have type: 'aBut it's expected to have type: 'aThe type constructor $Any_'a would escape its scope $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.
2294674bd · cknitt + Claude · Oct 27, 2026, 20:25 UTC

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.

modifiedDiagnostic existentials of two constructors

type rec any = First('a): any | Second('a): any let same = (First(x), Second(y)) => x == y
diagnostic
Before
After
This has type: $aThis has type: $a1But it's being compared to something of type: $aBut it's being compared to something of type: $a
f56b61ce0 · cknitt + Claude · Oct 27, 2026, 20:38 UTC

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.