Regression on Tuple.Union when using Tuple.toList

[hmf]

Compiler version

Worked on 3.2.1 Fails on 3.2.2-RC2

Minimized code

  val ll0: Tuple3["one", "two", "three"] = constValueTuple[("one", "two", "three")]
  val ll1 = constValueTuple[("one", "two", "three")].toList
  val ll3: List["one" | ("two" | ("three" | Nothing))] = constValueTuple[("one", "two", "three")].toList
  val ll4: List["one" | ("two" | "three")] = constValueTuple[("one", "two", "three")].toList

  inline def labels[Labels <: Tuple](using ev: Tuple.Union[Labels] <:< String): List[String] = 
    val tmp = constValueTuple[Labels].toList
    ev.substituteCo( tmp )

  val strings = labels[("one", "two", "three")]
  // returns List(one, two, three)
  println(strings.mkString("<", ", ", ">"))

Output

error] -- [E007] Type Mismatch Error: /home/hmf/VSCodeProjects/sploty/meta/src/data/Meta1.scala:46:53 
[error] 46 |  val ll1 = constValueTuple[("one", "two", "three")].toList
[error]    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |Found:    List[
[error]    |  Tuple.Union[(?1 : (("one" : String), ("two" : String), ("three" : String)))]
[error]    |]
[error]    |Required: List[("one" : String) | (("two" : String) | (("three" : String) | Nothing))]
[error]    |
[error]    |where:    ?1 is an unknown value of type (("one" : String), ("two" : String), ("three" : String))
[error]    |----------------------------------------------------------------------------
[error]    | Explanation (enabled by `-explain`)
[error]    |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[error]    |
[error]    | Tree: scala.compiletime.constValueTuple[Tuple3["one".type, "two".type, "three".type]].
[error]    |   toList
[error]    | I tried to show that
[error]    |   List[
[error]    |   Tuple.Union[(?1 : (("one" : String), ("two" : String), ("three" : String)))]
[error]    | ]
[error]    | conforms to
[error]    |   List[("one" : String) | (("two" : String) | (("three" : String) | Nothing))]
[error]    | but the comparison trace ended with `false`:
[error]    |
[error]    |   ==> List[   Tuple.Union[(?1 : (("one" : String), ("two" : String), ("three" : String)))] ]  <:  List[("one" : String) | (("two" : String) | (("three" : String) | Nothing))]
[error]    |     ==> Tuple.Union[(?1 : (("one" : String), ("two" : String), ("three" : String)))]  <:  ("one" : String) | (("two" : String) | (("three" : String) | Nothing))
[error]    |       ==> Tuple.Union[(?1 : (("one" : String), ("two" : String), ("three" : String)))]  <:  Nothing
[error]    |         ==> lub(Nothing, ("one" : String), canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, ("one" : String), canConstrain=false, isSoft=true) = ("one" : String)
[error]    |         ==> lub(Nothing, (("two" : String), ("three" : String)), canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, (("two" : String), ("three" : String)), canConstrain=false, isSoft=true) = (("two" : String), ("three" : String))
[error]    |         ==> lub(Nothing, ("two" : String), canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, ("two" : String), canConstrain=false, isSoft=true) = ("two" : String)
[error]    |         ==> lub(Nothing, ("three" : String) *: EmptyTuple.type, canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, ("three" : String) *: EmptyTuple.type, canConstrain=false, isSoft=true) = ("three" : String) *: EmptyTuple.type
[error]    |         ==> lub(Nothing, ("three" : String), canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, ("three" : String), canConstrain=false, isSoft=true) = ("three" : String)
[error]    |         ==> lub(Nothing, EmptyTuple.type, canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, EmptyTuple.type, canConstrain=false, isSoft=true) = EmptyTuple.type
[error]    |         ==> Nothing  <:  ("three" : String) in frozen constraint
[error]    |         <== Nothing  <:  ("three" : String) in frozen constraint = true
[error]    |         ==> lub(<notype>, <notype>, canConstrain=false, isSoft=true)
[error]    |         <== lub(<notype>, <notype>, canConstrain=false, isSoft=true) = <notype>
[error]    |         ==> lub(<notype>, <notype>, canConstrain=false, isSoft=true)
[error]    |         <== lub(<notype>, <notype>, canConstrain=false, isSoft=true) = <notype>
[error]    |         ==> lub(Nothing, ("one" : String), canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, ("one" : String), canConstrain=false, isSoft=true) = ("one" : String)
[error]    |         ==> lub(Nothing, (("two" : String), ("three" : String)), canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, (("two" : String), ("three" : String)), canConstrain=false, isSoft=true) = (("two" : String), ("three" : String))
[error]    |         ==> lub(Nothing, ("two" : String), canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, ("two" : String), canConstrain=false, isSoft=true) = ("two" : String)
[error]    |         ==> lub(Nothing, ("three" : String) *: EmptyTuple.type, canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, ("three" : String) *: EmptyTuple.type, canConstrain=false, isSoft=true) = ("three" : String) *: EmptyTuple.type
[error]    |         ==> lub(Nothing, ("three" : String), canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, ("three" : String), canConstrain=false, isSoft=true) = ("three" : String)
[error]    |         ==> lub(Nothing, EmptyTuple.type, canConstrain=false, isSoft=true)
[error]    |         <== lub(Nothing, EmptyTuple.type, canConstrain=false, isSoft=true) = EmptyTuple.type
[error]    |         ==> ("one" : String) | (("two" : String) | (("three" : String) | Nothing))  <:  Nothing
[error]    |           ==> String  <:  Nothing in frozen constraint
[error]    |           <== String  <:  Nothing in frozen constraint = false
[error]    |           ==> ("one" : String)  <:  Nothing
[error]    |             ==> String  <:  Nothing (left is approximated)
[error]    |             <== String  <:  Nothing (left is approximated) = false
[error]    |           <== ("one" : String)  <:  Nothing = false
[error]    |         <== ("one" : String) | (("two" : String) | (("three" : String) | Nothing))  <:  Nothing = false
[error]    |       <== Tuple.Union[(?1 : (("one" : String), ("two" : String), ("three" : String)))]  <:  Nothing = false
[error]    |     <== Tuple.Union[(?1 : (("one" : String), ("two" : String), ("three" : String)))]  <:  ("one" : String) | (("two" : String) | (("three" : String) | Nothing)) = false
[error]    |   <== List[   Tuple.Union[(?1 : (("one" : String), ("two" : String), ("three" : String)))] ]  <:  List[("one" : String) | (("two" : String) | (("three" : String) | Nothing))] = false

Expectation

That it will compile on the latest Scala compiler version.

[hmf]

Strangely enough,

  val ll0a = ll0.toList

is the only example that fails on both versions.

[nicolasstucki]

Minimized to

def test(tup: ("one", "two", "three")) = tup.toList

1 |def test(tup: ("one", "two", "three")) = tup.toList
  |                                         ^^^^^^^^^^
  |Found:    List[
  |  Tuple.Union[(tup : (("one" : String), ("two" : String), ("three" : String)))]]
  |Required: List[("one" : String) | (("two" : String) | (("three" : String) | Nothing))]

[nicolasstucki]

Bisecting the minimized version I found that the first bad release was 3.0.1-RC1-bin-20210513-b9773d6-NIGHTLY.

[nicolasstucki]

The first bad commit is 9e77a80983abf43be2f766fe2f2d1f343b853d7b in #12356

[nicolasstucki]

The original example started failing in 3.2.1-RC1-bin-20220904-b5fea82-NIGHTLY. First bad commit 46e3d773ce1cae594196dc984356e2629d3fd74a.

[odersky]

https://github.com/lampepfl/dotty/commit/46e3d773ce1cae594196dc984356e2629d3fd74a can cause this only by fixing a bug and therefore uncovering the underltying cause. I am afraid if we want to fix this we'll have to untangle the underlying matchtype resolution. I won't be able to do this; someone else will need to step up.

[mbovel]

Adding a .simplified here would fix it:

       /** True if `tp1` and `tp2` have compatible type constructors and their
        *  corresponding arguments are subtypes relative to their variance (see `isSubArgs`).
        */
-      def isMatchingApply(tp1: Type): Boolean = tp1.widen match {
+      def isMatchingApply(tp1: Type): Boolean = tp1.simplified match {
         case tp1 @ AppliedType(tycon1, args1) =>
           // We intentionally do not automatically dealias `tycon1` or `tycon2` here.
           // `TypeApplications#appliedTo` already takes care of dealiasing type

But I guess simplified is too slow to be called in the type comparer?

[odersky]

Yes, simplified works on a much higher level. But it's maybe a good angle to explore further. What are the types involved where simplified works but widen doesn't?

[mbovel]

I think the problem is when both tp1 and tp2 are AppliedType and tp1 is an unreduced match type.

Problematic isSubtype calls:

==> isSubType List[Tuple.Union[(tup : (("one" : String), ("two" : String), ("three" : String)))]] <:< List[("one" : String) | (("two" : String) | (("three" : String) | Nothing))]?
  ==> isSubType Tuple.Union[(tup : (("one" : String), ("two" : String), ("three" : String)))] <:< ("one" : String) | (("two" : String) | (("three" : String) | Nothing))?
    ==> isSubType Tuple.Union[(tup : (("one" : String), ("two" : String), ("three" : String)))] <:< Nothing

Maybe Tuple.Union[…] should be reduced before recursing the first time?

I also tried:

       def isMatchingApply(tp1: Type): Boolean = tp1.widen match {
+        case MatchType.InDisguise(mt) => isMatchingApply(mt.simplified)
+        case mt: MatchType => isMatchingApply(mt.simplified)
         case tp1 @ AppliedType(tycon1, args1) =>
           // We intentionally do not automatically dealias `tycon1` or `tycon2` here.
           // `TypeApplications#appliedTo` already takes care of dealiasing type

But this is not enough.

I'll further investigate.

[odersky]

Yes, if one of the compared types is a MatchType we should try to normalize it (which means reducing it). I am puzzled why this is not already the case.

[mbovel]

Mmh, that's the problem:

     tp2.atoms match
       case Atoms.Range(lo2, hi2) if canCompareAtoms && canCompare(hi2) =>
         tp1.atoms match
           case Atoms.Range(lo1, hi1) =>
             if hi1.subsetOf(lo2) || knownSingletons && hi2.size == 1 && hi1 == hi2 then
               Some(verified(true))
             else if !lo1.subsetOf(hi2) then
               Some(verified(false))
             else
               None
-          case _ => Some(verified(recur(tp1, NothingType)))
+          case _ => None
       case _ => None

tp2 has atoms, so the comparison stops at case tp2 @ OrType(tp21, tp22) in third try, before having a chance to reduce the application tp1 in fourth try.

[odersky]

Well spotted! Yes, that looks plausible.

[dwijnand]

I've found that add this case to the definition of atoms also fixes Nico's minimisation:

           // this corresponds to the special case in TypeComparer
           // which ensures that `X$ <:< X.type` returns true.
           single(tp.symbol.companionModule.termRef.asSeenFrom(tp.prefix, tp.symbol.owner))
+        case tp: MatchType if tp.reduced.exists =>
+          tp.reduced.atoms
         case tp: TypeProxy =>
           tp.superType.atoms match
             case Atoms.Range(_, hi) => Atoms.Range(Set.empty, hi)

But it doesn't fix the rest of the original....

-- [E007] Type Mismatch Error: tests/pos/i16583.orig.scala:9:36 ----------------
9 |  val tmp = constValueTuple[Labels].toList
  |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |Found:    List[Tuple.Union[(?1 : Labels)]]
  |Required: List[
  |  Labels match {
  |    case EmptyTuple => Nothing
  |    case h *: t => h | scala.Tuple.Fold[t, Nothing, [x, y] =>> x | y]
  |  }
  |]
  |
  |where:    ?1     is an unknown value of type Labels
  |          Labels is a type in method labels with bounds <: Tuple
  |
  |
  |Note: a match type could not be fully reduced:
  |
  |  trying to reduce  Tuple.Union[(?1 : Labels)]
  |  trying to reduce  scala.Tuple.Fold[(?1 : Labels), Nothing, [x, y] =>> x | y]
  |  failed since selector  (?1 : Labels)
  |  does not match  case EmptyTuple => Nothing
  |  and cannot be shown to be disjoint from it either.
  |  Therefore, reduction cannot advance to the remaining case
  |
  |    case h *: t => h | scala.Tuple.Fold[t, Nothing, [x, y] =>> x | y]
  |
  | longer explanation available when compiling with `-explain`

[dwijnand]

tp2 has atoms, so the comparison stops at case tp2 @ OrType(tp21, tp22) in third try, before having a chance to reduce the application tp1 in fourth try.

Not the first time I've wanted isSubType to check both sides for an operation before going to the next case (I ran into this in #16744).

[mbovel]

Maybe:

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index f097bd160fd..8d99a2d2d97 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1578,7 +1578,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               Some(verified(false))
             else
               None
-          case _ => Some(verified(recur(tp1, NothingType)))
+          case _ if knownSingletons =>
+            Some(verified(recur(tp1, NothingType)))
+          case _ =>
+            None
       case _ => None

?

Generally, computing atoms on types that could be further reduced/normalized seems fishy to me.

[Decel]

In case of original It still has the same issue, I believe

-- [E007] Type Mismatch Error: issues/16583/i16583.scala:9:36 ------------------
9 |  val tmp = constValueTuple[Labels].toList
  |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |Found:    List[Tuple.Union[(?1 : Labels)]]
  |Required: List[
  |  Labels match {
  |    case EmptyTuple => Nothing
  |    case h *: t => h | scala.Tuple.Fold[t, Nothing, [x, y] =>> x | y]
  |  }
  |]
  |
  |where:    ?1     is an unknown value of type Labels
  |          Labels is a type in method labels with bounds <: Tuple
  |
  |
  |Note: a match type could not be fully reduced:
  |
  |  trying to reduce  Tuple.Union[(?1 : Labels)]
  |  trying to reduce  scala.Tuple.Fold[(?1 : Labels), Nothing, [x, y] =>> x | y]
  |  failed since selector (?1 : Labels)
  |  does not match  case EmptyTuple => Nothing
  |  and cannot be shown to be disjoint from it either.
  |  Therefore, reduction cannot advance to the remaining case
  |
  |    case h *: t => h | scala.Tuple.Fold[t, Nothing, [x, y] =>> x | y]

[mbovel]

Looking with @Decel; ~we have provablyDisjoint((?1 : Labels), EmptyTuple) === true (!). So Labels match {... } reduces to the second case~ (not at all, no problem in provablyDisjoint actually 😅).

[Decel]

Now with the first part fixed, the issue is the same as #16654

[mbovel]

Thinking about it again, I wonder if this doesn't boil down to invariance of match types not playing well with inferred singleton types.

This does not hold:

type Labels <: Tuple
val x: Labels = ???
val v3: Tuple.Union[Labels] = (???): Tuple.Union[x.type]
// Found:    Tuple.Union[(x : Labels)]
// Required: Tuple.Union[Labels]

Consequently, this also can't hold:

val v2: List[Tuple.Union[Labels]] = (???): List[Tuple.Union[x.type]]

Nor:

val v1: List[
    Labels match
      case EmptyTuple => Nothing
      case h *: t => h | Tuple.Fold[t, Nothing, [x, y] =>> x | y]
] = (???): List[Tuple.Union[x.type]]

So I guess the question is more: why is the skolem (?1 : Labels) widened in the “found" type but not in the “required” one?

[mbovel]

Further minimized:

def toList(x: Tuple): List[Tuple.Union[x.type]] = ???
def test[Labels <: Tuple] = toList((???): Labels)
// Found:    List[Tuple.Union[(?1 : Labels)]]
// Required: List[
//   Labels match {
//     case EmptyTuple => Nothing
//     case h *: t => h | scala.Tuple.Fold[t, Nothing, [x, y] =>> x | y]
//   }
// ]

And without match types or tuples:

type F2[X, Y]
type F[X] = F2[X, X]
def toF(x: Any): F[x.type] = ???
def test[T] = toF((???): T)
// def test[T] = toF((???): T)
//               ^^^^^^^^^^^^^
//               Found:    F[(?1 : T)]
//               Required: F2[T, T]
//               where:    ?1 is an unknown value of type T

Type-avoidance related?

[mbovel]

In some of these cases, the skolem disappears because it is first converted to a TypeBounds in deskolemize:

https://github.com/lampepfl/dotty/blob/528d93189480570532ee20b27814dcc16a014775/compiler/src/dotty/tools/dotc/core/Types.scala#L1427-L1431

And then approximated to its higher bound in Reducer (called from appliedTo):

https://github.com/lampepfl/dotty/blob/528d93189480570532ee20b27814dcc16a014775/compiler/src/dotty/tools/dotc/core/TypeApplications.scala#L141-L146

Reducer approximates arguments for invariant parameters to their higher bounds. Why is that?

[mbovel]

Here is a self-contained example of appliedTo approximating a TypeBounds argument to its higher bound:

val Id = HKTypeLambda(List(T), List(Invariant))(
  _ => List(TypeBounds.empty),
  self => self.paramRefs(0)
)
assertTypesEquiv(
  Id.appliedTo(TypeBounds(defn.NothingType, defn.IntType)),
  defn.IntType
) // Pass

[odersky]

@mbovel That's because the truth for a HKTypeLambda is its structure, not the way it is declared. Declarations are only needed for named types. I.e.

  type Foo[T] = [X] => X

Here, type Foo is declared to be invariant (so it could not override an abstract type declared covariant). But the type lambda is covariant, since its type parameter is only used in covariant positions.

I added an explanation of this in #17554.