From 940b01167a0dcfa34b6230305b22a0460e2add40 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Wed, 28 Jul 2021 14:42:16 +0200 Subject: [PATCH 1/2] Fix #12800: Clarify MT reduction error on empty scrutinee --- .../tools/dotc/core/MatchTypeTrace.scala | 10 +++++++++ .../dotty/tools/dotc/core/TypeComparer.scala | 7 +++++-- tests/neg/12800.scala | 21 +++++++++++++++++++ 3 files changed, 36 insertions(+), 2 deletions(-) create mode 100644 tests/neg/12800.scala diff --git a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala index 054b445432a8..a7536027a079 100644 --- a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala +++ b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala @@ -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: @@ -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. */ @@ -91,6 +98,9 @@ object MatchTypeTrace: | matches none of the cases | | ${casesText(cases)}""" + case EmptyScrutinee(scrut) => + i""" failed since selector $scrut + | is uninhabited.""" case Stuck(scrut, stuckCase, otherCases) => i""" failed since selector $scrut | does not match ${caseText(stuckCase)} diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 38fd65cb4c54..033d26301df1 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -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) } } } diff --git a/tests/neg/12800.scala b/tests/neg/12800.scala new file mode 100644 index 000000000000..164276396bec --- /dev/null +++ b/tests/neg/12800.scala @@ -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. +} From 92f5806e359999db40e36209ebaaabd1041ec4e3 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Wed, 28 Jul 2021 20:40:29 +0200 Subject: [PATCH 2/2] Update error message --- compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala | 2 +- tests/neg/matchtype-seq.check | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala index a7536027a079..f711f8d1ab67 100644 --- a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala +++ b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala @@ -100,7 +100,7 @@ object MatchTypeTrace: | ${casesText(cases)}""" case EmptyScrutinee(scrut) => i""" failed since selector $scrut - | is uninhabited.""" + | is uninhabited (there are no values of that type).""" case Stuck(scrut, stuckCase, otherCases) => i""" failed since selector $scrut | does not match ${caseText(stuckCase)} diff --git a/tests/neg/matchtype-seq.check b/tests/neg/matchtype-seq.check index b5dc6923d374..c2207fa1aea3 100644 --- a/tests/neg/matchtype-seq.check +++ b/tests/neg/matchtype-seq.check @@ -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 ---------------------------------------------------- @@ -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 ---------------------------------------------------- @@ -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 ---------------------------------------------------- @@ -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 ----------------------------------------------------