Constraint solving for function overloading

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

@@ -619,6 +619,13 @@ class ConstraintSolver extends NormalForms { self: Typer =>
               recLb(ar.inner, b.inner)
               rec(b.inner.ub, ar.inner.ub, false)
             case (LhsRefined(S(b: ArrayBase), ts, r, _), _) => reportError()
+            case (LhsRefined(S(ov: Overload), ts, r, trs), RhsBases(_, S(L(f: FunctionType)), _)) =>
+              TupleSetConstraints.mk(ov, f) match {
+                case S(tsc) => if (!tsc.tvs.isEmpty && tsc.constraints.isEmpty) reportError()
+                case N => reportError()
+              }
+              // val t = TupleSetConstraints.mk(ov)
+              // annoying(Nil, LhsRefined(S(t), ts, r, trs), Nil, done_rs)
             case (LhsRefined(S(ov: Overload), ts, r, trs), _) =>
               annoying(Nil, LhsRefined(S(ov.approximatePos), ts, r, trs), Nil, done_rs) // TODO remove approx. with ambiguous constraints
             case (LhsRefined(S(Without(b, ns)), ts, r, _), RhsBases(pts, N | S(L(_)), _)) =>
@@ -818,13 +825,41 @@ class ConstraintSolver extends NormalForms { self: Typer =>
             val newBound = (cctx._1 ::: cctx._2.reverse).foldRight(rhs)((c, ty) =>
               if (c.prov is noProv) ty else mkProxy(ty, c.prov))
             lhs.upperBounds ::= newBound // update the bound
+            lhs.tsc.foreachEntry {
+              case (tsc, i) =>
+                if (!tsc.tvs(i)._1) {
+                  tsc.updateOn(i, rhs)
+                  if (tsc.constraints.isEmpty) reportError()
+                }
+            }
+            val u = lhs.tsc.filter(_._1.constraints.sizeCompare(1) === 0)
+            u.foreachEntry { case (k, _) => lhs.tsc.remove(k) }
+            u.foreachEntry { case (k, _) =>
+              k.constraints.head.zip(k.tvs).foreach {
+                case (c, (pol, t)) => if (pol) rec(t, c, true) else rec(c, t, true)
+              }
+            }
             lhs.lowerBounds.foreach(rec(_, rhs, true)) // propagate from the bound
 
           case (lhs, rhs: TypeVariable) if lhs.level <= rhs.level =>
             println(s"NEW $rhs LB (${lhs.level})")
             val newBound = (cctx._1 ::: cctx._2.reverse).foldLeft(lhs)((ty, c) =>
               if (c.prov is noProv) ty else mkProxy(ty, c.prov))
             rhs.lowerBounds ::= newBound // update the bound
+            rhs.tsc.foreachEntry {
+              case (tsc, i) =>
+                if(tsc.tvs(i)._1) {
+                  tsc.updateOn(i, lhs)
+                  if (tsc.constraints.isEmpty) reportError()
+                }
+            }
+            val u = rhs.tsc.filter(_._1.constraints.sizeCompare(1) === 0)
+            u.foreachEntry { case (k, _) => rhs.tsc.remove(k) }
+            u.foreachEntry { case (k, _) =>
+              k.constraints.head.zip(k.tvs).foreach {
+                case (c, (pol, t)) => if (pol) rec(t, c, true) else rec(c, t, true)
+              }
+            }
             rhs.upperBounds.foreach(rec(lhs, _, true)) // propagate from the bound
 
 
@@ -1472,6 +1507,7 @@ class ConstraintSolver extends NormalForms { self: Typer =>
         (implicit ctx: Ctx, freshened: MutMap[TV, ST])
         : SimpleType =
   {
+    val freshenedTsc: MutMap[TupleSetConstraints, TupleSetConstraints] = MutMap.empty
     def freshenImpl(ty: SimpleType, below: Level): SimpleType =
     // (trace(s"${lvl}. FRESHEN $ty || $above .. $below  ${ty.level} ${ty.level <= above}")
     {
@@ -1550,6 +1586,24 @@ class ConstraintSolver extends NormalForms { self: Typer =>
           freshened += tv -> v
           v.lowerBounds = tv.lowerBounds.mapConserve(freshen)
           v.upperBounds = tv.upperBounds.mapConserve(freshen)
+          tv.tsc.foreachEntry {
+            case (tsc, i) =>
+              val t = freshenedTsc.get(tsc) match {
+                case S(tsc) => tsc
+                case N =>
+                  val t = new TupleSetConstraints(tsc.constraints, tsc.tvs)(tsc.prov)
+                  freshenedTsc += tsc -> t
+                  t
+              }
+              t.tvs = t.tvs.zipWithIndex.map {
+                case ((p, tv: TV), j) if j == i => tv.tsc.remove(t); (p, v)
+                case (u, _) => u
+              }
+              t.tvs.zipWithIndex.foreach {
+                case ((_, tv: TV), i) => tv.tsc.update(t, i)
+                case _ => ()
+              }
+          }
           v
       }
 

shared/src/main/scala/mlscript/TypeSimplifier.scala

@@ -26,6 +26,7 @@ trait TypeSimplifier { self: Typer =>
     println(s"allVarPols: ${printPols(allVarPols)}")
 
     val renewed = MutMap.empty[TypeVariable, TypeVariable]
+    val renewedtsc = MutMap.empty[TupleSetConstraints, TupleSetConstraints]
 
     def renew(tv: TypeVariable): TypeVariable =
       renewed.getOrElseUpdate(tv,
@@ -75,8 +76,16 @@ trait TypeSimplifier { self: Typer =>
               tv.upperBounds.reverseIterator.map(process(_, S(false -> tv)))
                 .reduceOption(_ &- _).filterNot(_.isTop).toList
             else Nil
+          nv.tsc ++= tv.tsc.map { case (tsc, i) => renewedtsc.get(tsc) match {
+            case S(tsc) => (tsc, i)
+            case N if inPlace => (tsc, i)
+            case N =>
+              val t = new TupleSetConstraints(tsc.constraints, tsc.tvs)(tsc.prov)
+              renewedtsc += tsc -> t
+              t.tvs = t.tvs.map(x => (x._1, process(x._2, N)))
+              (t, i)
+          }}
         }
-
         nv
 
       case ComposedType(true, l, r) =>
@@ -544,7 +553,9 @@ trait TypeSimplifier { self: Typer =>
                 analyzed1.setAndIfUnset(tv -> pol(tv).getOrElse(false)) { apply(pol)(ty) }
               case N =>
                 if (pol(tv) =/= S(false))
-                  analyzed1.setAndIfUnset(tv -> true) { tv.lowerBounds.foreach(apply(pol.at(tv.level, true))) }
+                  analyzed1.setAndIfUnset(tv -> true) {
+                    tv.lowerBounds.foreach(apply(pol.at(tv.level, true)))
+                  }
                 if (pol(tv) =/= S(true))
                   analyzed1.setAndIfUnset(tv -> false) { tv.upperBounds.foreach(apply(pol.at(tv.level, false))) }
             }
@@ -918,6 +929,7 @@ trait TypeSimplifier { self: Typer =>
     println(s"[rec] ${recVars}")
 
     val renewals = MutMap.empty[TypeVariable, TypeVariable]
+    val renewaltsc = MutMap.empty[TupleSetConstraints, TupleSetConstraints]
 
     val semp = Set.empty[TV]
 
@@ -1012,6 +1024,14 @@ trait TypeSimplifier { self: Typer =>
                           res.lowerBounds = tv.lowerBounds.map(transform(_, pol.at(tv.level, true), Set.single(tv)))
                         if (occNums.contains(false -> tv))
                           res.upperBounds = tv.upperBounds.map(transform(_, pol.at(tv.level, false), Set.single(tv)))
+                        res.tsc ++= tv.tsc.map { case (tsc, i) => renewaltsc.get(tsc) match {
+                          case S(tsc) => (tsc, i)
+                          case N =>
+                            val t = new TupleSetConstraints(tsc.constraints, tsc.tvs)(tsc.prov)
+                            renewaltsc += tsc -> t
+                            t.tvs = t.tvs.map(x => (x._1, transform(x._2, PolMap.neu, Set.empty)))
+                            (t, i)
+                        }}
                     }
                     res
                   }()

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

@@ -112,7 +112,13 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
               assert(b.level > lvl)
               if (p) (b, tv) else (tv, b) }
           }.toList, innerTy)
-
+
+        val ambiguous: Bool = innerTy.getVars.toList.flatMap(_.tsc)
+          .flatMap(_._1.tvs.map(_._2))
+          .collect { case x: TV => x }
+          .exists(_.tsc.sizeIs > 1)
+        if (ambiguous) raise(ErrorReport(Ls(fromStr("ambiguous") -> N), true))
+
         println(s"Inferred poly constr: $cty  —— where ${cty.showBounds}")
 
         val cty_fresh =
@@ -578,7 +584,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
         tv.assignedTo = S(bod)
         tv
       case Rem(base, fs) => Without(rec(base), fs.toSortedSet)(tyTp(ty.toLoc, "field removal type"))
-      case Constrained(base, tvbs, where) =>
+      case Constrained(base, tvbs, where, tscs) =>
         val res = rec(base match {
           case ty: Type => ty
           case _ => die
@@ -591,6 +597,14 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
           constrain(rec(lo), rec(hi))(raise,
             tp(mergeOptions(lo.toLoc, hi.toLoc)(_ ++ _), "constraint specifiation"), ctx)
         }
+        tscs.foreach { case (typevars, constrs) =>
+          val tvs = typevars.map(x => (x._1, rec(x._2)))
+          val tsc = new TupleSetConstraints(constrs.map(_.map(rec)), tvs)(res.prov)
+          tvs.zipWithIndex.foreach {
+            case ((_, tv: TV), i) => tv.tsc += tsc -> i
+            case _ => ()
+          }
+        }
         res
       case PolyType(vars, ty) =>
         val oldLvl = ctx.lvl
@@ -1674,8 +1688,10 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
     val expandType = ()
 
     var bounds: Ls[TypeVar -> Bounds] = Nil
+    var tscs: Ls[Ls[(Bool, Type)] -> Ls[Ls[Type]]] = Nil
 
     val seenVars = mutable.Set.empty[TV]
+    val seenTscs = mutable.Set.empty[TupleSetConstraints]
 
     def field(ft: FieldType)(implicit ectx: ExpCtx): Field = ft match {
       case FieldType(S(l: TV), u: TV) if l === u =>
@@ -1783,6 +1799,17 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
                 if (l =/= Bot || u =/= Top)
                   bounds ::= nv -> Bounds(l, u)
             }
+            tv.tsc.foreachEntry {
+              case (tsc, i) =>
+                if (seenTscs.add(tsc)) {
+                  val tvs = tsc.tvs.map {
+                    case (pol, tv: TV) => (pol, tv.asTypeVar)
+                    case (pol, t) => (pol, go(t))
+                  }
+                  val constrs = tsc.constraints.map(_.map(go))
+                  tscs ::= tvs -> constrs
+                }
+            }
           }
           nv
         })
@@ -1832,17 +1859,20 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
         case Overload(as) => as.map(go).reduce(Inter)
         case PolymorphicType(lvl, bod) =>
           val boundsSize = bounds.size
+          val tscsSize = tscs.size
           val b = go(bod)
 
           // This is not completely correct: if we've already traversed TVs as part of a previous sibling PolymorphicType,
           // the bounds of these TVs won't be registered again...
           // FIXME in principle we'd want to compute a transitive closure...
           val newBounds = bounds.reverseIterator.drop(boundsSize).toBuffer
+          val newTscs = tscs.reverseIterator.drop(tscsSize).toBuffer
 
           val qvars = bod.varsBetween(lvl, MaxLevel).iterator
           val ftvs = b.freeTypeVariables ++
             newBounds.iterator.map(_._1) ++
-            newBounds.iterator.flatMap(_._2.freeTypeVariables)
+            newBounds.iterator.flatMap(_._2.freeTypeVariables) ++
+            newTscs.iterator.flatMap(_._1.map(_._2))
           val fvars = qvars.filter(tv => ftvs.contains(tv.asTypeVar))
           if (fvars.isEmpty) b else
             PolyType(fvars.map(_.asTypeVar pipe (R(_))).toList, b)
@@ -1851,16 +1881,16 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
           val lbs = others1.mapValues(_.head).groupMap(_._2)(_._1).toList
           val bounds = (ubs.mapValues(_.reduce(_ &- _)) ++ lbs.mapValues(_.reduce(_ | _)).map(_.swap))
           val procesased = bounds.map { case (lo, hi) => Bounds(go(lo), go(hi)) }
-          Constrained(go(bod), Nil, procesased)
+          Constrained(go(bod), Nil, procesased, Nil)
 
         // case DeclType(lvl, info) =>
 
     }
     // }(r => s"~> $r")
 
     val res = goLike(st)(new ExpCtx(Map.empty))
-    if (bounds.isEmpty) res
-    else Constrained(res, bounds, Nil)
+    if (bounds.isEmpty && tscs.isEmpty) res
+    else Constrained(res, bounds, Nil, tscs)
 
     // goLike(st)
   }