area:match-types Match type reduction stuck on disjointness test for types of the form `1 | Nothing`

[p-pavel]

Compiler version

3.4.2, 3.3.1

Minimized code

type Disj[A, B] = 
  A match 
    case B => true
    case _       => false

def f(a: Disj[1 | Nothing, 2 | Nothing]): Unit = ()

val t = f(false)

Output

Found:    (false : Boolean)
Required: com.perikov.typelevel.tests.Disj[(1 : Int) | Nothing, (2 : Int) | Nothing]

Note: a match type could not be fully reduced:

  trying to reduce  com.perikov.typelevel.tests.Disj[(1 : Int) | Nothing, (2 : Int) | Nothing]
  failed since selector (1 : Int) | Nothing
  does not match  case (2 : Int) | Nothing => (true : Boolean)
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case _ => (false : Boolean)

Expectation

Disj should reduce to false.

Types like this arise from Tuple.Union[(1,2,3)]