Simple GADT giving "match may not be exhaustive"

[atennapel]

Minimized code

enum Bool:
  case True
  case False

import Bool._

enum SBool[B <: Bool]:
  case STrue extends SBool[True.type]
  case SFalse extends SBool[False.type]

import SBool._

def f(b: SBool[True.type]): Unit = b match
  case STrue => ()

https://scastie.scala-lang.org/sFyhkz0wRg2Uvtl9GE37dQ

Output

match may not be exhaustive.

It would fail on pattern case: SFalse

Expectation

I would expect f to be exhaustive because from the type parameter we can know that SFalse cannot occur. Is this a limitation of Dotty or a bug?