@@ -267,8 +267,8 @@ trait SpaceLogic {
267
267
else
268
268
// `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
269
269
Or (ss1.zip(ss2).map((minus _).tupled).zip(0 to ss2.length - 1 ).map {
270
- case (ri, i) => Prod (tp1, fun1, sym1, ss1.updated(i, ri), full)
271
- })
270
+ case (ri, i) => Prod (tp1, fun1, sym1, ss1.updated(i, ri), full)
271
+ })
272
272
273
273
}
274
274
@@ -561,7 +561,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
561
561
562
562
val resTp = instantiate(childTp, parent)(ctx.fresh.setNewTyperState())
563
563
564
- if (! resTp.exists) {
564
+ if (! resTp.exists || ! inhabited(resTp) ) {
565
565
debug.println(s " [refine] unqualified child ousted: ${childTp.show} !< ${parent.show}" )
566
566
NoType
567
567
}
@@ -571,6 +571,25 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
571
571
}
572
572
}
573
573
574
+ /** Can this type be inhabited by a value?
575
+ *
576
+ * Intersection between singleton types and other types is always empty
577
+ * the singleton type is not a subtype of the other type.
578
+ * See patmat/i3573.scala for an example.
579
+ */
580
+ def inhabited (tpe : Type )(implicit ctx : Context ): Boolean = {
581
+ val emptySingletonIntersection = new ExistsAccumulator ({
582
+ case AndType (s : SingletonType , t) =>
583
+ ! (s <:< t)
584
+ case AndType (t, s : SingletonType ) =>
585
+ ! (s <:< t)
586
+ case x =>
587
+ false
588
+ })
589
+
590
+ ! emptySingletonIntersection(false , tpe)
591
+ }
592
+
574
593
/** Instantiate type `tp1` to be a subtype of `tp2`
575
594
*
576
595
* Return the instantiated type if type parameters and this type
@@ -625,7 +644,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
625
644
val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) }
626
645
val protoTp1 = thisTypeMap(tp1.appliedTo(tvars))
627
646
628
- val result = if (protoTp1 <:< tp2) {
647
+ if (protoTp1 <:< tp2) {
629
648
if (isFullyDefined(protoTp1, force)) protoTp1
630
649
else instUndetMap(protoTp1)
631
650
}
@@ -640,24 +659,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
640
659
NoType
641
660
}
642
661
}
643
-
644
- // The intersection between a singleton type s and another type t is
645
- // always empty when s is not a subtype of t. See patmat/i3573.scala
646
- val hasEmptyIntersections = new ExistsAccumulator ({
647
- case AndType (s : SingletonType , t) =>
648
- ! (s <:< t)
649
- case AndType (t, s : SingletonType ) =>
650
- ! (s <:< t)
651
- case x =>
652
- false
653
- })
654
-
655
- if (hasEmptyIntersections(false , result)) {
656
- debug.println(s " hasEmptyIntersections( $protoTp1) = true " )
657
- NoType
658
- } else {
659
- result
660
- }
661
662
}
662
663
663
664
/** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
0 commit comments