Skip to content

Commit 6e70794

Browse files
committed
Make use of banning to do more GADT reasoning
Specifically, now that "weird" classes can't be defined we can finally assume that if `A[T]` matches `B[y]` then `y <: T` / `y >: T` (covariance/contravariance).
1 parent 0ed2d83 commit 6e70794

File tree

10 files changed

+20
-67
lines changed

10 files changed

+20
-67
lines changed

compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala

+4-15
Original file line numberDiff line numberDiff line change
@@ -218,21 +218,11 @@ trait PatternTypeConstrainer { self: TypeComparer =>
218218
def constrainSimplePatternType(patternTp: Type, scrutineeTp: Type, forceInvariantRefinement: Boolean): Boolean = {
219219
def refinementIsInvariant(tp: Type): Boolean = tp match {
220220
case tp: SingletonType => true
221-
case tp: ClassInfo => tp.cls.is(Final) || tp.cls.is(Case)
221+
case tp: ClassInfo => !tp.cls.isOneOf(AbstractOrTrait)
222222
case tp: TypeProxy => refinementIsInvariant(tp.underlying)
223223
case _ => false
224224
}
225225

226-
def widenVariantParams(tp: Type) = tp match {
227-
case tp @ AppliedType(tycon, args) =>
228-
val args1 = args.zipWithConserve(tycon.typeParams)((arg, tparam) =>
229-
if (tparam.paramVarianceSign != 0) TypeBounds.empty else arg
230-
)
231-
tp.derivedAppliedType(tycon, args1)
232-
case tp =>
233-
tp
234-
}
235-
236226
val patternCls = patternTp.classSymbol
237227
val scrutineeCls = scrutineeTp.classSymbol
238228

@@ -243,8 +233,7 @@ trait PatternTypeConstrainer { self: TypeComparer =>
243233
val pt = if upcastPattern then patternTp.baseType(scrutineeCls) else patternTp
244234
val tp = if !upcastPattern then scrutineeTp.baseType(patternCls) else scrutineeTp
245235

246-
val assumeInvariantRefinement =
247-
migrateTo3 || forceInvariantRefinement || refinementIsInvariant(patternTp)
236+
val assumeInvariantRefinement = migrateTo3 || refinementIsInvariant(patternTp)
248237

249238
trace(i"constraining simple pattern type $tp >:< $pt", gadts, res => s"$res\ngadt = ${ctx.gadt.debugBoundsDescription}") {
250239
(tp, pt) match {
@@ -265,8 +254,8 @@ trait PatternTypeConstrainer { self: TypeComparer =>
265254
isSubType(SkolemType(patternTp), scrutineeTp)
266255
else {
267256
var res = true
268-
if variance < 1 then res &&= isSubType(argS, argP)
269-
if variance > -1 then res &&= isSubType(argP, argS)
257+
if variance < 1 || forceInvariantRefinement then res &&= isSubType(argS, argP)
258+
if variance > -1 || forceInvariantRefinement then res &&= isSubType(argP, argS)
270259
res
271260
}
272261
}

compiler/src/dotty/tools/dotc/typer/RefChecks.scala

+3-2
Original file line numberDiff line numberDiff line change
@@ -842,8 +842,9 @@ object RefChecks {
842842
tycon.typeParams.lazyZip(args1).lazyZip(args2).forall { (param, arg1, arg2) =>
843843
if superArgs.contains(arg1) then
844844
val variance = param.paramVarianceSign
845-
(variance > 0 || arg2 <:< arg1) &&
846-
(variance < 0 || arg1 <:< arg2)
845+
if variance == 0 then arg1 =:= arg2
846+
else if variance > 0 then arg1 <:< arg2
847+
else arg2 <:< arg1
847848
else
848849
// class Foo; class Bar
849850
// trait E[L] extends A[Foo] // combinedBT: A[Foo]

tests/neg-custom-args/fatal-warnings/type-test-syntesize.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ object Test {
1515
test[Any, String]
1616
test[Any, Some[_]]
1717
test[Any, Array[Int]]
18-
test[Seq[Int], List[Int]]
1918

19+
test[Seq[Int], List[Int]] // error
2020
test[Any, Some[Int]] // error
2121
test[Any, a.X] // error
2222
test[a.X, a.Y] // error

tests/neg-custom-args/isInstanceOf/gadt.scala

-13
This file was deleted.

tests/neg-custom-args/isInstanceOf/JavaSeqLiteral.scala renamed to tests/pos-special/isInstanceOf/JavaSeqLiteral.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ object Test1 {
88
class DummyTree extends JavaSeqLiteral[Any]
99

1010
def foo1(tree: Tree[Type]) =
11-
tree.isInstanceOf[JavaSeqLiteral[Type]] // error
11+
tree.isInstanceOf[JavaSeqLiteral[Type]]
1212

1313
foo1(new DummyTree)
1414
}
@@ -26,4 +26,4 @@ object Test2 {
2626
tree.isInstanceOf[JavaSeqLiteral[Type]]
2727

2828
foo1(new DummyTree)
29-
}
29+
}
+8-32
Original file line numberDiff line numberDiff line change
@@ -1,37 +1,13 @@
1-
sealed trait Exp[T]
2-
case class Num(n: Int) extends Exp[Int]
3-
case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int]
4-
case class Var[T](name: String) extends Exp[T]
5-
case class Lambda[T, U](x: Var[T], e: Exp[U]) extends Exp[T => U]
6-
case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]
1+
class Test {
2+
trait A[+T]
3+
class B[T] extends A[T]
74

8-
abstract class Env { outer =>
9-
def apply[T](x: Var[T]): T
5+
class C
6+
class D extends C
107

11-
def + [T](xe: (Var[T], T)) = new Env {
12-
def apply[T](x: Var[T]): T =
13-
if (x == xe._1) xe._2.asInstanceOf[T]
14-
else outer(x)
15-
}
16-
}
17-
18-
object Env {
19-
val empty = new Env {
20-
def apply[T](x: Var[T]): T = ???
21-
}
22-
}
23-
24-
object Test {
25-
26-
val exp = App(Lambda(Var[Int]("x"), Plus(Var[Int]("x"), Num(1))), Var[Int]("2"))
27-
28-
def eval[T](e: Exp[T])(env: Env): T = e match {
29-
case Num(n) => n
30-
case Plus(e1, e2) => eval(e1)(env) + eval(e2)(env)
31-
case v: Var[T] => env(v)
32-
case Lambda(x: Var[s], e) => ((y: s) => eval(e)(env + (x -> y)))
33-
case App(f, e) => eval(f)(env)(eval(e)(env))
8+
def quux(a: A[C]): Unit = a match {
9+
case _: B[C] =>
3410
}
3511

36-
eval(exp)(Env.empty)
12+
quux(new B[D])
3713
}

tests/neg-custom-args/isInstanceOf/i8932.scala renamed to tests/pos-special/isInstanceOf/i8932.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ class Dummy extends Bar[Nothing] with Foo[String]
55

66
def bugReport[A](foo: Foo[A]): Foo[A] =
77
foo match {
8-
case bar: Bar[A] => bar // error
8+
case bar: Bar[A] => bar
99
case dummy: Dummy => ???
1010
}
1111

12-
def test = bugReport(new Dummy: Foo[String])
12+
def test = bugReport(new Dummy: Foo[String])
File renamed without changes.
File renamed without changes.

0 commit comments

Comments
 (0)