Skip to content

Commit d9ef974

Browse files
oderskyodersky
committed
Refine Matchtype checking
Take up #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 #11982
1 parent cec9aa3 commit d9ef974

File tree

12 files changed

+288
-33
lines changed

12 files changed

+288
-33
lines changed

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

Lines changed: 9 additions & 0 deletions
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, pname: Name, bounds: 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, pname: Name, bounds: TypeBounds)(using Context) =
68+
matchTypeFail(NoInstance(scrut, stuckCase, pname, bounds))
69+
6570
/** Record a failure that scrutinee `scrut` is provably empty.
6671
* Only the first failure is recorded.
6772
*/
@@ -114,6 +119,10 @@ object MatchTypeTrace:
114119
| Therefore, reduction cannot advance to the remaining case$s
115120
|
116121
| ${casesText(otherCases)}"""
122+
case NoInstance(scrut, stuckCase, pname, bounds) =>
123+
i""" failed since selector $scrut
124+
| does not uniquely determine parameter $pname in ${caseText(stuckCase)}
125+
| The computed bounds for the parameter are: $bounds."""
117126

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

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

Lines changed: 68 additions & 29 deletions
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
@@ -2845,7 +2851,16 @@ object TypeComparer {
28452851
comparing(_.tracked(op))
28462852
}
28472853

2854+
object TrackingTypeComparer:
2855+
enum MatchResult:
2856+
case Reduced(tp: Type)
2857+
case Disjoint
2858+
case Stuck
2859+
case NoInstance(param: Name, bounds: TypeBounds)
2860+
28482861
class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
2862+
import TrackingTypeComparer.*
2863+
28492864
init(initctx)
28502865

28512866
override def trackingTypeComparer = this
@@ -2883,15 +2898,25 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
28832898
}
28842899

28852900
def matchCases(scrut: Type, cases: List[Type])(using Context): Type = {
2886-
def paramInstances = new TypeAccumulator[Array[Type]] {
2887-
def apply(inst: Array[Type], t: Type) = t match {
2888-
case t @ TypeParamRef(b, n) if b `eq` caseLambda =>
2889-
inst(n) = approximation(t, fromBelow = variance >= 0).simplified
2890-
inst
2901+
2902+
def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]:
2903+
def apply(insts: Array[Type], t: Type) = t match
2904+
case param @ TypeParamRef(b, n) if b eq caseLambda =>
2905+
insts(n) = {
2906+
if canApprox then
2907+
approximation(param, fromBelow = variance >= 0)
2908+
else constraint.entry(param) match
2909+
case entry: TypeBounds =>
2910+
val lo = fullLowerBound(param)
2911+
val hi = fullUpperBound(param)
2912+
if isSubType(hi, lo) then lo else TypeBounds(lo, hi)
2913+
case inst =>
2914+
assert(inst.exists, i"param = $param\nconstraint = $constraint")
2915+
inst
2916+
}.simplified
2917+
insts
28912918
case _ =>
2892-
foldOver(inst, t)
2893-
}
2894-
}
2919+
foldOver(insts, t)
28952920

28962921
def instantiateParams(inst: Array[Type]) = new TypeMap {
28972922
def apply(t: Type) = t match {
@@ -2907,7 +2932,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
29072932
* None if the match fails and we should consider the following cases
29082933
* because scrutinee and pattern do not overlap
29092934
*/
2910-
def matchCase(cas: Type): Option[Type] = trace(i"match case $cas vs $scrut", matchTypes) {
2935+
def matchCase(cas: Type): MatchResult = trace(i"match case $cas vs $scrut", matchTypes) {
29112936
val cas1 = cas match {
29122937
case cas: HKTypeLambda =>
29132938
caseLambda = constrained(cas)
@@ -2918,34 +2943,48 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
29182943

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

2921-
if (isSubType(scrut, pat))
2922-
// `scrut` is a subtype of `pat`: *It's a Match!*
2923-
Some {
2924-
caseLambda match {
2925-
case caseLambda: HKTypeLambda =>
2926-
val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
2927-
instantiateParams(instances)(body).simplified
2928-
case _ =>
2929-
body
2930-
}
2931-
}
2946+
def matches(canWidenAbstract: Boolean): Boolean =
2947+
val saved = this.canWidenAbstract
2948+
this.canWidenAbstract = canWidenAbstract
2949+
try necessarySubType(scrut, pat)
2950+
finally this.canWidenAbstract = saved
2951+
2952+
def redux(canApprox: Boolean): MatchResult =
2953+
caseLambda match
2954+
case caseLambda: HKTypeLambda =>
2955+
val instances = paramInstances(canApprox)(new Array(caseLambda.paramNames.length), pat)
2956+
instances.indices.find(instances(_).isInstanceOf[TypeBounds]) match
2957+
case Some(i) if !canApprox =>
2958+
MatchResult.NoInstance(caseLambda.paramNames(i), instances(i).bounds)
2959+
case _ =>
2960+
MatchResult.Reduced(instantiateParams(instances)(body).simplified)
2961+
case _ =>
2962+
MatchResult.Reduced(body)
2963+
2964+
if caseLambda.exists && matches(canWidenAbstract = false) then
2965+
redux(canApprox = true)
2966+
else if matches(canWidenAbstract = true) then
2967+
redux(canApprox = false)
29322968
else if (provablyDisjoint(scrut, pat))
29332969
// We found a proof that `scrut` and `pat` are incompatible.
29342970
// The search continues.
2935-
None
2971+
MatchResult.Disjoint
29362972
else
2937-
Some(NoType)
2973+
MatchResult.Stuck
29382974
}
29392975

29402976
def recur(remaining: List[Type]): Type = remaining match
29412977
case cas :: remaining1 =>
29422978
matchCase(cas) match
2943-
case None =>
2979+
case MatchResult.Disjoint =>
29442980
recur(remaining1)
2945-
case Some(NoType) =>
2981+
case MatchResult.Stuck =>
29462982
MatchTypeTrace.stuck(scrut, cas, remaining1)
29472983
NoType
2948-
case Some(tp) =>
2984+
case MatchResult.NoInstance(pname, bounds) =>
2985+
MatchTypeTrace.noInstance(scrut, cas, pname, bounds)
2986+
NoType
2987+
case MatchResult.Reduced(tp) =>
29492988
tp
29502989
case Nil =>
29512990
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)

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

Lines changed: 1 addition & 0 deletions
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

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
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 case Cov[x] => N[x]
28+
| The computed bounds for the parameter are: >: Box[Int].
29+
|
30+
| longer explanation available when compiling with `-explain`

‎tests/neg/6570-1.scala

Lines changed: 1 addition & 1 deletion
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
-- [E057] Type Mismatch Error: tests/neg/i11982.scala:9:34 -------------------------------------------------------------
2+
9 | b: ValueOf[Tuple.Head[Tuple.Tail[X]]] // error
3+
| ^
4+
| Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
5+
|
6+
| Note: a match type could not be fully reduced:
7+
|
8+
| trying to reduce Tuple.Tail[X]
9+
| failed since selector X
10+
| does not uniquely determine parameter xs in case _ *: xs => xs
11+
| The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple.
12+
|
13+
| longer explanation available when compiling with `-explain`
14+
-- [E057] Type Mismatch Error: tests/neg/i11982.scala:10:38 ------------------------------------------------------------
15+
10 | ): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] = // error
16+
| ^
17+
| Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
18+
|
19+
| Note: a match type could not be fully reduced:
20+
|
21+
| trying to reduce Tuple.Tail[X]
22+
| failed since selector X
23+
| does not uniquely determine parameter xs in case _ *: xs => xs
24+
| The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple.
25+
|
26+
| longer explanation available when compiling with `-explain`
27+
-- [E057] Type Mismatch Error: tests/neg/i11982.scala:12:25 ------------------------------------------------------------
28+
12 | type BB = Tuple.Head[Tuple.Tail[X]] // error
29+
| ^
30+
| Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
31+
|
32+
| Note: a match type could not be fully reduced:
33+
|
34+
| trying to reduce Tuple.Tail[X]
35+
| failed since selector X
36+
| does not uniquely determine parameter xs in case _ *: xs => xs
37+
| The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple.
38+
|
39+
| longer explanation available when compiling with `-explain`

‎tests/neg/i11982.scala

Lines changed: 27 additions & 0 deletions
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]]] // error
10+
): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] = // error
11+
type AA = Tuple.Head[X]
12+
type BB = Tuple.Head[Tuple.Tail[X]] // error
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]
23+
24+
@main def pairHello: Unit =
25+
assert(p1 == ("msg", 42))
26+
println(p1)
27+
}

‎tests/neg/i13780.check

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
-- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------
2+
18 | def int[X <: Y]: Int = unpair[X] // error
3+
| ^^^^^^^^^
4+
| Found: Head[X]
5+
| Required: Int
6+
|
7+
| where: X is a type in method int with bounds <: B.this.Y
8+
|
9+
|
10+
| Note: a match type could not be fully reduced:
11+
|
12+
| trying to reduce Head[X]
13+
| failed since selector X
14+
| does not uniquely determine parameter a in case (a, b) => a
15+
| The computed bounds for the parameter are: >: Int.
16+
|
17+
| longer explanation available when compiling with `-explain`
18+
-- [E007] Type Mismatch Error: tests/neg/i13780.scala:23:37 ------------------------------------------------------------
19+
23 | def string[X <: Y]: String = unpair[X] // error
20+
| ^^^^^^^^^
21+
| Found: Head[X]
22+
| Required: String
23+
|
24+
| where: X is a type in method string with bounds <: C.this.Y
25+
|
26+
|
27+
| Note: a match type could not be fully reduced:
28+
|
29+
| trying to reduce Head[X]
30+
| failed since selector X
31+
| does not uniquely determine parameter a in case (a, b) => a
32+
| The computed bounds for the parameter are: >: String.
33+
|
34+
| longer explanation available when compiling with `-explain`

0 commit comments

Comments
 (0)