3.2.0 regression around match types

[Bersier]

Compiler version

3.2-RC1, 3.2-RC2, 3.2-RC3, 3.2-RC4

Minimized code

@main def main(): Unit =
  println(summon[Sum[Minus[Succ[Zero]], Minus[Succ[Zero]]] =:= Minus[Succ[Succ[Zero]]]])

sealed trait IntT
sealed trait NatT extends IntT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT
final case class Minus[+N <: Succ[NatT]](n: N) extends IntT

type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match
  case Zero => X
  case Succ[y] => NatSum[Succ[X], y]

type NatDif[X <: NatT, Y <: NatT] <: IntT = Y match
  case Zero => X
  case Succ[y] => X match
    case Zero => Minus[Y]
    case Succ[x] => NatDif[x, y]

type Sum[X <: IntT, Y <: IntT] <: IntT = Y match
  case Zero => X
  case Minus[y] => X match
    case Minus[x] => Minus[NatSum[x, y]]
    case _ => NatDif[X, y]
  case _ => X match
    case Minus[x] => NatDif[Y, x]
    case _ => NatSum[X, Y]

Output

Cannot prove that Minus[NatSum[Succ[Succ[Zero]], NatT]] =:= Minus[Succ[Succ[Zero]]].

Note: a match type could not be fully reduced:

  trying to reduce  NatSum[Succ[Succ[Zero]], NatT]
  failed since selector  NatT
  does not match  case Zero => Succ[Succ[Zero]]
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case Succ[y] => NatSum[Succ[Succ[Succ[Zero]]], y]

Expectation

Code should compile, as in Scala 3.1.3.

[WojciechMazur]

Bisect points to 02f775f
What's interesting Scala 3.1.3 is the only final version allowing to compile this snippet (started working in 3.1.3-RC2, then started to fail since 3.2.0-RC1-bin-20220531-e2efddc-NIGHTLY)

[Bersier]

Expected reduction:

Sum[Minus[Succ[Zero]], Minus[Succ[Zero]]]
Minus[NatSum[Succ[Zero], Succ[Zero]]]
Minus[NatSum[Succ[Succ[Zero]], Zero]]
Minus[Succ[Succ[Zero]]]

Apparent reduction:

Sum[Minus[Succ[Zero]], Minus[Succ[Zero]]]
Minus[NatSum[Succ[Zero], Succ[Zero]]]
Minus[NatSum[Succ[Succ[Zero]], NatT]]

[anatoliykmetyuk]

This issue was picked for the Issue Spree No. 22 of 18 October 2022 which takes place in a week from now. @dwijnand, @nmcb, @markehammons, @mbovel, @SethTisue will be working on it. If you have any insight into the issue or guidance on how to fix it, please leave it here.

[SethTisue]

notes on the minimization:

• changing Zero to a case object (and using Zero.type in place of Zero) doesn't matter, so I guess we'll leave that as is
• the (n: N)s can be removed
• NatDif plays no role here, so we can delete it and write Sum and NatSum as follows:

type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match                                                 
  case Zero => X                                                                                    
  case Succ[y] => NatSum[Succ[X], y]                                                                
                                                                                                    
type Sum[X <: IntT, Y <: IntT] <: IntT = Y match                                                    
  case Minus[y] => X match                                                                          
    case Minus[x] => Minus[NatSum[x, y]]                                                            

here's a little script for verifying the pos/neg status on four relevant Scala versions:

scala-cli compile -S 3.1.2     . || echo "it failed on 3.1.2"
scala-cli compile -S 3.1.3     . && echo "it compiled on 3.1.3"
scala-cli compile -S 3.2.0-RC1 . || echo "it failed on 3.2.0-RC1"
scala-cli compile -S 3.nightly . || echo "it failed on 3.nightly"

[SethTisue]

and sadly, the bug only reproduces if you go through the first reduction step first. if you just write the second reduction step directly:

summon[Minus[NatSum[Succ[Zero], Succ[Zero]]] =:= Minus[NatSum[Succ[Succ[Zero]], Zero]]]

then it compiles in all four Scala versions 😭

[SethTisue]

We hope to find some connection with type avoidance, since that's the subject of the reverted PR Wojciech identified (#15341 reverted #13780).

Dale observes that in this code:

type Sum[X <: IntT, Y <: IntT] <: IntT = Y match                                                    
  case Minus[y] => X match                                                                          
    case Minus[x] => Minus[NatSum[x, y]]

perhaps type avoidance is inappropriately kicking in thinking that y needs to be avoided in NatSum[x,y]

[SethTisue]

The story of changes to type avoidance in the compiler has become convoluted.

Wojciech's bisect points to #15341 which partially reverted Olivier's #13780. But this is part of a larger story summarized at #15373.

Along the way, Guillaume's big type avoidance PR #14026 was first merged, then reverted, but not completely — the code was kept, but put behind a flag. More recent development is Martin's level-checking PR, #15746, and another PR by Martin, #15423.

(I hope I haven't misrepresented the story. At minimum, these are relevant issue and PR numbers.)

[SethTisue]

I failed to find any further useful minimizations, but I'm also not sure I tried every possible avenue :-/

[nmcb]

After thought having played around with the issue - changing the match of NatSum to below, ie. with the additional Succ[Zero] case makes the example compile; We expect this is because the Succ[Zero] match reduces to Zero, a more concrete type than the observed NatT, thus allowing the Sum match type to match the expected Zero directly:

type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match
  case Zero => X
  case Succ[Zero] => NatSum[Succ[X], Zero]
  case Succ[y] => NatSum[Succ[X], y]

[smarter]

We ruled out type avoidance (turning it off completely doesn't make a difference), the issue does go away if canWidenAbstract is set to false in https://github.com/lampepfl/dotty/blob/96d4ccdcfc3e0ff4d62e969374b92b6db590ccd3/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L3139

[mbovel]

Extracting the inner match makes the code compile:

type Sum[X <: IntT, Y <: IntT] <: IntT = Y match
  case Zero => X
  case Minus[y] => Sum1[X, y]
  case _ => X match
    case Minus[x] => NatDif[Y, x]
    case _ => NatSum[X, Y]

type Sum1[X <: IntT, y <: IntT] <: IntT = X match
  case Minus[x] => Minus[NatSum[x, y]]
  case _ => NatDif[X, y]

[mbovel]

That would also solves this issue:

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 8eb6a490010..dbe89ec385e 100644
-      else if matches(canWidenAbstract = true) then
+      else if !caseLambda.exists && matches(canWidenAbstract = true) then

But make these 2 OK tests fail:

https://github.com/lampepfl/dotty/blob/96d4ccdcfc3e0ff4d62e969374b92b6db590ccd3/tests/neg/wildcard-match.scala#L26-L37

It's really about the heuristics of when to widen abstract types and when not to.

[dwijnand]

We purposely backed out an overly restricting change because of the code that failed to compile because of it. So there was one patch version where it compiled and then not. So not a "regression" as I see it.