GADT pattern matching unsoundness.

[sir-wabbit]

object App {
  def main(args: Array[String]): Unit = {
    trait AgeT {
      type T
      def subst[F[_]](fa: F[Int]): F[T]
    }
    type Age = Age.T
    final val Age: AgeT = new AgeT {
      type T = Int
      def subst[F[_]](fa: F[Int]): F[T] = fa
    }

    sealed abstract class K[A]
    final case object KAge extends K[Age]
    final case object KInt extends K[Int]

    val kint: K[Age] = Age.subst[K](KInt)
    def get(k: K[Age]): String = k match {
      case KAge => "Age"
    }

    get(kint)
  }
}

Produces no warnings but results in a runtime MatchError failure.

Somewhat relevant paper (it describes a similar problem in Haskell that was solved by the introduction of roles, but I am not sure how applicable it is in the context of Scala).

[sir-wabbit]

I believe (pure speculation based on intuition at this point) that the underlying issue is that type equality is used in negative positions in patmat.SpaceLogic.

https://github.com/lampepfl/dotty/blob/7fa8a93694839b58b783128c2d8ae6098893a42f/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala#L220
https://github.com/lampepfl/dotty/blob/7fa8a93694839b58b783128c2d8ae6098893a42f/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala#L264

---

if (!(tpe1 =:= tpe2)) means "types are not provably equal", not "types are provably unequal".
This means that most occurrences of either !(A =:= B) or !(A <:< B) anywhere in the code are likely to be bugs. IMHO type comparison should return Option[Boolean], with Some(true) meaning "provably equal", Some(false) - "provably unequal", None - "neither". Or even better:

sealed abstract class TypeComparison
final case object ProvablyEqual extends TypeComparison
final case object ProvablyUnequal extends TypeComparison
final case object Indeterminate extends TypeComparison

In the example above it is impossible to prove that types Int and Age are not equal in the context of the pattern match, therefore it should result in an exhaustivity warning / error. If a similar pattern match was done inside of AgeT given type T = String, types would be provably unequal and there would be no need for a warning. So type equality / inequality actually depends on the current context.

[liufengyun]

Thanks a lot @alexknvl for reporting and the diagnosis. I just create a PR #3646 to handle this issue.

[sir-wabbit]

The following snippet still compiles with the fix:

object App {
  def main(args: Array[String]): Unit = {
    trait FooT {
      type T
    }
    val Foo: FooT = new FooT {
      type T = Int
    }
    type Foo = Foo.T
    type Bar = Foo

    sealed abstract class K[A]
    final case object K1 extends K[Int]
    final case object K2 extends K[Foo]
    final case object K3 extends K[Bar]

    def get(k: K[Int]): Unit = k match {
      case K1 => ()
      // case K2 => ()
      // case K3 => ()
    }
  }
}

but it is similarly unsound.

[sir-wabbit]

Running the code with debug output shows that:

candidates for K[Int] : [object K3, object K2, object K1]
[refine] unqualified child ousted: K3.type !< K[Int]
[refine] unqualified child ousted: K2.type !< K[Int]
K[Int] decomposes to [K1.type]

which is incorrect.

---

I believe that the offending lines are https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala#L628 and https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala#L634 (or rather corresponding else) -- !(A <:< B) does not mean that A is not a subtype of B, but rather that A could not be proved to be a subtype of B.

[liufengyun]

@alexknvl If you write get(K2) or get(K3), there will be a typing error, so I think it's correct to assume that the pattern above is exhaustive.

[sir-wabbit]

Here is an example that throws MatchError at runtime.

object App {
  def main(args: Array[String]): Unit = {
    trait FooT {
      type T
      def subst[F[_]](fa: F[T]): F[Int]
    }
    val Foo: FooT = new FooT {
      type T = Int

      def subst[F[_]](fa: F[T]): F[Int] = fa
    }
    type Foo = Foo.T
    type Bar = Foo

    sealed abstract class K[A]
    final case object K1 extends K[Int]
    final case object K2 extends K[Foo]
    final case object K3 extends K[Bar]

    val foo: K[Int] = Foo.subst[K](K2)
    def get(k: K[Int]): Unit = k match {
      case K1 => ()
      // case K2 => ()
      // case K3 => ()
    }

    get(foo)
  }
}

[sir-wabbit]

With the most recent fixes:

object App {
  def main(args: Array[String]): Unit = {
    trait ModuleSig {
      type Upper

      trait FooSig {
        type Type <: Upper
        def subst[F[_]](fa: F[Int]): F[Type]
      }

      val Foo: FooSig
    }
    val Module: ModuleSig = new ModuleSig {
      type Upper = Int

      val Foo: FooSig = new FooSig {
        type Type = Int
        def subst[F[_]](fa: F[Int]): F[Type] = fa
      }
    }
    type Upper = Module.Upper
    type Foo = Module.Foo.Type

    sealed abstract class K[F]
    final case object K1 extends K[Int]
    final case object K2 extends K[Foo]

    val kv: K[Foo] = Module.Foo.subst[K](K1)
    def test(k: K[Foo]): Unit = k match {
      case K2 => ()
    }

    test(kv)
  }
}

fails at runtime with MatchError.

[sir-wabbit]

Found a new example that fails with the most recent commit in #3646 :

object App {
  def main(args: Array[String]): Unit = {
    trait ModuleSig {
      type U2
      type U1

      trait FooSig {
        type Type = (U1 & U2)
        def subst[F[_]](fa: F[Int]): F[Type]
      }

      val Foo: FooSig
    }
    val Module: ModuleSig = new ModuleSig {
      type U1 = Int
      type U2 = Int

      val Foo: FooSig = new FooSig {
        // type Type = Int
        def subst[F[_]](fa: F[Int]): F[Type] = fa
      }
    }
    type Foo = Module.Foo.Type

    sealed abstract class K[F]
    final case object K1 extends K[Int]
    final case object K2 extends K[Foo]

    val kv: K[Foo] = Module.Foo.subst[K](K1)
    def test(k: K[Foo]): Unit = k match {
      case K2 => ()
    }

    test(kv)
  }
}

[sir-wabbit]

Another one

object App {
  def main(args: Array[String]): Unit = {
    trait ModuleSig {
      type F[_]
      type U

      trait FooSig {
        type Type = F[U]
        def subst[F[_]](fa: F[Int]): F[Type]
      }

      val Foo: FooSig
    }
    val Module: ModuleSig = new ModuleSig {
      type F[A] = Int

      val Foo: FooSig = new FooSig {
        // type Type = Int
        def subst[F[_]](fa: F[Int]): F[Type] = fa
      }
    }
    type Foo = Module.Foo.Type

    sealed abstract class K[F]
    final case object K1 extends K[Int]
    final case object K2 extends K[Foo]

    val kv: K[Foo] = Module.Foo.subst[K](K1)
    def test(k: K[Foo]): Unit = k match {
      case K2 => ()
    }

    test(kv)
  }
}

[edmundnoble]

I think it's a safe bet that there's no solution to this in general without roles (https://ghc.haskell.org/trac/ghc/wiki/Roles). It's either that, or admit that we don't know if abstract type members are subtypes of other types.

[sir-wabbit]

From a phone. AFAIU the problem can be roughly summarized as: given two types A and B with some free type variables (+ constraints), a) is A <:< B for all instantiations of type vars b) for some c) for none. I don't completely understand the code, but would it be fair to say that if there was a way to constructively solve (b), that would resolve this issue? The code seems to be doing some sort of type normalization and then check <:<, which might not work in general, since <:< instantiates all type vars as if they are completely independent modulo constraints (?). Negation of it = for a particular instantiation !(A <:< B), not for all instantiations. I don't think that roles are directly relevant since here we are not really dealing with newtypes, just abstract types.

…

On Dec 11, 2017 12:55, "Edmund Noble" ***@***.***> wrote: I think it's a safe bet that there's no solution to this in general without roles (https://ghc.haskell.org/trac/ghc/wiki/Roles). It's either that, or admit that we *don't know* if abstract type members are subtypes of other types. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#3645 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAiH7io-BcP2r_uJITOZVC1Y2MND_-gTks5s_WyWgaJpZM4Q8g3Z> .

[sir-wabbit]

Hm, on the other hand they are not really abstract (path.T for a stable path) and in their behavior is very close to newtypes, so maybe it is directly applicable :) I need to finish reading that paper...

…

On Dec 11, 2017 13:25, "Alexander Konovalov" ***@***.***> wrote: From a phone. AFAIU the problem can be roughly summarized as: given two types A and B with some free type variables (+ constraints), a) is A <:< B for all instantiations of type vars b) for some c) for none. I don't completely understand the code, but would it be fair to say that if there was a way to constructively solve (b), that would resolve this issue? The code seems to be doing some sort of type normalization and then check <:<, which might not work in general, since <:< instantiates all type vars as if they are completely independent modulo constraints (?). Negation of it = for a particular instantiation !(A <:< B), not for all instantiations. I don't think that roles are directly relevant since here we are not really dealing with newtypes, just abstract types. On Dec 11, 2017 12:55, "Edmund Noble" ***@***.***> wrote: > I think it's a safe bet that there's no solution to this in general > without roles (https://ghc.haskell.org/trac/ghc/wiki/Roles). It's either > that, or admit that we *don't know* if abstract type members are > subtypes of other types. > > — > You are receiving this because you were mentioned. > Reply to this email directly, view it on GitHub > <#3645 (comment)>, > or mute the thread > <https://github.com/notifications/unsubscribe-auth/AAiH7io-BcP2r_uJITOZVC1Y2MND_-gTks5s_WyWgaJpZM4Q8g3Z> > . >

[liufengyun]

@alexknvl you are right, the solution I proposed in #3646 is basically to say if there's some instantiation of type variables such that A <:< B.

I'm yet to learn about roles, thanks for the pointer @edmundnoble .