GADTs might need a different implementation scheme

[odersky]

Working with opaque types, which are based on our existing GADT machinery, I see more and more problems with our existing approach:

This one is known:

• GADT maps are different from constraints, so no unfication is possible between variables defined in one and variables defined in the other.

But these have not been voiced before:

• Knowledge about GADT bounds has spread far into the core algorithms of the compiler. It's not just subtyping, by now we consult the GADT bounds also

  • when computing members of a type
  • when computing base types
  • when following the underlying type of a type proxy

  It's not clear at all whether this is enough, or whether we need to consult GADT maps in more places.

• GADT maps pose enormous problems for caching. Every update to a GADT map invalidates all caches that contain values whose computation relied on the previous value (or relied on the fact that there was no GADT entry yet). But there is no way to trace these caches. The alternative of not caching any info that could be affected by GADT bounds is unappealing as well, because it looks very hard to figure out what might be affected later on.

So far, we have not seen much fail empirically, because GADTs were not really fully implemented so very little code relied on them. But if we want that to change, we have to take these problems seriously.

An alternative approach

Here's a different implementation scheme which avoids the cited problems (whether it will create new ones remains to be seen).

1. When type checking a case in a match, determine all type parameters with term owners that are referenced from the widened scrutinee type. Call these the GADT parameters. (This step is the same as in the current scheme)

2. Determine the support set of the GADT parameters. This is the smallest set S of term-owned symbols such that:

• every GADT parameter is in S.
• if a symbol x is owned by a term and has a type info T that refers to a symbol in S, then x is in S (for both term and type symbols x).

3. Define a map M over the support set as follows:

• Every GADT parameter in S is mapped to a type variable whose TypeParamRef origin has the bounds of the original symbol mapped recursively by M.

• Every other symbol s in S is mapped to a fresh symbol of the same kind as s, whose info is the original info of s mapped recursively by M.

  Contexts have a new field gadtMap that contains the current map.

4. A match case gets typechecked in a new context, where a new instance of M as computed in the last step is added to the gadtMap field and all TypeVars in M s image are added to the constraint.

5. When typechecking an identifier in typedIdent, map the computed type (always a TermRef or TypeRef) using the context's GADT map.

   [Aside: The mapping would be avoided if we could replace old scopes with new scopes in the context. But this means duplicating potentially a stack of context objects, because GADT parameters might be bound in outer contexts. This looks tricky.]

6. Typecheck pattern against scrutinee as usual. This might further constrain images of GADT parameters in the constraint. After that is done,

• instantiate all GADT TypeVars in M to fresh abstract type symbols, with the bounds copied over and mapped recursively.
• instantiate all pattern bound TypeVars as usual.

7. Typecheck the guard and RHS of the case as usual. At the end, check that the type of RHS
   conforms to the expected type of the match after mapping the latter with M. If the type of the RHS does not conform to expected type without applying M, insert a cast.

[odersky]

One consequence of the new scheme is that it is not applicable to opaque types, since it relies on local copies of local (i.e. term-owned) symbols. So #4028 would be invalidated and we have to go back to square one and develop a different scheme, and potentially a different spec for opaque types.

[odersky]

The new scheme is similar to the old in that GADTness does not propagate: The types referenced in scrutinee are the only ones that can be restricted further. We could widen that in two directions:

• other abstract types in the support set can also be constrained, or/and
• type parameters referred to in the bounds of a GADT parameter can also be constrained.

For the moment, we are most conservative, which is appropriate because the problem already looks hard enough as it is. With convincing use cases we might be forced to generalize.

[odersky]

The root of the problem is: what do GADT constraints mean? Assume the following simple GADT program:

trait C[X](elem: X)
class CInt(elem: Int) extends C(elem)
class CBoolean(elem: Boolean) extends C(elem)

def f[T](x: C[T]): T = x match {
  case CInt(y) => y
  case CBoolean(y) => y
}

This program needs GADT reasoning for typechecking. For instance, in the first case of f,
the right hand side is of type Int and the expected type is T. This typechecks because
we can derive the GADT constraints T >: Int and T <: Int by comparing the scrutinee type and the pattern type.

Now, the question: Knowing that T <: Int, what additional properties do values of T get from the type Int? For instance, does it mean that the members of T are also the members of Int?
In this case, we could modify the first case as follows:

  case CInt(y) => x.elem * y

The justification why this should work is as follows:

We have: x.elem: T. With T <: Int, we also have x.elem: Int. Therefore, a * operation is defined on x.elem.

Note that this reasoning uses the subsumption rule of subtyping. Subsumption is part of DOT but it's actually not part of the Scala spec, nor does the compiler implement it. So we conclude that the justification via subsumption gives some intuition but no hard guidance what to do. If we want to implement some approximation to subsumption we have to do it explicitly. It would mean lots of special purpose rules in the spec and lots of special cases in the compiler.

In light of the problems outlined in this issue it seems best to leave things where they are now: GADT constraints generate new subtyping relationships but nothing else. This solves points (2) and (3) outlined in the issue: scope creep and cache invalidation. It does mean that some code that intuitively "should work" doesn't. For instance,

  case CInt(y) => x.elem * y

would give an error "* is not a member of x.elem". You have to upcast explicitly to fix this:

case CInt(y) => (x.elem: Int) * y

Open question: Can we design hints that suggest such upcasts?

[milessabin]

Note that this reasoning uses the subsumption rule of subtyping. Subsumption is part of DOT but it's actually not part of the Scala spec, nor does the compiler implement it.

Are there any known counterexamples to subsumption in Scala 2/3?

[odersky]

Are there any known counterexamples to subsumption in Scala 2/3?

For instance:

trait A
trait B
def ab: A & B
def f(x: A) = 1
def f(x: B) = 2
f(ab)

With subsumption, this could return either 1 or 2. Without, it's a type error. The example shows that adding full subsumption is not even possible in full Scala since it would make type checking non-deterministic.

[milessabin]

OK, even in the absence of subsumption, couldn't we have an "adapt to subtype supertype" in the elaborator? ie. treat subsumption as a glorified view?

[liufengyun]

For instance:

trait A
trait B
def ab: A & B
def f(x: A) = 1
def f(x: B) = 2
f(ab)

With subsumption, this could return either 1 or 2.

It seems to me this example is more about an issue with algorithmic subtyping and overloading resolution. I think current Dotty (with algorithmic subtyping) is correct to produce an error here for ambiguities in overloading resolution.

It is mentioned in the slides of FoS (search for T-Invk) that compilers usually implement algorithmic-style (sub-)type checking rules, which has the subsumption rule "built-in". So the problem is whether there can be algorithmic (sub)type checking for Scala.

Theoretically, it is hopeless, as even algorithmic subtyping for F<: is undecidable, and algorithmic subtyping for DOT is known as undecidable as well.

[odersky]

OK, even in the absence of subsumption, couldn't we have an "adapt to subtype supertype" in the elaborator? ie. treat subsumption as a glorified view?

We could try but I find it unappealing. Views don't propose, so I fear this will be fragile and it could also be very expensive. Adding hints to error messages seems like an easier alternative.

[milessabin]

it could also be very expensive.

Is it really so bad? If type checking fails we retry with an ascription inserted ... this is only going to be an issue in opaque contexts and the RHSs of GADT pattern matches.

[odersky]

To give a concrete example: If we do the widening as a (compiler-generated) implicit conversion, then we could support members of the widened type, but we would fail to infer selections added by decorators or extension methods. Or we compose both and risk a combinatorial explosion. Either way, it's unappealing. I believe it's actually better to say "these are subtypes, i.e. you can coerce one to the other by a simple type ascription, but that's it".

[milessabin]

I'm not sure I see that.

If we're typing the body of the companion of an opaque type, or the RHS of a GADT pattern match then we know both the abstract type and the widened type. If type checking a selection fails for a term of the abstract type in one of those scenarios then we can insert the type ascription you're suggesting that users do by hand and then retypecheck. Having inserted the acription we'll pick up both direct members and members accessible via a view using the normal mechanisms.

I don't see where the risk of a combinatorial explosion comes in, other than in artificial cases which I don't think would being sufficiently likely programming patterns to be worrisome.

(The unlikely cases I have in mind being: opaque types nested in the companion of an opaque type; GADT pattern matches nested in the RHS of GADT pattern matches; and combinations of the two. In the unlikely event of someone doing that and it causing a compile time performance issue, manually inserting the ascription would fix it).

[Blaisorblade]

@milessabin The two biggest violations of subsumptions are Nothing (which has no methods but should have all, argh) and type members (if x.T >: S <: U then in DOT S <: U but this isn't algorithmic — and in fact, for Scala this generalizes to p.T).

A full fix for the latter requires checking all type members of everything in scope, which is clearly too expensive — (expert) users know an assertion is required instead, and this could be specified as required. This has precedents in dependent type theories — if you have a proof of equality in scope, you usually need to apply it explicitly (e.g. in Coq/Agda/Idris).

However, if we encoded opaque types as type members (as in the original blog post, tho we don't), opaque types would reduce to type aliases T = U in the body of the companion, for which subsumption already works. But it's not clear how expensive it'd be to produce that encoding.

[milessabin]

A full fix for the latter requires checking all type members of everything in scope

I don't see why that's the case in the scenarios in question (opaque type companion bodies and GADT match RHSs) ... can you give me an example?