Changes from meeting

Author: LPTK

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

@@ -287,25 +287,25 @@ object Type:
     if !prev.contains(a -> b) then c.getOrElseUpdate(a -> b, {
       (a, b) match
         case (Bot, _) | (_, Bot) => S(Set.empty)
-        case (NegType(t),_) => t.toBasic.!.simp.toBasic match
+        case (NegType(t),_) => t.!.simp.toBasic match
           case NegType(_) => N
           case a => disjoint(a, b)(prev)
-        case (_, NegType(t)) => t.toBasic.!.simp.toBasic match
+        case (_, NegType(t)) => t.!.simp.toBasic match
           case NegType(_) => N
           case a => disjoint(a, b)(prev)
         case (ClassLikeType(a, _), ClassLikeType(b, _)) if a.uid =/= b.uid => S(Set.empty)
         case (ComposedType(p, q, true), _) =>
-          val u = disjoint(p.toBasic.simp.toBasic, b)(prev)
-          val w = disjoint(q.toBasic.simp.toBasic, b)(prev)
+          val u = disjoint(p.simp.toBasic, b)(prev)
+          val w = disjoint(q.simp.toBasic, b)(prev)
           u.flatMap(u => w.map(u ++ _))
         case (_, ComposedType(p, q, true)) =>
-          val u = disjoint(a, p.toBasic.simp.toBasic)(prev)
-          val w = disjoint(a, q.toBasic.simp.toBasic)(prev)
+          val u = disjoint(a, p.simp.toBasic)(prev)
+          val w = disjoint(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 => disjoint(lb.toBasic.simp.toBasic, b)(p))
+            val k = v.state.lowerBounds.map(lb => disjoint(lb.simp.toBasic, b)(p))
             if k.exists(_.isEmpty) then N
             else S((k.flatten.flatten.toSet + Set.empty).map(_ + (v -> b)))
         case (_, v: InfVar) => disjoint(v, a)(prev)

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

@@ -4,9 +4,9 @@
 //│ Type: ⊤
 
 
-fun andt(x)=x&&true
-fun k(f:Nothing->Bool)=1
-fun ap(f)=x=>f(x)
+fun andt(x) = x && true
+fun k(f: Nothing -> Bool) = 1
+fun ap(f) = x => f(x)
 //│ Type: ⊤
 
 k(andt)
@@ -30,15 +30,28 @@ idIB(true)
 idIB(if true then 1 else true)
 //│ Type: Bool ∨ Int
 
-x=>
+x =>
   let y = x+1
   idIB(x)
 //│ Type: ('x) ->{⊥} ⊥
 //│ Where:
 //│   'x <: Int ∨ Bool
 //│   'x <: Int
-//│   'x#Bool ∨ Bool<:'app ∧ ⊥<:'eff}
 //│   'x#Int ∨ Int<:'app ∧ ⊥<:'eff}
+//│   'x#Bool ∨ Bool<:'app ∧ ⊥<:'eff}
+
+(x: Int) =>
+  let y = x + 1
+  idIB(x)
+//│ Type: (Int) ->{⊥} Int
+
+(x: Bool) =>
+  idIB(x)
+//│ Type: (Bool) ->{⊥} Bool
+
+(x: Bool) =>
+  idIB(idIB(x))
+//│ Type: (Bool) ->{⊥} Bool ∨ Int
 
 fun ap1(f)=f(1)
 ap1(idIB)
@@ -48,32 +61,53 @@ ap(idIB)(1)
 //│ Type: Int
 
 :todo
-x=>idIB(x)
+x => idIB(x)
 //│ Type: ('x) ->{⊥} ⊥
 //│ Where:
 //│   'x <: Int ∨ Bool
+//│   'x#Bool ∨ Bool<:'app ∧ ⊥<:'eff}
 //│   'x#Int ∨ Int<:'app ∧ ⊥<:'eff}
+
+fun forward(x) = idIB(x)
+forward
+//│ Type: ['x] -> 'x -> ⊥
+//│ Where:
+//│   'x <: Int ∨ Bool
 //│   'x#Bool ∨ Bool<:'app ∧ ⊥<:'eff}
+//│   'x#Int ∨ Int<:'app ∧ ⊥<:'eff}
+
+forward(1)
+//│ Type: ⊥
+
+forward(true)
+//│ Type: ⊥
 
 
 :todo // BbML
 fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
 //│ ╔══[ERROR] General type is not allowed here.
-//│ ║  l.60: 	fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
+//│ ║  l.87: 	fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
 //│ ╙──      	                           ^^^
 //│ ╔══[ERROR] General type is not allowed here.
-//│ ║  l.60: 	fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
+//│ ║  l.87: 	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.70: 	idIIBB([1, 2])
+//│ ║  l.97: 	idIIBB([1, 2])
 //│ ╙──      	       ^^^^^^
 //│ Type: ⊥
 
 
+x => if x is
+  Int then 0
+  Bool then 0
+//│ Type: (((¬Bool ∨ Int) ∨ Bool) ∧ (¬Int ∨ Int)) ->{⊥} Int
+
+
+
 class Pair[out A, out B](fst: A, snd: B)
 //│ Type: ⊤
 
@@ -99,7 +133,7 @@ idIIBB(new Pair(1, true))
 :todo
 fun foo: ["x": Int, "y": Int]
 //│ ╔══[ERROR] Invalid type
-//│ ║  l.100: 	fun foo: ["x": Int, "y": Int]
+//│ ║  l.134: 	fun foo: ["x": Int, "y": Int]
 //│ ╙──       	         ^^^^^^^^^^^^^^^^^^^^
 //│ Type: ⊤