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