Better bounds for inline matches

[julienrf]

The typical code for iterating over a Tuple at the type level looks like the following:

  // summons an instance of the type class `TC` for the tuple type `Elems`
  inline def loop[Elems]: TC[Elems] =
    inline erasedValue[Elems] match
      case _: EmptyTuple.type =>
        val tcEmptyTuple: TC[EmptyTuple.type] = ??? // create an instance of `TC` for the empty tuple
        tcEmptyTuple.asInstanceOf[TC[Elems]]
      case _: (head *: tail) =>
        val tcHead: TC[head] = summonInline[TC[head]]
        val tcTail: TC[tail] = loop[tail]
        val tcHeadTail: TC[head *: tail] = ??? // combine instances for `head` and `tail` according to `TC` abilities
        tcHeadTail.asInstanceOf[TC[Elems]]

Note that we have to use asInstanceOf in the branches of the inline match.

Let me explain my understanding of why these asInstanceOf calls are necessary.

Here is the error message we get if we remove the asInstanceOf:

[error] -- [E007] Type Mismatch Error:
[error] 43 |        tcEmptyTuple
[error]    |        ^^^^^^^^^^^^
[error]    |Found:    tcEmptyTuple : TC[EmptyTuple.type]
[error]    |Required: TC[Elems]
[error]    |
[error]    |where:    Elems is a type in method loop with bounds >: (?1 : EmptyTuple.type)

So, on the right-hand side of case _: EmptyTuple.type =>, the compiler concludes that Elems >: EmptyTuple.type, so returning a TC[EmptyTuple.type] gives a type mismatch error because TC[EmptyTuple.type] is not a subtype of TC[Elems], since TC is invariant in this example.

By the way, I must say that there is one thing I don’t understand: why do we have Elems >: EmptyTuple.type? I would expect the opposite relation: Elems <: EmptyTuple.type.

But, even with this change, the situation would be the same (ie, we would get a type mismatch error). But, what we the compiler could do would be to conclude that, since EmptyTuple.type is a singleton type, the relationship should really be Elems =:= EmptyTuple.type. In such a case, returning a TC[EmptyTuple.type] would type check without the need for an asInstanceOf call.

Now, let’s look at the second case.

[error] -- [E007] Type Mismatch Error:
[error] 53 |        tcHeadTail
[error]    |        ^^^^^^^^^^
[error]    |Found:    tcHeadTail : TC[head *: tail]
[error]    |Required: TC[Elems]
[error]    |
[error]    |where:    Elems is a type in method loop with bounds >: (?1 : head *: tail)
[error]    |          head  is a type in method loop with bounds 
[error]    |          tail  is a type in method loop with bounds <: Tuple

Here, the situation is a bit more subtle. It is similar in the fact that Elems >: (head *: tail). Again, it is not clear to me why the relation is not in the opposite side (Elems <: (head *: tail)).

In such a case, since the type *: is sealed and it has no known subtypes, so the compiler could conclude that Elems =:= (head *: tail), and the asInstanceOf call would not be necessary.

---

I am not sure what feature I am requesting, to be honest. I just found that implementing type class derivation forces us to rely on unsound code, which is unfortunate, and seems to be preventable.

[abgruszecki]

Your reasoning about what the compiler could conclude makes sense. The reason why it doesn't conclude that is that we reason about match and inline match the same way, even though the semantics of inline match allow us to infer more precise information.

For a normal match, if we have a match like ??? : S match { case _ : P => }, we only know that there exists a value which is at the same time of types S and P. To see why, think about List[Nothing] : it can be upcasted to List[String] and it can match a pattern like List() : List[Int], even though there's no subtyping between List[String] and List[Int]. The "weird" bound >: (?1 : head *: tail) is just a quirk of the current implementation.

If someone was feeling adventurous, as far as compiler features go, this one isn't that difficult to implement. The function for constraining pattern types is here. What needs to be done is that we need a different function (say, constrainInlinePatternType) that is called only for patterns of inline match and has more precise logic that @julienrf outlined above. If anyone wanted to implement that, I could help them along.

[julienrf]

I wonder if we need a different mechanism at all, instead of complexifying the existing mechanism.

I’m still experimenting with the API, so I might be doing something absurd, but here is how I would handle different paths of derivation for case classes with optional fields (ie, of type Option[?]) vs mandatory fields:

    val tcHead: TC[head] =
      inline erasedValue[head] match
        case _: Option[inner] =>
          val tc: TC[Option[inner]] = ??? // some code specific to `TC`
          tc
        case _: head =>
          val tc: TC[head] = ??? // some code specific to `TC`
          tc

Of course, I get the following error:

[error] -- [E007] Type Mismatch Error:
[error] 61 |              tc
[error]    |              ^^
[error]    |Found:    TC[Option[inner]]
[error]    |Required: TC[head]
[error]    |
[error]    |where:    head is a type in method summonRecord with bounds >: (?1 : Option[inner])

Here, the reasoning I made in the issue description does not apply. Maybe the type of the field (here, the type head) was Some[?], or None.type. In such a case, returning a TC[Option[inner]] is definitely not correct when a TC[Some[?]] or a TC[None.type] is expected…

So, I would say that we need a mechanism to match exactly on a type. E.g., here I want to check if the type head is exactly Option[?] (and not a subtype of it). That being said, maybe there is already a better way to do that, and I’m just not aware of it?

[bishabosha]

Here is a workaround (add an invariant "box" type):

import compiletime.{erasedValue, summonInline}

trait TC[T]

final case class INV[T] private ()

inline def loop[Elems]: TC[Elems] =
  inline erasedValue[INV[Elems]] match
    case _: INV[EmptyTuple] =>
      val tcEmptyTuple: TC[EmptyTuple] = ??? // create an instance of `TC` for the empty tuple
      tcEmptyTuple
    case _: INV[(head *: tail)] =>
      val tcHead: TC[head] = summonInline[TC[head]]
      val tcTail: TC[tail] = loop[tail]
      val tcHeadTail: TC[head *: tail] = ??? // combine instances for `head` and `tail` according to `TC` abilities
      tcHeadTail

[nicolasstucki]

This seems to be an instance of the following bug #8739

[nicolasstucki]

It might be simpler to implement this with a macro (see https://github.com/lampepfl/dotty/blob/master/tests/run-macros/quoted-ToExpr-derivation-macro/Derivation_1.scala#L50-L53).