Matching on Option[Option[T]] where T is abstract and obtained from inline def in super trait emits exhaustivity warning

[martingd]

Compiler version

Scala 3.2.1

Minimized code

trait Base:
    type Value
    inline def oov: Option[Option[Value]] = None
    def get: Option[Value]

trait X extends Base:
    override def get: Option[Value] =
        oov match
            case Some(ov) => ov
            case None => None

Output

The compiler emits the following warning:

[warn] -- [E029] Pattern Match Exhaustivity Warning: /path/to/Test.scala:8:8 
[warn] 8 |        oov match
[warn]   |        ^^^
[warn]   |        match may not be exhaustive.
[warn]   |
[warn]   |        It would fail on pattern case: Some(_)
[warn]   |
[warn]   | longer explanation available when compiling with `-explain`
[warn] one warning found

Expectation

The code should compile.

Workarounds

We have found three ways to make the code compile without this warning and one that gives a new unexpected error:

Extract oov to local value

trait Base:
    type Value
    inline def oov: Option[Option[Value]] = None
    def get: Option[Value]

trait X extends Base:
    override def get: Option[Value] =
        val local_oov = oov
        local_oov match
            case Some(ov) => ov
            case None => None

Remove inline

Without the inline modifier, the code compiles:

trait Base:
    type Value
    def oov: Option[Option[Value]] = None
    def get: Option[Value]

trait X extends Base:
    override def get: Option[Value] =
        oov match
            case Some(ov) => ov
            case None => None

Make type Value concrete

trait Base:
    type Value
    inline def oov: Option[Option[Value]] = None
    def get: Option[Value]

trait X extends Base:
    override type Value = Int
    override def get: Option[Value] =
        oov match
            case Some(ov) => ov
            case None => None

Adding transparent to inline results in new error

This code

trait Base:
    type Value
    transparent inline def oov: Option[Option[Value]] = None
    def get: Option[Value]

trait X extends Base:
    override def get: Option[Value] =
        oov match
            case Some(ov) => ov
            case None => None

causes the compiler to emit this error:

[error] -- [E007] Type Mismatch Error: /path/to/Test.scala:9:29 
[error] 9 |            case Some(ov) => ov
[error]   |                             ^^
[error]   |                             Found:    (ov : Any)
[error]   |                             Required: Option[X.this.Value]

[Kordyjan]

I think that transparent inline not working is expected as the method return type in such case is None which is Option[Nothing]. (Yeah, that is also a bug, but probably a different one).

Nevertheless, the original snippet is definitely a bug in the exhaustivity checker that was here even in 3.0.0.
@dwijnand any ideas?

[dwijnand]

No, no ideas why it being transparent changes things. But I can look.

[dwijnand]

That transparent inline one is also wrong: the type variable ?A in Some.unapply should infer to be upper-bounded by Nothing, and then instantiate to Nothing, not to Any.

[SethTisue]

This appears to be a type avoidance problem. After inlining, we have:

{
  val Base_this: (X.this : X) = this
  None:Option[Option[Base_this.Value]]
} match { ...

so the scrutinee's type now refers to Base_this, which is local to the block and thus subject to type avoidance.

That explains why the various workarounds work.

(The transparent version also looks like type avoidance, resulting in Option[Any].)

[SethTisue]

It's tempting to just slap an ensureConforms on it to typecast our way to working code, but that's a big-hammer fix. My fear is that in typecasting our way out of the problem, we might also end up inserting unsound typecasts in scenarios we didn't anticipate. (If the inliner has a bug, it's better for the bug to manifest itself as a compile-time error, as in this bug report, rather than manifesting silently as unsoundness.)

The inliner already has special logic around this references in particular, so perhaps adjusting that logic would be sufficient.

[smarter]

Seems like an avoidance bug, also reproducible by hand:

class A:
  type X
  def foo =
    val local: this.type = this
    val x: Option[local.X] = None
    x

x is inferred to have type Option[Any], but I don't see why avoidance couldn't produce Option[this.X] instead.

[SethTisue]

Dale, we touched on that possibility but you speculated it would probably be “too expensive”, want to expand on that thought?

[smarter]

Looks like this is caused by the use of tryWiden in https://github.com/lampepfl/dotty/blob/ef653b6a31180416ff6b7fdc432e9ef0343b7075/compiler/src/dotty/tools/dotc/core/TypeOps.scala#L495-L507
In our situation, tp is local.X and pre is this.type. Since the new prefix is a singleton it makes sense to go with that instead of the current logic which ends up widening local.X to Nothing .. Any (and then Any because we're in a covariant position)