Update unreducible match types error reporting

[EugeneFlesselle]

Match type reduction can fail for any of the following reasons:

• EmptyScrutinee: would be unsound to reduce
• Stuck: selector does not match a case and is not provably disjoint from it either
• NoInstance: selector does not uniquely determine params captures in pattern
• NoMatches: selector matches none of the cases
• LegacyPattern: match type contains an illegal case and sourceVersion >= 3.4

Out of those, only Stuck and NoInstance, could get reduced in a refined context.

Status quo

The match reducer returns:

• ErrorType for NoMatches and LegacyPattern,
• NoType, which implies the match type is left unreduced, in all other cases.

In addition, the implementation has an issue where the ErrorTypes can be left unreported, then entering the flexible type logic, thereby conforming to anything.

Proposed changes

In addition to fixing the aforementioned bug, this PR proposes to leave all unreducible match types as unreduced.
Of course the reduction may be needed at a later point for conformance, in which case the error message will still contain the same explanations from the MatchTypeTrace.

Fixes #19949
Fixes #19950

Discussion

All cases of failed match type reductions which we know will never reduce, even with refined scrutinee, should have a consistent behaviour. So NoMatches and EmptyScrutinee should either both be an error or both be left unreduced.

The current implementation attempts to do the former approach (but only for NoMatches), which has some limitations as discussed below (I'm not saying I can do better, hence the latter approach).

Undesirable errors

We dont always want an error for a NoMatches failed reduction, for example if we just need Nothing to conform to it:

trait TupleWrap[T <: Tuple]:  
  def head: Tuple.Head[T]  
  
object EmptyTupleWrap extends TupleWrap[EmptyTuple]:  
  def head = throw NoSuchElementException() // Error:
// |      ^  
// |      Match type reduction failed since selector EmptyTuple  
// |      matches none of the cases

But we could do def head: Nothing = ... to avoid the error here.

Generally speaking, places where the bounds of the match type suffice can still get a reduction error, and adding an ascription to avoid an inferred match type doesn't always do the trick.

Another refused example could be:

type Default[N <: Int] = N match  
  case 0 => 'a' | 'c'
  case 1 => 'b' | 'd'
  
def default(n: Int): Option[Default[n.type]] = n match  
  case _: (0 | 1) => Some[Default[n.type]]:  
    n match  
      case _: 0 => 'a' 
      case _: 1 => 'b'
  case _ => None  
  
default(2): Option[Char] // Error  
// |   ^  
// |   Match type reduction failed since selector (2 : Int)  
// |   matches none of the cases

even though the function looks reasonable and type-checking would be sound.

Missed errors

Also note in the EmptyTupleWrap example, we get a reduction error from a match type application which does not appear in the source code. A valid question might be when and for what exactly these conditions are checked ?

The goal is to report a type error early on for a NoMatches application right, but we are actually only doing so if we happen to do tryNormalize and end up in the MatchReducer.

Here is an example where were a match type with NoMatches is accepted

trait A:
  type X
  type R = X match
    case 0 => 'a'
    case 1 => 'b'

trait B extends A:
  type S = 2

type R1 = B#R // no error

Generally speaking, the NoMatches error can be circumvented with:

type AllowNoMatchesM[X] = {
  type X1 = X
  type R = X1 match
    case 0 => 'a'
    case 1 => 'b'
}#R
type R2 = AllowNoMatchesM[2] // no error

Also note the projections are used in the examples for simplicity but are not necessary, R can be used within B as unreduced without a reported error.

See #19799 for another example of inconsistent errors

[sjrd]

This would revert the semantics of match types to what they were a long time ago. I believe there were good reasons, based on practical experience, to report an error on reducing-to-nothing match types. That was however long before I started looking into match types. Perhaps @OlivierBlanvillain has some more concrete recollections?

In any case, this specific change would require a SIP at this point, unlike the other PR.

[EugeneFlesselle]

This would revert the semantics of match types to what they were a long time ago. I believe there were good reasons, based on practical experience, to report an error on reducing-to-nothing match types. That was however long before I started looking into match types. Perhaps @OlivierBlanvillain has some more concrete recollections?

Ah so I just found the PR #12768 which explicitly changed this.

[dwijnand]

Yeah, I think the users are reasonable in asking for this error eagerly.

[EugeneFlesselle]

For reference, I played around a bit and found the following:

With a simple case, we do get an error:

type M[X] = X match
  case 0 => 'a'
  case 1 => 'b'

type R1 = M[2] // error selector matches none of the cases

But with a setup like:

trait A:
  type X
  type R = X match
    case 0 => 'a'
    case 1 => 'b'

trait B extends A:
  type S = 2

type R2 = B#R // no error

the matches with no cases go by undetected.

Generally speaking, the rule can be circumvented with:

type AllowNoMatchesM[X] = {
  type X1 = X
  type R = X1 match
    case 0 => 'a'
    case 1 => 'b'
}#R

type R3 = AllowNoMatchesM[2] // no error

We could of course also consider this an error and try to fix it. But doing these kind of checks exhaustively seems complicated given the current implementation.

I find getting these errors in unpredictable ways worse then getting no errors at all (the second example is actually minimised from something I ran into when working with the generic tuples and was quite confused about).

[EugeneFlesselle]

Coming back to the original example (assuming the error is handled properly) #19949 (comment)

val t: T[Double] = new T[Double] {}
val x: t.M = "hello" // error

It also unclear to be reporting an error only on x but not t, despite its member M already being unreducible.

[odersky]

What is the difference between "no matches" and getting stuck?

Is "no matches" where we know that the match type cannot reduce in any refining context? In that case, I think it's reasonable to throw a type error if we know the error will be reported. I believe this can be tested with

  ctx.typeAssigner.isInstanceOf[Typer]

[odersky]

It's a pragmatic choice. The type system should not need any of this, but it is helpful to tell the user early that a match type makes no sense.

[EugeneFlesselle]

Is "no matches" where we know that the match type cannot reduce in any refining context?

Yes indeed, but it is possible for a refining context to yield a "stuck" match type, i.e. one that does not report an error.

I believe this can be tested with ctx.typeAssigner.isInstanceOf[Typer]

Ah thanks ! I found ctx.isTyper next to it which seems to be what I needed for #19953.

[odersky]

Yes indeed, but it is possible for a refining context to yield a "stuck" match type, i.e. one that does not report an error.

Can you point me towards a scenario where that happens?

[EugeneFlesselle]

Can you point me towards a scenario where that happens?

Yes, a simplistic example is:

type M[X] = X match
  case 0 => 'a'
  case 1 => 'b'

// type R1 = M[2] // error reduction failed since selector matches none of the cases

// but with a refined scrutinee:
type R2 = M[2 & 1] // no error because we do not try to reduce under an uninhabited scrutinee

In practice, this does realistically occur from outer reductions or when working with match types as members, but errors don't get reported in predictable ways: #19954 (comment)

---

I'm don't think keeping things as they are would be horrible either, just pointing out the current quirks with the design.

[odersky]

Ah, so it's because it hits the uninhabited type scrutinee! Should that also throw a TypeError then? It seems desirable that the behavior is maintained under context refinement.

[EugeneFlesselle]

Should that also throw a TypeError then? It seems desirable that the behavior is maintained under context refinement.

Yes I agree ! I'm trying that out now to see how much of the tests are impacted.
Reporting more errors now than previously might be harder to impose as a change than the inverse though.

Edit: Implemented in #19964

[odersky]

Why is bad-footprint removed? bad-footprint is an essential test. It's the only test we have that tests that match type reduction is consistent between contexts. That's the thing I have mentioned dozens of times already.

[EugeneFlesselle]

Why is bad-footprint removed? bad-footprint is an essential test. It's the only test we have that tests that match type reduction is consistent between contexts. That's the thing I have mentioned dozens of times already.

I should probably have added comment here in addition to the commit message.

Unfortunately, it used to only pass because of a missed ErrorType.
That said, yes we should definitely have this test, and it should definitely be re-enabled once #19434 is fixed.
I'm not sure how soon that will be though, and leaving the current ErrorTypes as is might lead to some more test cases passing for the wrong reasons being added.

[EugeneFlesselle]

Can we have a similar test case, but without opaque type aliases ?
It should not run into the previous issue in that case.

[EugeneFlesselle]

The PR is now based on #20017, allowing to keep bad-footprint.scala

[odersky]

Nice cleanup!