Logic subtyping and overloading

hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala

@@ -97,6 +97,8 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
             cctx.nest(bd -> v) givenIn:
               v.state.lowerBounds ::= bd
               v.state.upperBounds.foreach(ub => constrainImpl(bd, ub))
+              v.state.disjsub.toList.iterator.flatMap(_.check(v)).foreach:
+                case (a, b) => constrainImpl(a, b)
       case Conj(i, u, Nil) => (conj.i, conj.u) match
         case (_, Union(N, Nil)) =>
           // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} ∧ ¬⊥" -> N :: Nil))
@@ -107,16 +109,36 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
               constrainArgs(ta1, ta2)
           else constrainConj(Conj(conj.i, Union(f, rest), Nil))
         case (int: Inter, Union(f, _ :: rest)) => constrainConj(Conj(int, Union(f, rest), Nil))
-        case (Inter(S(FunType(args1, ret1, eff1))), Union(S(FunType(args2, ret2, eff2)), Nil)) =>
-          if args1.length =/= args2.length then
-            // raise(ErrorReport(msg"Cannot constrain ${conj.i.toString()} <: ${conj.u.toString()}" -> N :: Nil))
-            cctx.err
-          else
-            args1.zip(args2).foreach {
-              case (a1, a2) => constrainImpl(a2, a1)
-            }
-            constrainImpl(ret1, ret2)
-            constrainImpl(eff1, eff2)
+        case (Inter(S(fs:Ls[FunType])), Union(S(FunType(args2, ret2, eff2)), Nil)) =>
+          val k = args2.flatMap(x => Type.disjoint(x, x))
+          if k.forall(_.nonEmpty) then
+            val f = fs.filter(_.args.length === args2.length)
+            if args2.isEmpty then
+              if f.isEmpty then
+                cctx.err
+              else f.foreach: f =>
+                constrainImpl(f.ret, ret2)
+                constrainImpl(f.eff, eff2)
+            else
+              val args = f.map(x => Type.discriminant(x.args))
+              val c = (args2.head, args.foldLeft(Bot: Type) { case (t, (q, _)) => t | q })
+              val (cs, dss) = (args.iterator.zip(f).map:
+                case ((q, r), f) =>
+                  val cs = c :: (f.ret, ret2) :: (f.eff, eff2) :: args2.tail.zip(r)
+                  Type.disjoint(q, args2.head) match
+                    case N => (cs, Nil)
+                    case S(k) =>
+                      if k.nonEmpty then (Nil, k.map(k => DisjSub(mutable.Set.from(k), Nil, cs)))
+                      else (Nil, Nil)).toList.unzip
+              if k.isEmpty then
+                if f.isEmpty then
+                  cctx.err
+                else
+                  cs.flatten.foreach(u => constrainImpl(u._1, u._2))
+                  dss.flatten.foreach(_.commit())
+              else
+                k.reduce((x, y) => y.flatMap(y => x.map(_ ++ y))).foreach: k =>
+                  DisjSub(mutable.Set.from(k), dss.flatten, cs.flatten).commit()
         case _ =>
           // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} <: ${conj.u.toString()}" -> N :: Nil))
           cctx.err

hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala

@@ -76,7 +76,7 @@ object Conj:
   }){}
   lazy val empty: Conj = Conj(Inter.empty, Union.empty, Nil)
   def mkVar(v: InfVar, pol: Bool) = Conj(Inter.empty, Union.empty, (v, pol) :: Nil)
-  def mkInter(inter: ClassLikeType | FunType) =
+  def mkInter(inter: ClassLikeType | Ls[FunType]) =
     Conj(Inter(S(inter)), Union.empty, Nil)
   def mkUnion(union: ClassLikeType | FunType) =
     Conj(Inter.empty, union match {
@@ -85,18 +85,23 @@ object Conj:
     }, Nil)
 
 // * Some(ClassType) -> C[in D_i out D_i], Some(FunType) -> D_1 ->{D_2} D_3, None -> Top
-final case class Inter(v: Opt[ClassLikeType | FunType]) extends NormalForm:
+final case class Inter(v: Opt[ClassLikeType | Ls[FunType]]) extends NormalForm:
   def isTop: Bool = v.isEmpty
   def merge(other: Inter): Option[Inter] = (v, other.v) match
     case (S(ClassLikeType(cls1, targs1)), S(ClassLikeType(cls2, targs2))) if cls1.uid === cls2.uid =>
       S(Inter(S(ClassLikeType(cls1, targs1.lazyZip(targs2).map(_ & _)))))
     case (S(_: ClassLikeType), S(_: ClassLikeType)) => N
-    case (S(FunType(a1, r1, e1)), S(FunType(a2, r2, e2))) =>
-      S(Inter(S(FunType(a1.lazyZip(a2).map(_ | _), r1 & r2, e1 & e2))))
+    // case (S(FunType(a1, r1, e1)), S(FunType(a2, r2, e2))) =>
+    //   S(Inter(S(FunType(a1.lazyZip(a2).map(_ | _), r1 & r2, e1 & e2))))
+    case (S(a:Ls[FunType]),S(b:Ls[FunType]))=>S(Inter(S(a++b)))
     case (S(v), N) => S(Inter(S(v)))
     case (N, v) => S(Inter(v))
     case _ => N
-  def toBasic: BasicType = v.getOrElse(Top)
+  def toBasic: BasicType = v match
+    case N=>Top
+    case S(x:ClassLikeType)=>x
+    case S(Nil)=>Top
+    case S(x:Ls[FunType])=>x.reduce[Type](_&_).toBasic
   def toDnf(using TL): Disj = Disj(Conj(this, Union(N, Nil), Nil) :: Nil)
   override def show(using Scope): Str =
     toBasic.show
@@ -121,7 +126,7 @@ extends NormalForm with CachedBasicType:
     case (cls1, cls2) => cls1.name.uid <= cls2.name.uid
   }.foldLeft[Ls[ClassLikeType]](Nil)((res, cls) => (res, cls) match {
     case (Nil, cls) => cls :: Nil
-    case (ClassLikeType(cls1, targs1) :: tail, ClassLikeType(cls2, targs2)) if cls1.uid === cls2.uid => 
+    case (ClassLikeType(cls1, targs1) :: tail, ClassLikeType(cls2, targs2)) if cls1.uid === cls2.uid =>
       ClassLikeType(cls1, targs1.lazyZip(targs2).map(_ | _)) :: tail
     case (head :: tail, cls) => cls :: head :: tail
   }))
@@ -182,7 +187,7 @@ object NormalForm:
     case Bot => Disj.bot
     case v: InfVar => Disj(Conj.mkVar(v, true) :: Nil)
     case ct: ClassLikeType => Disj(Conj.mkInter(ct.toNorm) :: Nil)
-    case ft: FunType => Disj(Conj.mkInter(ft.toNorm) :: Nil)
+    case ft: FunType => Disj(Conj.mkInter(Ls(ft.toNorm)) :: Nil)
     case ComposedType(lhs, rhs, pol) =>
       if pol then union(dnf(lhs), dnf(rhs)) else inter(dnf(lhs), dnf(rhs))
     case NegType(ty) => neg(ty)

hkmc2/shared/src/main/scala/hkmc2/bbml/PrettyPrinter.scala

@@ -4,22 +4,29 @@ import scala.collection.mutable.{Set => MutSet, ListBuffer}
 import utils.Scope
 
 class PrettyPrinter(output: String => Unit)(using Scope):
+  def showDisjSub(ds: DisjSub): String = ds match
+    case DisjSub(d, dss, cs) =>
+      val g = d.iterator.map { case (x, y) => s"${x.show}#${y.show} ∨ " }.mkString
+      val h = dss.iterator.map("(" + showDisjSub(_) + ")").mkString(" ∧ ")
+      val b = cs.map { case (x, y) => s" ∧ ${x.simp.show}<:${y.simp.show}"}.mkString
+      s"  $g$h$b"
   def print(ty: GeneralType): Unit =
     output(s"Type: ${ty.show}")
     val bounds = PrettyPrinter.collectBounds(ty).distinct
     if !bounds.isEmpty then
       output("Where:")
       bounds.foreach {
         case (lhs, rhs) => output(s"  ${lhs.show} <: ${rhs.show}")
+        case ds: DisjSub => output(showDisjSub(ds))
       }
 
 object PrettyPrinter:
   def apply(output: String => Unit)(using Scope): PrettyPrinter = new PrettyPrinter(output)
 
   type Bound = (Type, Type) // * Type <: Type
 
-  private def collectBounds(ty: GeneralType): List[Bound] =
-    val res = ListBuffer[Bound]()
+  private def collectBounds(ty: GeneralType): List[Bound | DisjSub] =
+    val res = ListBuffer[Bound | DisjSub]()
     val cache = MutSet[Uid[InfVar]]()
     object CollectBounds extends TypeTraverser:
       override def apply(pol: Boolean)(ty: GeneralType): Unit = ty match
@@ -31,6 +38,7 @@ object PrettyPrinter:
             res ++= state.upperBounds.map: bd =>
               apply(false)(bd)
               (v, bd)
+            res ++= state.disjsub
             super.apply(pol)(ty)
         case _ => super.apply(pol)(ty)
     CollectBounds(true)(ty)

hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala

@@ -191,15 +191,17 @@ class TypeSimplifier(tl: TraceLogger):
             tv.state.upperBounds = newUBs
             val isPos = Analysis.posVars.contains(tv)
             val isNeg = Analysis.negVars.contains(tv)
-            // if (isPos && !isNeg && (Analysis.occsNum(tv) === 1 && {newLBs match { case (tv: IV) :: Nil => true; case _ => false }} || newLBs.forall(_.isSmall))) {
-            if isPos && !isNeg && ({newLBs match { case (tv: IV) :: Nil => true; case _ => false }} || newLBs.forall(_ => true)) then {
-            // if (isPos && !isNeg && ({newLBs match { case (tv: IV) :: Nil => true; case _ => false }})) {
-              newLBs.foldLeft(Bot: Type)(_ | _)
-            } else
-            // if (isNeg && !isPos && (Analysis.occsNum(tv) === 1 && {newUBs match { case (tv: IV) :: Nil => true; case _ => false }} || newUBs.forall(_.isSmall))) {
-            if isNeg && !isPos && ({newUBs match { case (tv: IV) :: Nil => true; case _ => false }} || newUBs.forall(_ => true)) then
-            // if (isNeg && !isPos && ({newUBs match { case (tv: IV) :: Nil => true; case _ => false }})) {
-              newUBs.foldLeft(Top: Type)(_ & _)
+            if tv.state.disjsub.isEmpty then
+              // if (isPos && !isNeg && (Analysis.occsNum(tv) === 1 && {newLBs match { case (tv: IV) :: Nil => true; case _ => false }} || newLBs.forall(_.isSmall))) {
+              if isPos && !isNeg && ({newLBs match { case (tv: IV) :: Nil => true; case _ => false }} || newLBs.forall(_ => true)) then {
+              // if (isPos && !isNeg && ({newLBs match { case (tv: IV) :: Nil => true; case _ => false }})) {
+                newLBs.foldLeft(Bot: Type)(_ | _)
+              } else
+              // if (isNeg && !isPos && (Analysis.occsNum(tv) === 1 && {newUBs match { case (tv: IV) :: Nil => true; case _ => false }} || newUBs.forall(_.isSmall))) {
+              if isNeg && !isPos && ({newUBs match { case (tv: IV) :: Nil => true; case _ => false }} || newUBs.forall(_ => true)) then
+              // if (isNeg && !isPos && ({newUBs match { case (tv: IV) :: Nil => true; case _ => false }})) {
+                newUBs.foldLeft(Top: Type)(_ & _)
+              else tv
             else
               // tv.lowerBounds = newLBs
               // tv.upperBounds = newUBs

hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala

@@ -5,7 +5,7 @@ import mlscript.utils.*, shorthands.*
 import syntax.*
 import semantics.*, semantics.Term.*
 import utils.*
-import scala.collection.mutable.{Set => MutSet}
+import scala.collection.mutable.{Set => MutSet, Map => MutMap}
 import utils.Scope
 import Elaborator.State
 
@@ -281,6 +281,44 @@ object Type:
     then lhs | rhs
     else lhs & rhs
   def mkNegType(ty: Type): Type = ty.!
+  def discriminant(a: Ls[Type]): (BasicType, Ls[Type]) = (a.head.toBasic.simp.toBasic, a.tail)
+  def disjointImpl(a: BasicType, b: BasicType)(prev: Set[BasicType -> BasicType])
+    (using c: MutMap[BasicType -> BasicType, Opt[Set[Set[InfVar->BasicType]]]])
+    : Opt[Set[Set[InfVar->BasicType]]] =
+    if !prev.contains(a -> b) then c.getOrElseUpdate(a -> b, {
+      (a, b) match
+        case (Bot, _) | (_, Bot) => S(Set.empty)
+        case (NegType(t),_) => t.!.simp.toBasic match
+          case NegType(_) => N
+          case a => disjointImpl(a, b)(prev)
+        case (_, NegType(t)) => t.!.simp.toBasic match
+          case NegType(_) => N
+          case a => disjointImpl(a, b)(prev)
+        case (ClassLikeType(a, _), ClassLikeType(b, _)) if a.uid =/= b.uid => S(Set.empty)
+        case (ComposedType(p, q, true), _) =>
+          val u = disjointImpl(p.simp.toBasic, b)(prev)
+          val w = disjointImpl(q.simp.toBasic, b)(prev)
+          u.flatMap(u => w.map(u ++ _))
+        case (_, ComposedType(p, q, true)) =>
+          val u = disjointImpl(a, p.simp.toBasic)(prev)
+          val w = disjointImpl(a, q.simp.toBasic)(prev)
+          u.flatMap(u => w.map(u ++ _))
+        case (a: InfVar, b: InfVar) if a.uid =/= b.uid => N
+        case (v: InfVar, _) =>
+          val p = prev + (v -> b)
+          val k = v.state.lowerBounds.map(lb => disjointImpl(lb.toBasic.simp.toBasic, b)(p))
+          if k.exists(_.isEmpty) then N
+          else S((k.flatten.flatten.toSet + Set.empty).map(_ + (v -> b)))
+        case (_, v: InfVar) =>
+          val p = prev + (a -> v)
+          val k = v.state.lowerBounds.map(lb => disjointImpl(a, lb.toBasic.simp.toBasic)(p))
+          if k.exists(_.isEmpty) then N
+          else S((k.flatten.flatten.toSet + Set.empty).map(_ + (v -> a)))
+        case _ => N
+    }) else S(Set.empty)
+  def disjoint(a: Type, b: Type): Opt[Set[Set[InfVar->BasicType]]] =
+    disjointImpl(a.simp.toBasic, b.simp.toBasic)(Set.empty)(using c = MutMap.empty)
+
 
 // * Poly types can not be used as type arguments
 case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], body: GeneralType) extends GeneralType:
@@ -388,3 +426,42 @@ case class PolyFunType(args: Ls[GeneralType], ret: GeneralType, eff: Type) exten
 class VarState:
   var lowerBounds: Ls[Type] = Nil
   var upperBounds: Ls[Type] = Nil
+  val disjsub: MutSet[DisjSub] = MutSet.empty
+  override def toString = "<>"
+
+case class DisjSub(disjoint: MutSet[InfVar -> BasicType], dss: Ls[DisjSub], cs: Ls[Type -> Type]):
+  def commit() = disjoint.keys.foreach(_.state.disjsub += this)
+  def checkAndCommit()(using c: MutMap[BasicType -> BasicType, Opt[Set[Set[InfVar->BasicType]]]]): Ls[Type -> Type] =
+    val cc: MutSet[InfVar -> BasicType] = MutSet.empty
+    val d = disjoint.flatMap: u =>
+      Type.disjointImpl(u._2, u._1)(Set.empty) match
+        case N =>
+          disjoint -= u
+          cc += u
+          N
+        case S(k) => if k.nonEmpty then S(k) else N
+    if disjoint.isEmpty then
+      dss.flatMap(_.checkAndCommit()) ++ cs
+    else
+      if d.nonEmpty then
+        commit()
+        d.reduce((x, y) => y.flatMap(y => x.map(_ ++ y))).foreach: k =>
+          DisjSub(MutSet.from(k), dss, cs).commit()
+      Nil
+  def checkImpl(v: InfVar)(using c: MutMap[BasicType -> BasicType, Opt[Set[Set[InfVar->BasicType]]]]) =
+    val (u, w) = disjoint.toList.partition(_._1.uid === v.uid)
+    val d = u.flatMap: u =>
+      Type.disjointImpl(u._2, u._1)(Set.empty) match
+        case N =>
+          disjoint -= u
+          N
+        case S(k) => if k.nonEmpty then S(k) else N
+    if disjoint.isEmpty then
+      dss.flatMap(_.checkAndCommit()) ++ cs
+    else
+      if disjoint.forall(_._1.uid =/= v.uid) then v.state.disjsub -= this
+      else if d.nonEmpty then
+        d.foldLeft(Set(w))((x, y) => y.flatMap(y => x.map(_ ++ y))).foreach: k =>
+          DisjSub(MutSet.from(k), dss, cs).commit()
+      Nil
+  def check(v: InfVar) = checkImpl(v)(using c = MutMap.empty)

hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls

@@ -152,7 +152,7 @@ fun foofoo(x) =
 new Printer(foofoo)
 //│ Type: Printer['T]
 //│ Where:
-//│   'T <: Int
+//│   'T#'T ∨  ∧ 'T<:'x ∧ Str<:Str ∧ ⊥<:⊥
 
 let ip = new Printer(foofoo) in ip.Printer#f(42)
 //│ Type: Str
@@ -166,6 +166,10 @@ let ip = new Printer(foofoo) in ip.Printer#f("42")
 //│ ╟── because: cannot constrain  Str  <:  'T
 //│ ╟── because: cannot constrain  Str  <:  ¬(¬'T)
 //│ ╟── because: cannot constrain  Str  <:  'T
+//│ ╟── because: cannot constrain  'T  <:  'x
+//│ ╟── because: cannot constrain  'T  <:  'x
+//│ ╟── because: cannot constrain  'T  <:  ¬¬Int
+//│ ╟── because: cannot constrain  'T  <:  ¬(¬{Int})
 //│ ╙── because: cannot constrain  Str  <:  ¬(¬{Int})
 //│ Type: Str
 
@@ -178,23 +182,49 @@ fun inc(x) = x + 1
 new TFun(inc)
 //│ Type: TFun['T]
 //│ Where:
-//│   Int <: 'T
-//│   'T <: Int
+//│   'T#'T ∨  ∧ 'T<:'x ∧ Int<:'T ∧ ⊥<:⊥
 
 let tf = new TFun(inc) in tf.TFun#f(1)
-//│ Type: Int
+//│ Type: 'T
+//│ Where:
+//│   Int <: 'T
+//│   'T <: Int
+//│    ∧ 'T<:'x ∧ Int<:'T ∧ ⊥<:⊥
 
 :e
 let tf = new TFun(inc) in tf.TFun#f("1")
 //│ ╔══[ERROR] Type error in string literal with expected type 'T
-//│ ║  l.188: 	let tf = new TFun(inc) in tf.TFun#f("1")
+//│ ║  l.195: 	let tf = new TFun(inc) in tf.TFun#f("1")
+//│ ║         	                                    ^^^
+//│ ╟── because: cannot constrain  Str  <:  'T
+//│ ╟── because: cannot constrain  Str  <:  'T
+//│ ╟── because: cannot constrain  Str  <:  ¬(¬'T)
+//│ ╟── because: cannot constrain  Str  <:  'T
+//│ ╟── because: cannot constrain  'T  <:  'x
+//│ ╟── because: cannot constrain  'T  <:  'x
+//│ ╟── because: cannot constrain  'T  <:  ¬¬Int
+//│ ╟── because: cannot constrain  'T  <:  ¬(¬{Int})
+//│ ╙── because: cannot constrain  Str  <:  ¬(¬{Int})
+//│ ╔══[ERROR] Type error in string literal with expected type 'T
+//│ ║  l.195: 	let tf = new TFun(inc) in tf.TFun#f("1")
 //│ ║         	                                    ^^^
 //│ ╟── because: cannot constrain  Str  <:  'T
 //│ ╟── because: cannot constrain  Str  <:  'T
 //│ ╟── because: cannot constrain  Str  <:  ¬(¬'T)
 //│ ╟── because: cannot constrain  Str  <:  'T
+//│ ╟── because: cannot constrain  Int  <:  'T
+//│ ╟── because: cannot constrain  Int  <:  'T
+//│ ╟── because: cannot constrain  'T  <:  'x
+//│ ╟── because: cannot constrain  'T  <:  'x
+//│ ╟── because: cannot constrain  'T  <:  ¬¬Int
+//│ ╟── because: cannot constrain  'T  <:  ¬(¬{Int})
 //│ ╙── because: cannot constrain  Str  <:  ¬(¬{Int})
-//│ Type: Str ∨ Int
+//│ Type: 'T
+//│ Where:
+//│   Int <: 'T
+//│   Str <: 'T
+//│   'T <: Int
+//│    ∧ 'T<:'x ∧ Int<:'T ∧ ⊥<:⊥
 
 class Pair[A, B](fst: A, snd: B)
 //│ Type: ⊤
@@ -254,7 +284,10 @@ fun fact(n) =
 //│ Type: ⊤
 
 fact
-//│ Type: Int -> Int
+//│ Type: ['n] -> 'n -> Int
+//│ Where:
+//│   'n <: Int
+//│   'n#Int ∨  ∧ Int<:'n ∧ Int<:'app ∧ 'eff<:'eff
 
 fact(1)
 //│ Type: Int
@@ -278,7 +311,10 @@ fun fact2 = case
 //│ Type: ⊤
 
 fact2
-//│ Type: Int -> Int
+//│ Type: ['caseScrut] -> 'caseScrut -> Int
+//│ Where:
+//│   'caseScrut <: Int
+//│   'caseScrut#Int ∨  ∧ Int<:'caseScrut ∧ Int<:'app ∧ 'eff<:'eff
 
 fact2(0)
 //│ Type: Int
@@ -296,6 +332,8 @@ f
 
 f(x => x).Foo#x
 //│ Type: ('A) ->{⊥} 'A
+//│ Where:
+//│   'A#'A ∨  ∧ 'A<:'x ∧ 'x<:'A ∧ ⊥<:⊥
 
 g => (new Foo(g)).Foo#x
 //│ Type: ('A -> 'A) ->{⊥} ('A) ->{⊥} 'A
@@ -308,7 +346,7 @@ throw new Error("oops")
 :e
 throw 42
 //│ ╔══[ERROR] Type error in throw
-//│ ║  l.309: 	throw 42
+//│ ║  l.347: 	throw 42
 //│ ║         	      ^^
 //│ ╙── because: cannot constrain  Int  <:  Error
 //│ Type: ⊥