Dotty should reason about singleton types gaining new type information

[LPTK]

Reopening https://github.com/lampepfl/dotty/issues/7885 as a feature request, as suggested by @odersky.

---

I think this is a known problem, but I did not find an issue currently documenting it.

Scala has these two important features:

• path-dependent types

• flow-based type refinement

The latter comes up in pattern matching (especially in the context of GADTs) and in boolean-based flow typing for explicit nulls.

The problem is that these two features do not play well with each other. Sometimes, we want flow-based refinement of a singleton's type in which path-dependent types may be rooted, and there is currently no way of achieving that.

---

Here is a simple and realistic example: I have a language definition interface called Base and a sub-language RunnableBase with more capabilities:

abstract class Base with
  type Rep
  type Value
  // other methods...

abstract class RunnableBase extends Base with
  def run(r: Rep): Value

We should be able to retain path-dependent types and flow-refined types, so that the code below would type-check (it currently does not):

def tryRun(b: Base)(r: b.Rep): Option[b.Value] =
  b match
  case c: (RunnableBase & b.type) =>
    Some(c.run(r)) // Found: b.Rep(r); Required: c.Rep
  case _ => None

https://scastie.scala-lang.org/SozHLp3cSaODeLK1p9ohug

There are two problems here:

• First, we have to use pattern c: (RunnableBase & b.type) instead of just c: RunnableBase (this is fine, just a little clunky);

• Dotty does not reason that since value c matched value b, then c.Rep is the same as b.Rep; or alternatively, that b.type should be refined to be a subtype of RunnableBase in the corresponding pattern matching branch.

---

The problem does come up in the wild: Here I was working around the problem using a subtyping evidence between singleton types and a higher-kinded-type subst function (but the code was broken in 2.12.8). The underlying issue is that there is poor reasoning about refined singleton types.

Another place where this would be useful: https://github.com/lampepfl/dotty/issues/7554#issuecomment-554347712, where @AleksanderBG commented:

GADT patmat cannot currently constrain singleton types. A mechanism for constraining singleton types is already implemented for explicit null types in their PR, so after that gets merged, we could look into reusing it for GADTs.

However, by now we know (see: https://github.com/lampepfl/dotty/issues/7882#issuecomment-570046273) that the mechanism implemented for explicit nulls — which is to adapt variable references with a cast to the refined type — is insufficient because it loses the singletonness of the reference, and prevents it from being used in a path.

---

I think the best way to solve this issue would be to have a proper system for adding more information to singleton types, the same way more information is added to type variables in GADT pattern matching. Then, we'd need to:

• refine singleton types using this mechanism when values of singleton types are pattern-matched and tested for null-ness; and

• make sure to assign type c.type to a pattern variable b which matches a value of type c.type — this should not only work in the example above, but also in cases such as (_: Option[b.type]) match { case Some(c: T) => ... }.