Match types' type binds are unsound

[abgruszecki]

It is possible to exploit the way match types bind type variable to make match types "forget" they are dealing with an abstract type. I have multiple examples, but possibly the one easiest to understand is:

object Base {
  trait Trait1
  trait Trait2
  type N[t] = t match {
    case String => Trait1
    case Int => Trait2
  }
}
import Base._

object UpperBoundParametricVariant {
  trait Cov[+T]
  type M[t] = t match { 
    case Cov[t] => N[t]
  }
  
  trait Root[A] {
    def thing: M[A]
  }

  trait Child[A <: Cov[Int]] extends Root[A]

  // we reduce `M[T]` to `Trait2`, even though we cannot be certain of that
  def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing

  class Asploder extends Child[Cov[String & Int]] {
    def thing = new Trait1 {}
  }

  def explode = foo(new Asploder) // ClassCastException
}

Essentially, what seems to happen is that when reducing M, we pick the Cov[t] case, bind t to a non-abstract type and happily proceed with the reduction. It's illustrating to consider that foo would not compile if we defined M like:

  type M[t] = t match {
    case Cov[String] => Trait1
    case Cov[Int] => Trait2
}

The other "exploits"

are here

object InheritanceVariant {
  // allows binding a variable to the UB of a type member
  type Trick[a] = { type A <: a }
  type M[t] = t match { case Trick[a] => N[a] }

  trait Root {
    type B
    def thing: M[B]
  }

  trait Child extends Root { type B <: { type A <: Int } }

  def foo(c: Child): Trait2 = c.thing

  class Asploder extends Child {
    type B = { type A = String & Int }
    def thing = new Trait1 {}
  }
}

object ThisTypeVariant {
  type Trick[a] = { type A <: a }
  type M[t] = t match { case Trick[a] => N[a] }

  trait Root {
    def thing: M[this.type]
  }

  trait Child extends Root { type A <: Int }

  def foo(c: Child): Trait2 = c.thing

  class Asploder extends Child {
    type A = String & Int
    def thing = new Trait1 {}
  }
}

object ParametricVariant {
  type Trick[a] = { type A <: a }
  type M[t] = t match { case Trick[a] => N[a] }
  
  trait Root[B] {
    def thing: M[B]
  }

  trait Child[B <: { type A <: Int }] extends Root[B]

  def foo[T <: { type A <: Int }](c: Child[T]): Trait2 = c.thing

  class Asploder extends Child[{ type A = String & Int }] {
    def thing = new Trait1 {}
  }

  def explode = foo(new Asploder)
}

object UpperBoundVariant {
  trait Cov[+T]
  type M[t] = t match { case Cov[t] => N[t] }
  
  trait Root {
    type A 
    def thing: M[A]
  }

  trait Child extends Root { type A <: Cov[Int] }

  def foo(c: Child): Trait2 = c.thing

  class Asploder extends Child {
    type A = Cov[String & Int]
    def thing = new Trait1 {}
  }

  def explode = foo(new Asploder)
}

/cc @OlivierBlanvillain

[abgruszecki]

We've just considered fixing this problem by checking that the scrutinee does not contain abstract types at the "toplevel" (as leaves of union of intersections). This would fix the following example:

type M[t] = t match {
  case Cov[t] => N[t]
}
[T <: Cov[Int]] => M[T]

However, it does nothing for the following one:

type M[t] = (Int, t) match {
  case (Int, Cov[t]) => N[t]
}
[T <: Cov[Int]] => M[T]

The problem seems to lie with being able to "destructure" an abstract type, i.e. bind type variables to its subcomponents. This is reinforced by the observation that, as far as I can tell, it's perfectly sound to bind a type variable directly to an abstract type:

type F[t] = t match { case List[u] => u }
def foo[U, T <: List[U](...): F[T] // no unsoundness possible here