Patterns and GADTs (was: Reviewing feedback on patterns in switch)

[Brian Goetz]

> 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.”