> 3. Type refinements for GADTs There are a number of unsatisfying aspects to how we currently handle GADTs; specifically, we are missing the type refinement process outlined in "Simple unification-based type inference for GADTs” (SPJ et al, 2005). Here are some examples of where we fall down.
Suppose we have sealed interface Node<T> { } record A<T>(T t) extends Node<T> { } record B(String s) extends Node<String> { } and we want to write: <T> T unbox(Node<T> n) { return switch (n) { case A<T> n -> n.t; case B n -> n.s; } } The RHS of all the arrows must be compatible with the return type, which is T. Clearly that is true for the first case, but not for the second; the compiler doesn’t know that T has to be String if we’ve matched a Node<T> to B. What is missing is to refine the type of T based on matches. Here, we would gather an additional constraint on `case B` for T=String; if we had a case which was covariant in T: record C<T extends B>(T t) then a `case C<T>` would gather an additional constraint of T <: B for its RHS. More generally, any code dominated by a match that provides additional bounds for type variables could benefit from those bounds. For example, we’d probably want the same in: if (n instanceof B b) { /* T is String here */ } and (as with flow scoping): if (! (n instanceof B b)) throw … // T is String here We can probably piggy back the specification of this on flow scoping, appealing to “wherever a binding introduced by this pattern would be in scope.”