Spurious exhaustivity warning using an irrefutable unapply with a singleton type

[SrTobi]

reproduction steps

minimized code:

object Test {
  sealed trait Base
  class Blub extends Base
  object Blub {
    def unapply(blub: Blub): Some[(Int, blub.type)] =
      Some(1 -> blub)
  }

  (null: Base) match {
    case Blub(i, x) => println(i)
  }
}

problem

Expect everything to compile without warnings, but gives

match may not be exhaustive.

It would fail on pattern case: Blub(_, _)

  (null: Base) match {

If the dependent type is removed or (null: Blub) used, the warning will go away

[dwijnand]

To add further proof (not that it's needed IMO), I think it's obviously a false positive when:

  (null: Base) match {
    case b: Blub => b match {
      case Blub(i, x) => println(i)
    }
  }

doesn't give the warning.

[dwijnand]

Hmm, maybe not good proof, as that doesn't warn because Blub isn't sealed... 🙄 When marked as sealed class Blub that version warns again. 🤔

[dwijnand]

Here's some tracing output:

exhaustivity: selTyp = Test.Base
exhaustivity: pat=Test.Blub(i @ _, x @ _):Test.Blub ====> space=Blub(_{Int}, _{(?1 : Test.Blub)})
exhaustivity:     selSpace = _: Base
exhaustivity: patternSpace = Blub(_{Int}, _{(?1 : Test.Blub)})
==> _: Base - Blub(_{Int}, _{(?1 : Test.Blub)})?
...
signature of Test.Blub.unapply ----> [Int, Test.Blub]
        ==> Blub(_{Int}, _{Blub}) - Blub(_{Int}, _{(?1 : Test.Blub)})?
...
          ==> _{Blub} - _{(?1 : Test.Blub)}?
...
          <== _{Blub} - _{(?1 : Test.Blub)} = _{Blub}

Looks to me like the way patterns are projected to spaces captures the dependent type, while the reading of the unappy signature doesn't, so they don't cancel out.