Skip to content

Fix #12800: Clarify match type reduction error on empty scrutinee #13184

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

Merged
merged 2 commits into from
Aug 9, 2021
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
10 changes: 10 additions & 0 deletions compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ object MatchTypeTrace:
case TryReduce(scrut: Type)
case NoMatches(scrut: Type, cases: List[Type])
case Stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])
case EmptyScrutinee(scrut: Type)
import TraceEntry._

private class MatchTrace:
Expand Down Expand Up @@ -61,6 +62,12 @@ object MatchTypeTrace:
def stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])(using Context) =
matchTypeFail(Stuck(scrut, stuckCase, otherCases))

/** Record a failure that scrutinee `scrut` is provably empty.
* Only the first failure is recorded.
*/
def emptyScrutinee(scrut: Type)(using Context) =
matchTypeFail(EmptyScrutinee(scrut))

/** Record in the trace that we are trying to reduce `scrut` when performing `op`
* If `op` succeeds the entry is removed after exit. If `op` fails, it stays.
*/
Expand Down Expand Up @@ -91,6 +98,9 @@ object MatchTypeTrace:
| matches none of the cases
|
| ${casesText(cases)}"""
case EmptyScrutinee(scrut) =>
i""" failed since selector $scrut
| is uninhabited (there are no values of that type)."""
case Stuck(scrut, stuckCase, otherCases) =>
i""" failed since selector $scrut
| does not match ${caseText(stuckCase)}
Expand Down
7 changes: 5 additions & 2 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2921,8 +2921,11 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
// obviously sound, but quite restrictive. With the current formulation,
// we need to be careful that `provablyEmpty` covers all the conditions
// used to conclude disjointness in `provablyDisjoint`.
if (provablyEmpty(scrut)) NoType
else recur(cases)
if (provablyEmpty(scrut))
MatchTypeTrace.emptyScrutinee(scrut)
NoType
else
recur(cases)
}
}
}
Expand Down
21 changes: 21 additions & 0 deletions tests/neg/12800.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
object Test {
type FieldType2[K, +V] = V with KeyTag2[K, V]
trait KeyTag2[K, +V] extends Any

type WrapUpper = Tuple
type Wrap[A] = Tuple1[A]

type Extract[A <: WrapUpper] = A match {
case Wrap[h] => h
}

summon[Extract[Wrap[FieldType2["foo", Int]]] =:= FieldType2["foo", Int]] // error
// ^
// Cannot prove that Main.Extract[Tuple1[Main.FieldType2[("foo" : String), Int]]] =:= Main.FieldType2[("foo" : String), Int].
//
// Note: a match type could not be fully reduced:
//
// trying to reduce Main.Extract[Tuple1[Main.FieldType2[("foo" : String), Int]]]
// failed since selector Tuple1[Main.FieldType2[("foo" : String), Int]]
// is uninhabited.
}
8 changes: 8 additions & 0 deletions tests/neg/matchtype-seq.check
Original file line number Diff line number Diff line change
Expand Up @@ -257,6 +257,8 @@ longer explanation available when compiling with `-explain`
| Note: a match type could not be fully reduced:
|
| trying to reduce Test.T9[(Nothing, String)]
| failed since selector (Nothing, String)
| is uninhabited (there are no values of that type).

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:106:40 ----------------------------------------------------
Expand All @@ -268,6 +270,8 @@ longer explanation available when compiling with `-explain`
| Note: a match type could not be fully reduced:
|
| trying to reduce Test.T9[(String, Nothing)]
| failed since selector (String, Nothing)
| is uninhabited (there are no values of that type).

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:107:37 ----------------------------------------------------
Expand All @@ -279,6 +283,8 @@ longer explanation available when compiling with `-explain`
| Note: a match type could not be fully reduced:
|
| trying to reduce Test.T9[(Int, Nothing)]
| failed since selector (Int, Nothing)
| is uninhabited (there are no values of that type).

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:108:37 ----------------------------------------------------
Expand All @@ -290,6 +296,8 @@ longer explanation available when compiling with `-explain`
| Note: a match type could not be fully reduced:
|
| trying to reduce Test.T9[(Nothing, Int)]
| failed since selector (Nothing, Int)
| is uninhabited (there are no values of that type).

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:109:29 ----------------------------------------------------
Expand Down