Inline matches don't refine on the RHS

[milessabin]

Equalities between types established by the cases of inline matches aren't known on the RHS,

object Test {
  import scala.compiletime._
  inline def foo[T](t: T): T =
    inline erasedValue[T] match {
      case _: Int => 23
      case _ => t
    }
}
-- [E007] Type Mismatch Error: tests/run/typeclass-derivation3.scala:5:21 ----
  5 |      case _: Int => 23
    |                     ^^
    |                     found:    Int(23)
    |                     required: T
one error found

Adding a cast allows this to compile,

object Test {
  import scala.compiletime._
  inline def foo[T](t: T): T =
    inline erasedValue[T] match {
      case _: Int => 23.asInstanceOf[T]
      case _ => t
    }
}

[abgruszecki]

I've taken a look at this and it seems that we cannot allow this code to compile, since T is in fact in covariant position, so all we can infer is that T <: Int. Consider how replacing _: Int with _: Any should behave from inlining perspective when foo[Int] is called.

This very similar example compiles with #5657 (and may even compile on master):

object `inline-match-gadt` {
  class Exactly[T]
  erased def exactType[T]: Exactly[T] = ???

  inline def foo[T](t: T): T =
    inline exactType[T] match {
      case _: Exactly[Int] => 23
      case _ => t
    }
}

@milessabin do you think we should add something like exactType and Exactly to scala.typelevel?

[milessabin]

@AleksanderBG gotcha.

I think we need to think a bit more about things like erasedValue and exactType. My intuitions were that using erasedValue would have the semantics you've shown for exactType ... I don't have much of a feel for whether that's my idiosyncrasy or if other people would have similar expectations.

In any case the following also works on master,

object Test {
  import scala.typelevel._
  type Inv[t] = t
  inline def foo[T](t: T): T =
    inline erasedValue[Inv[T]] match {
      case _: Int => 23
      case _ => t
    }
}

so we could tweak erasedValue to return Inv[T] if we decide that exact semantics are what would typically be expected.

[abgruszecki]

@milessabin Regarding erasedValue - the nice thing about it is it has no special semantics. Typecase patterns like _: Int in inline matches match when scrutinee type is a subtype of Int, which mirrors normal runtime pattern matching behaviour. In your original example, we cannot allow the code to compile because we're still not sure if 23 is of type T - consider:

object Test {
  import scala.typelevel._
  inline def foo[T](t: T): T = inline erasedValue[T] match {
    case _: Int => 23
    case _ => t
  }
  val notFive: 5 = foo[5](5) // === 23 !

To allow this code to compile, we would need to reduce typecase patterns only if they are equivalent to scrutinee type, but this seems to me even more surprising - consider:

object Test {
  inline def test = {
    inline val five = 5 // five is of type 5
    inline five match {
      case _: Int => true
      case _ => false
    }
  }
  val doesFiveMatchInt = test // false !
}

Also note that your last example also allows returning 23 as a value of type 5, so it's a bug and it'll have to be fixed.

To sum up: I think it's clear that the interaction between erasedValue and typing rules may be suprising. At the same time, it requires no special-case behaviour or syntax. For the time being, I'd recommend experimenting with something like this:

object Test {
  final abstract class Type[-A, +B]
  erased def typeof[T]: Type[T, T] = ???
  type Exactly[t]= Type[t, t]
  type Subtype[t] = Type[_, t]
  type Supertype[t] = Type[t, _]

  inline def isExactlyInt[t] = inline typeof[t] match {
    case _: Exactly[Int] => true
    case _ => false
  }

  isExactlyInt[Int] // true
  isExactlyInt[5] // false

  inline def isSubOfInt[t] = inline typeof[t] match {
    case _: Subtype[Int] => true
    case _ => false
  }

  isSubOfInt[Int] && isSubOfInt[5] // true
}

Alternatively, we could add special syntax for inline type matches. The downside I'm seeing immediately is that it'd be no longer possible to match both on a value and a type at the same time. I'll think about it a little bit more and open a PR/issue later.

[milessabin]

Ahh ... I'd missed that the use of the Inv type could hide unsoundness in that way.

Anyhow, all understood.

I like the look of typeof ... I definitely like it more than erasedValue. Consideration along these lines was what I had in mind when I said "I think we need to think a bit more about things like erasedValue ...".

@odersky I think we should replace erasedValue with @AleksanderBG's typeof above.

[abgruszecki]

@milessabin the reason why I don't want to merge this outright is:

1. it makes simple matches more verbose
2. It actually doesn't, after I checked, allow properly typing the methods, since we don't infer GADT bounds for variant symbols during normal compilation.

See #5683, in particular the annoying changes in typeclass-derivation and that typelevel-defaultValue does not pass tests.

[abgruszecki]

@biboudis @nicolasstucki I think this issue perfectly captures what we talked about on Monday. In particular see my comment #5564 (comment) which goes in detail on why we cannot allow erasedValue to work like one may expect it to and a potential hacky workaround.