Erratic compiler behavior for inlined function definitions

[Bersier]

See this discussion thread.

Compiler version

3.1.3

Minimized code

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

type Mod2[N <: NatT] <: NatT = N match
  case Zero => Zero
  case Succ[Zero] => Succ[Zero]
  case Succ[Succ[predPredN]] => Mod2[predPredN]

def mod2(n: NatT):  NatT = n match
  case Zero() => Zero()
  case Succ(Zero()) => Succ(Zero())
  case Succ(Succ(predPredN)) => mod2(predPredN)

inline def inlineMod2(inline n: NatT):  NatT = inline n match
  case Zero() => Zero()
  case Succ(Zero()) => Succ(Zero())
  case Succ(Succ(predPredN)) => inlineMod2(predPredN)

transparent inline def transparentInlineMod2(inline n: NatT):  NatT = inline n match
  case Zero() => Zero()
  case Succ(Zero()) => Succ(Zero())
  case Succ(Succ(predPredN)) => transparentInlineMod2(predPredN)

def dependentlyTypedMod2[N <: NatT](n: N): Mod2[N] = n match // exhaustivity warning; unexpected
  case Zero(): Zero => Zero()
  case Succ(Zero()): Succ[Zero] => Succ(Zero())
  case Succ(Succ(predPredN)): Succ[Succ[_]] => dependentlyTypedMod2(predPredN)

inline def inlineDependentlyTypedMod2[N <: NatT](inline n: N): Mod2[N] = inline n match
  case Zero(): Zero => Zero()
  case Succ(Zero()): Succ[Zero] => Succ(Zero())
  case Succ(Succ(predPredN)): Succ[Succ[_]] => inlineDependentlyTypedMod2(predPredN)

transparent inline def transparentInlineDependentlyTypedMod2[N <: NatT](inline n: N): Mod2[N] = inline n match
  case Zero(): Zero => Zero()
  case Succ(Zero()): Succ[Zero] => Succ(Zero())
  case Succ(Succ(predPredN)): Succ[Succ[_]] => transparentInlineDependentlyTypedMod2(predPredN)

def foo(n: NatT): NatT = mod2(n) match
  case Succ(Zero()) => Zero()
  case _ => n

inline def inlineFoo(inline n: NatT): NatT = inline inlineMod2(n) match
  case Succ(Zero()) => Zero()
  case _ => n

inline def transparentInlineFoo(inline n: NatT): NatT = inline transparentInlineMod2(n) match
  case Succ(Zero()) => Zero()
  case _ => n

@main def main(): Unit =
  println(mod2(Succ(Succ(Succ(Zero()))))) // prints Succ(Zero()), as expected
  println(foo(Succ(Succ(Succ(Zero()))))) // prints Zero(), as expected
  println(inlineMod2(Succ(Succ(Succ(Zero()))))) // prints Succ(Zero()), as expected
  println(inlineFoo(Succ(Succ(Succ(Zero()))))) // prints Succ(Succ(Succ(Zero()))); unexpected
  println(transparentInlineMod2(Succ(Succ(Succ(Zero()))))) // prints Succ(Zero()), as expected
  println(transparentInlineFoo(Succ(Succ(Succ(Zero()))))) // prints Zero(), as expected
  println(dependentlyTypedMod2(Succ(Succ(Succ(Zero()))))) // runtime error; unexpected
//  println(inlineDependentlyTypedMod2(Succ(Succ(Succ(Zero()))))) // doesn't compile; unexpected
//  println(transparentInlineDependentlyTypedMod2(Succ(Succ(Succ(Zero()))))) // doesn't compile; unexpected

Output

Succ(Zero())
Zero()
Succ(Zero())
Succ(Succ(Succ(Zero())))
Succ(Zero())
Zero()
[error] java.lang.ClassCastException: Succ cannot be cast to Zero
[error]         at main$package$.dependentlyTypedMod2(main.scala:27)
[error]         at main$package$.main(main.scala:59)
[error]         at main.main(main.scala:52)
[error]         at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[error]         at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
[error]         at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[error]         at java.lang.reflect.Method.invoke(Method.java:498) 

Expectation

1. inlineFoo(Succ(Succ(Succ(Zero())))) should not return Succ(Succ(Succ(Zero()))); inline should not change function output.
2. Compilation should not be negatively affected by more refined types.
3. No runtime exception

[odersky]

@Bersier Do you think you could give this a try to fix yourself?

[Bersier]

@odersky I have no familiarity with the compiler code. If someone gives me an introduction (in a video call) and is willing to help me when I get stuck, I could give it a try.

[odersky]

@Bersier Sorry, I confused you with someone else, who had worked on dotc before.

[odersky]

The first critical problem is if we just compare mod2 and dependentlyTypedMod2. The first is OK, the second fails with the runtime error. Here is their code after typer:

    def mod2(n: NatT): NatT = 
      n match 
        {
          case Zero():Zero => 
            Zero.apply()
          case Succ.unapply[NatT](Zero():Zero):Succ[NatT] => 
            Succ.apply[Zero](Zero.apply())
          case 
            Succ.unapply[NatT](Succ.unapply[NatT](predPredN @ _):Succ[NatT]):
              Succ[NatT]
           => 
            mod2(predPredN)
        }
    def dependentlyTypedMod2[N >: Nothing <: NatT](n: N): Mod2[N] = 
      (n match 
        {
          case Zero():Zero => 
            Zero.apply()
          case Succ.unapply[Zero](Zero()):Succ[Zero] => 
            Succ.apply[Zero](Zero.apply())
          case 
            Succ.unapply[Succ[_]](Succ.unapply[_](predPredN @ _)):
              Succ[Succ[_ @  >: Nothing <: Any]]
           => 
            dependentlyTypedMod2[_](predPredN):Mod2[_]
        }
      ).$asInstanceOf[
        
          N match {
            case Zero => Zero
            case Succ[Zero] => Succ[Zero]
            case Succ[Succ[predPredN]] => Mod2[predPredN]
          } <: NatT
        
      ]

The failing case is the second. Here we see for mod2:

          case Succ.unapply[NatT](Zero():Zero):Succ[NatT] => 
            Succ.apply[Zero](Zero.apply())

and for dependentlyTypedMod2:

          case Succ.unapply[Zero](Zero()):Succ[Zero] => 
            Succ.apply[Zero](Zero.apply())

This seems to assume too much type information. If you show the code after pattern matching that's confirmed. The mod2 code is as follows:

          if x9.$isInstanceOf[Succ[NatT]] then 
            {
              case val x17: Succ[NatT] = 
                Succ.unapply[NatT](x9.$asInstanceOf[Succ[NatT]])
              case val x18: NatT = x17._1
              if 
                x18.$isInstanceOf[Zero].&&(Zero.unapply(x18.$asInstanceOf[Zero])
                  )
               then 
                return[matchResult7] 
                  {
                    Succ.apply[Zero](Zero.apply())
                  }
               else ()

The dependentlyTypedMod2 code is as follows:

          if x21.$isInstanceOf[Succ[Zero]] then 
            {
              case val x28: Succ[Zero] = 
                Succ.unapply[Zero](x21.$asInstanceOf[Succ[Zero]])
              case val x29: Zero = x28._1
              if x29.ne(null).&&(Zero.unapply(x29)) then 
                return[matchResult8] 
                  {
                    Succ.apply[Zero](Zero.apply())
                  }
               else ()
            }
           else ()

Clearly, the RHS of x28 contains an unsound cast.

I believe the difference of the behaviors is due to GADT reasoning in the second case. It seems we are using GADT reasoning (i.e. what can we conclude if the pattern matches) already as input for the pattern matching itself.

[odersky]

In fact after further digging it looks it has nothing to do with GADT reasoning either. The culprit is combined unapply/type test pattern. It seems that's just handled incorrectly.

  case Zero(): Zero => Zero()
  case Succ(Zero()): Succ[Zero] => Succ(Zero())
  case Succ(Succ(predPredN)): Succ[Succ[_]] => dependentlyTypedMod2(predPredN)

Note that patterns like this are disallowed in Scala 2. We might end up doing the same thing.