Skip to content

Commit

Permalink
Update unreducible match types error reporting (#19954)
Browse files Browse the repository at this point in the history
Match type reduction can fail for any of the following reasons:
- EmptyScrutinee: would be unsound to reduce
- Stuck: selector does not match a case and is not provably disjoint
from it either
- NoInstance: selector does not uniquely determine params captures in
pattern
- NoMatches: selector matches none of the cases
- LegacyPattern: match type contains an illegal case and sourceVersion
>= 3.4

Out of those, only Stuck and NoInstance, *could* get reduced in a
refined context.

## Status quo

The match reducer returns:
- `ErrorType` for NoMatches and LegacyPattern,
- `NoType`, which implies the match type is left unreduced, in all other
cases.

In addition, the implementation has an issue where the `ErrorType`s can
be left unreported, then entering the flexible type logic, thereby
conforming to anything.

## Proposed changes

In addition to fixing the aforementioned bug, this PR proposes to leave
all unreducible match types as unreduced.
Of course the reduction may be needed at a later point for conformance,
in which case the error message will still contain the same explanations
from the `MatchTypeTrace`.

Fixes #19949 
Fixes #19950 

## Discussion

All cases of failed match type reductions which we know will never
reduce, even with refined scrutinee, should have a consistent behaviour.
So NoMatches and EmptyScrutinee should either both be an error or both
be left unreduced.

The current implementation attempts to do the former approach (but only
for NoMatches), which has some limitations as discussed below (I'm not
saying I can do better, hence the latter approach).

### Undesirable errors

We dont always want an error for a NoMatches failed reduction, for
example if we just need `Nothing` to conform to it:
```scala 3
trait TupleWrap[T <: Tuple]:  
  def head: Tuple.Head[T]  
  
object EmptyTupleWrap extends TupleWrap[EmptyTuple]:  
  def head = throw NoSuchElementException() // Error:
// |      ^  
// |      Match type reduction failed since selector EmptyTuple  
// |      matches none of the cases
```
But we could do `def head: Nothing = ...` to avoid the error here. 

Generally speaking, places where the bounds of the match type suffice
can still get a reduction error, and adding an ascription to avoid an
inferred match type doesn't always do the trick.

Another refused example could be:
```scala 3
type Default[N <: Int] = N match  
  case 0 => 'a' | 'c'
  case 1 => 'b' | 'd'
  
def default(n: Int): Option[Default[n.type]] = n match  
  case _: (0 | 1) => Some[Default[n.type]]:  
    n match  
      case _: 0 => 'a' 
      case _: 1 => 'b'
  case _ => None  
  
default(2): Option[Char] // Error  
// |   ^  
// |   Match type reduction failed since selector (2 : Int)  
// |   matches none of the cases
```
even though the function looks reasonable and type-checking would be
sound.

### Missed errors

Also note in the `EmptyTupleWrap` example, we get a reduction error from
a match type application which does not appear in the source code. A
valid question might be when and for what exactly these conditions are
checked ?

The goal is to report a type error early on for a NoMatches application
right, but we are actually only doing so if we happen to do
`tryNormalize` and end up in the `MatchReducer`.

Here is an example where were a match type with NoMatches is accepted
```scala 3
trait A:
  type X
  type R = X match
    case 0 => 'a'
    case 1 => 'b'

trait B extends A:
  type S = 2

type R1 = B#R // no error
```

Generally speaking, the NoMatches error can be circumvented with:
```scala 3
type AllowNoMatchesM[X] = {
  type X1 = X
  type R = X1 match
    case 0 => 'a'
    case 1 => 'b'
}#R
type R2 = AllowNoMatchesM[2] // no error
```

Also note the projections are used in the examples for simplicity but
are not necessary, `R` *can be* used within `B` as unreduced without a
reported error.

See #19799 for another example of inconsistent errors
  • Loading branch information
odersky committed Mar 27, 2024
2 parents 6a40dd5 + 2beb67e commit 4673f77
Show file tree
Hide file tree
Showing 12 changed files with 124 additions and 114 deletions.
14 changes: 13 additions & 1 deletion compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ object MatchTypeTrace:

private enum TraceEntry:
case TryReduce(scrut: Type)
case NoMatches(scrut: Type, cases: List[MatchTypeCaseSpec])
case Stuck(scrut: Type, stuckCase: MatchTypeCaseSpec, otherCases: List[MatchTypeCaseSpec])
case NoInstance(scrut: Type, stuckCase: MatchTypeCaseSpec, fails: List[(Name, TypeBounds)])
case EmptyScrutinee(scrut: Type)
Expand Down Expand Up @@ -50,6 +51,12 @@ object MatchTypeTrace:
case _ =>
case _ =>

/** Record a failure that scrutinee `scrut` does not match any case in `cases`.
* Only the first failure is recorded.
*/
def noMatches(scrut: Type, cases: List[MatchTypeCaseSpec])(using Context) =
matchTypeFail(NoMatches(scrut, cases))

/** Record a failure that scrutinee `scrut` does not match `stuckCase` but is
* not disjoint from it either, which means that the remaining cases `otherCases`
* cannot be visited. Only the first failure is recorded.
Expand All @@ -71,7 +78,7 @@ object MatchTypeTrace:
*/
def recurseWith(scrut: Type)(op: => Type)(using Context): Type =
ctx.property(MatchTrace) match
case Some(trace) =>
case Some(trace) if !trace.entries.contains(TryReduce(scrut)) =>
val prev = trace.entries
trace.entries = TryReduce(scrut) :: prev
val res = op
Expand All @@ -95,6 +102,11 @@ object MatchTypeTrace:
private def explainEntry(entry: TraceEntry)(using Context): String = entry match
case TryReduce(scrut: Type) =>
i" trying to reduce $scrut"
case NoMatches(scrut, cases) =>
i""" failed since selector $scrut
| matches none of the cases
|
| ${casesText(cases)}"""
case EmptyScrutinee(scrut) =>
i""" failed since selector $scrut
| is uninhabited (there are no values of that type)."""
Expand Down
25 changes: 8 additions & 17 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -3634,23 +3634,14 @@ class MatchReducer(initctx: Context) extends TypeComparer(initctx) {
MatchTypeTrace.emptyScrutinee(scrut)
NoType
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)
}
/* TODO warn ? then re-enable warn/12974.scala:26
val noCasesText = MatchTypeTrace.noMatchesText(scrut, cases)
report.warning(reporting.MatchTypeNoCases(noCasesText), pos = ???)
*/
MatchTypeTrace.noMatches(scrut, cases)
NoType

inFrozenConstraint(recur(cases))
}
}

Expand Down
12 changes: 0 additions & 12 deletions tests/neg-macros/toexproftuple.scala
Original file line number Diff line number Diff line change
@@ -1,22 +1,10 @@
import scala.quoted._, scala.deriving.*

inline def mcr: Any = ${mcrImpl}

def mcrImpl(using ctx: Quotes): Expr[Any] = {

val tpl: (Expr[1], Expr[2], Expr[3]) = ('{1}, '{2}, '{3})
'{val res: (1, 3, 3) = ${Expr.ofTuple(tpl)}; res} // error
// ^^^^^^^^^^^^^^^^^
// Found: quoted.Expr[(1 : Int) *: (2 : Int) *: (3 : Int) *: EmptyTuple]
// 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
// ^
// 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].

}
2 changes: 1 addition & 1 deletion tests/neg/10349.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ object Firsts:
case Map[_, v] => First[Option[v]]

def first[X](x: X): First[X] = x match
case x: Map[_, _] => first(x.values.headOption) // error
case x: Map[_, _] => first(x.values.headOption)

@main
def runFirsts2(): Unit =
Expand Down
3 changes: 2 additions & 1 deletion tests/neg/10747.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,5 @@ type Foo[A] = A match {
case Int => String
}

type B = Foo[Boolean] // error
type B = Foo[Boolean]
val _: B = "hello" // error
76 changes: 52 additions & 24 deletions tests/neg/i12049.check
Original file line number Diff line number Diff line change
Expand Up @@ -15,22 +15,39 @@
| case B => String
|
| longer explanation available when compiling with `-explain`
-- [E184] Type Error: tests/neg/i12049.scala:14:23 ---------------------------------------------------------------------
-- [E007] Type Mismatch Error: tests/neg/i12049.scala:14:17 ------------------------------------------------------------
14 |val y3: String = ??? : Last[Int *: Int *: Boolean *: String *: EmptyTuple] // error
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Match type reduction failed since selector EmptyTuple
| matches none of the cases
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Found: Last[EmptyTuple]
| Required: String
|
| case _ *: _ *: t => Last[t]
| case t *: EmptyTuple => t
-- [E184] Type Error: tests/neg/i12049.scala:22:26 ---------------------------------------------------------------------
| Note: a match type could not be fully reduced:
|
| trying to reduce Last[EmptyTuple]
| failed since selector EmptyTuple
| matches none of the cases
|
| case _ *: _ *: t => Last[t]
| case t *: EmptyTuple => t
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/i12049.scala:22:20 ------------------------------------------------------------
22 |val z3: (A, B, A) = ??? : Reverse[(A, B, A)] // error
| ^^^^^^^^^^^^^^^^^^
| Match type reduction failed since selector A *: EmptyTuple.type
| matches none of the cases
| ^^^^^^^^^^^^^^^^^^^^^^^^
| Found: Tuple.Concat[Reverse[A *: EmptyTuple.type], (B, A)]
| Required: (A, B, A)
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Tuple.Concat[Reverse[A *: EmptyTuple.type], (B, A)]
| trying to reduce Reverse[A *: EmptyTuple.type]
| failed since selector A *: EmptyTuple.type
| matches none of the cases
|
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
| case EmptyTuple => EmptyTuple
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
| case EmptyTuple => EmptyTuple
|
| longer explanation available when compiling with `-explain`
-- [E172] Type Error: tests/neg/i12049.scala:24:20 ---------------------------------------------------------------------
24 |val _ = summon[M[B]] // error
| ^
Expand All @@ -45,22 +62,33 @@
| Therefore, reduction cannot advance to the remaining case
|
| case B => String
-- [E184] Type Error: tests/neg/i12049.scala:25:26 ---------------------------------------------------------------------
-- [E172] Type Error: tests/neg/i12049.scala:25:78 ---------------------------------------------------------------------
25 |val _ = summon[String =:= Last[Int *: Int *: Boolean *: String *: EmptyTuple]] // error
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Match type reduction failed since selector EmptyTuple
| matches none of the cases
| ^
| Cannot prove that String =:= Last[EmptyTuple].
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Last[EmptyTuple]
| failed since selector EmptyTuple
| matches none of the cases
|
| case _ *: _ *: t => Last[t]
| case t *: EmptyTuple => t
-- [E184] Type Error: tests/neg/i12049.scala:26:29 ---------------------------------------------------------------------
| case _ *: _ *: t => Last[t]
| case t *: EmptyTuple => t
-- [E172] Type Error: tests/neg/i12049.scala:26:48 ---------------------------------------------------------------------
26 |val _ = summon[(A, B, A) =:= Reverse[(A, B, A)]] // error
| ^^^^^^^^^^^^^^^^^^
| Match type reduction failed since selector A *: EmptyTuple.type
| matches none of the cases
| ^
| Cannot prove that (A, B, A) =:= Tuple.Concat[Reverse[A *: EmptyTuple.type], (B, A)].
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Tuple.Concat[Reverse[A *: EmptyTuple.type], (B, A)]
| trying to reduce Reverse[A *: EmptyTuple.type]
| failed since selector A *: EmptyTuple.type
| matches none of the cases
|
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
| case EmptyTuple => EmptyTuple
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
| case EmptyTuple => EmptyTuple
-- [E008] Not Found Error: tests/neg/i12049.scala:28:21 ----------------------------------------------------------------
28 |val _ = (??? : M[B]).length // error
| ^^^^^^^^^^^^^^^^^^^
Expand Down
30 changes: 0 additions & 30 deletions tests/neg/i17944.check
Original file line number Diff line number Diff line change
Expand Up @@ -14,33 +14,3 @@
| Therefore, reduction cannot advance to the remaining case
|
| case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
| trying to reduce test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)]
| trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
| failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
| does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int))
| and cannot be shown to be disjoint from it either.
| Therefore, reduction cannot advance to the remaining case
|
| case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
| trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
| failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
| does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int))
| and cannot be shown to be disjoint from it either.
| Therefore, reduction cannot advance to the remaining case
|
| case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
| trying to reduce test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)]
| trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
| failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
| does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int))
| and cannot be shown to be disjoint from it either.
| Therefore, reduction cannot advance to the remaining case
|
| case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
| trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
| failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
| does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int))
| and cannot be shown to be disjoint from it either.
| Therefore, reduction cannot advance to the remaining case
|
| case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
9 changes: 9 additions & 0 deletions tests/neg/i19949.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@

trait T[N]:
type M = N match
case 0 => Any

val t: T[Double] = new T[Double] {}
val x: t.M = "hello" // error

val z: T[Double]#M = "hello" // error
40 changes: 28 additions & 12 deletions tests/neg/matchtype-seq.check
Original file line number Diff line number Diff line change
@@ -1,19 +1,35 @@
-- [E184] Type Error: tests/neg/matchtype-seq.scala:9:11 ---------------------------------------------------------------
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:9:18 ------------------------------------------------------
9 | identity[T1[3]]("") // error
| ^^^^^
| Match type reduction failed since selector (3 : Int)
| matches none of the cases
| ^^
| Found: ("" : String)
| Required: Test.T1[(3 : Int)]
|
| case (1 : Int) => Int
| case (2 : Int) => String
-- [E184] Type Error: tests/neg/matchtype-seq.scala:10:11 --------------------------------------------------------------
| Note: a match type could not be fully reduced:
|
| trying to reduce Test.T1[(3 : Int)]
| failed since selector (3 : Int)
| matches none of the cases
|
| case (1 : Int) => Int
| case (2 : Int) => String
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:10:18 -----------------------------------------------------
10 | identity[T1[3]](1) // error
| ^^^^^
| Match type reduction failed since selector (3 : Int)
| matches none of the cases
| ^
| Found: (1 : Int)
| Required: Test.T1[(3 : Int)]
|
| case (1 : Int) => Int
| case (2 : Int) => String
| Note: a match type could not be fully reduced:
|
| trying to reduce Test.T1[(3 : Int)]
| failed since selector (3 : Int)
| matches none of the cases
|
| case (1 : Int) => Int
| case (2 : Int) => String
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:11:20 -----------------------------------------------------
11 | identity[T1[Int]]("") // error
| ^^
Expand Down
15 changes: 0 additions & 15 deletions tests/pos/i18488.scala

This file was deleted.

10 changes: 10 additions & 0 deletions tests/pos/i19950.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@

trait Apply[F[_]]:
extension [T <: NonEmptyTuple](tuple: T)(using toMap: Tuple.IsMappedBy[F][T])
def mapN[B](f: Tuple.InverseMap[T, F] => B): F[B] = ???

given Apply[Option] = ???
given Apply[List] = ???
given Apply[util.Try] = ???

@main def Repro = (Option(1), Option(2), Option(3)).mapN(_ + _ + _)
2 changes: 1 addition & 1 deletion tests/neg/12974.scala → tests/warn/12974.scala
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ object RecMap {
def main(args: Array[String]) =
import Record._

val foo: Any = Rec.empty.fetch("foo") // error
val foo: Any = Rec.empty.fetch("foo") // TODO
// ^
// Match type reduction failed since selector EmptyTuple.type
// matches none of the cases
Expand Down

0 comments on commit 4673f77

Please sign in to comment.