Unspecified behaviour of match type on exact higher order type

[WojciechMazur]

Compiler version

3.3.0-RC3 (same behavior in every Scala version, including nightly)

Scala documentation does not specify is an example of match typed defined below are allowed.

Minimized code

type IsExpected[x, expected] <: Boolean = x match
  case expected => true
  case _        => false

type IsOptionInt[x] = IsExpected[x, Option[Int]]
summon[IsOptionInt[String] =:= false] // ok
summon[IsOptionInt[Option[Int]] =:= true] // ok
summon[IsOptionInt[Option[String]] =:= false] // compilation-error```

Output

Cannot prove that IsOptionInt[Option[String]] =:= (false : Boolean).

Note: a match type could not be fully reduced:

  trying to reduce  IsOptionInt[Option[String]]
  trying to reduce  IsExpected[Option[String], Option[Int]]
  failed since selector  Option[String]
  does not match  case Option[Int] => (true : Boolean)
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case _ => (false : Boolean)

Workaround

type IsExpected[x, expected] <: Boolean = x match
  case Option[t] => //
    expected match
      case Option[e] => IsExpected[t, e]
      case _         => false
  case expected => true
  case _        => false

Workaround 2

Use invariant type instead of covariant Option[+T]

type IsExpected[x, expected] <: Boolean = x match
  case expected => true
  case _        => false

sealed trait Opt[A]
object Non extends Opt[Nothing]
final class Som[A] extends Opt[A]

type IsOptInt[x] = IsExpected[x, Opt[Int]]
summon[IsOptInt[String] =:= false] // ok
summon[IsOptInt[Opt[Int]] =:= true] // ok
summon[IsOptInt[Opt[String]] =:= false] // ok

Expectation

Documentation of match types should define how exact type matches work. If it is a bug it should be fixed, otherwise compiler should produce a helpful explanation.