GADT and type variable specialization during inference

[Remi Forax]

Moved to amber-spec-experts,

I've got a very similar issue, if we support patter matching on Class.

  public Stream<T> createPrimitiveStrem(Class<T> type) {
    return switch(type) {
      case int.class -> new SpecializedStream<Integer>();
      case double.class -> new SpecializedStream<Double>();
      ...
    };
  }

A cast and a pinky swear @SuppressWarnings("unchecked") solve the issue but we may do better.

Rémi

----- Original Message -----
> From: "Brian Goetz" <brian.goetz at oracle.com>
> To: "Jan Lahoda" <jlahoda at openjdk.java.net>, "amber-dev" <amber-dev at openjdk.java.net>
> Sent: Lundi 8 Novembre 2021 21:37:24
> Subject: Re: RFR: 8273328: Compiler implementation for Pattern Matching for switch (Second Preview)

> This is more of a spec issue than a compiler issue.  I finally got
> around to running some of my favorite GADT examples on this.
> 
> I started with this Haskell type:
> 
>     data Term t where
>         Lit :: t -> Term t
>         Succ :: Term Int -> Term Int
>         IsZero :: Term Int -> Term Bool
>         If :: Term Bool -> Term a -> Term a -> Term a
> 
> I can map it to this Java hierarchy:
> 
>     sealed interface Term<T> { }
> 
>     record Lit<T>(T val) implements Term<T> { }
>     record Succ(Term<Integer> a) implements Term<Integer> { }
>     record IsZero(Term<Integer> a) implements Term<Boolean> { }
>     record If<T>(Term<Boolean> cond, Term<T> a, Term<T> b) implements
> Term<T> { }
> 
> We correctly eliminate the impossible cases in:
> 
>     String foo(Term<String> t) {
>         return switch (t) {
>             case Lit<String> -> "Lit";
>             case If<String> -> "If";
>         }
>     }
> 
> And the compiler correctly tells me that the switch is exhaustive.  But
> if I try to write an evaluator:
> 
>     static<T> T eval(Term<T> term) {
>         return switch (term) {
>         case Lit<T> t -> t.val;
>         case Succ t -> eval(t.a) + 1;
>         case IsZero t -> eval(t.a) == 0;
>         case If<T> t -> eval(t.cond) ? eval(t.a) : eval(t.b);
>         };
>     }
> 
> 
> I get errors on the Succ and IsZero cases.  In Haskell, the equivalent:
> 
>     eval :: Term t -> t
>     eval (Lit t) = t
>     eval (Succ i) = (eval i) + 1
>     ...
> 
> works correctly because when we match on `eval (Succ i)`, we unify t
> with Int, since that's the only instantiation for t that would work in
> this case.  That's what allows us to return an Int when we're expecting
> a t, because we've already figured out they are the same.
> 
> So in order to make our eval work, we would have to know to _refine_ the
> bounds of T on the RHS of
> 
>         case Succ t -> eval(t.a) + 1;
> 
> where we would say "Succ is Term<T>, and Succ extends Term<Integer>, so
> T=Integer here".
> 
> In the absence of this, I have to do an explicit boxing plus an
> unchecked cast:
> 
>     static<T> T eval(Term<T> term) {
>         return switch (term) {
>         case Lit<T> t -> t.val;
>         case Succ t -> (T) (Integer) (eval(t.a) + 1);
>         case IsZero t -> (T) (Boolean) (eval(t.a) == 0);
>         case If<T> t -> eval(t.cond) ? eval(t.a) : eval(t.b);
>         };
>     }
> 
> That we need both the boxing and the T cast is probably a bug.
>