Do not instantiate GadtMap TypeVars

Instead, record semi-instantiations in the constraint. Otherwise,
since the TypeVars live long enough, the _second_ case of a nested
pattern match would see bounds recorded by the _first_ one.

Author: Aleksander Boruch-Gruszecki

compiler/src/dotty/tools/dotc/core/Contexts.scala

@@ -777,7 +777,7 @@ object Contexts {
     override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = inCtx(ctx) {
       @annotation.tailrec def stripInst(tp: Type): Type = tp match {
         case tv: TypeVar =>
-          val inst = tv.inst orElse instType(tv)
+          val inst = instType(tv)
           if (inst.exists) stripInst(inst) else tv
         case _ => tp
       }
@@ -821,12 +821,11 @@ object Contexts {
             else if (isUpper) addLess(symTvar.origin, boundTvar.origin)
             else addLess(boundTvar.origin, symTvar.origin)
           case bound =>
-            if (cautiousSubtype(symTvar, bound, isSubtype = !isUpper)) { instantiate(symTvar, bound); true }
+            if (cautiousSubtype(symTvar, bound, isSubtype = !isUpper)) { unify(symTvar, bound); true }
             else if (isUpper) addUpperBound(symTvar.origin, bound)
             else addLowerBound(symTvar.origin, bound)
         }
 
-        vacuum()
         res
       }
 
@@ -835,24 +834,9 @@ object Contexts {
         case _ => false
       }
 
-      def instantiate(tv: TypeVar, tp: Type): Unit = {
-        // instantiating one TypeVar to another makes us actually lose information
-        // that is, we need to know that both TypeVars are equal to another
-        //   *and* be able to record further bounds on either one
-        if (tp.isInstanceOf[TypeVar]) return
-        val externalizedTp = (new TypeVarRemovingMap)(tp)
-        gadts.println(i"instantiating $tv to $externalizedTp    ( $tp )")
-        tv.inst = externalizedTp
-        constraint = constraint.replace(tv.origin, externalizedTp)
-      }
-
-      def vacuum(): Unit = {
-        constraint.foreachTypeVar { tv =>
-          if (!tv.inst.exists) {
-            val inst = instType(tv)
-            if (inst.exists) instantiate(tv, inst)
-          }
-        }
+      def unify(tv: TypeVar, tp: Type): Unit = {
+        gadts.println(i"manually unifying $tv with $tp")
+        constraint = constraint.updateEntry(tv.origin, tp)
       }
 
       val tvarBound = (new TypeVarInsertingMap)(bound)
@@ -877,8 +861,7 @@ object Contexts {
       mapping(sym) match {
         case null => null
         case tv =>
-          val tb =
-            if (tv.inst.exists) TypeAlias(tv.inst) else constraint.fullBounds(tv.origin)
+          val tb = constraint.fullBounds(tv.origin)
           val res = (new TypeVarRemovingMap)(tb).asInstanceOf[TypeBounds]
           // gadts.println(i"gadt bounds $sym: $res\t( $tv: $tb )")
           res

tests/gadt/GadtStlc.scala

@@ -0,0 +1,127 @@
+object GadtStlc {
+  // creates type-level "strings" like M[M[M[W]]]
+  object W
+  type W = W.type
+  class M[A]
+
+
+  // variable with name A
+  // Var[W]
+  // Var[M[W]]
+  sealed trait Var[A]
+  object VarW extends Var[W]
+  case class VarM[A] extends Var[M[A]]
+
+  // \s.e
+  sealed trait Abs[S, E]
+  case class AbsC[S, E](v: Var[S], b: E) extends Abs[Var[S], E]
+
+  // e1 e2
+  case class App[E1, E2](e1: E1, e2: E2)
+
+  // T1 -> T2
+  case class TyFun[T1, T2](t1: T1, t2: T2)
+
+  // arbitrary base literal
+  case object Lit
+  type Lit = Lit.type
+
+  // arbitrary base type
+  case object TyBase
+  type TyBase = TyBase.type
+
+  // IN[G, (X, TY)] === evidence that binding (X, TY) is in environment G
+  // x: ty \in G
+  sealed trait IN[G, P]
+  case class INOne[G, X, TY]() extends IN[(G, (X,TY)), (X, TY)]
+  // this is wrong - we need evidence that A does not contain a binding for X
+  case class INShift[G0, A, X, TY](in: IN[G0, (X, TY)]) extends IN[(G0, A), (X, TY)]
+
+  // DER[G, E, TY] === evidence that G |- E : TY
+  sealed trait DER[G, E, TY]
+  case class DVar[G, G0, X, TY](
+    in: IN[(G, G0), (Var[X], TY)]
+  ) extends DER[(G, G0), Var[X], TY]
+
+  case class DApp[G, E1, E2, TY1, TY2](
+    d1: DER[G, E1, TyFun[TY1, TY2]],
+    d2: DER[G, E2, TY1]
+  ) extends DER[G, App[E1, E2], TY2]
+
+  case class DAbs[G, X, E, TY1, TY2](
+    d1: DER[(G, (Var[X], TY1)), E, TY2]
+  ) extends DER[G, Abs[Var[X], E], TyFun[TY1, TY2]]
+
+  case class DLit[G]() extends DER[G, Lit, TyBase]
+
+  // forall G, a. G |- \x.x : a -> a
+  def test1[G, TY]: DER[G, Abs[Var[W], Var[W]], TyFun[TY, TY]] =
+    DAbs(DVar(INOne()))
+
+  // forall G. G |- \x.x : Lit -> Lit
+  def test2[G]: DER[G,  App[Abs[Var[W], Var[W]], Lit],  TyBase] =
+    DApp(DAbs(DVar(INOne())), DLit())
+
+  // forall G, c. G |- \x.\y. x y : (c -> c) -> c -> c
+  def test3[G, TY]: DER[G,
+    Abs[Var[W],
+      Abs[Var[M[W]],
+        App[Var[W], Var[M[W]]]
+      ]
+    ],
+    TyFun[TyFun[TY, TY], TyFun[TY, TY]]
+  ] = DAbs(DAbs(DApp(DVar(INShift(INOne())), DVar(INOne()))))
+
+
+  // evidence that E is a value
+  sealed trait ISVAL[E]
+  case class ISVAL_Abs[X, E]()  extends ISVAL[Abs[Var[X], E]]
+  case object ISVAL_Lit extends ISVAL[Lit]
+
+  // evidence that E1 reduces to E2
+  sealed trait REDUDER[E1, E2]
+  case class EApp1[E1a, E1b, E2](
+    ed: REDUDER[E1a, E1b]
+  ) extends REDUDER[App[E1a, E2], App[E1b, E2]]
+
+  case class EApp2[V1, E2a, E2b](
+    isval: ISVAL[V1],
+    ed: REDUDER[E2a, E2b]
+  ) extends REDUDER[App[V1, E2a], App[V1, E2b]]
+
+  case class EAppAbs[X, E, V2, R](
+    isval: ISVAL[V2]
+    // cheating - subst is hard
+    // , subst: SUBST[E, X, V2, R]
+  ) extends REDUDER[App[Abs[Var[X], E], V2], R]
+
+  // evidence that V is a lambda
+  sealed trait ISLAMBDA[V]
+  case class ISLAMBDAC[X, E]() extends ISLAMBDA[Abs[Var[X], E]]
+
+  // evidence that E reduces
+  type REDUCES[E] = REDUDER[E, _]
+
+  def followsIsLambda[G, V, TY1, TY2](
+    isval: ISVAL[V],
+    der: DER[G, V, TyFun[TY1, TY2]]
+  ): ISLAMBDA[V] = (isval, der) match {
+    case (_: ISVAL_Abs[x, e], _) => ISLAMBDAC[x, e]()
+  }
+
+  // \empty |- E : TY ==> E is a value /\ E reduces to some E1
+  def progress[E, TY](der: DER[Unit, E, TY]): Either[ISVAL[E], REDUCES[E]] =
+    der match {
+      case _: DAbs[g, a, e, ty1, ty2] => Left(ISVAL_Abs[a, e]())
+      case DLit() => Left(ISVAL_Lit)
+      case dapp: DApp[Unit, a, b, ty1, ty2] => progress(dapp.d1) match {
+        case Right(r1) => Right(EApp1[E2 = b](r1))
+        case Left(isv1) => progress(dapp.d2) match {
+          case Right(r2) => Right(EApp2(isv1, r2))
+          case Left(isv2) => followsIsLambda(isv1, dapp.d1) match {
+            case _: ISLAMBDAC[x, e] => Right(EAppAbs[x, e, b, _](isv2))
+          }
+        }
+      }
+    }
+}

tests/gadt/TypeSafeLambda.scala

@@ -0,0 +1,109 @@
+object TypeSafeLambda {
+
+  trait Category[Arr[_, _]] {
+    def id[A]: Arr[A, A]
+    def comp[A, B, C](ab: Arr[A, B], bc: Arr[B, C]): Arr[A, C]
+  }
+
+  trait Terminal[Term, Arr[_, _]] extends Category[Arr] {
+    def terminal[A]: Arr[A, Term]
+  }
+
+  trait ProductCategory[Prod[_, _], Arr[_, _]] extends Category[Arr] {
+    def first[A, B]: Arr[Prod[A, B], A]
+    def second[A, B]: Arr[Prod[A, B], B]
+    def pair[A, B, C](ab: Arr[A, B], ac: Arr[A, C]): Arr[A, Prod[B, C]]
+  }
+
+  trait Exponential[Exp[_, _], Prod[_, _], Arr[_, _]]
+    extends ProductCategory[Prod, Arr] {
+    def eval[A, B]: Arr[Prod[Exp[A, B], A], B]
+    def curry[A, B, C](a: Arr[Prod[C, A], B]): Arr[C, Exp[A, B]]
+  }
+
+  trait CartesianClosed[Term, Exp[_, _], Prod[_, _], Arr[_, _]]
+    extends Exponential[Exp, Prod, Arr] with Terminal[Term, Arr]
+
+  sealed trait V[Prod[_, _], Env, R]
+  case class Zero[Prod[_, _], Env, R]() extends V[Prod, Prod[Env, R], R]
+  case class Succ[Prod[_, _], Env, R, X](
+    v: V[Prod, Env, R]
+  ) extends V[Prod, Prod[Env, X], R]
+
+  sealed trait Lambda[Terminal, Exp[_, _], Prod[_, _], Env, R]
+
+  case class LUnit[Terminal, Exp[_, _], Prod[_, _], Env]()
+    extends Lambda[Terminal, Exp, Prod, Env, Terminal]
+
+  case class Var[Terminal, Exp[_, _], Prod[_, _], Env, R](
+    v: V[Prod, Env, R]
+  ) extends Lambda[Terminal, Exp, Prod, Env, R]
+
+  case class Lam[Terminal, Exp[_, _], Prod[_, _], Env, R, A](
+    lam: Lambda[Terminal, Exp, Prod, Prod[Env, A], R]
+  ) extends Lambda[Terminal, Exp, Prod, Env, Exp[A, R]]
+
+  case class App[Terminal, Exp[_, _], Prod[_, _], Env, R, R_](
+    f: Lambda[Terminal, Exp, Prod, Env, Exp[R, R_]],
+    a: Lambda[Terminal, Exp, Prod, Env, R]
+  ) extends Lambda[Terminal, Exp, Prod, Env, R_]
+
+  def interp[Term, Exp[_, _], Prod[_, _], Arr[_, _], S, T](
+    c: CartesianClosed[Term, Exp, Prod, Arr],
+    exp: Lambda[Term, Exp, Prod, S, T]
+  ): Arr[S, T] = exp match {
+    case LUnit() => c.terminal
+    case v: Var[t, e, var_p, env, r] => v.v match {
+      case _: Zero[z_p, z_env, z_r] => c.second[z_env, z_r]
+      case s: Succ[s_prod, s_env, s_r, x] =>
+        c.comp[A = s_prod[s_env, x], C = s_r](
+          c.first,
+          interp(c, Var[Term, Exp, Prod, s_env, s_r](s.v))
+        )
+    }
+    case Lam(lam) => c.curry(interp(c, lam))
+    case app: App[t, e, p, env, r, r_] =>
+      c.comp(
+        c.pair(
+          interp(c, app.f),
+          interp(c, app.a)),
+        c.eval[r, r_]
+      )
+  }
+
+  object example {
+    type Term = Unit
+    type Prod[A, B] = (A, B)
+    type Exp[A, B] = A => B
+    type Arr[A, B] = A => B
+
+    val c = new CartesianClosed[Term, Exp, Prod, Arr] {
+      def id[A]: A => A = a => a
+      def comp[A, B, C](f: A => B, g: B => C): A => C = f andThen g
+
+      def terminal[A]: A => Unit = a => ()
+
+      def first[A, B]: ((A, B)) => A = { case (a, _) => a }
+      def second[A, B]: ((A, B)) => B = { case (_, b) => b }
+      def pair[A, B, C](f: A => B, g: A => C): A => (B, C) =
+        a => (f(a), g(a))
+
+      def eval[A, B]: ((A => B, A)) => B = { case (f, a) => f(a) }
+      def curry[A, B, C](f: ((C, A)) => B): C => A => B =
+        c => a => f((c, a))
+    }
+
+    type Env = Unit Prod Int Prod (Int => String)
+    val exp = App[Term, Exp, Prod, Env, Int, String](
+      // args to Var are RHS "indices" into Env
+      Var(Zero()),
+      Var(Succ(Zero()))
+    )
+
+    val interped: (Env) => String =
+      interp[Term, Exp, Prod, Arr, Env, String] (c, exp)
+
+    interped((((), 1), { i: Int => i.toString })) : String // "1"
+  }
+
+}

tests/gadt/complexEQ.scala

@@ -0,0 +1,24 @@
+object complexEQ {
+  sealed trait EQ[A, B]
+  final case class Refl[A]() extends EQ[A, A]
+
+  def m[A, B, C, D](e1: EQ[A, (B, C)], e2: EQ[A, (C, D)], d: D): A =
+    e1 match {
+      case Refl() => e2 match {
+        case Refl() => 
+          val r1: (B, B) = (d, d)
+          val r2: (C, C) = r1
+          val r3: (D, D) = r1
+          r1
+      }
+    }
+
+  def m2[Z, A, B, C, D](e0: EQ[Z, A], e1: EQ[A, (B, C)], e2: EQ[Z, (C, D)], d: D): Z =
+    (e0, e1, e2) match {
+      case (Refl(), Refl(), Refl()) =>
+          val r1: (B, B) = (d, d)
+          val r2: (C, C) = r1
+          val r3: (D, D) = r1
+          r1
+    }
+}