Skip to content

Commit 7388f6c

Browse files
committed
make exhaustivity check work on native apply
1 parent 6e50ab3 commit 7388f6c

File tree

3 files changed

+88
-96
lines changed

3 files changed

+88
-96
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -972,7 +972,7 @@ object Types {
972972
case app @ AppliedType(tycon, args) =>
973973
val tycon1 = tycon.dealias(keepAnnots)
974974
if (tycon1 ne tycon) app.superType.dealias(keepAnnots): @tailrec
975-
else this
975+
else app.derivedAppliedType(tycon, args.map(_.dealias))
976976
case tp: TypeVar =>
977977
val tp1 = tp.instanceOpt
978978
if (tp1.exists) tp1.dealias(keepAnnots): @tailrec else tp

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

Lines changed: 86 additions & 94 deletions
Original file line numberDiff line numberDiff line change
@@ -403,20 +403,31 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
403403
else
404404
Prod(pat.tpe.stripAnnots, fun.tpe.widen, fun.symbol, pats.map(project), irrefutable(fun))
405405
case Typed(pat @ UnApply(_, _, _), _) => project(pat)
406-
case Typed(expr, _) => Typ(expr.tpe.stripAnnots, true)
406+
case Typed(expr, _) => Typ(erase(expr.tpe.stripAnnots), true)
407407
case _ =>
408408
debug.println(s"unknown pattern: $pat")
409409
Empty
410410
}
411411

412+
/* Erase a type binding according to erasure semantics in pattern matching */
413+
def erase(tp: Type): Type = tp match {
414+
case tp@AppliedType(tycon, args) => erase(tp.superType)
415+
if (tycon.isRef(defn.ArrayClass)) tp.derivedAppliedType(tycon, args.map(erase))
416+
else tp.derivedAppliedType(tycon, args.map(t => WildcardType(TypeBounds.empty)))
417+
case OrType(tp1, tp2) =>
418+
OrType(erase(tp1), erase(tp2))
419+
case AndType(tp1, tp2) =>
420+
AndType(erase(tp1), erase(tp2))
421+
case _ => tp
422+
}
412423

413424
/** Space of the pattern: unapplySeq(a, b, c: _*)
414425
*/
415426
def projectSeq(pats: List[Tree]): Space = {
416427
if (pats.isEmpty) return Typ(scalaNilType, false)
417428

418429
val (items, zero) = if (pats.last.tpe.isRepeatedParam)
419-
(pats.init, Typ(scalaListType.appliedTo(pats.head.tpe.widen), false))
430+
(pats.init, Typ(scalaListType.appliedTo(pats.last.tpe.argTypes.head), false))
420431
else
421432
(pats, Typ(scalaNilType, false))
422433

@@ -428,41 +439,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
428439
}
429440
}
430441

431-
432-
/* Erase a type binding according to erasure semantics in pattern matching */
433-
def erase(tp: Type): Type = {
434-
def doErase(tp: Type): Type = tp match {
435-
case tp: AppliedType => erase(tp.superType)
436-
case tp: RefinedType => erase(tp.parent)
437-
case _ => tp
438-
}
439-
440-
tp match {
441-
case OrType(tp1, tp2) =>
442-
OrType(erase(tp1), erase(tp2))
443-
case AndType(tp1, tp2) =>
444-
AndType(erase(tp1), erase(tp2))
445-
case _ =>
446-
val origin = doErase(tp)
447-
if (origin =:= defn.ArrayType) tp else origin
448-
}
449-
}
450-
451442
/** Is `tp1` a subtype of `tp2`? */
452443
def isSubType(tp1: Type, tp2: Type): Boolean = {
453-
// `erase` is a workaround to make the following code pass the check:
454-
//
455-
// def f(e: Either[Int, String]) = e match {
456-
// case Left(i) => i
457-
// case Right(s) => 0
458-
// }
459-
//
460-
// The problem is that when decompose `Either[Int, String]`, `Type.wrapIfMember`
461-
// only refines the type member inherited from `Either` -- it's complex to refine
462-
// the type members in `Left` and `Right`.
463-
//
464-
// FIXME: remove this hack
465-
val res = tp1 <:< erase(tp2)
444+
val res = tp1 <:< tp2
466445
debug.println(s"${tp1.show} <:< ${tp2.show} = $res")
467446
res
468447
}
@@ -563,15 +542,15 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
563542

564543
val childTp = if (child.isTerm) child.termRef else child.typeRef
565544

566-
val resTp = instantiate(childTp, expose(parent))(ctx.fresh.setNewTyperState)
545+
var resTp = instantiate(childTp, expose(parent))(ctx.fresh.setNewTyperState)
567546

568547
if (!resTp.exists) {
569548
debug.println(s"[refine] unqualified child ousted: ${childTp.show} !< ${parent.show}")
570549
NoType
571550
}
572551
else {
573552
debug.println(s"$child instantiated ------> $resTp")
574-
resTp
553+
resTp.dealias
575554
}
576555
}
577556

@@ -588,8 +567,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
588567
// precondition: `tp1` should have the shape `path.Child`, thus `ThisType` is always covariant
589568
val thisTypeMap = new TypeMap {
590569
def apply(t: Type): Type = t match {
591-
case t @ ThisType(tref) if !tref.symbol.isStaticOwner && !tref.symbol.is(Module) =>
592-
newTypeVar(TypeBounds.upper(mapOver(tref & tref.givenSelfType)))
570+
case tp @ ThisType(tref) if !tref.symbol.isStaticOwner && !tref.symbol.is(Module) =>
571+
// TODO: stackoverflow here
572+
// newTypeVar(TypeBounds.upper(mapOver(tp.underlying)))
573+
newTypeVar(TypeBounds.upper(mapOver(tref & tref.classSymbol.asClass.givenSelfType)))
593574
case _ =>
594575
mapOver(t)
595576
}
@@ -598,10 +579,34 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
598579
val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) }
599580
val protoTp1 = thisTypeMap(tp1.appliedTo(tvars))
600581

601-
if (protoTp1 <:< tp2 && isFullyDefined(protoTp1, ForceDegree.all)) protoTp1
582+
// replace type parameter references with fresh type vars or bounds
583+
val typeParamMap = new TypeMap {
584+
def apply(t: Type): Type = t match {
585+
586+
case tp: TypeRef if tp.underlying.isInstanceOf[TypeBounds] =>
587+
// See tests/patmat/gadt.scala tests/patmat/exhausting.scala
588+
val bound =
589+
if (variance == 0) tp.underlying.bounds // non-variant case is not well-founded
590+
else if (variance == 1) TypeBounds.upper(tp)
591+
else TypeBounds.lower(tp)
592+
newTypeVar(bound)
593+
case tp: RefinedType if tp.refinedInfo.isInstanceOf[TypeBounds] =>
594+
// Ideally, we would expect type inference to do the job
595+
// Check tests/patmat/t9657.scala
596+
expose(tp)
597+
case _ =>
598+
mapOver(t)
599+
}
600+
}
601+
602+
if (protoTp1 <:< tp2 && isFullyDefined(protoTp1, ForceDegree.noBottom)) protoTp1
602603
else {
603-
debug.println(s"$protoTp1 <:< $tp2 = false")
604-
NoType
604+
val protoTp2 = typeParamMap(tp2)
605+
if (protoTp1 <:< protoTp2 && isFullyDefined(protoTp1 & protoTp2, ForceDegree.noBottom)) protoTp1
606+
else {
607+
debug.println(s"$protoTp1 <:< $protoTp2 = false")
608+
NoType
609+
}
605610
}
606611
}
607612

@@ -652,6 +657,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
652657

653658
def refine(tp: Type): String = tp match {
654659
case tp: RefinedType => refine(tp.parent)
660+
case tp: AppliedType => refine(tp.typeConstructor)
655661
case tp: ThisType => refine(tp.tref)
656662
case tp: NamedType =>
657663
val pre = refinePrefix(tp.prefix)
@@ -740,64 +746,50 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
740746
}
741747

742748

743-
/** Expose refined type to eliminate reference to type variables
744-
*
745-
* A = B M { type T = A } ~~> M { type T = B }
746-
*
747-
* A <: X :> Y M { type T = A } ~~> M { type T <: X :> Y }
749+
/** Eliminate reference to type parameters in refinements
748750
*
749751
* A <: X :> Y B <: U :> V M { type T <: A :> B } ~~> M { type T <: X :> V }
750-
*
751-
* A = X B = Y M { type T <: A :> B } ~~> M { type T <: X :> Y }
752752
*/
753-
def expose(tp: Type): Type = {
754-
def follow(tp: Type, up: Boolean): Type = tp match {
755-
case tp: TypeProxy =>
756-
tp.underlying match {
757-
case TypeBounds(lo, hi) =>
758-
follow(if (up) hi else lo, up)
759-
case _ =>
760-
tp
761-
}
762-
case OrType(tp1, tp2) =>
763-
OrType(follow(tp1, up), follow(tp2, up))
764-
case AndType(tp1, tp2) =>
765-
AndType(follow(tp1, up), follow(tp2, up))
766-
}
753+
def expose(tp: Type, refineCtx: Boolean = false, up: Boolean = true): Type = tp match {
754+
case tp: AppliedType =>
755+
tp.derivedAppliedType(expose(tp.tycon, refineCtx, up), tp.args.map(expose(_, refineCtx, up)))
767756

768-
tp match {
769-
case tp: RefinedType =>
770-
tp.refinedInfo match {
771-
case tpa : TypeAlias =>
772-
val hi = follow(tpa.alias, true)
773-
val lo = follow(tpa.alias, false)
774-
val refined = if (hi =:= lo)
775-
tpa.derivedTypeAlias(hi)
776-
else
777-
tpa.derivedTypeBounds(lo, hi)
778-
779-
tp.derivedRefinedType(
780-
expose(tp.parent),
781-
tp.refinedName,
782-
refined
783-
)
784-
case tpb @ TypeBounds(lo, hi) =>
785-
tp.derivedRefinedType(
786-
expose(tp.parent),
787-
tp.refinedName,
788-
tpb.derivedTypeBounds(follow(lo, false), follow(hi, true))
789-
)
790-
case _ =>
791-
tp.derivedRefinedType(
792-
expose(tp.parent),
793-
tp.refinedName,
794-
tp.refinedInfo
795-
)
796-
}
797-
case _ => tp
798-
}
757+
case tp: TypeAlias =>
758+
val hi = expose(tp.alias, refineCtx, up)
759+
val lo = expose(tp.alias, refineCtx, up)
760+
761+
if (hi =:= lo)
762+
tp.derivedTypeAlias(hi)
763+
else
764+
tp.derivedTypeBounds(lo, hi)
765+
766+
case tp @ TypeBounds(lo, hi) =>
767+
tp.derivedTypeBounds(expose(lo, refineCtx, false), expose(hi, refineCtx, true))
768+
769+
case tp: RefinedType =>
770+
tp.derivedRefinedType(
771+
expose(tp.parent),
772+
tp.refinedName,
773+
expose(tp.refinedInfo, true, up)
774+
)
775+
case tp: TypeProxy if refineCtx =>
776+
tp.underlying match {
777+
case TypeBounds(lo, hi) =>
778+
expose(if (up) hi else lo, refineCtx, up)
779+
case _ =>
780+
tp
781+
}
782+
783+
case OrType(tp1, tp2) =>
784+
OrType(expose(tp1, refineCtx, up), expose(tp2, refineCtx, up))
785+
786+
case AndType(tp1, tp2) =>
787+
AndType(expose(tp1, refineCtx, up), expose(tp2, refineCtx, up))
788+
789+
case _ => tp
799790
}
800791

792+
801793
def checkExhaustivity(_match: Match): Unit = {
802794
val Match(sel, cases) = _match
803795
val selTyp = sel.tpe.widen.dealias

compiler/test/dotty/tools/dotc/transform/PatmatExhaustivityTest.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ class PatmatExhaustivityTest {
6565
(file, checkContent, actual)
6666
}
6767

68-
// @Test // TODO: reenable when exchaustivity is fixed
68+
@Test
6969
def patmatExhaustivity: Unit = {
7070
val res = Directory(testsDir).list.toList
7171
.filter(f => f.extension == "scala" || f.isDirectory)

0 commit comments

Comments
 (0)