Trait with type parameter does not specialize match result type

[atennapel]

Compiler version

3.0

Minimized code

sealed trait Ty {
  type T
}
case object TUnit extends Ty {
  type T = Unit
}
final case class TFun(dom: Ty, cod: Ty) extends Ty {
  type T = dom.T => cod.T
}

def default(ty: Ty): ty.T = ty match {
  case TUnit => ()
  case TFun(dom, cod) => { (x: dom.T) => default(cod) }
}

Output

Found:    Unit
Required: ty.T

Found:    dom.T => cod.T
Required: ty.T

Expectation

I expected the result type inside of the match to be specialized to Unit for TUnit and dom.T => cod.T for TFun, but this is not the case. It may be the case that I expect too much though.

With GADTs the result types are specialized, but I cannot type the x in the case of TFun, because I have no access to the type parameters of TFun:

sealed trait Ty[T]
case object TUnit extends Ty[Unit]
final case class TFun[A, B](dom: Ty[A], cod: Ty[B]) extends Ty[A => B]

def default[T](ty: Ty[T]): T = ty match {
  case TUnit => ()
  case TFun(dom, cod) => { x => default(cod) }
  /*
  Missing parameter type

  I could not infer the type of the parameter x.
  */
}

[LPTK]

GADT reasoning does not yet look at type members AFAIK. Here is an ugly workaround that wrangles the proofs manually:

sealed trait Ty {
  type T
}
class TUnit() extends Ty {
  type T = Unit
}
case object TUnit extends TUnit()
final case class TFun(dom: Ty, cod: Ty) extends Ty {
  type T = dom.T => cod.T
}
def default(ty: Ty): ty.T = ty match {
  case ty: (ty.type & TUnit) => (): ty.T
  case ty: (ty.type & TFun) =>
    val f = { (x: ty.dom.T) => default(ty.cod) }
    f: ty.T
}

The reason I had to make TUnit a class is that Dotty has limitations when it comes to intersections of singleton types.

However, this strangely raises a warning:

match may not be exhaustive.
It would fail on pattern case: TUnit(), TFun(_, _)

Maybe @liufengyun can tell us why.

---

Going back to the type-parameter version: In principle, you should be able to write:

def default[T](ty: Ty[T]): T = ty match {
  case TUnit => ()
  case TFun(dom, cod): TFun[a, b] => { (x: a) => default(cod) }
}

but it does not work:

Found:    a => b
Required: T

Maybe @abgruszecki has an idea why.

[liufengyun]

However, this strangely raises a warning:

match may not be exhaustive.
It would fail on pattern case: TUnit(), TFun(_, _)

Maybe @liufengyun can tell us why.

The reason is that the exhaustivity check always widens the singleton type of selector first -- after widening the subtyping does not hold any more.

[LPTK]

@liufengyun I seem to remember that this used to be different, wasn't it? It would be nice if there was at least a special-case to allow refining what is matched to subtype the singleton type of the scrutinee, otherwise we lose too much information in type-heavy programming patterns.

[liufengyun]

@liufengyun I seem to remember that this used to be different, wasn't it? It would be nice if there was at least a special-case to allow refining what is matched to subtype the singleton type of the scrutinee, otherwise we lose too much information in type-heavy programming patterns.

I think it's possible to do better here. I'll give it a try.

[liufengyun]

@LPTK I proposed a tentative solution in #12549 -- however, the scrutinee has to be explicitly annotated:

sealed trait Ty {
  type T
}

class TUnit() extends Ty {
  type T = Unit
}

case object TUnit extends TUnit()

final case class TFun(dom: Ty, cod: Ty) extends Ty {
  type T = dom.T => cod.T
}

def default(ty: Ty): ty.T = (ty: ty.type & Ty) match {
  case a: (ty.type & TUnit) => (): a.T
  case a: (ty.type & TFun) =>
    val f = { (x: a.dom.T) => default(a.cod) }
    f: a.T
}

[LPTK]

@liufengyun Cool, thanks for taking the time to look into this!