From 3e1fbd6ae786cdd3839b85b358ea4644147cbd41 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 29 Mar 2023 22:54:28 +0200 Subject: [PATCH 1/6] Refine criterion when to widen types Refine criterion when to widen types in match type reduction. We now do not widen if the compared-against type contains variant named type parameters. This is intended to fix the soundness problem in #17149. Fixes #17149 Fixes #15926 Todos: - [ ] Check & fix neg test failures - [ ] Add more tests - [ ] Also consider approximating abstract types to lower bounds. This is completely missing so far. There are neither tests nor an implementation. - [ ] Update the docs on match types to explain what goes on here. --- .../dotty/tools/dotc/core/TypeComparer.scala | 25 +++++++++++++++-- .../test/dotc/pos-test-pickling.blacklist | 1 + tests/neg/i17149.scala | 17 +++++++++++ tests/pos/i15926.scala | 28 +++++++++++++++++++ tests/pos/i17149.scala | 6 ++++ 5 files changed, 74 insertions(+), 3 deletions(-) create mode 100644 tests/neg/i17149.scala create mode 100644 tests/pos/i15926.scala create mode 100644 tests/pos/i17149.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 6857e3da38ed..52052671e991 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,28 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling fourthTry } + /** Can we widen an abstract type when comparing with `tp`? + * This is NOT the case if one of the following is true: + * - canWidenAbstract is false, + * - or `tp` contains a non-wildcard type parameter of the matched-against + * case lambda that appears in co- or contra-variant position + */ + 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) + 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 +908,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 _ => 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/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.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 From 77cb6acd52a770da177db2a5d61ff0530d66a43e Mon Sep 17 00:00:00 2001 From: Dale Wijnand Date: Thu, 30 Mar 2023 11:39:52 +0100 Subject: [PATCH 2/6] Fix match type reduction neg tests --- tests/neg/11982.scala | 12 ++++++------ tests/neg/6570-1.check | 6 ++---- tests/neg/i11982.check | 4 ---- tests/neg/i11982.scala | 27 --------------------------- tests/neg/i11982a.check | 18 ++++++------------ tests/neg/i13780.check | 31 +++++++++++++++++++++---------- tests/neg/i13780.scala | 2 +- tests/pos/i15926.extract.scala | 24 ++++++++++++++++++++++++ tests/pos/i15926.min.scala | 22 ++++++++++++++++++++++ 9 files changed, 82 insertions(+), 64 deletions(-) delete mode 100644 tests/neg/i11982.check delete mode 100644 tests/neg/i11982.scala create mode 100644 tests/pos/i15926.extract.scala create mode 100644 tests/pos/i15926.min.scala 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/6570-1.check b/tests/neg/6570-1.check index bdbadd0f752a..85c172364d9c 100644 --- a/tests/neg/6570-1.check +++ b/tests/neg/6570-1.check @@ -24,9 +24,7 @@ | | trying to reduce M[T] | failed since selector T - | does not uniquely determine parameter x in - | case Cov[x] => N[x] - | The computed bounds for the parameter are: - | x >: Box[Int] + | does not match case Cov[x] => N[x] + | and cannot be shown to be disjoint from it either. | | longer explanation available when compiling with `-explain` 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/i11982a.check b/tests/neg/i11982a.check index 1977aa30e8b5..d5f862af858a 100644 --- a/tests/neg/i11982a.check +++ b/tests/neg/i11982a.check @@ -7,10 +7,8 @@ | | trying to reduce Tuple.Tail[X] | failed since selector X - | does not uniquely determine parameter xs in - | case _ *: xs => xs - | The computed bounds for the parameter are: - | xs >: Any *: EmptyTuple.type <: Tuple + | does not match case _ *: xs => xs + | and cannot be shown to be disjoint from it either. | | longer explanation available when compiling with `-explain` -- [E057] Type Mismatch Error: tests/neg/i11982a.scala:10:38 ----------------------------------------------------------- @@ -22,10 +20,8 @@ | | trying to reduce Tuple.Tail[X] | failed since selector X - | does not uniquely determine parameter xs in - | case _ *: xs => xs - | The computed bounds for the parameter are: - | xs >: Any *: EmptyTuple.type <: Tuple + | does not match case _ *: xs => xs + | and cannot be shown to be disjoint from it either. | | longer explanation available when compiling with `-explain` -- [E057] Type Mismatch Error: tests/neg/i11982a.scala:12:25 ----------------------------------------------------------- @@ -37,9 +33,7 @@ | | trying to reduce Tuple.Tail[X] | failed since selector X - | does not uniquely determine parameter xs in - | case _ *: xs => xs - | The computed bounds for the parameter are: - | xs >: Any *: EmptyTuple.type <: Tuple + | does not match case _ *: xs => xs + | and cannot be shown to be disjoint from it either. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i13780.check b/tests/neg/i13780.check index aa0a47db5737..57b7ff6b261a 100644 --- a/tests/neg/i13780.check +++ b/tests/neg/i13780.check @@ -1,3 +1,20 @@ +-- [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 match case (a, b) => a + | and cannot be shown to be disjoint from it either. + | + | 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 | ^^^^^^^^^ @@ -11,11 +28,8 @@ | | 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 >: Int - | b >: Int + | does not match case (a, b) => a + | and cannot be shown to be disjoint from it either. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/i13780.scala:23:37 ------------------------------------------------------------ @@ -31,10 +45,7 @@ | | 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 >: String - | b >: String + | does not match case (a, b) => a + | and cannot be shown to be disjoint from it either. | | longer explanation available when compiling with `-explain` 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/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]] From 8a657456aedc0f6b535c4484f3a09efc8848ba89 Mon Sep 17 00:00:00 2001 From: Dale Wijnand Date: Thu, 30 Mar 2023 13:52:43 +0100 Subject: [PATCH 3/6] Allow type parameters to be widened, but consider them poison --- .../tools/dotc/core/ConstraintHandling.scala | 1 + .../dotty/tools/dotc/core/TypeComparer.scala | 18 ++++++++++++---- tests/neg/6570-1.check | 6 ++++-- tests/neg/i11982a.check | 18 ++++++++++------ tests/neg/i13780.check | 21 +++++++++++++------ 5 files changed, 46 insertions(+), 18 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 9ffe2bda73cb..eacb257d2d82 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -63,6 +63,7 @@ trait ConstraintHandling { * toplevel; it is turned on again when we add parts of the scrutinee to the constraint. */ protected var canWidenAbstract: Boolean = true + protected var poisoned: Set[TypeParamRef] = Set.empty protected var myNecessaryConstraintsOnly = false /** When collecting the constraints needed for a particular subtyping diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 52052671e991..36563c0dce1a 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -877,9 +877,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling override def apply(x: Boolean, t: Type) = x && t.match case t: TypeParamRef => - variance == 0 || (t.binder ne caseLambda) || t.paramName.is(WildcardParamName) + 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) = { @@ -3110,6 +3114,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { } def matchCases(scrut: Type, cases: List[Type])(using Context): Type = { + var poisoned: Set[TypeParamRef] = Set.empty def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]: def apply(insts: Array[Type], t: Type) = t match @@ -3121,10 +3126,10 @@ 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) @@ -3152,9 +3157,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/tests/neg/6570-1.check b/tests/neg/6570-1.check index 85c172364d9c..bdbadd0f752a 100644 --- a/tests/neg/6570-1.check +++ b/tests/neg/6570-1.check @@ -24,7 +24,9 @@ | | trying to reduce M[T] | failed since selector T - | does not match case Cov[x] => N[x] - | and cannot be shown to be disjoint from it either. + | does not uniquely determine parameter x in + | case Cov[x] => N[x] + | The computed bounds for the parameter are: + | x >: Box[Int] | | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i11982a.check b/tests/neg/i11982a.check index d5f862af858a..1977aa30e8b5 100644 --- a/tests/neg/i11982a.check +++ b/tests/neg/i11982a.check @@ -7,8 +7,10 @@ | | trying to reduce Tuple.Tail[X] | failed since selector X - | does not match case _ *: xs => xs - | and cannot be shown to be disjoint from it either. + | does not uniquely determine parameter xs in + | case _ *: xs => xs + | The computed bounds for the parameter are: + | xs >: Any *: EmptyTuple.type <: Tuple | | longer explanation available when compiling with `-explain` -- [E057] Type Mismatch Error: tests/neg/i11982a.scala:10:38 ----------------------------------------------------------- @@ -20,8 +22,10 @@ | | trying to reduce Tuple.Tail[X] | failed since selector X - | does not match case _ *: xs => xs - | and cannot be shown to be disjoint from it either. + | does not uniquely determine parameter xs in + | case _ *: xs => xs + | The computed bounds for the parameter are: + | xs >: Any *: EmptyTuple.type <: Tuple | | longer explanation available when compiling with `-explain` -- [E057] Type Mismatch Error: tests/neg/i11982a.scala:12:25 ----------------------------------------------------------- @@ -33,7 +37,9 @@ | | trying to reduce Tuple.Tail[X] | failed since selector X - | does not match case _ *: xs => xs - | and cannot be shown to be disjoint from it either. + | does not uniquely determine parameter xs in + | case _ *: xs => xs + | The computed bounds for the parameter are: + | xs >: Any *: EmptyTuple.type <: Tuple | | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i13780.check b/tests/neg/i13780.check index 57b7ff6b261a..63ba7dec6142 100644 --- a/tests/neg/i13780.check +++ b/tests/neg/i13780.check @@ -11,8 +11,11 @@ | | trying to reduce Head[X] | failed since selector X - | does not match case (a, b) => a - | and cannot be shown to be disjoint from it either. + | 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 ------------------------------------------------------------ @@ -28,8 +31,11 @@ | | trying to reduce Head[X] | failed since selector X - | does not match case (a, b) => a - | and cannot be shown to be disjoint from it either. + | does not uniquely determine parameters a, b in + | case (a, b) => a + | The computed bounds for the parameters are: + | a >: Int + | b >: Int | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/i13780.scala:23:37 ------------------------------------------------------------ @@ -45,7 +51,10 @@ | | trying to reduce Head[X] | failed since selector X - | does not match case (a, b) => a - | and cannot be shown to be disjoint from it either. + | does not uniquely determine parameters a, b in + | case (a, b) => a + | The computed bounds for the parameters are: + | a >: String + | b >: String | | longer explanation available when compiling with `-explain` From 94166934e2afae1af4a0a897088a46a71e191ee3 Mon Sep 17 00:00:00 2001 From: Dale Wijnand Date: Fri, 28 Apr 2023 01:07:58 +0100 Subject: [PATCH 4/6] Find & fix a LB/contra case --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 8 ++++++++ tests/pos/i15926.contra.scala | 7 +++++++ 2 files changed, 15 insertions(+) create mode 100644 tests/pos/i15926.contra.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 36563c0dce1a..51b7858179ca 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3136,6 +3136,14 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { 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) 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] From f7da93d122dd2f44277db358b1e3397806264791 Mon Sep 17 00:00:00 2001 From: Dale Wijnand Date: Wed, 24 May 2023 14:48:25 +0100 Subject: [PATCH 5/6] Tweak widenAbstractOKFor docs & doc poisoned --- .../dotty/tools/dotc/core/ConstraintHandling.scala | 7 +++++++ .../src/dotty/tools/dotc/core/TypeComparer.scala | 14 ++++++++++---- docs/_docs/reference/new-types/match-types.md | 2 ++ 3 files changed, 19 insertions(+), 4 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index eacb257d2d82..30e81038e225 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -63,6 +63,13 @@ trait ConstraintHandling { * toplevel; it is turned on again when we add parts of the scrutinee to the constraint. */ 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 diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 51b7858179ca..92f50bc48a29 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -867,10 +867,14 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling } /** Can we widen an abstract type when comparing with `tp`? - * This is NOT the case if one of the following is true: - * - canWidenAbstract is false, - * - or `tp` contains a non-wildcard type parameter of the matched-against - * case lambda that appears in co- or contra-variant position + * 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]: @@ -3114,6 +3118,8 @@ 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]]: 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 From 09f5e4c19a826f79f4a4b5ca48c7999f0d8d94bc Mon Sep 17 00:00:00 2001 From: Dale Wijnand Date: Tue, 23 May 2023 12:41:14 +0100 Subject: [PATCH 6/6] Restrict widening MatchTypes to its bounds During match type reduction, if we're going to allow approximating we must further restrict match types from widening to its bound. Failing to do so will record GADT constraint bounds that parameters will be approximated to, which is lossy and leads to a loss of type checking completion.. For instance, in a variant of i13633 with an added `<: (Boolean, Boolean)` bound to `PlusTri`, when reducing `PlusTri[a, b, O] match { case (x, y) => ... }`, widening the expansion of `PlusTri[a, b, O]` to its bound `(Boolean, Boolean)`, causes the recording the constraints bounds `x >: Boolean` and `y >: Boolean` and then reduction instantiates `x` and `y` to Boolean, losing the precision that comes from `a`, `b`, and `O`. This came up while implementing bounds checking to match type case bodies, and requires an important fix to PatternTypeConstrainer (the use of typeSymbol's) so the tests that require this are part of that effort. --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 92f50bc48a29..2706fbf1f410 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -1011,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) =>