Match type reduction failure when applied to a type containing a bounded wildcard

[Bersier]

Compiler version

3.4.0-RC4

Minimized code

trait Foo
trait Bar[T]

type MatchType[T] = T match
  case Bar[?] => Nothing
  case _ => T

def foo(b: Bar[? >: Foo]): MatchType[b.type] = ???

def bar(b: Bar[? >: Foo]): Nothing = foo(b)

Compiler output

Found:    MatchType[(b : Bar[? >: Foo])]
Required: Nothing

Note: a match type could not be fully reduced:

  trying to reduce  MatchType[(b : Bar[? >: Foo])]
  failed since selector (b : Bar[? >: Foo])
  does not match  case Bar[_] => Nothing
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case _ => (b : Bar[? >: Foo])

Expectation

No compile error

[sjrd]

Ah, that turns out to be an interesting one. The behavior is actually according to spec. If we look at the Matching algorithm at https://docs.scala-lang.org/sips/match-types-spec.html#matching, we can see what happens. We are trying to (b : Bar[? >: Foo <: Any]) against Bar[?]. The ? on the right is a wildcard capture, and Bar is invariant. Therefore, the following step applies:

• If P is a WildcardCapture ti = _:
  • If X is of the form _ >: L <: H, instantiate ti := H (anything between L and H would work here),

So it picks Any for the wildcard capture. Then it tests is Bar[? >: Foo <: Any] <:< Bar[Any], and the answer is false because Bar is invariant.

I don't think there is a good solution to this problem. There is nothing that the matching algorithm could pick that would work. Neither Foo nor Any, nor anything in between, will actually work here, because we have a wildcard type parameter on the left.

The real solution would be to consider ? in patterns as wildcard type args instead of wildcard captures. That would be changing the language, however.

[sjrd]

Or maybe I can make it work: main...dotty-staging:dotty:make-i19607-work ... although it still involves a (minor) change of spec.

We might need to discuss that at the next SIP meeting, to see whether we could still accommodate it. /cc @anatoliykmetyuk

[sjrd]

Perhaps we can consider this a "spec bug", since the intent of the spec was clearly to pick something that would always work (see text in parentheses), but picking hi does not actually always work. The solution I have is to pick the wildcard type argument itself.