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

[Remi Forax]

----- Original Message -----
> From: "Brian Goetz" <brian.goetz at oracle.com>
> To: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Sent: Tuesday, January 25, 2022 8:49:08 PM
> Subject: Patterns and GADTs (was: Reviewing feedback on patterns in switch)

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

I agree that we should do something to support GADTs

The instanceof example is not a source backward compatible change, remember that instanceof is not a preview feature.

The main objection to that is that we do not have flow scoping for local variables but we have it for type variables which is weird.
I wonder if we can come with an explicit syntax for it, the same way instanceof String s is an explicit syntax for local variables.

By example, something like
  return switch (n) {
    case A<T> n -> n.t;
    case B n -> n.s as T=String;
  };

but maybe it's too much ceremony.

regards,
Rémi