GADT matching doesn't brings subtyping relation into scope

[IndiscriminateCoding]

Minimized code

object Main extends App:
  enum Extends[A, B]:
    case Ev[B, A <: B]() extends (A Extends B)

    def cast(a: A): B = this match {
      case Extends.Ev() => a
    }

Output

Found:    (a : A)
Required: B

Expectation

I expect A <: B to be visible inside Extends.Ev() case body

[abgruszecki]

This is an interesting issue.

First off, GADTs currently cannot constrain type parameters of classes: https://github.com/lampepfl/dotty/issues/4323 (though this might actually be changing in the future, there's a person on this right now!)

Even if we modify cast to be a standalone function, the following error is emitted:

scala>   enum Extends[A, B]:                                                                                                                                                                                                                                                          
     |     case Ev[B, A <: B]() extends (A Extends B)
     | 
     |   def cast[A, B](a: A, ev: A Extends B): B = ev match {
     |     case Extends.Ev() => a
     |   }
     | 
5 |    case Extends.Ev() => a
  |         ^
  |         Type argument A does not conform to upper bound B

I think this error is not necessary. I will need to take a closer look.

Bottom line is, this works: https://github.com/lampepfl/dotty/blob/master/tests/neg/gadt-approximation-interaction.scala#L1

  enum SUB[-A, +B]:
    case Refl[S]() extends SUB[S, S]

  def foo[T](t: T, ev: T SUB Int) =
    ev match { case SUB.Refl() =>
      t + 2
    }

[IndiscriminateCoding]

I have another case where I expect GADTs to bring contraint to scope:

enum Ev[F <: AnyKind]:
  case HK() extends Ev[List]

def f[F <: AnyKind](ev: Ev[F]): Unit = ev match {
  case Ev.HK() =>
    type T = F[Int] // Error: F does not take type parameters
    ()
}

In this example, Ev.HK is intended to be an evidence that F is of kind F[_] (but it doesn't work). Looks like currently GADTs are only capable of bringing equality contraints to a scope (not subtyping or kind contraints).

[bishabosha]

@IndiscriminateCoding in this example you will have to extract F out using a type pattern:

enum Ev[F <: AnyKind]:                                                                                           
  case HK() extends Ev[List]

def f[F <: AnyKind](ev: Ev[F]): Unit = ev match {
  case Ev.HK(): Ev[f]  =>
    val m: f[Int] = List(1,2,3)
    ()
}

[IndiscriminateCoding]

@bishabosha Interesting! I didn't know that it is possible to introduce local types in such way - is it new (undocumented?) dotty feature?