Regression on Tuple.Union when using Tuple.toList #16583

hmf · 2022-12-23T15:55:36Z

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.

The text was updated successfully, but these errors were encountered:

hmf · 2022-12-23T16:05:41Z

Strangely enough,

  val ll0a = ll0.toList

is the only example that fails on both versions.

nicolasstucki · 2022-12-26T15:00:53Z

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 · 2022-12-26T15:20:54Z

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

nicolasstucki · 2022-12-26T15:27:12Z

The first bad commit is 9e77a80 in #12356

nicolasstucki · 2022-12-26T15:49:04Z

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

odersky · 2023-01-14T16:35:03Z

46e3d77 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 · 2023-03-07T19:39:40Z

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 · 2023-03-07T20:16:39Z

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 · 2023-03-07T20:35:34Z

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 · 2023-03-07T20:50:37Z

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 · 2023-03-07T21:16:45Z

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 · 2023-03-07T21:45:28Z

Well spotted! Yes, that looks plausible.

dwijnand · 2023-03-07T21:46:52Z

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 · 2023-03-07T21:51:25Z

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 · 2023-03-07T21:57:53Z

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 · 2023-03-07T22:03:15Z

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 · 2023-03-07T22:34:43Z

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 · 2023-03-07T23:27:32Z

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

mbovel · 2023-03-10T11:55:59Z

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 · 2023-03-10T12:07:13Z

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 · 2023-03-12T15:55:53Z

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 · 2023-03-13T13:51:14Z

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 · 2023-05-22T15:42:42Z

@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.

hmf added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Dec 23, 2022

nicolasstucki added area:inline and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Dec 26, 2022

nicolasstucki added the area:match-types label Dec 26, 2022

nicolasstucki removed the area:inline label Dec 26, 2022

prolativ added the regression This worked in a previous version but doesn't anymore label Dec 27, 2022

hmf changed the title ~~Possible regression using constValueTuple woth "3.2.2-RC2"~~ Possible regression using constValueTuple with "3.2.2-RC2" Dec 29, 2022

prolativ modified the milestones: 3.2.2 backports, 3.3.1-RC1 Jan 9, 2023

nicolasstucki mentioned this issue Jan 11, 2023

Regression in gekomad/itto-csv #16654

Closed

nicolasstucki changed the title ~~Possible regression using constValueTuple with "3.2.2-RC2"~~ Regression on Tuple.Union when using Tuple.toList Jan 20, 2023

mbovel self-assigned this Mar 7, 2023

anatoliykmetyuk assigned dwijnand May 22, 2023

Kordyjan modified the milestones: 3.3.1, 3.3.2 May 23, 2023

mbovel mentioned this issue Jun 1, 2023

Fix #16654 and partially fix #16583 #17592

Closed

dwijnand linked a pull request Jun 26, 2023 that will close this issue

Fix match type reduction with avoided types #18043

Merged

dwijnand closed this as completed in #18043 Jul 3, 2023

Kordyjan modified the milestones: 3.3.2, 3.4.0 Aug 1, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Regression on Tuple.Union when using Tuple.toList #16583

Regression on Tuple.Union when using Tuple.toList #16583

hmf commented Dec 23, 2022

hmf commented Dec 23, 2022

nicolasstucki commented Dec 26, 2022

nicolasstucki commented Dec 26, 2022

nicolasstucki commented Dec 26, 2022 •

edited

Loading

nicolasstucki commented Dec 26, 2022

odersky commented Jan 14, 2023

mbovel commented Mar 7, 2023

odersky commented Mar 7, 2023

mbovel commented Mar 7, 2023 •

edited

Loading

odersky commented Mar 7, 2023

mbovel commented Mar 7, 2023

odersky commented Mar 7, 2023

dwijnand commented Mar 7, 2023 •

edited

Loading

dwijnand commented Mar 7, 2023

mbovel commented Mar 7, 2023

Decel commented Mar 7, 2023

mbovel commented Mar 7, 2023 •

edited

Loading

Decel commented Mar 7, 2023

mbovel commented Mar 10, 2023 •

edited

Loading

mbovel commented Mar 10, 2023 •

edited

Loading

mbovel commented Mar 12, 2023 •

edited

Loading

mbovel commented Mar 13, 2023

odersky commented May 22, 2023

Regression on Tuple.Union when using Tuple.toList #16583

Regression on Tuple.Union when using Tuple.toList #16583

Comments

hmf commented Dec 23, 2022

Compiler version

Minimized code

Output

Expectation

hmf commented Dec 23, 2022

nicolasstucki commented Dec 26, 2022

nicolasstucki commented Dec 26, 2022

nicolasstucki commented Dec 26, 2022 • edited Loading

nicolasstucki commented Dec 26, 2022

odersky commented Jan 14, 2023

mbovel commented Mar 7, 2023

odersky commented Mar 7, 2023

mbovel commented Mar 7, 2023 • edited Loading

odersky commented Mar 7, 2023

mbovel commented Mar 7, 2023

odersky commented Mar 7, 2023

dwijnand commented Mar 7, 2023 • edited Loading

dwijnand commented Mar 7, 2023

mbovel commented Mar 7, 2023

Decel commented Mar 7, 2023

mbovel commented Mar 7, 2023 • edited Loading

Decel commented Mar 7, 2023

mbovel commented Mar 10, 2023 • edited Loading

mbovel commented Mar 10, 2023 • edited Loading

mbovel commented Mar 12, 2023 • edited Loading

mbovel commented Mar 13, 2023

odersky commented May 22, 2023

nicolasstucki commented Dec 26, 2022 •

edited

Loading

mbovel commented Mar 7, 2023 •

edited

Loading

dwijnand commented Mar 7, 2023 •

edited

Loading

mbovel commented Mar 7, 2023 •

edited

Loading

mbovel commented Mar 10, 2023 •

edited

Loading

mbovel commented Mar 10, 2023 •

edited

Loading

mbovel commented Mar 12, 2023 •

edited

Loading