Constraint solving for function overloading

compiler/shared/main/scala/mlscript/compiler/ClassLifter.scala

@@ -510,7 +510,7 @@ class ClassLifter(logDebugMsg: Boolean = false) {
       val nlhs = liftType(lb)
       val nrhs = liftType(ub)
       Bounds(nlhs._1, nrhs._1) -> (nlhs._2 ++ nrhs._2)
-    case Constrained(base: Type, bounds, where) =>
+    case Constrained(base: Type, bounds, where, tscs) =>
       val (nTargs, nCtx) = bounds.map { case (tv, Bounds(lb, ub)) =>
         val nlhs = liftType(lb)
         val nrhs = liftType(ub)
@@ -521,10 +521,18 @@ class ClassLifter(logDebugMsg: Boolean = false) {
         val nrhs = liftType(ub)
         Bounds(nlhs._1, nrhs._1) -> (nlhs._2 ++ nrhs._2)
       }.unzip
+      val (tscs0, nCtx3) = tscs.map { case (tvs, cs) =>
+        val (ntvs,c0) = tvs.map { case (p,v) =>
+          val (nv, c) = liftType(v)
+          (p,nv) -> c
+        }.unzip
+        val (ncs,c1) = cs.map(_.map(liftType).unzip).unzip
+        (ntvs,ncs) -> (c0 ++ c1.flatten)
+      }.unzip
       val (nBase, bCtx) = liftType(base)
-      Constrained(nBase, nTargs, bounds2) ->
-        ((nCtx ++ nCtx2).fold(emptyCtx)(_ ++ _) ++ bCtx)
-    case Constrained(_, _, _) => die
+      Constrained(nBase, nTargs, bounds2, tscs0) ->
+        ((nCtx ++ nCtx2 ++ nCtx3.flatten).fold(emptyCtx)(_ ++ _) ++ bCtx)
+    case Constrained(_, _, _, _) => die
     case Function(lhs, rhs) =>
       val nlhs = liftType(lhs)
       val nrhs = liftType(rhs)

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

@@ -627,6 +627,35 @@ 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)), _)) if noApproximateOverload =>
+              TupleSetConstraints.mk(ov, f) match {
+                case S(tsc) =>
+                  if (tsc.tvs.nonEmpty) {
+                    tsc.tvs.mapValuesIter(_.unwrapProxies).zipWithIndex.flatMap {
+                      case ((true, tv: TV), i) => tv.lowerBounds.iterator.map((_,tv,i,true))
+                      case ((false, tv: TV), i) => tv.upperBounds.iterator.map((_,tv,i,false))
+                      case _ => Nil
+                    }.find {
+                      case (b,_,i,_) =>
+                        tsc.updateImpl(i,b)
+                        tsc.constraints.isEmpty
+                    }.foreach {
+                      case (b,tv,_,p) => if (p) rec(b,tv,false) else rec(tv,b,false)
+                    }
+                    if (tsc.constraints.sizeCompare(1) === 0) {
+                      tsc.tvs.values.map(_.unwrapProxies).foreach {
+                        case tv: TV => tv.tsc.remove(tsc)
+                        case _ => ()
+                      }
+                      tsc.constraints.head.iterator.zip(tsc.tvs).foreach {
+                        case (c, (pol, t)) =>
+                          if (!pol) rec(c, t, false)
+                          if (pol) rec(t, c, false)
+                      }
+                    }
+                  }
+                case N => reportError(S(msg"is not an instance of `${f.expNeg}`"))
+              }
             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(_)), _)) =>
@@ -832,13 +861,53 @@ 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 { (tsc, v) =>
+              v.foreach { i =>
+                if (!tsc.tvs(i)._1) {
+                  tsc.updateOn(i, rhs)
+                  if (tsc.constraints.isEmpty) reportError()
+                }
+              }
+            }
+            val u = lhs.tsc.keysIterator.filter(_.constraints.sizeCompare(1)===0).duplicate
+            u._1.foreach { k =>
+              k.tvs.mapValuesIter(_.unwrapProxies).foreach {
+                case (_,tv: TV) => tv.tsc.remove(k)
+                case _ => ()
+              }
+            }
+            u._2.foreach { k =>
+              k.constraints.head.iterator.zip(k.tvs).foreach {
+                case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false)
+              }
+            }
             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 { (tsc, v) =>
+              v.foreach { i =>
+                if(tsc.tvs(i)._1) {
+                  tsc.updateOn(i, lhs)
+                  if (tsc.constraints.isEmpty) reportError()
+                }
+              }
+            }
+            val u = rhs.tsc.keysIterator.filter(_.constraints.sizeCompare(1)===0).duplicate
+            u._1.foreach { k =>
+              k.tvs.mapValuesIter(_.unwrapProxies).foreach {
+                case (_,tv: TV) => tv.tsc.remove(k)
+                case _ => ()
+              }
+            }
+            u._2.foreach { k =>
+              k.constraints.head.iterator.zip(k.tvs).foreach {
+                case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false)
+              }
+            }
             rhs.upperBounds.foreach(rec(lhs, _, true)) // propagate from the bound
 
 
@@ -1562,9 +1631,24 @@ class ConstraintSolver extends NormalForms { self: Typer =>
             assert(lvl <= below, "this condition should be false for the result to be correct")
             lvl
           })
+          val freshentsc = tv.tsc.flatMap { case (tsc,_) =>
+            if (tsc.tvs.values.map(_.unwrapProxies).forall {
+              case tv: TV => !freshened.contains(tv)
+              case _ => true
+            }) S(tsc) else N
+          }
           freshened += tv -> v
           v.lowerBounds = tv.lowerBounds.mapConserve(freshen)
           v.upperBounds = tv.upperBounds.mapConserve(freshen)
+          freshentsc.foreach { tsc =>
+            val t = new TupleSetConstraints(tsc.constraints, tsc.tvs)
+            t.constraints = t.constraints.map(_.map(freshen))
+            t.tvs = t.tvs.map(x => (x._1,freshen(x._2)))
+            t.tvs.values.map(_.unwrapProxies).zipWithIndex.foreach {
+              case (tv: TV, i) => tv.tsc.updateWith(t)(_.map(_ + i).orElse(S(Set(i))))
+              case _ => ()
+            }
+          }
           v
       }
 

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

@@ -25,6 +25,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,
@@ -78,8 +79,16 @@ trait TypeSimplifier { self: Typer =>
               ).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)
+              renewedtsc += tsc -> t
+              t.tvs = t.tvs.map(x => (x._1, process(x._2, N)))
+              (t, i)
+          }}
         }
-
         nv
 
       case ComposedType(true, l, r) =>
@@ -549,9 +558,15 @@ 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)))
+                    tv.tsc.keys.flatMap(_.tvs).foreach(u => apply(pol.at(tv.level,u._1))(u._2))
+                  }
                 if (pol(tv) =/= S(true))
-                  analyzed1.setAndIfUnset(tv -> false) { tv.upperBounds.foreach(apply(pol.at(tv.level, false))) }
+                  analyzed1.setAndIfUnset(tv -> false) {
+                    tv.upperBounds.foreach(apply(pol.at(tv.level, false)))
+                    tv.tsc.keys.flatMap(_.tvs).foreach(u => apply(pol.at(tv.level,u._1))(u._2))
+                  }
             }
           case _ =>
             super.apply(pol)(st)
@@ -643,8 +658,10 @@ trait TypeSimplifier { self: Typer =>
             case tv: TypeVariable =>
               pol(tv) match {
                 case S(pol_tv) =>
-                  if (analyzed2.add(pol_tv -> tv))
+                  if (analyzed2.add(pol_tv -> tv)) {
                     processImpl(st, pol, pol_tv)
+                    tv.tsc.keys.flatMap(_.tvs).foreach(u => processImpl(u._2,pol.at(tv.level,u._1),pol_tv))
+                  }
                 case N =>
                   if (analyzed2.add(true -> tv))
                     // * To compute the positive co-occurrences
@@ -690,6 +707,7 @@ trait TypeSimplifier { self: Typer =>
                 case S(p) =>
                   (if (p) tv2.lowerBounds else tv2.upperBounds).foreach(go)
                   // (if (p) getLbs(tv2) else getUbs(tv2)).foreach(go)
+                  tv2.tsc.keys.flatMap(_.tvs).foreach(u => go(u._2))
                 case N =>
                   trace(s"Analyzing invar-occ of $tv2") {
                     analyze2(tv2, pol)
@@ -789,7 +807,7 @@ trait TypeSimplifier { self: Typer =>
 
     // * Remove variables that are 'dominated' by another type or variable
     // *  A variable v dominated by T if T is in both of v's positive and negative cooccurrences
-    allVars.foreach { case v => if (v.assignedTo.isEmpty && !varSubst.contains(v)) {
+    allVars.foreach { case v => if (v.assignedTo.isEmpty && !varSubst.contains(v) && v.tsc.isEmpty) {
       println(s"2[v] $v ${coOccurrences.get(true -> v)} ${coOccurrences.get(false -> v)}")
 
       coOccurrences.get(true -> v).iterator.flatMap(_.iterator).foreach {
@@ -807,6 +825,7 @@ trait TypeSimplifier { self: Typer =>
 
         case w: TV if !(w is v) && !varSubst.contains(w) && !varSubst.contains(v) && !recVars(v)
           && coOccurrences.get(false -> v).exists(_(w))
+          && w.tsc.isEmpty
         =>
           // * Here we know that v is 'dominated' by w, so v can be inlined.
           // * Note that we don't want to unify the two variables here
@@ -833,7 +852,7 @@ trait TypeSimplifier { self: Typer =>
 
     // * Unify equivalent variables based on polar co-occurrence analysis:
     allVars.foreach { case v =>
-      if (!v.assignedTo.isDefined && !varSubst.contains(v)) // TODO also handle v.assignedTo.isDefined?
+      if (!v.assignedTo.isDefined && !varSubst.contains(v) && v.tsc.isEmpty) // TODO also handle v.assignedTo.isDefined?
         trace(s"3[v] $v +${coOccurrences.get(true -> v).mkString} -${coOccurrences.get(false -> v).mkString}") {
 
         def go(pol: Bool): Unit = coOccurrences.get(pol -> v).iterator.flatMap(_.iterator).foreach {
@@ -850,6 +869,7 @@ trait TypeSimplifier { self: Typer =>
               )
               && (v.level === w.level)
               // ^ Don't merge variables of differing levels
+              && w.tsc.isEmpty
             =>
             trace(s"[w] $w ${printPol(S(pol))}${coOccurrences.get(pol -> w).mkString}") {
 
@@ -923,6 +943,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]
 
@@ -999,7 +1020,7 @@ trait TypeSimplifier { self: Typer =>
               nv
             })
             pol(tv) match {
-              case S(p) if inlineBounds && !occursInvariantly(tv) && !recVars.contains(tv) =>
+              case S(p) if inlineBounds && !occursInvariantly(tv) && !recVars.contains(tv) && tv.tsc.isEmpty =>
                 // * Inline the bounds of non-rec non-invar-occ type variables
                 println(s"Inlining [${printPol(p)}] bounds of $tv (~> $res)")
                 // if (p) mergeTransform(true, pol, tv, Set.single(tv), canDistribForall) | res
@@ -1017,6 +1038,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)
+                            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

@@ -34,6 +34,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
   var constrainedTypes: Boolean = false
 
   var recordProvenances: Boolean = true
+  var noApproximateOverload: Boolean = false
 
   type Binding = Str -> SimpleType
   type Bindings = Map[Str, SimpleType]
@@ -168,7 +169,15 @@ 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 = innerTy.getVars.unsorted.flatMap(_.tsc.keys.flatMap(_.tvs))
+          .groupBy(_._2)
+          .filter { case (v,pvs) => pvs.sizeIs > 1 }
+        if (ambiguous.nonEmpty) raise(ErrorReport(
+          msg"ambiguous" -> N ::
+          ambiguous.map { case (v,_) => msg"cannot determine satisfiability of type ${v.expPos}" -> v.prov.loco }.toList
+          , true))
+
         println(s"Inferred poly constr: $cty  —— where ${cty.showBounds}")
 
         val cty_fresh =
@@ -662,7 +671,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
@@ -675,6 +684,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)
+          tvs.values.map(_.unwrapProxies).zipWithIndex.foreach {
+            case (tv: TV, i) => tv.tsc.updateWith(tsc)(_.map(_ + i).orElse(S(Set(i))))
+            case _ => ()
+          }
+        }
         res
       case PolyType(vars, ty) =>
         val oldLvl = ctx.lvl
@@ -1860,8 +1877,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 =>
@@ -1969,6 +1988,14 @@ 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(x => (x._1,go(x._2)))
+                  val constrs = tsc.constraints.map(_.map(go))
+                  tscs ::= tvs -> constrs
+                }
+            }
           }
           nv
         })
@@ -2018,17 +2045,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
@@ -2042,16 +2072,16 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne
           val lbs = groups2.toList
           val bounds = (ubs.mapValues(_.reduce(_ &- _)) ++ lbs.mapValues(_.reduce(_ | _)).map(_.swap))
           val processed = bounds.map { case (lo, hi) => Bounds(go(lo), go(hi)) }
-          Constrained(go(bod), Nil, processed)
+          Constrained(go(bod), Nil, processed, 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)
   }