GADT pattern matching unsoundness. #3645

sir-wabbit · 2017-12-10T14:37:30Z

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).

The text was updated successfully, but these errors were encountered:

sir-wabbit · 2017-12-10T15:20:20Z

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 · 2017-12-10T17:58:15Z

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

sir-wabbit · 2017-12-10T18:36:21Z

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 · 2017-12-10T18:58:46Z

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 · 2017-12-10T19:06:49Z

@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 · 2017-12-10T19:09:50Z

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 · 2017-12-11T02:49:35Z

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 · 2017-12-11T15:17:40Z

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 · 2017-12-11T16:28:55Z

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 · 2017-12-11T17:55:27Z

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 · 2017-12-11T18:25:23Z

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 · 2017-12-11T18:38:55Z

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 · 2017-12-11T21:44:23Z

@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 .

fix #3645: handle type alias in child instantiation

smarter · 2018-01-19T22:10:30Z

Reopening as it seems the issue is deeper than what #3646 fixed.

Blaisorblade · 2018-02-15T01:26:39Z

It's either that, or admit that we don't know if abstract type members are subtypes of other types.

👍 for the abstract types idea.

Hm, on the other hand they are not really abstract (path.T for a stable
path)

path is stable so T has a fixed definition, but that definition is hidden so path.T is still abstract. You can turn the Module into an argument so that it's more clearly abstract — I've done the exercise below.

I only have a vague idea about the code in #3646, but your intuition about what quantification is needed makes sense. IIUC, the code tries to reduce A <:< B to A' <:< B' (well, childTypeMap.apply(parent) <:< parentTypeMap.apply(tp2)) while preserving the result. It tries to compute A' and B' by picking a suitable substitution for type variables, but (a) in our scenario, we care about abstract type Foo in invariant position, so there's not much to maximize/minimize (b) the question we care for is "is there a type substitution G such that G(A) <:< G(B), and in this case there is indeed such a substitution (G(Foo) = Int). Not sure how to find it in general; but K[Foo] <:< K[Int] reduces to Foo =:= Int by invariance, which can be solved by unification (well, even matching). Unification and/or matching with subtyping are probably trickier, but we need some version of it for type inference?
EDIT: in fact, in this case trying to match K[Foo] against K1 seems equivalent to trying to apply def foobar[Foo](arg: F[Foo]) to F[Int]: in both cases we end up searching for the same type substitution.

@liufengyun any chance we can talk about this (maybe even tomorrow)? I'm sure I don't fully get the code but maybe we can help.

trait ModuleSig {
  type F[_]
  type U

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

  val Foo: FooSig
}

class ModuleUser(Module: ModuleSig) {
  def foo(): Unit = {
    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)
  }
}

object App {
  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
    }
  }
  def main(args: Array[String]): Unit =
    new ModuleUser(Module).foo()
}

Blaisorblade · 2018-02-15T02:47:19Z

I'm looking at roles, but I'm still wondering if they're indeed applicable to our Scala scenario — I haven't decided but I still think not. Maybe I'm missing something?

Looking at "Generative Type Abstraction and Type-level Computation":

that paper focuses on newtypes, not abstract types, and newtypes don't quite behave as abstract types. For instance, they show this code

data K a where
  KAge :: K Age
  KInt :: K Int
get :: K Age→ String
get KAge = "Age"

and claim that

Since get’s type signature declares that its argument is of type K Age, the patterns in get are exhaustive.

But claiming get is exhaustive makes little sense if Age is an abstract type. Instead, get is exhaustive if Age is concrete and distinct from Int, as is the case in Haskell at role "code". Conversely, the check we're discussing (looking if there are instantiations of Age that enable matching with KAge) makes little sense in Haskell, since Age isn't a type variable.

Overall, the goal is to take some hidden type equalities, and make them visible at role "type" (Sec. 3). But when typechecking ModuleUser we can't look at Module because of separate compilation (Module need not exist when we typecheck ModuleUser), so that idea doesn't translate so easily to our context. Sec. 1 claims the problem could arise with ML-style module systems, which are closer to Scala, and points to Sec. 7, but that doesn't show how the issues could arise with abstract types.

They add in Sec. 3.2 that:

These kinds in turn support the key insight of this paper: it is only safe to lift coercions through functions with parametric kinds.

but since Scala has abstract types, we can soundly write the coercions we want ourselves (as you did), and they're sound by themselves, it's hard to blame the coercion lifting, and much easier to blame the match.

in the end, Haskell doesn't implement roles as in "Generative Type Abstraction and Type-level Computation", but uses the evolved variant in "Safe Zero-cost Coercions for Haskell"; not sure if that complicates the picture, I might have to check it.

Blaisorblade · 2018-02-20T13:08:39Z

Took a look, talked with @liufengyun, tried the examples, and #3646 seems to fix all the given ones. @liufengyun also explained me why using <:< does the right thing after the preprocessing for types in invariant position; for types in variant position, I think I can see why "maximizing" the type variable works (though I'm a bit wobblier there): If K is covariant and for some X, K[X] satisfies constraints, then K[MaximizedX] also does.

In particular, I learned the answer to this question:

Unification and/or matching with subtyping are probably trickier, but we need some version of it for type inference?

In Dotty <:< is also a constraint solver for type variables.

Plan: check the examples are covered by testcases and close the issue.

Blaisorblade · 2018-02-20T13:11:59Z

Since even the last example is in https://github.com/lampepfl/dotty/pull/3646/files#diff-4511d6b273cb5ec2facf7dbd0ef33330, closing.

Blaisorblade · 2018-03-04T14:42:26Z

Sorry this was for another issue, doh!

liufengyun added a commit to dotty-staging/dotty that referenced this issue Dec 10, 2017

fix scala#3645: handle type alias in child instantiation

e04e529

liufengyun mentioned this issue Dec 10, 2017

fix #3645: handle type alias in child instantiation #3646

Merged

liufengyun added a commit to dotty-staging/dotty that referenced this issue Dec 19, 2017

fix scala#3645: handle type alias in child instantiation

b720fe2

liufengyun self-assigned this Jan 11, 2018

allanrenucci closed this as completed in #3646 Jan 18, 2018

allanrenucci added a commit that referenced this issue Jan 18, 2018

Merge pull request #3646 from dotty-staging/fix-3645

cebe706

fix #3645: handle type alias in child instantiation

smarter reopened this Jan 19, 2018

Blaisorblade self-assigned this Feb 15, 2018

Blaisorblade closed this as completed Feb 20, 2018

Blaisorblade mentioned this issue Feb 21, 2018

Subtype constraint solving is incomplete, so GADT exhaustiveness checking could be unsound #4029

Open

2 tasks

Blaisorblade mentioned this issue Mar 1, 2018

Blog Post: Announcing Dotty 0.6.0 and 0.7.0-RC1 #4053

Merged

Blaisorblade mentioned this issue Nov 12, 2018

WIP: Constraint-based GADT reasoning #5258

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

GADT pattern matching unsoundness. #3645

GADT pattern matching unsoundness. #3645

sir-wabbit commented Dec 10, 2017 •

edited

Loading

sir-wabbit commented Dec 10, 2017 •

edited

Loading

liufengyun commented Dec 10, 2017 •

edited

Loading

sir-wabbit commented Dec 10, 2017

sir-wabbit commented Dec 10, 2017 •

edited

Loading

liufengyun commented Dec 10, 2017

sir-wabbit commented Dec 10, 2017

sir-wabbit commented Dec 11, 2017 •

edited

Loading

sir-wabbit commented Dec 11, 2017 •

edited

Loading

sir-wabbit commented Dec 11, 2017

edmundnoble commented Dec 11, 2017

sir-wabbit commented Dec 11, 2017 via email

sir-wabbit commented Dec 11, 2017 via email

liufengyun commented Dec 11, 2017

smarter commented Jan 19, 2018

Blaisorblade commented Feb 15, 2018 •

edited

Loading

Blaisorblade commented Feb 15, 2018

Blaisorblade commented Feb 20, 2018 •

edited

Loading

Blaisorblade commented Feb 20, 2018

Blaisorblade commented Mar 4, 2018 •

edited

Loading

GADT pattern matching unsoundness. #3645

GADT pattern matching unsoundness. #3645

Comments

sir-wabbit commented Dec 10, 2017 • edited Loading

sir-wabbit commented Dec 10, 2017 • edited Loading

liufengyun commented Dec 10, 2017 • edited Loading

sir-wabbit commented Dec 10, 2017

sir-wabbit commented Dec 10, 2017 • edited Loading

liufengyun commented Dec 10, 2017

sir-wabbit commented Dec 10, 2017

sir-wabbit commented Dec 11, 2017 • edited Loading

sir-wabbit commented Dec 11, 2017 • edited Loading

sir-wabbit commented Dec 11, 2017

edmundnoble commented Dec 11, 2017

sir-wabbit commented Dec 11, 2017 via email

sir-wabbit commented Dec 11, 2017 via email

liufengyun commented Dec 11, 2017

smarter commented Jan 19, 2018

Blaisorblade commented Feb 15, 2018 • edited Loading

Blaisorblade commented Feb 15, 2018

Blaisorblade commented Feb 20, 2018 • edited Loading

Blaisorblade commented Feb 20, 2018

Blaisorblade commented Mar 4, 2018 • edited Loading

sir-wabbit commented Dec 10, 2017 •

edited

Loading

sir-wabbit commented Dec 10, 2017 •

edited

Loading

liufengyun commented Dec 10, 2017 •

edited

Loading

sir-wabbit commented Dec 10, 2017 •

edited

Loading

sir-wabbit commented Dec 11, 2017 •

edited

Loading

sir-wabbit commented Dec 11, 2017 •

edited

Loading

Blaisorblade commented Feb 15, 2018 •

edited

Loading

Blaisorblade commented Feb 20, 2018 •

edited

Loading

Blaisorblade commented Mar 4, 2018 •

edited

Loading