diff --git a/hkmc2/shared/src/main/scala/hkmc2/Config.scala b/hkmc2/shared/src/main/scala/hkmc2/Config.scala index 60904006f6..2df87d2504 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/Config.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/Config.scala @@ -12,6 +12,7 @@ case class Config( sanityChecks: Opt[SanityChecks], effectHandlers: Opt[EffectHandlers], liftDefns: Opt[LiftDefns], + simplifyTypes: Bool, ): def stackSafety: Opt[StackSafety] = effectHandlers.flatMap(_.stackSafety) @@ -26,6 +27,7 @@ object Config: // sanityChecks = S(SanityChecks(light = true)), effectHandlers = N, liftDefns = N, + simplifyTypes = true, ) case class SanityChecks(light: Bool) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala index 186992bc9f..b77a91eaf9 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala @@ -70,10 +70,16 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State, else v.state.lowerBounds ::= nv nv.state.upperBounds = v.state.upperBounds.map(extrude) // * propagate + nv.state.disjsub ++= v.state.disjsub.map: + case DisjSub(ds, dss, cs) => + val d = ds.mapKeys(v0 => if v === v0 then nv else v0) + DisjSub(mutable.LinkedHashSet.from(d), dss, cs) + nv.state.disjsub.foreach(_.commit()) nv }) case ft @ FunType(args, ret, eff) => FunType(args.map(arg => extrude(arg)(using lvl, !pol)), extrude(ret), extrude(eff)) + case RcdType(u) => RcdType(u.mapValues(extrude)) case ComposedType(lhs, rhs, p) => Type.mkComposedType(extrude(lhs), extrude(rhs), p) case NegType(ty) => Type.mkNegType(extrude(ty)(using lvl, !pol)) @@ -97,26 +103,73 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State, cctx.nest(bd -> v) givenIn: v.state.lowerBounds ::= bd v.state.upperBounds.foreach(ub => constrainImpl(bd, ub)) + val (dss, cs) = v.state.disjsub.toList.map(_.check(Map(v -> bd))).unzip + dss.flatten.foreach(_.commit()) + cs.flatten.foreach(u => constrainImpl(u._1, u._2)) case Conj(i, u, Nil) => (conj.i, conj.u) match - case (_, Union(N, Nil)) => + case (_, Union(N, Nil, Nil)) => // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} ∧ ¬⊥" -> N :: Nil)) cctx.err - case (Inter(S(ClassLikeType(cls1, targs1))), Union(f, ClassLikeType(cls2, targs2) :: rest)) => + case (Inter(S(ClassLikeType(cls1, targs1))), Union(f, ClassLikeType(cls2, targs2) :: rest, rcd)) => if cls1.uid === cls2.uid then targs1.zip(targs2).foreach: (ta1, ta2) => constrainArgs(ta1, ta2) - else constrainConj(Conj(conj.i, Union(f, rest), Nil)) - case (int: Inter, Union(f, _ :: rest)) => constrainConj(Conj(int, Union(f, rest), Nil)) - case (Inter(S(FunType(args1, ret1, eff1))), Union(S(FunType(args2, ret2, eff2)), Nil)) => - if args1.length =/= args2.length then - // raise(ErrorReport(msg"Cannot constrain ${conj.i.toString()} <: ${conj.u.toString()}" -> N :: Nil)) - cctx.err + else constrainConj(Conj(conj.i, Union(f, rest, rcd), Nil)) + case (int: Inter, Union(f, _ :: rest, rcd)) => constrainConj(Conj(int, Union(f, rest, rcd), Nil)) + case (Inter(S(RcdType(u))), Union(f, Nil, RcdType(w) :: Nil)) => + val um = u.toMap + val wm = w.toMap + val k = w.keys.toSet + if k.subsetOf(um.keySet) then + k.foreach(k => constrainImpl(um(k), wm(k))) + else cctx.err + case (Inter(S(u: RcdType)), Union(f, Nil, rs)) => + val us = u.fields.keys.toSet + val ws = rs.filter(_.fields.keys.forall(us)) + if ws.isEmpty then cctx.err else - args1.zip(args2).foreach { - case (a1, a2) => constrainImpl(a2, a1) - } - constrainImpl(ret1, ret2) - constrainImpl(eff1, eff2) + val q = ws.foldLeft(Bot: Type): (q, w) => + val wq = Type.discriminant(w) + Type.disjoint(wq, u).foreach: k => + if k.isEmpty then constrainImpl(u & wq, w) + else DisjSub(mutable.LinkedHashSet.from(k), Nil, Ls(wq -> w)).commit() + q | wq + Type.disjoint(q.!, u).foreach: k => + if k.isEmpty then constrainImpl(Top, Bot) + else DisjSub(mutable.LinkedHashSet.from(k), Nil, Ls(Top -> Bot)).commit() + case (Inter(S(fs: Ls[FunType])), Union(S(FunType(args2, ret2, eff2)), Nil, Nil)) => + val k = args2.map(x => Type.disjoint(x, x)) + if k.forall(_.nonEmpty) then + val f = fs.filter(_.args.length === args2.length) + if args2.isEmpty then + if f.isEmpty then + cctx.err + else f.foreach: f => + constrainImpl(f.ret, ret2) + constrainImpl(f.eff, eff2) + else + val args = f.map(x => RcdType(x.args.zipWithIndex.map(u => (s"${u._2}", u._1)))) + val args2r = args2.zipWithIndex.map(u => (s"${u._2}", u._1)) + val args2q = RcdType(args2r) + val (cs, dss) = (args.iterator.map(Type.discriminant).zip(f).map: + case (q, f) => + val cs = (f.ret, ret2) :: (f.eff, eff2) :: Nil + val ds = Type.disjoint(q, args2q) + if ds.exists(_.isEmpty) then (cs, Nil) + else (Nil, ds.map(k => DisjSub(mutable.LinkedHashSet.from(k), Nil, cs)))).toList.unzip + val c = (args2q, args.foldLeft(Bot: Type)(_ | _)) + val u = k.foldLeft(Set(Set.empty[InfVar -> BasicType]))((x, y) => y.flatMap(y => x.map(_ ++ y))) + if u.exists(_.isEmpty) then + if f.isEmpty then + cctx.err + else + dss.flatten.foreach(_.commit()) + constrainImpl(c._1, c._2) + cs.flatten.foreach(u => constrainImpl(u._1, u._2)) + else + val cs0 = c :: cs.flatten + val dss0 = dss.flatten + u.foreach(k => DisjSub(mutable.LinkedHashSet.from(k), dss0, cs0).commit()) case _ => // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} <: ${conj.u.toString()}" -> N :: Nil)) cctx.err @@ -134,7 +187,7 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State, inlineSkolemBounds(if pol then state.upperBounds.foldLeft[Type](v)(_ & _) else state.lowerBounds.foldLeft[Type](v)(_ | _), pol) case ComposedType(lhs, rhs, p) => ComposedType(inlineSkolemBounds(lhs, pol), inlineSkolemBounds(rhs, pol), p) case NegType(ty) => NegType(inlineSkolemBounds(ty, !pol)) - case _: ClassLikeType | _: FunType | _: InfVar | Top | Bot => ty + case _: ClassLikeType | _: FunType | _: RcdType |_: InfVar | Top | Bot => ty private def constrainImpl(lhs: Type, rhs: Type)(using BbCtx, CCtx, TL): Unit = if cctx.cache((lhs, rhs)) then log(s"Cached!") diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala index 78c0588dc6..ae5f7f3585 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala @@ -76,28 +76,36 @@ object Conj: }){} lazy val empty: Conj = Conj(Inter.empty, Union.empty, Nil) def mkVar(v: InfVar, pol: Bool) = Conj(Inter.empty, Union.empty, (v, pol) :: Nil) - def mkInter(inter: ClassLikeType | FunType) = + def mkInter(inter: ClassLikeType | Ls[FunType] | RcdType) = Conj(Inter(S(inter)), Union.empty, Nil) - def mkUnion(union: ClassLikeType | FunType) = + def mkUnion(union: ClassLikeType | FunType | RcdType) = Conj(Inter.empty, union match { - case cls: ClassLikeType => Union(N, cls :: Nil) - case fun: FunType => Union(S(fun), Nil) + case cls: ClassLikeType => Union(N, cls :: Nil, Nil) + case fun: FunType => Union(S(fun), Nil, Nil) + case r: RcdType => Union(N, Nil, Ls(r)) }, Nil) // * Some(ClassType) -> C[in D_i out D_i], Some(FunType) -> D_1 ->{D_2} D_3, None -> Top -final case class Inter(v: Opt[ClassLikeType | FunType]) extends NormalForm: +final case class Inter(v: Opt[ClassLikeType | Ls[FunType] | RcdType]) extends NormalForm: def isTop: Bool = v.isEmpty def merge(other: Inter): Option[Inter] = (v, other.v) match case (S(ClassLikeType(cls1, targs1)), S(ClassLikeType(cls2, targs2))) if cls1.uid === cls2.uid => S(Inter(S(ClassLikeType(cls1, targs1.lazyZip(targs2).map(_ & _))))) case (S(_: ClassLikeType), S(_: ClassLikeType)) => N - case (S(FunType(a1, r1, e1)), S(FunType(a2, r2, e2))) => - S(Inter(S(FunType(a1.lazyZip(a2).map(_ | _), r1 & r2, e1 & e2)))) + // case (S(FunType(a1, r1, e1)), S(FunType(a2, r2, e2))) => + // S(Inter(S(FunType(a1.lazyZip(a2).map(_ | _), r1 & r2, e1 & e2)))) + case (S(a: Ls[FunType]), S(b: Ls[FunType])) => S(Inter(S(a ++ b))) + case (S(a: RcdType), S(b: RcdType)) => S(Inter(S(a & b))) case (S(v), N) => S(Inter(S(v))) case (N, v) => S(Inter(v)) case _ => N - def toBasic: BasicType = v.getOrElse(Top) - def toDnf(using TL): Disj = Disj(Conj(this, Union(N, Nil), Nil) :: Nil) + def toBasic: BasicType = v match + case N => Top + case S(x: ClassLikeType) => x + case S(Nil) => Top + case S(x: Ls[FunType]) => x.reduce[Type](_&_).toBasic + case S(x: RcdType) => x + def toDnf(using TL): Disj = Disj(Conj(this, Union(N, Nil, Nil), Nil) :: Nil) override def show(using Scope): Str = toBasic.show @@ -106,11 +114,11 @@ object Inter: lazy val empty: Inter = Inter(N) // * fun: Some(FunType) -> D_1 ->{D_2} D_3, None -> bot -final case class Union(fun: Opt[FunType], cls: Ls[ClassLikeType]) +final case class Union(fun: Opt[FunType], cls: Ls[ClassLikeType], rcd: Ls[RcdType]) extends NormalForm with CachedBasicType: - def isBot = fun.isEmpty && cls.isEmpty + def isBot = fun.isEmpty && cls.isEmpty && rcd.isEmpty def toType = fun.getOrElse(Bot) | - cls.foldLeft[Type](Bot)(_ | _) + cls.foldLeft[Type](Bot)(_ | _) | rcd.foldLeft[Type](Bot)(_ | _) def merge(other: Union): Union = Union((fun, other.fun) match { case (S(FunType(a1, r1, e1)), S(FunType(a2, r2, e2))) => S(FunType(a1.lazyZip(a2).map(_ & _), r1 | r2, e1 | e2)) @@ -121,19 +129,19 @@ extends NormalForm with CachedBasicType: case (cls1, cls2) => cls1.name.uid <= cls2.name.uid }.foldLeft[Ls[ClassLikeType]](Nil)((res, cls) => (res, cls) match { case (Nil, cls) => cls :: Nil - case (ClassLikeType(cls1, targs1) :: tail, ClassLikeType(cls2, targs2)) if cls1.uid === cls2.uid => + case (ClassLikeType(cls1, targs1) :: tail, ClassLikeType(cls2, targs2)) if cls1.uid === cls2.uid => ClassLikeType(cls1, targs1.lazyZip(targs2).map(_ | _)) :: tail case (head :: tail, cls) => cls :: head :: tail - })) + }), rcd ++ other.rcd) def mkBasic: BasicType = - BasicType.union(fun.toList ::: cls) + BasicType.union(fun.toList ::: cls ::: rcd) def toDnf(using TL): Disj = NormalForm.neg(this) override def show(using Scope): Str = toType.show override def showDbg: Str = toType.showDbg object Union: - val empty: Union = Union(N, Nil) + val empty: Union = Union(N, Nil, Nil) sealed abstract class NormalForm extends TypeExt: def toBasic: BasicType @@ -167,6 +175,7 @@ object NormalForm: case v: InfVar => Disj(Conj.mkVar(v, false) :: Nil) case ct: ClassLikeType => Disj(Conj.mkUnion(ct) :: Nil) case ft: FunType => Disj(Conj.mkUnion(ft) :: Nil) + case r: RcdType => Disj(Conj.mkUnion(r) :: Nil) case ComposedType(lhs, rhs, pol) => if pol then inter(neg(lhs), neg(rhs)) else union(neg(lhs), neg(rhs)) case NegType(ty) => dnf(ty) @@ -176,13 +185,14 @@ object NormalForm: ty match case d: Disj => d case c: Conj => Disj(c :: Nil) - case i: Inter => Disj(Conj(i, Union(N, Nil), Nil) :: Nil) + case i: Inter => Disj(Conj(i, Union(N, Nil, Nil), Nil) :: Nil) case _ => ty.toBasic match case Top => Disj.top case Bot => Disj.bot case v: InfVar => Disj(Conj.mkVar(v, true) :: Nil) case ct: ClassLikeType => Disj(Conj.mkInter(ct.toNorm) :: Nil) - case ft: FunType => Disj(Conj.mkInter(ft.toNorm) :: Nil) + case ft: FunType => Disj(Conj.mkInter(Ls(ft.toNorm)) :: Nil) + case r: RcdType => Disj(Conj.mkInter(r.toNorm) :: Nil) case ComposedType(lhs, rhs, pol) => if pol then union(dnf(lhs), dnf(rhs)) else inter(dnf(lhs), dnf(rhs)) case NegType(ty) => neg(ty) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/PrettyPrinter.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/PrettyPrinter.scala index 80d011d4ad..1a8219c947 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/PrettyPrinter.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/PrettyPrinter.scala @@ -4,6 +4,12 @@ import scala.collection.mutable.{Set => MutSet, ListBuffer} import utils.Scope class PrettyPrinter(output: String => Unit)(using Scope): + def showDisjSub(ds: DisjSub): String = ds match + case DisjSub(d, dss, cs) => + val g = d.iterator.map { case (x, y) => s"${x.show}#${y.show} ∨ " }.mkString + val h = dss.iterator.map("(" + showDisjSub(_) + ")").mkString(" ∧ ") + val b = cs.iterator.map{ case (x, y) => s"${x.simp.show} <: ${y.simp.show}" }.mkString(" ∧ ") + s" $g$h$b" def print(ty: GeneralType): Unit = output(s"Type: ${ty.show}") val bounds = PrettyPrinter.collectBounds(ty).distinct @@ -11,6 +17,7 @@ class PrettyPrinter(output: String => Unit)(using Scope): output("Where:") bounds.foreach { case (lhs, rhs) => output(s" ${lhs.show} <: ${rhs.show}") + case ds: DisjSub => output(showDisjSub(ds)) } object PrettyPrinter: @@ -18,8 +25,8 @@ object PrettyPrinter: type Bound = (Type, Type) // * Type <: Type - private def collectBounds(ty: GeneralType): List[Bound] = - val res = ListBuffer[Bound]() + private def collectBounds(ty: GeneralType): List[Bound | DisjSub] = + val res = ListBuffer[Bound | DisjSub]() val cache = MutSet[Uid[InfVar]]() object CollectBounds extends TypeTraverser: override def apply(pol: Boolean)(ty: GeneralType): Unit = ty match @@ -31,6 +38,10 @@ object PrettyPrinter: res ++= state.upperBounds.map: bd => apply(false)(bd) (v, bd) + res ++= state.disjsub + val (p, n) = state.disjsub.map(_.children()).unzip + p.flatten.foreach(apply(true)) + n.flatten.foreach(apply(false)) super.apply(pol)(ty) case _ => super.apply(pol)(ty) CollectBounds(true)(ty) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala index 229f914766..c78b2cf107 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala @@ -14,7 +14,7 @@ final def printPol(pol: Bool): Str = pol match { case false => "-" } -class TypeSimplifier(tl: TraceLogger): +class TypeSimplifier(using tl: TL): import tl.{trace, log} def apply(pol: Bool, lvl: Int)(ty: GeneralType): GeneralType = @@ -60,6 +60,8 @@ class TypeSimplifier(tl: TraceLogger): val varSubst: MutMap[IV, IV] = MutMap.empty val traversedTVs: MutSet[IV] = MutSet.empty + + val traversedDisjSub: MutSet[DisjSub] = MutSet.empty def getRepr(tv: IV): IV = varSubst.get(tv) match { case S(tv2) => @@ -129,6 +131,13 @@ class TypeSimplifier(tl: TraceLogger): // traversingTVs += tv // traversedTVs += tv super.apply(pol)(ty) + val (p, n) = (tv.state.disjsub.flatMap: ds => + ds.subDisjSub.map: k => + if traversedDisjSub.add(ds) then + ds.children() + else (Nil, Nil)).unzip + p.flatten.foreach(apply(true)) + n.flatten.foreach(apply(false)) // traversingTVs -= tv curPath = oldPath case pt @ PolyType(tvs, outer, _) => // Avoid simplify outer variables to Top unexpectedly @@ -191,15 +200,17 @@ class TypeSimplifier(tl: TraceLogger): tv.state.upperBounds = newUBs val isPos = Analysis.posVars.contains(tv) val isNeg = Analysis.negVars.contains(tv) - // if (isPos && !isNeg && (Analysis.occsNum(tv) === 1 && {newLBs match { case (tv: IV) :: Nil => true; case _ => false }} || newLBs.forall(_.isSmall))) { - if isPos && !isNeg && ({newLBs match { case (tv: IV) :: Nil => true; case _ => false }} || newLBs.forall(_ => true)) then { - // if (isPos && !isNeg && ({newLBs match { case (tv: IV) :: Nil => true; case _ => false }})) { - newLBs.foldLeft(Bot: Type)(_ | _) - } else - // if (isNeg && !isPos && (Analysis.occsNum(tv) === 1 && {newUBs match { case (tv: IV) :: Nil => true; case _ => false }} || newUBs.forall(_.isSmall))) { - if isNeg && !isPos && ({newUBs match { case (tv: IV) :: Nil => true; case _ => false }} || newUBs.forall(_ => true)) then - // if (isNeg && !isPos && ({newUBs match { case (tv: IV) :: Nil => true; case _ => false }})) { - newUBs.foldLeft(Top: Type)(_ & _) + if tv.state.disjsub.isEmpty then + // if (isPos && !isNeg && (Analysis.occsNum(tv) === 1 && {newLBs match { case (tv: IV) :: Nil => true; case _ => false }} || newLBs.forall(_.isSmall))) { + if isPos && !isNeg && ({newLBs match { case (tv: IV) :: Nil => true; case _ => false }} || newLBs.forall(_ => true)) then { + // if (isPos && !isNeg && ({newLBs match { case (tv: IV) :: Nil => true; case _ => false }})) { + newLBs.foldLeft(Bot: Type)(_ | _) + } else + // if (isNeg && !isPos && (Analysis.occsNum(tv) === 1 && {newUBs match { case (tv: IV) :: Nil => true; case _ => false }} || newUBs.forall(_.isSmall))) { + if isNeg && !isPos && ({newUBs match { case (tv: IV) :: Nil => true; case _ => false }} || newUBs.forall(_ => true)) then + // if (isNeg && !isPos && ({newUBs match { case (tv: IV) :: Nil => true; case _ => false }})) { + newUBs.foldLeft(Top: Type)(_ & _) + else tv else // tv.lowerBounds = newLBs // tv.upperBounds = newUBs @@ -211,7 +222,7 @@ class TypeSimplifier(tl: TraceLogger): subst(ty) - def simplifyForall(ty: GeneralType): GeneralType = ty match + def simplifyForall(ty: GeneralType)(using TL): GeneralType = ty match case PolyType(tvs, outer, body) => val newBody = simplifyForall(body) val visited = PolyType.collectTVs(newBody) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeTraverser.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeTraverser.scala index 02f1b14b92..47e4e8735e 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeTraverser.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeTraverser.scala @@ -20,6 +20,7 @@ class TypeTraverser: case ty: Type => apply(pol)(ty) apply(!pol)(ty) + case RcdType(fields) => fields.values.foreach(apply(pol)) case InfVar(vlvl, uid, state, _) => if pol then state.lowerBounds.foreach(apply(true)) else state.upperBounds.foreach(apply(false)) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala index da2877b381..ff4abd93a0 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala @@ -2,7 +2,7 @@ package hkmc2 package bbml -import scala.collection.mutable.{HashSet, HashMap, ListBuffer} +import scala.collection.mutable.{HashSet, HashMap, ListBuffer, LinkedHashSet, LinkedHashMap} import scala.annotation.tailrec import mlscript.utils.*, shorthands.* @@ -73,7 +73,7 @@ object BbCtx: end BbCtx -class BBTyper(using elState: Elaborator.State, tl: TL): +class BBTyper(using elState: Elaborator.State, tl: TL)(using Config): import tl.{trace, log} private val infVarState = new InfVarUid.State() @@ -159,6 +159,13 @@ class BBTyper(using elState: Elaborator.State, tl: TL): 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) => @@ -177,20 +184,42 @@ class BBTyper(using elState: Elaborator.State, tl: TL): tv -> qv bds.foreach: case (tv, QuantVar(_, ub, lb)) => - ub.foreach(ub => tv.state.upperBounds ::= typeMonoType(ub)) - lb.foreach(lb => tv.state.lowerBounds ::= typeMonoType(lb)) + ub.foreach(ub => tv.state.upperBounds ::= monoOrErr(typeType(ub), ub)) + lb.foreach(lb => tv.state.lowerBounds ::= monoOrErr(typeType(lb), lb)) val lbty = tv.state.lowerBounds.foldLeft[Type](Bot)(_ | _) val ubty = tv.state.upperBounds.foldLeft[Type](Top)(_ & _) - constrain(lbty, ubty) + solver.constrain(lbty, ubty) PolyType(bds.map(_._1), S(outer), body) - private def typeMonoType(ty: Term)(using ctx: BbCtx, cctx: CCtx): Type = monoOrErr(typeType(ty), ty) + private def typeMonoType(ty: Term)(using ctx: BbCtx, cctx: CCtx): Type = monoOrErr(typeAndSubstType(ty, true)(using Map.empty), ty) - private def typeType(ty: Term)(using ctx: BbCtx, cctx: CCtx): GeneralType = - typeAndSubstType(ty, pol = true)(using Map.empty) + private def wffuns(fs: Ls[FunType]) = + val wf = fs.forall(f => (f.ret :: f.eff :: f.args).forall(wftype)) + wf && fs.combinations(2).forall: u => + Type.disjoint(Type.discriminant(u.head.args), Type.discriminant(u.tail.head.args)).isEmpty + private def wfrcds(rs: Ls[RcdType]) = + val wf = rs.forall(_.fields.forall(u => wftype(u._2))) + wf && rs.combinations(2).forall: u => + Type.disjoint(u.head, u.tail.head).isEmpty + private def wfcls(cs: Ls[ClassLikeType]) = + cs.forall(_.targs.forall(u => wftype(u.posPart) && wftype(u.negPart))) + private def wftype(ty: GeneralType): Bool = ty match + case t: PolyType => wftype(t.body) + case t: PolyFunType => (t.ret :: t.eff :: t.args).forall(wftype) + case t: Type => + val n = t.!.toDnf.conjs + val nf = n.iterator.map(_.i.v).forall: + case S(f: (Ls[FunType] | RcdType)) => false + case _ => true + nf && wffuns(n.flatMap(_.u.fun)) && n.forall(c => wfrcds(c.u.rcd) && wfcls(c.u.cls)) + + private def typeType(ty: Term, map: Map[Uid[Symbol], TypeArg] = Map.empty)(using ctx: BbCtx, cctx: CCtx): GeneralType = + val t = typeAndSubstType(ty, pol = true)(using map) + if !wftype(t) then error(msg"Ill-formed type" -> ty.toLoc :: Nil) + t private def instantiate(ty: PolyType)(using ctx: BbCtx): GeneralType = - ty.instantiate(infVarState.nextUid, freshEnv(new TempSymbol(N, "env")), ctx.lvl)(tl) + ty.instantiate(infVarState.nextUid, freshEnv(new TempSymbol(N, "env")), ctx.lvl) private def extrude(ty: GeneralType)(using ctx: BbCtx, pol: Bool, cctx: CCtx): GeneralType = ty match case ty: Type => solver.extrude(ty)(using ctx.lvl, pol, HashMap.empty) @@ -198,10 +227,23 @@ class BBTyper(using elState: Elaborator.State, tl: TL): case pf @ PolyFunType(args, ret, eff) => PolyFunType(args.map(extrude(_)(using ctx, !pol)), extrude(ret), solver.extrude(eff)(using ctx.lvl, pol, HashMap.empty)) - private def constrain(lhs: Type, rhs: Type)(using ctx: BbCtx, cctx: CCtx): Unit = - solver.constrain(lhs, rhs) + trait ConstraintHandler: + def constrain(lhs: Type, rhs: Type)(using ctx: BbCtx, cctx: CCtx): Unit + def commit(ds: DisjSub): Unit + + private def constraintCollector = + val cs = ListBuffer.empty[Type -> Type] + val dss = ListBuffer.empty[DisjSub] + val nc = new ConstraintHandler: + def constrain(lhs: Type, rhs: Type)(using ctx: BbCtx, cctx: CCtx) = + cs += lhs -> rhs + def commit(ds: DisjSub) = dss += ds + (nc, dss, cs) + + private def constrain(lhs: Type, rhs: Type)(using ctx: BbCtx, cctx: CCtx, c: ConstraintHandler): Unit = + c.constrain(lhs, rhs) - private def typeCode(code: Term)(using ctx: BbCtx, scope: Scope): (Type, Type, Type) = + private def typeCode(code: Term)(using ctx: BbCtx, scope: Scope, c: ConstraintHandler): (Type, Type, Type) = given CCtx = CCtx.init(code, N) code match case UnitVal() => (Top, Bot, Bot) @@ -267,7 +309,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): case _ => (error(msg"Cannot quote ${code.toString}" -> code.toLoc :: Nil), Bot, Bot) - private def typeFunDef(sym: Symbol, lam: Term, sig: Opt[Term], pctx: BbCtx)(using ctx: BbCtx, cctx: CCtx, scope: Scope) = lam match + private def typeFunDef(sym: Symbol, lam: Term, sig: Opt[Term], pctx: BbCtx)(using ctx: BbCtx, cctx: CCtx, scope: Scope, c: ConstraintHandler) = lam match case Term.Lam(params, body) => sig match case S(sig) => val sigTy = typeType(sig)(using ctx) @@ -286,54 +328,137 @@ class BBTyper(using elState: Elaborator.State, tl: TL): pctx += sym -> PolyType.generalize(funTy, S(outer), 1) case _ => error(msg"Function definition shape not yet supported for ${sym.nme}" -> lam.toLoc :: Nil) - private def typeSplit - (split: Split, sign: Opt[GeneralType])(using ctx: BbCtx)(using CCtx, Scope) - : (GeneralType, Type) = - split match - case Split.Cons(Branch(scrutinee, pattern, cons), alts) => - val (scrutineeTy, scrutineeEff) = typeCheck(scrutinee) - val nestCtx1 = ctx.nest - val nestCtx2 = ctx.nest - val patTy = pattern match - case Pattern.ClassLike(sym, _, _, _) => - val (clsTy, tv, emptyTy) = sym.asCls.flatMap(_.defn) match - case S(cls) => - (ClassLikeType(sym, cls.tparams.map(_ => freshWildcard(sym))), (freshVar(new TempSymbol(S(scrutinee), "scrut"))), ClassLikeType(sym, cls.tparams.map(_ => Wildcard.empty))) - case _ => - error(msg"Cannot match ${scrutinee.toString} as ${sym.toString}" -> split.toLoc :: Nil) - (Bot, Bot, Bot) - scrutinee match // * refine - case Ref(sym: LocalSymbol) => - nestCtx1 += sym -> clsTy - nestCtx2 += sym -> tv - case _ => () // TODO: refine all variables holding this value? - clsTy | (tv & Type.mkNegType(emptyTy)) - case Pattern.Lit(lit) => lit match + private def typeSplitImpl(split: Split, sign: GeneralType, eff: Type, br: Bool, path: Ls[Ls[Ref -> Type]]) + (using ctx: BbCtx, c: ConstraintHandler, sv: LinkedHashMap[Ref, Type])(using CCtx, Scope) + : Ls[Ls[Ref -> Type]] = split match + case Split.Cons(Branch(s: Ref, cp: Pattern.ClassLike, cons), alts) => + val cls = ClassLikeType(cp.sym, cp.sym.asCls.flatMap(_.defn).get.tparams.map(_ => Wildcard.empty)) + val (r, sty) = sv.get(s) match + case N => + val t = tryMkMono(typeCheck(s)._1, s) + sv += s -> t + (path, t) + case S(t) => + (path.filterNot: p => + p.find(_._1 === s).fold(false): u => + Type.disjoint(u._2.!, cls).isEmpty) -> t + if r.isEmpty then typeSplitImpl(alts, sign, eff, br, path) + else + val ctx1 = ctx.nest + ctx1 += s.sym -> (cls & sty) + sv -= s + val (nc, dss, cs) = constraintCollector + val p0 = Ls(s -> cls) :: typeSplitImpl(cons, sign, eff, true, r)(using ctx1, nc) + sv += s -> sty + if p0.contains(Nil) then typeSplitImpl(alts, sign, eff, br, path) + else + Type.disjoint(cls, sty).foreach: k => + if k.isEmpty then + dss.foreach(c.commit) + cs.foreach(u => constrain(u._1, u._2)) + else + val ks = LinkedHashSet.from(k) + dss.foreach(d => c.commit(DisjSub(ks ++ d.disjoint, d.dss, d.cs))) + if cs.nonEmpty then c.commit(DisjSub(ks, Nil, cs.toList)) + val p = path.flatMap(x => p0.map: y => + val m = (x ++ y).groupMapReduce(_._1)(_._2)(_ | _) + (x.keys ++ y.keys).distinct.map(k => k -> m(k)).toList) + val p1 = typeSplitImpl(alts, sign, eff, br, p) + if br then + p1.flatMap(y => p0.map: x => + val m = (x ++ y).groupMapReduce(_._1)(_._2)(_ | _) + (x.keys ++ y.keys).distinct.map(k => k -> m(k)).toList) + else Nil + case Split.Cons(Branch(s: Ref, Pattern.Lit(lit), cons), alts) => + constrain(tryMkMono(typeCheck(s)._1, s), lit match case _: Tree.BoolLit => BbCtx.boolTy case _: Tree.IntLit => BbCtx.intTy case _: Tree.DecLit => BbCtx.numTy case _: Tree.StrLit => BbCtx.strTy - case _: Tree.UnitLit => Top - constrain(tryMkMono(scrutineeTy, scrutinee), patTy) - val (consTy, consEff) = typeSplit(cons, sign)(using nestCtx1) - val (altsTy, altsEff) = typeSplit(alts, sign)(using nestCtx2) - val allEff = scrutineeEff | (consEff | altsEff) - (sign.getOrElse(tryMkMono(consTy, cons) | tryMkMono(altsTy, alts)), allEff) + case _: Tree.UnitLit => Top) + val p0 = typeSplitImpl(cons, sign, eff, true, path) + val p = path.flatMap(x => p0.map: y => + val m = (x ++ y).groupMapReduce(_._1)(_._2)(_ | _) + (x.keys ++ y.keys).distinct.map(k => k -> m(k)).toList) + val p1 = typeSplitImpl(alts, sign, eff, br, p) + if br then + p1.flatMap(y => p0.map: x => + val m = (x ++ y).groupMapReduce(_._1)(_._2)(_ | _) + (x.keys ++ y.keys).distinct.map(k => k -> m(k)).toList) + else Nil case Split.Let(name, term, tail) => val nestCtx = ctx.nest given BbCtx = nestCtx - val (termTy, termEff) = typeCheck(term) + val (nc, dss, cs) = constraintCollector + sv.keys.foreach: s => + val v = freshVar(new TempSymbol(S(s), s.sym.nme)) + nestCtx += s.sym -> v + val (termTy, termEff) = typeCheck(term)(using c = nc) val sk = freshSkolem(name) nestCtx += name -> termTy - val (tailTy, tailEff) = typeSplit(tail, sign)(using nestCtx) - (tailTy, termEff | tailEff) - case Split.Else(alts) => sign match - case S(sign) => ascribe(alts, sign) - case _ => typeCheck(alts) - case Split.End => (Bot, Bot) + nc.constrain(termEff, eff) + path.foreach: p => + val m = p.toMap + val d = p.flatMap { case (s, t) => sv.get(s).map(st => Type.disjoint(t.!, st)) } + val sc = sv.toList.map: + case (s, t) => + val v = nestCtx.get(s.sym).get + (m.getOrElse(s, Bot).! & t, monoOrErr(v, s)) + val ds = d.foldLeft(Set(Set.empty[InfVar -> BasicType]))((x, y) => y.flatMap(y => x.map(_ ++ y))) + if ds.exists(_.isEmpty) then + dss.foreach(c.commit(_)) + (sc ++ cs).distinct.foreach(u => constrain(u._1, u._2)) + else ds.foreach: k => + val ks = LinkedHashSet.from(k) + dss.foreach(d => c.commit(DisjSub(ks ++ d.disjoint, d.dss, d.cs))) + c.commit(DisjSub(ks, Nil, (sc ++ cs).distinct)) + typeSplitImpl(tail, sign, eff, br, path) + case Split.Else(e) => + val (nc, dss, cs) = constraintCollector + val ctx1 = ctx.nest + sv.keys.foreach: s => + val v = freshVar(new TempSymbol(S(s), s.sym.nme)) + ctx1 += s.sym -> v + nc.constrain(ascribe(e, sign)(using ctx1, c = nc)._2, eff) + path.foreach: p => + val m = p.toMap + val d = p.flatMap { case (s, t) => sv.get(s).map(st => Type.disjoint(t.!, st)) } + val sc = sv.toList.map: + case (s, t) => + val v = ctx1.get(s.sym).get + (m.getOrElse(s, Bot).! & t, monoOrErr(v, s)) + val ds = d.foldLeft(Set(Set.empty[InfVar -> BasicType]))((x, y) => y.flatMap(y => x.map(_ ++ y))) + if ds.exists(_.isEmpty) then + dss.foreach(c.commit(_)) + (sc ++ cs).distinct.foreach(u => constrain(u._1, u._2)) + else ds.foreach: k => + val ks = LinkedHashSet.from(k) + dss.foreach(d => c.commit(DisjSub(ks ++ d.disjoint, d.dss, d.cs))) + c.commit(DisjSub(ks, Nil, (sc ++ cs).distinct)) + Nil + case Split.End => + if !br then + path.foreach: p => + val m = p.toMap + val d = p.map { case (s, t) => Type.disjoint(t.!, sv(s)) } + val ds = d.foldLeft(Set(Set.empty[InfVar -> BasicType]))((x, y) => y.flatMap(y => x.map(_ ++ y))) + if ds.exists(_.isEmpty) then constrain(Top, Bot) + else ds.foreach: k => + val c0 = Ls(Top -> Bot) + val ks = LinkedHashSet.from(k) + c.commit(DisjSub(ks, Nil, c0)) + Ls(Nil) + + private def typeSplit + (split: Split, sign: Opt[GeneralType], path: Ls[Ls[Type -> ClassLikeType]] = Ls(Nil))(using ctx: BbCtx, c: ConstraintHandler)(using CCtx, Scope) + : (GeneralType, Type) = + val res = sign.orElse(S(freshVar(new TempSymbol(N, "res")))).get + val eff = freshVar(new TempSymbol(N, "eff")) + typeSplitImpl(split, res, eff, false, Ls(Nil))(using sv = LinkedHashMap.empty) + (res, eff) // * Note: currently, the returned type is not used or useful, but it could be in the future - private def ascribe(lhs: Term, rhs: GeneralType)(using ctx: BbCtx, scope: Scope): (GeneralType, Type) = + private def ascribe(lhs: Term, rhs: GeneralType)(using ctx: BbCtx, scope: Scope, c: ConstraintHandler): (GeneralType, Type) = trace[(GeneralType, Type)](s"${ctx.lvl}. Ascribing ${lhs.showDbg} : ${rhs.showDbg}", res => s"! ${res._2.showDbg}"): given CCtx = CCtx.init(lhs, S(rhs)) (lhs, rhs) match @@ -364,17 +489,33 @@ class BBTyper(using elState: Elaborator.State, tl: TL): ascribe(term, typeType(ty)) ascribe(term, rhs) case _ => - val (lhsTy, eff) = typeCheck(lhs) rhs match case pf: PolyFunType if pf.isPoly => (error(msg"Cannot type non-function term ${lhs.toString} as ${rhs.show}" -> lhs.toLoc :: Nil), Bot) case _ => - constrain(tryMkMono(lhsTy, lhs), monoOrErr(rhs, lhs)) - (rhs, eff) + val r = monoOrErr(rhs, lhs) + val n = r.!.toDnf.conjs + if n.flatMap(_.u.fun).length > 1 then + val eff = n.foldLeft(Bot: Type): (e, c) => + (c.i.v, c.u, c.vars) match + case (i, u, v) => + val n = i.fold(Bot: Type): + case x: (ClassLikeType | RcdType) => x.! + case x: Ls[FunType] => x.reduce[Type](_ & _).! + val k = Ls(u.fun, u.cls, u.cls).flatten.foldLeft(Bot: Type)(_ | _) + val vs = v.foldLeft(Bot: Type): (x, y) => + x | (if y._2 then y._1.! else y._1) + val (_, eff) = ascribe(lhs, n | k | vs) + e | eff + (rhs, eff) + else + val (lhsTy, eff) = typeCheck(lhs) + constrain(tryMkMono(lhsTy, lhs), r) + (rhs, eff) // TODO: t -> loc when toLoc is implemented private def app(lhs: (GeneralType, Type), rhs: Ls[Elem], t: Term) - (using ctx: BbCtx)(using CCtx, Scope) + (using ctx: BbCtx, c: ConstraintHandler)(using CCtx, Scope) : (GeneralType, Type) = lhs match case (PolyFunType(params, ret, eff), lhsEff) => @@ -401,7 +542,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): constrain(tryMkMono(funTy, t), FunType(argTy.map((tryMkMono(_, t))), retVar, effVar)) (retVar, argEff.foldLeft[Type](effVar | lhsEff)((res, e) => res | e)) - private def skolemize(ty: PolyType)(using ctx: BbCtx) = ty.skolemize(infVarState.nextUid, ctx.lvl)(tl) + private def skolemize(ty: PolyType)(using ctx: BbCtx) = ty.skolemize(infVarState.nextUid, ctx.lvl) // TODO: implement toLoc private def monoOrErr(ty: GeneralType, sc: Located)(using BbCtx) = @@ -413,10 +554,40 @@ class BBTyper(using elState: Elaborator.State, tl: TL): 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 - - private def typeCheck(t: Term)(using ctx: BbCtx, scope: Scope): (GeneralType, Type) = + + private def typeCheck(t: Term)(using ctx: BbCtx, scope: Scope, c: ConstraintHandler): (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) + def goStats(stats: Ls[Statement])(using 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 (td @ TermDefinition(k = Fun, params = ps :: Nil, sign = sig, body = S(body))) :: stats => + typeFunDef(td.sym, Term.Lam(ps, body), sig, ctx) + goStats(stats) + case (td @ TermDefinition(k = Fun, params = Nil, sign = sig, body = S(body))) :: stats => + typeFunDef(td.sym, body, sig, ctx) // * may be a case expressions + goStats(stats) + case (td1 @ TermDefinition(k = Fun, sign = S(sig), body = None)) :: (td2 @ TermDefinition(k = Fun, body = S(body))) :: stats + if td1.sym === td2.sym => goStats(td2 :: stats) // * avoid type check signatures twice + case (td @ TermDefinition(k = Fun, sign = S(sig), body = None)) :: stats => + ctx += td.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) t match case Term.Annotated(Annot.Untyped, _) => (Bot, Bot) case sel @ Term.SynthSel(Ref(_: TopLevelSymbol), nme) @@ -431,37 +602,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): -> 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 (td @ TermDefinition(k = Fun, params = ps :: Nil, sign = sig, body = S(body))) :: stats => - typeFunDef(td.sym, Term.Lam(ps, body), sig, ctx) - goStats(stats) - case (td @ TermDefinition(k = Fun, params = Nil, sign = sig, body = S(body))) :: stats => - typeFunDef(td.sym, body, sig, ctx) // * may be a case expressions - goStats(stats) - case (td1 @ TermDefinition(k = Fun, sign = S(sig), body = None)) :: (td2 @ TermDefinition(k = Fun, body = S(body))) :: stats - if td1.sym === td2.sym => goStats(td2 :: stats) // * avoid type check signatures twice - case (td @ TermDefinition(k = Fun, sign = S(sig), body = None)) :: stats => - ctx += td.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) + goStats(stats)(using effBuff = effBuff) val (ty, eff) = typeCheck(res) (ty, effBuff.foldLeft(eff)((res, e) => res | e)) case UnitVal() => (Top, Bot) @@ -498,7 +639,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): case Param(_, sym, sign, _) => if sym.nme === field.name then sign else N }.filter(_.isDefined)) match - case S(res) :: Nil => (typeAndSubstType(res, pol = true)(using map.toMap), eff) + case S(res) :: Nil => (typeType(res, map.toMap), eff) case _ => (error(msg"${field.name} is not a valid member in class ${clsSym.nme}" -> t.toLoc :: Nil), Bot) case N => (error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil), Bot) @@ -528,7 +669,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): require(clsDfn.paramsOpt.forall(_.restParam.isEmpty)) args.iterator.zip(clsDfn.params.params).foreach { case (arg, Param(sign = S(sign))) => - val (ty, eff) = ascribe(arg, typeAndSubstType(sign, pol = true)(using map.toMap)) + val (ty, eff) = ascribe(arg, typeType(sign, map.toMap)) effBuff += eff case _ => ??? } @@ -580,10 +721,32 @@ class BBTyper(using elState: Elaborator.State, tl: TL): (Bot, eff) case Term.Error => (Bot, Bot) // TODO: error type? + case Rcd(stats) => + // TODO RcdSpread + val (s, r) = stats.partitionMap: k => + k match + case RcdField(Lit(_: StrLit), _) => R(k) + case _ => L(k) + val effBuff = ListBuffer.empty[Type] + 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")) + constrain(tryMkMono(ty, u), RcdType(Ls(a -> v))) + (v, e) case _ => (error(msg"Term shape not yet supported by BbML: ${t.toString}" -> t.toLoc :: Nil), Bot) def typePurely(t: Term)(using BbCtx, Scope): GeneralType = + given ConstraintHandler = new ConstraintHandler: + def constrain(lhs: Type, rhs: Type)(using ctx: BbCtx, cctx: CCtx) = + solver.constrain(lhs, rhs) + def commit(ds: DisjSub) = ds.commit() val (ty, eff) = typeCheck(t) given CCtx = CCtx.init(t, N) constrain(eff, Bot) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala index fc90a0749e..c4e61bbb96 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala @@ -5,7 +5,7 @@ import mlscript.utils.*, shorthands.* import syntax.* import semantics.*, semantics.Term.* import utils.* -import scala.collection.mutable.{Set => MutSet} +import scala.collection.mutable.{Set => MutSet, Map => MutMap, LinkedHashSet} import utils.Scope import Elaborator.State @@ -133,11 +133,11 @@ sealed abstract class Type extends GeneralType with TypeArg: case _ => NegType(this) protected[bbml] def paren(using Scope): Str = toBasic match - case _: InfVar | _: ClassLikeType | _: NegType | Top | Bot => show + case _: InfVar | _: ClassLikeType | _: RcdType | _: NegType | Top | Bot => show case _: ComposedType | _: FunType => s"($show)" protected[bbml] def parenDbg: Str = toBasic match - case _: InfVar | _: ClassLikeType | _: NegType | Top | Bot => showDbg + case _: InfVar | _: ClassLikeType | _: RcdType | _: NegType | Top | Bot => showDbg case _: ComposedType | _: FunType => s"($showDbg)" sealed abstract class BasicType extends Type: @@ -148,6 +148,7 @@ sealed abstract class BasicType extends Type: case InfVar(lvl, _, _, _) => lvl case FunType(args, ret, eff) => (ret :: eff :: args).map(_.lvl).max + case RcdType(fields) => fields.values.map(_.lvl).maxOption.getOrElse(0) case ComposedType(lhs, rhs, _) => lhs.lvl.max(rhs.lvl) case NegType(ty) => ty.lvl @@ -156,6 +157,7 @@ sealed abstract class BasicType extends Type: def mapBasic(f: Type => Type): Type = this match case ClassLikeType(name, targs) => ClassLikeType(name, targs.map(_.mapArg(f))) case FunType(args, ret, eff) => FunType(args.map(f), f(ret), f(eff)) + case RcdType(fields) => RcdType(fields.mapValues(f)) case ComposedType(lhs, rhs, pol) => Type.mkComposedType(f(lhs), f(rhs), pol) case NegType(ty) => Type.mkNegType(f(ty)) case Top | Bot | _: InfVar => this @@ -173,11 +175,12 @@ sealed abstract class BasicType extends Type: 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}" + case RcdType(fields) => s"{${fields.map { case (l, t) => s"$l: ${t.show}" }.mkString(", ")}}" + case ComposedType(lhs, rhs, pol) => s"${lhs.paren} ${if pol then "|" else "&"} ${rhs.paren}" case NegType(ty) => s"¬${ty.paren}" case Top => "⊤" case Bot => "⊥" - + override def showDbg: Str = this match case ClassLikeType(name, targs) => if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]" @@ -186,7 +189,8 @@ sealed abstract class BasicType extends Type: 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}" + case RcdType(fields) => s"{${fields.map { case (l, t) => s"$l: ${t.showDbg}" }.mkString(", ")}}" + case ComposedType(lhs, rhs, pol) => s"${lhs.parenDbg} ${if pol then "|" else "&"} ${rhs.parenDbg}" case NegType(ty) => s"¬${ty.parenDbg}" case Top => "⊤" case Bot => "⊥" @@ -223,7 +227,7 @@ trait CachedNorm[A <: AnyRef]: _norm = d d else _norm - + object BasicType: // TOOD dedup @@ -251,6 +255,8 @@ case class ClassLikeType(name: TypeSymbol | ModuleSymbol, targs: Ls[TypeArg]) ex final case class InfVar(vlvl: Int, uid: Uid[InfVar], state: VarState, isSkolem: Bool)(val sym: Symbol, val hint: Str) extends BasicType: override def subst(using map: Map[Uid[InfVar], InfVar]): ThisType = map.get(uid).getOrElse(this) + def showBounds: Str = + s"lower: ${state.lowerBounds.map(_.showDbg).mkString(", ")} upper: ${state.upperBounds.map(_.showDbg).mkString(", ")} disjsub: ${state.disjsub}" given Ordering[InfVar] = Ordering.by(_.uid) @@ -260,6 +266,14 @@ case class FunType(args: Ls[Type], ret: Type, eff: Type) extends BasicType with override def subst(using map: Map[Uid[InfVar], InfVar]): ThisType = FunType(args.map(_.subst), ret.subst, eff.subst) +case class RcdType(fields: Ls[Str -> Type]) extends BasicType with CachedNorm[RcdType]: + def mkNorm(using TL): RcdType = + RcdType(fields.mapValues(_.toDnf)) + override def subst(using map: Map[Uid[InfVar], InfVar]): ThisType = + RcdType(fields.mapValues(_.subst)) + def & (that: RcdType): RcdType = + RcdType((fields ++ that.fields).groupMapReduce(_._1)(_._2)(_ & _).toList) + case class ComposedType(lhs: Type, rhs: Type, pol: Bool) extends BasicType: // * Positive -> union override def subst(using map: Map[Uid[InfVar], InfVar]): ThisType = Type.mkComposedType(lhs.subst, rhs.subst, pol) @@ -281,6 +295,60 @@ object Type: then lhs | rhs else lhs & rhs def mkNegType(ty: Type): Type = ty.! + def discriminant(a: Ls[Type])(using TL): RcdType = + discriminantRcd(RcdType(a.zipWithIndex.map(u => (s"${u._2}", u._1.toBasic)))) + def discriminantRcd(a: RcdType)(using TL): RcdType = + RcdType(a.fields.flatMap: + case (a, t) => discriminant(t) match + case Top => N + case t => S(a -> t)) + def discriminantIU(i: Inter, u: Union)(using TL): BasicType = (i.v, u.cls) match + case (N, cs) => cs.reduceOption[Type](_ | _).fold(Top)(NegType(_)) + case (S(ClassLikeType(c, t)), cs) => if cs.exists(_.name.uid === c.uid) then Bot else ClassLikeType(c, t.map(_ => Wildcard.empty)) + case (S(u: RcdType), _) => discriminantRcd(u) + case _ => Top + def discriminant(t: Type)(using TL): BasicType = + t.toDnf.conjs.foldLeft(Bot: Type)((x, y) => x | discriminantIU(y.i, y.u)).simp.toBasic + def disjointIU(i: Inter, u: Union)(using TL): Set[Set[InfVar -> BasicType]] = (i.v, u.cls, u.rcd) match + case (S(c: ClassLikeType), cs, _) if cs.exists(_.name.uid === c.name.uid) => Set.empty + case (S(RcdType(u)), _, rs) => + val k = u.iterator.map(u => u._1 -> disjointDisj(u._2.toDnf)).toMap + val p = rs.foldLeft[Ls[Ls[Str -> Type]]](Ls(Nil)): (p, w) => + if w.fields.keys.forall(k.contains) then p.flatMap(x => w.fields.map(_ :: x)) else p + val rd = p.flatMap: p => + val m = p.groupMapReduce(_._1)(_._2)(_ | _) + val d = u.map: + case (a, t) => m.get(a).fold(k(a))(q => Type.disjoint(q.!, t)) + d.foldLeft(Set(Set.empty[InfVar -> BasicType]))((x, y) => y.flatMap(y => x.map(_ ++ y))) + if rd.exists(_.isEmpty) then Set(Set.empty) else rd.toSet + case _ => Set(Set.empty) + def disjointConj(ty: Conj)(using TL): Set[Set[InfVar -> BasicType]] = + val d = disjointIU(ty.i, ty.u) + if d.isEmpty then Set.empty + else (ty.i.v, ty.u.cls, ty.u.rcd, ty.vars.iterator.filter(_._2).keys.toList) match + case (_, _, _, Nil) => d + case (N, Nil, Nil, v :: Nil) => + val lb = v.state.lowerBounds.foldLeft(Bot: Type)(_ | _) + disjointDisj(lb.toDnf) + Set(v -> v) + case (i, c, r, vs) => + val j = i match + case S(ClassLikeType(c, _)) => S(ClassLikeType(c, Nil)) + case S(u: RcdType) => S(u) + case _ => N + val vd = vs.combinations(2).collect { case x :: y :: _ => Ls(x -> y) }.flatten.toList + val ds = vs.flatMap(v => (j ++ (c ++ r).reduceOption[Type](_ | _).map(_.!)).map(x => v -> x.toBasic)).toSet ++ vd + val lb = vs.flatMap(_.state.lowerBounds.reduceOption[Type](_ | _)).reduceOption(_ & _).orElse(S(Bot)).get + val t = lb & Conj(Inter(j), Union(N, c, Nil), Nil) + disjointDisj(t.toDnf) + ds + def disjointDisj(t: Disj)(using TL): Set[Set[InfVar -> BasicType]] = + if t.conjs.isEmpty then Set.empty + else + val ds = t.conjs.flatMap(disjointConj) + if ds.exists(_.isEmpty) then Set(Set.empty) + else ds.toSet + def disjoint(a: Type, b: Type)(using TL): Set[Set[InfVar -> BasicType]] = + disjointDisj((a & b).toDnf) + // * Poly types can not be used as type arguments case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], body: GeneralType) extends GeneralType: @@ -307,21 +375,25 @@ case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], body: GeneralType) exte val newSt = new VarState() newSt.lowerBounds = state.lowerBounds.map(_.subst) newSt.upperBounds = state.upperBounds.map(_.subst) + newSt.disjsub ++= state.disjsub.map(_.subst) InfVar(lvl, uid, newSt, skolem)(v.sym, v.hint) }, outer, body.subst) // * outer should have no bound! - + // * This function will only return the body after substitution // * and \dom(map) should cover all tvs. // * This function is dedicated to `skolemize` and `instantiate`. - private def substAndGetBody(using map: Map[Uid[InfVar], InfVar]): GeneralType = + private def substAndGetBody(using map: Map[Uid[InfVar], InfVar])(using TL): GeneralType = tvs.foreach: case InfVar(lvl, uid, state, skolem) => val v = map(uid) v.state.lowerBounds = state.lowerBounds.map(_.subst) v.state.upperBounds = state.upperBounds.map(_.subst) + v.state.disjsub ++= state.disjsub.map(_.subst) + v.state.disjsub.foreach(_.commit()) + tl.log(s"adding bounds to $v: ${v.showBounds}") body.subst - - def skolemize(nextUid: => Uid[InfVar], lvl: Int)(tl: TL) = + + def skolemize(nextUid: => Uid[InfVar], lvl: Int)(using TL) = // * Note that by this point, the state is supposed to be frozen/treated as immutable // * `outer` is already skolemized when it is declared val map = tvs.map(v => @@ -331,31 +403,36 @@ case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], body: GeneralType) exte ).toMap substAndGetBody(using map) - def instantiate(nextUid: => Uid[InfVar], env: InfVar, lvl: Int)(tl: TL)(using State): GeneralType = + def instantiate(nextUid: => Uid[InfVar], env: InfVar, lvl: Int)(using State, TL): GeneralType = val map = (outer.map(_.uid -> env).toList ++ tvs.map(v => val nv = InfVar(lvl, nextUid, new VarState(), false)(new InstSymbol(v.sym), v.hint) tl.log(s"instantiate ${v.showDbg} ~> ${nv.showDbg}") + // tl.log(s"where ${nv.showBounds}") v.uid -> nv )).toMap substAndGetBody(using map) object PolyType: - def collectTVs(ty: GeneralType): Set[InfVar] = + def collectTVs(ty: GeneralType)(using TL): Set[InfVar] = val visited = MutSet.empty[InfVar] object CollectTVs extends TypeTraverser: override def apply(pol: Boolean)(ty: GeneralType): Unit = ty match case v @ InfVar(_, _, state, _) => + tl.log(s"collect ${v.showDbg} ${state.upperBounds}") if visited.add(v) then state.lowerBounds.foreach: bd => apply(true)(bd) state.upperBounds.foreach: bd => apply(false)(bd) + val (p, n) = state.disjsub.map(_.children()).unzip + p.flatten.foreach(apply(true)) + n.flatten.foreach(apply(false)) super.apply(pol)(ty) case _ => super.apply(pol)(ty) CollectTVs(true)(ty) visited.toSet - def generalize(ty: GeneralType, outer: Opt[InfVar], lvl: Int): PolyType = + def generalize(ty: GeneralType, outer: Opt[InfVar], lvl: Int)(using TL): PolyType = PolyType(collectTVs(ty).filter(v => outer.map(_.uid != v.uid).getOrElse(true)).toList.sorted, outer, ty) // * Functions that accept/return a polymorphic type. @@ -388,3 +465,32 @@ case class PolyFunType(args: Ls[GeneralType], ret: GeneralType, eff: Type) exten class VarState: var lowerBounds: Ls[Type] = Nil var upperBounds: Ls[Type] = Nil + val disjsub: LinkedHashSet[DisjSub] = LinkedHashSet.empty + override def toString = "<>" + +case class DisjSub(disjoint: LinkedHashSet[InfVar -> BasicType], dss: Ls[DisjSub], cs: Ls[Type -> Type]): + def commit() = disjoint.keys.foreach(_.state.disjsub += this) + def check(m: Map[InfVar, Type])(using TL): (Ls[DisjSub], Ls[Type -> Type]) = + if disjoint.isEmpty then (Nil, Nil) + else + disjoint.keys.foreach(_.state.disjsub -= this) + val d = disjoint.toList.map: u => + m.get(u._1).fold(Set(Set(u._1 -> u._2))): t => + val k = Type.disjoint(u._2, t | u._1) + k.foreach(x => if x.isEmpty then disjoint -= u) + k + if disjoint.isEmpty then + val (dss0, cs0) = dss.map(_.check(m)).unzip + (dss0.flatten, cs0.flatten ++ cs) + else + val dss1 = d.reduce((x, y) => y.flatMap(y => x.map(_ ++ y))).map: k => + DisjSub(LinkedHashSet.from(k), dss, cs) + (dss1.toList, Nil) + def children(): (Ls[Type], Ls[Type]) = + val (p, n) = dss.map(_.children()).unzip + (p.flatten ++ disjoint.keys ++ cs.keys, n.flatten ++ cs.values) + def subDisjSub: Ls[DisjSub] = this :: dss.flatMap(_.subDisjSub) + def subst(using map: Map[Uid[InfVar], InfVar]): DisjSub = + val d = disjoint.map: + case (v, t) => (map.get(v.uid).getOrElse(v), t.subst.toBasic) + DisjSub(d, dss.map(_.subst), cs.map(u => (u._1.subst, u._2.subst))) diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala index 378c4bed7c..276b717546 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala @@ -168,6 +168,7 @@ enum Term extends Statement: case Forall(tvs, outer, body) => "universal quantification" case WildcardTy(in, out) => "wildcard type" case Blk(stats, res) => "block" + case Rcd(stats) => "record" case Quoted(term) => "quoted term" case Unquoted(term) => "unquoted term" case New(cls, args, rft) => "object creation" diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls index 72ee59b5aa..775a4a74a1 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls @@ -145,14 +145,52 @@ let t = new Some(true) in t.Some#value data class Printer[T](f: T -> Str) //│ Type: ⊤ +fun foofoo(x) = + if x is Int then + let t = x + 1 in "foo" +foofoo +//│ Type: ['x, 'res, 'eff] -> 'x ->{'eff} 'res +//│ Where: +//│ 'x#Int ∨ Int & 'x <: Int ∧ Int <: Int ∧ Str <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Int ∨ ⊤ <: ⊥ + fun foofoo(x) = let t = x + 1 in "foo" //│ Type: ⊤ -new Printer(foofoo) -//│ Type: Printer['T] +:ns +foofoo +//│ Type: [outer, 'x] -> 'x -> Str //│ Where: -//│ 'T <: Int +//│ 'x <: ¬(¬{Int}) + +// TODO +fun f() = new Printer(foofoo) +f +//│ Type: ['T, 'x] -> () -> Printer['T] +//│ Where: +//│ 'T#'T ∨ ( 'T#'T ∨ Str <: Str ∧ ⊥ <: ⊥){0: 'T} <: {0: 'x} +//│ 'x <: Int + +f().Printer#f(42) +//│ Type: Str + +:e +f().Printer#f("oops") +//│ ╔══[ERROR] Type error in string literal with expected type 'T +//│ ║ l.179: f().Printer#f("oops") +//│ ║ ^^^^^^ +//│ ╟── because: cannot constrain Str <: 'T +//│ ╟── because: cannot constrain Str <: 'T +//│ ╟── because: cannot constrain Str <: ¬(¬'T1) +//│ ╟── because: cannot constrain Str <: 'T1 +//│ ╟── because: cannot constrain {0: 'T1} <: {0: ¬⊥ & 'x} +//│ ╟── because: cannot constrain 'T1 <: ¬⊥ & 'x +//│ ╟── because: cannot constrain 'T1 <: 'x +//│ ╟── because: cannot constrain 'T1 <: Int +//│ ╟── because: cannot constrain 'T1 <: ¬(¬{Int}) +//│ ╙── because: cannot constrain Str <: ¬(¬{Int}) +//│ Type: Str let ip = new Printer(foofoo) in ip.Printer#f(42) //│ Type: Str @@ -160,12 +198,17 @@ let ip = new Printer(foofoo) in ip.Printer#f(42) :e let ip = new Printer(foofoo) in ip.Printer#f("42") //│ ╔══[ERROR] Type error in string literal with expected type 'T -//│ ║ l.161: let ip = new Printer(foofoo) in ip.Printer#f("42") +//│ ║ l.199: 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 {0: 'T} <: {0: 'x} +//│ ╟── because: cannot constrain 'T <: 'x +//│ ╟── because: cannot constrain 'T <: 'x +//│ ╟── because: cannot constrain 'T <: ¬¬Int +//│ ╟── because: cannot constrain 'T <: ¬(¬{Int}) //│ ╙── because: cannot constrain Str <: ¬(¬{Int}) //│ Type: Str @@ -178,8 +221,8 @@ fun inc(x) = x + 1 new TFun(inc) //│ Type: TFun['T] //│ Where: -//│ Int <: 'T -//│ 'T <: Int +//│ 'T#'T ∨ ( 'T#'T ∨ Int <: 'T ∧ ⊥ <: ⊥){0: 'T} <: {0: 'x} +//│ 'x <: ¬¬Int let tf = new TFun(inc) in tf.TFun#f(1) //│ Type: Int @@ -187,14 +230,19 @@ let tf = new TFun(inc) in tf.TFun#f(1) :e let tf = new TFun(inc) in tf.TFun#f("1") //│ ╔══[ERROR] Type error in string literal with expected type 'T -//│ ║ l.188: let tf = new TFun(inc) in tf.TFun#f("1") +//│ ║ l.231: 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 {0: 'T} <: {0: 'x} +//│ ╟── because: cannot constrain 'T <: 'x +//│ ╟── because: cannot constrain 'T <: 'x +//│ ╟── because: cannot constrain 'T <: ¬¬Int +//│ ╟── because: cannot constrain 'T <: ¬(¬{Int}) //│ ╙── because: cannot constrain Str <: ¬(¬{Int}) -//│ Type: Str ∨ Int +//│ Type: Int | Str data class Pair[A, B](fst: A, snd: B) //│ Type: ⊤ @@ -225,7 +273,7 @@ if 1 < 2 then 1 else 0 if false then 1 else "1" -//│ Type: Int ∨ Str +//│ Type: Int if 1 is Int then 1 else 0 @@ -239,7 +287,10 @@ if 1 is Foo then 0 else 1 fun test(x) = if x is Int then x + 1 else 0 test -//│ Type: (¬Int ∨ Int) -> Int +//│ Type: ['x, 'res, 'eff, 'x1] -> 'x ->{'eff} 'res +//│ Where: +//│ 'x#Int ∨ Int & 'x <: Int ∧ Int <: Int ∧ Int <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Int ∨ ¬Int & 'x <: 'x1 ∧ Int <: 'res ∧ ⊥ <: 'eff test(1) //│ Type: Int @@ -296,6 +347,8 @@ f f(x => x).Foo#x //│ Type: ('A) ->{⊥} 'A +//│ Where: +//│ 'A#'A ∨ ( 'A#'A ∨ 'x <: 'A ∧ ⊥ <: ⊥){0: 'A} <: {0: 'x} g => (new Foo(g)).Foo#x //│ Type: ('A -> 'A) ->{⊥} ('A) ->{⊥} 'A @@ -308,7 +361,7 @@ throw new Error("oops") :e throw 42 //│ ╔══[ERROR] Type error in throw -//│ ║ l.309: throw 42 +//│ ║ l.362: throw 42 //│ ║ ^^ //│ ╙── because: cannot constrain Int <: Error //│ Type: ⊥ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls index ba89c19e39..fd43e6fb09 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls @@ -92,7 +92,7 @@ letreg of r => //│ ║ ^^^^^ //│ ╟── because: cannot constrain 'E <: ⊥ //│ ╟── because: cannot constrain 'E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ ¬'Rg <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & ¬'Rg <: ¬() //│ ╟── because: cannot constrain <: 'Rg //│ ╙── because: cannot constrain <: ¬() //│ Type: ⊥ @@ -128,7 +128,7 @@ letreg of r => //│ ║ ^^^ //│ ╟── because: cannot constrain 'E <: ⊥ //│ ╟── because: cannot constrain 'E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & 'Rg <: ¬() //│ ╟── because: cannot constrain 'Rg <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Reg[?, 'E] @@ -172,7 +172,7 @@ letreg of r => //│ ║ ^^^ //│ ╟── because: cannot constrain 'E <: ⊥ //│ ╟── because: cannot constrain 'E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & 'Rg <: ¬() //│ ╟── because: cannot constrain 'Rg <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Reg[?, 'E] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls index 260bc778f5..4661590c23 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls @@ -49,7 +49,7 @@ letreg of r => //│ ║ ^^^^^^^^^^ //│ ╟── because: cannot constrain 'E <: ⊥ //│ ╟── because: cannot constrain 'E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & 'Rg <: ¬() //│ ╟── because: cannot constrain 'Rg <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -88,7 +88,7 @@ letreg of r => //│ ║ ^^^^^^^^^^ //│ ╟── because: cannot constrain 'E <: ⊥ //│ ╟── because: cannot constrain 'E <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬() +//│ ╟── 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 4d47f09c44..97ef234dcb 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls @@ -56,7 +56,7 @@ fun bar: Foo[in Num out Int] //│ Type: ⊤ foo(bar) -//│ Type: Foo[in Num out Int] ∨ Foo[in Num] +//│ Type: Foo[in Num out Int] | Foo[in Num] :e fun badfoo: [A extends Str restricts Int] -> A -> A @@ -87,6 +87,7 @@ bazbaz //│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A //│ Where: //│ 'A <: Int +//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥){0: 'A} <: {0: 'A} bazbaz(42)(x => x + 1) //│ Type: Int @@ -97,6 +98,7 @@ cc //│ Where: //│ 'A -> 'A <: 'B //│ 'B <: 'A -> 'A +//│ 'B#'B ∨ ( 'B#'B ∨ 'B <: 'B ∧ ⊥ <: ⊥){0: 'B} <: {0: 'B} //│ 'B -> 'B <: 'A //│ 'A <: 'B -> 'B @@ -112,17 +114,19 @@ fun h: [C] -> ([A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B :e bazbaz as [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A //│ ╔══[ERROR] Cannot type non-function term Ref(member:bazbaz) as (A) ->{⊥} ([outer, 'B] -> 'B) ->{⊥} A -//│ ║ l.113: bazbaz as [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A +//│ ║ l.115: bazbaz as [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A //│ ╙── ^^^^^^ //│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A //│ Where: //│ 'A <: Int +//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥){0: 'A} <: {0: 'A} (x => f => bazbaz(x)(f)) as [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A //│ Type: ['A] -> ('A) ->{⊥} ('A -> 'A) ->{⊥} 'A //│ Where: //│ 'A <: Int +//│ 'A#'A ∨ ( 'A#'A ∨ 'A <: 'A ∧ ⊥ <: ⊥){0: 'A} <: {0: 'A} 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 c2be44ba59..48d8e46554 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls @@ -151,14 +151,14 @@ id as [A] -> A -> A //│ Type: ['A] -> ('A) ->{⊥} 'A 42 as Int | Num -//│ Type: Int ∨ Num +//│ Type: Int | Num 42 as [A] -> Int //│ Type: Int 42 as [A] -> Int | Num -//│ Type: Int ∨ Num +//│ Type: Int | Num fun foo: Int -> Int foo @@ -215,14 +215,14 @@ f fun f: ([A] -> ([B] -> A | B -> B | A) -> A) -> ([A] -> ([B] -> A | B -> B | A) -> A) f -//│ Type: (['A] -> (['B] -> ('A ∨ 'B) ->{⊥} 'B ∨ 'A) ->{⊥} 'A) ->{⊥} ['A] -> (['B] -> ('A ∨ 'B) ->{⊥} 'B ∨ 'A) ->{⊥} 'A +//│ Type: (['A] -> (['B] -> ('A | 'B) ->{⊥} 'B | 'A) ->{⊥} 'A) ->{⊥} ['A] -> (['B] -> ('A | 'B) ->{⊥} 'B | 'A) ->{⊥} 'A fun f: [A] -> [B] -> ([C] -> A | B -> B | C -> A | C) -> B f -//│ Type: ['A] -> (['C] -> ('A) ->{⊥} ('C) ->{⊥} 'A ∨ 'C) ->{⊥} ⊥ +//│ Type: ['A] -> (['C] -> ('A) ->{⊥} ('C) ->{⊥} 'A | 'C) ->{⊥} ⊥ fun f: [A, B] -> ([C] -> A | B -> B | C -> A | B | C) -> B f -//│ Type: ['A, 'B] -> (['C] -> ('A ∨ 'B) ->{⊥} ('B ∨ 'C) ->{⊥} ('A ∨ 'B) ∨ 'C) ->{⊥} 'B +//│ Type: ['A, 'B] -> (['C] -> ('A | 'B) ->{⊥} ('B | 'C) ->{⊥} ('A | 'B) | 'C) ->{⊥} 'B diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls index 84a350401b..9b923f445f 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls @@ -18,16 +18,8 @@ let foo = f => (x => f(x(x)) as [A] -> A -> A) in foo f => (let g = x => x(x) in f(g(g))) as [A] -> A -> A //│ Type: (⊥ -> (⊤ -> ⊥)) ->{⊥} ['A] -> ('A) ->{⊥} 'A -:e f => (let g = x => f(x(x)) in g) as [A] -> A -> A -//│ ╔══[ERROR] Type error in block with expected type (A) ->{⊥} A -//│ ║ l.22: f => (let g = x => f(x(x)) in g) as [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}) -//│ Type: (⊥ -> ⊥) ->{⊥} ['A] -> ('A) ->{⊥} 'A +//│ Type: (⊥ ->{⊤} ⊤) ->{⊥} ['A] -> ('A) ->{⊥} 'A f => (x => f(x(x)) as [A] -> A -> A) //│ Type: ('app -> (⊤ -> ⊥)) ->{⊥} ('x -> 'app) ->{⊥} ['A] -> ('A) ->{⊥} 'A @@ -48,14 +40,14 @@ let foo(f) = (f(x => x(x)) as [A] -> A -> A) in foo :todo fun foo(f) = (f(x => x(x)) as [A] -> A -> A) //│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but ('f) ->{⊥} [outer, 'A] -> ('A) ->{⊥} 'A found -//│ ║ l.49: fun foo(f) = (f(x => x(x)) as [A] -> A -> A) +//│ ║ l.41: fun foo(f) = (f(x => x(x)) as [A] -> A -> A) //│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ Type: ⊤ f => (let g = x => x(x) in let tmp = g(g) in f(g)) as [A] -> A -> A -//│ Type: (((('x ∨ ('x ->{'eff} 'app)) -> 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} ['A] -> ('A) ->{⊥} 'A +//│ Type: (((('x | ('x ->{'eff} 'app)) -> 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} ['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/bbDisjoint.mls b/hkmc2/shared/src/test/mlscript/bbml/bbDisjoint.mls index b1dc77f282..9d3badcc60 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbDisjoint.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbDisjoint.mls @@ -9,7 +9,7 @@ data class Pair[P, Q](fst: P, snd: Q) fun fork: [A, B extends ~A, T1, T2] -> (Any ->{A} T1, Any ->{B} T2) ->{A | B} Pair[out T1, out T2] fork -//│ Type: ['A, 'B, 'T1, 'T2] -> ((⊤) ->{'A} 'T1, (⊤) ->{'B} 'T2) ->{'A ∨ 'B} Pair[out 'T1, out 'T2] +//│ Type: ['A, 'B, 'T1, 'T2] -> ((⊤) ->{'A} 'T1, (⊤) ->{'B} 'T2) ->{'A | 'B} Pair[out 'T1, out 'T2] //│ Where: //│ 'B <: ¬'A @@ -63,8 +63,8 @@ region x in //│ ║ l.61: naive_helper(x) //│ ║ ^ //│ ╟── because: cannot constrain Region[x] <: 'r1 -//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'x1 out ¬⊥ ∧ 'x2] ∧ ¬⊥ <: 'r1 -//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'x1 out ¬⊥ ∧ 'x2] ∧ ¬⊥ <: Region[in 'reg out 'reg1] +//│ ╟── because: cannot constrain Region[in ¬⊥ & 'x1 out ¬⊥ & 'x2] & ¬⊥ <: 'r1 +//│ ╟── because: cannot constrain Region[in ¬⊥ & 'x1 out ¬⊥ & 'x2] & ¬⊥ <: Region[in 'reg out 'reg1] //│ ╟── because: cannot constrain 'x2 <: 'reg1 //│ ╟── because: cannot constrain 'x2 <: ¬(¬'reg1) //│ ╟── because: cannot constrain <: ¬(¬'reg1) @@ -74,8 +74,8 @@ region x in //│ ║ l.61: naive_helper(x) //│ ║ ^ //│ ╟── because: cannot constrain Region[x] <: 'r1 -//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'x1 out ¬⊥ ∧ 'x2] ∧ ¬⊥ <: 'r1 -//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'x1 out ¬⊥ ∧ 'x2] ∧ ¬⊥ <: Region[in 'reg out 'reg1] +//│ ╟── because: cannot constrain Region[in ¬⊥ & 'x1 out ¬⊥ & 'x2] & ¬⊥ <: 'r1 +//│ ╟── because: cannot constrain Region[in ¬⊥ & 'x1 out ¬⊥ & 'x2] & ¬⊥ <: Region[in 'reg out 'reg1] //│ ╟── because: cannot constrain 'x2 <: 'reg1 //│ ╟── because: cannot constrain 'x2 <: ¬(¬'reg1) //│ ╟── because: cannot constrain <: ¬(¬'reg1) @@ -88,7 +88,7 @@ region x in //│ ║ ^^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'eff <: ⊥ //│ ╟── because: cannot constrain 'eff <: ¬() -//│ ╟── because: cannot constrain (¬⊥ ∧ 'eff1) ∧ ¬'x3 <: ¬() +//│ ╟── because: cannot constrain (¬⊥ & 'eff1) & ¬'x3 <: ¬() //│ ╟── because: cannot constrain 'eff1 <: 'x3 //│ ╟── because: cannot constrain 'eff1 <: ¬() //│ ╟── because: cannot constrain 'eff1 <: ¬() @@ -137,13 +137,13 @@ region x in //│ ╟── because: cannot constrain x <: 'reg1 //│ ╟── because: cannot constrain x <: 'env //│ ╟── because: cannot constrain x <: 'env -//│ ╙── because: cannot constrain x <: outer ∨ y +//│ ╙── because: cannot constrain x <: outer | y //│ ╔══[ERROR] Type error in region expression with expected type [outer, 'A] -> Int //│ ║ l.129: (region y in let t = helper(x) in 42) as [A] -> Int //│ ║ ^^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'eff <: ⊥ //│ ╟── because: cannot constrain 'eff <: ¬() -//│ ╟── because: cannot constrain (¬⊥ ∧ ¬'y1) ∧ x <: ¬() +//│ ╟── because: cannot constrain (¬⊥ & ¬'y1) & x <: ¬() //│ ╟── because: cannot constrain x <: 'y1 //│ ╙── because: cannot constrain x <: ¬() //│ Type: Int @@ -195,7 +195,7 @@ fun annohelper(r1) = region r2 in fork((_ => r1.ref 1), (_ => r2.ref 2)) annohelper -//│ Type: [outer, 'T] -> (Region['T ∧ outer]) ->{'T ∧ outer} Pair[out Ref[Int, out 'T ∧ outer], out Ref[Int, out ¬outer]] +//│ Type: [outer, 'T] -> (Region['T & outer]) ->{'T & outer} Pair[out Ref[Int, out 'T & outer], out Ref[Int, out ¬outer]] region x in @@ -224,6 +224,7 @@ fun foo(r1) = //│ ╟── because: cannot constrain 'r1 ->{'eff} 'app <: 'foo //│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: 'foo //│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: Region[in 'r2 out 'r21] ->{'eff1} 'app1 +//│ ╟── because: cannot constrain {0: Region[in 'r2 out 'r21]} <: {0: 'r1} //│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1 //│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1 //│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: Region[in 'reg out 'reg1] @@ -231,7 +232,7 @@ fun foo(r1) = //│ ╟── because: cannot constrain 'r21 <: ¬(¬'reg1) //│ ╟── because: cannot constrain ¬outer <: ¬(¬'reg1) //│ ╟── because: cannot constrain ¬outer <: 'reg1 -//│ ╟── because: cannot constrain ¬outer <: ¬'r22 ∨ outer +//│ ╟── because: cannot constrain ¬outer <: ¬'r22 | outer //│ ╟── because: cannot constrain 'r22 <: ¬(¬outer) //│ ╙── because: cannot constrain ¬outer <: ¬(¬outer) //│ ╔══[ERROR] Type error in function literal @@ -246,6 +247,7 @@ fun foo(r1) = //│ ╟── because: cannot constrain 'r1 ->{'eff} 'app <: 'foo //│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: 'foo //│ ╟── because: cannot constrain ('r1) ->{'eff} ('app) <: Region[in 'r2 out 'r21] ->{'eff1} 'app1 +//│ ╟── because: cannot constrain {0: Region[in 'r2 out 'r21]} <: {0: 'r1} //│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1 //│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: 'r1 //│ ╟── because: cannot constrain Region[in 'r2 out 'r21] <: Region[in 'reg out 'reg1] @@ -307,7 +309,12 @@ fun foo(f) = borrow(r) of it => foo(f) foo -//│ Type: [outer, 'n, 'eff] -> (('n ->{¬outer} ('n ∨ Int)) ->{'eff} ⊤) ->{'eff} ⊥ +//│ Type: [outer, 'f, 'n, 'eff, 'app, 'eff1, 'eff2, 'T] -> 'f ->{'eff | 'eff1} 'app //│ Where: //│ 'n <: Int -//│ 'eff <: outer +//│ 'f <: ('n ->{¬outer} ('n | Int)) ->{'eff} ⊤ +//│ 'f#'f ∨ ( 'f#'f ∨ 'T <: 'app ∧ 'eff1 <: 'eff2){0: 'f} <: {0: 'f} +//│ 'app <: 'T +//│ 'eff2 <: outer +//│ 'eff <: 'eff1 +//│ 'eff2 <: 'eff1 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls index 5870cafe34..df3e9c8110 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls @@ -41,12 +41,22 @@ 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 (¬⊥ ∧ ¬'x1) ∧ y <: ¬() +//│ ╟── because: cannot constrain (¬⊥ & ¬'x1) & y <: ¬() //│ ╟── because: cannot constrain y <: 'x1 //│ ╙── because: cannot constrain y <: ¬() //│ Type: CodeBase[out 'y -> 'y, ⊥, ?] //│ Where: -//│ 'y <: Int +//│ 'x#'x ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'cde1#'cde1 ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x2#'x ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x2#'x ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x <: 'cde1 +//│ 'cde1#'cde1 ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'y <: 'cde2 +//│ 'x#'x ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'cde <: 'cde3 +//│ 'app <: ¬(¬'cde) +//│ 'x2 <: 'x data class C[A](m: A, n: A -> Int) //│ Type: ⊤ @@ -54,7 +64,7 @@ data class C[A](m: A, n: A -> Int) fun f: [A] -> ([B] -> (C[out B] & A) -> B) -> A -> Int f -//│ Type: ['A] -> (['B] -> (C[out 'B] ∧ 'A) ->{⊥} 'B) ->{⊥} ('A) ->{⊥} Int +//│ Type: ['A] -> (['B] -> (C[out 'B] & 'A) ->{⊥} 'B) ->{⊥} ('A) ->{⊥} Int fun g: [D] -> C[in Int out D] -> D g @@ -62,7 +72,9 @@ g f(g) -//│ Type: (¬C[?] ∨ C[in Int out ⊥]) ->{⊥} Int +//│ Type: ('A) ->{⊥} Int +//│ Where: +//│ 'A#C ∨ ( 'A#C ∨ 'D <: B ∧ ⊥ <: ⊥){0: C[out B] & 'A} <: {0: C[in Int out 'D]} fun foo: C[in Int out Nothing] foo @@ -78,16 +90,19 @@ f(g)(foo) :fixme // ??? f(g)(bar) //│ ╔══[ERROR] Type error in reference with expected type 'A -//│ ║ l.79: f(g)(bar) +//│ ║ l.91: 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 <: 'B1 -//│ ╟── because: cannot constrain Int ∧ 'B <: 'B1 -//│ ╟── because: cannot constrain Int ∧ 'B <: ¬() -//│ ╟── because: cannot constrain 'B <: ¬(Int) +//│ ╟── because: cannot constrain {0: C[out B] & 'A} <: {0: C[in Int out 'D]} +//│ ╟── because: cannot constrain C[in ⊥ out B] ∧ 'A <: C[in Int out 'D] +//│ ╟── because: cannot constrain 'A <: ¬C[in ⊥ out ¬⊥ & 'B1] | C[in Int out ¬⊥ & 'D1] +//│ ╟── because: cannot constrain C[in Int out Int] <: ¬C[in ⊥ out ¬⊥ & 'B1] | C[in Int out ¬⊥ & 'D1] +//│ ╟── because: cannot constrain (Int) & ('B1) <: ¬⊥ & 'D1 +//│ ╟── because: cannot constrain Int ∧ 'B1 <: 'D1 +//│ ╟── because: cannot constrain Int ∧ 'B1 <: 'B2 +//│ ╟── because: cannot constrain Int ∧ 'B1 <: 'B2 +//│ ╟── because: cannot constrain Int ∧ 'B1 <: ¬() +//│ ╟── because: cannot constrain 'B1 <: ¬(Int) //│ ╙── because: cannot constrain <: ¬(Int) //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls index caca71ece7..302a64314d 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls @@ -17,7 +17,20 @@ fun id(x) = x run(x `=> id(x) `* x) -//│ Type: Int -> Int +//│ Type: 'x -> 'cde +//│ Where: +//│ 'x#'x1 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'cde1#'cde1 ∨ 'x#'x1 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x#'x1 ∨ 'cde2#'cde2 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x <: 'x1 +//│ 'x1#'x1 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'cde1#'cde1 ∨ 'x1#'x1 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x1#'x1 ∨ 'cde2#'cde2 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x1 <: 'cde1 +//│ 'cde1#'cde1 ∨ 'cde2#'cde2 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x1 <: 'cde2 +//│ 'cde3 <: 'cde +//│ 'app <: ¬(¬'cde3) fun assertNotZero: [C] -> CodeBase[out Num, out C, out Any] -> CodeBase[out Num, out C, out Any] @@ -25,7 +38,17 @@ fun assertNotZero(x) = `if (x `== `0.0) then `error else x let checkedDiv = x `=> y `=> x `/. (assertNotZero(y)) run(checkedDiv) -//│ Type: Num -> (Num -> Num) +//│ Type: 'x -> (Num -> 'cde) +//│ Where: +//│ 'x#'x1 ∨ ( 'x1#Num ∨ Num <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Num ∨ Num <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Num, 1: Num} +//│ 'x <: 'x1 +//│ 'x1#'x1 ∨ ( 'x1#Num ∨ Num <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Num ∨ Num <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Num, 1: Num} +//│ 'x1 <: 'cde1 +//│ 'cde1#'cde1 ∨ ( 'x1#Num ∨ Num <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Num ∨ Num <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Num, 1: Num} +//│ Num <: 'cde2 +//│ 'cde3 <: 'cde +//│ 'cde4 <: 'cde3 +//│ 'app <: ¬(¬'cde4) @@ -38,10 +61,30 @@ show fun inc(dbg) = x `=> let c = x `+ `1 in let t = dbg(c) in c inc -//│ Type: ['eff] -> (CodeBase[out Int, ?, ?] ->{'eff} ⊤) ->{'eff} CodeBase[out Int -> Int, ⊥, ?] +//│ Type: ['x, 'cde, 'cde1, 'app, 'app1, 'eff, 'cde2, 'x1] -> (CodeBase[out 'app1, ?, ?] ->{'eff} ⊤) ->{'eff} CodeBase[out 'x -> 'cde2, ⊥, ?] +//│ Where: +//│ 'x#'x1 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde, 1: 'cde1} <: {0: Int, 1: Int} +//│ 'x1 <: 'cde +//│ 'cde#'cde ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde, 1: 'cde1} <: {0: Int, 1: Int} +//│ Int <: 'cde1 +//│ 'cde2 <: ⊤ +//│ 'app <: 'cde2 +//│ 'app <: 'app1 +//│ 'x <: 'x1 +//│ 'x1#'x1 ∨ ( 'x1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde, 1: 'cde1} <: {0: Int, 1: Int} inc(c => log(show(c))) -//│ Type: CodeBase[out Int -> Int, ⊥, ?] +//│ Type: CodeBase[out 'x -> 'cde, ⊥, ?] +//│ Where: +//│ 'x1#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int & ¬⊥, 1: Int & ¬⊥} +//│ 'x <: 'cde1 +//│ 'cde1#'cde1 ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int & ¬⊥, 1: Int & ¬⊥} +//│ Int <: 'cde2 +//│ 'cde <: ⊤ +//│ 'app <: 'cde +//│ 'app <: 'app1 +//│ 'x1 <: 'x +//│ 'x#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int & ¬⊥, 1: Int & ¬⊥} fun body: [T, C] -> (CodeBase[out Int, out T, out Any], CodeBase[out Int, out C, out Any]) -> Int -> CodeBase[out Int, out T | C, out Any] @@ -56,29 +99,21 @@ let gn5 = run(gib_naive(5)) fun bind(rhs, k) = `let x = rhs `in k(x) bind -//│ Type: ['cde, 'ctx, 'cde1, 'eff, 'cde2, 'ctx1] -> (CodeBase[out 'cde, out 'ctx, ?], CodeBase[in 'cde1 out 'cde1 ∨ 'cde, ?, ⊥] ->{'eff} CodeBase[out 'cde2, out 'ctx1, ?]) ->{'eff} CodeBase[out 'cde2, out 'ctx ∨ 'ctx1, ?] +//│ Type: ['cde, 'ctx, 'cde1, 'eff, 'cde2, 'ctx1] -> (CodeBase[out 'cde, out 'ctx, ?], CodeBase[in 'cde1 out 'cde1 | 'cde, ?, ⊥] ->{'eff} CodeBase[out 'cde2, out 'ctx1, ?]) ->{'eff} CodeBase[out 'cde2, out 'ctx | 'ctx1, ?] +:todo :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] 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, ?] -//│ ║ 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) //│ 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: ['G] -> (CodeBase[out Int, out 'G, ?], ['C] -> (CodeBase[out Int, out 'C, ?]) ->{⊥} CodeBase[out Int, out 'C ∨ 'G, ?]) ->{⊥} CodeBase[out Int, out 'G, ?] +//│ Type: ['G] -> (CodeBase[out Int, out 'G, ?], ['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] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbGetters.mls b/hkmc2/shared/src/test/mlscript/bbml/bbGetters.mls index feb6229bcb..60bae65382 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbGetters.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbGetters.mls @@ -37,7 +37,7 @@ fun test2() = 0 then 0 n then funny(n - 1) + 1 funny -//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but () ->{⊥} [outer, 'caseScrut, 'eff] -> 'caseScrut ->{'eff} Int found +//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but () ->{⊥} [outer, 'caseScrut, 'res, 'eff] -> 'caseScrut ->{'eff} 'res found //│ ║ l.37: 0 then 0 //│ ║ ^ //│ ║ l.38: n then funny(n - 1) + 1 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls index fd6a13fb37..330cf1e639 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: ['E, 'Res] -> (['R] -> (Region['R]) ->{'E ∨ 'R} 'Res) ->{'E} 'Res +//│ Type: ['E, 'Res] -> (['R] -> (Region['R]) ->{'E | 'R} 'Res) ->{'E} 'Res letreg(r => r) //│ Type: Region[?] @@ -20,7 +20,7 @@ letreg(r => r).ref 1 //│ ║ ^^^^^^^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'Res <: Region['reg] //│ ╟── because: cannot constrain 'Res <: ¬(¬{Region['reg]}) -//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ 'R out ¬⊥ ∧ 'R1] ∧ ¬⊥ <: ¬(¬{Region['reg]}) +//│ ╟── because: cannot constrain Region[in ¬⊥ & 'R out ¬⊥ & 'R1] & ¬⊥ <: ¬(¬{Region['reg]}) //│ ╟── because: cannot constrain 'R1 <: 'reg //│ ╟── because: cannot constrain 'R1 <: 'reg //│ ╟── because: cannot constrain 'R1 <: ¬(¬'R) @@ -31,7 +31,7 @@ letreg(r => r).ref 1 //│ ╔══[ERROR] Type error in block //│ ║ l.17: letreg(r => r).ref 1 //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain 'reg ∨ 'E <: ⊥ +//│ ╟── because: cannot constrain 'reg | 'E <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() //│ ╟── because: cannot constrain 'R1 <: ¬() //│ ╟── because: cannot constrain 'R1 <: ¬() @@ -49,11 +49,11 @@ 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 | 'E <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() //│ ╟── because: cannot constrain 'reg1 <: ¬() //│ ╟── because: cannot constrain 'reg1 <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ 'R <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & 'R <: ¬() //│ ╟── because: cannot constrain 'R <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -75,11 +75,11 @@ 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 | 'E <: ⊥ //│ ╟── because: cannot constrain 'eff <: ¬() //│ ╟── because: cannot constrain 'reg <: ¬() //│ ╟── because: cannot constrain 'reg <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ 'R <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & 'R <: ¬() //│ ╟── because: cannot constrain 'R <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Ref['arg, ?] @@ -108,7 +108,7 @@ letreg(r => !(r.ref 1)) //│ ╔══[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 | 'reg1 <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() //│ ╟── because: cannot constrain 'reg1 <: ¬() //│ ╟── because: cannot constrain 'reg1 <: ¬() @@ -116,7 +116,7 @@ letreg(r => !(r.ref 1)) //│ ╔══[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 | 'reg1 <: ⊥ //│ ╟── because: cannot constrain 'reg1 <: ¬() //│ ╙── 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 d88a66cf24..932fe99491 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls @@ -63,9 +63,9 @@ fun mapi = s => //│ ╟── 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 'reg <: ¬(¬E) -//│ ╟── because: cannot constrain (¬⊥ ∧ 'r) ∧ ¬outer <: ¬(¬E) +//│ ╟── because: cannot constrain (¬⊥ & 'r) & ¬outer <: ¬(¬E) //│ ╟── because: cannot constrain 'r <: ¬(¬E ∧ ¬outer) //│ ╙── because: cannot constrain ¬outer <: ¬(¬E ∧ ¬outer) //│ ╔══[ERROR] Type error in region expression with expected type ((Int, A) ->{E} A) ->{E} List[out A] @@ -80,9 +80,9 @@ fun mapi = s => //│ ╟── 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 'reg <: ¬(¬E) -//│ ╟── because: cannot constrain (¬⊥ ∧ 'r) ∧ ¬outer <: ¬(¬E) +//│ ╟── because: cannot constrain (¬⊥ & 'r) & ¬outer <: ¬(¬E) //│ ╟── because: cannot constrain 'r <: ¬(¬E ∧ ¬outer) //│ ╙── because: cannot constrain ¬outer <: ¬(¬E ∧ ¬outer) //│ ╔══[ERROR] Type error in region expression with expected type ((Int, A) ->{E} A) ->{E} List[out A] @@ -97,12 +97,67 @@ fun mapi = s => //│ ╟── 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 'reg <: ¬(¬E) -//│ ╟── because: cannot constrain (¬⊥ ∧ 'r) ∧ ¬outer <: ¬(¬E) +//│ ╟── because: cannot constrain (¬⊥ & 'r) & ¬outer <: ¬(¬E) //│ ╟── because: cannot constrain 'r <: ¬(¬E ∧ ¬outer) //│ ╙── because: cannot constrain ¬outer <: ¬(¬E ∧ ¬outer) //│ Type: ⊤ +fun mapii = s => + region r in + let i = r.ref 0 + f => map(s) of x => + i := !i + 1 + f(!i, x) +//│ Type: ⊤ - +:e +region r in + let sum = r.ref 0 + let s1 = mkList of !sum + let s2 = mapii(s1) of (x, i) => x * i + !sum + head(s2) +//│ ╔══[ERROR] Type error in block +//│ ║ l.117: let sum = r.ref 0 +//│ ║ ^^^^^^^ +//│ ║ l.118: let s1 = mkList of !sum +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.119: let s2 = mapii(s1) of (x, i) => x * i +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.120: !sum + head(s2) +//│ ║ ^^^^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'eff <: ⊥ +//│ ╟── because: cannot constrain 'eff <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & ¬'r <: ¬() +//│ ╟── because: cannot constrain <: 'r +//│ ╙── because: cannot constrain <: ¬() +//│ ╔══[ERROR] Type error in block +//│ ║ l.117: let sum = r.ref 0 +//│ ║ ^^^^^^^ +//│ ║ l.118: let s1 = mkList of !sum +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.119: let s2 = mapii(s1) of (x, i) => x * i +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.120: !sum + head(s2) +//│ ║ ^^^^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'eff <: ⊥ +//│ ╟── because: cannot constrain 'eff <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & ¬'r1 <: ¬() +//│ ╟── because: cannot constrain <: 'r1 +//│ ╙── because: cannot constrain <: ¬() +//│ ╔══[ERROR] Type error in block +//│ ║ l.117: let sum = r.ref 0 +//│ ║ ^^^^^^^ +//│ ║ l.118: let s1 = mkList of !sum +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.119: let s2 = mapii(s1) of (x, i) => x * i +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.120: !sum + head(s2) +//│ ║ ^^^^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'eff <: ⊥ +//│ ╟── because: cannot constrain 'eff <: ¬() +//│ ╟── because: cannot constrain ¬⊥ & ¬'r2 <: ¬() +//│ ╟── because: cannot constrain <: 'r2 +//│ ╙── because: cannot constrain <: ¬() +//│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls b/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls index 12253e77c7..a9d59cb42c 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls @@ -28,6 +28,6 @@ opt => opt as Option[out Int] //│ Type: (Option[out Int]) ->{⊥} Option[out Int] opt => (opt as Option[Int]) as Option[Int | Str] -//│ Type: (Option[out Int ∨ Str] ∧ Option[out Int]) ->{⊥} Option[out Int ∨ Str] +//│ Type: (Option[out Int | Str] & Option[out Int]) ->{⊥} Option[out Int | Str] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls index a66aa7ec02..661630a0d4 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls @@ -136,7 +136,7 @@ new Some((x => x) as [A] -> A -> A) //│ 'x -> 'x <: 'A let s = new Some((x => x) as [A] -> A -> A) in let t = s.Some#value(42) in s.Some#value(false) -//│ Type: Bool ∨ Int +//│ Type: Bool | Int fun gen: Int -> [A] -> A -> A fun gen(x) = diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls index 677363781a..8d600ea416 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls @@ -41,16 +41,48 @@ f `=> x `=> f`(x) x `=> y `=> x `+ y -//│ Type: CodeBase[out Int -> (Int -> Int), ⊥, ?] +//│ Type: CodeBase[out 'x -> ('x -> 'cde), ⊥, ?] +//│ Where: +//│ 'x#'x ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x#'x ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x#'x ∨ 'y1#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'cde1#'cde1 ∨ 'y1#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x <: 'cde1 +//│ 'cde1#'cde1 ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'cde1#'cde1 ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'y <: 'cde2 +//│ 'cde3 <: 'cde +//│ 'app <: ¬(¬'cde3) +//│ 'y1 <: 'y (x, y) `=> x `+ y -//│ Type: CodeBase[out (Int, Int) -> Int, ⊥, ?] +//│ Type: CodeBase[out ('x, 'x) -> 'cde, ⊥, ?] +//│ Where: +//│ 'x#'x ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x#'x ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'cde1#'cde1 ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x <: 'cde1 +//│ 'cde1#'cde1 ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'y <: 'cde2 +//│ 'app <: ¬(¬'cde) (x, y, z) `=> x `+ y `+ z -//│ Type: CodeBase[out (Int, Int, Int) -> Int, ⊥, ?] +//│ Type: CodeBase[out ('x, 'x, 'z) -> 'cde, ⊥, ?] +//│ Where: +//│ 'x#'x ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x#'x ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'cde1#'cde1 ∨ 'y#'y ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'x <: 'cde1 +//│ 'cde1#'cde1 ∨ 'cde2#'cde2 ∨ ( 'x#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'y#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'x#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde1#Int ∨ 'cde2#Int ∨ Int <: 'app ∧ ⊥ <: ⊥){0: 'cde1, 1: 'cde2} <: {0: Int, 1: Int} +//│ 'y <: 'cde2 +//│ 'cde3#'cde3 ∨ 'z#'z ∨ ( 'cde3#Int ∨ 'z#Int ∨ Int <: 'app1 ∧ ⊥ <: ⊥) ∧ ( 'cde3#Int ∨ 'cde4#Int ∨ Int <: 'app1 ∧ ⊥ <: ⊥){0: 'cde3, 1: 'cde4} <: {0: Int, 1: Int} +//│ 'cde3#'cde3 ∨ 'cde4#'cde4 ∨ ( 'cde3#Int ∨ 'z#Int ∨ Int <: 'app1 ∧ ⊥ <: ⊥) ∧ ( 'cde3#Int ∨ 'cde4#Int ∨ Int <: 'app1 ∧ ⊥ <: ⊥){0: 'cde3, 1: 'cde4} <: {0: Int, 1: Int} +//│ 'z <: 'cde4 +//│ 'app1 <: ¬(¬'cde) +//│ 'app <: ¬(¬'cde3) f `=> x `=> y `=> f`(x, y) //│ Type: CodeBase[out (('x, 'y) -> 'app) -> ('x -> ('y -> 'app)), ⊥, ?] @@ -61,7 +93,7 @@ f `=> x `=> y `=> f`(x, y) :e `let x = 42 `in x //│ ╔══[ERROR] Type error in unquoted term -//│ ║ l.62: `let x = 42 `in x +//│ ║ l.94: `let x = 42 `in x //│ ║ ^^ //│ ╙── because: cannot constrain Int <: CodeBase[out 'cde, out 'ctx, ?] //│ Type: CodeBase[⊥, ⊥, ?] @@ -69,8 +101,8 @@ f `=> x `=> y `=> f`(x, y) :e `let x = `0 `in 1 //│ ╔══[ERROR] Type error in unquoted term -//│ ║ l.70: `let x = `0 `in 1 -//│ ║ ^ +//│ ║ l.102: `let x = `0 `in 1 +//│ ║ ^ //│ ╙── because: cannot constrain Int <: CodeBase[out 'cde, out 'ctx, ?] //│ Type: CodeBase[⊥, ⊥, ?] @@ -82,7 +114,14 @@ 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), ⊥, ?] +//│ Where: +//│ 'x#'x ∨ ( 'x#'x ∨ Bool <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde#'cde ∨ Bool <: 'app ∧ ⊥ <: ⊥){0: 'cde, 1: 'cde1} <: {0: 'T, 1: 'T} +//│ 'x <: 'cde +//│ 'cde#'cde ∨ ( 'x#'x ∨ Bool <: 'app ∧ ⊥ <: ⊥) ∧ ( 'cde#'cde ∨ Bool <: 'app ∧ ⊥ <: ⊥){0: 'cde, 1: 'cde1} <: {0: 'T, 1: 'T} +//│ Num <: 'cde1 +//│ 'cde2 <: ¬(¬{Bool}) +//│ 'app <: ¬(¬'cde2) run(`1) //│ Type: Int @@ -91,15 +130,15 @@ run(`1) :e run(1) //│ ╔══[ERROR] Type error in integer literal with expected type CodeBase[out 'T, ⊥, ?] -//│ ║ l.92: run(1) -//│ ║ ^ +//│ ║ l.131: run(1) +//│ ║ ^ //│ ╙── because: cannot constrain Int <: CodeBase[out 'T, ⊥, ?] //│ Type: ⊥ :e x `=> run(x) //│ ╔══[ERROR] Type error in reference with expected type CodeBase[out 'T, ⊥, ?] -//│ ║ l.100: x `=> run(x) +//│ ║ l.139: x `=> run(x) //│ ║ ^ //│ ╟── because: cannot constrain CodeBase['x, x, ⊥] <: CodeBase[out 'T, ⊥, ?] //│ ╙── because: cannot constrain x <: ⊥ @@ -108,12 +147,12 @@ x `=> run(x) :e `let x = `42 `in run(x) //│ ╔══[ERROR] Type error in reference with expected type CodeBase[out 'T, ⊥, ?] -//│ ║ l.109: `let x = `42 `in run(x) +//│ ║ l.148: `let x = `42 `in run(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) +//│ ║ l.148: `let x = `42 `in run(x) //│ ║ ^^^^^^ //│ ╟── because: cannot constrain 'T <: CodeBase[out 'cde1, out 'ctx, ?] //│ ╟── because: cannot constrain 'T <: ¬(¬{CodeBase[out 'cde1, out 'ctx, ?]}) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls index f4e3c9c8cc..7c44341a9f 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls @@ -35,13 +35,12 @@ f fun f(x) = f(x) f -//│ Type: ⊤ -> ⊥ +//│ Type: ['x, 'eff, 'app] -> 'x ->{'eff} 'app +//│ Where: +//│ 'x#'x ∨ ( 'x#'x ∨ 'app <: 'app ∧ 'eff <: 'eff){0: 'x} <: {0: 'x} + -:todo fun f(x) = f(x.a) -//│ ╔══[ERROR] Term shape not yet supported by BbML: Sel(Ref(x),Ident(a)) -//│ ║ l.41: fun f(x) = f(x.a) -//│ ╙── ^^^ //│ Type: ⊤ @@ -51,7 +50,7 @@ data class Foo[A](a: A) :todo proper error Foo(123) //│ ╔══[ERROR] Variable not found: Foo -//│ ║ l.52: Foo(123) +//│ ║ l.51: Foo(123) //│ ╙── ^^^ //│ Type: ⊥ @@ -62,15 +61,16 @@ new Foo(123) :todo proper error fun f(x) = f(Foo.a(x)) -//│ ╔══[ERROR] Term shape not yet supported by BbML: Sel(Ref(member:Foo),Ident(a)) -//│ ║ l.64: fun f(x) = f(Foo.a(x)) -//│ ╙── ^^^^^ +//│ ╔══[ERROR] Variable not found: Foo +//│ ║ l.63: fun f(x) = f(Foo.a(x)) +//│ ╙── ^^^ //│ Type: ⊤ fun f(x) = f(x.Foo#a) f -//│ Type: ['x] -> Foo[out 'x] -> ⊥ +//│ Type: ['x, 'A, 'eff, 'app] -> Foo[out 'A] ->{'eff} 'app //│ Where: -//│ 'x <: Foo[out 'x] +//│ 'A#'A ∨ ( 'A#'A ∨ 'app <: 'app ∧ 'eff <: 'eff){0: 'A} <: {0: 'x} +//│ 'x <: Foo[out 'A] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls index 22701e863c..2dffe478c4 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls @@ -25,11 +25,11 @@ let r = region x in x.ref 42 //│ ║ ^^^^^^^^ //│ ║ l.22: !r //│ ║ ^^ -//│ ╟── because: cannot constrain 'reg ∨ 'eff <: ⊥ +//│ ╟── 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 'x <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -54,7 +54,7 @@ let t = region x in x in t.ref 42 //│ ╔══[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 | 'eff <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() //│ ╟── because: cannot constrain 'x1 <: ¬() //│ ╟── because: cannot constrain 'x1 <: ¬() @@ -75,11 +75,11 @@ in t := 0 //│ ║ ^^^^^^^^ //│ ║ l.72: in t := 0 //│ ║ ^^^^^^^^^ -//│ ╟── because: cannot constrain 'reg ∨ 'eff <: ⊥ +//│ ╟── 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 'x <: ¬() //│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -98,11 +98,11 @@ in !t //│ ║ ^^^^^^^^ //│ ║ l.95: in !t //│ ║ ^^^^^ -//│ ╟── because: cannot constrain 'reg ∨ 'eff <: ⊥ +//│ ╟── 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 'x <: ¬() //│ ╙── 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 | 'eff <: ⊥ //│ ╟── because: cannot constrain 'reg <: ¬() -//│ ╟── because: cannot constrain ¬⊥ ∧ 'x <: ¬() +//│ ╟── 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) = @@ -172,7 +172,7 @@ foo //│ '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) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls index b0cb998168..32b9809f84 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls @@ -47,9 +47,9 @@ fun mapi = s => f => //│ ╟── 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 'reg <: ¬(¬E) -//│ ╟── because: cannot constrain (¬⊥ ∧ 'r) ∧ ¬outer <: ¬(¬E) +//│ ╟── because: cannot constrain (¬⊥ & 'r) & ¬outer <: ¬(¬E) //│ ╟── because: cannot constrain 'r <: ¬(¬E ∧ ¬outer) //│ ╙── because: cannot constrain ¬outer <: ¬(¬E ∧ ¬outer) //│ ╔══[ERROR] Type error in region expression with expected type Seq[out A, out E] @@ -64,9 +64,9 @@ fun mapi = s => f => //│ ╟── 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 'reg <: ¬(¬E) -//│ ╟── because: cannot constrain (¬⊥ ∧ 'r) ∧ ¬outer <: ¬(¬E) +//│ ╟── because: cannot constrain (¬⊥ & 'r) & ¬outer <: ¬(¬E) //│ ╟── because: cannot constrain 'r <: ¬(¬E ∧ ¬outer) //│ ╙── because: cannot constrain ¬outer <: ¬(¬E ∧ ¬outer) //│ ╔══[ERROR] Type error in region expression with expected type Seq[out A, out E] @@ -81,9 +81,9 @@ fun mapi = s => f => //│ ╟── 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 'reg <: ¬(¬E) -//│ ╟── because: cannot constrain (¬⊥ ∧ 'r) ∧ ¬outer <: ¬(¬E) +//│ ╟── because: cannot constrain (¬⊥ & 'r) & ¬outer <: ¬(¬E) //│ ╟── because: cannot constrain 'r <: ¬(¬E ∧ ¬outer) //│ ╙── because: cannot constrain ¬outer <: ¬(¬E ∧ ¬outer) //│ Type: ⊤ @@ -96,7 +96,7 @@ fun mapi = s => f => i := !i + 1 f(!i, x) mapi -//│ Type: [outer, 'A, 'E, 'app, 'eff] -> Seq[out 'A, out 'E] -> (((Int, 'A) ->{'eff} 'app) -> Seq[out 'app, out (¬outer ∨ 'eff) ∨ 'E]) +//│ Type: [outer, 'A, 'E, 'app, 'eff] -> Seq[out 'A, out 'E] -> (((Int, 'A) ->{'eff} 'app) -> Seq[out 'app, out (¬outer | 'eff) | 'E]) // * 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] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbVariance.mls b/hkmc2/shared/src/test/mlscript/bbml/bbVariance.mls index 62e56acddf..75a466abc0 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbVariance.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbVariance.mls @@ -7,13 +7,13 @@ class Foo[out A] //│ Type: ⊤ (x: Foo[Int]) => (x as Foo[Int | Str]) -//│ Type: (Foo[out Int]) ->{⊥} Foo[out Int ∨ Str] +//│ Type: (Foo[out Int]) ->{⊥} Foo[out Int | Str] class Foo[in A] //│ Type: ⊤ (x: Foo[Int]) => (x as Foo[Int & Str]) -//│ Type: (Foo[in Int]) ->{⊥} Foo[in Int ∧ Str] +//│ Type: (Foo[in Int]) ->{⊥} Foo[in Int & Str] diff --git a/hkmc2/shared/src/test/mlscript/logicsub/DisjSub.mls b/hkmc2/shared/src/test/mlscript/logicsub/DisjSub.mls new file mode 100644 index 0000000000..489e0ac192 --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/DisjSub.mls @@ -0,0 +1,273 @@ +:bbml +//│ Type: ⊤ + +//│ Type: ⊤ + + +fun andt(x) = x && true +fun k(f: Nothing -> Bool) = 1 +fun ap(f) = x => f(x) +//│ Type: ⊤ + +k(andt) +//│ Type: Int + +k(ap(andt)) +//│ Type: Int + +k(k) +//│ Type: Int + +fun idIB: (Int -> Int) & (Bool -> Bool) +//│ Type: ⊤ + +idIB(1) +//│ Type: Int + +idIB(true) +//│ Type: Bool + +idIB(if true then 1 else true) +//│ Type: Int + +x => + let y = x+1 + idIB(x) +//│ Type: ('x) ->{'eff} 'app +//│ Where: +//│ 'x <: Int +//│ 'x#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: 'eff) ∧ ( 'x#Bool ∨ Bool <: 'app ∧ ⊥ <: 'eff){0: 'x} <: {0: Int} | {0: Bool} + +(x: Int) => + let y = x + 1 + idIB(x) +//│ Type: (Int) ->{⊥} Int + +(x: Bool) => + idIB(x) +//│ Type: (Bool) ->{⊥} Bool + +(x: Bool) => + idIB(idIB(x)) +//│ Type: (Bool) ->{⊥} Bool + +fun ap1(f)=f(1) +ap1(idIB) +//│ Type: Int + +ap(idIB)(1) +//│ Type: Int + +x => idIB(x) +//│ Type: ('x) ->{'eff} 'app +//│ Where: +//│ 'x#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: 'eff) ∧ ( 'x#Bool ∨ Bool <: 'app ∧ ⊥ <: 'eff){0: 'x} <: {0: Int} | {0: Bool} + +fun forward(x) = idIB(x) +forward +//│ Type: ['x, 'eff, 'app] -> 'x ->{'eff} 'app +//│ Where: +//│ 'x#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: 'eff) ∧ ( 'x#Bool ∨ Bool <: 'app ∧ ⊥ <: 'eff){0: 'x} <: {0: Int} | {0: Bool} + +forward(1) +//│ Type: Int + +forward(true) +//│ Type: Bool + + +:todo // BbML +fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool) +//│ ╔══[ERROR] General type is not allowed here. +//│ ║ l.80: fun idIIBB: ([Int, Int] -> Int) & ([Bool, Bool] -> Bool) +//│ ╙── ^^^ +//│ ╔══[ERROR] General type is not allowed here. +//│ ║ 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.90: idIIBB([1, 2]) +//│ ╙── ^^^^^^ +//│ Type: ⊥ + +class Pair[out A, out B](fst: A, snd: B) +//│ Type: ⊤ + +new Pair(1, 2) +//│ Type: Pair['A, 'B] +//│ Where: +//│ Int <: 'A +//│ Int <: 'B + +// WF check on intersection types +:e +fun idIIBB: (Pair[Int, Int] -> Int) & (Pair[Bool, Bool] -> Bool) +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.107: fun idIIBB: (Pair[Int, Int] -> Int) & (Pair[Bool, Bool] -> Bool) +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +:e +idIIBB(new Pair(1, 2)) +//│ ╔══[ERROR] Type error in application +//│ ║ l.114: 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 {0: Pair['A, 'B]} <: {0: Pair[in ⊥ out Int, in ⊥ out Int]} | {0: Pair[in ⊥ out Bool, in ⊥ out Bool]} +//│ ╟── because: cannot constrain {0: Pair['A, 'B]} & {0: Pair[?, ?]} <: {0: Pair[in ⊥ out Bool, in ⊥ out Bool]} +//│ ╟── because: cannot constrain (Pair['A, 'B]) & (Pair[in ⊥ out , in ⊥ out ]) <: 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.114: 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 {0: Pair['A, 'B]} <: {0: Pair[in ⊥ out Int, in ⊥ out Int]} | {0: Pair[in ⊥ out Bool, in ⊥ out Bool]} +//│ ╟── because: cannot constrain {0: Pair['A, 'B]} & {0: Pair[?, ?]} <: {0: Pair[in ⊥ out Bool, in ⊥ out Bool]} +//│ ╟── because: cannot constrain (Pair['A, 'B]) & (Pair[in ⊥ out , in ⊥ out ]) <: Pair[in ⊥ out Bool, in ⊥ out Bool] +//│ ╟── because: cannot constrain ('B) & () <: Bool +//│ ╟── because: cannot constrain 'B <: ¬(¬{Bool}) +//│ ╙── because: cannot constrain Int <: ¬(¬{Bool}) +//│ Type: Bool | Int + +:e +idIIBB(new Pair(1, true)) +//│ ╔══[ERROR] Type error in application +//│ ║ l.138: 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 {0: Pair['A, 'B]} <: {0: Pair[in ⊥ out Int, in ⊥ out Int]} | {0: Pair[in ⊥ out Bool, in ⊥ out Bool]} +//│ ╟── because: cannot constrain {0: Pair['A, 'B]} & {0: Pair[?, ?]} <: {0: Pair[in ⊥ out Int, in ⊥ out Int]} +//│ ╟── because: cannot constrain (Pair['A, 'B]) & (Pair[in ⊥ out , in ⊥ out ]) <: 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.138: 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 {0: Pair['A, 'B]} <: {0: Pair[in ⊥ out Int, in ⊥ out Int]} | {0: Pair[in ⊥ out Bool, in ⊥ out Bool]} +//│ ╟── because: cannot constrain {0: Pair['A, 'B]} & {0: Pair[?, ?]} <: {0: Pair[in ⊥ out Bool, in ⊥ out Bool]} +//│ ╟── because: cannot constrain (Pair['A, 'B]) & (Pair[in ⊥ out , in ⊥ out ]) <: Pair[in ⊥ out Bool, in ⊥ out Bool] +//│ ╟── because: cannot constrain ('A) & () <: Bool +//│ ╟── because: cannot constrain 'A <: ¬(¬{Bool}) +//│ ╙── because: cannot constrain Int <: ¬(¬{Bool}) +//│ Type: Bool | Int + + + + +fun foo: ["x": Int, "y": Int] +//│ Type: ⊤ + +foo +//│ Type: {x: Int, y: Int} + +:todo +fun foo(x) = if x is + [true, true] then 1 + [false, false] then 2 +//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(x),Tuple(2,false),Let($first0,SynthSel(Ref(x),Ident(0)),Let($first1,SynthSel(Ref(x),Ident(1)),Cons(Branch(Ref($first0),Lit(BoolLit(true)),Cons(Branch(Ref($first1),Lit(BoolLit(true)),Else(Lit(IntLit(1)))),End)),End)))),Cons(Branch(Ref(x),Tuple(2,false),Let($first0,SynthSel(Ref(x),Ident(0)),Let($first1,SynthSel(Ref(x),Ident(1)),Cons(Branch(Ref($first0),Lit(BoolLit(false)),Cons(Branch(Ref($first1),Lit(BoolLit(false)),Else(Lit(IntLit(2)))),End)),End)))),End)) (of class hkmc2.semantics.Split$Cons) + +{x: 1, y:true} +//│ Type: {x: Int, y: Bool} + +fun k(f) = + a: f(0) + b: f(true) +k +//│ Type: ['eff, 'app, 'eff1, 'app1] -> ((Bool ->{'eff1} 'app1) & (Int ->{'eff} 'app)) ->{'eff | 'eff1} {a: 'app, b: 'app1} + +k(idIB) +//│ Type: {a: Int, b: Bool} + +fun k(f) = (x, y) => + a: f(x) + b: f(y) +k +//│ Type: ['x, 'y, 'eff, 'app, 'eff1, 'app1] -> (('y ->{'eff1} 'app1) & ('x ->{'eff} 'app)) -> (('x, 'y) ->{'eff | 'eff1} {a: 'app, b: 'app1}) + +k(idIB)(true, 1) +//│ Type: {a: Bool, b: Int} + +:e +k(idIB)("true", 1) +//│ ╔══[ERROR] Type error in string literal with expected type 'x +//│ ║ l.198: k(idIB)("true", 1) +//│ ║ ^^^^^^ +//│ ╟── because: cannot constrain Str <: 'x +//│ ╟── because: cannot constrain Str <: 'x +//│ ╟── because: cannot constrain {0: 'x} <: {0: Int} | {0: Bool} +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ Type: {a: ⊥, b: Int} + +(x => x.x + idIB(x.y)) of (x:0, y:1) +//│ Type: Int + +data class Ls[A](prim: [R] -> (() -> R, (A, Ls[A]) -> R) -> R) +fun nil() = new Ls((n, _) => n()) +fun cons(x, y) = new Ls((n, r) => r(x, y)) +//│ Type: ⊤ + +fun map: [A, B, E] -> Ls[out A] -> (A -> B) -> Ls[out B] +//│ Type: ⊤ + +fun map: [A, B, E] -> Ls[A] -> (A -> B) -> Ls[B] +fun map = x => f => x.Ls#prim(() => nil(), (a, b) => cons(f(a), map(b)(f))) +//│ Type: ⊤ + +// fun map = x => f => new Ls((n, r) => x.Ls#prim(n, (a, b) => r(f(a), map(b)(f)))) + +x => map(x)(idIB) +//│ Type: (Ls['A]) ->{⊥} Ls['B] +//│ Where: +//│ 'A#'A ∨ ( 'A#Int ∨ Int <: 'B ∧ ⊥ <: ⊥) ∧ ( 'A#Bool ∨ Bool <: 'B ∧ ⊥ <: ⊥){0: 'A} <: {0: Int} | {0: Bool} + +map(nil())(idIB) +//│ Type: Ls['B] + +map(nil())(idIB) as Ls[Str] +//│ Type: Ls[Str] + +map(cons(1, nil()))(idIB) +//│ Type: Ls['B] +//│ Where: +//│ Int <: 'B + +map(cons(1, cons(true, nil())))(idIB) +//│ Type: Ls['B] +//│ Where: +//│ Bool <: 'B +//│ Int <: 'B + +:e +let x = cons(1, cons(true, nil())) in + map(cons(x, x))(idIB) +//│ ╔══[ERROR] Type error in reference with expected type ('A) ->{⊥} 'B +//│ ║ l.249: 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 ⊤ <: ⊥ +//│ Type: Ls['B] +//│ Where: +//│ Bool <: 'B +//│ Int <: 'B + +fun k: ((Int | Str, Int) -> Int) & ((Bool | Str, Bool) -> Bool) +//│ Type: ⊤ + +k("", if true then 1 else true) +//│ Type: Int + +fun k: ((Int, Int) -> Int) & ((Bool, Bool) -> Bool) +//│ Type: ⊤ + +x => k(x, x) +//│ Type: ('x) ->{'eff} 'app +//│ Where: +//│ 'x#'x ∨ ( 'x#Int ∨ Int <: 'app ∧ ⊥ <: 'eff) ∧ ( 'x#Bool ∨ Bool <: 'app ∧ ⊥ <: 'eff){0: 'x, 1: 'x} <: {0: Int, 1: Int} | {0: Bool, 1: Bool} diff --git a/hkmc2/shared/src/test/mlscript/logicsub/If.mls b/hkmc2/shared/src/test/mlscript/logicsub/If.mls new file mode 100644 index 0000000000..79e97aa16d --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/If.mls @@ -0,0 +1,229 @@ +:bbml +//│ Type: ⊤ + +//│ Type: ⊤ + +fun ib: Int | Bool +fun si: Str | Int +fun sib: Str | Int | Bool +fun rev: Str -> Str +fun not: Bool -> Bool +//│ Type: ⊤ + +fun f(x) = if x is + Int then 0 + Bool then x +f +//│ Type: ['x, 'res, 'eff] -> 'x ->{'eff} 'res +//│ Where: +//│ 'x#Int ∨ Int <: 'res ∧ ⊥ <: 'eff +//│ 'x#Bool ∨ Bool & 'x <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Int & ¬Bool ∨ ⊤ <: ⊥ + +f(ib) as Int | Bool +//│ Type: Int | Bool + +f(f(ib)) as Int | Bool +f(f(ib)) +//│ Type: Int | (Bool & 'x) +//│ Where: +//│ Int <: 'x +//│ Bool <: 'x +//│ 'x#¬Int & ¬Bool ∨ ⊤ <: ⊥ + +:e +f(si) +//│ ╔══[ERROR] Type error in reference with expected type 'x +//│ ║ l.35: f(si) +//│ ║ ^^ +//│ ╟── because: cannot constrain Str | Int <: 'x +//│ ╟── because: cannot constrain Str <: 'x +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ Type: Int + + +// order-dependent (expected) + +fun f(x, y) = if + x is Int then 1 + y is Str then "" +f(1, "") +//│ Type: Int + +f(1, sib) +//│ Type: Int + +fun f(x, y) = if + y is Str then "" + x is Int then 1 +f(1, "") +//│ Type: Str + +f(1, sib) +//│ Type: Int | Str + + +fun foorec(x, y, r) = if + x is Int and y is Int then x + y + x is Str then not(y) + y is Str then r(y, x, r) +//│ Type: ⊤ + +fun foo(x, y) = foorec(x, y, foorec) +//│ Type: ⊤ + +foo(true, "") +foo(1, 2) +foo as (Int, Int) -> Int +foo as (Str, Bool) -> Bool +(x => foo(x, true)) as Str -> Bool +(x => foo(x, "")) as Bool -> Bool +//│ Type: (Bool) ->{⊥} Bool + +:e +foo(1, "") +//│ ╔══[ERROR] Type error in string literal with expected type 'y +//│ ║ l.84: foo(1, "") +//│ ║ ^^ +//│ ╟── because: cannot constrain Str <: 'y +//│ ╟── because: cannot constrain Str <: 'y +//│ ╟── because: cannot constrain 'r <: (Str & 'y1, 'x, 'r) ->{'eff} 'app +//│ ╟── because: cannot constrain 'r <: ¬(¬{(Str & 'y1, 'x, 'r) ->{'eff} 'app}) +//│ ╟── because: cannot constrain ((¬⊥ & 'x1, ¬⊥ & 'y2, ¬⊥ & 'r1) ->{¬⊥ & 'eff1} (¬⊥ & 'res)) & ¬⊥ <: ¬(¬{(Str & 'y1, 'x, 'r) ->{'eff} 'app}) +//│ ╟── because: cannot constrain {0: Str & 'y1, 1: 'x, 2: 'r} <: {0: 'x1, 1: 'y2, 2: 'r1} +//│ ╟── because: cannot constrain 'x <: 'y2 +//│ ╟── because: cannot constrain 'x <: 'y2 +//│ ╟── because: cannot constrain 'x <: ¬(¬{Bool}) +//│ ╟── because: cannot constrain 'x <: ¬(¬{Bool}) +//│ ╟── because: cannot constrain ¬{Str} ∧ 'x2 <: ¬(¬{Bool}) +//│ ╟── because: cannot constrain 'x2 <: ¬(¬{Str | Bool}) +//│ ╟── because: cannot constrain ¬⊥ & 'x3 <: ¬(¬{Str | Bool}) +//│ ╟── because: cannot constrain 'x3 <: ¬(¬{Str | Bool}) +//│ ╙── because: cannot constrain Int <: ¬(¬{Str | Bool}) +//│ Type: Bool + +fun increv(x) = if x is + Int then x + 1 + else + rev(x) +increv +//│ Type: ['x, 'res, 'eff, 'x1] -> 'x ->{'eff} 'res +//│ Where: +//│ 'x#Int ∨ Int & 'x <: Int ∧ Int <: Int ∧ Int <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Int ∨ ¬Int & 'x <: 'x1 ∧ 'x1 <: Str ∧ Str <: 'res ∧ ⊥ <: 'eff + +fun increv'(x) = if x is + Int then x + 1 + Str then rev(x) +increv' +//│ Type: ['x, 'res, 'eff] -> 'x ->{'eff} 'res +//│ Where: +//│ 'x#Int ∨ Int & 'x <: Int ∧ Int <: Int ∧ Int <: 'res ∧ ⊥ <: 'eff +//│ 'x#Str ∨ Str & 'x <: Str ∧ Str <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Str & ¬Int ∨ ⊤ <: ⊥ + +:e +increv(sib) +//│ ╔══[ERROR] Type error in reference with expected type 'x +//│ ║ l.126: increv(sib) +//│ ║ ^^^ +//│ ╟── because: cannot constrain (Str | Int) | Bool <: 'x +//│ ╟── because: cannot constrain Bool <: 'x +//│ ╙── because: cannot constrain Bool <: ¬(¬{Str | Int}) +//│ Type: Int | Str + +:e +increv'(sib) +//│ ╔══[ERROR] Type error in reference with expected type 'x +//│ ║ l.136: increv'(sib) +//│ ║ ^^^ +//│ ╟── because: cannot constrain (Str | Int) | Bool <: 'x +//│ ╟── because: cannot constrain Bool <: 'x +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ Type: Int | Str + +increv(si) +//│ Type: Int | Str + +increv'(si) +//│ Type: Int | Str + +fun f(x, y) = if + x is Int and y is Int then 1 + x is Bool then y +//│ Type: ⊤ + +// literal matching not yet implemented + +:todo +x => if x is + true then 0 + false then 0 +//│ Type: (Bool) ->{⊥} Int + +fun f(x) = if + x is Int then x + 2 + x is Str then rev(x) + else + not(x) +f +//│ Type: ['x, 'res, 'eff, 'x1] -> 'x ->{'eff} 'res +//│ Where: +//│ 'x#Int ∨ Int & 'x <: Int ∧ Int <: Int ∧ Int <: 'res ∧ ⊥ <: 'eff +//│ 'x#Str ∨ Str & 'x <: Str ∧ Str <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Str & ¬Int ∨ (¬Int & ¬Str) & 'x <: 'x1 ∧ 'x1 <: Bool ∧ Bool <: 'res ∧ ⊥ <: 'eff + +f(sib) +//│ Type: (Bool | Int) | Str + +fun f(x, y) = if + x is Int then y + y is Str then 1 + x is Str then y + 1 + else + not(x) +f +//│ Type: ['x, 'y, 'res, 'eff, 'x1, 'y1, 'y2, 'x2] -> ('x, 'y) ->{'eff} 'res +//│ Where: +//│ 'x#Int ∨ 'y <: 'res ∧ ⊥ <: 'eff +//│ 'y#Str ∨ 'x#¬Int ∨ ¬Int & 'x <: 'x1 ∧ Int <: 'res ∧ ⊥ <: 'eff +//│ 'x#Str ∨ 'y#¬Str ∨ ¬Str & 'y <: 'y1 ∧ 'y1 <: Int ∧ Int <: Int ∧ Int <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Str & ¬Int ∨ 'y#¬Str ∨ ¬Str & 'y <: 'y2 ∧ (¬Int & ¬Str) & 'x <: 'x2 ∧ 'x2 <: Bool ∧ Bool <: 'res ∧ ⊥ <: 'eff + +f(ib, sib) +//│ Type: (((Bool | Int) | Bool) | Int) | Str + +:ns +f(ib, ib) +//│ Type: 'res +//│ Where: +//│ Bool <: 'y +//│ Int <: 'y +//│ 'y#Str ∨ ¬Int & 'x <: 'x1 ∧ Int <: 'res ∧ ⊥ <: 'eff +//│ Bool <: 'x +//│ Int <: 'x +//│ 'x <: ¬(¬{(Str | Int) | Bool}) +//│ 'x#Str ∨ ¬Str & 'y <: 'y1 ∧ 'y1 <: Int ∧ Int <: Int ∧ Int <: 'res ∧ ⊥ <: 'eff +//│ 'eff <: ¬() +//│ Bool <: 'res +//│ 'y <: 'res + +:todo +f(ib, ib) +//│ Type: Bool | 'res +//│ Where: +//│ Bool <: 'res +//│ 'res <: 'res + +fun f(x, y) = if + x is Int then 1 + y is Int then not(x) +f +//│ Type: ['x, 'y, 'res, 'eff, 'x1] -> ('x, 'y) ->{'eff} 'res +//│ Where: +//│ 'x#Int ∨ Int <: 'res ∧ ⊥ <: 'eff +//│ 'y#Int ∨ 'x#¬Int ∨ ¬Int & 'x <: 'x1 ∧ 'x1 <: Bool ∧ Bool <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Int ∨ 'y#¬Int ∨ ⊤ <: ⊥ + +f(ib, 1) +//│ Type: Bool | Int diff --git a/hkmc2/shared/src/test/mlscript/logicsub/List.mls b/hkmc2/shared/src/test/mlscript/logicsub/List.mls new file mode 100644 index 0000000000..d84f721c61 --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/List.mls @@ -0,0 +1,126 @@ +:bbml +//│ Type: ⊤ + +//│ Type: ⊤ +class + Nil() + Cons[A, Tl](val hd: A, val tl: Tl) +//│ Type: ⊤ + +let nil = new Nil() +//│ Type: ⊤ + +let cons(hd, tl) = new Cons(hd, tl) +//│ Type: ⊤ + +cons(0, 0) +//│ Type: Cons['A, 'Tl] +//│ Where: +//│ Int <: 'A +//│ Int <: 'Tl + +cons +//│ Type: (⊤, ⊤) ->{⊥} Cons['A, 'Tl] +//│ Where: +//│ Int <: 'A +//│ Int <: 'Tl + +fun cons(hd, tl) = new Cons(hd, tl) +//│ Type: ⊤ + +fun map(xs, f) = + if xs is + Nil then nil + Cons then new Cons(f(xs.Cons#hd), map(xs.Cons#tl, f)) +//│ Type: ⊤ + +nil map(x => x) +//│ Type: Nil + +let c = cons(1, nil) +c map(x => x) +//│ Type: Nil | Cons['A, 'Tl] +//│ Where: +//│ Int <: 'A +//│ Nil <: 'res +//│ Cons['A, 'Tl] <: 'res +//│ 'res <: 'Tl + +:e +cons(1, 2) map(x => x) +//│ ╔══[ERROR] Type error in function literal with expected type 'f +//│ ║ l.50: cons(1, 2) map(x => x) +//│ ║ ^^^^^^ +//│ ╟── because: cannot constrain 'x -> 'x <: 'f +//│ ╟── because: cannot constrain ('x) ->{⊥} ('x) <: 'f +//│ ╟── because: cannot constrain {0: 'Tl, 1: 'f} <: {0: 'xs, 1: 'f} +//│ ╟── because: cannot constrain 'Tl <: 'xs +//│ ╟── because: cannot constrain 'Tl <: ¬(¬'xs) +//│ ╟── because: cannot constrain Int <: ¬(¬'xs) +//│ ╟── because: cannot constrain Int <: 'xs +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ Type: Cons['A, 'Tl1] +//│ Where: +//│ Int <: 'A +//│ Cons['A, 'Tl1] <: 'res +//│ 'res <: 'Tl1 + +cons(1, cons("", nil)) map(x => cons(x, true)) +//│ Type: Nil | Cons['A, 'Tl] +//│ Where: +//│ Str | Int <: 'A1 +//│ Bool <: 'Tl1 +//│ Cons['A1, 'Tl1] <: 'A +//│ Nil <: 'res +//│ Cons['A, 'Tl] <: 'res +//│ 'res <: 'Tl + + +fun maprec(xs, f, r) = + if xs is + Nil then nil + Cons then new Cons(f(xs.Cons#hd), r(xs.Cons#tl, f, r)) +fun map(xs, f) = maprec(xs, f, maprec) +//│ Type: ⊤ + + +nil map(x => x) +//│ Type: Nil + +let c = cons(1, nil) +c map(x => x) +//│ Type: Cons['A, 'Tl] +//│ Where: +//│ Int <: 'A +//│ Nil <: 'Tl + +:e +cons(1, 2) map(x => x) +//│ ╔══[ERROR] Type error in function literal with expected type 'f +//│ ║ l.98: cons(1, 2) map(x => x) +//│ ║ ^^^^^^ +//│ ╟── because: cannot constrain 'x -> 'x <: 'f +//│ ╟── because: cannot constrain ('x) ->{⊥} ('x) <: 'f +//│ ╟── because: cannot constrain {0: 'Tl, 1: 'f1, 2: 'r} <: {0: 'xs, 1: 'f2, 2: 'r1} +//│ ╟── because: cannot constrain 'Tl <: 'xs +//│ ╟── because: cannot constrain 'Tl <: 'xs +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ Type: Cons['A, 'Tl1] +//│ Where: +//│ Int <: 'A + +let c = cons(nil, nil) +c map(x => x map(x => (a: x))) +//│ Type: Cons['A, 'Tl] +//│ Where: +//│ Nil <: 'A +//│ Nil <: 'Tl + +let c = cons(cons(nil, nil), nil) +c map(x => x map(x => (a: x))) +//│ Type: Cons['A, 'Tl] +//│ Where: +//│ {a: Nil} <: 'A1 +//│ Nil <: 'Tl1 +//│ Cons['A1, 'Tl1] <: 'A +//│ Nil <: 'Tl diff --git a/hkmc2/shared/src/test/mlscript/logicsub/MarlowWadler97.mls b/hkmc2/shared/src/test/mlscript/logicsub/MarlowWadler97.mls new file mode 100644 index 0000000000..febceb3a75 --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/MarlowWadler97.mls @@ -0,0 +1,106 @@ +:bbml +//│ Type: ⊤ +:js + +//│ Type: ⊤ + + +// * Sec. 9 of A Practical Subtyping System For Erlang +// * (https://homepages.inf.ed.ac.uk/wadler/papers/erlang/erlang.pdf) + + +class + Tru() + Fls() +//│ Type: ⊤ + +let + tru = new Tru() + fls = new Fls() +//│ fls = Fls() +//│ tru = Tru() +//│ Type: ⊤ + +// :ucs desugared +:ucs normalized +fun test(x, y) = if + x is Tru and y is Tru then tru + x is Tru and y is Tru then tru + x is Tru and y is Tru then tru + x is Fls then fls + y is Fls then fls +test +//│ Normalized: +//│ > if +//│ > x is Tru and +//│ > y is Tru then tru#666 +//│ > y is Fls then fls#666 +//│ > x is Fls then fls#666 +//│ > y is Fls then fls#666 +//│ = [function test] +//│ Type: ['x, 'y, 'res, 'eff, 'y1, 'x1] -> ('x, 'y) ->{'eff} 'res +//│ Where: +//│ 'x#Tru ∨ 'y#Tru ∨ Tru <: 'res ∧ ⊥ <: 'eff +//│ 'x#Fls ∨ 'y#¬Tru ∨ ¬Tru & 'y <: 'y1 ∧ Fls <: 'res ∧ ⊥ <: 'eff +//│ 'x#Fls ∨ 'y <: 'y1 ∧ Fls <: 'res ∧ ⊥ <: 'eff +//│ 'y#Fls ∨ 'x#¬Fls & ¬Tru ∨ (¬Tru & ¬Fls) & 'x <: 'x1 ∧ Fls <: 'res ∧ ⊥ <: 'eff +//│ 'y#Fls ∨ 'x#¬Fls ∨ ¬Fls & 'x <: 'x1 ∧ Fls <: 'res ∧ ⊥ <: 'eff +//│ 'x#¬Fls & ¬Tru ∨ 'y#¬Fls ∨ ⊤ <: ⊥ +//│ 'y#¬Fls & ¬Tru ∨ 'x#¬Fls ∨ ⊤ <: ⊥ + +test(tru, tru) +//│ = Tru() +//│ Type: Tru + +test(tru, fls) +//│ = Fls() +//│ Type: Fls + +test(fls, tru) +//│ = Fls() +//│ Type: Fls + +test(fls, fls) +//│ = Fls() +//│ Type: Fls + +test("hi", fls) +//│ = Fls() +//│ Type: Fls + + +:todo +:e +test(true, false) +//│ ═══[RUNTIME ERROR] Error: match error +//│ ╔══[ERROR] Type error in boolean literal with expected type 'y +//│ ╟── because: cannot constrain Bool <: 'y +//│ ╟── because: cannot constrain Bool <: 'y +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ ╔══[ERROR] Type error in boolean literal with expected type 'y +//│ ╟── because: cannot constrain Bool <: 'y +//│ ╟── because: cannot constrain Bool <: 'y +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ Type: ⊥ + + +// * Note: this version generates a large type + +fun test(x, y) = if + x is Tru and y is Tru then tru + x is Fls and y is Tru then fls + y is Fls then fls +// test +//│ Type: ⊤ + +// * Note: and this one even larger + +fun test(x, y) = if + x is Tru and y is Tru then tru + x is Fls and y is Tru then fls + y is Fls then fls + y is Fls then fls +// test +//│ Type: ⊤ + + diff --git a/hkmc2/shared/src/test/mlscript/logicsub/Records.mls b/hkmc2/shared/src/test/mlscript/logicsub/Records.mls new file mode 100644 index 0000000000..c03e36d222 --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/Records.mls @@ -0,0 +1,84 @@ +:bbml +//│ Type: ⊤ + +//│ Type: ⊤ + +{} +//│ Type: ⊤ + +let r = {} +//│ Type: ⊤ + +{1} +//│ Type: Int + +{1, 2} +//│ Type: Int + +{foo: 1} +//│ Type: {foo: Int} + +let rcd = { foo: 1, bar: "..." } +//│ Type: ⊤ + +:todo +[rcd.foo, rcd.bar] +//│ ╔══[ERROR] Term shape not yet supported by BbML: Tup(List(Fld(‹›,Sel(Ref(rcd),Ident(foo)),None), Fld(‹›,Sel(Ref(rcd),Ident(bar)),None))) +//│ ║ l.25: [rcd.foo, rcd.bar] +//│ ╙── ^^^^^^^^^^^^^^^^^^ +//│ Type: ⊥ + +// TODO: IntLit as label? +"0": rcd.foo +"1": rcd.bar +//│ Type: {0: Int, 1: Str} + +fun id(x) = x +//│ Type: ⊤ + +id of (x: 1) +//│ Type: {x: Int} + +:todo +id of { x: 1 } +//│ Type: Str + +id of ({ x: 1 }) +//│ Type: {x: Int} + +id of ({ x: 1, y: 2 }) +//│ Type: {x: Int, y: Int} + +id of (x: 1, y: 2) +//│ Type: {x: Int, y: Int} + +// * FIXME: handling of record arguments in resolver/checker +:fixme +id of { x: 1, y: 2 } +//│ ╔══[ERROR] Incorrect number of arguments +//│ ║ l.57: id of { x: 1, y: 2 } +//│ ╙── ^^^^^^^^^^^^^^^^^^ +//│ Type: ⊥ + +:todo +fun f(x) = + x: x.a + y: x.b +f of (a: 1, b: true) +//│ ╔══[ERROR] Type error in record with expected type 'x +//│ ║ l.67: f of (a: 1, b: true) +//│ ║ ^^^^^^^ +//│ ╟── because: cannot constrain {a: Int, b: Bool} <: 'x +//│ ╟── because: cannot constrain {a: Int, b: Bool} <: 'x +//│ ╟── because: cannot constrain {a: Int, b: Bool} <: ¬¬{a: 'sel} +//│ ╟── because: cannot constrain Int <: 'sel +//│ ╟── because: cannot constrain Int <: 'sel +//│ ╙── because: cannot constrain Int <: ¬¬{b: 'sel1} +//│ Type: {x: Int, y: ⊥} + +x: 1 +y: x +//│ Type: {x: Int, y: Int} + +(x => (x: 1, y: x))("") +//│ Type: {x: Int, y: Int} diff --git a/hkmc2/shared/src/test/mlscript/logicsub/elixir.mls b/hkmc2/shared/src/test/mlscript/logicsub/elixir.mls new file mode 100644 index 0000000000..8cd54de5fd --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/elixir.mls @@ -0,0 +1,152 @@ +:bbml +//│ Type: ⊤ + +//│ Type: ⊤ +// The Design Principles of the Elixir Type System +// https://www.irif.fr/~gc/papers/elixir-type-design.pdf + +class + Nil() + Cons[A, B](val car: A, val cdr: B) + Tru() + Fls() +//│ Type: ⊤ + +let tru = new Tru +let fls = new Fls +fun not: Tru | Fls -> Tru | Fls +fun not(x) = if x is + Tru then fls + Fls then tru +fun car(x) = x.Cons#car +fun cdr(x) = x.Cons#cdr +//│ Type: ⊤ + + + +fun negate: Int -> Int +fun negate(x) = if x is + Int then 0 - x +//│ Type: ⊤ + +fun subtract: (Int, Int) -> Int +fun subtract(a, b) = if + a is Int and b is Int then a + negate(b) +//│ Type: ⊤ + +fun negate: Int | Tru | Fls -> Int | Tru | Fls +fun negate(x) = if x is + Int then 0 - x + Tru then not(x) + Fls then not(x) +//│ Type: ⊤ + +:e +fun subtract: (Int, Int) -> Int +fun subtract(a, b) = if + a is Int and b is Int then a + negate(b) +//│ ╔══[ERROR] Type error in `if` expression with expected type Int +//│ ║ l.47: a is Int and b is Int then a + negate(b) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╙── because: cannot constrain (Int | Tru) | Fls <: Int +//│ ╔══[ERROR] Type error in `if` expression with expected type Int +//│ ║ l.47: a is Int and b is Int then a + negate(b) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╙── because: cannot constrain (Int | Tru) | Fls <: Int +//│ Type: ⊤ + +fun negate: (Int -> Int) & (Tru | Fls -> Tru | Fls) +fun negate(x) = if x is + Int then 0 - x + Tru then not(x) + Fls then not(x) +//│ Type: ⊤ + +fun subtract: (Int, Int) -> Int +fun subtract(a, b) = if + a is Int and b is Int then a + negate(b) +//│ Type: ⊤ + +// fun negate: (Fls | Nil -> Tru) & (~(Fls | Nil) -> Fls) + + + +// type t = [a: Int | Str, b: Tru | Fls] +// type s = [a: Int, b: Tru | Fls] | [a: Str, b: Tru | Fls] +// s = t +// fun apply: (t -> t, s) -> s +fun apply: (([a: Int | Str, b: Tru | Fls]) -> [a: Int | Str, b: Tru | Fls], [a: Int, b: Tru | Fls] | [a: Str, b: Tru | Fls]) -> + [a: Int, b: Tru | Fls] | [a: Str, b: Tru | Fls] +fun apply(f, x) = f(x) +//│ Type: ⊤ + + + +data class Ls[A](prim: [R] -> (() -> R, (A, Ls[A]) -> R) -> R) +fun nil() = new Ls((n, _) => n()) +fun cons(p, q) = new Ls((n, r) => r(p, q)) +fun from(x) = x.Ls#prim(() => new Nil, (x, y) => new Cons(x, from(y))) +//│ Type: ⊤ + +fun _in(x) = if x is + Nil then nil() + Cons then cons(car(x), cdr(x)) +fun _out(x) = x.Ls#prim(() => new Nil, (x, y) => new Cons(x, y)) +//│ Type: ⊤ + +fun map: [A, B] -> (Ls[A], A -> B) -> Ls[B] +fun map(xs, f) = + let x = _out(xs) + if x is + Cons then cons(f(car(x)), map(cdr(x), f)) + Nil then nil() +//│ Type: ⊤ + +fun reduce: [A, B] -> (Ls[A], B, (A, B) -> B) -> B +fun reduce(xs, acc, f) = + let x = _out(xs) + if x is + Cons then reduce(cdr(x), f(car(x), acc), f) + Nil then acc +//│ Type: ⊤ + +let xs = cons(1, cons(4, nil())) +//│ Type: ⊤ + +xs map(negate) +//│ Type: Ls['B] +//│ Where: +//│ Int <: 'B + +fun map(xs, f) = if xs is + Cons then cons(f(car(xs)), map(_out(cdr(xs)), f)) + Nil then nil() +//│ Type: ⊤ + +fun reduce: [A, B] -> ((Cons[A, Ls[A]], B, (A, B) -> B) -> B) & ((Nil, B, Any) -> B) +fun reduce(xs, acc, f) = if xs is + Cons then reduce(_out(cdr(xs)), f(car(xs), acc), f) + Nil then acc +//│ Type: ⊤ + +reduce(new Nil, 1, "function") +//│ Type: Int + +let xs = cons(1, cons(4, nil())) +//│ Type: ⊤ + +xs _out() map(negate) +//│ Type: Ls['A] | Ls['A1] +//│ Where: +//│ Int <: 'A1 +//│ 'A1 <: 'A +//│ 'A <: 'A1 + +fun negate: (Int -> Int) & (Bool -> Bool) & (~(Int | Bool) -> ~(Int | Bool)) +fun negate(x) = if x is + Int then 0 - x + Tru then not(x) + Fls then not(x) + else + x +//│ Type: ⊤ diff --git a/hkmc2/shared/src/test/mlscript/logicsub/popl22.mls b/hkmc2/shared/src/test/mlscript/logicsub/popl22.mls new file mode 100644 index 0000000000..b546acb5e7 --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/popl22.mls @@ -0,0 +1,544 @@ +:bbml +//│ Type: ⊤ + +//│ Type: ⊤ + +// On Type-Cases, Union Elimination, and Occurrence Typing +// https://www.irif.fr/~gc/papers/popl22.pdf + +// Occurence typing uses type test to refine the type of the term + +fun f(x) = if x is + Int then x + 1 // x: Int + else x.a // x: ~Int +//│ Type: ⊤ + +// Union elimination rule and set-theoretic types can capture occurence typing +// and the refinement can occur in any position +// instead of only by type test + +fun f(x1, x2) = if + x1(x2) is Int then x2 + 1 + else + x1(x2).Str#concat(x2) +//│ Type: ⊤ + +fun id: (Int -> Int) & (Str -> Str) +//│ Type: ⊤ + +f(id, 1) +//│ Type: Int + +f(id, "") +//│ Type: Str + +fun strint: Int | Str +//│ Type: ⊤ + +// Considering x2: Int | Str, the type is splitted to Int, and Str in two branches +// thus type check the following expression + +:e +f(id, strint) +//│ ╔══[ERROR] Type error in reference with expected type 'x2 +//│ ║ l.42: f(id, strint) +//│ ║ ^^^^^^ +//│ ╟── because: cannot constrain Int | Str <: 'x2 +//│ ╟── because: cannot constrain Str <: 'x2 +//│ ╙── because: cannot constrain Str <: ¬(¬{Int}) +//│ ╔══[ERROR] Type error in reference with expected type 'x2 +//│ ║ l.42: f(id, strint) +//│ ║ ^^^^^^ +//│ ╟── because: cannot constrain Int | Str <: 'x2 +//│ ╟── because: cannot constrain Str <: 'x2 +//│ ╟── because: cannot constrain Str <: 'app +//│ ╟── because: cannot constrain Str <: 'app +//│ ╟── because: cannot constrain 'app1 <: Str +//│ ╟── because: cannot constrain 'app1 <: ¬(¬{Str}) +//│ ╙── because: cannot constrain Int <: ¬(¬{Str}) +//│ ╔══[ERROR] Type error in reference with expected type 'x2 +//│ ║ l.42: f(id, strint) +//│ ║ ^^^^^^ +//│ ╟── because: cannot constrain Int | Str <: 'x2 +//│ ╟── because: cannot constrain Str <: 'x2 +//│ ╟── because: cannot constrain Str <: 'app +//│ ╟── because: cannot constrain Str <: 'app +//│ ╟── because: cannot constrain 'x2 <: Str +//│ ╟── because: cannot constrain 'x2 <: ¬(¬{Str}) +//│ ╙── because: cannot constrain Int <: ¬(¬{Str}) +//│ Type: Str | Int + +// without union elimination rule, type test on x2 is required + +fun f(x1, x2) = if x2 is + Int then x2 + 1 + else + x1(x2).Str#concat(x2) +//│ Type: ⊤ + +f(id, strint) +//│ Type: Str | Int + +data class Prod[A, B](val fst: A, val snd: B) +//│ Type: ⊤ + +class + Tru() + Fls() + Z() +//│ Type: ⊤ + +let tru = new Tru() +let fls = new Fls() +fun prod(p, q) = new Prod(p, q) +//│ Type: ⊤ + +// Maximal Sharing Canonical Forms is used in type checking + +fun y: Any -> Tru | Fls +//│ Type: ⊤ + +:e +{ fst: y(x => x), snd: y(x => x) } as [ fst: Tru, snd: Tru ] | [ fst: Fls, snd: Fls ] +//│ ╔══[ERROR] Type error in record with expected type {fst: Tru, snd: Tru} | {fst: Fls, snd: Fls} +//│ ║ l.102: { fst: y(x => x), snd: y(x => x) } as [ fst: Tru, snd: Tru ] | [ fst: Fls, snd: Fls ] +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain {fst: Tru | Fls, snd: Tru | Fls} <: {fst: Tru, snd: Tru} | {fst: Fls, snd: Fls} +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ Type: {fst: Tru, snd: Tru} | {fst: Fls, snd: Fls} + +// The above expression is typed with the following MSC-forms + +( + let a1 = y + let a2 = x => x + let a3 = a1(a2) + let a4 = { fst: a3, snd: a3 } + a4 +) +//│ Type: {fst: Tru | Fls, snd: Tru | Fls} + +// Again, type test on a3 is required + +( + let a1 = y + let a2 = x => x + let a3 = a1(a2) + let a4 = if a3 is Tru then { fst: a3, snd: a3 } else { fst: a3, snd: a3 } + a4 +) as [ fst: Tru, snd: Tru ] | [ fst: Fls, snd: Fls ] +//│ Type: {fst: Tru, snd: Tru} | {fst: Fls, snd: Fls} + + +// Since classes are merged in union, the following term type checks + +prod(y(x => x), y(x => x)) as Prod[Tru, Tru] | Prod[Fls, Fls] +//│ Type: Prod[Tru, Tru] | Prod[Fls, Fls] + +prod(y(x => x), y(x => x)) +//│ Type: Prod['A, 'B] +//│ Where: +//│ Fls | Tru <: 'A +//│ Fls | Tru <: 'B + + +fun a: (Int -> (Int | Bool)) | Prod[Int, Int | Bool] +fun n: Int +//│ Type: ⊤ + +// type test `a(n) is Int` does not refine a and n, and thus a(n) + +fun f(a, n) = if + a is Prod and + a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd + else a.Prod#snd + a(n) is Int then a(n) < 42 + else a(n) +//│ Type: ⊤ + +// while a(n) is Int, in the then branch, a(n) still has type Int | Bool + +:e +f(a, n) +//│ ╔══[ERROR] Type error in reference with expected type 'n +//│ ║ l.162: f(a, n) +//│ ║ ^ +//│ ╟── because: cannot constrain Int <: 'n +//│ ╟── because: cannot constrain Int <: 'n +//│ ╟── because: cannot constrain Int ∨ Bool <: 'app +//│ ╟── because: cannot constrain Int <: 'app +//│ ╟── because: cannot constrain 'app1 <: Int +//│ ╟── because: cannot constrain 'app1 <: ¬(¬{Int}) +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ Type: ((((Int | Bool) | Bool) | Int) | Bool) | Bool + +// the following rewrite refines x + +fun f(a, n) = if + a is Prod and + a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd + else a.Prod#snd + let x = a(n) + x is Int then x < 42 + else x +//│ Type: ⊤ + +f(a, n) +//│ Type: (((((Int & ¬Int) | (Bool & ¬Int)) | Bool) | Int) | Bool) | Bool + + + +fun is_int(x) = + if x is Int then tru else fls +//│ Type: ⊤ + +is_int as Int -> Tru +is_int as ~Int -> Fls +//│ Type: (¬Int) ->{⊥} Fls + +fun is_bool(x) = if x is + Tru then tru + Fls then tru + else fls +//│ Type: ⊤ + +is_bool as Tru | Fls -> Tru +is_bool as ~(Tru | Fls) -> Fls +//│ Type: (¬Tru & ¬Fls) ->{⊥} Fls + +// Originally, the paper defines False, empty string "" and zero 0 as Falsy +// and ~Falsy as Truthy +// Here Fls and Z are treated as falsy, and otherwise truthy + +fun not_(x) = if x is + Fls then tru + Z then tru + else fls +//│ Type: ⊤ + +not_ as Fls | Z -> Tru +not_ as ~(Fls | Z) -> Fls +//│ Type: (¬Fls & ¬Z) ->{⊥} Fls + +fun to_bool(x) = x not_() not_() +//│ Type: ⊤ + +to_bool as Fls | Z -> Fls +to_bool as ~(Fls | Z) -> Tru +//│ Type: (¬Fls & ¬Z) ->{⊥} Tru + +fun and_(x, y) = if x is + Fls then fls + Z then fls + else to_bool(y) +//│ Type: ⊤ + +and_ as (Fls | Z, Any) -> Fls +and_ as (~(Fls | Z), ~(Fls | Z)) -> Tru +and_ as (~(Fls | Z), Fls | Z) -> Fls +//│ Type: (¬Fls & ¬Z, Fls | Z) ->{⊥} Fls + + +fun or_(x, y) = not_(x) and_(not_(y)) not_() +//│ Type: ⊤ + +or_ as (~(Fls | Z), Any) -> Tru +or_ as (Fls | Z, ~(Fls | Z)) -> Tru +or_ as (Fls | Z, Fls | Z) -> Fls +//│ Type: (Fls | Z, Fls | Z) ->{⊥} Fls + +fun strlen: Str -> Int +fun plus: (Int | Z, Int | Z) -> Int | Z +//│ Type: ⊤ + +fun example14(input, extra) = if + input is_int() and_(extra.fst is_int()) is Tru then input + extra.fst + extra.fst is_int() is Tru then input strlen() + extra.fst + else new Z() +//│ Type: ⊤ + +example14 as (Int | Str, [fst: ~Int, snd: Any]) -> Z +example14 as (~(Int | Str), [fst: ~Int, snd: Any]) -> Z +//│ Type: (¬Int & ¬Str, {fst: ¬Int, snd: ⊤}) ->{⊥} Z + +:e +example14 as (Int | Str, [fst: Int, snd: Any]) -> Int +//│ ╔══[ERROR] Type error in reference with expected type (Int | Str, {fst: Int, snd: ⊤}) ->{⊥} Int +//│ ║ l.265: example14 as (Int | Str, [fst: Int, snd: Any]) -> Int +//│ ║ ^^^^^^^^^ +//│ ╟── because: cannot constrain ('input, 'extra) ->{'eff} 'res <: (Int | Str, {fst: Int, snd: ⊤}) -> Int +//│ ╟── because: cannot constrain {0: Int | Str, 1: {fst: Int, snd: ⊤}} <: {0: 'input, 1: 'extra} +//│ ╟── because: cannot constrain {fst: Int, snd: } <: 'extra +//│ ╟── because: cannot constrain {fst: Int, snd: } <: 'extra +//│ ╟── because: cannot constrain {fst: Int, snd: } <: ¬(¬{{fst: 'sel}}) +//│ ╟── because: cannot constrain Int <: 'sel +//│ ╟── because: cannot constrain Int <: 'sel +//│ ╟── because: cannot constrain Int <: ¬(¬'x) +//│ ╟── because: cannot constrain Int <: 'x +//│ ╟── because: cannot constrain Tru <: 'res1 +//│ ╟── because: cannot constrain Tru <: 'res1 +//│ ╟── because: cannot constrain 'input <: Str +//│ ╟── because: cannot constrain 'input <: ¬(¬{Str}) +//│ ╙── because: cannot constrain Int <: ¬(¬{Str}) +//│ ╔══[ERROR] Type error in reference with expected type (Int | Str, {fst: Int, snd: ⊤}) ->{⊥} Int +//│ ║ l.265: example14 as (Int | Str, [fst: Int, snd: Any]) -> Int +//│ ║ ^^^^^^^^^ +//│ ╟── because: cannot constrain ('input, 'extra) ->{'eff} 'res <: (Int | Str, {fst: Int, snd: ⊤}) -> Int +//│ ╟── because: cannot constrain {0: Int | Str, 1: {fst: Int, snd: ⊤}} <: {0: 'input, 1: 'extra} +//│ ╟── because: cannot constrain {fst: Int, snd: } <: 'extra +//│ ╟── because: cannot constrain {fst: Int, snd: } <: 'extra +//│ ╟── because: cannot constrain {fst: Int, snd: } <: ¬¬{fst: 'sel1} +//│ ╟── because: cannot constrain Int <: 'sel1 +//│ ╟── because: cannot constrain Int <: 'sel1 +//│ ╟── because: cannot constrain Int <: ¬(¬⊥ & ¬'x1) +//│ ╟── because: cannot constrain Int <: 'x1 +//│ ╟── because: cannot constrain Tru <: 'res2 +//│ ╟── because: cannot constrain Tru <: 'res2 +//│ ╟── because: cannot constrain Tru <: ¬(¬⊥ & ¬'y) +//│ ╟── because: cannot constrain Tru <: 'y +//│ ╟── because: cannot constrain Fls <: 'res3 +//│ ╟── because: cannot constrain Fls <: 'res3 +//│ ╟── because: cannot constrain Fls <: ¬(¬⊥ & ¬'x2) +//│ ╟── because: cannot constrain Fls <: 'x2 +//│ ╟── because: cannot constrain Tru <: 'res4 +//│ ╟── because: cannot constrain Tru <: 'res4 +//│ ╟── because: cannot constrain Tru <: ¬(¬'res5) +//│ ╟── because: cannot constrain Tru <: 'res5 +//│ ╟── because: cannot constrain 'input <: Int +//│ ╟── because: cannot constrain 'input <: ¬(¬{Int}) +//│ ╙── because: cannot constrain Str <: ¬(¬{Int}) +//│ Type: (Int | Str, {fst: Int, snd: ⊤}) ->{⊥} Int + +// using direct type test instead of predicate functions + +fun example14_(input, extra) = if + input is Int and extra.fst is Int then input + extra.fst + extra.fst is Int then input strlen() + extra.fst + else new Z() +//│ Type: ⊤ + +example14_ as (Int | Str, [fst: ~Int, snd: Any]) -> Z +example14_ as (Int | Str, [fst: Int, snd: Any]) -> Int +example14_ as (~(Int | Str), [fst: ~Int, snd: Any]) -> Z +//│ Type: (¬Int & ¬Str, {fst: ¬Int, snd: ⊤}) ->{⊥} Z + +fun is_string: (Str -> Tru) & (~Str -> Fls) +//│ Type: ⊤ + +// example6_wrong is ill typed + +:e +fun example6_wrong(x: Int | Str, y: Any) = if + x is_int() and_(y is_string()) is Tru then x + strlen(y) + else strlen(x) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.332: x is_int() and_(y is_string()) is Tru then x + strlen(y) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.333: else strlen(x) +//│ ║ ^^^^^^^^^^^^^^^^ +//│ ╙── because: cannot constrain Int | Str <: Int +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.332: x is_int() and_(y is_string()) is Tru then x + strlen(y) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.333: else strlen(x) +//│ ║ ^^^^^^^^^^^^^^^^ +//│ ╙── because: cannot constrain ⊤ <: Str +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.332: x is_int() and_(y is_string()) is Tru then x + strlen(y) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.333: else strlen(x) +//│ ║ ^^^^^^^^^^^^^^^^ +//│ ╙── because: cannot constrain Int | Str <: Str +//│ Type: ⊤ + +:e +fun example6_wrong(x: Int | Str, y: Any) = if + x is Int and y is Str then x + strlen(y) + else strlen(x) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.356: x is Int and y is Str then x + strlen(y) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.357: else strlen(x) +//│ ║ ^^^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain Int | Str <: 'x +//│ ╟── because: cannot constrain Int <: 'x +//│ ╙── because: cannot constrain Int <: ¬(¬{Str}) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.356: x is Int and y is Str then x + strlen(y) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.357: else strlen(x) +//│ ║ ^^^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'x <: Str +//│ ╟── because: cannot constrain 'x <: ¬(¬{Str}) +//│ ╙── because: cannot constrain Int <: ¬(¬{Str}) +//│ Type: ⊤ + +fun example6_ok(x, y) = if + x is_int() and_(y is_string()) is Tru then x + strlen(y) + else strlen(x) +//│ Type: ⊤ + +example6_ok as (Str, Any) -> Int +example6_ok as (Int, Str) -> Int +//│ Type: (Int, Str) ->{⊥} Int + +// the same as above + +:e +fun detailed_ex(a: (Int -> (Int | Bool)) | Prod[Int, Int | Bool], n: Int) = if + a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd + a is Prod then a.Prod#snd + a(n) is Int then a(n) < 42 + else a(n) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.389: a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.390: a is Prod then a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.391: a(n) is Int then a(n) < 42 +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.392: else a(n) +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'app <: Int +//│ ╟── because: cannot constrain 'app <: ¬(¬{Int}) +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.389: a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.390: a is Prod then a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.391: a(n) is Int then a(n) < 42 +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.392: else a(n) +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain ¬Prod[?, ?] & ((Int -> (Int | Bool)) | Prod[Int, Int | Bool]) <: 'a +//│ ╟── because: cannot constrain (Int) ->{⊥} (Int ∨ Bool) ∧ ¬{Prod[?, ?]} <: 'a +//│ ╟── because: cannot constrain (Int) ->{⊥} (Int ∨ Bool) ∧ ¬{Prod[?, ?]} <: ¬(¬{Int ->{'eff} 'app}) +//│ ╟── because: cannot constrain Int ∨ Bool <: 'app +//│ ╟── because: cannot constrain Bool <: 'app +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.389: a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.390: a is Prod then a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.391: a(n) is Int then a(n) < 42 +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.392: else a(n) +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'a <: Int ->{'eff} 'app +//│ ╟── because: cannot constrain 'a <: ¬(¬{Int ->{'eff} 'app}) +//│ ╟── because: cannot constrain (Int) ->{⊥} (Int ∨ Bool) ∧ ¬{Prod[?, ?]} <: ¬(¬{Int ->{'eff} 'app}) +//│ ╟── because: cannot constrain Int ∨ Bool <: 'app +//│ ╟── because: cannot constrain Bool <: 'app +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.389: a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.390: a is Prod then a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.391: a(n) is Int then a(n) < 42 +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.392: else a(n) +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'a <: Int ->{'eff} 'app +//│ ╟── because: cannot constrain 'a <: ¬(¬{Int ->{'eff} 'app}) +//│ ╟── because: cannot constrain (Int) ->{⊥} (Int ∨ Bool) ∧ ¬{Prod[?, ?]} <: ¬(¬{Int ->{'eff} 'app}) +//│ ╟── because: cannot constrain Int ∨ Bool <: 'app +//│ ╟── because: cannot constrain Bool <: 'app +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.389: a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.390: a is Prod then a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.391: a(n) is Int then a(n) < 42 +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.392: else a(n) +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'app <: Int +//│ ╟── because: cannot constrain 'app <: ¬(¬{Int}) +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.389: a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.390: a is Prod then a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.391: a(n) is Int then a(n) < 42 +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.392: else a(n) +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'app <: Int +//│ ╟── because: cannot constrain 'app <: ¬(¬{Int}) +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.389: a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.390: a is Prod then a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.391: a(n) is Int then a(n) < 42 +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.392: else a(n) +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'app <: Int +//│ ╟── because: cannot constrain 'app <: ¬(¬{Int}) +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.389: a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.390: a is Prod then a.Prod#snd +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.391: a(n) is Int then a(n) < 42 +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.392: else a(n) +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain 'app <: Int +//│ ╟── because: cannot constrain 'app <: ¬(¬{Int}) +//│ ╙── because: cannot constrain Bool <: ¬(¬{Int}) +//│ Type: ⊤ + +fun detailed_ex(a: (Int -> (Int | Bool)) | Prod[Int, Int | Bool], n: Int) = if + a is Prod and a.Prod#fst is Int and a.Prod#snd is Int then a.Prod#fst == a.Prod#snd + a is Prod then a.Prod#snd + let x = a(n) + x is Int then x < 42 + else x +//│ Type: ⊤ + +detailed_ex as ((Int -> Int | Bool) | Prod[Int, Int | Bool], Int) -> Int | Bool +//│ Type: ((Int -> (Int | Bool)) | Prod[Int, Int | Bool], Int) ->{⊥} Int | Bool + +// TODO a.Prod#snd is not refined + +:todo +detailed_ex as ((Int -> Int | Bool) | Prod[Int, Int | Bool], Int) -> Bool +//│ ╔══[ERROR] Type error in reference with expected type ((Int -> (Int | Bool)) | Prod[Int, Int | Bool], Int) ->{⊥} Bool +//│ ║ l.514: detailed_ex as ((Int -> Int | Bool) | Prod[Int, Int | Bool], Int) -> Bool +//│ ║ ^^^^^^^^^^^ +//│ ╟── because: cannot constrain ((Int -> (Int | Bool)) | Prod[Int, Int | Bool], Int) ->{'eff} 'res <: ((Int -> (Int | Bool)) | Prod[Int, Int | Bool], Int) -> Bool +//│ ╟── because: cannot constrain 'res <: Bool +//│ ╟── because: cannot constrain 'res <: ¬(¬{Bool}) +//│ ╙── because: cannot constrain Int & ¬⊥ <: ¬(¬{Bool}) +//│ Type: ((Int -> (Int | Bool)) | Prod[Int, Int | Bool], Int) ->{⊥} Bool + +a +//│ Type: (Int -> (Int | Bool)) | Prod[Int, Int | Bool] + +:todo +if a is + Prod then true + else a(1) +//│ ╔══[ERROR] Type error in `if` expression +//│ ║ l.528: if a is +//│ ║ ^^^^ +//│ ║ l.529: Prod then true +//│ ║ ^^^^^^^^^^^^^^^^ +//│ ║ l.530: else a(1) +//│ ║ ^^^^^^^^^^^ +//│ ╙── because: cannot constrain (Int -> (Int | Bool)) | Prod[Int, Int | Bool] <: Int ->{'eff} 'app +//│ Type: (Int | Bool) | Bool + +(x => if x is + Prod then true + else x(1)) of a +//│ Type: (Bool | Int) | Bool diff --git a/hkmc2/shared/src/test/mlscript/logicsub/wf.mls b/hkmc2/shared/src/test/mlscript/logicsub/wf.mls new file mode 100644 index 0000000000..6772203682 --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/wf.mls @@ -0,0 +1,206 @@ +:bbml +//│ Type: ⊤ + +//│ Type: ⊤ + +// functions intersection requires disjoint parameters + +fun wf: (Int -> Int) & (Str -> Str) +//│ Type: ⊤ + +:e +fun ill: (Int -> Int) & (Int -> Any) +fun ill(x) = x +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.12: fun ill: (Int -> Int) & (Int -> Any) +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +:e +fun ill: [a: Int] -> Int & [b: Int] -> Int +//│ ╔══[ERROR] Illegal forall annotation. +//│ ║ l.20: fun ill: [a: Int] -> Int & [b: Int] -> Int +//│ ╙── ^^^^^^^^ +//│ ═══[ERROR] Invalid type +//│ Type: ⊤ + +:e +fun ill: [A] -> (A -> A) & (Int -> Int) +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.28: fun ill: [A] -> (A -> A) & (Int -> Int) +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +fun wf: [a: (Int -> Int) & (Str -> Str)] +//│ Type: ⊤ + +:e +fun ill: [a: (Int -> Int) & (Int -> Any)] +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.38: fun ill: [a: (Int -> Int) & (Int -> Any)] +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +// intersection of the same function type may not always be simplified + +fun wf: (Int -> Int) & (Int -> Int) +//│ Type: ⊤ + +:e +fun ill: (Int -> Int) & (Str -> Str) & (Int -> Int) +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.50: fun ill: (Int -> Int) & (Str -> Str) & (Int -> Int) +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +// same rules apply on negative position +:e +fun ill: (Int -> Int) & (Int -> Any) -> Str +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.58: fun ill: (Int -> Int) & (Int -> Any) -> Str +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +// similarly, records union requires pairwise disjointness + +fun wf: [a: Int] | [a: Str] +//│ Type: ⊤ + +:e +fun ill: [A] -> (Int | Str, A) -> [a: Int, b: A] | [a: Int, b: Str] +fun ill(x, p) = if x is + Int then { a: x, b: p } + Str then { a: 0, b: x } +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.70: fun ill: [A] -> (Int | Str, A) -> [a: Int, b: A] | [a: Int, b: Str] +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╔══[ERROR] Type error in `if` expression with expected type {a: Int, b: A} | {a: Int, b: Str} +//│ ║ l.72: Int then { a: x, b: p } +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.73: Str then { a: 0, b: x } +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain {a: Int, b: Str & (Int | Str)} <: {a: Int, b: A} | {a: Int, b: Str} +//│ ╟── because: cannot constrain {a: Int, b: Str} & {a: Int} <: {a: Int, b: A} +//│ ╙── because: cannot constrain Str <: A +//│ Type: ⊤ + +// it is not required that all records shares the same discriminant field + +fun wf: + (([a: Int, b:Int]) -> Int) & + (([b: Bool, c: Bool]) -> Bool) & + (([a: Str, c: Str]) -> Str) +//│ Type: ⊤ + +fun wf: + (([tag: [a: Int, b:Int]]) -> Int) & + (([tag: [b: Str, c: Bool]]) -> Bool) & + (([tag: [a: Str, c: Str]]) -> Str) +//│ Type: ⊤ + +// functions union merges + +fun wf: ((([a: Int]) -> Int) | (([b: Str]) -> Str)) & (([b: Int]) -> Int) +fun wf(u) = u.b +//│ Type: ⊤ + +fun wf: ((Int | Bool -> Int) | (Bool -> Bool)) & (Str -> Str) +//│ Type: ⊤ + +wf("") +//│ Type: Str + +wf(true) +//│ Type: Bool | Int + +:e +wf(1) +//│ ╔══[ERROR] Type error in application +//│ ║ l.117: wf(1) +//│ ║ ^^^^^ +//│ ╟── because: cannot constrain (((Int | Bool) -> Int) | (Bool -> Bool)) & (Str -> Str) <: Int ->{'eff} 'app +//│ ╟── because: cannot constrain {0: Int} <: {0: Bool} | {0: Str} +//│ ╙── because: cannot constrain ⊤ <: ⊥ +//│ Type: Int + +// function negation and record negation are not wf + +:e +fun ill: ~(Int -> Int) +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.129: fun ill: ~(Int -> Int) +//│ ╙── ^^^^^^^^^^ +//│ Type: ⊤ + +:e +fun ill: ~[a: Int] +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.136: fun ill: ~[a: Int] +//│ ╙── ^^^^^^^^ +//│ Type: ⊤ + +:e +fun ill: (([a: Int]) -> Int) & (~[a: Int] -> ~Int) +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.143: fun ill: (([a: Int]) -> Int) & (~[a: Int] -> ~Int) +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +fun wf: (([a: Int]) -> Int) & (([a: ~Int]) -> ~Int) +//│ Type: ⊤ + +// class declaration has no wf check + +class F(f: (Int -> Int) & (Int -> Any)) +//│ Type: ⊤ + +// wf check on use site + +:e +fun k(f)=f.F#f +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.154: class F(f: (Int -> Int) & (Int -> Any)) +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +// Class not disjoint with itself + +class Pair[A, B](val a: A, val b: B) +class Tri[A, B, C](val a: A, val b: B, val c: C) +//│ Type: ⊤ + +:e +fun ill: (Pair[Int, Int] -> Int) & (Pair[Str, Str] -> Str) +//│ ╔══[ERROR] Ill-formed type +//│ ║ l.173: fun ill: (Pair[Int, Int] -> Int) & (Pair[Str, Str] -> Str) +//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ Type: ⊤ + +fun wf: [A] -> (Pair[A, Any] -> A) & (Tri[A, Any, Any] -> A) +fun wf(x) = if x is + Pair then x.Pair#a + Tri then x.Tri#a +//│ Type: ⊤ + +wf(new Pair(0, "")) +//│ Type: Int + +wf(new Tri(new Pair(0, ""), 0, "")) +//│ Type: Pair['A, 'B] +//│ Where: +//│ Int <: 'A +//│ Str <: 'B + +class + Z() + S() +//│ Type: ⊤ + +fun wf: ((Z, Z) -> Z) & ((Z, S) -> S) & ((S, Z | S) -> S) +//│ Type: ⊤ + +fun zs: Z | S +//│ Type: ⊤ + +wf(zs, zs) +//│ Type: S | Z diff --git a/hkmc2DiffTests/src/test/scala/hkmc2/BbmlDiffMaker.scala b/hkmc2DiffTests/src/test/scala/hkmc2/BbmlDiffMaker.scala index 71b8248465..03c7861dc5 100644 --- a/hkmc2DiffTests/src/test/scala/hkmc2/BbmlDiffMaker.scala +++ b/hkmc2DiffTests/src/test/scala/hkmc2/BbmlDiffMaker.scala @@ -9,7 +9,7 @@ import utils.Scope abstract class BbmlDiffMaker extends JSBackendDiffMaker: - val bbPreludeFile = file / os.up / os.RelPath("bbPrelude.mls") + val bbPreludeFile = file / os.up / os.up / "bbml" / os.RelPath("bbPrelude.mls") val bbmlOpt = new NullaryCommand("bbml"): override def onSet(): Unit = @@ -43,8 +43,12 @@ abstract class BbmlDiffMaker extends JSBackendDiffMaker: val ty = typer.typePurely(trm) val printer = PrettyPrinter((msg: String) => output(msg)) if debug.isSet then printer.print(ty) - val simplif = TypeSimplifier(tl) - val sty = simplif(true, 0)(ty) + val sty = + if config.simplifyTypes then + given hkmc2.utils.TL = tl + val simplif = new TypeSimplifier + simplif(true, 0)(ty) + else ty printer.print(sty) diff --git a/hkmc2DiffTests/src/test/scala/hkmc2/MLsDiffMaker.scala b/hkmc2DiffTests/src/test/scala/hkmc2/MLsDiffMaker.scala index 21e4866c50..25dfa58e99 100644 --- a/hkmc2DiffTests/src/test/scala/hkmc2/MLsDiffMaker.scala +++ b/hkmc2DiffTests/src/test/scala/hkmc2/MLsDiffMaker.scala @@ -52,6 +52,7 @@ abstract class MLsDiffMaker extends DiffMaker: val parseOnly = NullaryCommand("parseOnly") val typeCheck = FlagCommand(false, "typeCheck") + val noTypeSimplification = FlagCommand(false, "ns") // * Compiler configuration @@ -86,7 +87,8 @@ abstract class MLsDiffMaker extends DiffMaker: S(StackSafety(stackLimit = value)) , )), - liftDefns = Opt.when(liftDefns.isSet)(LiftDefns()) + liftDefns = Opt.when(liftDefns.isSet)(LiftDefns()), + simplifyTypes = noTypeSimplification.isUnset, )