Skip to content

Logic subtyping and overloading #286

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 43 commits into
base: hkmc2
Choose a base branch
from
Draft

Logic subtyping and overloading #286

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
9707a3f
disjunctive subtyping
auht Feb 25, 2025
cc87059
Changes from meeting
LPTK Feb 26, 2025
0298463
disjoint upperbound
auht Mar 5, 2025
bf4c763
Merge remote-tracking branch 'upstream/hkmc2' into logic-subtyping
auht Mar 5, 2025
ec5c55e
no disjoint upperbound
auht Mar 5, 2025
aa956a7
multiple disjointness
auht Mar 5, 2025
8bad1a5
Changes from meeting
LPTK Mar 6, 2025
86d300d
Add test case and move tests to logicsub folder
LPTK Mar 6, 2025
3b34199
constraints solving nested disjsub
auht Mar 7, 2025
ae28b42
ues linkedhashset
auht Mar 10, 2025
2f1f5f3
traverse disjsub
auht Mar 12, 2025
3d383a2
Changes from meeting
LPTK Mar 13, 2025
00e397b
fix pretty printer type traverse and tv subst
auht Mar 13, 2025
bdd4b7a
Merge remote-tracking branch 'upstream/hkmc2' into logic-subtyping
auht Mar 13, 2025
0bbfeca
wip rcdtype implementation
auht Mar 20, 2025
3a67c1f
wip rcdtype implementation and fun args disjointness
auht Mar 22, 2025
bd53f6f
intersections wf check
auht Mar 24, 2025
92dc44a
fix nested record wf check
auht Mar 26, 2025
69bcc5a
wip refined if
auht Mar 28, 2025
081de12
Update hkmc2/shared/src/test/mlscript/logicsub/Records.mls
auht Mar 28, 2025
52c6941
Merge remote-tracking branch 'upstream/hkmc2' into logic-subtyping
auht Mar 28, 2025
55b9066
wip fix
auht Apr 2, 2025
d99f3af
wip else branch disjointness
auht Apr 4, 2025
93d7ff6
fix if disjsub
auht Apr 6, 2025
3cd0f96
wip if
auht Apr 8, 2025
4996431
Merge remote-tracking branch 'upstream/hkmc2' into logic-subtyping
auht Apr 8, 2025
3928da0
test
auht Apr 8, 2025
88e3518
Pretty printer changes from meeting
LPTK Apr 11, 2025
f77ddbb
dnf disjointness
auht Apr 14, 2025
f009711
fix if
auht Apr 16, 2025
fd21398
fix if
auht Apr 16, 2025
4dc8cd7
fix missing constraints
auht Apr 18, 2025
0ed746e
test
auht Apr 18, 2025
836f3bb
elim branches
auht Apr 20, 2025
a9c4221
negtype and wip test
auht Apr 22, 2025
3bfe1c4
wip test explanation
auht Apr 22, 2025
91ac0d4
Merge remote-tracking branch 'upstream/hkmc2' into logic-subtyping
auht Apr 22, 2025
99b465b
rcd union neg disjointess
auht Apr 28, 2025
9e13a34
Merge remote-tracking branch 'upstream/hkmc2' into logic-subtyping
auht Apr 28, 2025
afb08c5
wf check and typing function intersection
auht May 4, 2025
2cfa234
Merge remote-tracking branch 'upstream/hkmc2' into logic-subtyping
auht May 4, 2025
69feb99
test
auht May 4, 2025
4a335ea
modify disjointness signature and impl
auht May 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
87 changes: 47 additions & 40 deletions hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,6 +159,13 @@ class BBTyper(using elState: Elaborator.State, tl: TL)(using Config):
ClassLikeType(tpeSym, ts)
case N =>
error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil)
case Term.Tup(fields) =>
// TODO
// denote record type by Tup for now
val u = fields.map:
case Fld(_, Lit(StrLit(a)), S(t)) => (a, typeMonoType(t))
case _ => ???
RcdType(u)
case Neg(rhs) =>
mono(rhs, !pol).!
case CompType(lhs, rhs, pol) =>
Expand Down Expand Up @@ -430,7 +437,37 @@ class BBTyper(using elState: Elaborator.State, tl: TL)(using Config):
case ft: PolyFunType =>
ft.monoOr(error(msg"Expected a monomorphic type or an instantiable type here, but ${ty.show} found" -> sc.toLoc :: Nil))
case ty: Type => ty


def goStats(stats: Ls[Statement])(using ctx: BbCtx, scope: Scope, cctx: CCtx, effBuff: ListBuffer[Type]): Unit = stats match
case Nil => ()
case (term: Term) :: stats =>
effBuff += typeCheck(term)._2
goStats(stats)
case LetDecl(sym, _) :: DefineVar(sym2, rhs) :: stats =>
require(sym2 is sym)
val (rhsTy, eff) = typeCheck(rhs)
effBuff += eff
ctx += sym -> rhsTy
goStats(stats)
case TermDefinition(_, Fun, sym, ps :: Nil, _, sig, S(body), _, _, _) :: stats =>
typeFunDef(sym, Term.Lam(ps, body), sig, ctx)
goStats(stats)
case TermDefinition(_, Fun, sym, Nil, _, sig, S(body), _, _, _) :: stats =>
typeFunDef(sym, body, sig, ctx) // * may be a case expressions
goStats(stats)
case TermDefinition(_, Fun, sym1, _, _, S(sig), None, _, _, _) :: (td @ TermDefinition(_, Fun, sym2, _, _, _, S(body), _, _, _)) :: stats
if sym1 === sym2 => goStats(td :: stats) // * avoid type check signatures twice
case TermDefinition(_, Fun, sym, _, _, S(sig), None, _, _, _) :: stats =>
ctx += sym -> typeType(sig)
goStats(stats)
case (clsDef: ClassDef) :: stats =>
goStats(stats)
case (modDef: ModuleDef) :: stats =>
goStats(stats)
case Import(sym, pth) :: stats =>
goStats(stats) // TODO:
case stat :: _ =>
TODO(stat)
private def typeCheck(t: Term)(using ctx: BbCtx, scope: Scope): (GeneralType, Type) =
trace[(GeneralType, Type)](s"${ctx.lvl}. Typing ${t.showDbg}", res => s": (${res._1.showDbg}, ${res._2.showDbg})"):
given CCtx = CCtx.init(t, N)
Expand All @@ -447,38 +484,8 @@ class BBTyper(using elState: Elaborator.State, tl: TL)(using Config):
(error(msg"Variable not found: ${sym.nme}"
-> t.toLoc :: Nil), Bot)
case Blk(stats, res) =>
val effBuff = ListBuffer.empty[Type]
def goStats(stats: Ls[Statement]): Unit = stats match
case Nil => ()
case (term: Term) :: stats =>
effBuff += typeCheck(term)._2
goStats(stats)
case LetDecl(sym, _) :: DefineVar(sym2, rhs) :: stats =>
require(sym2 is sym)
val (rhsTy, eff) = typeCheck(rhs)
effBuff += eff
ctx += sym -> rhsTy
goStats(stats)
case TermDefinition(_, Fun, sym, ps :: Nil, _, sig, S(body), _, _, _) :: stats =>
typeFunDef(sym, Term.Lam(ps, body), sig, ctx)
goStats(stats)
case TermDefinition(_, Fun, sym, Nil, _, sig, S(body), _, _, _) :: stats =>
typeFunDef(sym, body, sig, ctx) // * may be a case expressions
goStats(stats)
case TermDefinition(_, Fun, sym1, _, _, S(sig), None, _, _, _) :: (td @ TermDefinition(_, Fun, sym2, _, _, _, S(body), _, _, _)) :: stats
if sym1 === sym2 => goStats(td :: stats) // * avoid type check signatures twice
case TermDefinition(_, Fun, sym, _, _, S(sig), None, _, _, _) :: stats =>
ctx += sym -> typeType(sig)
goStats(stats)
case (clsDef: ClassDef) :: stats =>
goStats(stats)
case (modDef: ModuleDef) :: stats =>
goStats(stats)
case Import(sym, pth) :: stats =>
goStats(stats) // TODO:
case stat :: _ =>
TODO(stat)
goStats(stats)
val effBuff: ListBuffer[Type] = ListBuffer.empty
goStats(stats)(using effBuff = effBuff)
val (ty, eff) = typeCheck(res)
(ty, effBuff.foldLeft(eff)((res, e) => res | e))
case UnitVal() => (Top, Bot)
Expand Down Expand Up @@ -597,19 +604,19 @@ class BBTyper(using elState: Elaborator.State, tl: TL)(using Config):
(Bot, eff)
case Term.Error =>
(Bot, Bot) // TODO: error type?
case Rcd(fields@((_: RcdField) :: _)) =>
val u = fields.collect:
case RcdField(Lit(StrLit(a)), t) => (a, t, typeCheck(t))
val (w, e) = u.foldRight((Nil: Ls[Str -> Type], Bot: Type)):
case ((a, t, (ty, e)), (w, e0)) => ((a -> tryMkMono(ty, t) :: w), e | e0)
(RcdType(w), e)
case Rcd(stats) =>
// TODO RcdSpread
val (s, r) = stats.partitionMap: k =>
k match
case RcdField(Lit(_: StrLit), _) => R(k)
case _ => L(k)
typeCheck(Blk(s, Rcd(r)))
val effBuff: ListBuffer[Type] = ListBuffer.empty
goStats(s)(using effBuff = effBuff)
val u = r.map:
case RcdField(Lit(StrLit(a)), t) => (a, t, typeCheck(t))
val (w, eff) = u.foldRight((Nil: Ls[Str -> Type], Bot: Type)):
case ((a, t, (ty, e)), (w, e0)) => ((a -> tryMkMono(ty, t) :: w), e | e0)
(RcdType(w), effBuff.foldLeft(eff)((res, e) => res | e))
case Term.Sel(u, Ident(a)) =>
val (ty, e) = typeCheck(u)
val v = freshVar(new TempSymbol(S(t), "sel"))
Expand Down
7 changes: 6 additions & 1 deletion hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,11 @@ case class RcdType(fields: Ls[Str -> Type]) extends BasicType with CachedNorm[Rc
RcdType(fields.mapValues(_.subst))
def & (that: RcdType): RcdType =
RcdType((fields ++ that.fields).groupMapReduce(_._1)(_._2)(_ & _).toList)
def flatten: RcdType =
RcdType(fields.flatMap: u =>
(u._1, u._2.toBasic.simp.toBasic) match
case (a, r: RcdType) => r.flatten.fields.map(u => (s"$a.${u._1}", u._2))
case u => Ls(u))

case class ComposedType(lhs: Type, rhs: Type, pol: Bool) extends BasicType: // * Positive -> union
override def subst(using map: Map[Uid[InfVar], InfVar]): ThisType =
Expand All @@ -296,7 +301,7 @@ object Type:
else lhs & rhs
def mkNegType(ty: Type): Type = ty.!
def discriminant(a: Ls[Type]): (RcdType, RcdType) =
discriminantRcd(RcdType(a.zipWithIndex.map(u => (s"${u._2}", u._1.toBasic))))
discriminantRcd(RcdType(a.zipWithIndex.map(u => (s"${u._2}", u._1.toBasic))).flatten)
def discriminantRcd(a: RcdType): (RcdType, RcdType) =
val (u, w) = (a.fields.map:
case (a, t) =>
Expand Down
82 changes: 53 additions & 29 deletions hkmc2/shared/src/test/mlscript/logicsub/DisjSub.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,6 @@ ap1(idIB)
ap(idIB)(1)
//│ Type: Int

:todo
x => idIB(x)
//│ Type: ('x) ->{'eff} 'app
//│ Where:
Expand All @@ -80,17 +79,17 @@ forward(true)
:todo // BbML
fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
//│ ╔══[ERROR] General type is not allowed here.
//│ ║ l.81: fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
//│ ║ l.80: fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
//│ ╙── ^^^
//│ ╔══[ERROR] General type is not allowed here.
//│ ║ l.81: fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
//│ ║ l.80: fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool)
//│ ╙── ^^^^
//│ Type: ⊤

:todo // BbML
idIIBB([1, 2])
//│ ╔══[ERROR] Term shape not yet supported by BbML: Tup(List(Fld(‹›,Lit(IntLit(1)),None), Fld(‹›,Lit(IntLit(2)),None)))
//│ ║ l.91: idIIBB([1, 2])
//│ ║ l.90: idIIBB([1, 2])
//│ ╙── ^^^^^^
//│ Type: ⊥

Expand All @@ -111,29 +110,29 @@ new Pair(1, 2)
//│ Int <: 'A
//│ Int <: 'B

:todo // WF check on intersection types
// WF check on intersection types
:e
fun idIIBB: (Pair[Int, Int] -> Int) & (Pair[Bool, Bool] -> Bool)
//│ ╔══[ERROR] Ill-formed functions intersection
//│ ║ l.116: fun idIIBB: (Pair[Int, Int] -> Int) & (Pair[Bool, Bool] -> Bool)
//│ ║ l.115: fun idIIBB: (Pair[Int, Int] -> Int) & (Pair[Bool, Bool] -> Bool)
//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ Type: ⊤

:e
idIIBB(new Pair(1, 2))
//│ ╔══[ERROR] Type error in application
//│ ║ l.123: idIIBB(new Pair(1, 2))
//│ ║ l.122: idIIBB(new Pair(1, 2))
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── because: cannot constrain (Pair[out Int, out Int] -> Int) ∧ (Pair[out Bool, out Bool] -> Bool) <: Pair['A, 'B] ->{'eff} 'app
//│ ╟── because: cannot constrain Pair['A, 'B] <: Pair[in ⊥ out Bool, in ⊥ out Bool] ∧ ¬⊥
//│ ╟── because: cannot constrain Pair['A, 'B] <: Pair[in ⊥ out Bool, in ⊥ out Bool]
//│ ╟── because: cannot constrain 'A <: Bool
//│ ╟── because: cannot constrain 'A <: ¬(¬{Bool})
//│ ╙── because: cannot constrain Int <: ¬(¬{Bool})
//│ ╔══[ERROR] Type error in application
//│ ║ l.123: idIIBB(new Pair(1, 2))
//│ ║ l.122: idIIBB(new Pair(1, 2))
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── because: cannot constrain (Pair[out Int, out Int] -> Int) ∧ (Pair[out Bool, out Bool] -> Bool) <: Pair['A, 'B] ->{'eff} 'app
//│ ╟── because: cannot constrain Pair['A, 'B] <: Pair[in ⊥ out Bool, in ⊥ out Bool] ∧ ¬⊥
//│ ╟── because: cannot constrain Pair['A, 'B] <: Pair[in ⊥ out Bool, in ⊥ out Bool]
//│ ╟── because: cannot constrain 'B <: Bool
//│ ╟── because: cannot constrain 'B <: ¬(¬{Bool})
//│ ╙── because: cannot constrain Int <: ¬(¬{Bool})
Expand All @@ -142,18 +141,18 @@ idIIBB(new Pair(1, 2))
:e
idIIBB(new Pair(1, true))
//│ ╔══[ERROR] Type error in application
//│ ║ l.143: idIIBB(new Pair(1, true))
//│ ║ l.142: idIIBB(new Pair(1, true))
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── because: cannot constrain (Pair[out Int, out Int] -> Int) ∧ (Pair[out Bool, out Bool] -> Bool) <: Pair['A, 'B] ->{'eff} 'app
//│ ╟── because: cannot constrain Pair['A, 'B] <: Pair[in ⊥ out Int, in ⊥ out Int] ∧ ¬⊥
//│ ╟── because: cannot constrain Pair['A, 'B] <: Pair[in ⊥ out Int, in ⊥ out Int]
//│ ╟── because: cannot constrain 'B <: Int
//│ ╟── because: cannot constrain 'B <: ¬(¬{Int})
//│ ╙── because: cannot constrain Bool <: ¬(¬{Int})
//│ ╔══[ERROR] Type error in application
//│ ║ l.143: idIIBB(new Pair(1, true))
//│ ║ l.142: idIIBB(new Pair(1, true))
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── because: cannot constrain (Pair[out Int, out Int] -> Int) ∧ (Pair[out Bool, out Bool] -> Bool) <: Pair['A, 'B] ->{'eff} 'app
//│ ╟── because: cannot constrain Pair['A, 'B] <: Pair[in ⊥ out Bool, in ⊥ out Bool] ∧ ¬⊥
//│ ╟── because: cannot constrain Pair['A, 'B] <: Pair[in ⊥ out Bool, in ⊥ out Bool]
//│ ╟── because: cannot constrain 'A <: Bool
//│ ╟── because: cannot constrain 'A <: ¬(¬{Bool})
//│ ╙── because: cannot constrain Int <: ¬(¬{Bool})
Expand All @@ -163,21 +162,18 @@ idIIBB(new Pair(1, true))

:todo
fun foo: ["x": Int, "y": Int]
//│ ╔══[ERROR] Invalid type
//│ ║ l.165: fun foo: ["x": Int, "y": Int]
//│ ╙── ^^^^^^^^^^^^^^^^^^^^
//│ Type: ⊤

foo
//│ Type: ⊥
//│ Type: {x: Int, y: Int}

:todo
fun foo(x) = if x is
[true, true] then 1
[false, false] then 2
//│ /!!!\ Uncaught error: scala.MatchError: Tuple(2,false) (of class hkmc2.semantics.Pattern$Tuple)

{x:1, y:true}
{x: 1, y:true}
//│ Type: {x: Int, y: Bool}

fun k(f) =
Expand All @@ -201,7 +197,7 @@ k(idIB)(true, 1)
:e
k(idIB)("true", 1)
//│ ╔══[ERROR] Type error in string literal with expected type 'x
//│ ║ l.202: k(idIB)("true", 1)
//│ ║ l.198: k(idIB)("true", 1)
//│ ║ ^^^^^^
//│ ╟── because: cannot constrain Str <: 'x
//│ ╟── because: cannot constrain Str <: 'x
Expand Down Expand Up @@ -254,15 +250,15 @@ map(cons(1, cons(true, nil())))(idIB)
let x = cons(1, cons(true, nil())) in
map(cons(x, x))(idIB)
//│ ╔══[ERROR] Type error in reference with expected type ('A) ->{⊥} 'B
//│ ║ l.255: map(cons(x, x))(idIB)
//│ ║ l.251: map(cons(x, x))(idIB)
//│ ║ ^^^^
//│ ╟── because: cannot constrain (Int -> Int) ∧ (Bool -> Bool) <: 'A -> 'B
//│ ╟── because: cannot constrain {0: 'A} <: {0: Int} ∨ {0: Bool}
//│ ╟── because: cannot constrain 'A <: Bool ∨ Int
//│ ╟── because: cannot constrain 'A <: ¬(¬{Int ∨ Bool})
//│ ╙── because: cannot constrain Ls['A1] <: ¬(¬{Int ∨ Bool})
//│ ╔══[ERROR] Type error in reference with expected type ('A) ->{⊥} 'B
//│ ║ l.255: map(cons(x, x))(idIB)
//│ ║ l.251: map(cons(x, x))(idIB)
//│ ║ ^^^^
//│ ╟── because: cannot constrain (Int -> Int) ∧ (Bool -> Bool) <: 'A -> 'B
//│ ╟── because: cannot constrain {0: 'A} <: {0: Int} ∨ {0: Bool}
Expand All @@ -272,7 +268,7 @@ let x = cons(1, cons(true, nil())) in
//│ ╟── because: cannot constrain 'A1 <: ¬(¬{Int ∨ Bool})
//│ ╙── because: cannot constrain Ls['A1] <: ¬(¬{Int ∨ Bool})
//│ ╔══[ERROR] Type error in reference with expected type ('A) ->{⊥} 'B
//│ ║ l.255: map(cons(x, x))(idIB)
//│ ║ l.251: map(cons(x, x))(idIB)
//│ ║ ^^^^
//│ ╟── because: cannot constrain (Int -> Int) ∧ (Bool -> Bool) <: 'A -> 'B
//│ ╟── because: cannot constrain {0: 'A} <: {0: Int} ∨ {0: Bool}
Expand Down Expand Up @@ -303,14 +299,14 @@ x => k(x, x)
:e
fun ill: ((Int | Bool, Int | Bool) -> Str) & ((Bool | Str, Bool | Str) -> Str)
//│ ╔══[ERROR] Ill-formed functions intersection
//│ ║ l.304: fun ill: ((Int | Bool, Int | Bool) -> Str) & ((Bool | Str, Bool | Str) -> Str)
//│ ║ l.300: fun ill: ((Int | Bool, Int | Bool) -> Str) & ((Bool | Str, Bool | Str) -> Str)
//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ Type: ⊤

:e
fun id: [A] -> (A -> A) & (Int -> Int)
//│ ╔══[ERROR] Ill-formed functions intersection
//│ ║ l.311: fun id: [A] -> (A -> A) & (Int -> Int)
//│ ║ l.307: fun id: [A] -> (A -> A) & (Int -> Int)
//│ ╙── ^^^^^^^^^^^^^^^^^^^^^
//│ Type: ⊤

Expand All @@ -326,7 +322,7 @@ fst(cons(1, nil()))
:e
fun idInt: (Int -> Int) & (Int -> Int)
//│ ╔══[ERROR] Ill-formed functions intersection
//│ ║ l.327: fun idInt: (Int -> Int) & (Int -> Int)
//│ ║ l.323: fun idInt: (Int -> Int) & (Int -> Int)
//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^
//│ Type: ⊤

Expand All @@ -342,7 +338,7 @@ wf(true)
:e
wf(1)
//│ ╔══[ERROR] Type error in application
//│ ║ l.343: wf(1)
//│ ║ l.339: wf(1)
//│ ║ ^^^^^
//│ ╟── because: cannot constrain (((Int ∨ Bool) -> Int) ∨ (Bool -> Bool)) ∧ (Str -> Str) <: Int ->{'eff} 'app
//│ ╙── because: cannot constrain {0: Int} <: {0: Bool} ∨ {0: Str}
Expand All @@ -363,17 +359,45 @@ zs
:e
wf(zs, zs)
//│ ╔══[ERROR] Type error in application
//│ ║ l.364: wf(zs, zs)
//│ ║ l.360: wf(zs, zs)
//│ ║ ^^^^^^^^^^
//│ ╟── because: cannot constrain (((Z, Z) -> Z) ∧ ((Z, S) -> S)) ∧ ((S, Z ∨ S) -> S) <: (Z ∨ S, Z ∨ S) ->{'eff} 'app
//│ ╟── because: cannot constrain {0: Z ∨ S, 1: Z ∨ S} <: ({0: Z, 1: Z} ∨ {0: Z, 1: S}) ∨ {0: S, 1: Z ∨ S}
//│ ╟── because: cannot constrain {0: Z ∨ S, 1: Z ∨ S} <: {1: S}
//│ ╙── because: cannot constrain Z ∨ S <: S
//│ ╔══[ERROR] Type error in application
//│ ║ l.364: wf(zs, zs)
//│ ║ l.360: wf(zs, zs)
//│ ║ ^^^^^^^^^^
//│ ╟── because: cannot constrain (((Z, Z) -> Z) ∧ ((Z, S) -> S)) ∧ ((S, Z ∨ S) -> S) <: (Z ∨ S, Z ∨ S) ->{'eff} 'app
//│ ╟── because: cannot constrain {0: Z ∨ S, 1: Z ∨ S} <: ({0: Z, 1: Z} ∨ {0: Z, 1: S}) ∨ {0: S, 1: Z ∨ S}
//│ ╟── because: cannot constrain {0: Z ∨ S, 1: Z ∨ S} <: {1: Z}
//│ ╙── because: cannot constrain Z ∨ S <: Z
//│ Type: S ∨ Z

:e
fun ill:
(([a: Int, b:Int]) -> Int) &
(([b: Bool, c: Bool]) -> Bool) &
(([a: Str, c: Str]) -> Str)
//│ ╔══[ERROR] Ill-formed functions intersection
//│ ║ l.379: (([a: Int, b:Int]) -> Int) &
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ║ l.380: (([b: Bool, c: Bool]) -> Bool) &
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ║ l.381: (([a: Str, c: Str]) -> Str)
//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ Type: ⊤

:e
fun nested:
(([tag: [a: Int, b:Int]]) -> Int) &
(([tag: [b: Bool, c: Bool]]) -> Bool) &
(([tag: [a: Str, c: Str]]) -> Str)
//│ ╔══[ERROR] Ill-formed functions intersection
//│ ║ l.393: (([tag: [a: Int, b:Int]]) -> Int) &
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ║ l.394: (([tag: [b: Bool, c: Bool]]) -> Bool) &
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ║ l.395: (([tag: [a: Str, c: Str]]) -> Str)
//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ Type: ⊤
Loading
Loading