From cd55b2030585e4d3c2a0e903bee7a3f7ced160c4 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Thu, 3 Oct 2019 14:52:36 +0200 Subject: [PATCH 1/3] Fix #6570: Don't reduce MT with empty scrutinies --- .../dotty/tools/dotc/core/TypeComparer.scala | 85 ++++++++++---- tests/neg/6314-1.scala | 2 +- tests/neg/6314-2.scala | 4 +- tests/neg/6570-1.scala | 33 ++++++ tests/neg/6570.scala | 109 ++++++++++++++++++ tests/neg/matchtype-seq.scala | 8 +- .../staged-tuples/StagedTuple.scala | 2 +- tests/run/tuples1.scala | 3 +- 8 files changed, 214 insertions(+), 32 deletions(-) create mode 100644 tests/neg/6570-1.scala create mode 100644 tests/neg/6570.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index cb037b3275f5..fe85f023dfdd 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -16,6 +16,7 @@ import transform.TypeUtils._ import transform.SymUtils._ import scala.util.control.NonFatal import typer.ProtoTypes.constrained +import typer.Applications.productSelectorTypes import reporting.trace final class AbsentContext @@ -2136,6 +2137,35 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w /** Returns last check's debug mode, if explicitly enabled. */ def lastTrace(): String = "" + private def typeparamCorrespondsToField(tycon: Type, tparam: TypeParamInfo): Boolean = + productSelectorTypes(tycon, null).exists { + case tp: TypeRef => + (tp.designator: Any) == tparam // Bingo! + case _ => + false + } + + /** Is `tp` an empty type? + * + * `true` implies that we found a proof; uncertainty default to `false`. + */ + def provablyEmpty(tp: Type): Boolean = + tp.dealias match { + case tp if tp.isBottomType => true + case AndType(tp1, tp2) => disjoint(tp1, tp2) + case OrType(tp1, tp2) => provablyEmpty(tp1) && provablyEmpty(tp2) + case at @ AppliedType(tycon, args) => + args.lazyZip(tycon.typeParams).exists { (arg, tparam) => + tparam.paramVariance >= 0 && + provablyEmpty(arg) && + typeparamCorrespondsToField(tycon, tparam) + } + case tp: TypeProxy => + provablyEmpty(tp.underlying) + case _ => false + } + + /** Are `tp1` and `tp2` disjoint types? * * `true` implies that we found a proof; uncertainty default to `false`. @@ -2144,8 +2174,12 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w * * 1. Single inheritance of classes * 2. Final classes cannot be extended - * 3. ConstantTypes with distinc values are non intersecting + * 3. ConstantTypes with distinct values are non intersecting * 4. There is no value of type Nothing + * + * Note on soundness: the correctness of match types relies on on the + * property that in all possible contexts, a same match type expression + * is either stuck or reduces to the same case. */ def disjoint(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = { // println(s"disjoint(${tp1.show}, ${tp2.show})") @@ -2187,27 +2221,13 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w else false case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 => + // It is possible to conclude that two types applies are disjoints by + // looking at covariant type parameters if The said type parameters + // are disjoin and correspond to fields. + // (Type parameter disjointness is not enough by itself as it could + // lead to incorrect conclusions for phantom type parameters). def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = - disjoint(tp1, tp2) && { - // We still need to proof that `Nothing` is not a valid - // instantiation of this type parameter. We have two ways - // to get to that conclusion: - // 1. `Nothing` does not conform to the type parameter's lb - // 2. `tycon1` has a field typed with this type parameter. - // - // Because of separate compilation, the use of 2. is - // limited to case classes. - import dotty.tools.dotc.typer.Applications.productSelectorTypes - val lowerBoundedByNothing = tparam.paramInfo.bounds.lo eq NothingType - val typeUsedAsField = - productSelectorTypes(tycon1, null).exists { - case tp: TypeRef => - (tp.designator: Any) == tparam // Bingo! - case _ => - false - } - !lowerBoundedByNothing || typeUsedAsField - } + disjoint(tp1, tp2) && typeparamCorrespondsToField(tycon1, tparam) args1.lazyZip(args2).lazyZip(tycon1.typeParams).exists { (arg1, arg2, tparam) => @@ -2419,6 +2439,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { }.apply(tp) val defn.MatchCase(pat, body) = cas1 + if (isSubType(scrut, pat)) // `scrut` is a subtype of `pat`: *It's a Match!* Some { @@ -2433,7 +2454,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { else if (isSubType(widenAbstractTypes(scrut), widenAbstractTypes(pat))) Some(NoType) else if (disjoint(scrut, pat)) - // We found a proof that `scrut` and `pat` are incompatible. + // We found a proof that `scrut` and `pat` are incompatible. // The search continues. None else @@ -2445,7 +2466,25 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { case Nil => NoType } - inFrozenConstraint(recur(cases)) + inFrozenConstraint { + // Empty types break the basic assumption that if a scrutinee and a + // pattern are disjoint it's OK to reduce passed that pattern. Indeed, + // empty types viewed as a set of value is always a subset of any other + // types. As a result, we first check that the scrutinee isn't empty + // before proceeding with reduction. See `tests/neg/6570.scala` and + // `6570-1.scala` for examples that exploit emptiness to break match + // type soundness. + + // If we revered the uncertainty case of this empty check, that is, + // `!provablyNonEmpty` instead of `provablyEmpty`, that would be + // obviously sound, but quite restrictive. With the current formulation, + // we need to be careful that `provablyEmpty` covers all the conditions + // used to conclude disjointness in `disjoint`. + if (provablyEmpty(scrut)) + NoType + else + recur(cases) + } } } diff --git a/tests/neg/6314-1.scala b/tests/neg/6314-1.scala index 98adf3d3e644..5d5662c338e3 100644 --- a/tests/neg/6314-1.scala +++ b/tests/neg/6314-1.scala @@ -18,7 +18,7 @@ object G { } def main(args: Array[String]): Unit = { - val a: Bar[X & Y] = "hello" + val a: Bar[X & Y] = "hello" // error val i: Bar[Y & Foo] = Foo.apply[Bar](a) val b: Int = i // error println(b + 1) diff --git a/tests/neg/6314-2.scala b/tests/neg/6314-2.scala index c47ae7a2a950..216e759ca359 100644 --- a/tests/neg/6314-2.scala +++ b/tests/neg/6314-2.scala @@ -12,11 +12,11 @@ object G { case Y => Int } - val a: Bar[X & Foo] = "hello" + val a: Bar[X & Foo] = "hello" // error val b: Bar[Y & Foo] = 1 // error def main(args: Array[String]): Unit = { - val a: Bar[X & Foo] = "hello" + val a: Bar[X & Foo] = "hello" // error val i: Bar[Y & Foo] = Foo.apply[Bar](a) val b: Int = i // error println(b + 1) diff --git a/tests/neg/6570-1.scala b/tests/neg/6570-1.scala new file mode 100644 index 000000000000..046daba285b1 --- /dev/null +++ b/tests/neg/6570-1.scala @@ -0,0 +1,33 @@ +import scala.Tuple._ + +trait Trait1 +trait Trait2 + +case class Box[+T](t: T) + +type N[x] = x match { + case Box[String] => Trait1 + case Box[Int] => Trait2 +} + +trait Cov[+T] +type M[t] = t match { + case Cov[x] => N[x] +} + +trait Root[A] { + def thing: M[A] +} + +class Asploder extends Root[Cov[Box[Int & String]]] { + def thing = new Trait1 {} // error +} + +object Main { + def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing + + def explode = foo(new Asploder) + + def main(args: Array[String]): Unit = + explode +} diff --git a/tests/neg/6570.scala b/tests/neg/6570.scala new file mode 100644 index 000000000000..069aa45313a7 --- /dev/null +++ b/tests/neg/6570.scala @@ -0,0 +1,109 @@ +object Base { + trait Trait1 + trait Trait2 + type N[t] = t match { + case String => Trait1 + case Int => Trait2 + } +} +import Base._ + +object UpperBoundParametricVariant { + trait Cov[+T] + type M[t] = t match { + case Cov[x] => N[x] + } + + trait Root[A] { + def thing: M[A] + } + + trait Child[A <: Cov[Int]] extends Root[A] + + // we reduce `M[T]` to `Trait2`, even though we cannot be certain of that + def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing + + class Asploder extends Child[Cov[String & Int]] { + def thing = new Trait1 {} // error + } + + def explode = foo(new Asploder) // ClassCastException +} + +object InheritanceVariant { + // allows binding a variable to the UB of a type member + type Trick[a] = { type A <: a } + type M[t] = t match { case Trick[a] => N[a] } + + trait Root { + type B + def thing: M[B] + } + + trait Child extends Root { type B <: { type A <: Int } } + + def foo(c: Child): Trait2 = c.thing + + class Asploder extends Child { + type B = { type A = String & Int } + def thing = new Trait1 {} // error + } +} + +object ThisTypeVariant { + type Trick[a] = { type A <: a } + type M[t] = t match { case Trick[a] => N[a] } + + trait Root { + def thing: M[this.type] + } + + trait Child extends Root { type A <: Int } + + def foo(c: Child): Trait2 = c.thing + + class Asploder extends Child { + type A = String & Int + def thing = new Trait1 {} // error + } +} + +object ParametricVariant { + type Trick[a] = { type A <: a } + type M[t] = t match { case Trick[a] => N[a] } + + trait Root[B] { + def thing: M[B] + } + + trait Child[B <: { type A <: Int }] extends Root[B] + + def foo[T <: { type A <: Int }](c: Child[T]): Trait2 = c.thing + + class Asploder extends Child[{ type A = String & Int }] { + def thing = new Trait1 {} // error + } + + def explode = foo(new Asploder) +} + +object UpperBoundVariant { + trait Cov[+T] + type M[t] = t match { case Cov[t] => N[t] } + + trait Root { + type A + def thing: M[A] + } + + trait Child extends Root { type A <: Cov[Int] } + + def foo(c: Child): Trait2 = c.thing + + class Asploder extends Child { + type A = Cov[String & Int] + def thing = new Trait1 {} // error + } + + def explode = foo(new Asploder) +} diff --git a/tests/neg/matchtype-seq.scala b/tests/neg/matchtype-seq.scala index fed785703fd2..79a38fb2f5e4 100644 --- a/tests/neg/matchtype-seq.scala +++ b/tests/neg/matchtype-seq.scala @@ -102,10 +102,10 @@ object Test { identity[T9[Tuple2[Int, String]]](1) identity[T9[Tuple2[String, Int]]]("1") - identity[T9[Tuple2[Nothing, String]]](1) - identity[T9[Tuple2[String, Nothing]]]("1") - identity[T9[Tuple2[Int, Nothing]]](1) - identity[T9[Tuple2[Nothing, Int]]]("1") + identity[T9[Tuple2[Nothing, String]]](1) // error + identity[T9[Tuple2[String, Nothing]]]("1") // error + identity[T9[Tuple2[Int, Nothing]]](1) // error + identity[T9[Tuple2[Nothing, Int]]]("1") // error identity[T9[Tuple2[_, _]]]("") // error identity[T9[Tuple2[_, _]]](1) // error identity[T9[Tuple2[Any, Any]]]("") // error diff --git a/tests/run-staging/staged-tuples/StagedTuple.scala b/tests/run-staging/staged-tuples/StagedTuple.scala index c18902f8a47c..7455af47ea5e 100644 --- a/tests/run-staging/staged-tuples/StagedTuple.scala +++ b/tests/run-staging/staged-tuples/StagedTuple.scala @@ -79,7 +79,7 @@ object StagedTuple { } def headStaged[Tup <: NonEmptyTuple : Type](tup: Expr[Tup], size: Option[Int])(given QuoteContext): Expr[Head[Tup]] = { - if (!specialize) '{dynamicApply($tup, 0)} + if (!specialize) '{dynamicApply[Tup, 0]($tup, 0)} else { val resVal = size match { case Some(1) => diff --git a/tests/run/tuples1.scala b/tests/run/tuples1.scala index 6570ebb850b5..e3978e51ac15 100644 --- a/tests/run/tuples1.scala +++ b/tests/run/tuples1.scala @@ -62,7 +62,8 @@ object Test extends App { def head2[X <: NonEmptyTuple](x: X): Tuple.Head[X] = x.head val hd1: Int = head1(x3) - val hd2: Int = head2(x3) + // Without an explicit type parameter type inferance infers Nothing here. + val hd2: Int = head2[x3.type](x3) def tail1(x: NonEmptyTuple): Tuple.Tail[x.type] = x.tail def tail2[X <: NonEmptyTuple](x: X): Tuple.Tail[X] = x.tail From 7d3ba8fc3184ab63c1907c13a7d4061ba52d38a0 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Thu, 3 Oct 2019 14:54:06 +0200 Subject: [PATCH 2/3] Rename disjoint to provablyDisjoint The new name is explicit about the function output in case of uncertainty. --- .../dotty/tools/dotc/core/TypeComparer.scala | 40 +++++++++---------- .../tools/dotc/transform/patmat/Space.scala | 4 +- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index fe85f023dfdd..bad235a231be 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2152,7 +2152,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w def provablyEmpty(tp: Type): Boolean = tp.dealias match { case tp if tp.isBottomType => true - case AndType(tp1, tp2) => disjoint(tp1, tp2) + case AndType(tp1, tp2) => provablyDisjoint(tp1, tp2) case OrType(tp1, tp2) => provablyEmpty(tp1) && provablyEmpty(tp2) case at @ AppliedType(tycon, args) => args.lazyZip(tycon.typeParams).exists { (arg, tparam) => @@ -2166,7 +2166,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w } - /** Are `tp1` and `tp2` disjoint types? + /** Are `tp1` and `tp2` provablyDisjoint types? * * `true` implies that we found a proof; uncertainty default to `false`. * @@ -2181,8 +2181,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w * property that in all possible contexts, a same match type expression * is either stuck or reduces to the same case. */ - def disjoint(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = { - // println(s"disjoint(${tp1.show}, ${tp2.show})") + def provablyDisjoint(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = { + // println(s"provablyDisjoint(${tp1.show}, ${tp2.show})") /** Can we enumerate all instantiations of this type? */ def isClosedSum(tp: Symbol): Boolean = tp.is(Sealed) && tp.isOneOf(AbstractOrTrait) && !tp.hasAnonymousChild @@ -2215,9 +2215,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w // of classes. true else if (isClosedSum(cls1)) - decompose(cls1, tp1).forall(x => disjoint(x, tp2)) + decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2)) else if (isClosedSum(cls2)) - decompose(cls2, tp2).forall(x => disjoint(x, tp1)) + decompose(cls2, tp2).forall(x => provablyDisjoint(x, tp1)) else false case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 => @@ -2227,7 +2227,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w // (Type parameter disjointness is not enough by itself as it could // lead to incorrect conclusions for phantom type parameters). def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = - disjoint(tp1, tp2) && typeparamCorrespondsToField(tycon1, tparam) + provablyDisjoint(tp1, tp2) && typeparamCorrespondsToField(tycon1, tparam) args1.lazyZip(args2).lazyZip(tycon1.typeParams).exists { (arg1, arg2, tparam) => @@ -2256,29 +2256,29 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w } } case (tp1: HKLambda, tp2: HKLambda) => - disjoint(tp1.resType, tp2.resType) + provablyDisjoint(tp1.resType, tp2.resType) case (_: HKLambda, _) => - // The intersection of these two types would be ill kinded, they are therefore disjoint. + // The intersection of these two types would be ill kinded, they are therefore provablyDisjoint. true case (_, _: HKLambda) => true case (tp1: OrType, _) => - disjoint(tp1.tp1, tp2) && disjoint(tp1.tp2, tp2) + provablyDisjoint(tp1.tp1, tp2) && provablyDisjoint(tp1.tp2, tp2) case (_, tp2: OrType) => - disjoint(tp1, tp2.tp1) && disjoint(tp1, tp2.tp2) + provablyDisjoint(tp1, tp2.tp1) && provablyDisjoint(tp1, tp2.tp2) case (tp1: AndType, tp2: AndType) => - (disjoint(tp1.tp1, tp2.tp1) || disjoint(tp1.tp2, tp2.tp2)) && - (disjoint(tp1.tp1, tp2.tp2) || disjoint(tp1.tp2, tp2.tp1)) + (provablyDisjoint(tp1.tp1, tp2.tp1) || provablyDisjoint(tp1.tp2, tp2.tp2)) && + (provablyDisjoint(tp1.tp1, tp2.tp2) || provablyDisjoint(tp1.tp2, tp2.tp1)) case (tp1: AndType, _) => - disjoint(tp1.tp2, tp2) || disjoint(tp1.tp1, tp2) + provablyDisjoint(tp1.tp2, tp2) || provablyDisjoint(tp1.tp1, tp2) case (_, tp2: AndType) => - disjoint(tp1, tp2.tp2) || disjoint(tp1, tp2.tp1) + provablyDisjoint(tp1, tp2.tp2) || provablyDisjoint(tp1, tp2.tp1) case (tp1: TypeProxy, tp2: TypeProxy) => - disjoint(tp1.underlying, tp2) || disjoint(tp1, tp2.underlying) + provablyDisjoint(tp1.underlying, tp2) || provablyDisjoint(tp1, tp2.underlying) case (tp1: TypeProxy, _) => - disjoint(tp1.underlying, tp2) + provablyDisjoint(tp1.underlying, tp2) case (_, tp2: TypeProxy) => - disjoint(tp1, tp2.underlying) + provablyDisjoint(tp1, tp2.underlying) case _ => false } @@ -2453,7 +2453,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { } else if (isSubType(widenAbstractTypes(scrut), widenAbstractTypes(pat))) Some(NoType) - else if (disjoint(scrut, pat)) + else if (provablyDisjoint(scrut, pat)) // We found a proof that `scrut` and `pat` are incompatible. // The search continues. None @@ -2479,7 +2479,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { // `!provablyNonEmpty` instead of `provablyEmpty`, that would be // obviously sound, but quite restrictive. With the current formulation, // we need to be careful that `provablyEmpty` covers all the conditions - // used to conclude disjointness in `disjoint`. + // used to conclude disjointness in `provablyDisjoint`. if (provablyEmpty(scrut)) NoType else diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala index e86cd9f172bf..b1fdf12aaf50 100644 --- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala +++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala @@ -302,7 +302,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { // Since projections of types don't include null, intersection with null is empty. if (tp1 == nullType || tp2 == nullType) Empty else { - val res = ctx.typeComparer.disjoint(tp1, tp2) + val res = ctx.typeComparer.provablyDisjoint(tp1, tp2) if (res) Empty else if (tp1.isSingleton) Typ(tp1, true) @@ -529,7 +529,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { def inhabited(tp: Type): Boolean = tp.dealias match { - case AndType(tp1, tp2) => !ctx.typeComparer.disjoint(tp1, tp2) + case AndType(tp1, tp2) => !ctx.typeComparer.provablyDisjoint(tp1, tp2) case OrType(tp1, tp2) => inhabited(tp1) || inhabited(tp2) case tp: RefinedType => inhabited(tp.parent) case tp: TypeRef => inhabited(tp.prefix) From 04b2c3e702d5d9f72c38b8bc2e43fda8e708001a Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Thu, 10 Oct 2019 11:00:41 +0200 Subject: [PATCH 3/3] Address review --- .../dotty/tools/dotc/core/TypeComparer.scala | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index bad235a231be..72a935bb6e50 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2140,14 +2140,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w private def typeparamCorrespondsToField(tycon: Type, tparam: TypeParamInfo): Boolean = productSelectorTypes(tycon, null).exists { case tp: TypeRef => - (tp.designator: Any) == tparam // Bingo! + tp.designator.eq(tparam) // Bingo! case _ => false } /** Is `tp` an empty type? * - * `true` implies that we found a proof; uncertainty default to `false`. + * `true` implies that we found a proof; uncertainty defaults to `false`. */ def provablyEmpty(tp: Type): Boolean = tp.dealias match { @@ -2156,9 +2156,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w case OrType(tp1, tp2) => provablyEmpty(tp1) && provablyEmpty(tp2) case at @ AppliedType(tycon, args) => args.lazyZip(tycon.typeParams).exists { (arg, tparam) => - tparam.paramVariance >= 0 && - provablyEmpty(arg) && - typeparamCorrespondsToField(tycon, tparam) + tparam.paramVariance >= 0 + && provablyEmpty(arg) + && typeparamCorrespondsToField(tycon, tparam) } case tp: TypeProxy => provablyEmpty(tp.underlying) @@ -2168,7 +2168,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w /** Are `tp1` and `tp2` provablyDisjoint types? * - * `true` implies that we found a proof; uncertainty default to `false`. + * `true` implies that we found a proof; uncertainty defaults to `false`. * * Proofs rely on the following properties of Scala types: * @@ -2178,7 +2178,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w * 4. There is no value of type Nothing * * Note on soundness: the correctness of match types relies on on the - * property that in all possible contexts, a same match type expression + * property that in all possible contexts, the same match type expression * is either stuck or reduces to the same case. */ def provablyDisjoint(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = { @@ -2221,8 +2221,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w else false case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 => - // It is possible to conclude that two types applies are disjoints by - // looking at covariant type parameters if The said type parameters + // It is possible to conclude that two types applies are disjoint by + // looking at covariant type parameters if the said type parameters // are disjoin and correspond to fields. // (Type parameter disjointness is not enough by itself as it could // lead to incorrect conclusions for phantom type parameters).