Skip to content

Fix #10747: Raise type error on unreducible match type #12768

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

Merged
merged 9 commits into from
Sep 14, 2021
Merged

Fix #10747: Raise type error on unreducible match type #12768

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
5bf38d8
Fix #10747: Raise type error on unreducible MT
OlivierBlanvillain Jun 4, 2021
cb5b924
Don't simplify MT right-hand sides
OlivierBlanvillain Jun 9, 2021
3537f7c
Update neg test error annotations
OlivierBlanvillain Jun 9, 2021
bfb7726
Don't normalize in VarianceChecker
OlivierBlanvillain Jun 11, 2021
89e26c7
Add test case
OlivierBlanvillain Jun 11, 2021
0cad72a
Fix #12974: Add test case
OlivierBlanvillain Jul 28, 2021
308cbb1
Fix 10747-shapeless-min.scala
OlivierBlanvillain Jul 28, 2021
509727a
Update invariantDisjoint check
OlivierBlanvillain Jul 28, 2021
11a2082
Update check files
OlivierBlanvillain Jul 28, 2021
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
24 changes: 17 additions & 7 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 @@ -102,12 +102,22 @@ object MatchTypeTrace:
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)}
| and cannot be shown to be disjoint from it either.
| Therefore, reduction cannot advance to the remaining case${if otherCases.length == 1 then "" else "s"}
|
| ${casesText(otherCases)}"""
val msg =
i""" failed since selector $scrut
| does not match ${caseText(stuckCase)}
| and cannot be shown to be disjoint from it either."""
if otherCases.length == 0 then msg
else
val s = if otherCases.length == 1 then "" else "s"
i"""$msg
| Therefore, reduction cannot advance to the remaining case$s
|
| ${casesText(otherCases)}"""

end MatchTypeTrace
def noMatchesText(scrut: Type, cases: List[Type])(using Context): String =
i"""failed since selector $scrut
|matches none of the cases
|
| ${casesText(cases)}"""

end MatchTypeTrace
17 changes: 8 additions & 9 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 @@ -2542,7 +2542,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
x && {
t match {
case tp: TypeRef if tp.symbol.isAbstractOrParamType => false
case _: SkolemType | _: TypeVar => false
case _: SkolemType | _: TypeVar | _: TypeParamRef => false
case _ => foldOver(x, t)
}
}
Expand Down Expand Up @@ -2585,17 +2585,17 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
provablyDisjoint(tp1, tp2) && typeparamCorrespondsToField(tycon1, tparam)

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

inFrozenConstraint {
// Empty types break the basic assumption that if a scrutinee and a
Expand Down
4 changes: 3 additions & 1 deletion compiler/src/dotty/tools/dotc/core/TypeOps.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,8 @@ object TypeOps:
tp2
case tp1 => tp1
}
case defn.MatchCase(pat, body) =>
defn.MatchCase(simplify(pat, theMap), body)
case tp: AppliedType =>
tp.tycon match
case tycon: TypeRef if tycon.info.isInstanceOf[MatchAlias] =>
Expand Down Expand Up @@ -485,7 +487,7 @@ object TypeOps:
tp
else tryWiden(tp, tp.prefix).orElse {
if (tp.isTerm && variance > 0 && !pre.isSingleton)
apply(tp.info.widenExpr)
apply(tp.info.widenExpr)
else if (upper(pre).member(tp.name).exists)
super.derivedSelect(tp, pre)
else
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ class VarianceChecker(using Context) {
def apply(status: Option[VarianceError], tp: Type): Option[VarianceError] = trace(s"variance checking $tp of $base at $variance", variances) {
try
if (status.isDefined) status
else tp.normalized match {
else tp match {
case tp: TypeRef =>
val sym = tp.symbol
if (sym.isOneOf(VarianceFlags) && base.isContainedIn(sym.owner)) checkVarianceOfSymbol(sym)
Expand Down
61 changes: 57 additions & 4 deletions tests/neg-macros/toexproftuple.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,63 @@
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} // 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] = { // 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

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
'{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
}
5 changes: 5 additions & 0 deletions tests/neg/10747.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
type Foo[A] = A match {
case Int => String
}

type B = Foo[Boolean] // error
35 changes: 35 additions & 0 deletions tests/neg/12974.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
package example

object RecMap {

object Record {
// use this scope to bound who can see inside the opaque type
opaque type Rec[A <: Tuple] = Map[String, Any]

object Rec {
type HasKey[A <: Tuple, K] =
A match
case (K, t) *: _ => t
case _ *: t => HasKey[t, K]

val empty: Rec[EmptyTuple] = Map.empty

extension [A <: Tuple](toMap: Rec[A])
def fetch[K <: String & Singleton](key: K): HasKey[A, K] =
toMap(key).asInstanceOf[HasKey[A, K]]
}
}

def main(args: Array[String]) =
import Record._

val foo: Any = Rec.empty.fetch("foo") // error
// ^
// Match type reduction failed since selector EmptyTuple.type
// matches none of the cases
//
// case (("foo" : String), t) *: _ => t
// case _ *: t => example.RecMap.Record.Rec.HasKey[t, ("foo" : String)]

end main
}
5 changes: 2 additions & 3 deletions tests/neg/6697.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,7 @@
|
| trying to reduce Test.Sub[O]
| failed since selector O
| matches none of the cases
|
| case Test.Of[sup, sub] => sub
| does not match case Test.Of[sup, sub] => sub
| and cannot be shown to be disjoint from it either.

longer explanation available when compiling with `-explain`
76 changes: 24 additions & 52 deletions tests/neg/i12049.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,39 +15,22 @@
| case B => String

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/i12049.scala:14:17 ------------------------------------------------------------
-- Error: tests/neg/i12049.scala:14:23 ---------------------------------------------------------------------------------
14 |val y3: String = ??? : Last[Int *: Int *: Boolean *: String *: EmptyTuple] // error
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Found: Last[EmptyTuple.type]
| Required: String
| ^
| Match type reduction failed since selector EmptyTuple.type
| matches none of the cases
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Last[EmptyTuple.type]
| failed since selector EmptyTuple.type
| 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 ------------------------------------------------------------
| case _ *: _ *: t => Last[t]
| case t *: EmptyTuple => t
-- Error: tests/neg/i12049.scala:22:26 ---------------------------------------------------------------------------------
22 |val z3: (A, B, A) = ??? : Reverse[(A, B, A)] // error
| ^^^^^^^^^^^^^^^^^^^^^^^^
| 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
| ^
| Match type reduction failed since selector A *: EmptyTuple.type
| matches none of the cases
|
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
| case EmptyTuple => EmptyTuple

longer explanation available when compiling with `-explain`
| case t1 *: t2 *: ts => Tuple.Concat[Reverse[ts], (t2, t1)]
| case EmptyTuple => EmptyTuple
-- Error: tests/neg/i12049.scala:24:20 ---------------------------------------------------------------------------------
24 |val _ = summon[M[B]] // error
| ^
Expand All @@ -62,33 +45,22 @@ longer explanation available when compiling with `-explain`
| Therefore, reduction cannot advance to the remaining case
|
| case B => String
-- Error: tests/neg/i12049.scala:25:78 ---------------------------------------------------------------------------------
-- Error: tests/neg/i12049.scala:25:26 ---------------------------------------------------------------------------------
25 |val _ = summon[String =:= Last[Int *: Int *: Boolean *: String *: EmptyTuple]] // error
| ^
| Cannot prove that String =:= Last[EmptyTuple.type].
|
| Note: a match type could not be fully reduced:
| ^
| Match type reduction failed since selector EmptyTuple.type
| matches none of the cases
|
| trying to reduce Last[EmptyTuple.type]
| failed since selector EmptyTuple.type
| matches none of the cases
|
| case _ *: _ *: t => Last[t]
| case t *: EmptyTuple => t
-- Error: tests/neg/i12049.scala:26:48 ---------------------------------------------------------------------------------
| case _ *: _ *: t => Last[t]
| case t *: EmptyTuple => t
-- Error: tests/neg/i12049.scala:26:29 ---------------------------------------------------------------------------------
26 |val _ = summon[(A, B, A) =:= Reverse[(A, B, A)]] // error
| ^
| 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
| ^
| Match type reduction 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
40 changes: 12 additions & 28 deletions tests/neg/matchtype-seq.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,35 +1,19 @@
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:9:18 ------------------------------------------------------
-- Error: tests/neg/matchtype-seq.scala:9:11 ---------------------------------------------------------------------------
9 | identity[T1[3]]("") // error
| ^^
| Found: ("" : String)
| Required: Test.T1[(3 : Int)]
| ^
| Match type reduction failed since selector (3 : Int)
| matches none of the cases
|
| 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 -----------------------------------------------------
| case (1 : Int) => Int
| case (2 : Int) => String
-- Error: tests/neg/matchtype-seq.scala:10:11 --------------------------------------------------------------------------
10 | identity[T1[3]](1) // error
| ^
| Found: (1 : Int)
| Required: Test.T1[(3 : Int)]
| ^
| Match type reduction failed since selector (3 : Int)
| matches none of the cases
|
| 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`
| case (1 : Int) => Int
| case (2 : Int) => String
-- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:11:20 -----------------------------------------------------
11 | identity[T1[Int]]("") // error
| ^^
Expand Down
Loading