WIP: Constraint-based GADT reasoning

[abgruszecki]

This is the current state of the "smart" GADT Map, written by re-using ConstraintHandling. An example of code that did not compile previously and now does:

object injectivity {
  sealed trait EQ[A, B]
  final case class Refl[A](u: Unit) extends EQ[A, A]

  def conform[A, B, C, D](a: A, b: B, eq: EQ[(A, B), (C, D)]): C =
    eq match {
      case Refl(()) => a
    }
}

All old tests still pass. Test suite as a whole fails, since no new code compiles with no-deep-subtypes flag. The implementation is a bit hacky as well.

Since all the new examples fail deep-subtypes, it's likely this approach will ultimately not work. We will probably need after all to keep only a single Constraint and allow freezing only a part of it.

[abgruszecki]

So, turns out that remembering to substitute TypeParams with TypeVars in the bounds is quite important for correctness.
After that, all tests pass with -Yno-deep-subtypes flag. The status of current GADT issues is:

• fixed Problem with type checking GADTs #3666 - now compiles with -Yno-deep-subtypes
• "fixed" GADT typechecking requires unification analogue (via ConstraintHandling) #4176 (works correctly after accounting for GADT patmat doesn't narrow class type parameters #4323)
• fixed "imprecise bounds" of GADT bounds are not precise enough #4075
• not fixed: type inference in GADT bounds are not precise enough #4075 (this time the type inferred is One[a], where a is an inner type param)
• fixed GADT pattern matching produces conformance constraints instead of equality (HKTs) #5068 (albeit with an unprincipled makeshift fix)
• not fixed: GADT example fails to typecheck because it requires injectivity of type constructors #4471

Continuing to poke at #4471, it produces the most complex constraints so far. Some additional changes are required to make the example compile, but it still fails to infer one final constraint necessary to typecheck the code.

[abgruszecki]

Correction: #4471 now appears to be fixed. As a side effect, type inference in #4075 is now fixed too.

[abgruszecki]

test performance please

[dottybot]

performance test scheduled: 5 job(s) in queue, 1 running.

[dottybot]

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/5258/ to see the changes.

Benchmarks is based on merging with master (45eb6aa)

[abgruszecki]

test performance please

[dottybot]

performance test scheduled: 1 job(s) in queue, 0 running.

[dottybot]

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/5258/ to see the changes.

Benchmarks is based on merging with master (c0941f3)

[abgruszecki]

test performance please: 777a8f8 8f2e6e1

[dottybot]

performance test scheduled for 777a8f8 8f2e6e1: 1 job(s) in queue, 0 running.

[dottybot]

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/5258/ to see the changes.

Benchmarks is based on merging with master (180c8df)

[Blaisorblade]

Answering on #5300 (comment), as a summary of what was discussed today.

Since opaque types behave like abstract types, the code below requires case StringExpr() => in the match to be exhaustive, since the principle is that Pos = Int must be hidden from code outside Pos's companion, such as the pattern match in question.

opaque type Pos = Int
object Pos {
  def mkPos(i: Int): Pos = {
    require(i > 0)
    i
  }
  def coerce[F[_]](fa: F[Int]): F[Pos] = fa
}

sealed trait Expr[T]
final case class PosExpr(p: Pos) extends Expr[Pos]
final case class IntExpr(i: Int) extends Expr[Int]
final case class StringExpr() extends Expr[String]

def eval(e: Expr[Pos]): Pos = e match {
  case PosExpr(p) => p
  case IntExpr(_) => Pos.mkPos(1)
  case StringExpr() => Pos.mkPos(2)
}

For abstract types that's already implemented, after a discussion in #3645 where people initially thought roles would be necessary. The solution to that problem appears noncontroversial. What's more, the original question was already on the (manual) encoding of opaque types!

[Blaisorblade]

Also for the record:

• Opaque types - selftype encoding #5300 (comment) suggests maybe moving ElimOpaque after pattern matching. @AleksanderBG you can create a separate issue if you prefer?

[abgruszecki]

@Blaisorblade I think this is not the PR you want 😄

EDIT - ok, I think I see why you commented here. I think it would be best to limit this PR to discussion about adding unification to GADT solving, not to GADTs in general. I'll open a separate issue for exhaustivity warnings, and a PR to add the test.

[abgruszecki]

test performance please: e73d2e8 b05630b 20dc62d

[dottybot]

performance test scheduled for e73d2e8 b05630b 20dc62d: 1 job(s) in queue, 0 running.

[abgruszecki]

Note for anyone curious: the performance comparison is between:

1. creating "fake" TypeVars for each symbol and substituting them when adding and retrieving bounds (simplest)
2. modifying Constraint to allow pseudo-TypeVars which have a TypeRef as .underlying (as opposed to TypeParamRef) (requires horrible duo of mutually recursive f-bounded types, but no substitutions)
3. adding ad-hoc cache to 1.

I had to revert 756cd0a - due to some black magic this breaks tests when combined with weak conformance changes, but not on its own. Will need to investigate further.

[dottybot]

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/5258/ to see the changes.

Benchmarks is based on merging with master (2d23cba)

[abgruszecki]

@odersky @smarter FWIW I think this is best reviewed as a whole (Github shows commits in a non-existant order anyway due to rebases). One commit which is worth seeing alone is f008bbc - I'm not entirely certain this is the best fix and I'll revert it if you think it's bad.

The code for HKTs remains unsound (see 3084bf9 ), but this will be tracked as a separate issue. That's also the reason for keeping 756cd0a reverted.

[abgruszecki]

test performance please

[dottybot]

performance test scheduled: 1 job(s) in queue, 1 running.

[dottybot]

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/5258/ to see the changes.

Benchmarks is based on merging with master (052c3b1)

[abgruszecki]

Working on #5405 made me consider why SmartGADTMap state isn't part of TyperState. Implicit search already forks TyperState, manipulates it and restores it, so why do we need to re-do that logic for GADT constraint state as well? While at first glance this seems like a good idea, after some consideration I have my doubts:

1. GADT constraints don't really work like other constraints: they are inferred during a few subtype checks and then frozen. The places that currently call .set(New|Explore)TyperState don't really want to unlock them.
2. The places that want to add GADT constraints would need to call .setNewTyperState, which would then need committing. This seems wasteful from performance perspective.
3. Disabling GADT bound caching whenever a bound addition is in progress gets trickier if the state is separate from the class performing the check.

Overall, we might still want to do it, but for the time being it seems best to me to just merge this PR as-is, work with it for a bit and only consider unifying GADT & Typer state afterwards.

[abgruszecki]

Closing in favour of #5611.