Skip to content

Commit 6e7adfc

Browse files
authored
Merge pull request #15500 from dotty-staging/backport-15423
Backport #15423: Refine Matchtype checking
2 parents 8e63cb4 + e0b563d commit 6e7adfc

16 files changed

+356
-44
lines changed

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

+13-1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ package core
44

55
import Types._, Contexts._, Symbols._, Decorators._
66
import util.Property
7+
import Names.Name
78

89
/** A utility module to produce match type reduction traces in error messages.
910
*/
@@ -13,6 +14,7 @@ object MatchTypeTrace:
1314
case TryReduce(scrut: Type)
1415
case NoMatches(scrut: Type, cases: List[Type])
1516
case Stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])
17+
case NoInstance(scrut: Type, stuckCase: Type, fails: List[(Name, TypeBounds)])
1618
case EmptyScrutinee(scrut: Type)
1719
import TraceEntry._
1820

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

67+
def noInstance(scrut: Type, stuckCase: Type, fails: List[(Name, TypeBounds)])(using Context) =
68+
matchTypeFail(NoInstance(scrut, stuckCase, fails))
69+
6570
/** Record a failure that scrutinee `scrut` is provably empty.
6671
* Only the first failure is recorded.
6772
*/
@@ -82,7 +87,7 @@ object MatchTypeTrace:
8287
case _ =>
8388
op
8489

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

118130
def noMatchesText(scrut: Type, cases: List[Type])(using Context): String =
119131
i"""failed since selector $scrut

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

+75-37
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
6060
/** Indicates whether the subtype check used GADT bounds */
6161
private var GADTused: Boolean = false
6262

63+
protected var canWidenAbstract: Boolean = true
64+
6365
private var myInstance: TypeComparer = this
6466
def currentInstance: TypeComparer = myInstance
6567

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

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

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

2858+
object TrackingTypeComparer:
2859+
enum MatchResult:
2860+
case Reduced(tp: Type)
2861+
case Disjoint
2862+
case Stuck
2863+
case NoInstance(fails: List[(Name, TypeBounds)])
2864+
28522865
class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
2866+
import TrackingTypeComparer.*
2867+
28532868
init(initctx)
28542869

28552870
override def trackingTypeComparer = this
@@ -2887,31 +2902,36 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
28872902
}
28882903

28892904
def matchCases(scrut: Type, cases: List[Type])(using Context): Type = {
2890-
def paramInstances = new TypeAccumulator[Array[Type]] {
2891-
def apply(inst: Array[Type], t: Type) = t match {
2892-
case t @ TypeParamRef(b, n) if b `eq` caseLambda =>
2893-
inst(n) = approximation(t, fromBelow = variance >= 0).simplified
2894-
inst
2905+
2906+
def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]:
2907+
def apply(insts: Array[Type], t: Type) = t match
2908+
case param @ TypeParamRef(b, n) if b eq caseLambda =>
2909+
insts(n) =
2910+
if canApprox then
2911+
approximation(param, fromBelow = variance >= 0).simplified
2912+
else constraint.entry(param) match
2913+
case entry: TypeBounds =>
2914+
val lo = fullLowerBound(param)
2915+
val hi = fullUpperBound(param)
2916+
if isSubType(hi, lo) then lo.simplified else Range(lo, hi)
2917+
case inst =>
2918+
assert(inst.exists, i"param = $param\nconstraint = $constraint")
2919+
inst.simplified
2920+
insts
28952921
case _ =>
2896-
foldOver(inst, t)
2897-
}
2898-
}
2922+
foldOver(insts, t)
28992923

2900-
def instantiateParams(inst: Array[Type]) = new TypeMap {
2924+
def instantiateParams(insts: Array[Type]) = new ApproximatingTypeMap {
2925+
variance = 0
29012926
def apply(t: Type) = t match {
2902-
case t @ TypeParamRef(b, n) if b `eq` caseLambda => inst(n)
2927+
case t @ TypeParamRef(b, n) if b `eq` caseLambda => insts(n)
29032928
case t: LazyRef => apply(t.ref)
29042929
case _ => mapOver(t)
29052930
}
29062931
}
29072932

2908-
/** Match a single case.
2909-
* @return Some(tp) if the match succeeds with type `tp`
2910-
* Some(NoType) if the match fails, and there is an overlap between pattern and scrutinee
2911-
* None if the match fails and we should consider the following cases
2912-
* because scrutinee and pattern do not overlap
2913-
*/
2914-
def matchCase(cas: Type): Option[Type] = trace(i"match case $cas vs $scrut", matchTypes) {
2933+
/** Match a single case. */
2934+
def matchCase(cas: Type): MatchResult = trace(i"match case $cas vs $scrut", matchTypes) {
29152935
val cas1 = cas match {
29162936
case cas: HKTypeLambda =>
29172937
caseLambda = constrained(cas)
@@ -2922,34 +2942,52 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
29222942

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

2925-
if (isSubType(scrut, pat))
2926-
// `scrut` is a subtype of `pat`: *It's a Match!*
2927-
Some {
2928-
caseLambda match {
2929-
case caseLambda: HKTypeLambda =>
2930-
val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
2931-
instantiateParams(instances)(body).simplified
2932-
case _ =>
2933-
body
2934-
}
2935-
}
2945+
def matches(canWidenAbstract: Boolean): Boolean =
2946+
val saved = this.canWidenAbstract
2947+
this.canWidenAbstract = canWidenAbstract
2948+
try necessarySubType(scrut, pat)
2949+
finally this.canWidenAbstract = saved
2950+
2951+
def redux(canApprox: Boolean): MatchResult =
2952+
caseLambda match
2953+
case caseLambda: HKTypeLambda =>
2954+
val instances = paramInstances(canApprox)(new Array(caseLambda.paramNames.length), pat)
2955+
instantiateParams(instances)(body) match
2956+
case Range(lo, hi) =>
2957+
MatchResult.NoInstance {
2958+
caseLambda.paramNames.zip(instances).collect {
2959+
case (name, Range(lo, hi)) => (name, TypeBounds(lo, hi))
2960+
}
2961+
}
2962+
case redux =>
2963+
MatchResult.Reduced(redux.simplified)
2964+
case _ =>
2965+
MatchResult.Reduced(body)
2966+
2967+
if caseLambda.exists && matches(canWidenAbstract = false) then
2968+
redux(canApprox = true)
2969+
else if matches(canWidenAbstract = true) then
2970+
redux(canApprox = false)
29362971
else if (provablyDisjoint(scrut, pat))
29372972
// We found a proof that `scrut` and `pat` are incompatible.
29382973
// The search continues.
2939-
None
2974+
MatchResult.Disjoint
29402975
else
2941-
Some(NoType)
2976+
MatchResult.Stuck
29422977
}
29432978

29442979
def recur(remaining: List[Type]): Type = remaining match
29452980
case cas :: remaining1 =>
29462981
matchCase(cas) match
2947-
case None =>
2982+
case MatchResult.Disjoint =>
29482983
recur(remaining1)
2949-
case Some(NoType) =>
2984+
case MatchResult.Stuck =>
29502985
MatchTypeTrace.stuck(scrut, cas, remaining1)
29512986
NoType
2952-
case Some(tp) =>
2987+
case MatchResult.NoInstance(fails) =>
2988+
MatchTypeTrace.noInstance(scrut, cas, fails)
2989+
NoType
2990+
case MatchResult.Reduced(tp) =>
29532991
tp
29542992
case Nil =>
29552993
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)

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

+8-2
Original file line numberDiff line numberDiff line change
@@ -5977,7 +5977,13 @@ object Types {
59775977
case _ =>
59785978
scrutinee match
59795979
case Range(lo, hi) => range(bound.bounds.lo, bound.bounds.hi)
5980-
case _ => tp.derivedMatchType(bound, scrutinee, cases)
5980+
case _ =>
5981+
if cases.exists(isRange) then
5982+
Range(
5983+
tp.derivedMatchType(bound, scrutinee, cases.map(lower)),
5984+
tp.derivedMatchType(bound, scrutinee, cases.map(upper)))
5985+
else
5986+
tp.derivedMatchType(bound, scrutinee, cases)
59815987

59825988
override protected def derivedSkolemType(tp: SkolemType, info: Type): Type =
59835989
if info eq tp.info then tp
@@ -6013,7 +6019,7 @@ object Types {
60136019
/** A range of possible types between lower bound `lo` and upper bound `hi`.
60146020
* Only used internally in `ApproximatingTypeMap`.
60156021
*/
6016-
private case class Range(lo: Type, hi: Type) extends UncachedGroundType {
6022+
case class Range(lo: Type, hi: Type) extends UncachedGroundType {
60176023
assert(!lo.isInstanceOf[Range])
60186024
assert(!hi.isInstanceOf[Range])
60196025

compiler/test/dotty/tools/dotc/CompilationTests.scala

+1
Original file line numberDiff line numberDiff line change
@@ -200,6 +200,7 @@ class CompilationTests {
200200
@Test def runAll: Unit = {
201201
implicit val testGroup: TestGroup = TestGroup("runAll")
202202
aggregateTests(
203+
compileFile("tests/run-custom-args/typeclass-derivation1.scala", defaultOptions.without(yCheckOptions*)),
203204
compileFile("tests/run-custom-args/tuple-cons.scala", allowDeepSubtypes),
204205
compileFile("tests/run-custom-args/i5256.scala", allowDeepSubtypes),
205206
compileFile("tests/run-custom-args/no-useless-forwarders.scala", defaultOptions and "-Xmixin-force-forwarders:false"),

tests/neg/6570-1.check

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:23:27 ------------------------------------------------------------
2+
23 | def thing = new Trait1 {} // error
3+
| ^
4+
| Found: Object with Trait1 {...}
5+
| Required: N[Box[Int & String]]
6+
|
7+
| Note: a match type could not be fully reduced:
8+
|
9+
| trying to reduce N[Box[Int & String]]
10+
| failed since selector Box[Int & String]
11+
| is uninhabited (there are no values of that type).
12+
|
13+
| longer explanation available when compiling with `-explain`
14+
-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:36:54 ------------------------------------------------------------
15+
36 | def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing // error
16+
| ^^^^^^^
17+
| Found: M[T]
18+
| Required: Trait2
19+
|
20+
| where: T is a type in method foo with bounds <: Cov[Box[Int]]
21+
|
22+
|
23+
| Note: a match type could not be fully reduced:
24+
|
25+
| trying to reduce M[T]
26+
| failed since selector T
27+
| does not uniquely determine parameter x in
28+
| case Cov[x] => N[x]
29+
| The computed bounds for the parameter are:
30+
| x >: Box[Int]
31+
|
32+
| longer explanation available when compiling with `-explain`

tests/neg/6570-1.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ class Asploder extends Root[Cov[Box[Int & String]]] {
3333
}
3434

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

3939
def main(args: Array[String]): Unit =

tests/neg/6570.scala

+3-3
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ object UpperBoundParametricVariant {
2121
trait Child[A <: Cov[Int]] extends Root[A]
2222

2323
// we reduce `M[T]` to `Trait2`, even though we cannot be certain of that
24-
def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing
24+
def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing // error
2525

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

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

45-
def foo(c: Child): Trait2 = c.thing
45+
def foo(c: Child): Trait2 = c.thing // error
4646

4747
class Asploder extends Child {
4848
type B = { type A = String & Int }
@@ -98,7 +98,7 @@ object UpperBoundVariant {
9898

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

101-
def foo(c: Child): Trait2 = c.thing
101+
def foo(c: Child): Trait2 = c.thing // error
102102

103103
class Asploder extends Child {
104104
type A = Cov[String & Int]

tests/neg/i11982.check

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
-- Error: tests/neg/i11982.scala:22:38 ---------------------------------------------------------------------------------
2+
22 | val p1: ("msg", 42) = unpair[Tshape] // error: no singleton value for Any
3+
| ^
4+
| No singleton value available for Any.

tests/neg/i11982.scala

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
package tuplefun
2+
object Unpair {
3+
4+
def pair[A, B](using a: ValueOf[A], b: ValueOf[B]): Tuple2[A, B] =
5+
(a.value, b.value)
6+
7+
def unpair[X <: Tuple2[?, ?]](
8+
using a: ValueOf[Tuple.Head[X]],
9+
b: ValueOf[Tuple.Head[Tuple.Tail[X]]]
10+
): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] =
11+
type AA = Tuple.Head[X]
12+
type BB = Tuple.Head[Tuple.Tail[X]]
13+
pair[AA, BB](using a, b)
14+
}
15+
16+
object UnpairApp {
17+
import Unpair._
18+
19+
type Tshape = ("msg", 42)
20+
21+
// the following won't compile when in the same file as Unpair
22+
val p1: ("msg", 42) = unpair[Tshape] // error: no singleton value for Any
23+
24+
@main def pairHello: Unit =
25+
assert(p1 == ("msg", 42))
26+
println(p1)
27+
}

0 commit comments

Comments
 (0)