Skip to content

[WIP] Report TypeError for match type with no case or uninhabited scrutinee #19964

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.

Sign up for GitHub

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

Closed
wants to merge 6 commits into from
Closed

[WIP] Report TypeError for match type with no case or uninhabited scrutinee #19964

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
c79c664
Add regression tests
EugeneFlesselle Mar 15, 2024
b2c544a
Revert "ErrorType instead of throwing in match type "no cases""
EugeneFlesselle Mar 15, 2024
ed5ddfe
Update check-files and remove i18488.scala
EugeneFlesselle Mar 15, 2024
a9a8c82
Check ctx.isTyper before throwing TypeError for match type with no cases
EugeneFlesselle Mar 17, 2024
79ab567
Report an error on match type empty scrutinee
EugeneFlesselle Mar 17, 2024
ecbb620
Update check-files and error annotations
EugeneFlesselle Mar 17, 2024
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
14 changes: 4 additions & 10 deletions compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ object MatchTypeTrace:
case TryReduce(scrut: Type)
case Stuck(scrut: Type, stuckCase: MatchTypeCaseSpec, otherCases: List[MatchTypeCaseSpec])
case NoInstance(scrut: Type, stuckCase: MatchTypeCaseSpec, fails: List[(Name, TypeBounds)])
case EmptyScrutinee(scrut: Type)
import TraceEntry.*

private class MatchTrace:
Expand Down Expand Up @@ -60,12 +59,6 @@ object MatchTypeTrace:
def noInstance(scrut: Type, stuckCase: MatchTypeCaseSpec, fails: List[(Name, TypeBounds)])(using Context) =
matchTypeFail(NoInstance(scrut, stuckCase, fails))

/** 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 @@ -95,9 +88,6 @@ object MatchTypeTrace:
private def explainEntry(entry: TraceEntry)(using Context): String = entry match
case TryReduce(scrut: Type) =>
i" trying to reduce $scrut"
case EmptyScrutinee(scrut) =>
i""" failed since selector $scrut
| is uninhabited (there are no values of that type)."""
case Stuck(scrut, stuckCase, otherCases) =>
val msg =
i""" failed since selector $scrut
Expand Down Expand Up @@ -125,6 +115,10 @@ object MatchTypeTrace:
|
| ${casesText(cases)}"""

def emptyScrutineeText(scrut: Type)(using Context): String =
i"""failed since selector $scrut
|is uninhabited (there are no values of that type)."""

def illegalPatternText(scrut: Type, cas: MatchTypeCaseSpec.LegacyPatMat)(using Context): String =
i"""The match type contains an illegal case:
| ${caseText(cas)}
Expand Down
34 changes: 15 additions & 19 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3567,6 +3567,13 @@ class MatchReducer(initctx: Context) extends TypeComparer(initctx) {
def matchMissingCaptures(spec: MatchTypeCaseSpec.MissingCaptures): MatchResult =
MatchResult.Stuck

/**
* Report the failed match type reduction when possible, leave it unreduced otherwise
* See constvalue-of-failed-match-type.scala for an example where this is needed
*/
inline def tryReportingReductionError(typeError: TypeError) =
if ctx.isTyper then throw typeError else NoType

def recur(remaining: List[MatchTypeCaseSpec]): Type = remaining match
case (cas: MatchTypeCaseSpec.LegacyPatMat) :: _ if sourceVersion.isAtLeast(SourceVersion.`3.4`) =>
val errorText = MatchTypeTrace.illegalPatternText(scrut, cas)
Expand All @@ -3591,26 +3598,15 @@ class MatchReducer(initctx: Context) extends TypeComparer(initctx) {
// probably disjoint from it, we prevent reduction.
// See `tests/neg/6570.scala` and `6570-1.scala` for examples that
// exploit emptiness to break match type soundness.
MatchTypeTrace.emptyScrutinee(scrut)
NoType
tryReportingReductionError:
val scrutText = MatchTypeTrace.emptyScrutineeText(scrut)
MatchTypeReductionError(em"Match type reduction $scrutText")
case Nil =>
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)
ErrorType(reporting.MatchTypeNoCases(casesText))

inFrozenConstraint {
if scrut.isError then
// if the scrutinee is an error type
// then just return that as the result
// not doing so will result in the first type case matching
// because ErrorType (as a FlexType) is <:< any type case
// this situation can arise from any kind of nesting of match types,
// e.g. neg/i12049 `Tuple.Concat[Reverse[ts], (t2, t1)]`
// if Reverse[ts] fails with no matches,
// the error type should be the reduction of the Concat too
scrut
else
recur(cases)
}
tryReportingReductionError:
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)
MatchTypeReductionError(em"Match type reduction $casesText")

inFrozenConstraint(recur(cases))
}
}

Expand Down
3 changes: 3 additions & 0 deletions compiler/src/dotty/tools/dotc/core/TypeErrors.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,9 @@ object TypeError:
def toMessage(using Context) = msg
end TypeError

class MatchTypeReductionError(msg: Message)(using Context) extends TypeError:
def toMessage(using Context) = msg

class MalformedType(pre: Type, denot: Denotation, absMembers: Set[Name])(using Context) extends TypeError:
def toMessage(using Context) = em"malformed type: $pre is not a legal prefix for $denot because it contains abstract type member${if (absMembers.size == 1) "" else "s"} ${absMembers.mkString(", ")}"

Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/typer/Implicits.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -663,7 +663,7 @@ trait ImplicitRunInfo:
traverseChildren(t)
case t =>
traverseChildren(t)
traverse(t.normalized)
traverse(try t.normalized catch case _: MatchTypeReductionError => t)
catch case ex: Throwable => handleRecursive("collectParts of", t.show, ex)

def apply(tp: Type): collection.Set[Type] =
Expand Down
49 changes: 45 additions & 4 deletions tests/neg-macros/toexproftuple.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,33 @@
import scala.quoted._, scala.deriving.*
import scala.quoted._, scala.deriving.* // error
// ^
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
// matches none of the cases
//
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
// case EmptyTuple => EmptyTuple

inline def mcr: Any = ${mcrImpl}
inline def mcr: Any = ${mcrImpl} // error
// ^
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
// matches none of the cases
//
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
// case EmptyTuple => EmptyTuple

def mcrImpl(using ctx: Quotes): Expr[Any] = {
def mcrImpl(using ctx: Quotes): Expr[Any] = { // error // error
//^
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
// matches none of the cases
//
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
// case EmptyTuple => EmptyTuple

// ^
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
// matches none of the cases
//
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
// case EmptyTuple => EmptyTuple

val tpl: (Expr[1], Expr[2], Expr[3]) = ('{1}, '{2}, '{3})
'{val res: (1, 3, 3) = ${Expr.ofTuple(tpl)}; res} // error
Expand All @@ -11,12 +36,28 @@ def mcrImpl(using ctx: Quotes): Expr[Any] = {
// Required: quoted.Expr[((1 : Int), (3 : Int), (3 : Int))]

val tpl2: (Expr[1], 2, Expr[3]) = ('{1}, 2, '{3})
'{val res = ${Expr.ofTuple(tpl2)}; res} // error
'{val res = ${Expr.ofTuple(tpl2)}; res} // error // error // error // error
// ^
// Cannot prove that (quoted.Expr[(1 : Int)], (2 : Int), quoted.Expr[(3 : Int)]) =:= scala.Tuple.Map[
// scala.Tuple.InverseMap[
// (quoted.Expr[(1 : Int)], (2 : Int), quoted.Expr[(3 : Int)])
// , quoted.Expr]
// , quoted.Expr].

// ^
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
// matches none of the cases
//
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
// case EmptyTuple => EmptyTuple

// ^
// Cyclic reference involving val res

// ^
// Match type reduction failed since selector ((2 : Int), quoted.Expr[(3 : Int)])
// matches none of the cases
//
// case quoted.Expr[x] *: t => x *: scala.Tuple.InverseMap[t, quoted.Expr]
// case EmptyTuple => EmptyTuple
}
4 changes: 2 additions & 2 deletions tests/neg/6314-2.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ object G {

def main(args: Array[String]): Unit = {
val a: Bar[X & Foo] = "hello" // error
val i: Bar[Y & Foo] = Foo.apply[Bar](a)
val b: Int = i // error
val i: Bar[Y & Foo] = Foo.apply[Bar](a) // error // error
val b: Int = i
println(b + 1)
}
}
36 changes: 20 additions & 16 deletions tests/neg/6314-6.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,16 +1,20 @@
-- Error: tests/neg/6314-6.scala:26:3 ----------------------------------------------------------------------------------
26 | (new YY {}).boom // error: object creation impossible
| ^
|object creation impossible, since def apply(fa: String): Int in trait XX in object Test3 is not defined
|(Note that
| parameter String in def apply(fa: String): Int in trait XX in object Test3 does not match
| parameter Test3.Bar[X & Object with Test3.YY {...}#Foo] in def apply(fa: Test3.Bar[X & YY.this.Foo]): Test3.Bar[Y & YY.this.Foo] in trait YY in object Test3
| )
-- Error: tests/neg/6314-6.scala:52:3 ----------------------------------------------------------------------------------
52 | (new YY {}).boom // error: object creation impossible
| ^
|object creation impossible, since def apply(fa: String): Int in trait XX in object Test4 is not defined
|(Note that
| parameter String in def apply(fa: String): Int in trait XX in object Test4 does not match
| parameter Test4.Bar[X & Object with Test4.YY {...}#FooAlias] in def apply(fa: Test4.Bar[X & YY.this.FooAlias]): Test4.Bar[Y & YY.this.FooAlias] in trait YY in object Test4
| )
-- Error: tests/neg/6314-6.scala:24:18 ---------------------------------------------------------------------------------
24 | def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa // error // error
| ^
| Match type reduction failed since selector X & YY.this.Foo
| is uninhabited (there are no values of that type).
-- Error: tests/neg/6314-6.scala:24:33 ---------------------------------------------------------------------------------
24 | def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa // error // error
| ^
| Match type reduction failed since selector Y & YY.this.Foo
| is uninhabited (there are no values of that type).
-- Error: tests/neg/6314-6.scala:50:18 ---------------------------------------------------------------------------------
50 | def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa // error // error
| ^
| Match type reduction failed since selector X & YY.this.FooAlias
| is uninhabited (there are no values of that type).
-- Error: tests/neg/6314-6.scala:50:38 ---------------------------------------------------------------------------------
50 | def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa // error // error
| ^
| Match type reduction failed since selector Y & YY.this.FooAlias
| is uninhabited (there are no values of that type).
8 changes: 4 additions & 4 deletions tests/neg/6314-6.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,9 @@ object Test3 {
trait YY extends XX {
type Foo = X & Y

def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa
def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa // error // error
}
(new YY {}).boom // error: object creation impossible
(new YY {}).boom
}

object Test4 {
Expand All @@ -47,7 +47,7 @@ object Test4 {
trait YY extends XX {
type Foo = X & Y

def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa
def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa // error // error
}
(new YY {}).boom // error: object creation impossible
(new YY {}).boom
}
16 changes: 4 additions & 12 deletions tests/neg/6570-1.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,16 +1,8 @@
-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:23:27 ------------------------------------------------------------
-- Error: tests/neg/6570-1.scala:23:11 ---------------------------------------------------------------------------------
23 | def thing = new Trait1 {} // error
| ^
| Found: Object with Trait1 {...}
| Required: N[Box[Int & String]]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce N[Box[Int & String]]
| failed since selector Box[Int & String]
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
| ^
| Match type reduction failed since selector Box[Int & String]
| is uninhabited (there are no values of that type).
-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:36:54 ------------------------------------------------------------
36 | def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing // error
| ^^^^^^^
Expand Down
80 changes: 20 additions & 60 deletions tests/neg/6570.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,19 +17,11 @@
| x >: Int
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:29:29 --------------------------------------------------------------
-- Error: tests/neg/6570.scala:29:13 -----------------------------------------------------------------------------------
29 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
| ^
| Match type reduction failed since selector String & Int
| is uninhabited (there are no values of that type).
-- [E007] Type Mismatch Error: tests/neg/6570.scala:47:32 --------------------------------------------------------------
47 | def foo(c: Child): Trait2 = c.thing // error
| ^^^^^^^
Expand All @@ -46,45 +38,21 @@
| a >: Int
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:51:29 --------------------------------------------------------------
-- Error: tests/neg/6570.scala:51:13 -----------------------------------------------------------------------------------
51 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:69:29 --------------------------------------------------------------
| ^
| Match type reduction failed since selector String & Int
| is uninhabited (there are no values of that type).
-- Error: tests/neg/6570.scala:69:13 -----------------------------------------------------------------------------------
69 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:86:29 --------------------------------------------------------------
| ^
| Match type reduction failed since selector String & Int
| is uninhabited (there are no values of that type).
-- Error: tests/neg/6570.scala:86:13 -----------------------------------------------------------------------------------
86 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
| ^
| Match type reduction failed since selector String & Int
| is uninhabited (there are no values of that type).
-- [E007] Type Mismatch Error: tests/neg/6570.scala:103:32 -------------------------------------------------------------
103 | def foo(c: Child): Trait2 = c.thing // error
| ^^^^^^^
Expand All @@ -101,16 +69,8 @@
| t >: Int
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:107:29 -------------------------------------------------------------
-- Error: tests/neg/6570.scala:107:13 ----------------------------------------------------------------------------------
107 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
| ^
| Match type reduction failed since selector String & Int
| is uninhabited (there are no values of that type).
Loading