Skip to content

Commit

Permalink
Merge pull request #15423 from dotty-staging/fix-11982
Browse files Browse the repository at this point in the history
Refine Matchtype checking
  • Loading branch information
odersky authored Jun 19, 2022
2 parents 1f813bc + e9c4539 commit 4cb967f
Show file tree
Hide file tree
Showing 16 changed files with 356 additions and 44 deletions.
14 changes: 13 additions & 1 deletion compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala
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, fails: List[(Name, 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, fails: List[(Name, TypeBounds)])(using Context) =
matchTypeFail(NoInstance(scrut, stuckCase, fails))

/** Record a failure that scrutinee `scrut` is provably empty.
* Only the first failure is recorded.
*/
Expand All @@ -82,7 +87,7 @@ object MatchTypeTrace:
case _ =>
op

private def caseText(tp: Type)(using Context): String = tp match
def caseText(tp: Type)(using Context): String = tp match
case tp: HKTypeLambda => caseText(tp.resultType)
case defn.MatchCase(any, body) if any eq defn.AnyType => i"case _ => $body"
case defn.MatchCase(pat, body) => i"case $pat => $body"
Expand Down Expand Up @@ -114,6 +119,13 @@ object MatchTypeTrace:
| Therefore, reduction cannot advance to the remaining case$s
|
| ${casesText(otherCases)}"""
case NoInstance(scrut, stuckCase, fails) =>
def params = if fails.length == 1 then "parameter" else "parameters"
i""" failed since selector $scrut
| does not uniquely determine $params ${fails.map(_._1)}%, % in
| ${caseText(stuckCase)}
| The computed bounds for the $params are:
| ${fails.map((name, bounds) => i"$name$bounds")}%\n %"""

def noMatchesText(scrut: Type, cases: List[Type])(using Context): String =
i"""failed since selector $scrut
Expand Down
112 changes: 75 additions & 37 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
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 @@ -2851,7 +2857,16 @@ object TypeComparer {
comparing(_.tracked(op))
}

object TrackingTypeComparer:
enum MatchResult:
case Reduced(tp: Type)
case Disjoint
case Stuck
case NoInstance(fails: List[(Name, TypeBounds)])

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

init(initctx)

override def trackingTypeComparer = this
Expand Down Expand Up @@ -2889,31 +2904,36 @@ 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).simplified
else constraint.entry(param) match
case entry: TypeBounds =>
val lo = fullLowerBound(param)
val hi = fullUpperBound(param)
if isSubType(hi, lo) then lo.simplified else Range(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 instantiateParams(insts: Array[Type]) = new ApproximatingTypeMap {
variance = 0
def apply(t: Type) = t match {
case t @ TypeParamRef(b, n) if b `eq` caseLambda => inst(n)
case t @ TypeParamRef(b, n) if b `eq` caseLambda => insts(n)
case t: LazyRef => apply(t.ref)
case _ => mapOver(t)
}
}

/** Match a single case.
* @return Some(tp) if the match succeeds with type `tp`
* Some(NoType) if the match fails, and there is an overlap between pattern and scrutinee
* 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) {
/** Match a single case. */
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 @@ -2924,34 +2944,52 @@ 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)
instantiateParams(instances)(body) match
case Range(lo, hi) =>
MatchResult.NoInstance {
caseLambda.paramNames.zip(instances).collect {
case (name, Range(lo, hi)) => (name, TypeBounds(lo, hi))
}
}
case redux =>
MatchResult.Reduced(redux.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(fails) =>
MatchTypeTrace.noInstance(scrut, cas, fails)
NoType
case MatchResult.Reduced(tp) =>
tp
case Nil =>
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)
Expand Down
10 changes: 8 additions & 2 deletions compiler/src/dotty/tools/dotc/core/Types.scala
Original file line number Diff line number Diff line change
Expand Up @@ -5755,7 +5755,13 @@ object Types {
case _ =>
scrutinee match
case Range(lo, hi) => range(bound.bounds.lo, bound.bounds.hi)
case _ => tp.derivedMatchType(bound, scrutinee, cases)
case _ =>
if cases.exists(isRange) then
Range(
tp.derivedMatchType(bound, scrutinee, cases.map(lower)),
tp.derivedMatchType(bound, scrutinee, cases.map(upper)))
else
tp.derivedMatchType(bound, scrutinee, cases)

override protected def derivedSkolemType(tp: SkolemType, info: Type): Type =
if info eq tp.info then tp
Expand Down Expand Up @@ -5791,7 +5797,7 @@ object Types {
/** A range of possible types between lower bound `lo` and upper bound `hi`.
* Only used internally in `ApproximatingTypeMap`.
*/
private case class Range(lo: Type, hi: Type) extends UncachedGroundType {
case class Range(lo: Type, hi: Type) extends UncachedGroundType {
assert(!lo.isInstanceOf[Range])
assert(!hi.isInstanceOf[Range])

Expand Down
1 change: 1 addition & 0 deletions compiler/test/dotty/tools/dotc/CompilationTests.scala
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
32 changes: 32 additions & 0 deletions tests/neg/6570-1.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
-- [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:
| x >: Box[Int]
|
| longer explanation available when compiling with `-explain`
2 changes: 1 addition & 1 deletion tests/neg/6570-1.scala
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
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
4 changes: 4 additions & 0 deletions tests/neg/i11982.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- Error: tests/neg/i11982.scala:22:38 ---------------------------------------------------------------------------------
22 | val p1: ("msg", 42) = unpair[Tshape] // error: no singleton value for Any
| ^
| No singleton value available for Any.
27 changes: 27 additions & 0 deletions tests/neg/i11982.scala
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]]]
): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] =
type AA = Tuple.Head[X]
type BB = Tuple.Head[Tuple.Tail[X]]
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] // error: no singleton value for Any

@main def pairHello: Unit =
assert(p1 == ("msg", 42))
println(p1)
}
Loading

0 comments on commit 4cb967f

Please sign in to comment.