Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refine Matchtype checking #15423

Merged
merged 4 commits into from
Jun 19, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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 @@ -2845,7 +2851,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 @@ -2883,31 +2898,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 @@ -2918,34 +2938,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 @@ -5953,7 +5953,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 @@ -5989,7 +5995,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