From e74015980186e302eed0fd3c750ad90332a01026 Mon Sep 17 00:00:00 2001 From: AU Heung Tung <101095686+auht@users.noreply.github.com> Date: Fri, 4 Oct 2024 20:47:09 +0800 Subject: [PATCH] guard with flag --- .../scala/mlscript/ConstraintSolver.scala | 64 +++--- .../main/scala/mlscript/TypeSimplifier.scala | 47 +++-- shared/src/main/scala/mlscript/Typer.scala | 16 +- shared/src/test/diff/fcp/Overloads.mls | 101 ++++----- .../src/test/diff/fcp/Overloads_Precise.mls | 197 ++++++++++++++++++ 5 files changed, 310 insertions(+), 115 deletions(-) create mode 100644 shared/src/test/diff/fcp/Overloads_Precise.mls diff --git a/shared/src/main/scala/mlscript/ConstraintSolver.scala b/shared/src/main/scala/mlscript/ConstraintSolver.scala index 13ec610c3..5d60ac1ff 100644 --- a/shared/src/main/scala/mlscript/ConstraintSolver.scala +++ b/shared/src/main/scala/mlscript/ConstraintSolver.scala @@ -861,24 +861,26 @@ class ConstraintSolver extends NormalForms { self: Typer => val newBound = (cctx._1 ::: cctx._2.reverse).foldRight(rhs)((c, ty) => if (c.prov is noProv) ty else mkProxy(ty, c.prov)) lhs.upperBounds ::= newBound // update the bound - lhs.tsc.foreachEntry { (tsc, v) => - v.foreach { i => - if (!tsc.tvs(i)._1) { - tsc.updateOn(i, rhs) - if (tsc.constraints.isEmpty) reportError() + if (noApproximateOverload) { + lhs.tsc.foreachEntry { (tsc, v) => + v.foreach { i => + if (!tsc.tvs(i)._1) { + tsc.updateOn(i, rhs) + if (tsc.constraints.isEmpty) reportError() + } } } - } - val u = lhs.tsc.keysIterator.filter(_.constraints.sizeCompare(1)===0).duplicate - u._1.foreach { k => - k.tvs.mapValuesIter(_.unwrapProxies).foreach { - case (_,tv: TV) => tv.tsc.remove(k) - case _ => () + val u = lhs.tsc.keysIterator.filter(_.constraints.sizeCompare(1)===0).duplicate + u._1.foreach { k => + k.tvs.mapValuesIter(_.unwrapProxies).foreach { + case (_,tv: TV) => tv.tsc.remove(k) + case _ => () + } } - } - u._2.foreach { k => - k.constraints.head.iterator.zip(k.tvs).foreach { - case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false) + u._2.foreach { k => + k.constraints.head.iterator.zip(k.tvs).foreach { + case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false) + } } } lhs.lowerBounds.foreach(rec(_, rhs, true)) // propagate from the bound @@ -888,24 +890,26 @@ class ConstraintSolver extends NormalForms { self: Typer => val newBound = (cctx._1 ::: cctx._2.reverse).foldLeft(lhs)((ty, c) => if (c.prov is noProv) ty else mkProxy(ty, c.prov)) rhs.lowerBounds ::= newBound // update the bound - rhs.tsc.foreachEntry { (tsc, v) => - v.foreach { i => - if(tsc.tvs(i)._1) { - tsc.updateOn(i, lhs) - if (tsc.constraints.isEmpty) reportError() + if (noApproximateOverload) { + rhs.tsc.foreachEntry { (tsc, v) => + v.foreach { i => + if(tsc.tvs(i)._1) { + tsc.updateOn(i, lhs) + if (tsc.constraints.isEmpty) reportError() + } } } - } - val u = rhs.tsc.keysIterator.filter(_.constraints.sizeCompare(1)===0).duplicate - u._1.foreach { k => - k.tvs.mapValuesIter(_.unwrapProxies).foreach { - case (_,tv: TV) => tv.tsc.remove(k) - case _ => () + val u = rhs.tsc.keysIterator.filter(_.constraints.sizeCompare(1)===0).duplicate + u._1.foreach { k => + k.tvs.mapValuesIter(_.unwrapProxies).foreach { + case (_,tv: TV) => tv.tsc.remove(k) + case _ => () + } } - } - u._2.foreach { k => - k.constraints.head.iterator.zip(k.tvs).foreach { - case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false) + u._2.foreach { k => + k.constraints.head.iterator.zip(k.tvs).foreach { + case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false) + } } } rhs.upperBounds.foreach(rec(lhs, _, true)) // propagate from the bound diff --git a/shared/src/main/scala/mlscript/TypeSimplifier.scala b/shared/src/main/scala/mlscript/TypeSimplifier.scala index 6b34a9473..f5a0bd813 100644 --- a/shared/src/main/scala/mlscript/TypeSimplifier.scala +++ b/shared/src/main/scala/mlscript/TypeSimplifier.scala @@ -79,15 +79,16 @@ trait TypeSimplifier { self: Typer => ).map(process(_, S(false -> tv))) .reduceOption(_ &- _).filterNot(_.isTop).toList else Nil - nv.tsc ++= tv.tsc.map { case (tsc, i) => renewedtsc.get(tsc) match { - case S(tsc) => (tsc, i) - case N if inPlace => (tsc, i) - case N => - val t = new TupleSetConstraints(tsc.constraints, tsc.tvs) - renewedtsc += tsc -> t - t.tvs = t.tvs.map(x => (x._1, process(x._2, N))) - (t, i) - }} + if (noApproximateOverload) + nv.tsc ++= tv.tsc.iterator.map { case (tsc, i) => renewedtsc.get(tsc) match { + case S(tsc) => (tsc, i) + case N if inPlace => (tsc, i) + case N => + val t = new TupleSetConstraints(tsc.constraints, tsc.tvs) + renewedtsc += tsc -> t + t.tvs = t.tvs.map(x => (x._1, process(x._2, N))) + (t, i) + }} } nv @@ -560,12 +561,14 @@ trait TypeSimplifier { self: Typer => if (pol(tv) =/= S(false)) analyzed1.setAndIfUnset(tv -> true) { tv.lowerBounds.foreach(apply(pol.at(tv.level, true))) - tv.tsc.keys.flatMap(_.tvs).foreach(u => apply(pol.at(tv.level,u._1))(u._2)) + if (noApproximateOverload) + tv.tsc.keys.flatMap(_.tvs).foreach(u => apply(pol.at(tv.level,u._1))(u._2)) } if (pol(tv) =/= S(true)) analyzed1.setAndIfUnset(tv -> false) { tv.upperBounds.foreach(apply(pol.at(tv.level, false))) - tv.tsc.keys.flatMap(_.tvs).foreach(u => apply(pol.at(tv.level,u._1))(u._2)) + if (noApproximateOverload) + tv.tsc.keys.flatMap(_.tvs).foreach(u => apply(pol.at(tv.level,u._1))(u._2)) } } case _ => @@ -660,7 +663,8 @@ trait TypeSimplifier { self: Typer => case S(pol_tv) => if (analyzed2.add(pol_tv -> tv)) { processImpl(st, pol, pol_tv) - tv.tsc.keys.flatMap(_.tvs).foreach(u => processImpl(u._2,pol.at(tv.level,u._1),pol_tv)) + if (noApproximateOverload) + tv.tsc.keys.flatMap(_.tvs).foreach(u => processImpl(u._2,pol.at(tv.level,u._1),pol_tv)) } case N => if (analyzed2.add(true -> tv)) @@ -707,7 +711,7 @@ trait TypeSimplifier { self: Typer => case S(p) => (if (p) tv2.lowerBounds else tv2.upperBounds).foreach(go) // (if (p) getLbs(tv2) else getUbs(tv2)).foreach(go) - tv2.tsc.keys.flatMap(_.tvs).foreach(u => go(u._2)) + if (noApproximateOverload) tv2.tsc.keys.flatMap(_.tvs).foreach(u => go(u._2)) case N => trace(s"Analyzing invar-occ of $tv2") { analyze2(tv2, pol) @@ -1038,14 +1042,15 @@ trait TypeSimplifier { self: Typer => res.lowerBounds = tv.lowerBounds.map(transform(_, pol.at(tv.level, true), Set.single(tv))) if (occNums.contains(false -> tv)) res.upperBounds = tv.upperBounds.map(transform(_, pol.at(tv.level, false), Set.single(tv))) - res.tsc ++= tv.tsc.map { case (tsc, i) => renewaltsc.get(tsc) match { - case S(tsc) => (tsc, i) - case N => - val t = new TupleSetConstraints(tsc.constraints, tsc.tvs) - renewaltsc += tsc -> t - t.tvs = t.tvs.map(x => (x._1, transform(x._2, PolMap.neu, Set.empty))) - (t, i) - }} + if (noApproximateOverload) + res.tsc ++= tv.tsc.map { case (tsc, i) => renewaltsc.get(tsc) match { + case S(tsc) => (tsc, i) + case N => + val t = new TupleSetConstraints(tsc.constraints, tsc.tvs) + renewaltsc += tsc -> t + t.tvs = t.tvs.map(x => (x._1, transform(x._2, PolMap.neu, Set.empty))) + (t, i) + }} } res }() diff --git a/shared/src/main/scala/mlscript/Typer.scala b/shared/src/main/scala/mlscript/Typer.scala index 380590558..af88e803b 100644 --- a/shared/src/main/scala/mlscript/Typer.scala +++ b/shared/src/main/scala/mlscript/Typer.scala @@ -170,13 +170,15 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne if (p) (b, tv) else (tv, b) } }.toList, innerTy) - val ambiguous = innerTy.getVars.unsorted.flatMap(_.tsc.keys.flatMap(_.tvs)) - .groupBy(_._2) - .filter { case (v,pvs) => pvs.sizeIs > 1 } - if (ambiguous.nonEmpty) raise(ErrorReport( - msg"ambiguous" -> N :: - ambiguous.map { case (v,_) => msg"cannot determine satisfiability of type ${v.expPos}" -> v.prov.loco }.toList - , true)) + if (noApproximateOverload) { + val ambiguous = innerTy.getVars.unsorted.flatMap(_.tsc.keys.flatMap(_.tvs)) + .groupBy(_._2) + .filter { case (v,pvs) => pvs.sizeIs > 1 } + if (ambiguous.nonEmpty) raise(ErrorReport( + msg"ambiguous" -> N :: + ambiguous.map { case (v,_) => msg"cannot determine satisfiability of type ${v.expPos}" -> v.prov.loco }.toList + , true)) + } println(s"Inferred poly constr: $cty —— where ${cty.showBounds}") diff --git a/shared/src/test/diff/fcp/Overloads.mls b/shared/src/test/diff/fcp/Overloads.mls index a74fbc536..d000a52f9 100644 --- a/shared/src/test/diff/fcp/Overloads.mls +++ b/shared/src/test/diff/fcp/Overloads.mls @@ -1,6 +1,6 @@ :NoJS -:NoApproximateOverload + type IISS = int -> int & string -> string type BBNN = bool -> bool & number -> number @@ -31,37 +31,22 @@ IISS : ZZII //│ ╔══[ERROR] Type mismatch in type ascription: //│ ║ l.30: IISS : ZZII //│ ║ ^^^^ -//│ ╟── type `int -> int & string -> string` is not an instance of `0 -> 0` +//│ ╟── type `int` does not match type `0` //│ ║ l.12: def IISS: int -> int & string -> string -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── but it flows into reference with expected type `0 -> 0` -//│ ║ l.30: IISS : ZZII -//│ ║ ^^^^ -//│ ╟── Note: constraint arises from function type: +//│ ║ ^^^ +//│ ╟── Note: constraint arises from literal type: //│ ║ l.7: type ZZII = 0 -> 0 & int -> int -//│ ║ ^^^^^^ -//│ ╟── from type reference: -//│ ║ l.30: IISS : ZZII -//│ ╙── ^^^^ +//│ ╙── ^ //│ res: ZZII :e IISS : BBNN //│ ╔══[ERROR] Type mismatch in type ascription: -//│ ║ l.49: IISS : BBNN -//│ ║ ^^^^ -//│ ╟── type `int -> int & string -> string` is not an instance of `bool -> bool` -//│ ║ l.12: def IISS: int -> int & string -> string -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── but it flows into reference with expected type `bool -> bool` -//│ ║ l.49: IISS : BBNN +//│ ║ l.43: IISS : BBNN //│ ║ ^^^^ -//│ ╟── Note: constraint arises from function type: +//│ ╟── type `bool` does not match type `int | string` //│ ║ l.6: type BBNN = bool -> bool & number -> number -//│ ║ ^^^^^^^^^^^^ -//│ ╟── from type reference: -//│ ║ l.49: IISS : BBNN -//│ ╙── ^^^^ +//│ ╙── ^^^^ //│ res: BBNN @@ -74,18 +59,16 @@ IISS : (0 | 1) -> number //│ res: (0 | 1) -> number IISS : 'a -> 'a -//│ res: 'a -> 'a -//│ where -//│ [-'a, +'a] in {[int, int], [string, string]} +//│ res: ('a & (int | string)) -> (int | string | 'a) IISS 0 -//│ res: int +//│ res: int | string (IISS : int -> int) 0 //│ res: int (if true then IISS else BBNN) 0 -//│ res: number +//│ res: bool | number | string // * Note that this is not considered ambiguous // * because the type variable occurrences are polar, @@ -94,38 +77,48 @@ IISS 0 // * Conceptually, we'd expect this inferred type to reduce to `int -> number`, // * but it's tricky to do such simplifications in general. def f = fun x -> (if true then IISS else BBNN) x -//│ f: 'a -> 'b -//│ where -//│ [+'a, -'b] in {[int, int], [string, string]} -//│ [+'a, -'b] in {[bool, bool], [number, number]} +//│ f: int -> (bool | number | string) f(0) -//│ res: number +//│ res: bool | number | string -// FIXME +:e f(0) + 1 //│ ╔══[ERROR] Type mismatch in operator application: -//│ ║ l.106: f(0) + 1 -//│ ║ ^^^^^^ -//│ ╟── type `number` is not an instance of type `int` +//│ ║ l.86: f(0) + 1 +//│ ║ ^^^^^^ +//│ ╟── type `bool` is not an instance of type `int` //│ ║ l.13: def BBNN: bool -> bool & number -> number -//│ ║ ^^^^^^ +//│ ║ ^^^^ //│ ╟── but it flows into application with expected type `int` -//│ ║ l.106: f(0) + 1 -//│ ╙── ^^^^ +//│ ║ l.86: f(0) + 1 +//│ ╙── ^^^^ //│ res: error | int +:e f : int -> number +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.99: f : int -> number +//│ ║ ^ +//│ ╟── type `bool` is not an instance of type `number` +//│ ║ l.13: def BBNN: bool -> bool & number -> number +//│ ║ ^^^^ +//│ ╟── Note: constraint arises from type reference: +//│ ║ l.99: f : int -> number +//│ ╙── ^^^^^^ //│ res: int -> number :e f : number -> int //│ ╔══[ERROR] Type mismatch in type ascription: -//│ ║ l.122: f : number -> int +//│ ║ l.112: f : number -> int //│ ║ ^ -//│ ╟── type `number` does not match type `?a` -//│ ║ l.122: f : number -> int -//│ ╙── ^^^^^^ +//│ ╟── type `number` does not match type `int | string` +//│ ║ l.112: f : number -> int +//│ ║ ^^^^^^ +//│ ╟── Note: constraint arises from reference: +//│ ║ l.79: def f = fun x -> (if true then IISS else BBNN) x +//│ ╙── ^ //│ res: number -> int @@ -141,17 +134,11 @@ if true then IISS else BBNN :e (if true then IISS else BBNN) : (0 | 1 | true) -> number //│ ╔══[ERROR] Type mismatch in type ascription: -//│ ║ l.142: (if true then IISS else BBNN) : (0 | 1 | true) -> number +//│ ║ l.135: (if true then IISS else BBNN) : (0 | 1 | true) -> number //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── type `int -> int & string -> string` is not an instance of `(0 | 1 | true) -> number` -//│ ║ l.12: def IISS: int -> int & string -> string -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── but it flows into reference with expected type `(0 | 1 | true) -> number` -//│ ║ l.142: (if true then IISS else BBNN) : (0 | 1 | true) -> number -//│ ║ ^^^^ -//│ ╟── Note: constraint arises from function type: -//│ ║ l.142: (if true then IISS else BBNN) : (0 | 1 | true) -> number -//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── type `true` does not match type `int | string` +//│ ║ l.135: (if true then IISS else BBNN) : (0 | 1 | true) -> number +//│ ╙── ^^^^ //│ res: (0 | 1 | true) -> number @@ -169,13 +156,13 @@ not test //│ <: test: //│ ~(int -> int) //│ ╔══[ERROR] Type mismatch in application: -//│ ║ l.167: not test +//│ ║ l.154: not test //│ ║ ^^^^^^^^ //│ ╟── type `~(int -> int)` is not an instance of type `bool` -//│ ║ l.161: def test: ~(int -> int) +//│ ║ l.148: def test: ~(int -> int) //│ ║ ^^^^^^^^^^^^^ //│ ╟── but it flows into reference with expected type `bool` -//│ ║ l.167: not test +//│ ║ l.154: not test //│ ╙── ^^^^ //│ res: bool | error diff --git a/shared/src/test/diff/fcp/Overloads_Precise.mls b/shared/src/test/diff/fcp/Overloads_Precise.mls new file mode 100644 index 000000000..d24fc5dfc --- /dev/null +++ b/shared/src/test/diff/fcp/Overloads_Precise.mls @@ -0,0 +1,197 @@ + +:NoJS +:NoApproximateOverload + +type IISS = int -> int & string -> string +type BBNN = bool -> bool & number -> number +type ZZII = 0 -> 0 & int -> int +//│ Defined type alias IISS +//│ Defined type alias BBNN +//│ Defined type alias ZZII + +def IISS: int -> int & string -> string +def BBNN: bool -> bool & number -> number +def ZZII: 0 -> 0 & int -> int +//│ IISS: int -> int & string -> string +//│ BBNN: bool -> bool & number -> number +//│ ZZII: 0 -> 0 & int -> int + + +IISS : IISS +//│ res: IISS + +IISS : int -> int & string -> string +//│ res: int -> int & string -> string + +IISS : IISS | BBNN +//│ res: BBNN | IISS + +:e +IISS : ZZII +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.30: IISS : ZZII +//│ ║ ^^^^ +//│ ╟── type `int -> int & string -> string` is not an instance of `0 -> 0` +//│ ║ l.12: def IISS: int -> int & string -> string +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── but it flows into reference with expected type `0 -> 0` +//│ ║ l.30: IISS : ZZII +//│ ║ ^^^^ +//│ ╟── Note: constraint arises from function type: +//│ ║ l.7: type ZZII = 0 -> 0 & int -> int +//│ ║ ^^^^^^ +//│ ╟── from type reference: +//│ ║ l.30: IISS : ZZII +//│ ╙── ^^^^ +//│ res: ZZII + +:e +IISS : BBNN +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.49: IISS : BBNN +//│ ║ ^^^^ +//│ ╟── type `int -> int & string -> string` is not an instance of `bool -> bool` +//│ ║ l.12: def IISS: int -> int & string -> string +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── but it flows into reference with expected type `bool -> bool` +//│ ║ l.49: IISS : BBNN +//│ ║ ^^^^ +//│ ╟── Note: constraint arises from function type: +//│ ║ l.6: type BBNN = bool -> bool & number -> number +//│ ║ ^^^^^^^^^^^^ +//│ ╟── from type reference: +//│ ║ l.49: IISS : BBNN +//│ ╙── ^^^^ +//│ res: BBNN + + +// * These tests show that we currently throw away information when constraining LHS overloading sets: + +IISS : int -> int +//│ res: int -> int + +IISS : (0 | 1) -> number +//│ res: (0 | 1) -> number + +IISS : 'a -> 'a +//│ res: 'a -> 'a +//│ where +//│ [-'a, +'a] in {[int, int], [string, string]} + +IISS 0 +//│ res: int + +(IISS : int -> int) 0 +//│ res: int + +(if true then IISS else BBNN) 0 +//│ res: number + +// * Note that this is not considered ambiguous +// * because the type variable occurrences are polar, +// * meaning that the TSCs are always trivially satisfiable +// * and thus the code is well-typed. +// * Conceptually, we'd expect this inferred type to reduce to `int -> number`, +// * but it's tricky to do such simplifications in general. +def f = fun x -> (if true then IISS else BBNN) x +//│ f: 'a -> 'b +//│ where +//│ [+'a, -'b] in {[int, int], [string, string]} +//│ [+'a, -'b] in {[bool, bool], [number, number]} + +f(0) +//│ res: number + +:e +f(0) + 1 +//│ ╔══[ERROR] Type mismatch in operator application: +//│ ║ l.106: f(0) + 1 +//│ ║ ^^^^^^ +//│ ╟── type `number` is not an instance of type `int` +//│ ║ l.13: def BBNN: bool -> bool & number -> number +//│ ║ ^^^^^^ +//│ ╟── but it flows into application with expected type `int` +//│ ║ l.106: f(0) + 1 +//│ ╙── ^^^^ +//│ res: error | int + +f : int -> number +//│ res: int -> number + +:e +f : number -> int +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.122: f : number -> int +//│ ║ ^ +//│ ╟── type `number` does not match type `?a` +//│ ║ l.122: f : number -> int +//│ ╙── ^^^^^^ +//│ res: number -> int + + +if true then IISS else BBNN +//│ res: bool -> bool & number -> number | int -> int & string -> string + +(if true then IISS else ZZII) : int -> int +//│ res: int -> int + +(if true then IISS else BBNN) : (0 | 1) -> number +//│ res: (0 | 1) -> number + +:e +(if true then IISS else BBNN) : (0 | 1 | true) -> number +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.142: (if true then IISS else BBNN) : (0 | 1 | true) -> number +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── type `int -> int & string -> string` is not an instance of `(0 | 1 | true) -> number` +//│ ║ l.12: def IISS: int -> int & string -> string +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── but it flows into reference with expected type `(0 | 1 | true) -> number` +//│ ║ l.142: (if true then IISS else BBNN) : (0 | 1 | true) -> number +//│ ║ ^^^^ +//│ ╟── Note: constraint arises from function type: +//│ ║ l.142: (if true then IISS else BBNN) : (0 | 1 | true) -> number +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^ +//│ res: (0 | 1 | true) -> number + + +// * Note that type normalization used to be very aggressive at approximating non-tag type negations, +// * to simplify the result, but this was changed as it was unsound + +def test: ~(int -> int) +//│ test: ~(int -> int) + +// * See also test file BooleanFail.mls about this previous unsoundness +:e +test = 42 +not test +//│ 42 +//│ <: test: +//│ ~(int -> int) +//│ ╔══[ERROR] Type mismatch in application: +//│ ║ l.167: not test +//│ ║ ^^^^^^^^ +//│ ╟── type `~(int -> int)` is not an instance of type `bool` +//│ ║ l.161: def test: ~(int -> int) +//│ ║ ^^^^^^^^^^^^^ +//│ ╟── but it flows into reference with expected type `bool` +//│ ║ l.167: not test +//│ ╙── ^^^^ +//│ res: bool | error + +def test: ~(int -> int) & ~bool +//│ test: ~bool & ~(int -> int) + +def test: ~(int -> int) & bool +//│ test: bool + +def test: ~(int -> int) & ~(bool -> bool) +//│ test: ~(nothing -> (bool | int)) + +def test: ~(int -> int | bool -> bool) +//│ test: ~(nothing -> (bool | int)) + +def test: ~(int -> int & string -> string) & ~(bool -> bool & number -> number) +//│ test: in ~(nothing -> (number | string) & int -> number & nothing -> (bool | string) & nothing -> (bool | int)) out ~(nothing -> (bool | int) & nothing -> (bool | string) & int -> number & nothing -> (number | string)) + +