GADT typechecking requires unification analogue (via ConstraintHandling)

[Blaisorblade]

In #4069 @smarter suggests GADT constraints might require unification:

We end up with GADT constraints foo >:> S and S >:> foo but we don't have a mechanism to unify GADT constraints, so we end up with a loop in subtyping checks. We could add a special case to handle simple unifications like this but it seems like to be completely general we really need to reuse all of ConstraintHandling to deal with GADT constraints too.

So here's an unification-based use of GADTs: length-indexed vectors, which indeed doesn't typecheck. I also initially hoped to use erased for TNatSum (which would maybe work in Agda), but that'd be a request for enhancement in fact (and not sure it's one we should grant).

I think this is still a relatively simple testcase, and I'm not sure it requires ConstraintHandling in the way @smarter meant, but I hope it is helpful. Before fixing this, I'd suggest a review the literature to find a comprehensive design (and I volunteer to take a look).
"Principal Type Inference for GADTs", from 2016, is a relatively recent reference (and pretty original) with a decent review of related work; I think "Complete and Decidable Type Inference for GADTs" and "OutsideIn(x) modular type inference with local assumptions" describe GHC's basic approach, while "GADTs Meet Their Match: Pattern-matching Warnings That Account for GADTs, Guards, and Laziness" describe GHC extensions for warnings.

object NatsVects {
  sealed trait TNat
  case class TZero() extends TNat
  case class TSucc[N <: TNat] extends TNat

  object TNatSum {
    sealed trait TSum[M, N, R]
    case class TSumZero[N]() extends TSum[TZero, N, N]
    case class TSumM[M <: TNat, N, R <: TNat](sum: TSum[M, N, R]) extends TSum[TSucc[M], N, TSucc[R]]
  }
  import TNatSum._

  implicit def tSumZero[N]: TSum[TZero, N, N] =
    TSumZero()
    //new TSum[TZero, N, N]() {}
  implicit def tSumM[M <: TNat, N, R <: TNat](implicit sum: TSum[M, N, R]): TSum[TSucc[M], N, TSucc[R]] =
    TSumM(sum)
    //new TSum[TSucc[M], N, TSucc[R]] {}

  sealed trait Vec[+T, N <: TNat]
  case object VNil extends Vec[Nothing, TZero] // fails but in refchecks
  case class VCons[T, N <: TNat](x: T, xs: Vec[T, N]) extends Vec[T, TSucc[N]]

  implicit class vecOps[T, M <: TNat]($this: Vec[T, M]) extends AnyVal {
    def append[N <: TNat, R <: TNat](that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] = {
      // tsum match {
      //   case _: TSumZero[N] => // Here N = R
      //     $this match {
      //       case VNil =>
      //         //that
      //         that.asInstanceOf[Vec[T, R]]
      //       case VCons(x, xs) =>
      //         ???
      //     }
      //   case TSumM(sum) =>
      //     ???
      // }
      $this match {
        case VNil => // M = TZero
          tsum match {
            case _: TSumZero[TZero] =>
              //that
              that.asInstanceOf[Vec[T, R]]
            case _: TSumM[_, _, _] => // Impossible, this forces M = TSucc[M1]
              ???
          }
        case vxs: VCons[T, m1] => // M = TSucc[m1], xs: Vec[T, m1]
          val x = vxs.x
          val xs = vxs.xs
        //case VCons(x, xs) => 
          tsum match {
            case _: TSumZero[TZero] => // impossible, since this forces M = TZero.
              ???
            // fails
            // case tsum1: TSumM[`m1`, n, r] => // M = TSucc[m1], R = TSucc[r]
            //   implicit val tsum2 = tsum1.sum
            //   val appended = xs append that
            //   VCons(x, appended) // Vec[T, TSucc[r]]
            //works
            case tsum1: TSumM[`m1`, N, r] => // M = TSucc[m1], R = TSucc[r]
              implicit val tsum2 = tsum1.sum
              // I should be able to return:
              //VCons(x, xs append that) // Vec[T, TSucc[r]] = Vec[T, R]

              val vxs1 = xs append that
              val vxs2 = VCons(x, vxs1)
              // vxs1
              // [error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/gadtVect.scala:65:14
              // [error] 65 |              vxs1
              // [error]    |              ^^^^
              // [error]    |    found:    NatsVects.Vec[T, r](vxs1)
              // [error]    |    required: NatsVects.Vec[T, R]
              // [error]    |
              // [error]    |    where:    r is a type in method append with bounds <: NatsVects.TNat
              // vxs2
              // [error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/gadtVect.scala:71:14
              // [error] 71 |              vxs2
              // [error]    |              ^^^^
              // [error]    |    found:    NatsVects.VCons[T, r](vxs2)
              // [error]    |    required: NatsVects.Vec[T, R]
              // [error]    |
              // [error]    |    where:    r is a type in method append with bounds <: NatsVects.TNat

              vxs2.asInstanceOf // sorry this works
          }
      }
    }
  }
}

[odersky]

See also test in #4069:

object i3666 {
  sealed trait Exp[T]
  case class Num(n: Int) extends Exp[Int]
  case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int]
  case class Var[T](name: String) extends Exp[T]
  case class Lambda[T, U](x: Var[T], e: Exp[U]) extends Exp[T => U]
  case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]

  abstract class Env { outer =>
    def apply[T](x: Var[T]): T

    def + [T](xe: (Var[T], T)) = new Env {
      def apply[T](x: Var[T]): T =
        if (x == xe._1) xe._2.asInstanceOf[T]
        else outer(x)
    }
  }

  object Env {
    val empty = new Env {
      def apply[T](x: Var[T]): T = ???
    }
  }

  object Test {

    val exp = App(Lambda(Var[Int]("x"), Plus(Var[Int]("x"), Num(1))), Var[Int]("2"))

    def eval[T](e: Exp[T])(env: Env): T = e match {
      case Num(n) => n
      case Plus(e1, e2) => eval(e1)(env) + eval(e2)(env)
      case v: Var[_] =>
        env(v)
      case Lambda(x: Var[s], e) => ((y: s) => eval(e)(env + (x -> y)))
      case App(f, e) => eval(f)(env)(eval(e)(env))
    }

    eval(exp)(Env.empty)
  }
}
// A HOAS well-typed interpreter
object i3666Hoas {
  sealed trait Exp[T]
  case class IntLit(n: Int) extends Exp[Int]
  case class BooleanLit(b: Boolean) extends Exp[Boolean]

  case class GenLit[T](t: T) extends Exp[T]
  case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int]
  case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T]
  case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]


  def eval[T](e: Exp[T]): T = e match {
    case IntLit(n) => n
    case BooleanLit(b) => b
    case GenLit(t) => t
    case Plus(e1, e2) => eval(e1) + eval(e2)
    case f: Fun[s, t]  =>
      (v: s) => eval(f.f(GenLit(v)))
    case App(f, e) => eval(f)(eval(e))
  }

  val exp = App(Fun[S = Int](x => Plus(x, IntLit(1))), IntLit(2))

  eval(exp)
}

[Blaisorblade]

While reviewing the literature and unification one should also consider #4471.

[abgruszecki]

Here's a version of the original file which compiles even on master:

object i4176 {
  sealed trait TNat
  case class TZero() extends TNat
  case class TSucc[N <: TNat] extends TNat

  object TNatSum {
    sealed trait TSum[M, N, R]
    case class TSumZero[N]() extends TSum[TZero, N, N]
    case class TSumM[M <: TNat, N, R <: TNat](sum: TSum[M, N, R]) extends TSum[TSucc[M], N, TSucc[R]]
  }
  import TNatSum._

  implicit def tSumZero[N]: TSum[TZero, N, N] =
    TSumZero()
  implicit def tSumM[M <: TNat, N, R <: TNat](implicit sum: TSum[M, N, R]): TSum[TSucc[M], N, TSucc[R]] =
    TSumM(sum)

  sealed trait Vec[T, N <: TNat]
  case object VNil extends Vec[Nothing, TZero] // fails but in refchecks
  case class VCons[T, N <: TNat](x: T, xs: Vec[T, N]) extends Vec[T, TSucc[N]]

  def append0[T, M <: TNat, N <: TNat, R <: TNat]($this: Vec[T, M], that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] =
    ($this, tsum) match {
      case (VNil, TSumZero()) => that
      case (VCons(x, xs), TSumM(sum)) => VCons(x, append0(xs, that)(sum))
    }

  def append[T, M <: TNat, N <: TNat, R <: TNat]($this: Vec[T, M], that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] =
      tsum match {
        case TSumZero() =>
          $this match { case VNil => that }
        case TSumM(sum) =>
          $this match { case VCons(x, xs) => VCons(x, append(xs, that)(sum)) }
      }

}

Original code wasn't compiling because class parameters aren't considered for GADT narrowing, which is already tracked in #5068.

The code does compile with multiple spurious warnings of this sort:

-- Warning: tests/gadt/i4176.scala:33:29 ---------------------------------------
33 |          $this match { case VCons(x, xs) => VCons(x, append(xs, that)(sum)) }
   |                             ^^^^^^^^^^^^
   |      the type test for i4176.VCons[T, M$1] cannot be checked at runtime

We may want to open a separate issue to track that.