Dotty: Cannot return member of refined type from pattern match - Type Mismatch Error

[Sciss]

Minimized code

package patmat

object UGB {
  trait Value
  final case class Bar() extends Value
  final case class Baz() extends Value

  final case class Foo() extends Input {
    type Value = Bar
  }

  final case class Quux() extends Input {
    type Value = Baz
  }

  trait Input {
    type Value <: UGB.Value
  }
}

trait Test {
  def request[Res](in: UGB.Input { type Value = Res }): Res =
    in match {
      case _: UGB.Foo   => UGB.Bar()
      case _: UGB.Quux  => UGB.Baz()
    }
}

Output

[error] 24 |      case _: UGB.Foo   => UGB.Bar()
[error]    |                           ^^^^^^^^^
[error]    |                           Found:    patmat.UGB.Bar
[error]    |                           Required: Res
[error] -- [E007] Type Mismatch Error: /data/temp/DottyPathDepPatProblem/src/main/scala/patmat/Test.scala:25:34 
[error] 25 |      case _: UGB.Quux  => UGB.Baz()
[error]    |                           ^^^^^^^^^
[error]    |                           Found:    patmat.UGB.Baz
[error]    |                           Required: Res
[error] two errors found

Expectation

Should compile (does in Scala 2)

[Sciss]

If there was a work-around, any hint would be appreciated!

[smarter]

Replacing the type member by a type parameter would probably work

@abgruszecki Can the GADT logic handle type members?

[Sciss]

yes, type param worked in my case!

[LPTK]

This is the usual limitation of GADT type info not being picked up when you don't use the corresponding terms directly.

So an alternative workaround is:

  def request[Res](in: UGB.Input { type Value = Res }): Res =
    in match {
      case x: (UGB.Foo & in.type)   => UGB.Bar(): x.Value
      case x: (UGB.Quux & in.type)  => UGB.Baz(): x.Value
    }

[Sciss]

although & in.type won't compile in Scala 2

[LPTK]

I'm afraid the Scala 2 support for GADTs is completely broken anyways 🤷

You could in theory use with instead of &, but it will probably not work well if at all.

[abgruszecki]

GADT logic doesn't record constraints based on refinements right now. The simplest way to make the example from the OP work would be, I think, what @LPTK suggested. There's also no need for the type param as far as I can tell, the function might as well return in.Value.

Reg. GADT logic and type member interaction: there's nothing fundamental preventing it from working, it's just that it turned out that implementing it seemed to require duplicating type comparison code for type members and I simply ran out of time for my semester project. If there was a good example of code that needed this sort of reasoning, I could take another look at the relevant GADT logic.