diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 9ffe2bda73cb..30e81038e225 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -64,6 +64,14 @@ trait ConstraintHandling { */ protected var canWidenAbstract: Boolean = true + /** + * Used for match type reduction. + * When an abstract type may not be widened, according to `widenAbstractOKFor`, + * we record it in this set, so that we can ultimately fail the reduction, but + * with all the information that comes out from continuing to widen the abstract type. + */ + protected var poisoned: Set[TypeParamRef] = Set.empty + protected var myNecessaryConstraintsOnly = false /** When collecting the constraints needed for a particular subtyping * judgment to be true, we sometimes need to approximate the constraint diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 6857e3da38ed..2706fbf1f410 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -24,6 +24,7 @@ import typer.Applications.productSelectorTypes import reporting.trace import annotation.constructorOnly import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing, isBoxedCapturing, boxed, boxedUnlessFun, boxedIfTypeParam, isAlwaysPure} +import NameKinds.WildcardParamName /** Provides methods to compare types. */ @@ -865,10 +866,36 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling fourthTry } + /** Can we widen an abstract type when comparing with `tp`? + * This is the case with the following cases: + * - if `canWidenAbstract` is true. + * + * Secondly, if `tp` is a type parameter, we can widen if: + * - if `tp` is not a type parameter of the matched-against case lambda + * - if `tp` is an invariant or wildcard type parameter + * - finally, allow widening, but record the type parameter in `poisoned`, + * so that can be accounted for during the reduction step + */ + def widenAbstractOKFor(tp: Type): Boolean = + val acc = new TypeAccumulator[Boolean]: + override def apply(x: Boolean, t: Type) = + x && t.match + case t: TypeParamRef => + variance == 0 + || (t.binder ne caseLambda) + || t.paramName.is(WildcardParamName) + || { poisoned += t; true } + case _ => + foldOver(x, t) + + canWidenAbstract && acc(true, tp) + def tryBaseType(cls2: Symbol) = { val base = nonExprBaseType(tp1, cls2).boxedIfTypeParam(tp1.typeSymbol) if base.exists && (base ne tp1) - && (!caseLambda.exists || canWidenAbstract || tp1.widen.underlyingClassRef(refinementOK = true).exists) + && (!caseLambda.exists + || widenAbstractOKFor(tp2) + || tp1.widen.underlyingClassRef(refinementOK = true).exists) then isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) && recordGadtUsageIf { MatchType.thatReducesUsingGadt(tp1) } @@ -889,8 +916,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling || narrowGADTBounds(tp1, tp2, approx, isUpper = true)) && (tp2.isAny || GADTusage(tp1.symbol)) - (!caseLambda.exists || canWidenAbstract) - && isSubType(hi1.boxedIfTypeParam(tp1.symbol), tp2, approx.addLow) && (trustBounds || isSubType(lo1, tp2, approx.addLow)) + (!caseLambda.exists || widenAbstractOKFor(tp2)) + && isSubType(hi1.boxedIfTypeParam(tp1.symbol), tp2, approx.addLow) && (trustBounds || isSubType(lo1, tp2, approx.addLow)) || compareGADT || tryLiftedToThis1 case _ => @@ -984,7 +1011,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling tp1.cases.corresponds(tp2.cases)(isSubType) case _ => false } - recur(tp1.underlying, tp2) || compareMatch + (!caseLambda.exists || canWidenAbstract) && recur(tp1.underlying, tp2) || compareMatch case tp1: AnnotatedType if tp1.isRefining => isNewSubType(tp1.parent) case JavaArrayType(elem1) => @@ -3091,6 +3118,9 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { } def matchCases(scrut: Type, cases: List[Type])(using Context): Type = { + // a reference for the type parameters poisoned during matching + // for use during the reduction step + var poisoned: Set[TypeParamRef] = Set.empty def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]: def apply(insts: Array[Type], t: Type) = t match @@ -3102,16 +3132,24 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { case entry: TypeBounds => val lo = fullLowerBound(param) val hi = fullUpperBound(param) - if isSubType(hi, lo) then lo.simplified else Range(lo, hi) + if !poisoned(param) && isSubType(hi, lo) then lo.simplified else Range(lo, hi) case inst => assert(inst.exists, i"param = $param\nconstraint = $constraint") - inst.simplified + if !poisoned(param) then inst.simplified else Range(inst, inst) insts case _ => foldOver(insts, t) def instantiateParams(insts: Array[Type]) = new ApproximatingTypeMap { variance = 0 + + override def range(lo: Type, hi: Type): Type = + if variance == 0 && (lo eq hi) then + // override the default `lo eq hi` test, which removes the Range + // which leads to a Reduced result, instead of NoInstance + Range(lower(lo), upper(hi)) + else super.range(lo, hi) + def apply(t: Type) = t match { case t @ TypeParamRef(b, n) if b `eq` caseLambda => insts(n) case t: LazyRef => apply(t.ref) @@ -3133,9 +3171,14 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { def matches(canWidenAbstract: Boolean): Boolean = val saved = this.canWidenAbstract + val savedPoisoned = this.poisoned this.canWidenAbstract = canWidenAbstract + this.poisoned = Set.empty try necessarySubType(scrut, pat) - finally this.canWidenAbstract = saved + finally + poisoned = this.poisoned + this.poisoned = savedPoisoned + this.canWidenAbstract = saved def redux(canApprox: Boolean): MatchResult = caseLambda match diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist index d1dd83f36ff7..3db9483961be 100644 --- a/compiler/test/dotc/pos-test-pickling.blacklist +++ b/compiler/test/dotc/pos-test-pickling.blacklist @@ -48,6 +48,7 @@ i6505.scala i15158.scala i15155.scala i15827.scala +i17149.scala # Opaque type i5720.scala diff --git a/docs/_docs/reference/new-types/match-types.md b/docs/_docs/reference/new-types/match-types.md index d646dd11880b..41f3af11214f 100644 --- a/docs/_docs/reference/new-types/match-types.md +++ b/docs/_docs/reference/new-types/match-types.md @@ -140,6 +140,8 @@ An instantiation `Is` is _minimal_ for `Xs` if all type variables in `Xs` that appear covariantly and nonvariantly in `Is` are as small as possible and all type variables in `Xs` that appear contravariantly in `Is` are as large as possible. Here, "small" and "large" are understood with respect to `<:`. +But, type parameter will not be "large" if a pattern containing it is matched +against lambda case in co- or contra-variant position. For simplicity, we have omitted constraint handling so far. The full formulation of subtyping tests describes them as a function from a constraint and a pair of diff --git a/tests/neg/11982.scala b/tests/neg/11982.scala index 1f50ab2dfe4f..dd7a2b9b055e 100644 --- a/tests/neg/11982.scala +++ b/tests/neg/11982.scala @@ -4,8 +4,8 @@ type Head[X] = X match { } object Unpair { - def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1 - unpair[Tuple2["msg", 42]]: "msg" // error + def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1 // error + unpair[Tuple2["msg", 42]]: "msg" } @@ -14,8 +14,8 @@ type Head2[X] = X match { } object Unpair2 { - def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1 - unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg" // error + def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1 // error + unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg" } @@ -35,6 +35,6 @@ type Head4[X] = X match { } object Unpair4 { - def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1 - unpair[Foo["msg", 42]]: "msg" // error + def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1 // error + unpair[Foo["msg", 42]]: "msg" } diff --git a/tests/neg/i11982.check b/tests/neg/i11982.check deleted file mode 100644 index 304accbf0269..000000000000 --- a/tests/neg/i11982.check +++ /dev/null @@ -1,4 +0,0 @@ --- [E172] Type Error: tests/neg/i11982.scala:22:38 --------------------------------------------------------------------- -22 | val p1: ("msg", 42) = unpair[Tshape] // error: no singleton value for Any - | ^ - |No singleton value available for Any; eligible singleton types for `ValueOf` synthesis include literals and stable paths. diff --git a/tests/neg/i11982.scala b/tests/neg/i11982.scala deleted file mode 100644 index e8ef12ef34e0..000000000000 --- a/tests/neg/i11982.scala +++ /dev/null @@ -1,27 +0,0 @@ -package tuplefun -object Unpair { - - def pair[A, B](using a: ValueOf[A], b: ValueOf[B]): Tuple2[A, B] = - (a.value, b.value) - - def unpair[X <: Tuple2[?, ?]]( - using a: ValueOf[Tuple.Head[X]], - b: ValueOf[Tuple.Head[Tuple.Tail[X]]] - ): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] = - type AA = Tuple.Head[X] - type BB = Tuple.Head[Tuple.Tail[X]] - pair[AA, BB](using a, b) -} - -object UnpairApp { - import Unpair._ - - type Tshape = ("msg", 42) - - // the following won't compile when in the same file as Unpair - val p1: ("msg", 42) = unpair[Tshape] // error: no singleton value for Any - - @main def pairHello: Unit = - assert(p1 == ("msg", 42)) - println(p1) -} \ No newline at end of file diff --git a/tests/neg/i13780.check b/tests/neg/i13780.check index aa0a47db5737..63ba7dec6142 100644 --- a/tests/neg/i13780.check +++ b/tests/neg/i13780.check @@ -1,3 +1,23 @@ +-- [E007] Type Mismatch Error: tests/neg/i13780.scala:12:32 ------------------------------------------------------------ +12 | def unpair[X <: Y]: Head[X] = "" // error + | ^^ + | Found: ("" : String) + | Required: Head[X] + | + | where: X is a type in method unpair with bounds <: A.this.Y + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Head[X] + | failed since selector X + | does not uniquely determine parameters a, b in + | case (a, b) => a + | The computed bounds for the parameters are: + | a >: Any + | b >: Any + | + | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------ 18 | def int[X <: Y]: Int = unpair[X] // error | ^^^^^^^^^ diff --git a/tests/neg/i13780.scala b/tests/neg/i13780.scala index 7e7e2e3ecb74..56badbd356fc 100644 --- a/tests/neg/i13780.scala +++ b/tests/neg/i13780.scala @@ -9,7 +9,7 @@ trait Z { class A extends Z { type Y <: Tuple2[Any, Any] - def unpair[X <: Y]: Head[X] = "" + def unpair[X <: Y]: Head[X] = "" // error def any[X <: Y]: Any = unpair[X] } diff --git a/tests/neg/i17149.scala b/tests/neg/i17149.scala new file mode 100644 index 000000000000..17f3f901e457 --- /dev/null +++ b/tests/neg/i17149.scala @@ -0,0 +1,17 @@ +type Ext1[S] = S match { + case Seq[t] => t +} +type Ext2[S] = S match { + case Seq[_] => Int +} +type Ext3[S] = S match { + case Array[t] => t +} +type Ext4[S] = S match { + case Array[_] => Int +} +def foo[T <: Seq[Any], A <: Array[B], B] = + summon[Ext1[T] =:= T] // error + summon[Ext2[T] =:= Int] // ok + summon[Ext3[A] =:= B] // ok + summon[Ext4[A] =:= Int] // ok \ No newline at end of file diff --git a/tests/pos/i15926.contra.scala b/tests/pos/i15926.contra.scala new file mode 100644 index 000000000000..2e7d848c923c --- /dev/null +++ b/tests/pos/i15926.contra.scala @@ -0,0 +1,7 @@ +trait Show[-A >: Nothing] + +type MT1[I <: Show[Nothing], N] = I match + case Show[a] => N match + case Int => a + +val a = summon[MT1[Show[String], Int] =:= String] diff --git a/tests/pos/i15926.extract.scala b/tests/pos/i15926.extract.scala new file mode 100644 index 000000000000..45177bd3c946 --- /dev/null +++ b/tests/pos/i15926.extract.scala @@ -0,0 +1,24 @@ +// like pos/i15926.scala +// but with the nested match type extracted +// which is a workaround that fixed the problem +sealed trait Nat +final case class Zero() extends Nat +final case class Succ[+N <: Nat]() extends Nat + +final case class Neg[+N <: Succ[Nat]]() + +type Sum[X, Y] = Y match + case Zero => X + case Succ[y] => Sum[Succ[X], y] + +type IntSum[A, B] = B match + case Neg[b] => IntSumNeg[A, b] + +type IntSumNeg[A, B] = A match + case Neg[a] => Neg[Sum[a, B]] + +type One = Succ[Zero] +type Two = Succ[One] + +class Test: + def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]] diff --git a/tests/pos/i15926.min.scala b/tests/pos/i15926.min.scala new file mode 100644 index 000000000000..531467fd4a0f --- /dev/null +++ b/tests/pos/i15926.min.scala @@ -0,0 +1,22 @@ +// like pos/i15926.scala +// but minimised to the subset of paths needed +// to fail the specific test case +sealed trait Nat +final case class Zero() extends Nat +final case class Succ[+N <: Nat]() extends Nat + +final case class Neg[+N <: Succ[Nat]]() + +type Sum[X, Y] = Y match + case Zero => X + case Succ[y] => Sum[Succ[X], y] + +type IntSum[A, B] = B match + case Neg[b] => A match + case Neg[a] => Neg[Sum[a, b]] + +type One = Succ[Zero] +type Two = Succ[One] + +class Test: + def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]] diff --git a/tests/pos/i15926.scala b/tests/pos/i15926.scala new file mode 100644 index 000000000000..df4fc2271cd2 --- /dev/null +++ b/tests/pos/i15926.scala @@ -0,0 +1,28 @@ + +@main def main(): Unit = + println(summon[Sum[Minus[Succ[Zero]], Minus[Succ[Zero]]] =:= Minus[Succ[Succ[Zero]]]]) + +sealed trait IntT +sealed trait NatT extends IntT +final case class Zero() extends NatT +final case class Succ[+N <: NatT](n: N) extends NatT +final case class Minus[+N <: Succ[NatT]](n: N) extends IntT + +type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match + case Zero => X + case Succ[y] => NatSum[Succ[X], y] + +type NatDif[X <: NatT, Y <: NatT] <: IntT = Y match + case Zero => X + case Succ[y] => X match + case Zero => Minus[Y] + case Succ[x] => NatDif[x, y] + +type Sum[X <: IntT, Y <: IntT] <: IntT = Y match + case Zero => X + case Minus[y] => X match + case Minus[x] => Minus[NatSum[x, y]] + case _ => NatDif[X, y] + case _ => X match + case Minus[x] => NatDif[Y, x] + case _ => NatSum[X, Y] \ No newline at end of file diff --git a/tests/pos/i17149.scala b/tests/pos/i17149.scala new file mode 100644 index 000000000000..7a659334badb --- /dev/null +++ b/tests/pos/i17149.scala @@ -0,0 +1,6 @@ +type Ext[S <: Seq[_]] = S match { + case Seq[t] => t +} + +val _ = implicitly[Ext[Seq[Int]] =:= Int] // e.scala: Cannot prove that e.Ext[Seq[Int]] =:= Int +val _ = summon[Ext[Seq[Int]] =:= Int] \ No newline at end of file