Skip to content

Commit 6a85b09

Browse files
committed
Fix reachability of non-reducing match type children
The reduction of a match type gets "stuck" when a case doesn't match but is also not provably disjoint from it. In these situations the match type reduction returns NoType, which means that in `A <:< B` if B reduces to NoType, then false will be returned. In the reachability/Space logic subtype checks are used to refine the candidate children of the scrutinee type so that impossible children aren't marked as missing and possible cases aren't marked as unreachable. To achieve that there is already some type mapping that runs before subtyping to approximate the parent. We extend that parent approximating logic so that non-reducing match types in the parent don't result in all the candidate children being rejected. The motivating case is NonEmptyTuple, its single-child `*:`, and the `Tuple.Tail` match type. In `Tuple.Tail[NonEmptyTuple]`, `case _ *: xs =>` won't match because NonEmptyTuple isn't a subtype of `*:` but it's also not provably disjoint from it (indeed it's `*:` parent)! So the reduction gets stuck, leading to NoType, leading to not a subtype. I had initially looked to fix this for single-child abstract sealed types, but that would still cause false positives in legitimate multi-child sealed types and an exhaustive match type (see WithExhaustiveMatch in patmat/i13189.scala). Also it's less scary to change the subtyping wrapping logic rather than the actually match type's reduction/matching logic. In a way the problem is that subtyping checks is too boolean: the candidate rejection wants to drop children that are definitely not subtypes, but the match type reduction is too conservative by returning NoType as soon as the obvious case isn't met. What subtyping should say there is ¯\_(ツ)_/¯
1 parent 525f4a5 commit 6a85b09

File tree

3 files changed

+98
-7
lines changed

3 files changed

+98
-7
lines changed

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

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -702,13 +702,18 @@ object TypeOps:
702702
//
703703
// 1. Replace type parameters in T with tvars
704704
// 2. Replace `A.this.C` with `A#C` (see tests/patmat/i12681.scala)
705+
// 3. Replace non-reducing MatchType to its bound
705706
//
706707
val approximateParent = new TypeMap {
707708
val boundTypeParams = util.HashMap[TypeRef, TypeVar]()
708709

709710
def apply(tp: Type): Type = tp.dealias match {
710-
case _: MatchType =>
711-
tp // break cycles
711+
case tp: MatchType =>
712+
val reduced = tp.reduced
713+
if reduced.exists then tp // break cycles
714+
else mapOver(tp.bound) // if the match type doesn't statically reduce
715+
// then to avoid it failing the <:<
716+
// we'll approximate by widening to its bounds
712717

713718
case ThisType(tref: TypeRef) if !tref.symbol.isStaticOwner =>
714719
tref
@@ -729,7 +734,7 @@ object TypeOps:
729734
tv
730735
end if
731736

732-
case AppliedType(tycon: TypeRef, _) if !tycon.dealias.typeSymbol.isClass =>
737+
case tp @ AppliedType(tycon: TypeRef, _) if !tycon.dealias.typeSymbol.isClass && !tp.isMatchAlias =>
733738

734739
// In tests/patmat/i3645g.scala, we need to tell whether it's possible
735740
// that K1 <: K[Foo]. If yes, we issue a warning; otherwise, no

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

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -427,10 +427,7 @@ object Types {
427427
def isMatch(using Context): Boolean = stripped match {
428428
case _: MatchType => true
429429
case tp: HKTypeLambda => tp.resType.isMatch
430-
case tp: AppliedType =>
431-
tp.tycon match
432-
case tycon: TypeRef => tycon.info.isInstanceOf[MatchAlias]
433-
case _ => false
430+
case tp: AppliedType => tp.isMatchAlias
434431
case _ => false
435432
}
436433

tests/patmat/i13189.scala

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
// original report
2+
def foo(opt: Option[Tuple.Tail[NonEmptyTuple]]): Unit =
3+
opt match
4+
case None => ???
5+
case Some(a) => ???
6+
7+
8+
// again with a mini-Tuple with the extra NonEmptyTupExtra parent, to test transitivity
9+
object WithExtraParent:
10+
sealed trait Tup
11+
12+
object Tup {
13+
type Tail[X <: NonEmptyTup] <: Tup = X match {
14+
case _ **: xs => xs
15+
}
16+
}
17+
18+
object EmptyTup extends Tup
19+
20+
sealed trait NonEmptyTup extends Tup
21+
sealed trait NonEmptyTupExtra extends NonEmptyTup
22+
sealed abstract class **:[+H, +T <: Tup] extends NonEmptyTupExtra
23+
24+
object **: {
25+
def unapply[H, T <: Tup](x: H **: T): (H, T) = null
26+
}
27+
28+
def foo(opt: Option[Tup.Tail[NonEmptyTup]]): Unit =
29+
opt match
30+
case None => ???
31+
case Some(a) => ???
32+
end WithExtraParent
33+
34+
35+
// again with a non-abstract parent
36+
object WithNonAbstractParent:
37+
sealed trait Tup
38+
39+
object Tup {
40+
type Tail[X <: NonEmptyTup] <: Tup = X match {
41+
case _ **: xs => xs
42+
}
43+
}
44+
45+
object EmptyTup extends Tup
46+
47+
sealed class NonEmptyTup extends Tup
48+
sealed class **:[+H, +T <: Tup] extends NonEmptyTup
49+
50+
object **: {
51+
def unapply[H, T <: Tup](x: H **: T): (H, T) = null
52+
}
53+
54+
def foo(opt: Option[Tup.Tail[NonEmptyTup]]): Unit =
55+
opt match
56+
case None => ???
57+
case Some(a) => ???
58+
end WithNonAbstractParent
59+
60+
61+
// again with multiple children, but an exhaustive match
62+
object WithExhaustiveMatch:
63+
sealed trait Tup
64+
65+
object Tup {
66+
type Tail[X <: NonEmptyTup] <: Tup = X match {
67+
case _ **: xs => xs
68+
case _ *+: xs => xs
69+
}
70+
}
71+
72+
object EmptyTup extends Tup
73+
74+
sealed trait NonEmptyTup extends Tup
75+
sealed abstract class **:[+H, +T <: Tup] extends NonEmptyTup
76+
sealed abstract class *+:[+H, +T <: Tup] extends NonEmptyTup
77+
78+
object **: {
79+
def unapply[H, T <: Tup](x: H **: T): (H, T) = null
80+
}
81+
object *+: {
82+
def unapply[H, T <: Tup](x: H *+: T): (H, T) = null
83+
}
84+
85+
def foo(opt: Option[Tup.Tail[NonEmptyTup]]): Unit =
86+
opt match
87+
case None => ???
88+
case Some(a) => ???
89+
end WithExhaustiveMatch

0 commit comments

Comments
 (0)