Skip to content

Commit b3ef04f

Browse files
anatoliykmetyukanatoliykmetyuk
authored
Merge pull request #12768 from dotty-staging/fix-10747
Fix #10747: Raise type error on unreducible match type
2 parents 4742767 + 11a2082 commit b3ef04f

13 files changed

+225
-109
lines changed

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

Lines changed: 17 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -102,12 +102,22 @@ object MatchTypeTrace:
102102
i""" failed since selector $scrut
103103
| is uninhabited (there are no values of that type)."""
104104
case Stuck(scrut, stuckCase, otherCases) =>
105-
i""" failed since selector $scrut
106-
| does not match ${caseText(stuckCase)}
107-
| and cannot be shown to be disjoint from it either.
108-
| Therefore, reduction cannot advance to the remaining case${if otherCases.length == 1 then "" else "s"}
109-
|
110-
| ${casesText(otherCases)}"""
105+
val msg =
106+
i""" failed since selector $scrut
107+
| does not match ${caseText(stuckCase)}
108+
| and cannot be shown to be disjoint from it either."""
109+
if otherCases.length == 0 then msg
110+
else
111+
val s = if otherCases.length == 1 then "" else "s"
112+
i"""$msg
113+
| Therefore, reduction cannot advance to the remaining case$s
114+
|
115+
| ${casesText(otherCases)}"""
111116

112-
end MatchTypeTrace
117+
def noMatchesText(scrut: Type, cases: List[Type])(using Context): String =
118+
i"""failed since selector $scrut
119+
|matches none of the cases
120+
|
121+
| ${casesText(cases)}"""
113122

123+
end MatchTypeTrace

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

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2542,7 +2542,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
25422542
x && {
25432543
t match {
25442544
case tp: TypeRef if tp.symbol.isAbstractOrParamType => false
2545-
case _: SkolemType | _: TypeVar => false
2545+
case _: SkolemType | _: TypeVar | _: TypeParamRef => false
25462546
case _ => foldOver(x, t)
25472547
}
25482548
}
@@ -2585,17 +2585,17 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
25852585
def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
25862586
provablyDisjoint(tp1, tp2) && typeparamCorrespondsToField(tycon1, tparam)
25872587

2588-
// In the invariant case, we used a weaker version of disjointness:
2589-
// we consider types not equal with respect to =:= to be disjoint
2588+
// In the invariant case, we also use a stronger notion of disjointness:
2589+
// we consider fully instantiated types not equal wrt =:= to be disjoint
25902590
// (under any context). This is fine because it matches the runtime
25912591
// semantics of pattern matching. To implement a pattern such as
25922592
// `case Inv[T] => ...`, one needs a type tag for `T` and the compiler
25932593
// is used at runtime to check it the scrutinee's type is =:= to `T`.
2594-
// Note that this is currently a theoretical concern since we Dotty
2594+
// Note that this is currently a theoretical concern since Dotty
25952595
// doesn't have type tags, meaning that users cannot write patterns
25962596
// that do type tests on higher kinded types.
25972597
def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
2598-
covariantDisjoint(tp1, tp2, tparam) ||
2598+
provablyDisjoint(tp1, tp2) ||
25992599
!isSameType(tp1, tp2) &&
26002600
fullyInstantiated(tp1) && // We can only trust a "no" from `isSameType` when
26012601
fullyInstantiated(tp2) // both `tp1` and `tp2` are fully instantiated.
@@ -2924,14 +2924,13 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
29242924
case None =>
29252925
recur(remaining1)
29262926
case Some(NoType) =>
2927-
if remaining1.isEmpty then MatchTypeTrace.noMatches(scrut, cases)
2928-
else MatchTypeTrace.stuck(scrut, cas, remaining1)
2927+
MatchTypeTrace.stuck(scrut, cas, remaining1)
29292928
NoType
29302929
case Some(tp) =>
29312930
tp
29322931
case Nil =>
2933-
MatchTypeTrace.noMatches(scrut, cases)
2934-
NoType
2932+
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)
2933+
throw new TypeError(s"Match type reduction $casesText")
29352934

29362935
inFrozenConstraint {
29372936
// Empty types break the basic assumption that if a scrutinee and a

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -137,6 +137,8 @@ object TypeOps:
137137
tp2
138138
case tp1 => tp1
139139
}
140+
case defn.MatchCase(pat, body) =>
141+
defn.MatchCase(simplify(pat, theMap), body)
140142
case tp: AppliedType =>
141143
tp.tycon match
142144
case tycon: TypeRef if tycon.info.isInstanceOf[MatchAlias] =>
@@ -485,7 +487,7 @@ object TypeOps:
485487
tp
486488
else tryWiden(tp, tp.prefix).orElse {
487489
if (tp.isTerm && variance > 0 && !pre.isSingleton)
488-
apply(tp.info.widenExpr)
490+
apply(tp.info.widenExpr)
489491
else if (upper(pre).member(tp.name).exists)
490492
super.derivedSelect(tp, pre)
491493
else

‎compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ class VarianceChecker(using Context) {
133133
def apply(status: Option[VarianceError], tp: Type): Option[VarianceError] = trace(s"variance checking $tp of $base at $variance", variances) {
134134
try
135135
if (status.isDefined) status
136-
else tp.normalized match {
136+
else tp match {
137137
case tp: TypeRef =>
138138
val sym = tp.symbol
139139
if (sym.isOneOf(VarianceFlags) && base.isContainedIn(sym.owner)) checkVarianceOfSymbol(sym)

‎tests/neg-macros/toexproftuple.scala

Lines changed: 57 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,63 @@
1-
import scala.quoted._, scala.deriving.*
1+
import scala.quoted._, scala.deriving.* // error
2+
// ^
3+
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
4+
// matches none of the cases
5+
//
6+
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
7+
// case EmptyTuple => EmptyTuple
8+
9+
inline def mcr: Any = ${mcrImpl} // error
10+
// ^
11+
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
12+
// matches none of the cases
13+
//
14+
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
15+
// case EmptyTuple => EmptyTuple
16+
17+
def mcrImpl(using ctx: Quotes): Expr[Any] = { // error // error
18+
//^
19+
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
20+
// matches none of the cases
21+
//
22+
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
23+
// case EmptyTuple => EmptyTuple
24+
25+
// ^
26+
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
27+
// matches none of the cases
28+
//
29+
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
30+
// case EmptyTuple => EmptyTuple
231

3-
inline def mcr: Any = ${mcrImpl}
4-
def mcrImpl(using ctx: Quotes): Expr[Any] = {
532
val tpl: (Expr[1], Expr[2], Expr[3]) = ('{1}, '{2}, '{3})
633
'{val res: (1, 3, 3) = ${Expr.ofTuple(tpl)}; res} // error
34+
// ^^^^^^^^^^^^^^^^^
35+
// Found: quoted.Expr[(1 : Int) *: (2 : Int) *: (3 : Int) *: EmptyTuple]
36+
// Required: quoted.Expr[((1 : Int), (3 : Int), (3 : Int))]
737

838
val tpl2: (Expr[1], 2, Expr[3]) = ('{1}, 2, '{3})
9-
'{val res = ${Expr.ofTuple(tpl2)}; res} // error
39+
'{val res = ${Expr.ofTuple(tpl2)}; res} // error // error // error // error
40+
// ^
41+
// Cannot prove that (quoted.Expr[(1 : Int)], (2 : Int), quoted.Expr[(3 : Int)]) =:= scala.Tuple.Map[
42+
// scala.Tuple.InverseMap[
43+
// (quoted.Expr[(1 : Int)], (2 : Int), quoted.Expr[(3 : Int)])
44+
// , quoted.Expr]
45+
// , quoted.Expr].
46+
47+
// ^
48+
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
49+
// matches none of the cases
50+
//
51+
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
52+
// case EmptyTuple => EmptyTuple
53+
54+
// ^
55+
// Cyclic reference involving val res
56+
57+
// ^
58+
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
59+
// matches none of the cases
60+
//
61+
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
62+
// case EmptyTuple => EmptyTuple
1063
}

‎tests/neg/10747.scala

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
type Foo[A] = A match {
2+
case Int => String
3+
}
4+
5+
type B = Foo[Boolean] // error

‎tests/neg/12974.scala

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
package example
2+
3+
object RecMap {
4+
5+
object Record {
6+
// use this scope to bound who can see inside the opaque type
7+
opaque type Rec[A <: Tuple] = Map[String, Any]
8+
9+
object Rec {
10+
type HasKey[A <: Tuple, K] =
11+
A match
12+
case (K, t) *: _ => t
13+
case _ *: t => HasKey[t, K]
14+
15+
val empty: Rec[EmptyTuple] = Map.empty
16+
17+
extension [A <: Tuple](toMap: Rec[A])
18+
def fetch[K <: String & Singleton](key: K): HasKey[A, K] =
19+
toMap(key).asInstanceOf[HasKey[A, K]]
20+
}
21+
}
22+
23+
def main(args: Array[String]) =
24+
import Record._
25+
26+
val foo: Any = Rec.empty.fetch("foo") // error
27+
// ^
28+
// Match type reduction failed since selector EmptyTuple.type
29+
// matches none of the cases
30+
//
31+
// case (("foo" : String), t) *: _ => t
32+
// case _ *: t => example.RecMap.Record.Rec.HasKey[t, ("foo" : String)]
33+
34+
end main
35+
}

‎tests/neg/6697.check

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@
77
|
88
| trying to reduce Test.Sub[O]
99
| failed since selector O
10-
| matches none of the cases
11-
|
12-
| case Test.Of[sup, sub] => sub
10+
| does not match case Test.Of[sup, sub] => sub
11+
| and cannot be shown to be disjoint from it either.
1312

1413
longer explanation available when compiling with `-explain`

‎tests/neg/i12049.check

Lines changed: 24 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -15,39 +15,22 @@
1515
| case B => String
1616

1717
longer explanation available when compiling with `-explain`
18-
-- [E007] Type Mismatch Error: tests/neg/i12049.scala:14:17 ------------------------------------------------------------
18+
-- Error: tests/neg/i12049.scala:14:23 ---------------------------------------------------------------------------------
1919
14 |val y3: String = ??? : Last[Int *: Int *: Boolean *: String *: EmptyTuple] // error
20-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
21-
| Found: Last[EmptyTuple.type]
22-
| Required: String
20+
| ^
21+
| Match type reduction failed since selector EmptyTuple.type
22+
| matches none of the cases
2323
|
24-
| Note: a match type could not be fully reduced:
25-
|
26-
| trying to reduce Last[EmptyTuple.type]
27-
| failed since selector EmptyTuple.type
28-
| matches none of the cases
29-
|
30-
| case _ *: _ *: t => Last[t]
31-
| case t *: EmptyTuple => t
32-
33-
longer explanation available when compiling with `-explain`
34-
-- [E007] Type Mismatch Error: tests/neg/i12049.scala:22:20 ------------------------------------------------------------
24+
| case _ *: _ *: t => Last[t]
25+
| case t *: EmptyTuple => t
26+
-- Error: tests/neg/i12049.scala:22:26 ---------------------------------------------------------------------------------
3527
22 |val z3: (A, B, A) = ??? : Reverse[(A, B, A)] // error
36-
| ^^^^^^^^^^^^^^^^^^^^^^^^
37-
| Found: Tuple.Concat[Reverse[A *: EmptyTuple.type], (B, A)]
38-
| Required: (A, B, A)
39-
|
40-
| Note: a match type could not be fully reduced:
41-
|
42-
| trying to reduce Tuple.Concat[Reverse[A *: EmptyTuple.type], (B, A)]
43-
| trying to reduce Reverse[A *: EmptyTuple.type]
44-
| failed since selector A *: EmptyTuple.type
45-
| matches none of the cases
28+
| ^
29+
| Match type reduction failed since selector A *: EmptyTuple.type
30+
| matches none of the cases
4631
|
47-
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
48-
| case EmptyTuple => EmptyTuple
49-
50-
longer explanation available when compiling with `-explain`
32+
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
33+
| case EmptyTuple => EmptyTuple
5134
-- Error: tests/neg/i12049.scala:24:20 ---------------------------------------------------------------------------------
5235
24 |val _ = summon[M[B]] // error
5336
| ^
@@ -62,33 +45,22 @@ longer explanation available when compiling with `-explain`
6245
| Therefore, reduction cannot advance to the remaining case
6346
|
6447
| case B => String
65-
-- Error: tests/neg/i12049.scala:25:78 ---------------------------------------------------------------------------------
48+
-- Error: tests/neg/i12049.scala:25:26 ---------------------------------------------------------------------------------
6649
25 |val _ = summon[String =:= Last[Int *: Int *: Boolean *: String *: EmptyTuple]] // error
67-
| ^
68-
| Cannot prove that String =:= Last[EmptyTuple.type].
69-
|
70-
| Note: a match type could not be fully reduced:
50+
| ^
51+
| Match type reduction failed since selector EmptyTuple.type
52+
| matches none of the cases
7153
|
72-
| trying to reduce Last[EmptyTuple.type]
73-
| failed since selector EmptyTuple.type
74-
| matches none of the cases
75-
|
76-
| case _ *: _ *: t => Last[t]
77-
| case t *: EmptyTuple => t
78-
-- Error: tests/neg/i12049.scala:26:48 ---------------------------------------------------------------------------------
54+
| case _ *: _ *: t => Last[t]
55+
| case t *: EmptyTuple => t
56+
-- Error: tests/neg/i12049.scala:26:29 ---------------------------------------------------------------------------------
7957
26 |val _ = summon[(A, B, A) =:= Reverse[(A, B, A)]] // error
80-
| ^
81-
| Cannot prove that (A, B, A) =:= Tuple.Concat[Reverse[A *: EmptyTuple.type], (B, A)].
82-
|
83-
| Note: a match type could not be fully reduced:
84-
|
85-
| trying to reduce Tuple.Concat[Reverse[A *: EmptyTuple.type], (B, A)]
86-
| trying to reduce Reverse[A *: EmptyTuple.type]
87-
| failed since selector A *: EmptyTuple.type
88-
| matches none of the cases
58+
| ^
59+
| Match type reduction failed since selector A *: EmptyTuple.type
60+
| matches none of the cases
8961
|
90-
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
91-
| case EmptyTuple => EmptyTuple
62+
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
63+
| case EmptyTuple => EmptyTuple
9264
-- [E008] Not Found Error: tests/neg/i12049.scala:28:21 ----------------------------------------------------------------
9365
28 |val _ = (??? : M[B]).length // error
9466
| ^^^^^^^^^^^^^^^^^^^

‎tests/neg/matchtype-seq.check

Lines changed: 12 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,19 @@
1-
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:9:18 ------------------------------------------------------
1+
-- Error: tests/neg/matchtype-seq.scala:9:11 ---------------------------------------------------------------------------
22
9 | identity[T1[3]]("") // error
3-
| ^^
4-
| Found: ("" : String)
5-
| Required: Test.T1[(3 : Int)]
3+
| ^
4+
| Match type reduction failed since selector (3 : Int)
5+
| matches none of the cases
66
|
7-
| Note: a match type could not be fully reduced:
8-
|
9-
| trying to reduce Test.T1[(3 : Int)]
10-
| failed since selector (3 : Int)
11-
| matches none of the cases
12-
|
13-
| case (1 : Int) => Int
14-
| case (2 : Int) => String
15-
16-
longer explanation available when compiling with `-explain`
17-
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:10:18 -----------------------------------------------------
7+
| case (1 : Int) => Int
8+
| case (2 : Int) => String
9+
-- Error: tests/neg/matchtype-seq.scala:10:11 --------------------------------------------------------------------------
1810
10 | identity[T1[3]](1) // error
19-
| ^
20-
| Found: (1 : Int)
21-
| Required: Test.T1[(3 : Int)]
11+
| ^
12+
| Match type reduction failed since selector (3 : Int)
13+
| matches none of the cases
2214
|
23-
| Note: a match type could not be fully reduced:
24-
|
25-
| trying to reduce Test.T1[(3 : Int)]
26-
| failed since selector (3 : Int)
27-
| matches none of the cases
28-
|
29-
| case (1 : Int) => Int
30-
| case (2 : Int) => String
31-
32-
longer explanation available when compiling with `-explain`
15+
| case (1 : Int) => Int
16+
| case (2 : Int) => String
3317
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:11:20 -----------------------------------------------------
3418
11 | identity[T1[Int]]("") // error
3519
| ^^

0 commit comments

Comments
 (0)