Support for GADTs

shared/src/main/scala/mlscript/ConstraintSolver.scala

@@ -682,8 +682,8 @@ class ConstraintSolver extends NormalForms { self: Typer =>
       val originalVars = ty.getVars
 
       // * FIXME ctx.extrCache and ctx.extrCache2 should be indexed by the level of the extrusion!
-      // val res = extrude(ty, lowerLvl, pol, upperLvl)(ctx, ctx.extrCache, ctx.extrCache2, reason)
-      val res = extrude(ty, lowerLvl, pol, upperLvl)(ctx, MutMap.empty, MutSortMap.empty, reason)
+      // TODO somehow handle extrCache2
+      val res = extrude(ty, lowerLvl, pol, upperLvl)(ctx, MutSortMap.empty, reason)
 
       val newVars = res.getVars -- originalVars
       if (newVars.nonEmpty) trace(s"RECONSTRAINING TVs") {
@@ -1341,7 +1341,7 @@ class ConstraintSolver extends NormalForms { self: Typer =>
     * `upperLvl` tracks the lowest such current quantification level. */
   private final
   def extrude(ty: SimpleType, lowerLvl: Int, pol: Boolean, upperLvl: Level)
-        (implicit ctx: Ctx, cache: MutMap[TypeVarOrRigidVar->Bool, TypeVarOrRigidVar], cache2: MutSortMap[TraitTag, TraitTag], reason: Ls[Ls[ST]])
+        (implicit ctx: Ctx, cache2: MutSortMap[TraitTag, TraitTag], reason: Ls[Ls[ST]])
         : SimpleType =
   // (trace(s"EXTR[${printPol(S(pol))}] $ty || $lowerLvl .. $upperLvl  ${ty.level} ${ty.level <= lowerLvl}"){
     if (ty.level <= lowerLvl) ty else ty match {
@@ -1356,9 +1356,9 @@ class ConstraintSolver extends NormalForms { self: Typer =>
         ArrayType(ar.update(extrude(_, lowerLvl, !pol, upperLvl), extrude(_, lowerLvl, pol, upperLvl)))(t.prov)
       case w @ Without(b, ns) => Without(extrude(b, lowerLvl, pol, upperLvl), ns)(w.prov)
       case tv @ AssignedVariable(ty) =>
-        cache.getOrElse(tv -> true, {
+        ctx.extrCache.getOrElse(tv -> true, {
           val nv = freshVar(tv.prov, S(tv), tv.nameHint)(lowerLvl)
-          cache += tv -> true -> nv
+          ctx.extrCache.set(tv -> true, nv)
           val tyPos = extrude(ty, lowerLvl, true, upperLvl)
           val tyNeg = extrude(ty, lowerLvl, false, upperLvl)
           if (tyPos === tyNeg)
@@ -1372,24 +1372,24 @@ class ConstraintSolver extends NormalForms { self: Typer =>
           nv
         })
       case tv: TypeVariable if tv.level > upperLvl =>
-        assert(!cache.contains(tv -> false), (tv, cache))
+        assert(!ctx.extrCache.contains(tv -> false), (tv, ctx.extrCache.cache.get(lvl)))
         // * If the TV's level is strictly greater than `upperLvl`,
         // *  it means the TV is quantified by a type being copied,
         // *  so all we need to do is copy this TV along (it is not extruded).
         // * We pick `tv -> true` (and not `tv -> false`) arbitrarily.
         if (tv.lowerBounds.isEmpty && tv.upperBounds.isEmpty) tv
-        else cache.getOrElse(tv -> true, {
+        else ctx.extrCache.getOrElse(tv -> true, {
           val nv = freshVar(tv.prov, S(tv), tv.nameHint)(tv.level)
-          cache += tv -> true -> nv
+          ctx.extrCache.set(tv -> true, nv)
           nv.lowerBounds = tv.lowerBounds.map(extrude(_, lowerLvl, true, upperLvl))
           nv.upperBounds = tv.upperBounds.map(extrude(_, lowerLvl, false, upperLvl))
           nv
         })
       case t @ SpliceType(fs) => 
         t.updateElems(extrude(_, lowerLvl, pol, upperLvl), extrude(_, lowerLvl, !pol, upperLvl), extrude(_, lowerLvl, pol, upperLvl), t.prov)
-      case tv: TypeVariable => cache.getOrElse(tv -> pol, {
+      case tv: TypeVariable => ctx.extrCache.getOrElse(tv -> pol, {
         val nv = freshVar(tv.prov, S(tv), tv.nameHint)(lowerLvl)
-        cache += tv -> pol -> nv
+        ctx.extrCache.set(tv -> pol, nv)
         if (pol) {
           tv.upperBounds ::= nv
           nv.lowerBounds = tv.lowerBounds.map(extrude(_, lowerLvl, pol, upperLvl))

shared/src/main/scala/mlscript/Typer.scala

@@ -46,6 +46,37 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
 
   type GenLambdas >: Bool
   def doGenLambdas(implicit gl: GenLambdas): Bool = gl === true
+
+  class ExtrCache(
+    val cache: MutMap[Level, MutMap[TypeVarOrRigidVar->Bool, TypeVarOrRigidVar]],
+  ) {
+      private var cycle: Int = 0
+      // TODO maybe find a better way
+      def clearAbove()(implicit lvl: Level): Unit = 
+        if (cycle > 1024) {
+          cache.keys.foreach(k => if (k > lvl) cache.remove(k))
+          cycle = 0
+        }
+
+      def getOrElse(k: TypeVarOrRigidVar->Bool, df: => TypeVarOrRigidVar)(implicit lvl: Level): TypeVarOrRigidVar =
+        cache.get(lvl).flatMap(_.get(k)).getOrElse(df)
+
+      def set(k: TypeVarOrRigidVar->Bool, v: TypeVarOrRigidVar)(implicit lvl: Level): Unit = {
+        cycle += 1
+        cache.get(lvl) match {
+          case None => cache += lvl -> MutMap(k -> v)
+          case Some(cc) => cc += k -> v
+        }
+        clearAbove()  // TODO
+      }
+
+     def contains(k: TypeVarOrRigidVar->Bool)(implicit lvl: Level): Bool =
+      cache.get(lvl).map(_.contains(k)).getOrElse(false)
+  }
+
+  object ExtrCache {
+    def empty: ExtrCache = new ExtrCache(MutMap.empty)
+  }
 
   /**  `env`: maps the names of all global and local bindings to their types
     *  Keys of `mthEnv`:
@@ -67,8 +98,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
       tyDefs2: MutMap[Str, DelayedTypeInfo],
       inRecursiveDef: Opt[Var], // TODO rm
       extrCtx: ExtrCtx,
-      extrCache: MutMap[TypeVarOrRigidVar->Bool, TypeVarOrRigidVar], 
-      extrCache2: MutSortMap[TraitTag, TraitTag]
+      extrCache: ExtrCache,
   ) {
     def +=(b: Str -> TypeInfo): Unit = env += b
     def ++=(bs: IterableOnce[Str -> TypeInfo]): Unit = bs.iterator.foreach(+=)
@@ -84,7 +114,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
     def containsMth(parent: Opt[Str], nme: Str): Bool = containsMth(R(parent, nme))
     def nest: Ctx = copy(Some(this), MutMap.empty, MutMap.empty)
     def nextLevel[R](k: Ctx => R)(implicit raise: Raise, prov: TP): R = {
-      val newCtx = copy(lvl = lvl + 1, extrCtx = MutMap.empty, extrCache = MutMap.empty, extrCache2 = MutSortMap.empty)
+      val newCtx = copy(lvl = lvl + 1, extrCtx = MutMap.empty)
       val res = k(newCtx)
       val ec = newCtx.extrCtx
       assert(constrainedTypes || newCtx.extrCtx.isEmpty)
@@ -154,8 +184,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
       tyDefs2 = MutMap.empty,
       inRecursiveDef = N,
       MutMap.empty,
-      MutMap.empty, 
-      MutSortMap.empty
+      ExtrCache.empty
     )
     def init: Ctx = if (!newDefs) initBase else {
       val res = initBase.copy(

shared/src/test/diff/ecoop23/PolymorphicVariants.mls

@@ -25,7 +25,7 @@ fun list_assoc(s, l) =
       if s === h.0 then Success(h.1)
       else list_assoc(s, t)
     Nil then NotFound()
-//│ fun list_assoc: forall 'A. (Eql[?], Cons[{0: anything, 1: 'A} | ~??A] | Nil) -> (NotFound | Success['A])
+//│ fun list_assoc: forall 'a 'A. (Eql[in 'a], Cons[{0: 'a, 1: 'A} | ~??A] | Nil) -> (NotFound | Success['A])
 
 // fun list_assoc(s: Str, l: Cons[{ _1: Str, _2: 'b }] | Nil): NotFound | Success['b]
 
@@ -73,9 +73,9 @@ mixin EvalLambda {
 //│ mixin EvalLambda() {
 //│   super: {eval: ('a, 'b) -> 'c}
 //│   this: {
-//│     eval: ('a, ??A & 'A) -> 'd & (Cons[[Str, 'd]], ??A0 & 'A0) -> 'c & (Cons[[Str, Var]], ??A1 & 'A1) -> 'A2
+//│     eval: ('a, ??A & 'A) -> 'd & (Cons[[Str, 'd]], ??A0 & 'A0) -> 'c & (Cons[[Str, Var] | 'A1], ??A1 & 'A2) -> 'A3
 //│   }
-//│   fun eval: ('a & (Cons[anything] | Nil), Abs['A1] | App['A & (Abs['A0] | Object & ~#Abs | ~??A)] | Object & 'b & ~#Abs & ~#App) -> (Abs['A2] | App['d] | 'c)
+//│   fun eval: ('a & (Cons['A1] | Nil), Abs['A2] | App['A & (Abs['A0] | Object & ~#Abs | ~??A)] | Object & 'b & ~#Abs & ~#App) -> (Abs['A3] | App['d] | 'c)
 //│ }
 
 module Test1 extends EvalVar, EvalLambda
@@ -98,14 +98,14 @@ Test1.eval(Nil, Var("a"))
 Test1.eval(Nil, Abs("b", Var("a")))
 //│ Abs['a] | App['a] | 'a
 //│   where
-//│     'a :> Abs['a] | Var | App['a]
+//│     'a :> App['a] | Abs['a] | Var
 //│ res
 //│     = Abs {}
 
 Test1.eval(Cons(["c", Var("d")], Nil), App(Abs("b", Var("b")), Var("c")))
 //│ Abs['a] | App['a] | 'a
 //│   where
-//│     'a :> App['a] | Abs['a] | Var
+//│     'a :> Abs['a] | Var | App['a]
 //│ res
 //│     = Var {}
 
@@ -129,7 +129,7 @@ fun map_expr(f, v) =
     Numb then v
     Add(l, r) then Add(f(l), f(r))
     Mul(l, r) then Mul(f(l), f(r))
-//│ fun map_expr: forall 'A 'A0 'A1 'A2. ((??A & 'A1) -> 'A2 & (??A0 & 'A) -> 'A0, Add['A1] | Mul['A] | Numb | Var) -> (Add['A2] | Mul['A0] | Numb | Var)
+//│ fun map_expr: forall 'A 'A0 'A1 'A2. ((??A & 'A) -> 'A0 & (??A0 & 'A1) -> 'A2, Add['A] | Mul['A1] | Numb | Var) -> (Add['A0] | Mul['A2] | Numb | Var)
 
 mixin EvalExpr {
   fun eval(sub, v) =

shared/src/test/diff/ecoop23/SimpleRegionDSL_annot.mls

@@ -360,7 +360,7 @@ fun mk(n) = if n is
   _ then Scale(Vector(0, 0), mk(n))
 //│ fun mk: forall 'a. Object -> 'a
 //│   where
-//│     'a :> Outside['a] | Union['a] | Intersect['a] | Translate['a] | Scale['a]
+//│     'a :> Outside['a] | Translate['a] | Scale['a] | Union['a] | Intersect['a]
 
 :re
 TestElim.eliminate(mk(100))

shared/src/test/diff/ecoop23/SimpleRegionDSL_raw.mls

@@ -372,13 +372,13 @@ fun mk(n) = if n is
   _ then Scale(Vector(0, 0), mk(n))
 //│ fun mk: forall 'a. Object -> 'a
 //│   where
-//│     'a :> Outside['a] | Union['a] | Intersect['a] | Translate['a] | Scale['a]
+//│     'a :> Outside['a] | Scale['a] | Union['a] | Intersect['a] | Translate['a]
 
 :re
 TestElim.eliminate(mk(100))
 //│ Intersect['a] | Outside['a] | Scale['a] | Translate['a] | Union['a] | 'a
 //│   where
-//│     'a :> Union['a] | Intersect['a] | Translate['a] | Scale['a] | Outside['a]
+//│     'a :> Outside['a] | Union['a] | Intersect['a] | Translate['a] | Scale['a]
 //│ res
 //│ Runtime error:
 //│   RangeError: Maximum call stack size exceeded
@@ -412,7 +412,7 @@ module Lang extends SizeBase, SizeExt, Contains, Text, IsUniv, IsEmpty, Eliminat
 //│   'Region5 <: Intersect['Region3] | Outside['Region4] | Scale['Region5] | Translate['Region6] | Union['Region7] | 'a & (Object & ~#Intersect & ~#Outside & ~#Scale & ~#Translate & ~#Union | ~#Intersect & ~#Outside & ~#Scale & ~#Translate & ~#Union & ~??Region21) | ~??Region21
 //│   'Region6 <: Intersect['Region3] | Outside['Region4] | Scale['Region5] | Translate['Region6] | Union['Region7] | 'a & (Object & ~#Intersect & ~#Outside & ~#Scale & ~#Translate & ~#Union | ~#Intersect & ~#Outside & ~#Scale & ~#Translate & ~#Union & ~??Region22) | ~??Region22
 //│   'Region7 <: Intersect['Region3] | Outside['Region4] | Scale['Region5] | Translate['Region6] | Union['Region7] | 'a & (Object & ~#Intersect & ~#Outside & ~#Scale & ~#Translate & ~#Union | ~#Intersect & ~#Outside & ~#Scale & ~#Translate & ~#Union & ~??Region23) | ~??Region23
-//│   'a :> Union['a] | Intersect['a] | Translate['a] | Scale['a] | Outside['a]
+//│   'a :> Outside['a] | Union['a] | Intersect['a] | Translate['a] | Scale['a]
 //│   'Region <: Circle | Intersect['Region] | Outside['Region0] | Translate['Region1] | Union['Region2] | ~??Region24
 //│   'Region0 <: Circle | Intersect['Region] | Outside['Region0] | Translate['Region1] | Union['Region2] | ~??Region25
 //│   'Region1 <: Circle | Intersect['Region] | Outside['Region0] | Translate['Region1] | Union['Region2] | ~??Region26

shared/src/test/diff/ex/RepMin.mls

@@ -88,7 +88,7 @@ fun walk(t, mn) = if t is
     let mnl = walk(l, mn)
     let mnr = walk(r, mn)
     [min(mnl.0, mnr.0), Node(mnl.1, mnr.1)]
-//│ fun walk: forall 'A 'A0 'a. (Leaf['A & (Num | ~??A)] | Node['A0 & (Num | ~??A | ~??A0)], Int & 'a) -> [??A & ('A | ??A0 & 'A0), Leaf['a | ??A & ('A | ??A0 & 'A0)] | Node['a | ??A & ('A | ??A0 & 'A0)]]
+//│ fun walk: forall 'A 'a 'A0. (Leaf['A0 & (Num | ~??A)] | Node['A & (Num | ~??A | ~??A0)], Int & 'a) -> [??A & ('A0 | ??A0 & 'A), Leaf['a | ??A & ('A0 | ??A0 & 'A)] | Node['a | ??A & ('A0 | ??A0 & 'A)]]
 
 
 let tree = Node of (Node of (Node of Leaf(1), Leaf(5)), Leaf(3)), Node of Leaf(3), Leaf(2)
@@ -125,10 +125,10 @@ fun walk(t, mn) = if t is
     Pair of n, Leaf(if n > 2 * mn then mn else n)
   Node(l, r) and walk(l, mn) is Pair(mn1, l1) and walk(r, mn) is Pair(mn2, r1) then
     Pair of min(mn1, mn2), Node(l1, r1)
-//│ fun walk: forall 'a 'A 'A0 'A1 'b. (Leaf['A1 & (Num | ~??A)] | Node['A & (Num | ~??A | ~??A0)], Int & 'a) -> Pair[??A & 'b & ('A1 | ??A0 & 'A), nothing]
+//│ fun walk: forall 'A 'A0 'A1 'a 'b. (Leaf['A1 & (Num | ~??A)] | Node['A & (Num | ~??A | ~??A0)], Int & 'b) -> Pair[??A & 'a & ('A1 | ??A0 & 'A), nothing]
 //│   where
-//│     'b :> ??A1 & 'A0 | ??A2 & 'A0
-//│     'A0 :> 'b | ??A & ('A1 | ??A0 & 'A)
+//│     'a :> ??A1 & 'A0 | ??A2 & 'A0
+//│     'A0 :> 'a | ??A & ('A1 | ??A0 & 'A)
 
 String of walk(tree, 2)
 //│ Str

shared/src/test/diff/fcp-lit/Leijen.mls

@@ -946,7 +946,7 @@ def newRef4: forall 'a 's. 'a -> ST['s, (Ref['s, 'a], Ref['s, 'a])]
 runST4 (newRef4 1)
 //│ runST4: (forall 's. ST['s, ('a, 'b,)]) -> ('a, 'b,)
 //│ newRef4: 'a -> ST['s, (Ref['s, 'a], Ref['s, 'a],)]
-//│ res: (Ref[in ??s & 's out 's | 's0 | ??s0, 1], Ref[in ??s & 's0 out 's | 's0 | ??s0, 1],)
+//│ res: (Ref[in ??s & 's out 's | ??s0, 1], Ref[in ??s & 's out 's | ??s0, 1],)
 
 
 // * Distributivity demonstration:

shared/src/test/diff/fcp-lit/QML.mls

@@ -202,7 +202,7 @@ def sstep = fun xx -> xx (fun (xinit, xsub) ->
     then xsub r1 (div i 2)
     else xsub r2 (div i 2) in
   fun f -> f (init, sub))
-//│ ((forall 'a 'b 'c 'd 'e. ('e -> 'a, 'b -> int -> 'c,) -> (('e -> ('a, 'a,), (('b, 'b,),) -> int -> 'c,) -> 'd) -> 'd) -> 'f) -> 'f
+//│ ((forall 'a 'b 'c 'd 'e. ('c -> 'd, 'e -> int -> 'a,) -> (('c -> ('d, 'd,), (('e, 'e,),) -> int -> 'a,) -> 'b) -> 'b) -> 'f) -> 'f
 //│   <:  sstep:
 //│ ExSmall -> ExSmall
 //│ ╔══[ERROR] Type error in def definition
@@ -440,7 +440,7 @@ def step = fun xx -> xx (fun ((((xinit, xsub), xupdate), xfold),) ->
     else (fst r, xupdate (snd r) (div i 2) a) in
   let fold f b r = xfold f (xfold f b (fst r)) (snd r) in
     fun f -> f ((((init, sub), update), fold),) )
-//│ ((forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm 'n 'o 'p. (((('l -> 'm, 'b -> int -> 'f,), 'i -> int -> 'e -> 'p & 'n -> int -> 'e -> 'j,), 'h -> ('d -> 'o -> 'k & 'c -> 'g -> 'd),),) -> ((((('l -> ('m, 'm,), (('b, 'b,),) -> int -> 'f,), forall 'q 'r. (('i & 'q, 'n & 'r,),) -> int -> 'e -> ('p | 'q, 'r | 'j,),), 'h -> 'c -> (('g, 'o,),) -> 'k,),) -> 'a) -> 'a) -> 's) -> 's
+//│ ((forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm 'n 'o 'p. (((('f -> 'b, 'l -> int -> 'n,), 'g -> int -> 'c -> 'o & 'i -> int -> 'c -> 'd,), 'h -> ('k -> 'p -> 'a & 'e -> 'm -> 'k),),) -> ((((('f -> ('b, 'b,), (('l, 'l,),) -> int -> 'n,), forall 'q 'r. (('g & 'q, 'i & 'r,),) -> int -> 'c -> ('o | 'q, 'r | 'd,),), 'h -> 'e -> (('m, 'p,),) -> 'a,),) -> 'j) -> 'j) -> 's) -> 's
 //│   <:  step:
 //│ ExSig -> ExSig
 //│ ╔══[ERROR] Type error in def definition

shared/src/test/diff/fcp/QML_exist_Records_D.mls

@@ -363,10 +363,10 @@ def step arr = arr (forall 'a. fun impl -> forall 'r. fun (k: ArraysImplConsumer
 
 // * ...unless we use `stepImpl_ty` instead of `stepImpl`
 def step arr = arr (fun impl -> forall 'r. fun (k: ArraysImplConsumer['a, 'r]) -> k (stepImpl_ty impl))
-//│ ((forall 'r 'a 'r0 'a0 'a1. ArraysImpl[in 'a0 & 'a1 out 'a0 | 'a1, 'r0] -> ArraysImplConsumer['a, 'r] -> 'r) -> 'b) -> 'b
+//│ ((forall 'a 'r 'a0 'a1 'r0. ArraysImpl[in 'a1 & 'a out 'a1 | 'a, 'r] -> ArraysImplConsumer['a0, 'r0] -> 'r0) -> 'b) -> 'b
 //│   where
-//│     'a :> 'a0
-//│        <: 'a1
+//│     'a0 :> 'a1
+//│         <: 'a
 //│   <:  step:
 //│ Arrays['a] -> Arrays['a]
 //│     = [Function: step8]
@@ -467,7 +467,7 @@ def stepImpl_Ann = forall 'a 'rep. fun arrImpl -> {
 //│             = [Function: stepImpl_Ann]
 
 def step arr = arr (fun impl -> fun (k: ArraysImplConsumer['a, 'r]) -> k (stepImpl_Ann impl))
-//│ ((forall 'a 'rep 'b. {
+//│ ((forall 'rep 'b 'a. {
 //│   fold: Fold['a, 'rep],
 //│   init: 'a -> 'rep,
 //│   sub: 'rep -> int -> 'a,