From a080994ff4ec5c174d14de2744066065149d5419 Mon Sep 17 00:00:00 2001 From: NeilKleistGao Date: Fri, 20 Dec 2024 15:58:00 +0800 Subject: [PATCH 1/3] Add ticks for tvs --- .../src/main/scala/hkmc2/bbml/types.scala | 4 +- .../src/test/mlscript/bbml/bbBasics.mls | 62 ++++++------- .../src/test/mlscript/bbml/bbBorrowing.mls | 52 +++++------ .../src/test/mlscript/bbml/bbBorrowing2.mls | 8 +- .../src/test/mlscript/bbml/bbBounds.mls | 52 +++++------ .../shared/src/test/mlscript/bbml/bbCheck.mls | 24 ++--- .../src/test/mlscript/bbml/bbCodeGen.mls | 2 +- .../test/mlscript/bbml/bbCyclicExtrude.mls | 40 ++++----- .../src/test/mlscript/bbml/bbErrors.mls | 18 ++-- .../src/test/mlscript/bbml/bbExtrude.mls | 48 +++++----- .../src/test/mlscript/bbml/bbFunGenFix.mls | 2 +- .../shared/src/test/mlscript/bbml/bbFuns.mls | 6 +- .../shared/src/test/mlscript/bbml/bbGPCE.mls | 24 ++--- hkmc2/shared/src/test/mlscript/bbml/bbId.mls | 10 +-- .../test/mlscript/bbml/bbLetRegEncoding.mls | 86 +++++++++--------- .../shared/src/test/mlscript/bbml/bbList.mls | 54 ++++++------ .../src/test/mlscript/bbml/bbOption.mls | 2 +- .../shared/src/test/mlscript/bbml/bbPoly.mls | 46 +++++----- hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls | 42 ++++----- hkmc2/shared/src/test/mlscript/bbml/bbRec.mls | 12 +-- hkmc2/shared/src/test/mlscript/bbml/bbRef.mls | 88 +++++++++---------- .../src/test/mlscript/bbml/bbSelfApp.mls | 4 +- hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls | 56 ++++++------ 23 files changed, 371 insertions(+), 371 deletions(-) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala index 79f73a540..29a1b665e 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala @@ -170,7 +170,7 @@ sealed abstract class BasicType extends Type: if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.show).mkString(", ")}]" case v @ InfVar(lvl, uid, _, isSkolem) => val name = scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.hint)) - if isSkolem then s"<${name}>" else s"${name}" + if isSkolem then s"'<${name}>" else s"'${name}" case FunType(arg :: Nil, ret, eff) => s"${arg.paren} ->${printEff(eff)} ${ret.paren}" case FunType(args, ret, eff) => s"(${args.map(_.show).mkString(", ")}) ->${printEff(eff)} ${ret.paren}" case ComposedType(lhs, rhs, pol) => s"${lhs.paren} ${if pol then "∨" else "∧"} ${rhs.paren}" @@ -183,7 +183,7 @@ sealed abstract class BasicType extends Type: if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]" case v @ InfVar(lvl, uid, _, isSkolem) => val name = if v.hint.isEmpty then s"${v.sym.nme}" else s"${v.sym.nme}(${v.hint})" - if isSkolem then s"<${name}${uid}>_${lvl}" else s"${name}${uid}_${lvl}" + if isSkolem then s"'<${name}${uid}>_${lvl}" else s"'${name}${uid}_${lvl}" case FunType(arg :: Nil, ret, eff) => s"${arg.parenDbg} ->{${eff.showDbg}} ${ret.parenDbg}" case FunType(args, ret, eff) => s"(${args.map(_.showDbg).mkString(", ")}) ->{${eff.showDbg}} ${ret.parenDbg}" case ComposedType(lhs, rhs, pol) => s"${lhs.parenDbg} ${if pol then "∨" else "∧"} ${rhs.parenDbg}" diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls index b66ad5153..f1e1e0c97 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls @@ -20,7 +20,7 @@ false fun id(x) = x id -//│ Type: forall x: x -> x +//│ Type: forall 'x: 'x -> 'x fun inc(x) = x + 1 //│ Type: ⊤ @@ -29,7 +29,7 @@ fun mul(x, y) = x * y //│ Type: ⊤ x => x -//│ Type: (x) ->{⊥} x +//│ Type: ('x) ->{⊥} 'x + //│ Type: (Int, Int) ->{⊥} Int @@ -109,14 +109,14 @@ class Some[A](value: A) //│ Type: ⊤ new Some(true) -//│ Type: Some[A] +//│ Type: Some['A] //│ Where: -//│ Bool <: A +//│ Bool <: 'A new Some(42) -//│ Type: Some[A] +//│ Type: Some['A] //│ Where: -//│ Int <: A +//│ Int <: 'A let p = new Point(1.0, 0.0, 0.0) in p.Point#x //│ Type: Num @@ -150,22 +150,22 @@ fun foofoo(x) = //│ Type: ⊤ new Printer(foofoo) -//│ Type: Printer[T] +//│ Type: Printer['T] //│ Where: -//│ T <: Int +//│ 'T <: Int let ip = new Printer(foofoo) in ip.Printer#f(42) //│ Type: Str :e let ip = new Printer(foofoo) in ip.Printer#f("42") -//│ ╔══[ERROR] Type error in string literal with expected type T +//│ ╔══[ERROR] Type error in string literal with expected type 'T //│ ║ l.161: 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 Str <: T +//│ ╟── because: cannot constrain Str <: 'T +//│ ╟── because: cannot constrain Str <: 'T +//│ ╟── because: cannot constrain Str <: ¬(¬'T) +//│ ╟── because: cannot constrain Str <: 'T //│ ╙── because: cannot constrain Str <: ¬(¬{Int}) //│ Type: Str @@ -176,23 +176,23 @@ fun inc(x) = x + 1 //│ Type: ⊤ new TFun(inc) -//│ Type: TFun[T] +//│ Type: TFun['T] //│ Where: -//│ Int <: T -//│ T <: Int +//│ Int <: 'T +//│ 'T <: Int let tf = new TFun(inc) in tf.TFun#f(1) //│ Type: Int :e let tf = new TFun(inc) in tf.TFun#f("1") -//│ ╔══[ERROR] Type error in string literal with expected type T +//│ ╔══[ERROR] Type error in string literal with expected type 'T //│ ║ l.188: 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 Str <: 'T +//│ ╟── because: cannot constrain Str <: 'T +//│ ╟── because: cannot constrain Str <: ¬(¬'T) +//│ ╟── because: cannot constrain Str <: 'T //│ ╙── because: cannot constrain Str <: ¬(¬{Int}) //│ Type: Str ∨ Int @@ -207,17 +207,17 @@ class Pair[A, B](fst: A, snd: B) new Pair(id, id) -//│ Type: Pair[A, B] +//│ Type: Pair['A, 'B] //│ Where: -//│ x -> x <: A -//│ x1 -> x1 <: B +//│ 'x -> 'x <: 'A +//│ 'x1 -> 'x1 <: 'B new Pair(x => x, x => x) -//│ Type: Pair[A, B] +//│ Type: Pair['A, 'B] //│ Where: -//│ x -> x <: A -//│ x1 -> x1 <: B +//│ 'x -> 'x <: 'A +//│ 'x1 -> 'x1 <: 'B if 1 < 2 then 1 else 0 @@ -276,17 +276,17 @@ class Foo[A](x: A -> A) //│ Type: ⊤ new Foo(x => x) -//│ Type: Foo[A] +//│ Type: Foo['A] fun f(g) = new Foo(g) f -//│ Type: forall A: (A -> A) -> Foo[A] +//│ Type: forall 'A: ('A -> 'A) -> Foo['A] f(x => x).Foo#x -//│ Type: (A) ->{⊥} A +//│ Type: ('A) ->{⊥} 'A g => (new Foo(g)).Foo#x -//│ Type: (A -> A) ->{⊥} (A) ->{⊥} A +//│ Type: ('A -> 'A) ->{⊥} ('A) ->{⊥} 'A throw new Error("oops") diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls index d6a2aa121..aac41b556 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls @@ -36,9 +36,9 @@ fun next: [A, Br] -> Iter[A, Br] ->{Br} A //│ Type: ⊤ letreg(r => r) -//│ Type: Reg[?, E] +//│ Type: Reg[?, 'E] //│ Where: -//│ E <: ⊥ +//│ 'E <: ⊥ letreg of r => let b = mkVec(r) @@ -48,9 +48,9 @@ letreg of r => 123 clear(b) r -//│ Type: Reg[?, E] +//│ Type: Reg[?, 'E] //│ Where: -//│ E <: ⊥ +//│ 'E <: ⊥ // * Non-lexical borrowing pattern encoded with a thunk @@ -90,10 +90,10 @@ letreg of r => //│ ║ ^^^^^^^^^^^^^^^^^^ //│ ║ l.75: k() //│ ║ ^^^^^ -//│ ╟── because: cannot constrain E <: ⊥ -//│ ╟── because: cannot constrain E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ ¬Rg <: ¬() -//│ ╟── because: cannot constrain <: Rg +//│ ╟── because: cannot constrain 'E <: ⊥ +//│ ╟── because: cannot constrain 'E <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ ¬'Rg <: ¬() +//│ ╟── because: cannot constrain <: 'Rg //│ ╙── because: cannot constrain <: ¬() //│ Type: ⊥ @@ -126,15 +126,15 @@ letreg of r => //│ ║ ^^^^^^^^^^ //│ ║ l.109: r //│ ║ ^^^ -//│ ╟── because: cannot constrain E <: ⊥ -//│ ╟── because: cannot constrain E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ Rg <: ¬() -//│ ╟── because: cannot constrain Rg <: ¬() +//│ ╟── because: cannot constrain 'E <: ⊥ +//│ ╟── because: cannot constrain 'E <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬() +//│ ╟── because: cannot constrain 'Rg <: ¬() //│ ╙── because: cannot constrain <: ¬() -//│ Type: Reg[?, E] +//│ Type: Reg[?, 'E] //│ Where: -//│ ⊤ <: E -//│ E <: ⊥ +//│ ⊤ <: 'E +//│ 'E <: ⊥ letreg of r => @@ -143,9 +143,9 @@ letreg of r => next(it) use(r) r -//│ Type: Reg[?, E] +//│ Type: Reg[?, 'E] //│ Where: -//│ E <: ⊥ +//│ 'E <: ⊥ :e letreg of r => @@ -170,15 +170,15 @@ letreg of r => //│ ║ ^^^^^^^^ //│ ║ l.157: r //│ ║ ^^^ -//│ ╟── because: cannot constrain E <: ⊥ -//│ ╟── because: cannot constrain E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ Rg <: ¬() -//│ ╟── because: cannot constrain Rg <: ¬() +//│ ╟── because: cannot constrain 'E <: ⊥ +//│ ╟── because: cannot constrain 'E <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬() +//│ ╟── because: cannot constrain 'Rg <: ¬() //│ ╙── because: cannot constrain <: ¬() -//│ Type: Reg[?, E] +//│ Type: Reg[?, 'E] //│ Where: -//│ ⊤ <: E -//│ E <: ⊥ +//│ ⊤ <: 'E +//│ 'E <: ⊥ letreg of r0 => letreg of r1 => @@ -187,9 +187,9 @@ letreg of r0 => next(it) use(r1) r1 -//│ Type: Reg[?, in E] +//│ Type: Reg[?, in 'E] //│ Where: -//│ E <: ⊥ +//│ 'E <: ⊥ // * Can leak the iterator diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls index 854172d6c..c6c4cefc2 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls @@ -47,10 +47,10 @@ letreg of r => //│ ║ ^^^^^^^^^^^ //│ ║ l.36: write(r) //│ ║ ^^^^^^^^^^ -//│ ╟── because: cannot constrain E <: ⊥ -//│ ╟── because: cannot constrain E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ Rg <: ¬() -//│ ╟── because: cannot constrain Rg <: ¬() +//│ ╟── because: cannot constrain 'E <: ⊥ +//│ ╟── because: cannot constrain 'E <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬() +//│ ╟── because: cannot constrain 'Rg <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls index d78b667b8..dd4df6199 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls @@ -8,33 +8,33 @@ (x => x): [A restricts Int] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ Int <: A +//│ Int <: 'A (x => x - 1): [A extends Int restricts Int] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ Int <: A -//│ A <: Int +//│ Int <: 'A +//│ 'A <: Int fun iid: [A extends Int] -> A -> A fun iid(x) = x //│ Type: ⊤ iid -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ A <: Int +//│ 'A <: Int :e iid("42") -//│ ╔══[ERROR] Type error in string literal with expected type A +//│ ╔══[ERROR] Type error in string literal with expected type 'A //│ ║ l.32: iid("42") //│ ║ ^^^^ -//│ ╟── because: cannot constrain Str <: A -//│ ╟── because: cannot constrain Str <: A +//│ ╟── because: cannot constrain Str <: 'A +//│ ╟── because: cannot constrain Str <: 'A //│ ╙── because: cannot constrain Str <: Int //│ Type: Str @@ -47,10 +47,10 @@ class Foo[A] fun foo: [A extends Foo[in Nothing out Any] restricts Foo[in Num]] -> A -> A foo -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ Foo[in Num] <: A -//│ A <: Foo[?] +//│ Foo[in Num] <: 'A +//│ 'A <: Foo[?] fun bar: Foo[in Num out Int] //│ Type: ⊤ @@ -73,7 +73,7 @@ baz fun bazbaz: [A extends Int] -> A -> [B extends A] -> B bazbaz -//│ Type: (Int) ->{⊥} forall B: ⊥ +//│ Type: (Int) ->{⊥} forall 'B: ⊥ fun foofun: [A extends Int -> Int restricts Any -> Int] -> A -> Int -> Int foofun @@ -84,21 +84,21 @@ foofun(x => x + 1)(42) fun bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A bazbaz -//│ Type: forall A: (A) ->{⊥} (forall B: A -> A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} (forall 'B: 'A -> 'A) ->{⊥} 'A //│ Where: -//│ A <: Int +//│ 'A <: Int bazbaz(42)(x => x + 1) //│ Type: Int fun cc: [A extends B -> B restricts B -> B, B extends A -> A restricts A -> A] -> A -> B -> Bool cc -//│ Type: forall A, B: (A) ->{⊥} (B) ->{⊥} Bool +//│ Type: forall 'A, 'B: ('A) ->{⊥} ('B) ->{⊥} Bool //│ Where: -//│ A -> A <: B -//│ B <: A -> A -//│ B -> B <: A -//│ A <: B -> B +//│ 'A -> 'A <: 'B +//│ 'B <: 'A -> 'A +//│ 'B -> 'B <: 'A +//│ 'A <: 'B -> 'B fun w: Any -> Nothing //│ Type: ⊤ @@ -111,18 +111,18 @@ fun h: [C] -> ([A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B :e bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A -//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as () ->{⊥} (forall B: B) ->{⊥} +//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as (') ->{⊥} (forall 'B: 'B) ->{⊥} ' //│ ║ l.113: bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A //│ ╙── ^^^^^^ -//│ Type: forall A: (A) ->{⊥} (forall B: A -> A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} (forall 'B: 'A -> 'A) ->{⊥} 'A //│ Where: -//│ A <: Int +//│ 'A <: Int (x => f => bazbaz(x)(f)): [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A -//│ Type: forall A: (A) ->{⊥} (forall B: A -> A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} (forall 'B: 'A -> 'A) ->{⊥} 'A //│ Where: -//│ A <: Int +//│ 'A <: Int h(x => f => bazbaz(x)(f))(42) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls index fc72fcc91..dbafab0d8 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls @@ -78,7 +78,7 @@ fun high(f) = f(42) //│ Type: ⊤ high -//│ Type: (forall A: (A) ->{⊥} A) ->{⊥} Int +//│ Type: (forall 'A: ('A) ->{⊥} 'A) ->{⊥} Int high((x => x): [A] -> A -> A) @@ -92,19 +92,19 @@ high(x => x + 1) //│ ╔══[ERROR] Type error in reference with expected type Int //│ ║ l.91: high(x => x + 1) //│ ║ ^ -//│ ╙── because: cannot constrain <: Int -//│ ╔══[ERROR] Type error in application with expected type +//│ ╙── because: cannot constrain ' <: Int +//│ ╔══[ERROR] Type error in application with expected type ' //│ ║ l.91: high(x => x + 1) //│ ║ ^^^^^ -//│ ╙── because: cannot constrain Int <: +//│ ╙── because: cannot constrain Int <: ' //│ Type: Int (let a = 0 in x => x): [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A (if false then x => x else y => y): [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A fun baz: Int -> (([A] -> A -> A), Int) -> Int @@ -119,24 +119,24 @@ fun baz(z) = :e baz: Int -> (([A] -> A -> A), Int) -> Int -//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#18),Ident(baz)) as (Int) ->{⊥} (forall A: (A) ->{⊥} A, Int) ->{⊥} Int +//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#18),Ident(baz)) as (Int) ->{⊥} (forall 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int //│ ║ l.121: baz: Int -> (([A] -> A -> A), Int) -> Int //│ ╙── ^^^ //│ Type: ⊥ baz(42) -//│ Type: (forall A: (A) ->{⊥} A, Int) ->{⊥} Int +//│ Type: (forall 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int :e baz(42): (([A] -> A -> A), Int) -> Int -//│ ╔══[ERROR] Cannot type non-function term App(SynthSel(Ref(globalThis:block#18),Ident(baz)),Tup(List(Fld(‹›,Lit(IntLit(42)),None)))) as (forall A: (A) ->{⊥} A, Int) ->{⊥} Int +//│ ╔══[ERROR] Cannot type non-function term App(SynthSel(Ref(globalThis:block#18),Ident(baz)),Tup(List(Fld(‹›,Lit(IntLit(42)),None)))) as (forall 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int //│ ║ l.132: baz(42): (([A] -> A -> A), Int) -> Int //│ ╙── ^^^^^^^ //│ Type: ⊥ (z => (f, x) => baz(z)(f, x)): Int -> (([A] -> A -> A), Int) -> Int -//│ Type: (Int) ->{⊥} (forall A: (A) ->{⊥} A, Int) ->{⊥} Int +//│ Type: (Int) ->{⊥} (forall 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int fun id: [A] -> A -> A @@ -144,11 +144,11 @@ fun id(x) = x //│ Type: ⊤ id: [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A (id: [A] -> A -> A): [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A 42: Int | Num //│ Type: Int ∨ Num diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCodeGen.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCodeGen.mls index b7ece7e2e..be711fb10 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCodeGen.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCodeGen.mls @@ -54,7 +54,7 @@ false //│ JS (unsanitized): //│ (x) => { return x; } //│ = [Function (anonymous)] -//│ Type: forall T: (T) ->{⊥} T +//│ Type: forall 'T: ('T) ->{⊥} 'T :sjs diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls index c01bd9133..0a39f1e4f 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls @@ -5,57 +5,57 @@ let f = (x => (x : [A] -> A -> A)) in f -//│ Type: (⊤ -> ⊥) ->{⊥} forall A: (A) ->{⊥} A +//│ Type: (⊤ -> ⊥) ->{⊥} forall 'A: ('A) ->{⊥} 'A let f = ((x => x) : [A] -> A -> A) in f -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A let foo = f => (x => f(x(x)) : [A] -> A -> A) in foo -//│ Type: (app -> (⊤ -> ⊥)) ->{⊥} (x -> app) ->{⊥} forall A: (A) ->{⊥} A +//│ Type: ('app -> (⊤ -> ⊥)) ->{⊥} ('x -> 'app) ->{⊥} forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ x <: x -> app +//│ 'x <: 'x -> 'app f => (let g = x => x(x) in f(g(g))) : [A] -> A -> A -//│ Type: (⊥ -> (⊤ -> ⊥)) ->{⊥} forall A: (A) ->{⊥} A +//│ Type: (⊥ -> (⊤ -> ⊥)) ->{⊥} forall 'A: ('A) ->{⊥} 'A :e f => (let g = x => f(x(x)) in g) : [A] -> A -> A -//│ ╔══[ERROR] Type error in block with expected type () ->{⊥} +//│ ╔══[ERROR] Type error in block with expected type (') ->{⊥} ' //│ ║ l.22: f => (let g = x => f(x(x)) in g) : [A] -> A -> A //│ ║ ^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain x ->{eff ∨ eff1} app <: -> -//│ ╟── because: cannot constrain <: x -//│ ╟── because: cannot constrain <: x -//│ ╙── because: cannot constrain <: ¬(¬{x ->{eff1} app1}) -//│ Type: (⊥ -> ⊥) ->{⊥} forall A: (A) ->{⊥} A +//│ ╟── because: cannot constrain 'x ->{'eff ∨ 'eff1} 'app <: ' -> ' +//│ ╟── because: cannot constrain ' <: 'x +//│ ╟── because: cannot constrain ' <: 'x +//│ ╙── because: cannot constrain ' <: ¬(¬{'x ->{'eff1} 'app1}) +//│ Type: (⊥ -> ⊥) ->{⊥} forall 'A: ('A) ->{⊥} 'A f => (x => f(x(x)) : [A] -> A -> A) -//│ Type: (app -> (⊤ -> ⊥)) ->{⊥} (x -> app) ->{⊥} forall A: (A) ->{⊥} A +//│ Type: ('app -> (⊤ -> ⊥)) ->{⊥} ('x -> 'app) ->{⊥} forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ x <: x -> app +//│ 'x <: 'x -> 'app let foo = f => (f(x => x(x)) : [A] -> A -> A) in foo -//│ Type: (((x ->{eff} app) ->{eff} app) -> (⊤ -> ⊥)) ->{⊥} forall A: (A) ->{⊥} A +//│ Type: ((('x ->{'eff} 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ x <: x ->{eff} app +//│ 'x <: 'x ->{'eff} 'app :todo let foo(f) = (f(x => x(x)) : [A] -> A -> A) in foo -//│ Type: (((x ->{eff} app) ->{eff} app) -> (⊤ -> ⊥)) ->{⊥} forall A: (A) ->{⊥} A +//│ Type: ((('x ->{'eff} 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ x <: x ->{eff} app +//│ 'x <: 'x ->{'eff} 'app :todo fun foo(f) = (f(x => x(x)) : [A] -> A -> A) -//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (f) ->{⊥} forall A: (A) ->{⊥} A found +//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but ('f) ->{⊥} forall 'A: ('A) ->{⊥} 'A found //│ ║ l.49: fun foo(f) = (f(x => x(x)) : [A] -> A -> A) //│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ Type: ⊤ f => (let g = x => x(x) in let tmp = g(g) in f(g)) : [A] -> A -> A -//│ Type: ((((x ∨ (x ->{eff} app)) -> app) ->{eff} app) -> (⊤ -> ⊥)) ->{⊥} forall A: (A) ->{⊥} A +//│ Type: (((('x ∨ ('x ->{'eff} 'app)) -> 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ x <: (x ∨ (x ->{eff} app)) -> app +//│ 'x <: ('x ∨ ('x ->{'eff} 'app)) -> 'app diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls b/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls index 23ef7b5c4..e2a4d2040 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls @@ -8,16 +8,16 @@ //│ ╔══[ERROR] Type error in application //│ ║ l.7: 2(2) //│ ║ ^^^^ -//│ ╙── because: cannot constrain Int <: Int ->{eff} app +//│ ╙── because: cannot constrain Int <: Int ->{'eff} 'app //│ Type: ⊥ (x => x(0))(1) -//│ ╔══[ERROR] Type error in integer literal with expected type x +//│ ╔══[ERROR] Type error in integer literal with expected type 'x //│ ║ l.14: (x => x(0))(1) //│ ║ ^ -//│ ╟── because: cannot constrain Int <: x -//│ ╟── because: cannot constrain Int <: x -//│ ╙── because: cannot constrain Int <: ¬(¬{Int ->{eff} app}) +//│ ╟── because: cannot constrain Int <: 'x +//│ ╟── because: cannot constrain Int <: 'x +//│ ╙── because: cannot constrain Int <: ¬(¬{Int ->{'eff} 'app}) //│ Type: ⊥ (1).Foo#a() @@ -30,11 +30,11 @@ fun inc(x) = x + 1 inc("oops") -//│ ╔══[ERROR] Type error in string literal with expected type x +//│ ╔══[ERROR] Type error in string literal with expected type 'x //│ ║ l.32: inc("oops") //│ ║ ^^^^^^ -//│ ╟── because: cannot constrain Str <: x -//│ ╟── because: cannot constrain Str <: x +//│ ╟── because: cannot constrain Str <: 'x +//│ ╟── because: cannot constrain Str <: 'x //│ ╙── because: cannot constrain Str <: ¬¬Int //│ Type: Int @@ -43,7 +43,7 @@ inc : Int //│ ╔══[ERROR] Type error in selection with expected type Int //│ ║ l.42: inc : Int //│ ║ ^^^ -//│ ╙── because: cannot constrain x -> Int <: Int +//│ ╙── because: cannot constrain 'x -> Int <: Int //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls index 06575b832..82ba2bbfc 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls @@ -8,9 +8,9 @@ fun f(y) = // * the parameter type of y is extruded. f -//│ Type: forall y: y -> y +//│ Type: forall 'y: 'y -> 'y //│ Where: -//│ y <: ⊤ -> Int +//│ 'y <: ⊤ -> Int fun foo: [A] -> A -> Int fun foo(x) = 0 @@ -28,25 +28,25 @@ fun g(y) = //│ Type: ⊤ g -//│ Type: (forall A: (⊥) ->{⊥} Int) ->{⊥} forall A: (⊤) ->{⊥} Int +//│ Type: (forall 'A: (⊥) ->{⊥} Int) ->{⊥} forall 'A: (⊤) ->{⊥} Int g(foo) //│ Type: (⊤) ->{⊥} Int :e y `=> (let t = run(x `=> x `+ y) in y) -//│ ╔══[ERROR] Type error in quoted term with expected type CodeBase[out T, ⊥, ?] +//│ ╔══[ERROR] Type error in quoted term with expected type CodeBase[out 'T, ⊥, ?] //│ ║ l.37: y `=> (let t = run(x `=> x `+ y) in y) //│ ║ ^^^^^^^^^^^^ -//│ ╟── because: cannot constrain CodeBase[out x -> cde, out ctx, ?] <: CodeBase[out T, ⊥, ?] -//│ ╟── because: cannot constrain ctx <: ⊥ -//│ ╟── because: cannot constrain ctx <: ¬() -//│ ╟── because: cannot constrain (¬⊥ ∧ ¬x) ∧ <: ¬() -//│ ╟── because: cannot constrain <: x -//│ ╙── because: cannot constrain <: ¬() -//│ Type: CodeBase[out y -> y, ⊥, ?] +//│ ╟── because: cannot constrain CodeBase[out 'x -> 'cde, out 'ctx, ?] <: CodeBase[out 'T, ⊥, ?] +//│ ╟── because: cannot constrain 'ctx <: ⊥ +//│ ╟── because: cannot constrain 'ctx <: ¬() +//│ ╟── because: cannot constrain (¬⊥ ∧ ¬'x) ∧ ' <: ¬() +//│ ╟── because: cannot constrain ' <: 'x +//│ ╙── because: cannot constrain ' <: ¬() +//│ Type: CodeBase[out 'y -> 'y, ⊥, ?] //│ Where: -//│ y <: Int +//│ 'y <: Int class C[A](m: A, n: A -> Int) //│ Type: ⊤ @@ -54,11 +54,11 @@ class C[A](m: A, n: A -> Int) fun f: [A] -> ([B] -> (C[out B] & A) -> B) -> A -> Int f -//│ Type: forall A: (forall B: (C[out B] ∧ A) ->{⊥} B) ->{⊥} (A) ->{⊥} Int +//│ Type: forall 'A: (forall 'B: (C[out 'B] ∧ 'A) ->{⊥} 'B) ->{⊥} ('A) ->{⊥} Int fun g: [D] -> C[in Int out D] -> D g -//│ Type: forall D: (C[in Int out D]) ->{⊥} D +//│ Type: forall 'D: (C[in Int out 'D]) ->{⊥} 'D f(g) @@ -77,17 +77,17 @@ f(g)(foo) :fixme // ??? f(g)(bar) -//│ ╔══[ERROR] Type error in selection with expected type A +//│ ╔══[ERROR] Type error in selection with expected type 'A //│ ║ l.79: f(g)(bar) //│ ║ ^^^ -//│ ╟── because: cannot constrain C[Int] <: A -//│ ╟── because: cannot constrain C[in Int out Int] <: A -//│ ╟── because: cannot constrain C[in Int out Int] <: ¬C[in ⊥ out ¬⊥ ∧ B] ∨ C[in Int out ¬⊥ ∧ D] -//│ ╟── because: cannot constrain (Int) ∧ (B) <: ¬⊥ ∧ D -//│ ╟── because: cannot constrain Int ∧ B <: D -//│ ╟── because: cannot constrain Int ∧ B <: B -//│ ╟── because: cannot constrain Int ∧ B <: B -//│ ╟── because: cannot constrain Int ∧ B <: ¬() -//│ ╟── because: cannot constrain B <: ¬(Int) +//│ ╟── because: cannot constrain C[Int] <: 'A +//│ ╟── because: cannot constrain C[in Int out Int] <: 'A +//│ ╟── because: cannot constrain C[in Int out Int] <: ¬C[in ⊥ out ¬⊥ ∧ 'B] ∨ C[in Int out ¬⊥ ∧ 'D] +//│ ╟── because: cannot constrain (Int) ∧ ('B) <: ¬⊥ ∧ 'D +//│ ╟── because: cannot constrain Int ∧ 'B <: 'D +//│ ╟── because: cannot constrain Int ∧ 'B <: 'B +//│ ╟── because: cannot constrain Int ∧ 'B <: 'B +//│ ╟── because: cannot constrain Int ∧ 'B <: ¬() +//│ ╟── because: cannot constrain 'B <: ¬(Int) //│ ╙── because: cannot constrain <: ¬(Int) //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls b/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls index 1ef0c4d68..b288fa11d 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls @@ -31,7 +31,7 @@ fun helper(a) = write(a) //│ Type: ⊤ helper -//│ Type: forall Rg: Reg[out Rg, ?] ->{Rg} Int +//│ Type: forall 'Rg: Reg[out 'Rg, ?] ->{'Rg} Int subreg(basereg) of r0 => helper(r0) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls b/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls index 1b24fb99e..0dd7ab661 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls @@ -5,7 +5,7 @@ fun f(x, y) = x(y) f -//│ Type: forall y, eff, app: (y ->{eff} app, y) ->{eff} app +//│ Type: forall 'y, 'eff, 'app: ('y ->{'eff} 'app, 'y) ->{'eff} 'app f((x => x), 42) @@ -19,9 +19,9 @@ fun id: [A] -> A -> A //│ Type: ⊤ id : [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A id(id) : [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls index aa0c8b067..7a50a58bd 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls @@ -8,7 +8,7 @@ fun power(x) = case 0 then `1.0 n then x `*. power(x)(n - 1) power -//│ Type: forall C: (CodeBase[out Num, out C, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Num, out C, ?] +//│ Type: forall 'C: (CodeBase[out Num, out 'C, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Num, out 'C, ?] fun id: [A] -> A -> A @@ -38,7 +38,7 @@ show fun inc(dbg) = x `=> let c = x `+ `1 in let t = dbg(c) in c inc -//│ Type: forall eff: (CodeBase[out Int, ?, ?] ->{eff} ⊤) ->{eff} CodeBase[out Int -> Int, ⊥, ?] +//│ Type: forall 'eff: (CodeBase[out Int, ?, ?] ->{'eff} ⊤) ->{'eff} CodeBase[out Int -> Int, ⊥, ?] inc(c => log(show(c))) //│ Type: CodeBase[out Int -> Int, ⊥, ?] @@ -56,7 +56,7 @@ let gn5 = run(gib_naive(5)) fun bind(rhs, k) = `let x = rhs `in k(x) bind -//│ Type: forall cde, ctx, cde, eff, cde1, ctx1: (CodeBase[out cde, out ctx, ?], CodeBase[in cde out cde ∨ cde, ?, ⊥] ->{eff} CodeBase[out cde1, out ctx1, ?]) ->{eff} CodeBase[out cde1, out ctx ∨ ctx1, ?] +//│ Type: forall 'cde, 'ctx, 'cde, 'eff, 'cde1, 'ctx1: (CodeBase[out 'cde, out 'ctx, ?], CodeBase[in 'cde out 'cde ∨ 'cde, ?, ⊥] ->{'eff} CodeBase[out 'cde1, out 'ctx1, ?]) ->{'eff} CodeBase[out 'cde1, out 'ctx ∨ 'ctx1, ?] :e fun body: [G] -> (CodeBase[out Int, out G, out Any], CodeBase[out Int, out G, out Any]) -> Int -> CodeBase[out Int, out G, out Any] @@ -64,21 +64,21 @@ fun body(x, y) = case 0 then x 1 then y n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out C, out Any] -//│ ╔══[ERROR] Type error in application with expected type CodeBase[out Int, out , ?] +//│ ╔══[ERROR] Type error in application with expected type CodeBase[out Int, out ', ?] //│ ║ l.66: n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out C, out Any] //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain CodeBase[out cde, out ctx ∨ ctx1, ?] <: CodeBase[out Int, out , ?] -//│ ╟── because: cannot constrain ctx ∨ ctx1 <: -//│ ╟── because: cannot constrain ctx1 <: ¬(¬) -//│ ╟── because: cannot constrain ctx2 <: ¬(¬) -//│ ╟── because: cannot constrain ctx2 <: ¬(¬) -//│ ╙── because: cannot constrain <: ¬(¬) +//│ ╟── because: cannot constrain CodeBase[out 'cde, out 'ctx ∨ 'ctx1, ?] <: CodeBase[out Int, out ', ?] +//│ ╟── because: cannot constrain 'ctx ∨ 'ctx1 <: ' +//│ ╟── because: cannot constrain 'ctx1 <: ¬(¬') +//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬') +//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬') +//│ ╙── because: cannot constrain <: ¬(¬') //│ Type: ⊤ fun bind: [G] -> (CodeBase[out Int, out G, out Any], [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C | G, out Any]) -> CodeBase[out Int, out G, out Any] fun bind(rhs, k) = `let x = rhs `in k(x) bind -//│ Type: forall G: (CodeBase[out Int, out G, ?], forall C: (CodeBase[out Int, out C, ?]) ->{⊥} CodeBase[out Int, out C ∨ G, ?]) ->{⊥} CodeBase[out Int, out G, ?] +//│ Type: forall 'G: (CodeBase[out Int, out 'G, ?], forall 'C: (CodeBase[out Int, out 'C, ?]) ->{⊥} CodeBase[out Int, out 'C ∨ 'G, ?]) ->{⊥} CodeBase[out Int, out 'G, ?] fun body: [G] -> (CodeBase[out Int, out G, out Any], CodeBase[out Int, out G, out Any]) -> Int -> CodeBase[out Int, out G, out Any] @@ -87,7 +87,7 @@ fun body(x, y) = case 1 then y n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C, out Any] body -//│ Type: forall G: (CodeBase[out Int, out G, ?], CodeBase[out Int, out G, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Int, out G, ?] +//│ Type: forall 'G: (CodeBase[out Int, out 'G, ?], CodeBase[out Int, out 'G, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Int, out 'G, ?] fun gib(n) = (x, y) `=> body(x, y)(n) let g5 = run(gib(5)) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbId.mls b/hkmc2/shared/src/test/mlscript/bbml/bbId.mls index 04d941f9c..7cd08a05e 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbId.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbId.mls @@ -10,28 +10,28 @@ id(1) //│ Type: Int id -//│ Type: forall x: x -> x +//│ Type: forall 'x: 'x -> 'x id(true) //│ Type: Bool id -//│ Type: forall x: x -> x +//│ Type: forall 'x: 'x -> 'x fun id(x) = x //│ Type: ⊤ id : [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A (y => y) : [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A fun id(x) = x (y => id(y)) : [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls index b552ae973..5c4d53386 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls @@ -8,7 +8,7 @@ fun letreg: [E,Res] -> ([R] -> Region[R] ->{E | R} Res) ->{E} Res //│ Type: ⊤ letreg -//│ Type: forall E, Res: (forall R: (Region[R]) ->{E ∨ R} Res) ->{E} Res +//│ Type: forall 'E, 'Res: (forall 'R: (Region['R]) ->{'E ∨ 'R} 'Res) ->{'E} 'Res letreg(r => r) //│ Type: Region[?] @@ -18,23 +18,23 @@ letreg(r => r).ref 1 //│ ╔══[ERROR] Type error in reference creation //│ ║ l.17: letreg(r => r).ref 1 //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Res <: Region[reg] -//│ ╟── because: cannot constrain Res <: ¬(¬{Region[reg]}) -//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ R out ¬⊥ ∧ R] ∧ ¬⊥ <: ¬(¬{Region[reg]}) -//│ ╟── because: cannot constrain R <: reg -//│ ╟── because: cannot constrain R <: reg -//│ ╟── because: cannot constrain R <: ¬(¬R) -//│ ╟── because: cannot constrain R <: ¬(¬R) -//│ ╟── because: cannot constrain <: ¬(¬R) -//│ ╟── because: cannot constrain <: R +//│ ╟── because: cannot constrain 'Res <: Region['reg] +//│ ╟── because: cannot constrain 'Res <: ¬(¬{Region['reg]}) +//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'R out ¬⊥ ∧ 'R] ∧ ¬⊥ <: ¬(¬{Region['reg]}) +//│ ╟── because: cannot constrain 'R <: 'reg +//│ ╟── because: cannot constrain 'R <: 'reg +//│ ╟── because: cannot constrain 'R <: ¬(¬'R) +//│ ╟── because: cannot constrain 'R <: ¬(¬'R) +//│ ╟── because: cannot constrain <: ¬(¬'R) +//│ ╟── because: cannot constrain <: 'R //│ ╙── because: cannot constrain <: ¬() //│ ╔══[ERROR] Type error in block //│ ║ l.17: letreg(r => r).ref 1 //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain reg ∨ E <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain R <: ¬() -//│ ╟── because: cannot constrain R <: ¬() +//│ ╟── because: cannot constrain 'reg ∨ 'E <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain 'R <: ¬() +//│ ╟── because: cannot constrain 'R <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Ref[Int, ?] @@ -49,12 +49,12 @@ letreg(r => !(r.ref 1)) //│ ╔══[ERROR] Type error in block //│ ║ l.48: !letreg(r => r.ref 1) //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain reg ∨ E <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ R <: ¬() -//│ ╟── because: cannot constrain R <: ¬() +//│ ╟── because: cannot constrain 'reg ∨ 'E <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'R <: ¬() +//│ ╟── because: cannot constrain 'R <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -68,23 +68,23 @@ let f = letreg(r => arg => r.ref arg) //│ Type: ⊤ f -//│ Type: arg ->{⊤} Ref[arg, ?] +//│ Type: 'arg ->{⊤} Ref['arg, ?] :e letreg(r => arg => r.ref arg)(0) //│ ╔══[ERROR] Type error in block //│ ║ l.74: letreg(r => arg => r.ref arg)(0) //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain eff ∨ E <: ⊥ -//│ ╟── because: cannot constrain eff <: ¬() -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ R <: ¬() -//│ ╟── because: cannot constrain R <: ¬() +//│ ╟── because: cannot constrain 'eff ∨ 'E <: ⊥ +//│ ╟── because: cannot constrain 'eff <: ¬() +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'R <: ¬() +//│ ╟── because: cannot constrain 'R <: ¬() //│ ╙── because: cannot constrain <: ¬() -//│ Type: Ref[arg, ?] +//│ Type: Ref['arg, ?] //│ Where: -//│ Int <: arg +//│ Int <: 'arg @@ -95,30 +95,30 @@ fun letreg: [E,Res] -> ([R] -> Region[R] -> Res) ->{E} Res :e letreg(r => r.ref 1) -//│ ╔══[ERROR] Type error in function literal with expected type (Region[]) ->{⊥} Res +//│ ╔══[ERROR] Type error in function literal with expected type (Region[']) ->{⊥} 'Res //│ ║ l.97: letreg(r => r.ref 1) //│ ║ ^^^^^^^^^^^^ -//│ ╟── because: cannot constrain reg <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╙── because: cannot constrain <: ¬() +//│ ╟── because: cannot constrain 'reg <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╙── because: cannot constrain ' <: ¬() //│ Type: Ref[Int, ?] :e letreg(r => !(r.ref 1)) -//│ ╔══[ERROR] Type error in function literal with expected type (Region[]) ->{⊥} Res +//│ ╔══[ERROR] Type error in function literal with expected type (Region[']) ->{⊥} 'Res //│ ║ l.107: letreg(r => !(r.ref 1)) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain reg ∨ reg1 <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╙── because: cannot constrain <: ¬() -//│ ╔══[ERROR] Type error in function literal with expected type (Region[]) ->{⊥} Res +//│ ╟── because: cannot constrain 'reg ∨ 'reg1 <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╙── because: cannot constrain ' <: ¬() +//│ ╔══[ERROR] Type error in function literal with expected type (Region[']) ->{⊥} 'Res //│ ║ l.107: letreg(r => !(r.ref 1)) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain reg ∨ reg1 <: ⊥ -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╙── because: cannot constrain <: ¬() +//│ ╟── because: cannot constrain 'reg ∨ 'reg1 <: ⊥ +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╙── because: cannot constrain ' <: ¬() //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls index 2abc6d6ae..2d065c0fe 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls @@ -51,7 +51,7 @@ fun mapi = s => f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ) ->{} ) ->{} List[out ] +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ') ->{'} ') ->{'} List[out '] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -60,15 +60,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain f ->{E1} List[out B] <: ((Int, ) ->{} ) ->{} List[out ] -//│ ╟── because: cannot constrain E1 <: -//│ ╟── because: cannot constrain E1 <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ reg <: ¬(¬) -//│ ╟── because: cannot constrain reg <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ r <: ¬(¬) -//│ ╟── because: cannot constrain r <: ¬(¬) -//│ ╙── because: cannot constrain <: ¬(¬) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ) ->{} ) ->{} List[out ] +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, ') ->{'} ') ->{'} List[out '] +//│ ╟── because: cannot constrain 'E1 <: ' +//│ ╟── because: cannot constrain 'E1 <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') +//│ ╟── because: cannot constrain 'reg <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') +//│ ╟── because: cannot constrain 'r <: ¬(¬') +//│ ╙── because: cannot constrain <: ¬(¬') +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ') ->{'} ') ->{'} List[out '] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -77,15 +77,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain f ->{E1} List[out B] <: ((Int, ) ->{} ) ->{} List[out ] -//│ ╟── because: cannot constrain E1 <: -//│ ╟── because: cannot constrain E1 <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ reg <: ¬(¬) -//│ ╟── because: cannot constrain reg <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ r <: ¬(¬) -//│ ╟── because: cannot constrain r <: ¬(¬) -//│ ╙── because: cannot constrain <: ¬(¬) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ) ->{} ) ->{} List[out ] +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, ') ->{'} ') ->{'} List[out '] +//│ ╟── because: cannot constrain 'E1 <: ' +//│ ╟── because: cannot constrain 'E1 <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') +//│ ╟── because: cannot constrain 'reg <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') +//│ ╟── because: cannot constrain 'r <: ¬(¬') +//│ ╙── because: cannot constrain <: ¬(¬') +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ') ->{'} ') ->{'} List[out '] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -94,14 +94,14 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain f ->{E1} List[out B] <: ((Int, ) ->{} ) ->{} List[out ] -//│ ╟── because: cannot constrain E1 <: -//│ ╟── because: cannot constrain E1 <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ reg <: ¬(¬) -//│ ╟── because: cannot constrain reg <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ r <: ¬(¬) -//│ ╟── because: cannot constrain r <: ¬(¬) -//│ ╙── because: cannot constrain <: ¬(¬) +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, ') ->{'} ') ->{'} List[out '] +//│ ╟── because: cannot constrain 'E1 <: ' +//│ ╟── because: cannot constrain 'E1 <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') +//│ ╟── because: cannot constrain 'reg <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') +//│ ╟── because: cannot constrain 'r <: ¬(¬') +//│ ╙── because: cannot constrain <: ¬(¬') //│ Type: ⊤ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls b/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls index 5fd02827c..aa6444334 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls @@ -7,7 +7,7 @@ class Option[out A](inspect: [E, Res] -> (() ->{E} Res, A ->{E} Res) ->{E} Res) //│ Type: ⊤ opt => opt.Option#inspect -//│ Type: (Option[out A]) ->{⊥} forall E, Res: (() ->{E} Res, (A) ->{E} Res) ->{E} Res +//│ Type: (Option[out 'A]) ->{⊥} forall 'E, 'Res: (() ->{'E} 'Res, ('A) ->{'E} 'Res) ->{'E} 'Res opt => opt.Option#inspect( () => 42 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls index cd0bc4567..23df7f1c5 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls @@ -19,26 +19,26 @@ fun id(x) = x //│ Type: ⊤ id -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A :e (x => x + 1): [A] -> A -> A //│ ╔══[ERROR] Type error in reference with expected type Int //│ ║ l.25: (x => x + 1): [A] -> A -> A //│ ║ ^ -//│ ╙── because: cannot constrain <: Int -//│ ╔══[ERROR] Type error in application with expected type +//│ ╙── because: cannot constrain ' <: Int +//│ ╔══[ERROR] Type error in application with expected type ' //│ ║ l.25: (x => x + 1): [A] -> A -> A //│ ║ ^^^^^ -//│ ╙── because: cannot constrain Int <: -//│ Type: forall A: (A) ->{⊥} A +//│ ╙── because: cannot constrain Int <: ' +//│ Type: forall 'A: ('A) ->{⊥} 'A (x => x): [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A id: [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A id: Int -> Int //│ Type: (Int) ->{⊥} Int @@ -50,7 +50,7 @@ myInc(id, 0) //│ Type: Int let t = 42 in ((x => x): [A] -> A -> A) -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A id(42) @@ -64,10 +64,10 @@ class Pair[A, B](a: A, b: B) //│ Type: ⊤ new Pair(42, true) -//│ Type: Pair[A, B] +//│ Type: Pair['A, 'B] //│ Where: -//│ Int <: A -//│ Bool <: B +//│ Int <: 'A +//│ Bool <: 'B fun swap: [A, B] -> Pair[out A, out B] -> Pair[out B, out A] fun swap(p) = new Pair(p.Pair#b, p.Pair#a) @@ -75,7 +75,7 @@ fun swap(p) = new Pair(p.Pair#b, p.Pair#a) swap -//│ Type: forall A, B: (Pair[out A, out B]) ->{⊥} Pair[out B, out A] +//│ Type: forall 'A, 'B: (Pair[out 'A, out 'B]) ->{⊥} Pair[out 'B, out 'A] let t = new Pair(42, true) in swap(t) //│ Type: Pair[out Bool, out Int] @@ -84,17 +84,17 @@ let t = new Pair("114", "514") in swap(t) //│ Type: Pair[out Str, out Str] let id = ((x => x): [A] -> A -> A) in new Pair(id(42), id("42")) -//│ Type: Pair[A, B] +//│ Type: Pair['A, 'B] //│ Where: -//│ Int <: A -//│ Str <: B +//│ Int <: 'A +//│ Str <: 'B fun foo: ([A] -> A -> A) -> Int fun foo(x) = 42 //│ Type: ⊤ foo -//│ Type: (forall A: (A) ->{⊥} A) ->{⊥} Int +//│ Type: (forall 'A: ('A) ->{⊥} 'A) ->{⊥} Int foo(id) //│ Type: Int @@ -120,9 +120,9 @@ class Bar[A](x: A, f: [B] -> B -> B) new Bar(0, id) -//│ Type: Bar[A] +//│ Type: Bar['A] //│ Where: -//│ Int <: A +//│ Int <: 'A let bar = new Bar(0, id) in bar.Bar#f(bar.Bar#x) //│ Type: Int @@ -131,9 +131,9 @@ class Some[A](value: A) //│ Type: ⊤ new Some((x => x): [A] -> A -> A) -//│ Type: Some[A] +//│ Type: Some['A] //│ Where: -//│ x -> x <: A +//│ 'x -> 'x <: 'A let s = new Some((x => x): [A] -> A -> A) in let t = s.Some#value(42) in s.Some#value(false) //│ Type: Bool ∨ Int @@ -144,11 +144,11 @@ fun gen(x) = //│ Type: ⊤ gen -//│ Type: (Int) ->{⊥} forall A: (A) ->{⊥} A +//│ Type: (Int) ->{⊥} forall 'A: ('A) ->{⊥} 'A gen(42) -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A // FIXME: toLoc :fixme @@ -164,4 +164,4 @@ fun cnt(x) = 42 //│ Type: ⊤ (x => x): [A] -> A -> A -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls index b632bfff2..dabf0f154 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls @@ -21,7 +21,7 @@ x `=> x -//│ Type: CodeBase[out x -> x, ⊥, ?] +//│ Type: CodeBase[out 'x -> 'x, ⊥, ?] x `=> `42 //│ Type: CodeBase[out ⊤ -> Int, ⊥, ?] @@ -31,12 +31,12 @@ x `=> 42 //│ ╔══[ERROR] Type error in unquoted term //│ ║ l.30: x `=> 42 //│ ║ ^^ -//│ ╙── because: cannot constrain Int <: CodeBase[out cde, out ctx, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out 'cde, out 'ctx, ?] //│ Type: CodeBase[out ⊤ -> ⊥, ⊥, ?] f `=> x `=> f`(x) -//│ Type: CodeBase[out (x -> app) -> (x -> app), ⊥, ?] +//│ Type: CodeBase[out ('x -> 'app) -> ('x -> 'app), ⊥, ?] @@ -53,7 +53,7 @@ x `=> y `=> x `+ y //│ Type: CodeBase[out (Int, Int, Int) -> Int, ⊥, ?] f `=> x `=> y `=> f`(x, y) -//│ Type: CodeBase[out ((x, y) -> app) -> (x -> (y -> app)), ⊥, ?] +//│ Type: CodeBase[out (('x, 'y) -> 'app) -> ('x -> ('y -> 'app)), ⊥, ?] `let x = `42 `in x //│ Type: CodeBase[out Int, ⊥, ?] @@ -63,7 +63,7 @@ f `=> x `=> y `=> f`(x, y) //│ ╔══[ERROR] Type error in unquoted term //│ ║ l.62: `let x = 42 `in x //│ ║ ^^ -//│ ╙── because: cannot constrain Int <: CodeBase[out cde, out ctx, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out 'cde, out 'ctx, ?] //│ Type: CodeBase[⊥, ⊥, ?] :e @@ -71,7 +71,7 @@ f `=> x `=> y `=> f`(x, y) //│ ╔══[ERROR] Type error in unquoted term //│ ║ l.70: `let x = `0 `in 1 //│ ║ ^ -//│ ╙── because: cannot constrain Int <: CodeBase[out cde, out ctx, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out 'cde, out 'ctx, ?] //│ Type: CodeBase[⊥, ⊥, ?] @@ -82,7 +82,7 @@ f `=> x `=> y `=> f`(x, y) x `=> `if x `== `0.0 then `1.0 else x -//│ Type: CodeBase[out x -> (x ∨ Num), ⊥, ?] +//│ Type: CodeBase[out 'x -> ('x ∨ Num), ⊥, ?] run(`1) //│ Type: Int @@ -90,34 +90,34 @@ run(`1) :e run(1) -//│ ╔══[ERROR] Type error in integer literal with expected type CodeBase[out T, ⊥, ?] +//│ ╔══[ERROR] Type error in integer literal with expected type CodeBase[out 'T, ⊥, ?] //│ ║ l.92: run(1) //│ ║ ^ -//│ ╙── because: cannot constrain Int <: CodeBase[out T, ⊥, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out 'T, ⊥, ?] //│ Type: ⊥ :e x `=> run(x) -//│ ╔══[ERROR] Type error in reference with expected type CodeBase[out T, ⊥, ?] +//│ ╔══[ERROR] Type error in reference with expected type CodeBase[out 'T, ⊥, ?] //│ ║ l.100: x `=> run(x) //│ ║ ^ -//│ ╟── because: cannot constrain CodeBase[x, , ⊥] <: CodeBase[out T, ⊥, ?] -//│ ╙── because: cannot constrain <: ⊥ -//│ Type: CodeBase[out CodeBase[out cde, ?, ?] -> cde, out ctx, ?] +//│ ╟── because: cannot constrain CodeBase['x, ', ⊥] <: CodeBase[out 'T, ⊥, ?] +//│ ╙── because: cannot constrain ' <: ⊥ +//│ Type: CodeBase[out CodeBase[out 'cde, ?, ?] -> 'cde, out 'ctx, ?] :e `let x = `42 `in run(x) -//│ ╔══[ERROR] Type error in reference with expected type CodeBase[out T, ⊥, ?] +//│ ╔══[ERROR] Type error in reference with expected type CodeBase[out 'T, ⊥, ?] //│ ║ l.109: `let x = `42 `in run(x) //│ ║ ^ -//│ ╟── because: cannot constrain CodeBase[cde, , ⊥] <: CodeBase[out T, ⊥, ?] -//│ ╙── because: cannot constrain <: ⊥ +//│ ╟── because: cannot constrain CodeBase['cde, ', ⊥] <: CodeBase[out 'T, ⊥, ?] +//│ ╙── because: cannot constrain ' <: ⊥ //│ ╔══[ERROR] Type error in unquoted term //│ ║ l.109: `let x = `42 `in run(x) //│ ║ ^^^^^^ -//│ ╟── because: cannot constrain T <: CodeBase[out cde1, out ctx, ?] -//│ ╟── because: cannot constrain T <: ¬(¬{CodeBase[out cde1, out ctx, ?]}) -//│ ╟── because: cannot constrain cde <: ¬(¬{CodeBase[out cde1, out ctx, ?]}) -//│ ╟── because: cannot constrain cde <: CodeBase[out cde1, out ctx, ?] -//│ ╙── because: cannot constrain Int <: CodeBase[out cde1, out ctx, ?] +//│ ╟── because: cannot constrain 'T <: CodeBase[out 'cde1, out 'ctx, ?] +//│ ╟── because: cannot constrain 'T <: ¬(¬{CodeBase[out 'cde1, out 'ctx, ?]}) +//│ ╟── because: cannot constrain 'cde <: ¬(¬{CodeBase[out 'cde1, out 'ctx, ?]}) +//│ ╟── because: cannot constrain 'cde <: CodeBase[out 'cde1, out 'ctx, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out 'cde1, out 'ctx, ?] //│ Type: CodeBase[⊥, ⊥, ?] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls index a7609e6f5..fc994866b 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls @@ -12,9 +12,9 @@ fun f x = f fun f(x) = f f -//│ Type: forall f: ⊤ -> (⊤ -> f) +//│ Type: forall 'f: ⊤ -> (⊤ -> 'f) //│ Where: -//│ ⊤ -> f <: f +//│ ⊤ -> 'f <: 'f fun f(x) = f(x) f @@ -39,9 +39,9 @@ Foo(123) //│ Type: ⊥ new Foo(123) -//│ Type: Foo[A] +//│ Type: Foo['A] //│ Where: -//│ Int <: A +//│ Int <: 'A :todo proper error fun f(x) = f(Foo.a(x)) @@ -52,8 +52,8 @@ fun f(x) = f(Foo.a(x)) fun f(x) = f(x.Foo#a) f -//│ Type: forall x: Foo[out x] -> ⊥ +//│ Type: forall 'x: Foo[out 'x] -> ⊥ //│ Where: -//│ x <: Foo[out x] +//│ 'x <: Foo[out 'x] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls index a1a61bbcb..71eeec06b 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls @@ -25,12 +25,12 @@ let r = region x in x.ref 42 //│ ║ ^^^^^^^^ //│ ║ l.22: !r //│ ║ ^^ -//│ ╟── because: cannot constrain reg ∨ eff <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ x <: ¬() -//│ ╟── because: cannot constrain x <: ¬() +//│ ╟── because: cannot constrain 'reg ∨ 'eff <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'x <: ¬() +//│ ╟── because: cannot constrain 'x <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -43,21 +43,21 @@ let t = region x in x in t.ref 42 //│ ╔══[ERROR] Type error in reference creation //│ ║ l.42: let t = region x in x in t.ref 42 //│ ║ ^^^^^^^^ -//│ ╟── because: cannot constrain Region[in x out x] <: Region[reg] -//│ ╟── because: cannot constrain x <: reg -//│ ╟── because: cannot constrain x <: reg -//│ ╟── because: cannot constrain x <: ¬(¬x) -//│ ╟── because: cannot constrain x <: ¬(¬x) -//│ ╟── because: cannot constrain <: ¬(¬x) -//│ ╟── because: cannot constrain <: x +//│ ╟── because: cannot constrain Region[in 'x out 'x] <: Region['reg] +//│ ╟── because: cannot constrain 'x <: 'reg +//│ ╟── because: cannot constrain 'x <: 'reg +//│ ╟── because: cannot constrain 'x <: ¬(¬'x) +//│ ╟── because: cannot constrain 'x <: ¬(¬'x) +//│ ╟── because: cannot constrain <: ¬(¬'x) +//│ ╟── because: cannot constrain <: 'x //│ ╙── because: cannot constrain <: ¬() //│ ╔══[ERROR] Type error in block //│ ║ l.42: let t = region x in x in t.ref 42 //│ ║ ^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain reg ∨ eff <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain x <: ¬() -//│ ╟── because: cannot constrain x <: ¬() +//│ ╟── because: cannot constrain 'reg ∨ 'eff <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain 'x <: ¬() +//│ ╟── because: cannot constrain 'x <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Ref[Int, ?] @@ -75,12 +75,12 @@ in t := 0 //│ ║ ^^^^^^^^ //│ ║ l.72: in t := 0 //│ ║ ^^^^^^^^^ -//│ ╟── because: cannot constrain reg ∨ eff <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ x <: ¬() -//│ ╟── because: cannot constrain x <: ¬() +//│ ╟── because: cannot constrain 'reg ∨ 'eff <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'x <: ¬() +//│ ╟── because: cannot constrain 'x <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -98,12 +98,12 @@ in !t //│ ║ ^^^^^^^^ //│ ║ l.95: in !t //│ ║ ^^^^^ -//│ ╟── because: cannot constrain reg ∨ eff <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain reg1 <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ x <: ¬() -//│ ╟── because: cannot constrain x <: ¬() +//│ ╟── because: cannot constrain 'reg ∨ 'eff <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain 'reg1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'x <: ¬() +//│ ╟── because: cannot constrain 'x <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -125,12 +125,12 @@ fun rid(x) = :e region x in (let dz = x.ref 42 in 42): [A] -> Int -//│ ╔══[ERROR] Type error in block with expected type forall A: Int +//│ ╔══[ERROR] Type error in block with expected type forall 'A: Int //│ ║ l.127: (let dz = x.ref 42 in 42): [A] -> Int //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain reg <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╙── because: cannot constrain <: ¬() +//│ ╟── because: cannot constrain 'reg <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╙── because: cannot constrain ' <: ¬() //│ Type: Int @@ -144,12 +144,12 @@ in t(42) //│ ║ ^^^^^^^^^^^^ //│ ║ l.141: in t(42) //│ ║ ^^^^^^^^ -//│ ╟── because: cannot constrain reg ∨ eff <: ⊥ -//│ ╟── because: cannot constrain reg <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ x <: ¬() -//│ ╟── because: cannot constrain x <: ¬() +//│ ╟── because: cannot constrain 'reg ∨ 'eff <: ⊥ +//│ ╟── because: cannot constrain 'reg <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ 'x <: ¬() +//│ ╟── because: cannot constrain 'x <: ¬() //│ ╙── because: cannot constrain <: ¬() -//│ Type: Ref[in y out y ∨ Int, ?] +//│ Type: Ref[in 'y out 'y ∨ Int, ?] fun foo: [A] -> Int ->{A} Int fun foo(x) = @@ -159,7 +159,7 @@ fun foo(x) = region x in x.ref ((x => x): [A] -> A -> A) -//│ Type: Ref[A -> A, ?] +//│ Type: Ref['A -> 'A, ?] fun foo: [A extends Int] -> A -> A @@ -167,23 +167,23 @@ fun foo(x) = x //│ Type: ⊤ foo -//│ Type: forall A: (A) ->{⊥} A +//│ Type: forall 'A: ('A) ->{⊥} 'A //│ Where: -//│ A <: Int +//│ 'A <: Int region x in x.ref foo -//│ Type: Ref[in A -> (A ∧ Int) out (A ∧ Int) -> A, ?] +//│ Type: Ref[in 'A -> ('A ∧ Int) out ('A ∧ Int) -> 'A, ?] fun bar: ([A] -> A -> A) -> Int fun bar(f) = f(42) //│ Type: ⊤ bar -//│ Type: (forall A: (A) ->{⊥} A) ->{⊥} Int +//│ Type: (forall 'A: ('A) ->{⊥} 'A) ->{⊥} Int :e region x in x.ref bar -//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall A: (A) ->{⊥} A) ->{⊥} Int found +//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall 'A: ('A) ->{⊥} 'A) ->{⊥} Int found //│ ║ l.185: region x in x.ref bar //│ ╙── ^^^ //│ Type: Ref[⊥, ?] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls index 675d0ed50..c0890fca0 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls @@ -12,9 +12,9 @@ fun f(x) = x(x) //│ Type: ⊤ f -//│ Type: forall x, eff, app: (x ->{eff} app) ->{eff} app +//│ Type: forall 'x, 'eff, 'app: ('x ->{'eff} 'app) ->{'eff} 'app //│ Where: -//│ x <: x ->{eff} app +//│ 'x <: 'x ->{'eff} 'app f(f) //│ Type: ⊥ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls index e957b614a..c6b32b9d5 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls @@ -35,7 +35,7 @@ fun mapi = s => f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out , out ] +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out ', out '] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -44,15 +44,15 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out B, out E1] <: Seq[out , out ] -//│ ╟── because: cannot constrain E1 <: -//│ ╟── because: cannot constrain E1 <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ reg <: ¬(¬) -//│ ╟── because: cannot constrain reg <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ r <: ¬(¬) -//│ ╟── because: cannot constrain r <: ¬(¬) -//│ ╙── because: cannot constrain <: ¬(¬) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out , out ] +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out ', out '] +//│ ╟── because: cannot constrain 'E1 <: ' +//│ ╟── because: cannot constrain 'E1 <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') +//│ ╟── because: cannot constrain 'reg <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') +//│ ╟── because: cannot constrain 'r <: ¬(¬') +//│ ╙── because: cannot constrain <: ¬(¬') +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out ', out '] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -61,15 +61,15 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out B, out E1] <: Seq[out , out ] -//│ ╟── because: cannot constrain E1 <: -//│ ╟── because: cannot constrain E1 <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ reg <: ¬(¬) -//│ ╟── because: cannot constrain reg <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ r <: ¬(¬) -//│ ╟── because: cannot constrain r <: ¬(¬) -//│ ╙── because: cannot constrain <: ¬(¬) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out , out ] +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out ', out '] +//│ ╟── because: cannot constrain 'E1 <: ' +//│ ╟── because: cannot constrain 'E1 <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') +//│ ╟── because: cannot constrain 'reg <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') +//│ ╟── because: cannot constrain 'r <: ¬(¬') +//│ ╙── because: cannot constrain <: ¬(¬') +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out ', out '] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -78,14 +78,14 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out B, out E1] <: Seq[out , out ] -//│ ╟── because: cannot constrain E1 <: -//│ ╟── because: cannot constrain E1 <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ reg <: ¬(¬) -//│ ╟── because: cannot constrain reg <: ¬(¬) -//│ ╟── because: cannot constrain ¬⊥ ∧ r <: ¬(¬) -//│ ╟── because: cannot constrain r <: ¬(¬) -//│ ╙── because: cannot constrain <: ¬(¬) +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out ', out '] +//│ ╟── because: cannot constrain 'E1 <: ' +//│ ╟── because: cannot constrain 'E1 <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') +//│ ╟── because: cannot constrain 'reg <: ¬(¬') +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') +//│ ╟── because: cannot constrain 'r <: ¬(¬') +//│ ╙── because: cannot constrain <: ¬(¬') //│ Type: ⊤ // * Notice the inferred type, which produces an unusable Sequence (of effect `?` ie `Any`) @@ -96,7 +96,7 @@ fun mapi = s => f => i := !i + 1 f(!i, x) mapi -//│ Type: forall A, E, app, eff: Seq[out A, out E] -> (((Int, A) ->{eff} app) -> Seq[out app, ?]) +//│ Type: forall 'A, 'E, 'app, 'eff: Seq[out 'A, out 'E] -> (((Int, 'A) ->{'eff} 'app) -> Seq[out 'app, ?]) // * This version is correct as it keeps the mutation encapsulated within the region fun mapi_force: [A, E] -> Seq[out A, out E] -> ((Int, A) ->{E} A) ->{E} Seq[out A, Nothing] From 8e0fff7f414216e0e9b66f30ebfcdf856c929136 Mon Sep 17 00:00:00 2001 From: NeilKleistGao Date: Fri, 20 Dec 2024 17:08:38 +0800 Subject: [PATCH 2/3] Improve skolem pp --- .../src/main/scala/hkmc2/bbml/types.scala | 7 ++- .../src/test/mlscript/bbml/bbBounds.mls | 2 +- .../shared/src/test/mlscript/bbml/bbCheck.mls | 6 +-- .../test/mlscript/bbml/bbCyclicExtrude.mls | 10 ++-- .../src/test/mlscript/bbml/bbExtrude.mls | 6 +-- .../shared/src/test/mlscript/bbml/bbGPCE.mls | 14 ++--- .../test/mlscript/bbml/bbLetRegEncoding.mls | 12 ++--- .../shared/src/test/mlscript/bbml/bbList.mls | 54 +++++++++---------- .../shared/src/test/mlscript/bbml/bbPoly.mls | 6 +-- hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls | 8 +-- hkmc2/shared/src/test/mlscript/bbml/bbRef.mls | 2 +- hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls | 54 +++++++++---------- 12 files changed, 90 insertions(+), 91 deletions(-) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala index 29a1b665e..f9a18daf1 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala @@ -168,9 +168,8 @@ sealed abstract class BasicType extends Type: this match case ClassLikeType(name, targs) => if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.show).mkString(", ")}]" - case v @ InfVar(lvl, uid, _, isSkolem) => - val name = scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.hint)) - if isSkolem then s"'<${name}>" else s"'${name}" + case v @ InfVar(lvl, uid, _, _) => + "'" + scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.hint)) case FunType(arg :: Nil, ret, eff) => s"${arg.paren} ->${printEff(eff)} ${ret.paren}" case FunType(args, ret, eff) => s"(${args.map(_.show).mkString(", ")}) ->${printEff(eff)} ${ret.paren}" case ComposedType(lhs, rhs, pol) => s"${lhs.paren} ${if pol then "∨" else "∧"} ${rhs.paren}" @@ -183,7 +182,7 @@ sealed abstract class BasicType extends Type: if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]" case v @ InfVar(lvl, uid, _, isSkolem) => val name = if v.hint.isEmpty then s"${v.sym.nme}" else s"${v.sym.nme}(${v.hint})" - if isSkolem then s"'<${name}${uid}>_${lvl}" else s"'${name}${uid}_${lvl}" + if isSkolem then s"<${name}${uid}>_${lvl}" else s"'${name}${uid}_${lvl}" case FunType(arg :: Nil, ret, eff) => s"${arg.parenDbg} ->{${eff.showDbg}} ${ret.parenDbg}" case FunType(args, ret, eff) => s"(${args.map(_.showDbg).mkString(", ")}) ->{${eff.showDbg}} ${ret.parenDbg}" case ComposedType(lhs, rhs, pol) => s"${lhs.parenDbg} ${if pol then "∨" else "∧"} ${rhs.parenDbg}" diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls index dd4df6199..0c3014356 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls @@ -111,7 +111,7 @@ fun h: [C] -> ([A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B :e bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A -//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as (') ->{⊥} (forall 'B: 'B) ->{⊥} ' +//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as ('A) ->{⊥} (forall 'B: 'B) ->{⊥} 'A //│ ║ l.113: bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A //│ ╙── ^^^^^^ //│ Type: forall 'A: ('A) ->{⊥} (forall 'B: 'A -> 'A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls index dbafab0d8..544f029ec 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls @@ -92,11 +92,11 @@ high(x => x + 1) //│ ╔══[ERROR] Type error in reference with expected type Int //│ ║ l.91: high(x => x + 1) //│ ║ ^ -//│ ╙── because: cannot constrain ' <: Int -//│ ╔══[ERROR] Type error in application with expected type ' +//│ ╙── because: cannot constrain 'A <: Int +//│ ╔══[ERROR] Type error in application with expected type 'A //│ ║ l.91: high(x => x + 1) //│ ║ ^^^^^ -//│ ╙── because: cannot constrain Int <: ' +//│ ╙── because: cannot constrain Int <: 'A //│ Type: Int (let a = 0 in x => x): [A] -> A -> A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls index 0a39f1e4f..4d5298342 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls @@ -20,13 +20,13 @@ f => (let g = x => x(x) in f(g(g))) : [A] -> A -> A :e f => (let g = x => f(x(x)) in g) : [A] -> A -> A -//│ ╔══[ERROR] Type error in block with expected type (') ->{⊥} ' +//│ ╔══[ERROR] Type error in block with expected type ('A) ->{⊥} 'A //│ ║ l.22: f => (let g = x => f(x(x)) in g) : [A] -> A -> A //│ ║ ^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'x ->{'eff ∨ 'eff1} 'app <: ' -> ' -//│ ╟── because: cannot constrain ' <: 'x -//│ ╟── because: cannot constrain ' <: 'x -//│ ╙── because: cannot constrain ' <: ¬(¬{'x ->{'eff1} 'app1}) +//│ ╟── because: cannot constrain 'x ->{'eff ∨ 'eff1} 'app <: 'A -> 'A +//│ ╟── because: cannot constrain 'A <: 'x +//│ ╟── because: cannot constrain 'A <: 'x +//│ ╙── because: cannot constrain 'A <: ¬(¬{'x ->{'eff1} 'app1}) //│ Type: (⊥ -> ⊥) ->{⊥} forall 'A: ('A) ->{⊥} 'A f => (x => f(x(x)) : [A] -> A -> A) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls index 82ba2bbfc..4de6f02cf 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls @@ -41,9 +41,9 @@ y `=> (let t = run(x `=> x `+ y) in y) //│ ╟── because: cannot constrain CodeBase[out 'x -> 'cde, out 'ctx, ?] <: CodeBase[out 'T, ⊥, ?] //│ ╟── because: cannot constrain 'ctx <: ⊥ //│ ╟── because: cannot constrain 'ctx <: ¬() -//│ ╟── because: cannot constrain (¬⊥ ∧ ¬'x) ∧ ' <: ¬() -//│ ╟── because: cannot constrain ' <: 'x -//│ ╙── because: cannot constrain ' <: ¬() +//│ ╟── because: cannot constrain (¬⊥ ∧ ¬'x) ∧ 'y <: ¬() +//│ ╟── because: cannot constrain 'y <: 'x +//│ ╙── because: cannot constrain 'y <: ¬() //│ Type: CodeBase[out 'y -> 'y, ⊥, ?] //│ Where: //│ 'y <: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls index 7a50a58bd..a7e01addf 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls @@ -64,15 +64,15 @@ fun body(x, y) = case 0 then x 1 then y n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out C, out Any] -//│ ╔══[ERROR] Type error in application with expected type CodeBase[out Int, out ', ?] +//│ ╔══[ERROR] Type error in application with expected type CodeBase[out Int, out 'G, ?] //│ ║ l.66: n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out C, out Any] //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain CodeBase[out 'cde, out 'ctx ∨ 'ctx1, ?] <: CodeBase[out Int, out ', ?] -//│ ╟── because: cannot constrain 'ctx ∨ 'ctx1 <: ' -//│ ╟── because: cannot constrain 'ctx1 <: ¬(¬') -//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬') -//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬') -//│ ╙── because: cannot constrain <: ¬(¬') +//│ ╟── because: cannot constrain CodeBase[out 'cde, out 'ctx ∨ 'ctx1, ?] <: CodeBase[out Int, out 'G, ?] +//│ ╟── because: cannot constrain 'ctx ∨ 'ctx1 <: 'G +//│ ╟── because: cannot constrain 'ctx1 <: ¬(¬'G) +//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬'G) +//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬'G) +//│ ╙── because: cannot constrain <: ¬(¬'G) //│ Type: ⊤ fun bind: [G] -> (CodeBase[out Int, out G, out Any], [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C | G, out Any]) -> CodeBase[out Int, out G, out Any] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls index 5c4d53386..89eb493eb 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls @@ -95,30 +95,30 @@ fun letreg: [E,Res] -> ([R] -> Region[R] -> Res) ->{E} Res :e letreg(r => r.ref 1) -//│ ╔══[ERROR] Type error in function literal with expected type (Region[']) ->{⊥} 'Res +//│ ╔══[ERROR] Type error in function literal with expected type (Region['R]) ->{⊥} 'Res //│ ║ l.97: letreg(r => r.ref 1) //│ ║ ^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() -//│ ╙── because: cannot constrain ' <: ¬() +//│ ╙── because: cannot constrain 'R <: ¬() //│ Type: Ref[Int, ?] :e letreg(r => !(r.ref 1)) -//│ ╔══[ERROR] Type error in function literal with expected type (Region[']) ->{⊥} 'Res +//│ ╔══[ERROR] Type error in function literal with expected type (Region['R]) ->{⊥} 'Res //│ ║ l.107: letreg(r => !(r.ref 1)) //│ ║ ^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg ∨ 'reg1 <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() //│ ╟── because: cannot constrain 'reg1 <: ¬() //│ ╟── because: cannot constrain 'reg1 <: ¬() -//│ ╙── because: cannot constrain ' <: ¬() -//│ ╔══[ERROR] Type error in function literal with expected type (Region[']) ->{⊥} 'Res +//│ ╙── because: cannot constrain 'R <: ¬() +//│ ╔══[ERROR] Type error in function literal with expected type (Region['R]) ->{⊥} 'Res //│ ║ l.107: letreg(r => !(r.ref 1)) //│ ║ ^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg ∨ 'reg1 <: ⊥ //│ ╟── because: cannot constrain 'reg1 <: ¬() -//│ ╙── because: cannot constrain ' <: ¬() +//│ ╙── because: cannot constrain 'R <: ¬() //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls index 2d065c0fe..5df224041 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls @@ -51,7 +51,7 @@ fun mapi = s => f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ') ->{'} ') ->{'} List[out '] +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -60,15 +60,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, ') ->{'} ') ->{'} List[out '] -//│ ╟── because: cannot constrain 'E1 <: ' -//│ ╟── because: cannot constrain 'E1 <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') -//│ ╟── because: cannot constrain 'reg <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') -//│ ╟── because: cannot constrain 'r <: ¬(¬') -//│ ╙── because: cannot constrain <: ¬(¬') -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ') ->{'} ') ->{'} List[out '] +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] +//│ ╟── because: cannot constrain 'E1 <: 'E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) +//│ ╟── because: cannot constrain 'r <: ¬(¬'E) +//│ ╙── because: cannot constrain <: ¬(¬'E) +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -77,15 +77,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, ') ->{'} ') ->{'} List[out '] -//│ ╟── because: cannot constrain 'E1 <: ' -//│ ╟── because: cannot constrain 'E1 <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') -//│ ╟── because: cannot constrain 'reg <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') -//│ ╟── because: cannot constrain 'r <: ¬(¬') -//│ ╙── because: cannot constrain <: ¬(¬') -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, ') ->{'} ') ->{'} List[out '] +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] +//│ ╟── because: cannot constrain 'E1 <: 'E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) +//│ ╟── because: cannot constrain 'r <: ¬(¬'E) +//│ ╙── because: cannot constrain <: ¬(¬'E) +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -94,14 +94,14 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, ') ->{'} ') ->{'} List[out '] -//│ ╟── because: cannot constrain 'E1 <: ' -//│ ╟── because: cannot constrain 'E1 <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') -//│ ╟── because: cannot constrain 'reg <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') -//│ ╟── because: cannot constrain 'r <: ¬(¬') -//│ ╙── because: cannot constrain <: ¬(¬') +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] +//│ ╟── because: cannot constrain 'E1 <: 'E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) +//│ ╟── because: cannot constrain 'r <: ¬(¬'E) +//│ ╙── because: cannot constrain <: ¬(¬'E) //│ Type: ⊤ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls index 23df7f1c5..d2be5bfb7 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls @@ -26,11 +26,11 @@ id //│ ╔══[ERROR] Type error in reference with expected type Int //│ ║ l.25: (x => x + 1): [A] -> A -> A //│ ║ ^ -//│ ╙── because: cannot constrain ' <: Int -//│ ╔══[ERROR] Type error in application with expected type ' +//│ ╙── because: cannot constrain 'A <: Int +//│ ╔══[ERROR] Type error in application with expected type 'A //│ ║ l.25: (x => x + 1): [A] -> A -> A //│ ║ ^^^^^ -//│ ╙── because: cannot constrain Int <: ' +//│ ╙── because: cannot constrain Int <: 'A //│ Type: forall 'A: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls index dabf0f154..3b4e3c740 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls @@ -101,8 +101,8 @@ x `=> run(x) //│ ╔══[ERROR] Type error in reference with expected type CodeBase[out 'T, ⊥, ?] //│ ║ l.100: x `=> run(x) //│ ║ ^ -//│ ╟── because: cannot constrain CodeBase['x, ', ⊥] <: CodeBase[out 'T, ⊥, ?] -//│ ╙── because: cannot constrain ' <: ⊥ +//│ ╟── because: cannot constrain CodeBase['x, 'x, ⊥] <: CodeBase[out 'T, ⊥, ?] +//│ ╙── because: cannot constrain 'x <: ⊥ //│ Type: CodeBase[out CodeBase[out 'cde, ?, ?] -> 'cde, out 'ctx, ?] :e @@ -110,8 +110,8 @@ x `=> run(x) //│ ╔══[ERROR] Type error in reference with expected type CodeBase[out 'T, ⊥, ?] //│ ║ l.109: `let x = `42 `in run(x) //│ ║ ^ -//│ ╟── because: cannot constrain CodeBase['cde, ', ⊥] <: CodeBase[out 'T, ⊥, ?] -//│ ╙── because: cannot constrain ' <: ⊥ +//│ ╟── because: cannot constrain CodeBase['cde, 'x, ⊥] <: CodeBase[out 'T, ⊥, ?] +//│ ╙── because: cannot constrain 'x <: ⊥ //│ ╔══[ERROR] Type error in unquoted term //│ ║ l.109: `let x = `42 `in run(x) //│ ║ ^^^^^^ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls index 71eeec06b..ab52cd57b 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls @@ -130,7 +130,7 @@ region x in //│ ║ ^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() -//│ ╙── because: cannot constrain ' <: ¬() +//│ ╙── because: cannot constrain 'x <: ¬() //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls index c6b32b9d5..d5e9f3380 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls @@ -35,7 +35,7 @@ fun mapi = s => f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out ', out '] +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 'A, out 'E] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -44,15 +44,15 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out ', out '] -//│ ╟── because: cannot constrain 'E1 <: ' -//│ ╟── because: cannot constrain 'E1 <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') -//│ ╟── because: cannot constrain 'reg <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') -//│ ╟── because: cannot constrain 'r <: ¬(¬') -//│ ╙── because: cannot constrain <: ¬(¬') -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out ', out '] +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out 'A, out 'E] +//│ ╟── because: cannot constrain 'E1 <: 'E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) +//│ ╟── because: cannot constrain 'r <: ¬(¬'E) +//│ ╙── because: cannot constrain <: ¬(¬'E) +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 'A, out 'E] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -61,15 +61,15 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out ', out '] -//│ ╟── because: cannot constrain 'E1 <: ' -//│ ╟── because: cannot constrain 'E1 <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') -//│ ╟── because: cannot constrain 'reg <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') -//│ ╟── because: cannot constrain 'r <: ¬(¬') -//│ ╙── because: cannot constrain <: ¬(¬') -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out ', out '] +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out 'A, out 'E] +//│ ╟── because: cannot constrain 'E1 <: 'E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) +//│ ╟── because: cannot constrain 'r <: ¬(¬'E) +//│ ╙── because: cannot constrain <: ¬(¬'E) +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 'A, out 'E] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -78,14 +78,14 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out ', out '] -//│ ╟── because: cannot constrain 'E1 <: ' -//│ ╟── because: cannot constrain 'E1 <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬') -//│ ╟── because: cannot constrain 'reg <: ¬(¬') -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬') -//│ ╟── because: cannot constrain 'r <: ¬(¬') -//│ ╙── because: cannot constrain <: ¬(¬') +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out 'A, out 'E] +//│ ╟── because: cannot constrain 'E1 <: 'E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) +//│ ╟── because: cannot constrain 'r <: ¬(¬'E) +//│ ╙── because: cannot constrain <: ¬(¬'E) //│ Type: ⊤ // * Notice the inferred type, which produces an unusable Sequence (of effect `?` ie `Any`) From af3924c0b5989198d665c8e875880e329ce9bca8 Mon Sep 17 00:00:00 2001 From: NeilKleistGao Date: Sat, 21 Dec 2024 09:22:49 +0800 Subject: [PATCH 3/3] Remove unecessary ticks for skolem --- .../src/main/scala/hkmc2/bbml/types.scala | 7 +-- .../src/test/mlscript/bbml/bbBounds.mls | 2 +- .../shared/src/test/mlscript/bbml/bbCheck.mls | 6 +-- .../test/mlscript/bbml/bbCyclicExtrude.mls | 10 ++-- .../src/test/mlscript/bbml/bbExtrude.mls | 6 +-- .../shared/src/test/mlscript/bbml/bbGPCE.mls | 14 ++--- .../test/mlscript/bbml/bbLetRegEncoding.mls | 12 ++--- .../shared/src/test/mlscript/bbml/bbList.mls | 54 +++++++++---------- .../shared/src/test/mlscript/bbml/bbPoly.mls | 6 +-- hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls | 8 +-- hkmc2/shared/src/test/mlscript/bbml/bbRef.mls | 2 +- hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls | 54 +++++++++---------- 12 files changed, 91 insertions(+), 90 deletions(-) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala index f9a18daf1..15ee10be9 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala @@ -168,8 +168,9 @@ sealed abstract class BasicType extends Type: this match case ClassLikeType(name, targs) => if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.show).mkString(", ")}]" - case v @ InfVar(lvl, uid, _, _) => - "'" + scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.hint)) + case v @ InfVar(lvl, uid, _, isSkolem) => + val name = scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.hint)) + if isSkolem then name else s"'${name}" case FunType(arg :: Nil, ret, eff) => s"${arg.paren} ->${printEff(eff)} ${ret.paren}" case FunType(args, ret, eff) => s"(${args.map(_.show).mkString(", ")}) ->${printEff(eff)} ${ret.paren}" case ComposedType(lhs, rhs, pol) => s"${lhs.paren} ${if pol then "∨" else "∧"} ${rhs.paren}" @@ -182,7 +183,7 @@ sealed abstract class BasicType extends Type: if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]" case v @ InfVar(lvl, uid, _, isSkolem) => val name = if v.hint.isEmpty then s"${v.sym.nme}" else s"${v.sym.nme}(${v.hint})" - if isSkolem then s"<${name}${uid}>_${lvl}" else s"'${name}${uid}_${lvl}" + if isSkolem then s"${name}${uid}_${lvl}" else s"'${name}${uid}_${lvl}" case FunType(arg :: Nil, ret, eff) => s"${arg.parenDbg} ->{${eff.showDbg}} ${ret.parenDbg}" case FunType(args, ret, eff) => s"(${args.map(_.showDbg).mkString(", ")}) ->{${eff.showDbg}} ${ret.parenDbg}" case ComposedType(lhs, rhs, pol) => s"${lhs.parenDbg} ${if pol then "∨" else "∧"} ${rhs.parenDbg}" diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls index 0c3014356..705d160c0 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls @@ -111,7 +111,7 @@ fun h: [C] -> ([A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B :e bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A -//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as ('A) ->{⊥} (forall 'B: 'B) ->{⊥} 'A +//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as (A) ->{⊥} (forall 'B: 'B) ->{⊥} A //│ ║ l.113: bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A //│ ╙── ^^^^^^ //│ Type: forall 'A: ('A) ->{⊥} (forall 'B: 'A -> 'A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls index 544f029ec..705128efb 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls @@ -92,11 +92,11 @@ high(x => x + 1) //│ ╔══[ERROR] Type error in reference with expected type Int //│ ║ l.91: high(x => x + 1) //│ ║ ^ -//│ ╙── because: cannot constrain 'A <: Int -//│ ╔══[ERROR] Type error in application with expected type 'A +//│ ╙── because: cannot constrain A <: Int +//│ ╔══[ERROR] Type error in application with expected type A //│ ║ l.91: high(x => x + 1) //│ ║ ^^^^^ -//│ ╙── because: cannot constrain Int <: 'A +//│ ╙── because: cannot constrain Int <: A //│ Type: Int (let a = 0 in x => x): [A] -> A -> A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls index 4d5298342..15b4eda12 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls @@ -20,13 +20,13 @@ f => (let g = x => x(x) in f(g(g))) : [A] -> A -> A :e f => (let g = x => f(x(x)) in g) : [A] -> A -> A -//│ ╔══[ERROR] Type error in block with expected type ('A) ->{⊥} 'A +//│ ╔══[ERROR] Type error in block with expected type (A) ->{⊥} A //│ ║ l.22: f => (let g = x => f(x(x)) in g) : [A] -> A -> A //│ ║ ^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'x ->{'eff ∨ 'eff1} 'app <: 'A -> 'A -//│ ╟── because: cannot constrain 'A <: 'x -//│ ╟── because: cannot constrain 'A <: 'x -//│ ╙── because: cannot constrain 'A <: ¬(¬{'x ->{'eff1} 'app1}) +//│ ╟── because: cannot constrain 'x ->{'eff ∨ 'eff1} 'app <: A -> A +//│ ╟── because: cannot constrain A <: 'x +//│ ╟── because: cannot constrain A <: 'x +//│ ╙── because: cannot constrain A <: ¬(¬{'x ->{'eff1} 'app1}) //│ Type: (⊥ -> ⊥) ->{⊥} forall 'A: ('A) ->{⊥} 'A f => (x => f(x(x)) : [A] -> A -> A) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls index 4de6f02cf..24bbc3e21 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls @@ -41,9 +41,9 @@ y `=> (let t = run(x `=> x `+ y) in y) //│ ╟── because: cannot constrain CodeBase[out 'x -> 'cde, out 'ctx, ?] <: CodeBase[out 'T, ⊥, ?] //│ ╟── because: cannot constrain 'ctx <: ⊥ //│ ╟── because: cannot constrain 'ctx <: ¬() -//│ ╟── because: cannot constrain (¬⊥ ∧ ¬'x) ∧ 'y <: ¬() -//│ ╟── because: cannot constrain 'y <: 'x -//│ ╙── because: cannot constrain 'y <: ¬() +//│ ╟── because: cannot constrain (¬⊥ ∧ ¬'x) ∧ y <: ¬() +//│ ╟── because: cannot constrain y <: 'x +//│ ╙── because: cannot constrain y <: ¬() //│ Type: CodeBase[out 'y -> 'y, ⊥, ?] //│ Where: //│ 'y <: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls index a7e01addf..a52e94778 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls @@ -64,15 +64,15 @@ fun body(x, y) = case 0 then x 1 then y n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out C, out Any] -//│ ╔══[ERROR] Type error in application with expected type CodeBase[out Int, out 'G, ?] +//│ ╔══[ERROR] Type error in application with expected type CodeBase[out Int, out G, ?] //│ ║ l.66: n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out C, out Any] //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain CodeBase[out 'cde, out 'ctx ∨ 'ctx1, ?] <: CodeBase[out Int, out 'G, ?] -//│ ╟── because: cannot constrain 'ctx ∨ 'ctx1 <: 'G -//│ ╟── because: cannot constrain 'ctx1 <: ¬(¬'G) -//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬'G) -//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬'G) -//│ ╙── because: cannot constrain <: ¬(¬'G) +//│ ╟── because: cannot constrain CodeBase[out 'cde, out 'ctx ∨ 'ctx1, ?] <: CodeBase[out Int, out G, ?] +//│ ╟── because: cannot constrain 'ctx ∨ 'ctx1 <: G +//│ ╟── because: cannot constrain 'ctx1 <: ¬(¬G) +//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬G) +//│ ╟── because: cannot constrain 'ctx2 <: ¬(¬G) +//│ ╙── because: cannot constrain <: ¬(¬G) //│ Type: ⊤ fun bind: [G] -> (CodeBase[out Int, out G, out Any], [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C | G, out Any]) -> CodeBase[out Int, out G, out Any] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls index 89eb493eb..9c4e98616 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls @@ -95,30 +95,30 @@ fun letreg: [E,Res] -> ([R] -> Region[R] -> Res) ->{E} Res :e letreg(r => r.ref 1) -//│ ╔══[ERROR] Type error in function literal with expected type (Region['R]) ->{⊥} 'Res +//│ ╔══[ERROR] Type error in function literal with expected type (Region[R]) ->{⊥} 'Res //│ ║ l.97: letreg(r => r.ref 1) //│ ║ ^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() -//│ ╙── because: cannot constrain 'R <: ¬() +//│ ╙── because: cannot constrain R <: ¬() //│ Type: Ref[Int, ?] :e letreg(r => !(r.ref 1)) -//│ ╔══[ERROR] Type error in function literal with expected type (Region['R]) ->{⊥} 'Res +//│ ╔══[ERROR] Type error in function literal with expected type (Region[R]) ->{⊥} 'Res //│ ║ l.107: letreg(r => !(r.ref 1)) //│ ║ ^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg ∨ 'reg1 <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() //│ ╟── because: cannot constrain 'reg1 <: ¬() //│ ╟── because: cannot constrain 'reg1 <: ¬() -//│ ╙── because: cannot constrain 'R <: ¬() -//│ ╔══[ERROR] Type error in function literal with expected type (Region['R]) ->{⊥} 'Res +//│ ╙── because: cannot constrain R <: ¬() +//│ ╔══[ERROR] Type error in function literal with expected type (Region[R]) ->{⊥} 'Res //│ ║ l.107: letreg(r => !(r.ref 1)) //│ ║ ^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg ∨ 'reg1 <: ⊥ //│ ╟── because: cannot constrain 'reg1 <: ¬() -//│ ╙── because: cannot constrain 'R <: ¬() +//│ ╙── because: cannot constrain R <: ¬() //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls index 5df224041..ce9e7123a 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls @@ -51,7 +51,7 @@ fun mapi = s => f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, A) ->{E} A) ->{E} List[out A] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -60,15 +60,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] -//│ ╟── because: cannot constrain 'E1 <: 'E -//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) -//│ ╟── because: cannot constrain 'r <: ¬(¬'E) -//│ ╙── because: cannot constrain <: ¬(¬'E) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, A) ->{E} A) ->{E} List[out A] +//│ ╟── because: cannot constrain 'E1 <: E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬E) +//│ ╟── because: cannot constrain 'r <: ¬(¬E) +//│ ╙── because: cannot constrain <: ¬(¬E) +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, A) ->{E} A) ->{E} List[out A] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -77,15 +77,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] -//│ ╟── because: cannot constrain 'E1 <: 'E -//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) -//│ ╟── because: cannot constrain 'r <: ¬(¬'E) -//│ ╙── because: cannot constrain <: ¬(¬'E) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, A) ->{E} A) ->{E} List[out A] +//│ ╟── because: cannot constrain 'E1 <: E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬E) +//│ ╟── because: cannot constrain 'r <: ¬(¬E) +//│ ╙── because: cannot constrain <: ¬(¬E) +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, A) ->{E} A) ->{E} List[out A] //│ ║ l.50: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.51: f => map(s) of x => @@ -94,14 +94,14 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.53: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, 'A) ->{'E} 'A) ->{'E} List[out 'A] -//│ ╟── because: cannot constrain 'E1 <: 'E -//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) -//│ ╟── because: cannot constrain 'r <: ¬(¬'E) -//│ ╙── because: cannot constrain <: ¬(¬'E) +//│ ╟── because: cannot constrain 'f ->{'E1} List[out 'B] <: ((Int, A) ->{E} A) ->{E} List[out A] +//│ ╟── because: cannot constrain 'E1 <: E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬E) +//│ ╟── because: cannot constrain 'r <: ¬(¬E) +//│ ╙── because: cannot constrain <: ¬(¬E) //│ Type: ⊤ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls index d2be5bfb7..0892f9c0d 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls @@ -26,11 +26,11 @@ id //│ ╔══[ERROR] Type error in reference with expected type Int //│ ║ l.25: (x => x + 1): [A] -> A -> A //│ ║ ^ -//│ ╙── because: cannot constrain 'A <: Int -//│ ╔══[ERROR] Type error in application with expected type 'A +//│ ╙── because: cannot constrain A <: Int +//│ ╔══[ERROR] Type error in application with expected type A //│ ║ l.25: (x => x + 1): [A] -> A -> A //│ ║ ^^^^^ -//│ ╙── because: cannot constrain Int <: 'A +//│ ╙── because: cannot constrain Int <: A //│ Type: forall 'A: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls index 3b4e3c740..814553d58 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls @@ -101,8 +101,8 @@ x `=> run(x) //│ ╔══[ERROR] Type error in reference with expected type CodeBase[out 'T, ⊥, ?] //│ ║ l.100: x `=> run(x) //│ ║ ^ -//│ ╟── because: cannot constrain CodeBase['x, 'x, ⊥] <: CodeBase[out 'T, ⊥, ?] -//│ ╙── because: cannot constrain 'x <: ⊥ +//│ ╟── because: cannot constrain CodeBase['x, x, ⊥] <: CodeBase[out 'T, ⊥, ?] +//│ ╙── because: cannot constrain x <: ⊥ //│ Type: CodeBase[out CodeBase[out 'cde, ?, ?] -> 'cde, out 'ctx, ?] :e @@ -110,8 +110,8 @@ x `=> run(x) //│ ╔══[ERROR] Type error in reference with expected type CodeBase[out 'T, ⊥, ?] //│ ║ l.109: `let x = `42 `in run(x) //│ ║ ^ -//│ ╟── because: cannot constrain CodeBase['cde, 'x, ⊥] <: CodeBase[out 'T, ⊥, ?] -//│ ╙── because: cannot constrain 'x <: ⊥ +//│ ╟── because: cannot constrain CodeBase['cde, x, ⊥] <: CodeBase[out 'T, ⊥, ?] +//│ ╙── because: cannot constrain x <: ⊥ //│ ╔══[ERROR] Type error in unquoted term //│ ║ l.109: `let x = `42 `in run(x) //│ ║ ^^^^^^ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls index ab52cd57b..4a726d8f9 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls @@ -130,7 +130,7 @@ region x in //│ ║ ^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() -//│ ╙── because: cannot constrain 'x <: ¬() +//│ ╙── because: cannot constrain x <: ¬() //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls index d5e9f3380..813444f33 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls @@ -35,7 +35,7 @@ fun mapi = s => f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 'A, out 'E] +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out A, out E] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -44,15 +44,15 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out 'A, out 'E] -//│ ╟── because: cannot constrain 'E1 <: 'E -//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) -//│ ╟── because: cannot constrain 'r <: ¬(¬'E) -//│ ╙── because: cannot constrain <: ¬(¬'E) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 'A, out 'E] +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out A, out E] +//│ ╟── because: cannot constrain 'E1 <: E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬E) +//│ ╟── because: cannot constrain 'r <: ¬(¬E) +//│ ╙── because: cannot constrain <: ¬(¬E) +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out A, out E] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -61,15 +61,15 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out 'A, out 'E] -//│ ╟── because: cannot constrain 'E1 <: 'E -//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) -//│ ╟── because: cannot constrain 'r <: ¬(¬'E) -//│ ╙── because: cannot constrain <: ¬(¬'E) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 'A, out 'E] +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out A, out E] +//│ ╟── because: cannot constrain 'E1 <: E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬E) +//│ ╟── because: cannot constrain 'r <: ¬(¬E) +//│ ╙── because: cannot constrain <: ¬(¬E) +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out A, out E] //│ ║ l.34: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.35: map(s) of x => @@ -78,14 +78,14 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.37: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out 'A, out 'E] -//│ ╟── because: cannot constrain 'E1 <: 'E -//│ ╟── because: cannot constrain 'E1 <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain 'reg <: ¬(¬'E) -//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬'E) -//│ ╟── because: cannot constrain 'r <: ¬(¬'E) -//│ ╙── because: cannot constrain <: ¬(¬'E) +//│ ╟── because: cannot constrain Seq[out 'B, out 'E1] <: Seq[out A, out E] +//│ ╟── because: cannot constrain 'E1 <: E +//│ ╟── because: cannot constrain 'E1 <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain 'reg <: ¬(¬E) +//│ ╟── because: cannot constrain ¬⊥ ∧ 'r <: ¬(¬E) +//│ ╟── because: cannot constrain 'r <: ¬(¬E) +//│ ╙── because: cannot constrain <: ¬(¬E) //│ Type: ⊤ // * Notice the inferred type, which produces an unusable Sequence (of effect `?` ie `Any`)