A simple way to check exhaustivity of GADTs

[liufengyun]

This is an alternative to #3454.

The idea (implemented in OCaml, briefly mentioned in the space paper) is simple: just exclude counterexamples that are not satisfiable.

The PR passed all GADT tests, and it should have better performance by only enabling the checking for invariant GADTs. It doesn't do any changes to the core algorithm.

Many thanks to @AleksanderBG for his work on checking GADTs and pushing the limits of exhaustivity check for Scala.

cc/ @AleksanderBG: we're still interested in your algorithm , it would be nice to have detailed evaluation of the two approaches when #3454 is done.

[OlivierBlanvillain]

This block looks like a tvarMap.getOrElseUpdate(tref.symbol, newTypeVar(tref.underlying.bounds))

[OlivierBlanvillain]

I feel that we should use something other than ??? for unreachable cases, to me ??? really has the semantic of a TODO: "implementation is missing here, to be added later"

Maybe something like this? Not sure where should that definition could go...

def impossible: Nothing = throw new AssertionError("This expression shouldn't be reachable.")

[allanrenucci]

assert(false, "Unreachable code")?

[OlivierBlanvillain]

@allanrenucci assert returns Unit

[allanrenucci]

My bad...

[OlivierBlanvillain]

I'm not sure what you mean by checkGADT the implementation looks like it's computing isDeeplyInvariant

[liufengyun]

Yes, something like shouldCheckGADT with a comment is more friendly.

[abgruszecki]

@liufengyun Is it possible to use ctx.gadt to further restrict initial tvar bounds? There are cases like the following one:

object O {
  sealed trait NumExpr[T]
  case class IntLit(v: Int) extends NumExpr[Int]
  case class DoubleLit(v: Double) extends NumExpr[Double]
  case class Mul[T](n1: NumExpr[T], n2: NumExpr[T]) extends NumExpr[T]

  def simplify[T](e: NumExpr[T]): NumExpr[T] = e match {
    case Mul(IntLit(i), ie) => ie match {
      case IntLit(0) => IntLit(0)
      case IntLit(1) => IntLit(i)
      case IntLit(_) | Mul(_, _) => e
    }
    case _ => e
  }
}

where the typechecker already knows that T ~ Int from the outer match. If I understand correctly that these bounds are recorded in ctx.gadt, using it would improve the warnings while barely requiring any adjustments.

[liufengyun]

@AleksanderBG Good observation. The ctx.gadt information is only available during type checking (phase Frontend), in pattern matcher it's too late to get that information.

Edited: Also, I think it's up to the typer to give ie the type IntLit.