Match Types: implement cantPossiblyMatch #5996

OlivierBlanvillain · 2019-02-28T15:45:08Z

This PR implements one of the missing aspects of Match Types: an algorithm to determine when it is sound to reduce match types (see discussion in #5300).

To understand the problem that is being solved, we can look at the motivational example from the Haskell Role paper (adapted to Scala).

Given this class:

class Foo {
  type Age

  type Type[X] = X match {
    case Age => Char
    case Int => Boolean
  }

  def method[X](x: X): Type[X] = ...
}

What is the type of method(1)?

On master, the compiler answers with "it depends", it could be either Char or Boolean, which is obviously unsound:

val foo = new Foo { type Age = Int }
foo.method(1): Char
(foo: Foo).method(1): Boolean

The current algorithm to reduce match types is as follows:

foreach pattern
if (scrutinee <:< pattern)
  return pattern's result type
else
  continue

The unsoundness comes from the fact that the answer of scrutinee <:< pattern can change depending on the context, which can result in equivalent expressions being typed differently.

The proposed solution is to extend the algorithm above with an additional intersection check:

foreach pattern
if (scrutinee <:< pattern)
  return pattern's result type
if (!intersecting(scrutinee, pattern))
  continue
else
  abort

Where intersecting returns false if there is a proof that both of its arguments are not intersecting. In the absence of such proof, the reduction is aborted. This algorithm solves the type Age example by preventing the reduction of Type[X] when Age is abstract (and X != Age) . I believe this is enough to have sound type functions without the need for adding roles to the type system.

This PR is best reviewed commit by commit as it contains quite a bit refactoring, all the interesting work is condescended in the commit entitled Implement cantPossiblyMatch.

This commit implements one of the missing aspects of Match Types: an algorithm to determine when it is sound to reduce match types (see discussion in scala#5300). To understand the problem that is being solved, we can look at the motivational example from the [Haskell Role paper](https://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf) (adapted to Scala). Given this class: ```scala class Foo { type Age type Type[X] = X match { case Age => Char case Int => Boolean } def method[X](x: X): Type[X] = ... } ``` What is the type of `method(1)`? On master, the compiler answers with "it depends", it could be either `Char` or `Boolean`, which is obviously unsound: ```scala val foo = new Foo { type Age = Int } foo.method(1): Char (foo: Foo).method(1): Boolean ``` The current algorithm to reduce match types is as follows: ``` foreach pattern if (scrutinee <:< pattern) return pattern's result type else continue ``` The unsoundness comes from the fact that the answer of `scrutinee <:< pattern` can change depending on the context, which can result in equivalent expressions being typed differently. The proposed solution is to extend the algorithm above with an additional intersection check: ``` foreach pattern if (scrutinee <:< pattern) return pattern's result type if (!intersecting(scrutinee, pattern)) continue else abort ``` Where `intersecting` returns `false` if there is a proof that both of its arguments are not intersecting. In the absence of such proof, the reduction is aborted. This algorithm solves the `type Age` example by preventing the reduction of `Type[X]` (with `X != Age`) when `Age is abstract. I believe this is enough to have sound type functions without the need for adding roles to the type system.

This commit also updates pattern matching exhaustivity tests for the new type inhavitation decision procedure. The diffs in t6420 and t7466 comes from a bug a the previous algorithm that would conclue that given `val a: Int`, `1` and `a.type` are non- intersecting because they are both singleton types. However, we can only get to that conclusion when both types are ConstantTypes. The diff in andtype-opentype-interaction come from the fact that the new decomposition of sealed types is more powerful than the previous one. For instance, we can now rule out `SealedClass & OpenTrait` as both types are provably non intersecting. i3574.scala is pending for now due to the removal of inhabitation check of childrens, it will be enabled back in a subsequent commit.

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

`Some isSubType List` returns `false`, so use derivesFrom instead.

compiler/src/dotty/tools/dotc/ast/tpd.scala

compiler/src/dotty/tools/dotc/transform/SymUtils.scala

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

odersky · 2019-03-05T21:26:43Z

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

-              instantiateParams(instances)(body)
+    var result: Type = NoType
+    var remainingCases = cases
+    while (!remainingCases.isEmpty) {


Why not use a tail-recursive function for matchCases?

I don't want constraints created while trying to evaluate one case to be carried over to the following cases, but I'm not sure if having these extra constraints could change anything...

compiler/src/dotty/tools/dotc/typer/Typer.scala

odersky · 2019-03-05T21:54:11Z

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

@@ -516,101 +514,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {

    val childTp = if (child.isTerm) child.termRef else child.typeRef

-    val resTp = instantiate(childTp, parent)(ctx.fresh.setNewTyperState())
-
-    if (!resTp.exists || !inhabited(resTp)) {


The first part returning NoType is no longer present. Is that intentional? EDIT: I see that seems to be handled by the next commit "Check inhabitation of children" now. Correct?

Also, I don't understand SpaceEngines inhabited enough so I have to ask: Does SpaceEngine follow the same logic that an abstract type / type parameter and a class type can potentially overlap? /cc @liufengyun

Yes, it takes the bounds & variance of abstract type & type parameters into consideration.

So it reports non-exhaustive warnings for the following code (it is possible that T = Int | Boolean):

object O { sealed trait Expr[+T] case class IExpr(x: Int) extends Expr[Int] case class BExpr(b: Boolean) extends Expr[Boolean] def foo[T](x: Expr[T], y: Expr[T]) = (x, y) match { case (IExpr(_), IExpr(_)) => true case (BExpr(_), BExpr(_)) => false } }

It does not report warning for the following code, due to nonvariance of the type parameter:

object O { sealed trait Expr[T] case class BExpr(bool: Boolean) extends Expr[Boolean] case class IExpr(int: Int) extends Expr[Int] def join[T](e1: Expr[T], e2: Expr[T]): Expr[T] = (e1, e2) match { case (IExpr(i1), IExpr(i2)) => IExpr(i1 + i2) case (BExpr(b1), BExpr(b2)) => BExpr(b1 & b2) } }

Yes I did that in a separate commit because it requires some extra logic: this check from space takes a type as input and looks for unrealizable intersections inside, while the other check started from two types and checks if their intersection is unrealizable. The commits move a test back and forth in /pending to document what is handled by that code.

odersky · 2019-03-05T22:16:02Z

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

+                      }
+                  }
+                  !(fullyInstantiated.apply(true, arg1) &&
+                    fullyInstantiated.apply(true, arg2))


I think this still misses the case where we have an abstract TypeRef that is not a type parameter. Also, it is a bit unsatisfactory that for toplevel TypeRefs and TypeParamRefs we go to their supertypes but here we do not. So if I understand correctly in the case where we have a TypeParamRef A <: Int and a TypeParamRef B <: String, we would diagnose a possible overlap for

NonVariant[A], NonVariant[B]

but no such overlap for

CoVariant[A], Covariant[B]

(because for the latter we do a recursive call of intersecting).

I think this still misses the case where we have an abstract TypeRef that is not a type parameter.

I changed the test from tp.symbol.is(TypeParam) to tp.symbol.isAbstractOrParamType and added a test.

Also, it is a bit unsatisfactory that for toplevel TypeRefs and TypeParamRefs we go to their supertypes but here we do not. [...]

Indeed, I guess I can also run the covariant test in the invariant case, invariance should give us more ways to prove non overlap, not less!

odersky · 2019-03-06T06:58:50Z

It's great that this unifies essential logic for match types and exhaustivity checking!

This reverts commit 6e39fcb.

This reverts commit bb1515e.

liufengyun · 2019-03-06T10:52:45Z

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

+            }
+          }
+          if (inhabited.apply(true, refined)) refined
+          else NoType


It seems that a nested non-inhabitable intersection type does not necessarily mean the outer type is non-inhabited, just as Nothing does not imply F[Nothing] is non-inhabited..

Good point, I've updated that check to be more conservative while traversing refined.

To be more conservative during the traversal. As pointed out in the review "nested non-inhabitable intersection type does not necessarily mean the outer type is non-inhabited".

OlivierBlanvillain added 6 commits February 28, 2019 13:41

Minor TypeTestsCasts refactoring

c1b7e84

Rename evalOnce to letBind

6e39fcb

Rename cmp to typeComparer

eef623a

Remove reduceParallel

6755f52

Fix spacing for TypeComparer comments

88cfb7e

Flag ChildrenQueried in hasAnonymousChild

bb1515e

OlivierBlanvillain requested a review from odersky February 28, 2019 18:13

OlivierBlanvillain assigned odersky Feb 28, 2019

OlivierBlanvillain added 5 commits March 1, 2019 14:53

Move refineUsingParent to Typer

d1180cc

Check inhabitation of children in Space

b0c1e7b

Only trust isSameType for fully instanciated types

c3d23fe

OlivierBlanvillain force-pushed the match-types branch from cb34288 to c3d23fe Compare March 1, 2019 13:53

abgruszecki reviewed Mar 1, 2019

View reviewed changes

compiler/src/dotty/tools/dotc/core/TypeComparer.scala Outdated Show resolved Hide resolved

OlivierBlanvillain added 3 commits March 4, 2019 14:43

Use derivesFrom instead of isSubType for classes

4f934ad

`Some isSubType List` returns `false`, so use derivesFrom instead.

Handle type parameters using symbol.is(TypeParam)

80c25e3

Fix AppliedType logic

ab74827

odersky requested changes Mar 5, 2019

View reviewed changes

odersky assigned OlivierBlanvillain and unassigned odersky Mar 5, 2019

OlivierBlanvillain added 2 commits March 6, 2019 10:58

Revert "Rename evalOnce to letBind"

1df0d8b

This reverts commit 6e39fcb.

Revert "Flag ChildrenQueried in hasAnonymousChild"

8827eff

This reverts commit bb1515e.

liufengyun reviewed Mar 6, 2019

View reviewed changes

OlivierBlanvillain added 4 commits March 6, 2019 14:53

Address review

ffa8acf

Move refineUsingParent to TypeOps

e7f6049

Factor out cov. test and use it in the inv. case

f4df58d

Update inhabited check in Space

ea04343

To be more conservative during the traversal. As pointed out in the review "nested non-inhabitable intersection type does not necessarily mean the outer type is non-inhabited".

odersky approved these changes Mar 9, 2019

View reviewed changes

odersky merged commit 51d8cab into scala:master Mar 9, 2019

OlivierBlanvillain mentioned this pull request Mar 9, 2019

Make all match types invariant #6047

Closed

LPTK mentioned this pull request May 28, 2019

Make type projections safe instead of dropping them lampepfl/dotty-feature-requests#14

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Match Types: implement cantPossiblyMatch #5996

Match Types: implement cantPossiblyMatch #5996

OlivierBlanvillain commented Feb 28, 2019 •

edited

Loading

odersky Mar 5, 2019

OlivierBlanvillain Mar 6, 2019

odersky Mar 5, 2019

odersky Mar 5, 2019

liufengyun Mar 6, 2019

OlivierBlanvillain Mar 6, 2019

odersky Mar 5, 2019

OlivierBlanvillain Mar 6, 2019

odersky commented Mar 6, 2019

liufengyun Mar 6, 2019

OlivierBlanvillain Mar 6, 2019

Match Types: implement cantPossiblyMatch #5996

Match Types: implement cantPossiblyMatch #5996

Conversation

OlivierBlanvillain commented Feb 28, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

odersky commented Mar 6, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

OlivierBlanvillain commented Feb 28, 2019 •

edited

Loading