Skip to content

Commit

Permalink
Refine Matchtype checking
Browse files Browse the repository at this point in the history 
Take up scala#13780 again, but refine it so that abstract types are allowed in match type
reduction as long as they uniquely instantiate type parameters of the type pattern.

Fixes scala#11982
  • Loading branch information
@odersky @bishabosha
odersky authored and bishabosha committed Oct 18, 2022
1 parent ebacde8 commit de9c544
Show file tree
Hide file tree
Showing 12 changed files with 288 additions and 33 deletions.
9 changes: 9 additions & 0 deletions compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ package core

import Types._, Contexts._, Symbols._, Decorators._
import util.Property
import Names.Name

/** A utility module to produce match type reduction traces in error messages.
*/
Expand All @@ -13,6 +14,7 @@ object MatchTypeTrace:
case TryReduce(scrut: Type)
case NoMatches(scrut: Type, cases: List[Type])
case Stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])
case NoInstance(scrut: Type, stuckCase: Type, pname: Name, bounds: TypeBounds)
case EmptyScrutinee(scrut: Type)
import TraceEntry._

Expand Down Expand Up @@ -62,6 +64,9 @@ object MatchTypeTrace:
def stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])(using Context) =
matchTypeFail(Stuck(scrut, stuckCase, otherCases))

def noInstance(scrut: Type, stuckCase: Type, pname: Name, bounds: TypeBounds)(using Context) =
matchTypeFail(NoInstance(scrut, stuckCase, pname, bounds))

/** Record a failure that scrutinee `scrut` is provably empty.
* Only the first failure is recorded.
*/
Expand Down Expand Up @@ -114,6 +119,10 @@ object MatchTypeTrace:
| Therefore, reduction cannot advance to the remaining case$s
|
| ${casesText(otherCases)}"""
case NoInstance(scrut, stuckCase, pname, bounds) =>
i""" failed since selector $scrut
| does not uniquely determine parameter $pname in ${caseText(stuckCase)}
| The computed bounds for the parameter are: $bounds."""

def noMatchesText(scrut: Type, cases: List[Type])(using Context): String =
i"""failed since selector $scrut
Expand Down
97 changes: 68 additions & 29 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
/** Indicates whether the subtype check used GADT bounds */
private var GADTused: Boolean = false

protected var canWidenAbstract: Boolean = true

private var myInstance: TypeComparer = this
def currentInstance: TypeComparer = myInstance

Expand Down Expand Up @@ -757,9 +759,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling

def tryBaseType(cls2: Symbol) = {
val base = nonExprBaseType(tp1, cls2)
if (base.exists && (base `ne` tp1))
isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) ||
base.isInstanceOf[OrType] && fourthTry
if base.exists && (base ne tp1)
&& (!caseLambda.exists || canWidenAbstract || tp1.widen.underlyingClassRef(refinementOK = true).exists)
then
isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow)
|| base.isInstanceOf[OrType] && fourthTry
// if base is a disjunction, this might have come from a tp1 type that
// expands to a match type. In this case, we should try to reduce the type
// and compare the redux. This is done in fourthTry
Expand All @@ -776,7 +780,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
|| narrowGADTBounds(tp1, tp2, approx, isUpper = true))
&& (tp2.isAny || GADTusage(tp1.symbol))

isSubType(hi1, tp2, approx.addLow) || compareGADT || tryLiftedToThis1
(!caseLambda.exists || canWidenAbstract) && isSubType(hi1, tp2, approx.addLow)
|| compareGADT
|| tryLiftedToThis1
case _ =>
// `Mode.RelaxedOverriding` is only enabled when checking Java overriding
// in explicit nulls, and `Null` becomes a bottom type, which allows
Expand Down Expand Up @@ -2849,7 +2855,16 @@ object TypeComparer {
comparing(_.tracked(op))
}

object TrackingTypeComparer:
enum MatchResult:
case Reduced(tp: Type)
case Disjoint
case Stuck
case NoInstance(param: Name, bounds: TypeBounds)

class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
import TrackingTypeComparer.*

init(initctx)

override def trackingTypeComparer = this
Expand Down Expand Up @@ -2887,15 +2902,25 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
}

def matchCases(scrut: Type, cases: List[Type])(using Context): Type = {
def paramInstances = new TypeAccumulator[Array[Type]] {
def apply(inst: Array[Type], t: Type) = t match {
case t @ TypeParamRef(b, n) if b `eq` caseLambda =>
inst(n) = approximation(t, fromBelow = variance >= 0).simplified
inst

def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]:
def apply(insts: Array[Type], t: Type) = t match
case param @ TypeParamRef(b, n) if b eq caseLambda =>
insts(n) = {
if canApprox then
approximation(param, fromBelow = variance >= 0)
else constraint.entry(param) match
case entry: TypeBounds =>
val lo = fullLowerBound(param)
val hi = fullUpperBound(param)
if isSubType(hi, lo) then lo else TypeBounds(lo, hi)
case inst =>
assert(inst.exists, i"param = $param\nconstraint = $constraint")
inst
}.simplified
insts
case _ =>
foldOver(inst, t)
}
}
foldOver(insts, t)

def instantiateParams(inst: Array[Type]) = new TypeMap {
def apply(t: Type) = t match {
Expand All @@ -2911,7 +2936,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
* None if the match fails and we should consider the following cases
* because scrutinee and pattern do not overlap
*/
def matchCase(cas: Type): Option[Type] = trace(i"match case $cas vs $scrut", matchTypes) {
def matchCase(cas: Type): MatchResult = trace(i"match case $cas vs $scrut", matchTypes) {
val cas1 = cas match {
case cas: HKTypeLambda =>
caseLambda = constrained(cas)
Expand All @@ -2922,34 +2947,48 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {

val defn.MatchCase(pat, body) = cas1: @unchecked

if (isSubType(scrut, pat))
// `scrut` is a subtype of `pat`: *It's a Match!*
Some {
caseLambda match {
case caseLambda: HKTypeLambda =>
val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
instantiateParams(instances)(body).simplified
case _ =>
body
}
}
def matches(canWidenAbstract: Boolean): Boolean =
val saved = this.canWidenAbstract
this.canWidenAbstract = canWidenAbstract
try necessarySubType(scrut, pat)
finally this.canWidenAbstract = saved

def redux(canApprox: Boolean): MatchResult =
caseLambda match
case caseLambda: HKTypeLambda =>
val instances = paramInstances(canApprox)(new Array(caseLambda.paramNames.length), pat)
instances.indices.find(instances(_).isInstanceOf[TypeBounds]) match
case Some(i) if !canApprox =>
MatchResult.NoInstance(caseLambda.paramNames(i), instances(i).bounds)
case _ =>
MatchResult.Reduced(instantiateParams(instances)(body).simplified)
case _ =>
MatchResult.Reduced(body)

if caseLambda.exists && matches(canWidenAbstract = false) then
redux(canApprox = true)
else if matches(canWidenAbstract = true) then
redux(canApprox = false)
else if (provablyDisjoint(scrut, pat))
// We found a proof that `scrut` and `pat` are incompatible.
// The search continues.
None
MatchResult.Disjoint
else
Some(NoType)
MatchResult.Stuck
}

def recur(remaining: List[Type]): Type = remaining match
case cas :: remaining1 =>
matchCase(cas) match
case None =>
case MatchResult.Disjoint =>
recur(remaining1)
case Some(NoType) =>
case MatchResult.Stuck =>
MatchTypeTrace.stuck(scrut, cas, remaining1)
NoType
case Some(tp) =>
case MatchResult.NoInstance(pname, bounds) =>
MatchTypeTrace.noInstance(scrut, cas, pname, bounds)
NoType
case MatchResult.Reduced(tp) =>
tp
case Nil =>
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)
Expand Down
1 change: 1 addition & 0 deletions compiler/test/dotty/tools/dotc/CompilationTests.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -200,6 +200,7 @@ class CompilationTests {
@Test def runAll: Unit = {
implicit val testGroup: TestGroup = TestGroup("runAll")
aggregateTests(
compileFile("tests/run-custom-args/typeclass-derivation1.scala", defaultOptions.without(yCheckOptions*)),
compileFile("tests/run-custom-args/tuple-cons.scala", allowDeepSubtypes),
compileFile("tests/run-custom-args/i5256.scala", allowDeepSubtypes),
compileFile("tests/run-custom-args/no-useless-forwarders.scala", defaultOptions and "-Xmixin-force-forwarders:false"),
Expand Down
30 changes: 30 additions & 0 deletions tests/neg/6570-1.check
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:23:27 ------------------------------------------------------------
23 | def thing = new Trait1 {} // error
| ^
| Found: Object with Trait1 {...}
| Required: N[Box[Int & String]]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce N[Box[Int & String]]
| failed since selector Box[Int & String]
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:36:54 ------------------------------------------------------------
36 | def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing // error
| ^^^^^^^
| Found: M[T]
| Required: Trait2
|
| where: T is a type in method foo with bounds <: Cov[Box[Int]]
|
|
| Note: a match type could not be fully reduced:
|
| trying to reduce M[T]
| failed since selector T
| does not uniquely determine parameter x in case Cov[x] => N[x]
| The computed bounds for the parameter are: >: Box[Int].
|
| longer explanation available when compiling with `-explain`
2 changes: 1 addition & 1 deletion tests/neg/6570-1.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ class Asploder extends Root[Cov[Box[Int & String]]] {
}

object Main {
def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing
def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing // error
def explode = foo(new Asploder)

def main(args: Array[String]): Unit =
Expand Down
6 changes: 3 additions & 3 deletions tests/neg/6570.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ object UpperBoundParametricVariant {
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
def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing // error

class Asploder extends Child[Cov[String & Int]] {
def thing = new Trait1 {} // error
Expand All @@ -42,7 +42,7 @@ object InheritanceVariant {

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

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

class Asploder extends Child {
type B = { type A = String & Int }
Expand Down Expand Up @@ -98,7 +98,7 @@ object UpperBoundVariant {

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

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

class Asploder extends Child {
type A = Cov[String & Int]
Expand Down
39 changes: 39 additions & 0 deletions tests/neg/i11982.check
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
-- [E057] Type Mismatch Error: tests/neg/i11982.scala:9:34 -------------------------------------------------------------
9 | b: ValueOf[Tuple.Head[Tuple.Tail[X]]] // error
| ^
| Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Tuple.Tail[X]
| failed since selector X
| does not uniquely determine parameter xs in case _ *: xs => xs
| The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple.
|
| longer explanation available when compiling with `-explain`
-- [E057] Type Mismatch Error: tests/neg/i11982.scala:10:38 ------------------------------------------------------------
10 | ): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] = // error
| ^
| Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Tuple.Tail[X]
| failed since selector X
| does not uniquely determine parameter xs in case _ *: xs => xs
| The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple.
|
| longer explanation available when compiling with `-explain`
-- [E057] Type Mismatch Error: tests/neg/i11982.scala:12:25 ------------------------------------------------------------
12 | type BB = Tuple.Head[Tuple.Tail[X]] // error
| ^
| Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Tuple.Tail[X]
| failed since selector X
| does not uniquely determine parameter xs in case _ *: xs => xs
| The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple.
|
| longer explanation available when compiling with `-explain`
27 changes: 27 additions & 0 deletions tests/neg/i11982.scala
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
package tuplefun
object Unpair {

def pair[A, B](using a: ValueOf[A], b: ValueOf[B]): Tuple2[A, B] =
(a.value, b.value)

def unpair[X <: Tuple2[?, ?]](
using a: ValueOf[Tuple.Head[X]],
b: ValueOf[Tuple.Head[Tuple.Tail[X]]] // error
): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] = // error
type AA = Tuple.Head[X]
type BB = Tuple.Head[Tuple.Tail[X]] // error
pair[AA, BB](using a, b)
}

object UnpairApp {
import Unpair._

type Tshape = ("msg", 42)

// the following won't compile when in the same file as Unpair
val p1: ("msg", 42) = unpair[Tshape]

@main def pairHello: Unit =
assert(p1 == ("msg", 42))
println(p1)
}
34 changes: 34 additions & 0 deletions tests/neg/i13780.check
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
-- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------
18 | def int[X <: Y]: Int = unpair[X] // error
| ^^^^^^^^^
| Found: Head[X]
| Required: Int
|
| where: X is a type in method int with bounds <: B.this.Y
|
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Head[X]
| failed since selector X
| does not uniquely determine parameter a in case (a, b) => a
| The computed bounds for the parameter are: >: Int.
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/i13780.scala:23:37 ------------------------------------------------------------
23 | def string[X <: Y]: String = unpair[X] // error
| ^^^^^^^^^
| Found: Head[X]
| Required: String
|
| where: X is a type in method string with bounds <: C.this.Y
|
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Head[X]
| failed since selector X
| does not uniquely determine parameter a in case (a, b) => a
| The computed bounds for the parameter are: >: String.
|
| longer explanation available when compiling with `-explain`
Loading

0 comments on commit de9c544

Please sign in to comment.