`inline` changes code behavior

Question
1

While trying to minimize some code for which the compiler returned an unexpected error, I came upon yet another unexpected behavior for the code below.

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

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

inline def foo(inline n: NatT): NatT = inline mod2(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 Succ(Succ(Succ(Zero()))); unexpected

foo(Succ(Succ(Succ(Zero())))) unexpectedly returns Succ(Succ(Succ(Zero()))). This behavior goes away if all the inline keywords are removed. In that case, it returns Zero(), as expected.

Who is at fault?

2

It’s because of what is and what isn’t compile-time knowable for Scala. When you have mod2(Succ(Succ(Succ(Zero()))) that does eventually resolve to Succ(Zero()) but that’s not reflected in the return type, and the compiler can’t know much about the results of mod2 unless they’re reflected in the return type. Making mod2 transparent inline fixes things to work the way you want.

3

Thanks! It’s useful to know that transparent fixes it in this case.

Shouldn’t there be a compile-error, however? That’s the expected behavior if the compiler cannot reduce it at compile-time, right? In fact, I’ve encountered that behavior several times.

Returning the wrong value still seems like a bug.

4

It’s not really returning the wrong value. You’re not getting a compile time error about failure to reduce because for both of your inline defs you have a wild-card case that matches anything, including results you don’t expect.

1 Like
5

But cases are to be checked sequentially. The wildcard case should only be reached if all the previous cases got ruled out, which is not the case here.

So the wildcard should really be read as “anything except for all the previous cases”.

6

Yes the default case should only trigger after the first one fails, and that’s what happened here. Without transparent, the value cannot be proven to be Succ(Zero()), don’t ask me why, and that case is being passed for the default case where you return n. If I I had to guess why the first case is failing, I’d guess it’s because the recursion in mod2, but I can’t say that for sure.

7

But that’s the thing, the first case did not fail. The compiler might not be able to prove whether it succeeds, but that’s not the same as a failure. Match case failure means the compiler can prove that a case cannot possibly match.

Absence of proof is not proof of absence.

8

But that’s the thing, the first case did not fail.

It does. One thing I did when testing your code was to remove the default case. It might be one thing to argue that it shouldn’t fail (and I’m not sure that follows in inline code, rules are different than with standard scala code), but the case does in fact fail.

Without the default case, you get the unable to reduce error you were looking for, and you get that because the first case doesn’t match mod2’s output when using standard inline.

9

You’re right. Sorry, I should have said “the first case should not have failed”. Inline code does have additional restrictions, but it’s not supposed to evaluate to a different result. So that’s the bug, I guess.

10

ticket