Skip to content

Commit b6b9a0a

Browse files
NeilKleistGaoNeilKleistGao
committed
WIP: Cache properly and improve nf show
1 parent 4d70a25 commit b6b9a0a

17 files changed

+236
-229
lines changed

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ case class CCtx(cache: Cache, parents: Ls[(Type, Type)], origin: Term, exp: Opt[
2121
case N => msg""
2222
}" -> origin.toLoc
2323
:: parents.reverse.map(p =>
24-
msg"because: cannot constrain ${p._1.simp.show} <: ${p._2.simp.show}" -> N
24+
msg"because: cannot constrain ${p._1.show} <: ${p._2.show}" -> N
2525
)
2626
))
2727
def nest(sub: (Type, Type)): CCtx =
@@ -87,13 +87,13 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
8787
else
8888
val bd = if v.lvl >= rest.lvl then rest else extrude(rest)(using v.lvl, true, mutable.HashMap.empty)
8989
if pol then
90-
val nc = Type.mkNegType(bd).toBasic
90+
val nc = Type.mkNegType(bd).toDnf
9191
log(s"New bound: ${v.showDbg} <: ${nc.showDbg}")
9292
cctx.nest(v -> nc) givenIn:
9393
v.state.upperBounds ::= nc
9494
v.state.lowerBounds.foreach(lb => constrainImpl(lb, nc))
9595
else
96-
val c = bd.toBasic
96+
val c = bd.toDnf
9797
log(s"New bound: ${v.showDbg} :> ${c.showDbg}")
9898
cctx.nest(c -> v) givenIn:
9999
v.state.lowerBounds ::= c
@@ -138,7 +138,7 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
138138
case _: ClassLikeType | _: FunType | _: InfVar | Top | Bot => ty
139139

140140
private def constrainImpl(lhs: Type, rhs: Type)(using BbCtx, CCtx, TL): Unit =
141-
val p = lhs.toBasic -> rhs.toBasic
141+
val p = lhs.toDnf -> rhs.toDnf
142142
if cctx.cache(p) then log(s"Cached!")
143143
else trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"):
144144
cctx.nest(p) givenIn:

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,20 +54,22 @@ extends NormalForm with CachedBasicType:
5454
})
5555
def toDnf(using TL): Disj = Disj(this :: Nil)
5656
override def show(using Scope): Str =
57-
((i :: Nil).filterNot(_.isTop).map(_.show) :::
57+
val s = ((i :: Nil).filterNot(_.isTop).map(_.show) :::
5858
(u :: Nil).filterNot(_.isBot).map("¬{"+_.show+"}") :::
5959
vars.map:
6060
case (tv, true) => tv.show
6161
case (tv, false) => "¬" + tv.show
6262
).mkString(" ∧ ")
63+
if s.isEmpty then "⊤" else s
6364

6465
override def showDbg: Str =
65-
((i :: Nil).filterNot(_.isTop).map(_.showDbg) :::
66+
val s = ((i :: Nil).filterNot(_.isTop).map(_.showDbg) :::
6667
(u :: Nil).filterNot(_.isBot).map("~{"+_.showDbg+"}") :::
6768
vars.map:
6869
case (tv, true) => tv.showDbg
6970
case (tv, false) => "~" + tv.showDbg
7071
).mkString(" && ")
72+
if s.isEmpty then "⊤" else s
7173
object Conj:
7274
// * Conj objects cannot be created with `new` except in this file.
7375
// * This is because we want to sort the vars in the apply function.

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,8 +80,6 @@ trait CachedBasicType extends Type:
8080
abstract class TypeExt extends Type:
8181
override def hashCode: Int =
8282
toBasic.hashCode
83-
override def equals(that: Any): Bool =
84-
toBasic === that
8583

8684
sealed abstract class Type extends GeneralType with TypeArg:
8785

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -164,9 +164,9 @@ let ip = new Printer(foofoo) in ip.Printer#f("42")
164164
//│ ║ ^^^^
165165
//│ ╟── because: cannot constrain Str <: 'T
166166
//│ ╟── because: cannot constrain Str <: 'T
167-
//│ ╟── because: cannot constrain Str <: ¬(¬'T)
168167
//│ ╟── because: cannot constrain Str <: 'T
169-
//│ ╙── because: cannot constrain Str <: ¬(¬{Int})
168+
//│ ╟── because: cannot constrain Str <: 'T
169+
//│ ╙── because: cannot constrain Str <: Int
170170
//│ Type: Str
171171

172172
data class TFun[T](f: T -> T)
@@ -191,9 +191,9 @@ let tf = new TFun(inc) in tf.TFun#f("1")
191191
//│ ║ ^^^
192192
//│ ╟── because: cannot constrain Str <: 'T
193193
//│ ╟── because: cannot constrain Str <: 'T
194-
//│ ╟── because: cannot constrain Str <: ¬(¬'T)
195194
//│ ╟── because: cannot constrain Str <: 'T
196-
//│ ╙── because: cannot constrain Str <: ¬(¬{Int})
195+
//│ ╟── because: cannot constrain Str <: 'T
196+
//│ ╙── because: cannot constrain Str <: Int
197197
//│ Type: Str ∨ Int
198198

199199
data class Pair[A, B](fst: A, snd: B)

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -91,10 +91,10 @@ letreg of r =>
9191
//│ ║ l.75: k()
9292
//│ ║ ^^^^^
9393
//│ ╟── because: cannot constrain 'E <: ⊥
94-
//│ ╟── because: cannot constrain 'E <: ¬()
95-
//│ ╟── because: cannot constrain ¬'Rg <: ¬()
94+
//│ ╟── because: cannot constrain 'E <: ⊥
95+
//│ ╟── because: cannot constrain ¬'Rg <: ⊥
9696
//│ ╟── because: cannot constrain ⊤ <: 'Rg
97-
//│ ╙── because: cannot constrain ⊤ <: ¬()
97+
//│ ╙── because: cannot constrain ⊤ <: ⊥
9898
//│ Type: ⊥
9999

100100
:e
@@ -127,10 +127,10 @@ letreg of r =>
127127
//│ ║ l.109: r
128128
//│ ║ ^^^
129129
//│ ╟── because: cannot constrain 'E <: ⊥
130-
//│ ╟── because: cannot constrain 'E <: ¬()
131-
//│ ╟── because: cannot constrain 'Rg <: ¬()
132-
//│ ╟── because: cannot constrain 'Rg <: ¬()
133-
//│ ╙── because: cannot constrain ⊤ <: ¬()
130+
//│ ╟── because: cannot constrain 'E <: ⊥
131+
//│ ╟── because: cannot constrain 'Rg <: ⊥
132+
//│ ╟── because: cannot constrain 'Rg <: ⊥
133+
//│ ╙── because: cannot constrain ⊤ <: ⊥
134134
//│ Type: Reg[?, 'E]
135135
//│ Where:
136136
//│ ⊤ <: 'E
@@ -171,10 +171,10 @@ letreg of r =>
171171
//│ ║ l.157: r
172172
//│ ║ ^^^
173173
//│ ╟── because: cannot constrain 'E <: ⊥
174-
//│ ╟── because: cannot constrain 'E <: ¬()
175-
//│ ╟── because: cannot constrain 'Rg <: ¬()
176-
//│ ╟── because: cannot constrain 'Rg <: ¬()
177-
//│ ╙── because: cannot constrain ⊤ <: ¬()
174+
//│ ╟── because: cannot constrain 'E <: ⊥
175+
//│ ╟── because: cannot constrain 'Rg <: ⊥
176+
//│ ╟── because: cannot constrain 'Rg <: ⊥
177+
//│ ╙── because: cannot constrain ⊤ <: ⊥
178178
//│ Type: Reg[?, 'E]
179179
//│ Where:
180180
//│ ⊤ <: 'E

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -48,10 +48,10 @@ letreg of r =>
4848
//│ ║ l.36: write(r)
4949
//│ ║ ^^^^^^^^^^
5050
//│ ╟── because: cannot constrain 'E <: ⊥
51-
//│ ╟── because: cannot constrain 'E <: ¬()
52-
//│ ╟── because: cannot constrain 'Rg <: ¬()
53-
//│ ╟── because: cannot constrain 'Rg <: ¬()
54-
//│ ╙── because: cannot constrain ⊤ <: ¬()
51+
//│ ╟── because: cannot constrain 'E <: ⊥
52+
//│ ╟── because: cannot constrain 'Rg <: ⊥
53+
//│ ╟── because: cannot constrain 'Rg <: ⊥
54+
//│ ╙── because: cannot constrain ⊤ <: ⊥
5555
//│ Type: Int
5656

5757

@@ -87,10 +87,10 @@ letreg of r =>
8787
//│ ║ l.75: write(r)
8888
//│ ║ ^^^^^^^^^^
8989
//│ ╟── because: cannot constrain 'E <: ⊥
90-
//│ ╟── because: cannot constrain 'E <: ¬()
91-
//│ ╟── because: cannot constrain 'Rg <: ¬()
92-
//│ ╟── because: cannot constrain 'Rg <: ¬()
93-
//│ ╙── because: cannot constrain ⊤ <: ¬()
90+
//│ ╟── because: cannot constrain 'E <: ⊥
91+
//│ ╟── because: cannot constrain 'Rg <: ⊥
92+
//│ ╟── because: cannot constrain 'Rg <: ⊥
93+
//│ ╙── because: cannot constrain ⊤ <: ⊥
9494
//│ Type: Int
9595

9696

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -180,8 +180,8 @@ foo(42, 1)
180180
//│ ║ l.178: foo(42, 1)
181181
//│ ║ ^
182182
//│ ╟── because: cannot constrain Int <: ¬'A
183-
//│ ╟── because: cannot constrain 'A <: ¬(Int)
184-
//│ ╙── because: cannot constrain Int <: ¬(Int)
183+
//│ ╟── because: cannot constrain 'A <: ¬{Int}
184+
//│ ╙── because: cannot constrain Int <: ¬{Int}
185185
//│ Type: Int
186186

187187
foo(42, false)

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,10 +23,10 @@ f => (let g = x => f(x(x)) in g) as [A] -> A -> A
2323
//│ ╔══[ERROR] Type error in block with expected type (A) ->{⊥} A
2424
//│ ║ l.22: f => (let g = x => f(x(x)) in g) as [A] -> A -> A
2525
//│ ║ ^^^^^^^^^^^^^^^^^
26-
//│ ╟── because: cannot constrain 'x ->{'eff ∨ 'eff1} 'app <: A -> A
26+
//│ ╟── because: cannot constrain ('x) ->{'eff ∨ 'eff1} ('app) <: (A) ->{⊥} (A)
2727
//│ ╟── because: cannot constrain A <: 'x
2828
//│ ╟── because: cannot constrain A <: 'x
29-
//│ ╙── because: cannot constrain A <: ¬(¬{'x ->{'eff1} 'app1})
29+
//│ ╙── because: cannot constrain A <: ('x) ->{'eff1} ('app1)
3030
//│ Type: (⊥ -> ⊥) ->{⊥} ['A] -> ('A) ->{⊥} 'A
3131

3232
f => (x => f(x(x)) as [A] -> A -> A)

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

Lines changed: 52 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,12 @@ region x in
3030
//│ ║ l.28: fork((_ => x.ref 1), (_ => x.ref 2))
3131
//│ ║ ^^^^^^^
3232
//│ ╟── because: cannot constrain 'reg <: 'B
33-
//│ ╟── because: cannot constrain 'reg <: ¬(¬'B)
34-
//│ ╟── because: cannot constrain x <: ¬(¬'B)
33+
//│ ╟── because: cannot constrain 'reg <: 'B
34+
//│ ╟── because: cannot constrain x <: 'B
3535
//│ ╟── because: cannot constrain x <: 'B
3636
//│ ╟── because: cannot constrain x <: ¬'A
37-
//│ ╟── because: cannot constrain 'A <: ¬(x)
38-
//│ ╙── because: cannot constrain x <: ¬(x)
37+
//│ ╟── because: cannot constrain 'A <: ¬x
38+
//│ ╙── because: cannot constrain x <: ¬x
3939
//│ Type: Pair[out Ref[Int, ?], out Ref[Int, ?]]
4040

4141

@@ -63,37 +63,38 @@ region x in
6363
//│ ║ l.61: naive_helper(x)
6464
//│ ║ ^
6565
//│ ╟── because: cannot constrain Region[x] <: 'r1
66-
//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'x1 out ¬⊥ ∧ 'x2] <: 'r1
67-
//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'x1 out ¬⊥ ∧ 'x2] <: Region[in 'reg out 'reg1]
66+
//│ ╟── because: cannot constrain Region[in 'x1 out 'x2] <: 'r1
67+
//│ ╟── because: cannot constrain Region[in 'x1 out 'x2] <: Region[in 'reg out 'reg1]
68+
//│ ╟── because: cannot constrain 'x2 <: 'reg1
6869
//│ ╟── because: cannot constrain 'x2 <: 'reg1
69-
//│ ╟── because: cannot constrain 'x2 <: ¬(¬'reg1)
70-
//│ ╟── because: cannot constrain ⊤ <: ¬(¬'reg1)
70+
//│ ╟── because: cannot constrain ⊤ <: 'reg1
7171
//│ ╟── because: cannot constrain ⊤ <: 'reg1
7272
//│ ╙── because: cannot constrain ⊤ <: ⊥
7373
//│ ╔══[ERROR] Type error in reference with expected type 'r1
7474
//│ ║ l.61: naive_helper(x)
7575
//│ ║ ^
7676
//│ ╟── because: cannot constrain Region[x] <: 'r1
77-
//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'x1 out ¬⊥ ∧ 'x2] <: 'r1
78-
//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'x1 out ¬⊥ ∧ 'x2] <: Region[in 'reg out 'reg1]
77+
//│ ╟── because: cannot constrain Region[in 'x1 out 'x2] <: 'r1
78+
//│ ╟── because: cannot constrain Region[in 'x1 out 'x2] <: Region[in 'reg out 'reg1]
79+
//│ ╟── because: cannot constrain 'x2 <: 'reg1
7980
//│ ╟── because: cannot constrain 'x2 <: 'reg1
80-
//│ ╟── because: cannot constrain 'x2 <: ¬(¬'reg1)
81-
//│ ╟── because: cannot constrain ⊤ <: ¬(¬'reg1)
81+
//│ ╟── because: cannot constrain ⊤ <: 'reg1
8282
//│ ╟── because: cannot constrain ⊤ <: 'reg1
8383
//│ ╟── because: cannot constrain ⊤ <: 'reg
84-
//│ ╙── because: cannot constrain ⊤ <: ¬()
84+
//│ ╟── because: cannot constrain ⊤ <: 'reg
85+
//│ ╙── because: cannot constrain ⊤ <: ⊥
8586
//│ ╔══[ERROR] Type error in block
8687
//│ ║ l.61: naive_helper(x)
8788
//│ ║ ^^^^^^^^^^^^^^^
8889
//│ ╟── because: cannot constrain 'eff <: ⊥
89-
//│ ╟── because: cannot constrain 'eff <: ¬()
90-
//│ ╟── because: cannot constrain 'eff1 ∧ ¬'x3 <: ¬()
90+
//│ ╟── because: cannot constrain 'eff <: ⊥
91+
//│ ╟── because: cannot constrain ¬'x3 ∧ 'eff1 <: ⊥
9192
//│ ╟── because: cannot constrain 'eff1 <: 'x3
92-
//│ ╟── because: cannot constrain 'eff1 <: ¬()
93-
//│ ╟── because: cannot constrain 'eff1 <: ¬()
94-
//│ ╟── because: cannot constrain 'reg1 <: ¬()
95-
//│ ╟── because: cannot constrain 'reg1 <: ¬()
96-
//│ ╙── because: cannot constrain ⊤ <: ¬()
93+
//│ ╟── because: cannot constrain 'eff1 <: ⊥
94+
//│ ╟── because: cannot constrain 'eff1 <: ⊥
95+
//│ ╟── because: cannot constrain 'reg1 <: ⊥
96+
//│ ╟── because: cannot constrain 'reg1 <: ⊥
97+
//│ ╙── because: cannot constrain ⊤ <: ⊥
9798
//│ Type: Pair[out Ref[Int, ?], out Ref[Int, ?]]
9899

99100

@@ -127,22 +128,24 @@ region x in
127128
region x in
128129
(region y in let t = helper(x) in 42) as [A] -> Int
129130
//│ ╔══[ERROR] Type error in reference with expected type 'r1
130-
//│ ║ l.128: (region y in let t = helper(x) in 42) as [A] -> Int
131+
//│ ║ l.129: (region y in let t = helper(x) in 42) as [A] -> Int
131132
//│ ║ ^
132133
//│ ╟── because: cannot constrain Region[x] <: 'r1
133-
//│ ╟── because: cannot constrain Region[in x out x] <: 'r1
134-
//│ ╟── because: cannot constrain Region[in x out x] <: Region[in 'reg out 'reg1]
134+
//│ ╟── because: cannot constrain Region[x] <: 'r1
135+
//│ ╟── because: cannot constrain Region[x] <: Region[in 'reg out 'reg1]
135136
//│ ╟── because: cannot constrain x <: 'reg1
137+
//│ ╟── because: cannot constrain x <: 'reg1
138+
//│ ╟── because: cannot constrain x <: 'env
136139
//│ ╟── because: cannot constrain x <: 'env
137140
//│ ╙── because: cannot constrain x <: outer ∨ y
138141
//│ ╔══[ERROR] Type error in region expression with expected type [outer, 'A] -> Int
139-
//│ ║ l.128: (region y in let t = helper(x) in 42) as [A] -> Int
142+
//│ ║ l.129: (region y in let t = helper(x) in 42) as [A] -> Int
140143
//│ ║ ^^^^^^^^^^^^^^^
141144
//│ ╟── because: cannot constrain 'eff <: ⊥
142-
//│ ╟── because: cannot constrain 'eff <: ¬()
143-
//│ ╟── because: cannot constrain ¬'y1 ∧ x <: ¬()
145+
//│ ╟── because: cannot constrain 'eff <: ⊥
146+
//│ ╟── because: cannot constrain ¬'y1 ∧ x <: ⊥
144147
//│ ╟── because: cannot constrain x <: 'y1
145-
//│ ╙── because: cannot constrain x <: ¬()
148+
//│ ╙── because: cannot constrain x <: ⊥
146149
//│ Type: Int
147150

148151

@@ -163,10 +166,10 @@ fun badanno: outer
163166
:e
164167
fun badanno2: [outer A, outer B] -> Int ->{A | B} Int
165168
//│ ╔══[ERROR] Only one outer variable can be bound.
166-
//│ ║ l.164: fun badanno2: [outer A, outer B] -> Int ->{A | B} Int
169+
//│ ║ l.167: fun badanno2: [outer A, outer B] -> Int ->{A | B} Int
167170
//│ ╙── ^^^^^^^^^^^^^^^^^^
168171
//│ ╔══[ERROR] Illegal forall annotation.
169-
//│ ║ l.164: fun badanno2: [outer A, outer B] -> Int ->{A | B} Int
172+
//│ ║ l.167: fun badanno2: [outer A, outer B] -> Int ->{A | B} Int
170173
//│ ╙── ^^^^^^^^^^^^^^^^^^
171174
//│ ═══[ERROR] Invalid type
172175
//│ Type: ⊤
@@ -210,48 +213,49 @@ fun foo(r1) =
210213
fork((_ => r1.ref 1), (_ => r2.ref 2))
211214
foo(r2)
212215
//│ ╔══[ERROR] Type error in function literal
213-
//│ ║ l.208: fun foo(r1) =
216+
//│ ║ l.211: fun foo(r1) =
214217
//│ ║ ^^^^^
215-
//│ ║ l.209: region r2 in
218+
//│ ║ l.212: region r2 in
216219
//│ ║ ^^^^^^^^^^^^^^
217-
//│ ║ l.210: fork((_ => r1.ref 1), (_ => r2.ref 2))
220+
//│ ║ l.213: fork((_ => r1.ref 1), (_ => r2.ref 2))
218221
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
219-
//│ ║ l.211: foo(r2)
222+
//│ ║ l.214: foo(r2)
220223
//│ ║ ^^^^^^^^^^^
221-
//│ ╟── because: cannot constrain 'r1 ->{'eff} 'app <: 'foo
222224
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: 'foo
223-
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: Region[in 'r2 out 'r21] ->{'eff1} 'app1
225+
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: 'foo
226+
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: (Region[in 'r2 out 'r21]) ->{'eff1} ('app1)
224227
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1
225228
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1
226229
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: Region[in 'reg out 'reg1]
227230
//│ ╟── because: cannot constrain 'r21 <: 'reg1
228-
//│ ╟── because: cannot constrain 'r21 <: ¬(¬'reg1)
229-
//│ ╟── because: cannot constrain ¬outer <: ¬(¬'reg1)
231+
//│ ╟── because: cannot constrain 'r21 <: 'reg1
232+
//│ ╟── because: cannot constrain ¬outer <: 'reg1
230233
//│ ╟── because: cannot constrain ¬outer <: 'reg1
231234
//│ ╟── because: cannot constrain ¬outer <: ¬'r22 ∨ outer
232-
//│ ╟── because: cannot constrain 'r22 <: ¬(¬outer)
233-
//│ ╙── because: cannot constrain ¬outer <: ¬(¬outer)
235+
//│ ╟── because: cannot constrain 'r22 <: outer
236+
//│ ╙── because: cannot constrain ¬outer <: outer
234237
//│ ╔══[ERROR] Type error in function literal
235-
//│ ║ l.208: fun foo(r1) =
238+
//│ ║ l.211: fun foo(r1) =
236239
//│ ║ ^^^^^
237-
//│ ║ l.209: region r2 in
240+
//│ ║ l.212: region r2 in
238241
//│ ║ ^^^^^^^^^^^^^^
239-
//│ ║ l.210: fork((_ => r1.ref 1), (_ => r2.ref 2))
242+
//│ ║ l.213: fork((_ => r1.ref 1), (_ => r2.ref 2))
240243
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
241-
//│ ║ l.211: foo(r2)
244+
//│ ║ l.214: foo(r2)
242245
//│ ║ ^^^^^^^^^^^
243-
//│ ╟── because: cannot constrain 'r1 ->{'eff} 'app <: 'foo
244246
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: 'foo
245-
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: Region[in 'r2 out 'r21] ->{'eff1} 'app1
247+
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: 'foo
248+
//│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: (Region[in 'r2 out 'r21]) ->{'eff1} ('app1)
246249
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1
247250
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1
248251
//│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: Region[in 'reg out 'reg1]
249252
//│ ╟── because: cannot constrain 'r21 <: 'reg1
250-
//│ ╟── because: cannot constrain 'r21 <: ¬(¬'reg1)
251-
//│ ╟── because: cannot constrain ¬outer <: ¬(¬'reg1)
253+
//│ ╟── because: cannot constrain 'r21 <: 'reg1
252254
//│ ╟── because: cannot constrain ¬outer <: 'reg1
255+
//│ ╟── because: cannot constrain ¬outer <: 'reg1
256+
//│ ╟── because: cannot constrain ¬outer <: 'reg
253257
//│ ╟── because: cannot constrain ¬outer <: 'reg
254-
//│ ╙── because: cannot constrain ¬outer <: ¬()
258+
//│ ╙── because: cannot constrain ¬outer <: ⊥
255259
//│ Type: ⊤
256260

257261

0 commit comments

Comments
 (0)