----- Original Message -----
> From: "Brian Goetz" <brian.go...@oracle.com>
> To: "amber-spec-experts" <amber-spec-experts@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
