Existentials and GADTs

Existentials hide which witness was chosen while preserving operations valid for that witness. GADTs reveal type-index information when a constructor is matched. Both rely on scoped dependent reasoning rather than unchecked casts.

Introducing an existential

type Showable = exists (a:Type).
    { value:a, display:a -> String };

value item : Showable =
    { value = 42, display = showInt };

There is no pack keyword. The expected existential type guides witness inference. Add a more specific annotation when the witness is ambiguous.

Eliminating an existential

unpack item as (a, package) in
    package.display(package.value)

Inside the body, a is a fresh rigid type and package has fields at that witness. The result may not mention a, and a value whose type mentions a cannot escape. This skolem/escape rule is what makes the abstraction safe.

Field access may implicitly open a package only when the complete expression can satisfy the same rule. unpack is the clear canonical form.

GADT result refinement

type Vec(a:Type,n:Nat) =
    VNil : Vec(a,Z)
  + VCons * head:a * tail:Vec(a,n) : Vec(a,Succ(n));

Each constructor states a more precise result index. Matching VNil refines the length to Z; matching VCons exposes a predecessor. The checker uses these equalities within the corresponding branch only.

Why annotations sometimes help

Existential introduction works backward from an expected type, while GADT elimination refines forward from a constructor. At boundaries where neither direction supplies enough information, an expression annotation makes the intended witness or index explicit without performing a cast.

Runtime behavior

Type witnesses may erase when irrelevant, but retained values and operations still compile normally. The native reference path has source-level acceptance and representative execution coverage for existential packages and GADT refinement; higher-kinded runtime passage and some very general dependent paths remain tracked implementation work.

Common mistakes

There is no pack form, and an unpacked witness cannot escape its lexical scope. GADT refinements are branch-local; do not reuse one constructor’s index fact in a sibling branch.

Recap

Existentials hide a witness while preserving valid operations. GADT matching does the complementary job of revealing index facts for exactly one branch.

Normative details: Language Reference §5.6 and §6.