Skip to content

Commit 99b465b

Browse files
auhtauht
committed
rcd union neg disjointess
1 parent 91ac0d4 commit 99b465b

File tree

14 files changed

+191
-229
lines changed

14 files changed

+191
-229
lines changed

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

Lines changed: 19 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -122,27 +122,20 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
122122
if k.subsetOf(um.keySet) then
123123
k.foreach(k => constrainImpl(um(k), wm(k)))
124124
else cctx.err
125-
case (Inter(S(u: RcdType)), Union(f, Nil, rs@(RcdType(w) :: _))) =>
126-
val ws = rs.foldLeft(Nil): (x, w) =>
127-
val d = Type.disjoint(w, u)
128-
if d === S(Set.empty) then x else Ls(d -> w) ++ x
129-
ws match
130-
case Nil => cctx.err
131-
case (_, w) :: Nil => constrainImpl(u, w)
132-
case ((_, RcdType(w)) :: (_, RcdType(z)) :: _) =>
133-
val (wm, zm) = (w.toMap, z.toMap)
134-
val k = wm.keySet & zm.keySet
135-
val dk = k.find(k => Type.disjoint(wm(k), zm(k)) === S(Set.empty)).get
136-
val ku = ws.foldLeft(Bot: Type):
137-
case (ku, (_, w)) => ku | w.fields.find(_._1 === dk).get._2
138-
ws.foreach:
139-
case (S(k), w) => k.foreach: k =>
140-
DisjSub(mutable.LinkedHashSet.from(k), Nil, Ls(u -> RcdType(w.fields.filter(_._1 =/= k)))).commit()
141-
case _ =>
142-
constrainImpl(u.fields.find(_._1 === dk).get._2, ku)
143-
ws.foreach:
144-
case (N, w) => constrainImpl(u, RcdType(w.fields.filter(_._1 =/= dk)))
145-
case _ =>
125+
case (Inter(S(u: RcdType)), Union(f, Nil, rs)) =>
126+
val us = u.fields.keys.toSet
127+
val ws = rs.filter(_.fields.keys.forall(us))
128+
if ws.isEmpty then cctx.err
129+
else
130+
val q = ws.foldLeft(Bot: Type): (q, w) =>
131+
val wq = Type.discriminant(w)
132+
Type.disjoint(wq, u) match
133+
case N => constrainImpl(u & wq, w)
134+
case S(k) => k.foreach(k => DisjSub(mutable.LinkedHashSet.from(k), Nil, Ls(wq -> w)).commit())
135+
q | wq
136+
Type.disjoint(q.!, u) match
137+
case N => constrainImpl(Top, Bot)
138+
case S(k) => k.foreach(k => DisjSub(mutable.LinkedHashSet.from(k), Nil, Ls(Top -> Bot)).commit())
146139
case (Inter(S(fs: Ls[FunType])), Union(S(FunType(args2, ret2, eff2)), Nil, Nil)) =>
147140
val k = args2.flatMap(x => Type.disjoint(x, x))
148141
if k.forall(_.nonEmpty) then
@@ -154,19 +147,17 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
154147
constrainImpl(f.ret, ret2)
155148
constrainImpl(f.eff, eff2)
156149
else
157-
val args = f.map(x => Type.discriminant(x.args))
150+
val args = f.map(x => RcdType(x.args.zipWithIndex.map(u => (s"${u._2}", u._1))))
158151
val args2r = args2.zipWithIndex.map(u => (s"${u._2}", u._1))
159152
val args2q = RcdType(args2r)
160-
val (cs, dss) = (args.iterator.zip(f).map:
161-
case ((q, r), f) =>
162-
val rm = r.fields.toMap
163-
val rcs = args2r.flatMap(u => rm.get(u._1).filter(_ =/= Top).map(u._2 -> _))
164-
val cs = (f.ret, ret2) :: (f.eff, eff2) :: rcs
153+
val (cs, dss) = (args.iterator.map(Type.discriminant).zip(f).map:
154+
case (q, f) =>
155+
val cs = (f.ret, ret2) :: (f.eff, eff2) :: Nil //rcs
165156
Type.disjoint(q, args2q) match
166157
case N => (cs, Nil)
167158
case S(k) =>
168159
(Nil, k.map(k => DisjSub(mutable.LinkedHashSet.from(k), Nil, cs)))).toList.unzip
169-
val c = (args2q, args.foldLeft(Bot: Type) { case (t, (q, _)) => t | q })
160+
val c = (args2q, args.foldLeft(Bot: Type)(_ | _))
170161
if k.isEmpty then
171162
if f.isEmpty then
172163
cctx.err

‎hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -173,15 +173,15 @@ class BBTyper(using elState: Elaborator.State, tl: TL)(using Config):
173173
if !pol then
174174
val lfa = l.toDnf.conjs.flatMap(_.i.v).collect:
175175
case (f :: fs) =>
176-
val fd = Type.discriminant(f.args)._1
176+
val fd = Type.discriminant(f.args).flatten
177177
fs.foldLeft(fd: Type, fd.fields.keys.toSet): (x, y) =>
178-
val d = Type.discriminant(y.args)._1
178+
val d = Type.discriminant(y.args).flatten
179179
(x._1 | d, x._2 & d.fields.keys.toSet)
180180
val rfa = r.toDnf.conjs.flatMap(_.i.v).collect:
181181
case (f :: fs) =>
182-
val fd = Type.discriminant(f.args)._1
182+
val fd = Type.discriminant(f.args).flatten
183183
fs.foldLeft(fd: Type, fd.fields.keys.toSet): (x, y) =>
184-
val d = Type.discriminant(y.args)._1
184+
val d = Type.discriminant(y.args).flatten
185185
(x._1 | d, x._2 & d.fields.keys.toSet)
186186
val d = lfa.iterator.flatMap(x => rfa.iterator.map(y => (x, y))).exists:
187187
case ((x, u), (y, w)) => (u & w).isEmpty || Type.disjoint(x, y) =/= S(Set.empty)
@@ -386,19 +386,20 @@ class BBTyper(using elState: Elaborator.State, tl: TL)(using Config):
386386
val nestCtx = ctx.nest
387387
given BbCtx = nestCtx
388388
val (nc, dss, cs) = constraintCollector
389-
val sv0 = HashMap.empty[Ref, InfVar]
390389
sv.keys.foreach: s =>
391390
val v = freshVar(new TempSymbol(S(s), s.sym.nme))
392391
nestCtx += s.sym -> v
393-
sv0 += s -> v
394392
val (termTy, termEff) = typeCheck(term)(using c = nc)
395393
val sk = freshSkolem(name)
396394
nestCtx += name -> termTy
397395
nc.constrain(termEff, eff)
398396
path.foreach: p =>
399397
val m = p.toMap
400398
val d = p.flatMap { case (s, t) => sv.get(s).flatMap(st => Type.disjoint(t.!, st)) }
401-
val sc = sv.toList.map { case (s, t) => (m.getOrElse(s, Bot).! & t, sv0(s)) }
399+
val sc = sv.toList.map:
400+
case (s, t) =>
401+
val v = nestCtx.get(s.sym).get
402+
(m.getOrElse(s, Bot).! & t, monoOrErr(v, s))
402403
if d.isEmpty then
403404
dss.foreach(c.commit(_))
404405
(sc ++ cs).distinct.foreach(u => constrain(u._1, u._2))
@@ -411,16 +412,17 @@ class BBTyper(using elState: Elaborator.State, tl: TL)(using Config):
411412
case Split.Else(e) =>
412413
val (nc, dss, cs) = constraintCollector
413414
val ctx1 = ctx.nest
414-
val sv0 = HashMap.empty[Ref, InfVar]
415415
sv.keys.foreach: s =>
416416
val v = freshVar(new TempSymbol(S(s), s.sym.nme))
417417
ctx1 += s.sym -> v
418-
sv0 += s -> v
419418
nc.constrain(ascribe(e, sign)(using ctx1, c = nc)._2, eff)
420419
path.foreach: p =>
421420
val m = p.toMap
422421
val d = p.flatMap { case (s, t) => sv.get(s).flatMap(st => Type.disjoint(t.!, st)) }
423-
val sc = sv.toList.map { case (s, t) => (m.getOrElse(s, Bot).! & t, sv0(s)) }
422+
val sc = sv.toList.map:
423+
case (s, t) =>
424+
val v = ctx1.get(s.sym).get
425+
(m.getOrElse(s, Bot).! & t, monoOrErr(v, s))
424426
if d.isEmpty then
425427
dss.foreach(c.commit(_))
426428
(sc ++ cs).distinct.foreach(u => constrain(u._1, u._2))

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

Lines changed: 39 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -300,53 +300,57 @@ object Type:
300300
then lhs | rhs
301301
else lhs & rhs
302302
def mkNegType(ty: Type): Type = ty.!
303-
def discriminant(a: Ls[Type]): (RcdType, RcdType) =
304-
discriminantRcd(RcdType(a.zipWithIndex.map(u => (s"${u._2}", u._1.toBasic))).flatten)
305-
def discriminantRcd(a: RcdType): (RcdType, RcdType) =
306-
val (u, w) = (a.fields.map:
307-
case (a, t) =>
308-
val (q, r) = discriminant(t.toBasic)
309-
(RcdType(Ls(a -> q)), RcdType(Ls(a -> r)))
310-
).unzip
311-
(u.reduce(_ & _), w.reduce(_ & _))
312-
def discriminant(a: BasicType): (BasicType, BasicType) = a.simp.toBasic match
313-
case Bot => (Bot, Bot)
314-
case c@ClassLikeType(_, Nil) => (c, Top)
315-
case ClassLikeType(c, t) => (ClassLikeType(c, t.map(_ => Wildcard.empty)), a)
316-
case a@RcdType(_ :: _) => discriminantRcd(a)
317-
case a@ComposedType(l, r, true) =>
318-
val q = (discriminant(l.toBasic)._1 | discriminant(r.toBasic)._1).toBasic
319-
(q, (a | q.!).toBasic)
320-
case ComposedType(l, r, false) =>
321-
val (u, w) = discriminant(l.toBasic)
322-
val (q, p) = discriminant(r.toBasic)
323-
((u & q).toBasic, (w & p).toBasic)
324-
case NegType(t) => (a, Top)
325-
case a => (Top, a)
326-
def disjointIU(i: Inter, u: Union)(using TL): Opt[Set[Set[InfVar -> BasicType]]] = (i.v, u.cls) match
327-
case (S(c: ClassLikeType), cs) if cs.exists(_.name.uid === c.name.uid) => S(Set.empty)
328-
case (S(RcdType(u)), _) =>
329-
val kk = u.values.map(t => disjointDisj(t.toDnf)).toList
330-
val k = kk.flatten.toList
331-
if k.isEmpty then N
303+
def discriminant(a: Ls[Type])(using TL): RcdType =
304+
discriminantRcd(RcdType(a.zipWithIndex.map(u => (s"${u._2}", u._1.toBasic))))
305+
def discriminantRcd(a: RcdType)(using TL): RcdType =
306+
RcdType(a.fields.flatMap:
307+
case (a, t) => discriminant(t) match
308+
case Top => N
309+
case t => S(a -> t))
310+
def discriminantIU(i: Inter, u: Union)(using TL): BasicType = (i.v, u.cls) match
311+
case (N, cs) => cs.reduceOption[Type](_ | _).fold(Top)(NegType(_))
312+
case (S(ClassLikeType(c, t)), cs) => if cs.exists(_.name.uid === c.uid) then Bot else ClassLikeType(c, t.map(_ => Wildcard.empty))
313+
case (S(u: RcdType), _) => discriminantRcd(u)
314+
case _ => Top
315+
def discriminant(t: Type)(using TL): BasicType =
316+
t.toDnf.conjs.foldLeft(Bot: Type)((x, y) => x | discriminantIU(y.i, y.u)).simp.toBasic
317+
def disjointIU(i: Inter, u: Union)(using TL): Opt[Set[Set[InfVar -> BasicType]]] = (i.v, u.cls, u.rcd) match
318+
case (S(c: ClassLikeType), cs, _) if cs.exists(_.name.uid === c.name.uid) => S(Set.empty)
319+
case (S(RcdType(u)), _, rs) =>
320+
val k = u.values.flatMap(t => disjointDisj(t.toDnf)).toList
321+
val rd =
322+
if rs.isEmpty then Nil
323+
else
324+
val um = u.toMap
325+
val p = rs.foldLeft[Ls[Ls[Str -> Type]]](Ls(Nil)): (p, w) =>
326+
if w.fields.keys.forall(um.contains) then p.flatMap(x => w.fields.map(_ :: x)) else p
327+
p.map: p =>
328+
val m = p.groupMapReduce(_._1)(_._2)(_ | _)
329+
val d = p.keys.distinct.flatMap(a => Type.disjoint(m(a).!, um(a)))
330+
if d.isEmpty then N
331+
else S(d.reduce((x, y) => y.flatMap(y => x.map(_ ++ y))))
332+
if k.isEmpty then
333+
if rd.isEmpty || rd.contains(N) then N else S(rd.flatten.flatten.toSet)
332334
else if k.exists(_.isEmpty) then S(Set.empty)
333-
else S(k.reduce((x, y) => y.flatMap(y => x.map(_ ++ y))))
335+
else
336+
if rd.contains(N) then N
337+
else S(k.reduce((x, y) => y.flatMap(y => x.map(_ ++ y))) ++ rd.flatten.flatten)
334338
case _ => N
335339
def disjointConj(ty: Conj)(using TL): Opt[Set[Set[InfVar -> BasicType]]] =
336340
val d = disjointIU(ty.i, ty.u)
337341
if d.exists(_.isEmpty) then S(Set.empty)
338-
else (ty.i.v, ty.u.cls, ty.vars.iterator.filter(_._2).keys.toList) match
339-
case (_, _, Nil) => d
340-
case (N, Nil, v :: Nil) =>
342+
else (ty.i.v, ty.u.cls, ty.u.rcd, ty.vars.iterator.filter(_._2).keys.toList) match
343+
case (_, _, _, Nil) => d
344+
case (N, Nil, Nil, v :: Nil) =>
341345
val lb = v.state.lowerBounds.reduceOption(_ | _).orElse(S(Bot)).get
342346
disjointDisj(lb.toDnf).map(_ + Set(v -> v))
343-
case (i, c, vs) =>
347+
case (i, c, r, vs) =>
344348
val j = i match
345349
case S(ClassLikeType(c, _)) => S(ClassLikeType(c, Nil))
346350
case S(u: RcdType) => S(u)
347351
case _ => N
348352
val vd = vs.combinations(2).collect { case x :: y :: _ => Ls(x -> y, y -> x) }.flatten.toList
349-
val ds = vs.flatMap(v => (j ++ c.reduceOption[Type](_ | _).map(_.!)).map(x => v -> x.toBasic)).toSet ++ vd
353+
val ds = vs.flatMap(v => (j ++ (c ++ r).reduceOption[Type](_ | _).map(_.!)).map(x => v -> x.toBasic)).toSet ++ vd
350354
val lb = vs.flatMap(_.state.lowerBounds.reduceOption[Type](_ | _)).reduceOption(_ & _).orElse(S(Bot)).get
351355
val t = lb & Conj(Inter(j), Union(N, c, Nil), Nil)
352356
disjointDisj(t.toDnf).map(_ + ds)

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

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@ fun f() = new Printer(foofoo)
169169
f
170170
//│ Type: ['T, 'x] -> () -> Printer['T]
171171
//│ Where:
172-
//│ 'T#'T ∨ ( 'T#'T ∨ Str <: Str ∧ ⊥ <: ⊥ ∧ 'T <: 'x){0: 'T} <: {0: ⊤}
172+
//│ 'T#'T ∨ ( 'T#'T ∨ Str <: Str ∧ ⊥ <: ⊥){0: 'T} <: {0: 'x}
173173
//│ 'x <: Int
174174

175175
f().Printer#f(42)
@@ -184,7 +184,8 @@ f().Printer#f("oops")
184184
//│ ╟── because: cannot constrain Str <: 'T
185185
//│ ╟── because: cannot constrain Str <: ¬(¬'T1)
186186
//│ ╟── because: cannot constrain Str <: 'T1
187-
//│ ╟── because: cannot constrain 'T1 <: 'x
187+
//│ ╟── because: cannot constrain {0: 'T1} <: {0: ¬⊥ & 'x}
188+
//│ ╟── because: cannot constrain 'T1 <: ¬⊥ & 'x
188189
//│ ╟── because: cannot constrain 'T1 <: 'x
189190
//│ ╟── because: cannot constrain 'T1 <: Int
190191
//│ ╟── because: cannot constrain 'T1 <: ¬(¬{Int})
@@ -197,12 +198,13 @@ let ip = new Printer(foofoo) in ip.Printer#f(42)
197198
:e
198199
let ip = new Printer(foofoo) in ip.Printer#f("42")
199200
//│ ╔══[ERROR] Type error in string literal with expected type 'T
200-
//│ ║ l.198: let ip = new Printer(foofoo) in ip.Printer#f("42")
201+
//│ ║ l.199: let ip = new Printer(foofoo) in ip.Printer#f("42")
201202
//│ ║ ^^^^
202203
//│ ╟── because: cannot constrain Str <: 'T
203204
//│ ╟── because: cannot constrain Str <: 'T
204205
//│ ╟── because: cannot constrain Str <: ¬(¬'T)
205206
//│ ╟── because: cannot constrain Str <: 'T
207+
//│ ╟── because: cannot constrain {0: 'T} <: {0: 'x}
206208
//│ ╟── because: cannot constrain 'T <: 'x
207209
//│ ╟── because: cannot constrain 'T <: 'x
208210
//│ ╟── because: cannot constrain 'T <: ¬¬Int
@@ -219,7 +221,7 @@ fun inc(x) = x + 1
219221
new TFun(inc)
220222
//│ Type: TFun['T]
221223
//│ Where:
222-
//│ 'T#'T ∨ ( 'T#'T ∨ Int <: 'T ∧ ⊥ <: ⊥ ∧ 'T <: 'x){0: 'T} <: {0: ⊤}
224+
//│ 'T#'T ∨ ( 'T#'T ∨ Int <: 'T ∧ ⊥ <: ⊥){0: 'T} <: {0: 'x}
223225
//│ 'x <: ¬¬Int
224226

225227
let tf = new TFun(inc) in tf.TFun#f(1)
@@ -228,12 +230,13 @@ let tf = new TFun(inc) in tf.TFun#f(1)
228230
:e
229231
let tf = new TFun(inc) in tf.TFun#f("1")
230232
//│ ╔══[ERROR] Type error in string literal with expected type 'T
231-
//│ ║ l.229: let tf = new TFun(inc) in tf.TFun#f("1")
233+
//│ ║ l.231: let tf = new TFun(inc) in tf.TFun#f("1")
232234
//│ ║ ^^^
233235
//│ ╟── because: cannot constrain Str <: 'T
234236
//│ ╟── because: cannot constrain Str <: 'T
235237
//│ ╟── because: cannot constrain Str <: ¬(¬'T)
236238
//│ ╟── because: cannot constrain Str <: 'T
239+
//│ ╟── because: cannot constrain {0: 'T} <: {0: 'x}
237240
//│ ╟── because: cannot constrain 'T <: 'x
238241
//│ ╟── because: cannot constrain 'T <: 'x
239242
//│ ╟── because: cannot constrain 'T <: ¬¬Int
@@ -345,7 +348,7 @@ f
345348
f(x => x).Foo#x
346349
//│ Type: ('A) ->{⊥} 'A
347350
//│ Where:
348-
//│ 'A#'A ∨ ( 'A#'A ∨ 'x <: 'A ∧ ⊥ <: ⊥ ∧ 'A <: 'x){0: 'A} <: {0: ⊤}
351+
//│ 'A#'A ∨ ( 'A#'A ∨ 'x <: 'A ∧ ⊥ <: ⊥){0: 'A} <: {0: 'x}
349352

350353
g => (new Foo(g)).Foo#x
351354
//│ Type: ('A -> 'A) ->{⊥} ('A) ->{⊥} 'A
@@ -358,7 +361,7 @@ throw new Error("oops")
358361
:e
359362
throw 42
360363
//│ ╔══[ERROR] Type error in throw
361-
//│ ║ l.359: throw 42
364+
//│ ║ l.362: throw 42
362365
//│ ║ ^^
363366
//│ ╙── because: cannot constrain Int <: Error
364367
//│ Type: ⊥

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ bazbaz
8787
//│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A
8888
//│ Where:
8989
//│ 'A <: Int
90-
//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥ ∧ 'A <: 'A){0: 'A} <: {0: ⊤}
90+
//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥){0: 'A} <: {0: 'A}
9191

9292
bazbaz(42)(x => x + 1)
9393
//│ Type: Int
@@ -98,7 +98,7 @@ cc
9898
//│ Where:
9999
//│ 'A -> 'A <: 'B
100100
//│ 'B <: 'A -> 'A
101-
//│ 'B#'B ∨ ( 'B#'B ∨ 'B <: 'B ∧ ⊥ <: ⊥ ∧ 'B <: 'B){0: 'B} <: {0: ⊤}
101+
//│ 'B#'B ∨ ( 'B#'B ∨ 'B <: 'B ∧ ⊥ <: ⊥){0: 'B} <: {0: 'B}
102102
//│ 'B -> 'B <: 'A
103103
//│ 'A <: 'B -> 'B
104104

@@ -119,14 +119,14 @@ bazbaz as [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) ->
119119
//│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A
120120
//│ Where:
121121
//│ 'A <: Int
122-
//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥ ∧ 'A <: 'A){0: 'A} <: {0: ⊤}
122+
//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥){0: 'A} <: {0: 'A}
123123

124124

125125
(x => f => bazbaz(x)(f)) as [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A
126126
//│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A
127127
//│ Where:
128128
//│ 'A <: Int
129-
//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥ ∧ 'A <: 'A){0: 'A} <: {0: ⊤}
129+
//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥){0: 'A} <: {0: 'A}
130130

131131

132132
h(x => f => bazbaz(x)(f))(42)

‎hkmc2/shared/src/test/mlscript/bbml/bbDisjoint.mls

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -224,6 +224,7 @@ fun foo(r1) =
224224
//│ ╟── because: cannot constrain 'r1 ->{'eff} 'app <: 'foo
225225
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: 'foo
226226
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: Region[in 'r2 out 'r21] ->{'eff1} 'app1
227+
//│ ╟── because: cannot constrain {0: Region[in 'r2 out 'r21]} <: {0: 'r1}
227228
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1
228229
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1
229230
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: Region[in 'reg out 'reg1]
@@ -246,6 +247,7 @@ fun foo(r1) =
246247
//│ ╟── because: cannot constrain 'r1 ->{'eff} 'app <: 'foo
247248
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: 'foo
248249
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: Region[in 'r2 out 'r21] ->{'eff1} 'app1
250+
//│ ╟── because: cannot constrain {0: Region[in 'r2 out 'r21]} <: {0: 'r1}
249251
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1
250252
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1
251253
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: Region[in 'reg out 'reg1]

‎hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ g
7474
f(g)
7575
//│ Type: ('A) ->{⊥} Int
7676
//│ Where:
77-
//│ 'A#C ∨ ( 'A#C ∨ 'D <: B ∧ ⊥ <: ⊥ ∧ C[out B] & 'A <: C[in Int out 'D]){0: C[out B] & 'A} <: {0: C[?]}
77+
//│ 'A#C ∨ ( 'A#C ∨ 'D <: B ∧ ⊥ <: ⊥){0: C[out B] & 'A} <: {0: C[in Int out 'D]}
7878

7979
fun foo: C[in Int out Nothing]
8080
foo
@@ -94,7 +94,8 @@ f(g)(bar)
9494
//│ ║ ^^^
9595
//│ ╟── because: cannot constrain C[Int] <: 'A
9696
//│ ╟── because: cannot constrain C[in Int out Int] <: 'A
97-
//│ ╟── because: cannot constrain C[out B] & 'A <: C[in Int out 'D]
97+
//│ ╟── because: cannot constrain {0: C[out B] & 'A} <: {0: C[in Int out 'D]}
98+
//│ ╟── because: cannot constrain C[in ⊥ out B] ∧ 'A <: C[in Int out 'D]
9899
//│ ╟── because: cannot constrain 'A <: ¬C[in ⊥ out ¬⊥ & 'B1] | C[in Int out ¬⊥ & 'D1]
99100
//│ ╟── because: cannot constrain C[in Int out Int] <: ¬C[in ⊥ out ¬⊥ & 'B1] | C[in Int out ¬⊥ & 'D1]
100101
//│ ╟── because: cannot constrain (Int) & ('B1) <: ¬⊥ & 'D1

‎hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -76,15 +76,15 @@ inc
7676
inc(c => log(show(c)))
7777
//│ Type: CodeBase[out 'x -> 'cde, ⊥, ?]
7878
//│ Where:
79-
//│ 'x1#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int}
79+
//│ 'x1#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int & ¬⊥, 1: Int & ¬⊥}
8080
//│ 'x <: 'cde1
81-
//│ 'cde1#'cde1 ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int}
81+
//│ 'cde1#'cde1 ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int & ¬⊥, 1: Int & ¬⊥}
8282
//│ Int <: 'cde2
8383
//│ 'cde <: ⊤
8484
//│ 'app <: 'cde
8585
//│ 'app <: 'app1
8686
//│ 'x1 <: 'x
87-
//│ 'x#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int}
87+
//│ 'x#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int & ¬⊥, 1: Int & ¬⊥}
8888

8989

9090
fun body: [T, C] -> (CodeBase[out Int, out T, out Any], CodeBase[out Int, out C, out Any]) -> Int -> CodeBase[out Int, out T | C, out Any]

0 commit comments

Comments
 (0)