GADT pattern matching unsoundness.

sir-wabbit commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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

sir-wabbit commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

@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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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" notifications@github.com 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 https://github.com/lampepfl/dotty/issues/3645#issuecomment-350804092, or mute the thread https://github.com/notifications/unsubscribe-auth/AAiH7io-BcP2r_uJITOZVC1Y2MND_-gTks5s_WyWgaJpZM4Q8g3Z .

sir-wabbit commented 6 years ago

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" alex.knvl@gmail.com 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" notifications@github.com 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 https://github.com/lampepfl/dotty/issues/3645#issuecomment-350804092, or mute the thread https://github.com/notifications/unsubscribe-auth/AAiH7io-BcP2r_uJITOZVC1Y2MND_-gTks5s_WyWgaJpZM4Q8g3Z .

liufengyun commented 6 years ago

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

smarter commented 6 years ago

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

Blaisorblade commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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

Blaisorblade commented 6 years ago

Sorry this was for another issue, doh!

scala / scala3

GADT pattern matching unsoundness. #3645