Dotty: Methods with pattern-matching and dependent types

[japgolly]

Given:

  sealed trait F { type A }
  case object FI extends F { type A = Int }
  case object FS extends F { type A = String }

This snippet:

  def test1a(f: F): f.A =
    f match {
      case FI => 1
      case _: FS.type => ""
    }

fails with:

-- [E007] Type Mismatch Error: <console>:9:19 ----------------------------------
9 |        case FI => 1
  |                   ^
  |                   found:    Int(1)
  |                   required: f.A
-- [E007] Type Mismatch Error: <console>:10:27 ---------------------------------
10 |        case _: FS.type => ""
   |                           ^^
   |                           found:    String("")
   |                           required: f.A

But I can prove it works with a little hacky workaround:

  def test1b(f: F): f.A = {
    def dirtyHack[B](f: F { type A = B }): B =
      f match {
        case FI => 1
        case _: FS.type => ""
      }
    dirtyHack[f.A](f)
  }

Notice that the f match { ... } is the original implementation verbatim.
It would be great if the first snippet worked.

[odersky]

The workaround uses GADT matching but the original does not. It is currently not clear what the rules for such extended GADT matching should be. This would be a worthwhile research problem for somebody to take on. But I don't see an immediate fix.

[julienrf]

I think we should re-open this issue, especially because the “little hacky workaround” doesn’t work anymore: https://scastie.scala-lang.org/l21lZJfsThiUMJlBeSuSsg

[julienrf]

The current specification for typed patterns is the following:

A typed pattern x: T consists of a pattern variable x and a type pattern T. The type of x is the type pattern T.

And, for pattern binders:

A pattern binder x @ p consists of a pattern variable x and a pattern p. The type of the variable x is the static type T implied by the pattern p.

And, for variable patterns:

A variable pattern x is a simple identifier which starts with a lower case letter. It matches any value, and binds the variable name to that value. The type of x is the expected type of the pattern as given from outside.

Would the problem be fixed adding the following?

An _outer_ pattern is a pattern that is not nested in another pattern (such as a constructor pattern). The type of a variable name x introduced by an outer pattern is refined to x.type & e.type, where x.type is the type of x as per the previously described pattern rules, and e.type is the type of the selector expression.
Here is an example that illustrates this rule:
~~~ scala
case class T(nested: Option[T])

def f(t: T): Unit = t match {
case t1 @ T(Some(t2: T)) => println("t1 has type 'T & t.type', but t2 has type 'T'")
}
~~~

cc @AleksanderBG

[Blaisorblade]

I think that's what @AleksanderBG plans, but this is not enough here.

• It’s important that the type of e is not implicitly widened; the translation might need to use SkolemType internally — that is, z.type where z is a fresh variable containing the result of e (assume that e match ... is rewritten to val z = e; z match ...), and where z.type is an actual singleton type.
• BTW, if you want to propose this for the spec, please keep .type as syntax for actual singleton types.
• In this case, I’m not sure that spec is enough. No variables are actually bound by the original program — maybe we should apply this spec also to dummy variables introduced implicitly; so case FI => becomes case x @ FI =>.
• And even if you have a variable x : FI.type & f.type in scope, does that affect whether Int <: f.type? That might need additional effort.

[Blaisorblade]

@AleksanderBG can you reopen this, if you find it interesting/appropriate?

[abgruszecki]

I'll be looking into extending GADT constraints to also work on singleton types. I'll keep this issue on my radar.