Unsound conformance from selection of member MatchType #19949
Comments
EugeneFlesselle
added
itype:bug
stat:needs triage
EugeneFlesselle
changed the title
Gedochao
added
the
regression
|
Doesn't compile on 3.3.3, so it's also a regression... |
It was introduced by #18016 |
It looks like it shouldn't compile. So not a regression, "just" a soundness bug. |
|
@sjrd @dwijnand @odersky There are 3 possible solutions:
Handling the case in
|
|
Logically, a match type with no matching cases should simply not reduce (or return NoType, and then upstream we'd not reduce when we see that). When that causes follow-on erorrs (e.g. TypeMismatch) we show the failing reduction in ShowMatchTrace. |
Okay, that is exactly what #19954 implements. @sjrd mentioned this requiring a SIP #19954 (comment). If so, should I merge it with covariance improvements ? |
My preference is 1 over 3 over 2, fwiw. |
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 `ErrorType`s 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: ```scala 3 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: ```scala 3 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 ```scala 3 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: ```scala 3 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
Match type with no cases reduces to unreported
ErrorTypeCompiler version
3.4.2-RC1
Minimized code
We also have the same issue when using a projection:
Minimised from @Gedochao's #19936 (comment)
The text was updated successfully, but these errors were encountered: