GADT: superclass' type param instantiated to union type in a subclass does not infer properly

[TomasMikula]

Compiler version

3.2.2
3.3.0-RC3

Minimized code

enum Foo[A]:
  case Bar[X, Y]() extends Foo[X | Y]

def go[A](foo: Foo[A]): Unit =
  foo match
    case b: Foo.Bar[x, y] => 
      summon[(x | y) <:< A] // OK
      summon[(x | y) =:= A] // KO: Cannot prove that x | y =:= A.

Output

Cannot prove that x | y =:= A.

where:    x is a type in method go with bounds <: A
          y is a type in method go with bounds <: A

Expectation

Should compile.

[sjrd]

That does not seem to be a realistic expectation. From an abstract A, the compiler cannot know how to decompose it into x and y. It has to come up with something for x and y individually. The only thing it can know about them is that x <: A and y <: A. Asking it to "remember" that x | y must in fact be A is beyond what the type system promises. The type system does not carry around arbitrary relationships between multiple types like that. Even if it did, employing them to prove properties would require proof trees of arbitrary sizes, making the type system undecidable.

[TomasMikula]

The compiler does remember that A = (x || y) in this case:

class Context[||[_, _]]:

  enum Foo[A]:
    case Bar[X, Y]() extends Foo[X || Y]
  
  def go[A](foo: Foo[A]): Unit =
    foo match
      case b: Foo.Bar[x, y] =>
        summon[(x || y) =:= A] // OK

[sjrd]

Your || type had a left and right side, which can be extracted. Even when you have A || B || C, it is (A || B) || C, and it is distinct from A || (B || C).

| has none of those properties. Instead, it is by design associative and commutative. That means that it cannot be decomposed in a unique way.

Any treatment that relies on decomposing a union type is doomed to fail.

[TomasMikula]

The two examples (with | and ||) together show that on a concrete type (|) the compiler infers less than on an abstract type (||). At runtime, it could well be that type ||[A, B] = A | B. When the compiler does not know that, it infers more than if it knew that. This is strange because the behavior is not monotonic (more information in, less information out).

I have previously hit the problem of not inferring (X || Y) = (P || Q) from the two equations (X || Y) = A, A = (P || Q).

Is it correct to say that the compiler wants (at most) one canonical decomposition of any type variable?
Ideally, it would be the smallest one, i.e. such that any other decomposition is a sub-decomposition of the canonical one.
However, such decomposition may not exist, as is demonstrated in the previous paragraph, where after committing to A := X || Y, the other decomposition A := P || Q is not a sub-decomposition of the first one (and is thus ignored).

A := X | Y seems to not be even considered as a decomposition of A, perhaps because it is obviously not unique.

Am I getting this roughly right?

Then, since trying to get a unique decomposition is futile anyway (as demonstrated by A = X || Y, A = P || Q), why not include A = X | Y as a possible decomposition of A?

[sjrd]

P || Q is a unique decomposition of A. So is X || Y. The fact that the type system is not able to prove that P || Q =:= X || Y is a different problem. To prove it, it needs to conjure up from nowhere the relationships to A. This is not something type systems usually do. Of course, in the theory of type systems we typically want transitivity (A <: B and B <: C implies A <: C), but it is never implemented that way (in the sense that we do not conjure up B to prove A <: C). Unfortunately, due to abstract type members and their lower+upper bounds, we do not know how to implement the Scala type system in a way that enforces transitivity. This is why sometimes having better information at hand allows us to prove less.

[TomasMikula]

P || Q is a unique decomposition of A. So is X || Y.

That itself sounds like a contradiction to me 😉. But you are probably just using the word "unique" in a different way. I'm going to call it a "good enough" decomposition for now.

So P || Q is a good enough decomposition of A, while X | Y, for some reason, is not good enough. I can see that P || Q would be preferable to X | Y, at least as a heuristic that usually gives better results. But in the absence of anything better, why is X | Y not good enough? Note how there's no conjuring up intermediate variables in this case.

I am guessing the reason to not consider X | Y as good enough is that the implementation commits to the first encountered good enough decomposition, and thus using X | Y would preclude it from later using the more preferable P || Q. Is this a roughly correct statement about the implementation?

The fact that the type system is not able to prove that P || Q =:= X || Y is a different problem. To prove it, it needs to conjure up from nowhere the relationships to A.

That one is tricky (and not the point of this ticket), but my hunch is there is an algorithm to infer this without conjuring up anything.