no disjoint upperbound

Author: auht

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

@@ -92,9 +92,6 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
             cctx.nest(v -> nc) givenIn:
               v.state.upperBounds ::= nc
               v.state.lowerBounds.foreach(lb => constrainImpl(lb, nc))
-              v.state.disjsub.foreach: d =>
-                Type.disjoint(d.disjoint(v), bd.toBasic.simp.toBasic)(Set.empty)(using c = mutable.Map.empty)
-                  .foreach(_.foreach(k => DisjSub(d.disjoint ++ k, d.dss, d.cs).commit()))
           else
             log(s"New bound: ${v.showDbg} :> ${bd.showDbg}")
             cctx.nest(bd -> v) givenIn:

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

@@ -306,11 +306,8 @@ object Type:
         case (v: InfVar, _) =>
             val p = prev + (v->b)
             val k = v.state.lowerBounds.map(lb => disjoint(lb.toBasic.simp.toBasic, b)(p))
-              if k.exists(_.isEmpty) then N
-              else
-                val u = (k.flatten.flatten.toSet + Set.empty).map(_ + (v -> b))
-                val w = v.state.upperBounds.flatMap(ub => disjoint(ub.toBasic.simp.toBasic, b)(p))
-                S(w.fold(u)((x, y) => y.flatMap(y => x.map(_ ++ y))))
+            if k.exists(_.isEmpty) then N
+            else S((k.flatten.flatten.toSet + Set.empty).map(_ + (v -> b)))
         case (_, v: InfVar) => disjoint(v, a)(prev)
         case _ => N
     }) else N

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

@@ -38,6 +38,7 @@ x=>
 //│   'x <: Int ∨ Bool
 //│   'x <: Int
 //│   'x#Int ∨ Int<:'app ∧ ⊥<:'eff}
+//│   'x#Bool ∨ Bool<:'app ∧ ⊥<:'eff}
 
 fun ap1(f)=f(1)
 ap1(idIB)
@@ -58,17 +59,17 @@ x=>idIB(x)
 :todo // BbML
 fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
 //│ ╔══[ERROR] General type is not allowed here.
-//│ ║  l.59: 	fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
+//│ ║  l.60: 	fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
 //│ ╙──      	                           ^^^
 //│ ╔══[ERROR] General type is not allowed here.
-//│ ║  l.59: 	fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
+//│ ║  l.60: 	fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
 //│ ╙──      	                                                   ^^^^
 //│ Type: ⊤
 
 :todo // BbML
 idIIBB([1, 2])
 //│ ╔══[ERROR] Term shape not yet supported by BbML: Tup(List(Fld(‹›,Lit(IntLit(1)),None), Fld(‹›,Lit(IntLit(2)),None)))
-//│ ║  l.69: 	idIIBB([1, 2])
+//│ ║  l.70: 	idIIBB([1, 2])
 //│ ╙──      	       ^^^^^^
 //│ Type: ⊥
 
@@ -98,8 +99,8 @@ idIIBB(new Pair(1, true))
 :todo
 fun foo: ["x": Int, "y": Int]
 //│ ╔══[ERROR] Invalid type
-//│ ║  l.99: 	fun foo: ["x": Int, "y": Int]
-//│ ╙──      	         ^^^^^^^^^^^^^^^^^^^^
+//│ ║  l.100: 	fun foo: ["x": Int, "y": Int]
+//│ ╙──       	         ^^^^^^^^^^^^^^^^^^^^
 //│ Type: ⊤
 
 foo

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

@@ -87,7 +87,7 @@ bazbaz
 //│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A
 //│ Where:
 //│   'A <: Int
-//│   'A#Int ∨ 'A<:'A ∧ ⊥<:⊥ ∧ 'A<:'A}
+//│   'A#'A ∨ 'A<:'A ∧ ⊥<:⊥ ∧ 'A<:'A}
 
 bazbaz(42)(x => x + 1)
 //│ Type: Int
@@ -119,14 +119,14 @@ bazbaz as [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) ->
 //│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A
 //│ Where:
 //│   'A <: Int
-//│   'A#Int ∨ 'A<:'A ∧ ⊥<:⊥ ∧ 'A<:'A}
+//│   'A#'A ∨ 'A<:'A ∧ ⊥<:⊥ ∧ 'A<:'A}
 
 
 (x => f => bazbaz(x)(f)) as [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A
 //│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A
 //│ Where:
 //│   'A <: Int
-//│   'A#Int ∨ 'A<:'A ∧ ⊥<:⊥ ∧ 'A<:'A}
+//│   'A#'A ∨ 'A<:'A ∧ ⊥<:⊥ ∧ 'A<:'A}
 
 
 h(x => f => bazbaz(x)(f))(42)

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

@@ -40,7 +40,7 @@ let foo(f) = (f(x => x(x)) as [A] -> A -> A) in foo
 :todo
 fun foo(f) = (f(x => x(x)) as [A] -> A -> A)
 //│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but ('f) ->{⊥} [outer, 'A] -> ('A) ->{⊥} 'A found
-//│ ║  l.42: 	fun foo(f) = (f(x => x(x)) as [A] -> A -> A)
+//│ ║  l.41: 	fun foo(f) = (f(x => x(x)) as [A] -> A -> A)
 //│ ╙──      	        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 //│ Type: ⊤