From efb66c18de9a1a2d9abe5034bd9edb266f1dc355 Mon Sep 17 00:00:00 2001 From: Fa1sePRoMiSe Date: Mon, 25 Nov 2024 16:38:21 +0800 Subject: [PATCH] Patches for BbML (#240) * Fix extrusion cache * Fix boolean if type check * Fix quotes * Fix run function type * Fix context envs * Slightly improve error messages * Fix missing operators * Cache skolem extrusion * Rename prelude file --- .../src/test/scala/hkmc2/BbmlDiffMaker.scala | 6 +- .../scala/hkmc2/bbml/ConstraintSolver.scala | 19 +-- .../main/scala/hkmc2/bbml/NormalForm.scala | 4 +- .../src/main/scala/hkmc2/bbml/bbML.scala | 105 +++++++++-------- .../src/main/scala/hkmc2/bbml/types.scala | 14 ++- .../src/main/scala/hkmc2/syntax/Parser.scala | 8 +- .../src/test/mlscript/bbml/bbBasics.mls | 77 ++++++------ .../src/test/mlscript/bbml/bbBorrowing.mls | 92 ++++++++------- .../src/test/mlscript/bbml/bbBorrowing2.mls | 8 +- .../src/test/mlscript/bbml/bbBounds.mls | 52 ++++----- .../shared/src/test/mlscript/bbml/bbCheck.mls | 26 ++--- .../test/mlscript/bbml/bbCyclicExtrude.mls | 40 +++---- .../src/test/mlscript/bbml/bbErrors.mls | 18 +-- .../src/test/mlscript/bbml/bbExtrude.mls | 44 ++++--- .../src/test/mlscript/bbml/bbFunGenFix.mls | 2 +- .../shared/src/test/mlscript/bbml/bbFuns.mls | 6 +- .../shared/src/test/mlscript/bbml/bbGPCE.mls | 51 ++++---- hkmc2/shared/src/test/mlscript/bbml/bbId.mls | 10 +- .../test/mlscript/bbml/bbLetRegEncoding.mls | 94 ++++++++------- .../shared/src/test/mlscript/bbml/bbList.mls | 52 +++++---- .../src/test/mlscript/bbml/bbOption.mls | 2 +- .../shared/src/test/mlscript/bbml/bbPoly.mls | 46 ++++---- .../bbml/{bbPredef.mls => bbPrelude.mls} | 13 ++- hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls | 93 +++++++-------- hkmc2/shared/src/test/mlscript/bbml/bbRec.mls | 12 +- hkmc2/shared/src/test/mlscript/bbml/bbRef.mls | 110 ++++++++++-------- .../src/test/mlscript/bbml/bbSelfApp.mls | 4 +- hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls | 50 ++++---- .../src/test/mlscript/bbml/bbSyntax.mls | 2 +- 29 files changed, 566 insertions(+), 494 deletions(-) rename hkmc2/shared/src/test/mlscript/bbml/{bbPredef.mls => bbPrelude.mls} (58%) diff --git a/hkmc2/jvm/src/test/scala/hkmc2/BbmlDiffMaker.scala b/hkmc2/jvm/src/test/scala/hkmc2/BbmlDiffMaker.scala index 603147d7d..778434845 100644 --- a/hkmc2/jvm/src/test/scala/hkmc2/BbmlDiffMaker.scala +++ b/hkmc2/jvm/src/test/scala/hkmc2/BbmlDiffMaker.scala @@ -8,15 +8,15 @@ import hkmc2.bbml.* abstract class BbmlDiffMaker extends JSBackendDiffMaker: - val bbPredefFile = file / os.up / os.RelPath("bbPredef.mls") + val bbPreludeFile = file / os.up / os.RelPath("bbPrelude.mls") val bbmlOpt = new NullaryCommand("bbml"): override def onSet(): Unit = super.onSet() if isGlobal then typeCheck.disable.isGlobal = true typeCheck.disable.setCurrentValue(()) - if file =/= bbPredefFile then - importFile(bbPredefFile, verbose = false) + if file =/= bbPreludeFile then + importFile(bbPreludeFile, verbose = false) lazy val bbCtx = diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala index 7cc6662e6..9a5d4347c 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala @@ -37,9 +37,9 @@ class ConstraintSolver(infVarState: InfVarUid.State, tl: TraceLogger): import hkmc2.bbml.NormalForm.* - private def freshXVar(lvl: Int): InfVar = InfVar(lvl, infVarState.nextUid, new VarState(), false) + private def freshXVar(lvl: Int, hint: Option[Str]): InfVar = InfVar(lvl, infVarState.nextUid, new VarState(), false)(hint) - def extrude(ty: Type)(using lvl: Int, pol: Bool, cache: ExtrudeCache): Type = + def extrude(ty: Type)(using lvl: Int, pol: Bool, cache: ExtrudeCache, bbctx: BbCtx, cctx: CCtx, tl: TL): Type = trace[Type](s"Extruding[${printPol(pol)}] $ty", r => s"~> $r"): if ty.lvl <= lvl then ty else ty.toBasic/*TODO improve extrude directly*/ match case ClassLikeType(sym, targs) => @@ -49,13 +49,18 @@ class ConstraintSolver(infVarState: InfVarUid.State, tl: TraceLogger): case t: Type => Wildcard(extrude(t)(using lvl, !pol), extrude(t)) }) case v @ InfVar(_, uid, state, true) => // * skolem - if pol then - state.upperBounds.foldLeft[Type](Top)(_ & _) - else - state.lowerBounds.foldLeft[Type](Bot)(_ | _) + cache.getOrElse(uid -> pol, { + val nv = freshXVar(lvl, v.hint) + cache += uid -> pol -> nv + if pol then + constrainImpl(state.upperBounds.foldLeft[Type](Top)(_ & _), nv) + else + constrainImpl(nv, state.lowerBounds.foldLeft[Type](Bot)(_ | _)) + nv + }) case v @ InfVar(_, uid, _, false) => cache.getOrElse(uid -> pol, { - val nv = freshXVar(lvl) + val nv = freshXVar(lvl, v.hint) cache += uid -> pol -> nv if pol then v.state.upperBounds ::= nv diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala index e566e6414..14b0d535c 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/NormalForm.scala @@ -34,8 +34,8 @@ extends NormalForm with CachedBasicType: }.foldLeft[Opt[Ls[(InfVar, Bool)]]](S(Nil))((res, p) => (res, p) match { // * None -> bot case (N, _) => N case (S(Nil), p) => S(p :: Nil) - case (S((InfVar(v, uid1, s, k), p1) :: tail), (InfVar(_, uid2, _, _), p2)) if uid1 === uid2 => - if p1 === p2 then S((InfVar(v, uid1, s, k), p1) :: tail) else N + case (S((lhs @ InfVar(v, uid1, s, k), p1) :: tail), (InfVar(_, uid2, _, _), p2)) if uid1 === uid2 => + if p1 === p2 then S((InfVar(v, uid1, s, k)(lhs.hint), p1) :: tail) else N case (S(head :: tail), p) => S(p :: head :: tail) }) vars match diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala index d2fc0a387..5e373c924 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala @@ -23,13 +23,10 @@ final case class BbCtx( ctx: Ctx, parent: Option[BbCtx], lvl: Int, - clsDefs: HashMap[Str, ClassDef], - env: HashMap[Uid[Symbol], GeneralType], - quoteSkolemEnv: HashMap[Uid[Symbol], InfVar], // * SkolemTag for variables in quasiquotes + env: HashMap[Uid[Symbol], GeneralType] ): def +=(p: Symbol -> GeneralType): Unit = env += p._1.uid -> p._2 def get(sym: Symbol): Option[GeneralType] = env.get(sym.uid) orElse parent.dlof(_.get(sym))(None) - def *=(cls: ClassDef): Unit = clsDefs += cls.sym.id.name -> cls def getCls(name: Str): Option[TypeSymbol] = for elem <- ctx.get(name) @@ -38,10 +35,8 @@ final case class BbCtx( yield cls def &=(p: (Symbol, Type, InfVar)): Unit = env += p._1.uid -> BbCtx.varTy(p._2, p._3)(using this) - quoteSkolemEnv += p._1.uid -> p._3 - def getSk(sym: Symbol): Option[Type] = quoteSkolemEnv.get(sym.uid) orElse parent.dlof(_.getSk(sym))(None) - def nest: BbCtx = copy(parent = Some(this)) - def nextLevel: BbCtx = copy(lvl = lvl + 1) + def nest: BbCtx = copy(parent = Some(this), env = HashMap.empty) + def nextLevel: BbCtx = copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty) given (using ctx: BbCtx): Raise = ctx.raise @@ -62,7 +57,7 @@ object BbCtx: def refTy(ct: Type, sk: Type)(using ctx: BbCtx): Type = ClassLikeType(ctx.getCls("Ref").get, Wildcard(ct, ct) :: Wildcard.out(sk) :: Nil) def init(raise: Raise)(using Elaborator.State, Elaborator.Ctx): BbCtx = - new BbCtx(raise, summon, None, 1, HashMap.empty, HashMap.empty, HashMap.empty) + new BbCtx(raise, summon, None, 1, HashMap.empty) end BbCtx @@ -72,13 +67,13 @@ class BBTyper(using elState: Elaborator.State, tl: TL): private val infVarState = new InfVarUid.State() private val solver = new ConstraintSolver(infVarState, tl) - private def freshSkolem(using ctx: BbCtx): InfVar = - InfVar(ctx.lvl, infVarState.nextUid, new VarState(), true) - private def freshVar(using ctx: BbCtx): InfVar = - InfVar(ctx.lvl, infVarState.nextUid, new VarState(), false) - private def freshWildcard(using ctx: BbCtx) = - val in = freshVar - val out = freshVar + private def freshSkolem(hint: Option[Str])(using ctx: BbCtx): InfVar = + InfVar(ctx.lvl, infVarState.nextUid, new VarState(), true)(hint) + private def freshVar(hint: Option[Str])(using ctx: BbCtx): InfVar = + InfVar(ctx.lvl, infVarState.nextUid, new VarState(), false)(hint) + private def freshWildcard(hint: Option[Str])(using ctx: BbCtx) = + val in = freshVar(hint) + val out = freshVar(hint) // in.state.upperBounds ::= out // * Not needed for soundness; complicates inferred types Wildcard(in, out) @@ -157,7 +152,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): private def genPolyType(tvs: Ls[QuantVar], body: => GeneralType)(using ctx: BbCtx, cctx: CCtx) = val bds = tvs.map: case qv @ QuantVar(sym, ub, lb) => - val tv = freshVar + val tv = freshVar(S(sym.name)) ctx += sym -> tv // TODO: a type var symbol may be better... tv -> qv bds.foreach: @@ -176,7 +171,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): private def instantiate(ty: PolyType)(using ctx: BbCtx): GeneralType = ty.instantiate(infVarState.nextUid, ctx.lvl)(tl) - private def extrude(ty: GeneralType)(using ctx: BbCtx, pol: Bool): GeneralType = ty match + 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) case PolyType(tvs, body) => PolyType(tvs, extrude(body)) case PolyFunType(args, ret, eff) => @@ -185,7 +180,6 @@ class BBTyper(using elState: Elaborator.State, tl: TL): private def constrain(lhs: Type, rhs: Type)(using ctx: BbCtx, cctx: CCtx): Unit = solver.constrain(lhs, rhs) - // TODO: content type private def typeCode(code: Term)(using ctx: BbCtx): (Type, Type, Type) = given CCtx = CCtx.init(code, N) code match @@ -201,12 +195,12 @@ class BBTyper(using elState: Elaborator.State, tl: TL): given BbCtx = nestCtx val bds = params.map: case Param(_, sym, _) => - val tv = freshVar - val sk = freshSkolem + val tv = freshVar(S(sym.name)) + val sk = freshSkolem(S(sym.name)) nestCtx &= (sym, tv, sk) (tv, sk) val (bodyTy, ctxTy, eff) = typeCode(body) - val res = freshVar(using ctx) + val res = freshVar(N)(using ctx) constrain(ctxTy, bds.foldLeft[Type](res)((res, bd) => res | bd._2)) (FunType(bds.map(_._1), bodyTy, Bot), res, eff) case Term.App(lhs, Term.Tup(rhs)) => @@ -215,26 +209,29 @@ class BBTyper(using elState: Elaborator.State, tl: TL): case (res, p: Fld) => val (ty, ctx, eff) = typeCode(p.term) (ty :: res._1, res._2 | ctx, res._3 | eff) - val resTy = freshVar + val resTy = freshVar(N) constrain(lhsTy, FunType(rhsTy.reverse, resTy, Bot)) // TODO: right (resTy, lhsCtx | rhsCtx, lhsEff | rhsEff) + case sel @ Term.Sel(Term.Ref(_: TopLevelSymbol), _) if sel.symbol.isDefined => + val (opTy, eff) = typeCheck(Ref(sel.symbol.get)(sel.nme, 666)) // FIXME 666 + (tryMkMono(opTy, sel), Bot, eff) case Term.Unquoted(body) => val (ty, eff) = typeCheck(body) - val tv = freshVar - val cr = freshVar + val tv = freshVar(N) + val cr = freshVar(N) constrain(tryMkMono(ty, body), BbCtx.codeTy(tv, cr)) (tv, cr, eff) case Term.Blk(LetDecl(sym) :: DefineVar(sym2, rhs) :: Nil, body) if sym2 is sym => // TODO: more than one!! val (rhsTy, rhsCtx, rhsEff) = typeCode(rhs)(using ctx) val nestCtx = ctx.nextLevel given BbCtx = nestCtx - val sk = freshSkolem + val sk = freshSkolem(S(sym.nme)) nestCtx &= (sym, rhsTy, sk) val (bodyTy, bodyCtx, bodyEff) = typeCode(body) - val res = freshVar(using ctx) + val res = freshVar(N)(using ctx) constrain(bodyCtx, sk | res) (bodyTy, rhsCtx | res, rhsEff | bodyEff) - case Term.IfLike(Keyword.`if`, Split.Cons(Branch(cond, Pattern.Lit(BoolLit(true)), Split.Else(cons)), Split.Else(alts))) => + case Term.IfLike(Keyword.`if`, Split.Let(_, cond, Split.Cons(Branch(_, Pattern.Lit(BoolLit(true)), Split.Else(cons)), Split.Else(alts)))) => val (condTy, condCtx, condEff) = typeCode(cond) val (consTy, consCtx, consEff) = typeCode(cons) val (altsTy, altsCtx, altsEff) = typeCode(alts) @@ -252,7 +249,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): () case N => given BbCtx = ctx.nextLevel - val funTyV = freshVar + val funTyV = freshVar(S(sym.nme)) pctx += sym -> funTyV // for recursive functions val (res, _) = typeCheck(lam) val funTy = tryMkMono(res, lam) @@ -266,10 +263,10 @@ class BBTyper(using elState: Elaborator.State, tl: TL): : (GeneralType, Type) = split match case Split.Cons(Branch(scrutinee, Pattern.ClassLike(sym, _, _, _), cons), alts) => - // * Pattern matching + // * Pattern matching for classes val (clsTy, tv, emptyTy) = ctx.getCls(sym.nme).flatMap(_.defn) match case S(cls) => - (ClassLikeType(sym, cls.tparams.map(_ => freshWildcard)), freshVar, ClassLikeType(sym, cls.tparams.map(_ => Wildcard.empty))) + (ClassLikeType(sym, cls.tparams.map(_ => freshWildcard(N))), (freshVar(N)), ClassLikeType(sym, cls.tparams.map(_ => Wildcard.empty))) case _ => error(msg"Cannot match ${scrutinee.toString} as ${sym.toString}" -> split.toLoc :: Nil) (Bot, Bot, Bot) @@ -286,6 +283,23 @@ class BBTyper(using elState: Elaborator.State, tl: TL): val (altsTy, altsEff) = typeSplit(alts, sign)(using nestCtx2) val allEff = scrutineeEff | (consEff | altsEff) (sign.getOrElse(tryMkMono(consTy, cons) | tryMkMono(altsTy, alts)), allEff) + // * Pattern matching for literals + case Split.Cons(Branch(scrutinee, Pattern.Lit(lit), cons), alts) => + val (scrutineeTy, scrutineeEff) = typeCheck(scrutinee) + val litTy = 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), litTy) + val nestCtx1 = ctx.nest + val nestCtx2 = ctx.nest + 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 Split.Let(name, term, tail) => val nestCtx = ctx.nest given BbCtx = nestCtx @@ -361,8 +375,8 @@ class BBTyper(using elState: Elaborator.State, tl: TL): val (ty, eff) = typeCheck(f.term) Left(ty) :: Right(eff) :: Nil .partitionMap(x => x) - val effVar = freshVar - val retVar = freshVar + val effVar = freshVar(N) + val retVar = freshVar(N) constrain(tryMkMono(funTy, t), FunType(argTy.map((tryMkMono(_, t))), retVar, effVar)) (retVar, argEff.foldLeft[Type](effVar | lhsEff)((res, e) => res | e)) @@ -394,8 +408,6 @@ class BBTyper(using elState: Elaborator.State, tl: TL): (error(msg"Variable not found: ${sym.nme}" -> t.toLoc :: Nil), Bot) case Blk(stats, res) => - val nestCtx = ctx.nest - given BbCtx = nestCtx val effBuff = ListBuffer.empty[Type] def goStats(stats: Ls[Statement]): Unit = stats match case Nil => () @@ -406,7 +418,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): require(sym2 is sym) val (rhsTy, eff) = typeCheck(rhs) effBuff += eff - nestCtx += sym -> rhsTy + ctx += sym -> rhsTy goStats(stats) case TermDefinition(_, Fun, sym, ParamList(_, ps) :: Nil, sig, Some(body), _, _) :: stats => typeFunDef(sym, Term.Lam(ps, body), sig, ctx) @@ -418,7 +430,6 @@ class BBTyper(using elState: Elaborator.State, tl: TL): ctx += sym -> typeType(sig) goStats(stats) case (clsDef: ClassDef) :: stats => - ctx *= clsDef goStats(stats) goStats(stats) val (ty, eff) = typeCheck(res) @@ -434,7 +445,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): given BbCtx = nestCtx val tvs = params.map: case Param(_, sym, sign) => - val ty = sign.map(s => typeType(s)(using nestCtx)).getOrElse(freshVar) + val ty = sign.map(s => typeType(s)(using nestCtx)).getOrElse(freshVar(S(sym.nme))) nestCtx += sym -> ty ty val (bodyTy, eff) = typeCheck(body) @@ -446,7 +457,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): val map = HashMap[Uid[Symbol], TypeArg]() val targs = clsDfn.tparams.map { case TyParam(_, _, targ) => - val ty = freshWildcard + val ty = freshWildcard(N) map += targ.uid -> ty ty } @@ -471,12 +482,12 @@ class BBTyper(using elState: Elaborator.State, tl: TL): val map = HashMap[Uid[Symbol], TypeArg]() val targs = clsDfn.tparams.map { case TyParam(_, S(_), targ) => - val ty = freshVar + val ty = freshVar(N) map += targ.uid -> ty ty case TyParam(_, N, targ) => // val ty = freshWildcard // FIXME probably not correct - val ty = freshVar + val ty = freshVar(N) map += targ.uid -> ty ty } @@ -498,28 +509,28 @@ class BBTyper(using elState: Elaborator.State, tl: TL): case Term.Region(sym, body) => val nestCtx = ctx.nextLevel given BbCtx = nestCtx - val sk = freshSkolem + val sk = freshSkolem(S(sym.nme)) nestCtx += sym -> BbCtx.regionTy(sk) val (res, eff) = typeCheck(body) - val tv = freshVar(using ctx) + val tv = freshVar(N)(using ctx) constrain(eff, tv | sk) (extrude(res)(using ctx, true), tv | allocType) case Term.RegRef(reg, value) => val (regTy, regEff) = typeCheck(reg) val (valTy, valEff) = typeCheck(value) - val sk = freshVar + val sk = freshVar(N) constrain(tryMkMono(regTy, reg), BbCtx.regionTy(sk)) (BbCtx.refTy(tryMkMono(valTy, value), sk), sk | (regEff | valEff)) case Term.Assgn(lhs, rhs) => val (lhsTy, lhsEff) = typeCheck(lhs) val (rhsTy, rhsEff) = typeCheck(rhs) - val sk = freshVar + val sk = freshVar(N) constrain(tryMkMono(lhsTy, lhs), BbCtx.refTy(tryMkMono(rhsTy, rhs), sk)) (tryMkMono(rhsTy, rhs), sk | (lhsEff | rhsEff)) case Term.Deref(ref) => val (refTy, refEff) = typeCheck(ref) - val sk = freshVar - val ctnt = freshVar + val sk = freshVar(N) + val ctnt = freshVar(N) constrain(tryMkMono(refTy, ref), BbCtx.refTy(ctnt, sk)) (ctnt, sk | refEff) case Term.Quoted(body) => diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala index 048dfa735..273ac5f5c 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala @@ -156,7 +156,9 @@ sealed abstract class BasicType extends Type: this match case ClassLikeType(name, targs) => if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.mkString(", ")}]" - case InfVar(lvl, uid, _, isSkolem) => if isSkolem then s"<α>${uid}_$lvl" else s"α${uid}_$lvl" + case v @ InfVar(lvl, uid, _, isSkolem) => + val name = v.hint.getOrElse("α") + if isSkolem then s"<$name>${uid}_$lvl" else s"$name${uid}_$lvl" case FunType(arg :: Nil, ret, eff) => s"${arg.paren} ->${printEff(eff)} ${ret.paren}" case FunType(args, ret, eff) => s"(${args.mkString(", ")}) ->${printEff(eff)} ${ret.paren}" case ComposedType(lhs, rhs, pol) => s"${lhs.paren} ${if pol then "∨" else "∧"} ${rhs.paren}" @@ -222,7 +224,7 @@ case class ClassLikeType(name: TypeSymbol | ModuleSymbol, targs: Ls[TypeArg]) ex case ty: Type => ty.subst }) -final case class InfVar(vlvl: Int, uid: Uid[InfVar], state: VarState, isSkolem: Bool) extends BasicType: +final case class InfVar(vlvl: Int, uid: Uid[InfVar], state: VarState, isSkolem: Bool)(val hint: Option[Str]) extends BasicType: override def subst(using map: Map[Uid[InfVar], InfVar]): ThisType = map.get(uid).getOrElse(this) given Ordering[InfVar] = Ordering.by(_.uid) @@ -267,11 +269,11 @@ case class PolyType(tvs: Ls[InfVar], body: GeneralType) extends GeneralType: override def subst(using map: Map[Uid[InfVar], InfVar]): ThisType = PolyType(tvs.map { - case InfVar(lvl, uid, state, skolem) => + case v @ InfVar(lvl, uid, state, skolem) => val newSt = new VarState() newSt.lowerBounds = state.lowerBounds.map(_.subst) newSt.upperBounds = state.upperBounds.map(_.subst) - InfVar(lvl, uid, newSt, skolem) + InfVar(lvl, uid, newSt, skolem)(v.hint) }, body.subst) // * This function will only return the body after substitution @@ -288,7 +290,7 @@ case class PolyType(tvs: Ls[InfVar], body: GeneralType) extends GeneralType: def skolemize(nextUid: => Uid[InfVar], lvl: Int)(tl: TL) = // * Note that by this point, the state is supposed to be frozen/treated as immutable val map = tvs.map(v => - val sk = InfVar(lvl, nextUid, new VarState(), true) + val sk = InfVar(lvl, nextUid, new VarState(), true)(v.hint) tl.log(s"skolemize $v ~> $sk") v.uid -> sk ).toMap @@ -296,7 +298,7 @@ case class PolyType(tvs: Ls[InfVar], body: GeneralType) extends GeneralType: def instantiate(nextUid: => Uid[InfVar], lvl: Int)(tl: TL): GeneralType = val map = tvs.map(v => - val nv = InfVar(lvl, nextUid, new VarState(), false) + val nv = InfVar(lvl, nextUid, new VarState(), false)(v.hint) tl.log(s"instantiate $v ~> $nv") v.uid -> nv ).toMap diff --git a/hkmc2/shared/src/main/scala/hkmc2/syntax/Parser.scala b/hkmc2/shared/src/main/scala/hkmc2/syntax/Parser.scala index b1fbb84ea..f9b88ec9a 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/syntax/Parser.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/syntax/Parser.scala @@ -547,7 +547,9 @@ abstract class Parser( val ele = simpleExprImpl(prec) term match case InfixApp(lhs, Keyword.`then`, rhs) => - Quoted(IfElse(InfixApp(Unquoted(lhs), Keyword.`then`, Unquoted(rhs)), Unquoted(ele))) + Quoted(IfLike(Keyword.`if`, Block( + InfixApp(Unquoted(lhs), Keyword.`then`, Unquoted(rhs)) :: Modified(Keyword.`else`, N, Unquoted(ele)) :: Nil + ))) case tk => err(msg"Expected '`in'; found ${tk.toString} instead" -> tk.toLoc :: Nil) errExpr @@ -559,7 +561,9 @@ abstract class Parser( errExpr case (IDENT(nme, sym), loc) :: _ => consume - exprCont(Tree.Quoted(Tree.Ident(nme).withLoc(S(loc))), prec, allowNewlines = false) + val res = + if nme === "true" then Tree.BoolLit(true) else if nme === "false" then Tree.BoolLit(false) else Tree.Ident(nme) + exprCont(Tree.Quoted(res.withLoc(S(loc))), prec, allowNewlines = false) case (LITVAL(lit), l0) :: _ => consume exprCont(Tree.Quoted(lit.asTree.withLoc(S(l0))), prec, allowNewlines = false) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls index c6883a585..3c89d7bf9 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls @@ -19,7 +19,7 @@ false fun id(x) = x id -//│ Type: forall α1_2: α1_2 -> α1_2 +//│ Type: forall x3_2: x3_2 -> x3_2 fun inc(x) = x + 1 //│ Type: ⊤ @@ -28,7 +28,7 @@ fun mul(x, y) = x * y //│ Type: ⊤ x => x -//│ Type: (α7_1) ->{⊥} α7_1 +//│ Type: (x9_1) ->{⊥} x9_1 + //│ Type: (Int, Int) ->{⊥} Int @@ -108,14 +108,14 @@ class Some[A](value: A) //│ Type: ⊤ new Some(true) -//│ Type: Some[α13_1] +//│ Type: Some[α15_1] //│ Where: -//│ Bool <: α13_1 +//│ Bool <: α15_1 new Some(42) -//│ Type: Some[α14_1] +//│ Type: Some[α16_1] //│ Where: -//│ Int <: α14_1 +//│ Int <: α16_1 let p = new Point(1.0, 0.0, 0.0) in p.Point#x //│ Type: Num @@ -149,22 +149,22 @@ fun foofoo(x) = //│ Type: ⊤ new Printer(foofoo) -//│ Type: Printer[α22_1] +//│ Type: Printer[α24_1] //│ Where: -//│ α22_1 <: Int +//│ α24_1 <: Int let ip = new Printer(foofoo) in ip.Printer#f(42) //│ Type: Str :e let ip = new Printer(foofoo) in ip.Printer#f("42") -//│ ╔══[ERROR] Type error in string literal with expected type α30_1 +//│ ╔══[ERROR] Type error in string literal with expected type α32_1 //│ ║ l.160: let ip = new Printer(foofoo) in ip.Printer#f("42") //│ ║ ^^^^ +//│ ╟── because: cannot constrain Str <: α32_1 +//│ ╟── because: cannot constrain Str <: α32_1 +//│ ╟── because: cannot constrain Str <: ¬(~α30_1) //│ ╟── because: cannot constrain Str <: α30_1 -//│ ╟── because: cannot constrain Str <: α30_1 -//│ ╟── because: cannot constrain Str <: ¬(~α28_1) -//│ ╟── because: cannot constrain Str <: α28_1 //│ ╙── because: cannot constrain Str <: ¬(~{Int}) //│ Type: Str @@ -175,23 +175,23 @@ fun inc(x) = x + 1 //│ Type: ⊤ new TFun(inc) -//│ Type: TFun[α34_1] +//│ Type: TFun[α36_1] //│ Where: -//│ Int <: α34_1 -//│ α34_1 <: Int +//│ Int <: α36_1 +//│ α36_1 <: Int let tf = new TFun(inc) in tf.TFun#f(1) //│ Type: Int :e let tf = new TFun(inc) in tf.TFun#f("1") -//│ ╔══[ERROR] Type error in string literal with expected type α42_1 +//│ ╔══[ERROR] Type error in string literal with expected type α44_1 //│ ║ l.187: let tf = new TFun(inc) in tf.TFun#f("1") //│ ║ ^^^ +//│ ╟── because: cannot constrain Str <: α44_1 +//│ ╟── because: cannot constrain Str <: α44_1 +//│ ╟── because: cannot constrain Str <: ¬(~α42_1) //│ ╟── because: cannot constrain Str <: α42_1 -//│ ╟── because: cannot constrain Str <: α42_1 -//│ ╟── because: cannot constrain Str <: ¬(~α40_1) -//│ ╟── because: cannot constrain Str <: α40_1 //│ ╙── because: cannot constrain Str <: ¬(~{Int}) //│ Type: Str ∨ Int @@ -205,77 +205,68 @@ class Pair[A, B](fst: A, snd: B) //│ Type: Bool -:fixme if 1 < 2 then 1 else 0 -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut),Lit(BoolLit(true)),Else(Lit(IntLit(1)))),Else(Lit(IntLit(0)))) (of class hkmc2.semantics.Split$Cons) +//│ Type: Int + -:fixme if false then 1 else "1" -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut),Lit(BoolLit(true)),Else(Lit(IntLit(1)))),Else(Lit(StrLit(1)))) (of class hkmc2.semantics.Split$Cons) +//│ Type: Int ∨ Str if 1 is Int then 1 else 0 //│ Type: Int + fun test(x) = if x is Int then x + 1 else 0 test -//│ Type: (Int ∧ (¬Int ∨ Int)) -> Int +//│ Type: (¬Int ∨ Int) -> Int test(1) //│ Type: Int -:fixme // FIXME[CY] test("1") -//│ ╔══[ERROR] Type error in string literal with expected type α64_1 -//│ ║ l.230: test("1") -//│ ║ ^^^ -//│ ╟── because: cannot constrain Str <: α64_1 -//│ ╟── because: cannot constrain Str <: α64_1 -//│ ╙── because: cannot constrain Str <: Int //│ Type: Int -:fixme fun fact(n) = if n > 1 then n * fact(n - 1) else 1 -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut),Lit(BoolLit(true)),Else(App(Sel(Ref(globalThis:import#bbPredef),Ident(*)),Tup(List(Fld(‹›,Ref(n),None), Fld(‹›,App(Sel(Ref(globalThis:block#49),Ident(fact)),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))),None)))))),Else(Lit(IntLit(1)))) (of class hkmc2.semantics.Split$Cons) +//│ Type: ⊤ fact -//│ Type: ⊥ +//│ Type: Int -> Int fact(1) -//│ Type: ⊥ +//│ Type: Int -:fixme fun fact2 = case 0 then 1 n then n * fact2(n - 1) -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut),Lit(IntLit(0)),Else(Lit(IntLit(1)))),Let(n,Ref(caseScrut),Else(App(Sel(Ref(globalThis:import#bbPredef),Ident(*)),Tup(List(Fld(‹›,Ref(n),None), Fld(‹›,App(Sel(Ref(globalThis:block#52),Ident(fact2)),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))),None))))))) (of class hkmc2.semantics.Split$Cons) +//│ Type: ⊤ fact2 -//│ Type: ⊥ +//│ Type: Int -> Int fact2(0) -//│ Type: ⊥ +//│ Type: Int class Foo[A](x: A -> A) //│ Type: ⊤ new Foo(x => x) -//│ Type: Foo[α74_1] +//│ Type: Foo[α76_1] fun f(g) = new Foo(g) f -//│ Type: forall α77_2: (α77_2 -> α77_2) -> Foo[α77_2] +//│ Type: forall α79_2: (α79_2 -> α79_2) -> Foo[α79_2] f(x => x).Foo#x -//│ Type: (α79_1) ->{⊥} α79_1 +//│ Type: (α81_1) ->{⊥} α81_1 g => (new Foo(g)).Foo#x -//│ Type: (α84_1 -> α84_1) ->{⊥} (α84_1) ->{⊥} α84_1 +//│ Type: (α86_1 -> α86_1) ->{⊥} (α86_1) ->{⊥} α86_1 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls index 2e7978390..1a4586da3 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls @@ -35,9 +35,9 @@ fun next: [A, Br] -> Iter[A, Br] ->{Br} A //│ Type: ⊤ letreg(r => r) -//│ Type: Reg[?, α21_1] +//│ Type: Reg[?, E23_1] //│ Where: -//│ α21_1 <: Alloc +//│ E23_1 <: Alloc letreg of r => let b = mkVec(r) @@ -47,11 +47,11 @@ letreg of r => 123 clear(b) r -//│ Type: Reg[?, α24_1] +//│ Type: Reg[?, E28_1] //│ Where: -//│ α24_1 <: Alloc +//│ E28_1 <: Alloc + -:fixme // * Non-lexical borrowing pattern encoded with a thunk letreg of r => let b = mkVec(r) @@ -61,7 +61,7 @@ letreg of r => 123 if next(it) > 0 then () => 0 else () => clear(b) k() -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut),Lit(BoolLit(true)),Else(Lam(List(),Lit(IntLit(0))))),Else(Lam(List(),App(Sel(Ref(globalThis:block#5),Ident(clear)),Tup(List(Fld(‹›,Ref(b),None))))))) (of class hkmc2.semantics.Split$Cons) +//│ Type: Int :e letreg of r => @@ -89,9 +89,11 @@ letreg of r => //│ ║ ^^^^^^^^^^^^^^^^^^ //│ ║ l.74: k() //│ ║ ^^^^^ -//│ ╟── because: cannot constrain α62_1 <: Alloc -//│ ╟── because: cannot constrain α62_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain E73_1 <: Alloc +//│ ╟── because: cannot constrain E73_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ ¬Rg96_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ~{Alloc} <: Rg96_1 +//│ ╙── because: cannot constrain ~{Alloc} <: ¬() //│ Type: ⊥ :e @@ -105,31 +107,33 @@ letreg of r => clear(b) r //│ ╔══[ERROR] Type error in block -//│ ║ l.98: letreg of r => -//│ ║ ^^^^^^^^^^^^^^ -//│ ║ l.99: let b = mkVec(r) -//│ ║ ^^^^^^^^^^^^^^^^^^ -//│ ║ l.100: clear(b) +//│ ║ l.100: letreg of r => +//│ ║ ^^^^^^^^^^^^^^ +//│ ║ l.101: let b = mkVec(r) +//│ ║ ^^^^^^^^^^^^^^^^^^ +//│ ║ l.102: clear(b) //│ ║ ^^^^^^^^^^ -//│ ║ l.101: iterate(b) of it => +//│ ║ l.103: iterate(b) of it => //│ ║ ^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.102: next(it) +//│ ║ l.104: next(it) //│ ║ ^^^^^^^^^^^^ -//│ ║ l.103: clear(b) +//│ ║ l.105: clear(b) //│ ║ ^^^^^^^^^^^^ -//│ ║ l.104: 123 +//│ ║ l.106: 123 //│ ║ ^^^^^^^ -//│ ║ l.105: clear(b) +//│ ║ l.107: clear(b) //│ ║ ^^^^^^^^^^ -//│ ║ l.106: r +//│ ║ l.108: r //│ ║ ^^^ -//│ ╟── because: cannot constrain α84_1 <: Alloc -//│ ╟── because: cannot constrain α84_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) -//│ Type: Reg[?, α84_1] +//│ ╟── because: cannot constrain E97_1 <: Alloc +//│ ╟── because: cannot constrain E97_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ Rg117_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain Rg117_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ Type: Reg[?, E97_1] //│ Where: -//│ ⊤ <: α84_1 -//│ α84_1 <: Alloc +//│ ⊤ <: E97_1 +//│ E97_1 <: Alloc letreg of r => @@ -138,9 +142,9 @@ letreg of r => next(it) use(r) r -//│ Type: Reg[?, α106_1] +//│ Type: Reg[?, E123_1] //│ Where: -//│ α106_1 <: Alloc +//│ E123_1 <: Alloc :e letreg of r => @@ -151,27 +155,29 @@ letreg of r => use(r) r //│ ╔══[ERROR] Type error in block -//│ ║ l.146: letreg of r => +//│ ║ l.150: letreg of r => //│ ║ ^^^^^^^^^^^^^^ -//│ ║ l.147: use(r) +//│ ║ l.151: use(r) //│ ║ ^^^^^^^^ -//│ ║ l.148: integers(r) of it => +//│ ║ l.152: integers(r) of it => //│ ║ ^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.149: use(r) +//│ ║ l.153: use(r) //│ ║ ^^^^^^^^^^ -//│ ║ l.150: next(it) +//│ ║ l.154: next(it) //│ ║ ^^^^^^^^^^^^ -//│ ║ l.151: use(r) +//│ ║ l.155: use(r) //│ ║ ^^^^^^^^ -//│ ║ l.152: r +//│ ║ l.156: r //│ ║ ^^^ -//│ ╟── because: cannot constrain α118_1 <: Alloc -//│ ╟── because: cannot constrain α118_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) -//│ Type: Reg[?, α118_1] +//│ ╟── because: cannot constrain E137_1 <: Alloc +//│ ╟── because: cannot constrain E137_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ Rg149_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain Rg149_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ Type: Reg[?, E137_1] //│ Where: -//│ ⊤ <: α118_1 -//│ α118_1 <: Alloc +//│ ⊤ <: E137_1 +//│ E137_1 <: Alloc letreg of r0 => letreg of r1 => @@ -180,9 +186,9 @@ letreg of r0 => next(it) use(r1) r1 -//│ Type: Reg[?, in α147_1] +//│ Type: Reg[?, in E174_1] //│ Where: -//│ α147_1 <: Alloc +//│ E174_1 <: Alloc // * Can leak the iterator diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls index 26541901b..79d8c5bca 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls @@ -46,9 +46,11 @@ letreg of r => //│ ║ ^^^^^^^^^^^ //│ ║ l.35: write(r) //│ ║ ^^^^^^^^^^ -//│ ╟── because: cannot constrain α27_1 <: Alloc -//│ ╟── because: cannot constrain α27_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain E29_1 <: Alloc +//│ ╟── because: cannot constrain E29_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ Rg41_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain Rg41_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls index 138bc7b90..735887e2e 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls @@ -7,33 +7,33 @@ (x => x): [A restricts Int] -> A -> A -//│ Type: forall α2_2: (α2_2) ->{⊥} α2_2 +//│ Type: forall A4_2: (A4_2) ->{⊥} A4_2 //│ Where: -//│ Int <: α2_2 +//│ Int <: A4_2 (x => x - 1): [A extends Int restricts Int] -> A -> A -//│ Type: forall α4_2: (α4_2) ->{⊥} α4_2 +//│ Type: forall A6_2: (A6_2) ->{⊥} A6_2 //│ Where: -//│ Int <: α4_2 -//│ α4_2 <: Int +//│ Int <: A6_2 +//│ A6_2 <: Int fun iid: [A extends Int] -> A -> A fun iid(x) = x //│ Type: ⊤ iid -//│ Type: forall α7_2: (α7_2) ->{⊥} α7_2 +//│ Type: forall A9_2: (A9_2) ->{⊥} A9_2 //│ Where: -//│ α7_2 <: Int +//│ A9_2 <: Int :e iid("42") -//│ ╔══[ERROR] Type error in string literal with expected type α9_1 +//│ ╔══[ERROR] Type error in string literal with expected type A11_1 //│ ║ l.31: iid("42") //│ ║ ^^^^ -//│ ╟── because: cannot constrain Str <: α9_1 -//│ ╟── because: cannot constrain Str <: α9_1 +//│ ╟── because: cannot constrain Str <: A11_1 +//│ ╟── because: cannot constrain Str <: A11_1 //│ ╙── because: cannot constrain Str <: Int //│ Type: Str @@ -46,10 +46,10 @@ class Foo[A] fun foo: [A extends Foo[in Nothing out Any] restricts Foo[in Num]] -> A -> A foo -//│ Type: forall α11_2: (α11_2) ->{⊥} α11_2 +//│ Type: forall A13_2: (A13_2) ->{⊥} A13_2 //│ Where: -//│ Foo[in Num] <: α11_2 -//│ α11_2 <: Foo[?] +//│ Foo[in Num] <: A13_2 +//│ A13_2 <: Foo[?] fun bar: Foo[in Num out Int] //│ Type: ⊤ @@ -72,7 +72,7 @@ baz fun bazbaz: [A extends Int] -> A -> [B extends A] -> B bazbaz -//│ Type: (Int) ->{⊥} forall α17_3: ⊥ +//│ Type: (Int) ->{⊥} forall B19_3: ⊥ fun foofun: [A extends Int -> Int restricts Any -> Int] -> A -> Int -> Int foofun @@ -83,21 +83,21 @@ foofun(x => x + 1)(42) fun bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A bazbaz -//│ Type: forall α21_2: (α21_2) ->{⊥} (forall α22_3: α21_2 -> α21_2) ->{⊥} α21_2 +//│ Type: forall A23_2: (A23_2) ->{⊥} (forall B24_3: A23_2 -> A23_2) ->{⊥} A23_2 //│ Where: -//│ α21_2 <: Int +//│ A23_2 <: Int bazbaz(42)(x => x + 1) //│ Type: Int fun cc: [A extends B -> B restricts B -> B, B extends A -> A restricts A -> A] -> A -> B -> Bool cc -//│ Type: forall α26_2, α27_2: (α26_2) ->{⊥} (α27_2) ->{⊥} Bool +//│ Type: forall A28_2, B29_2: (A28_2) ->{⊥} (B29_2) ->{⊥} Bool //│ Where: -//│ α26_2 -> α26_2 <: α27_2 -//│ α27_2 <: α26_2 -> α26_2 -//│ α27_2 -> α27_2 <: α26_2 -//│ α26_2 <: α27_2 -> α27_2 +//│ A28_2 -> A28_2 <: B29_2 +//│ B29_2 <: A28_2 -> A28_2 +//│ B29_2 -> B29_2 <: A28_2 +//│ A28_2 <: B29_2 -> B29_2 fun w: Any -> Nothing //│ Type: ⊤ @@ -110,18 +110,18 @@ fun h: [C] -> ([A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B :e bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A -//│ ╔══[ERROR] Cannot type non-function term Sel(Ref(globalThis:block#16),Ident(bazbaz)) as (<α>35_2) ->{⊥} (forall α34_3: α34_3) ->{⊥} <α>35_2 +//│ ╔══[ERROR] Cannot type non-function term Sel(Ref(globalThis:block#16),Ident(bazbaz)) as (37_2) ->{⊥} (forall B36_3: B36_3) ->{⊥} 37_2 //│ ║ l.112: bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A //│ ╙── ^^^^^^ -//│ Type: forall α33_2: (α33_2) ->{⊥} (forall α34_3: α33_2 -> α33_2) ->{⊥} α33_2 +//│ Type: forall A35_2: (A35_2) ->{⊥} (forall B36_3: A35_2 -> A35_2) ->{⊥} A35_2 //│ Where: -//│ α33_2 <: Int +//│ A35_2 <: Int (x => f => bazbaz(x)(f)): [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A -//│ Type: forall α36_2: (α36_2) ->{⊥} (forall α37_3: α36_2 -> α36_2) ->{⊥} α36_2 +//│ Type: forall A38_2: (A38_2) ->{⊥} (forall B39_3: A38_2 -> A38_2) ->{⊥} A38_2 //│ Where: -//│ α36_2 <: Int +//│ A38_2 <: Int h(x => f => bazbaz(x)(f))(42) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls index 085769743..31a6d65c4 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls @@ -77,7 +77,7 @@ fun high(f) = f(42) //│ Type: ⊤ high -//│ Type: (forall α6_2: (α6_2) ->{⊥} α6_2) ->{⊥} Int +//│ Type: (forall A8_2: (A8_2) ->{⊥} A8_2) ->{⊥} Int high((x => x): [A] -> A -> A) @@ -91,19 +91,19 @@ high(x => x + 1) //│ ╔══[ERROR] Type error in reference with expected type Int //│ ║ l.90: high(x => x + 1) //│ ║ ^ -//│ ╙── because: cannot constrain <α>10_2 <: Int -//│ ╔══[ERROR] Type error in application with expected type <α>10_2 +//│ ╙── because: cannot constrain 12_2 <: Int +//│ ╔══[ERROR] Type error in application with expected type 12_2 //│ ║ l.90: high(x => x + 1) //│ ║ ^^^^^ -//│ ╙── because: cannot constrain Int <: <α>10_2 +//│ ╙── because: cannot constrain Int <: 12_2 //│ Type: Int (let a = 0 in x => x): [A] -> A -> A -//│ Type: forall α11_2: (α11_2) ->{⊥} α11_2 +//│ Type: forall A13_2: (A13_2) ->{⊥} A13_2 + -:fixme (if false then x => x else y => y): [A] -> A -> A -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut),Lit(BoolLit(true)),Else(Lam(List(Param(‹›,x,None)),Ref(x)))),Else(Lam(List(Param(‹›,y,None)),Ref(y)))) (of class hkmc2.semantics.Split$Cons) +//│ Type: forall A16_2: (A16_2) ->{⊥} A16_2 fun baz: Int -> (([A] -> A -> A), Int) -> Int @@ -118,24 +118,24 @@ fun baz(z) = :e baz: Int -> (([A] -> A -> A), Int) -> Int -//│ ╔══[ERROR] Cannot type non-function term Sel(Ref(globalThis:block#17),Ident(baz)) as (Int) ->{⊥} (forall α25_2: (α25_2) ->{⊥} α25_2, Int) ->{⊥} Int +//│ ╔══[ERROR] Cannot type non-function term Sel(Ref(globalThis:block#17),Ident(baz)) as (Int) ->{⊥} (forall A26_2: (A26_2) ->{⊥} A26_2, Int) ->{⊥} Int //│ ║ l.120: baz: Int -> (([A] -> A -> A), Int) -> Int //│ ╙── ^^^ //│ Type: ⊥ baz(42) -//│ Type: (forall α21_2: (α21_2) ->{⊥} α21_2, Int) ->{⊥} Int +//│ Type: (forall A22_2: (A22_2) ->{⊥} A22_2, Int) ->{⊥} Int :e baz(42): (([A] -> A -> A), Int) -> Int -//│ ╔══[ERROR] Cannot type non-function term App(Sel(Ref(globalThis:block#17),Ident(baz)),Tup(List(Fld(‹›,Lit(IntLit(42)),None)))) as (forall α26_2: (α26_2) ->{⊥} α26_2, Int) ->{⊥} Int +//│ ╔══[ERROR] Cannot type non-function term App(Sel(Ref(globalThis:block#17),Ident(baz)),Tup(List(Fld(‹›,Lit(IntLit(42)),None)))) as (forall A27_2: (A27_2) ->{⊥} A27_2, Int) ->{⊥} Int //│ ║ l.131: baz(42): (([A] -> A -> A), Int) -> Int //│ ╙── ^^^^^^^ //│ Type: ⊥ (z => (f, x) => baz(z)(f, x)): Int -> (([A] -> A -> A), Int) -> Int -//│ Type: (Int) ->{⊥} (forall α27_2: (α27_2) ->{⊥} α27_2, Int) ->{⊥} Int +//│ Type: (Int) ->{⊥} (forall A28_2: (A28_2) ->{⊥} A28_2, Int) ->{⊥} Int fun id: [A] -> A -> A @@ -143,11 +143,11 @@ fun id(x) = x //│ Type: ⊤ id: [A] -> A -> A -//│ Type: forall α33_2: (α33_2) ->{⊥} α33_2 +//│ Type: forall A34_2: (A34_2) ->{⊥} A34_2 (id: [A] -> A -> A): [A] -> A -> A -//│ Type: forall α36_2: (α36_2) ->{⊥} α36_2 +//│ Type: forall A37_2: (A37_2) ->{⊥} A37_2 42: Int | Num //│ Type: Int ∨ Num diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls index 0eb9648c4..0917daecf 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls @@ -4,57 +4,57 @@ let f = (x => (x : [A] -> A -> A)) in f -//│ Type: (⊤ -> ⊥) ->{⊥} forall α1_2: (α1_2) ->{⊥} α1_2 +//│ Type: (⊤ -> ⊥) ->{⊥} forall A3_2: (A3_2) ->{⊥} A3_2 let f = ((x => x) : [A] -> A -> A) in f -//│ Type: forall α3_2: (α3_2) ->{⊥} α3_2 +//│ Type: forall A7_2: (A7_2) ->{⊥} A7_2 let foo = f => (x => f(x(x)) : [A] -> A -> A) in foo -//│ Type: (α11_1 -> (⊤ -> ⊥)) ->{⊥} (α6_1 -> α11_1) ->{⊥} forall α7_2: (α7_2) ->{⊥} α7_2 +//│ Type: (α15_1 -> (⊤ -> ⊥)) ->{⊥} (x10_1 -> α15_1) ->{⊥} forall A11_2: (A11_2) ->{⊥} A11_2 //│ Where: -//│ α6_1 <: α6_1 -> α11_1 +//│ x10_1 <: x10_1 -> α15_1 f => (let g = x => x(x) in f(g(g))) : [A] -> A -> A -//│ Type: (⊥ -> (⊤ -> ⊥)) ->{⊥} forall α19_2: (α19_2) ->{⊥} α19_2 +//│ Type: (⊥ -> (⊤ -> ⊥)) ->{⊥} forall A25_2: (A25_2) ->{⊥} A25_2 :e f => (let g = x => f(x(x)) in g) : [A] -> A -> A -//│ ╔══[ERROR] Type error in block with expected type (<α>31_2) ->{⊥} <α>31_2 +//│ ╔══[ERROR] Type error in block with expected type (39_2) ->{⊥} 39_2 //│ ║ l.21: f => (let g = x => f(x(x)) in g) : [A] -> A -> A //│ ║ ^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α32_2 ->{α35_2 ∨ α33_2} α36_2 <: <α>31_2 -> <α>31_2 -//│ ╟── because: cannot constrain <α>31_2 <: D( α32_2 ) -//│ ╟── because: cannot constrain <α>31_2 <: α32_2 -//│ ╙── because: cannot constrain <α>31_2 <: ¬(~{α32_2 ->{α33_2} α34_2}) -//│ Type: (⊥ -> ⊥) ->{⊥} forall α30_2: (α30_2) ->{⊥} α30_2 +//│ ╟── because: cannot constrain x40_2 ->{α43_2 ∨ α41_2} α44_2 <: 39_2 -> 39_2 +//│ ╟── because: cannot constrain 39_2 <: D( x40_2 ) +//│ ╟── because: cannot constrain 39_2 <: x40_2 +//│ ╙── because: cannot constrain 39_2 <: ¬(~{x40_2 ->{α41_2} α42_2}) +//│ Type: (⊥ -> ⊥) ->{⊥} forall A38_2: (A38_2) ->{⊥} A38_2 f => (x => f(x(x)) : [A] -> A -> A) -//│ Type: (α46_1 -> (⊤ -> ⊥)) ->{⊥} (α41_1 -> α46_1) ->{⊥} forall α42_2: (α42_2) ->{⊥} α42_2 +//│ Type: (α55_1 -> (⊤ -> ⊥)) ->{⊥} (x50_1 -> α55_1) ->{⊥} forall A51_2: (A51_2) ->{⊥} A51_2 //│ Where: -//│ α41_1 <: α41_1 -> α46_1 +//│ x50_1 <: x50_1 -> α55_1 let foo = f => (f(x => x(x)) : [A] -> A -> A) in foo -//│ Type: (((α61_1 ->{α64_1} α63_1) ->{α64_1} α63_1) -> (⊤ -> ⊥)) ->{⊥} forall α54_2: (α54_2) ->{⊥} α54_2 +//│ Type: (((x72_1 ->{α75_1} α74_1) ->{α75_1} α74_1) -> (⊤ -> ⊥)) ->{⊥} forall A65_2: (A65_2) ->{⊥} A65_2 //│ Where: -//│ α61_1 <: α61_1 ->{α64_1} α63_1 +//│ x72_1 <: x72_1 ->{α75_1} α74_1 :todo let foo(f) = (f(x => x(x)) : [A] -> A -> A) in foo -//│ Type: (((α77_1 ->{α80_1} α79_1) ->{α80_1} α79_1) -> (⊤ -> ⊥)) ->{⊥} forall α70_2: (α70_2) ->{⊥} α70_2 +//│ Type: (((x90_1 ->{α93_1} α92_1) ->{α93_1} α92_1) -> (⊤ -> ⊥)) ->{⊥} forall A83_2: (A83_2) ->{⊥} A83_2 //│ Where: -//│ α77_1 <: α77_1 ->{α80_1} α79_1 +//│ x90_1 <: x90_1 ->{α93_1} α92_1 :todo fun foo(f) = (f(x => x(x)) : [A] -> A -> A) -//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (α86_2) ->{⊥} forall α87_3: (α87_3) ->{⊥} α87_3 found +//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (f101_2) ->{⊥} forall A102_3: (A102_3) ->{⊥} A102_3 found //│ ║ l.48: fun foo(f) = (f(x => x(x)) : [A] -> A -> A) //│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ Type: ⊤ f => (let g = x => x(x) in let tmp = g(g) in f(g)) : [A] -> A -> A -//│ Type: ((((α110_1 ∨ (α110_1 ->{α113_1} α112_1)) -> α112_1) ->{α113_1} α112_1) -> (⊤ -> ⊥)) ->{⊥} forall α103_2: (α103_2) ->{⊥} α103_2 +//│ Type: ((((x127_1 ∨ (x127_1 ->{α130_1} α129_1)) -> α129_1) ->{α130_1} α129_1) -> (⊤ -> ⊥)) ->{⊥} forall A120_2: (A120_2) ->{⊥} A120_2 //│ Where: -//│ α110_1 <: (α110_1 ∨ (α110_1 ->{α113_1} α112_1)) -> α112_1 +//│ x127_1 <: (x127_1 ∨ (x127_1 ->{α130_1} α129_1)) -> α129_1 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls b/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls index cc6c72e4a..282e7789d 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls @@ -7,16 +7,16 @@ //│ ╔══[ERROR] Type error in application //│ ║ l.6: 2(2) //│ ║ ^^^^ -//│ ╙── because: cannot constrain Int <: Int ->{α0_1} α1_1 +//│ ╙── because: cannot constrain Int <: Int ->{α2_1} α3_1 //│ Type: ⊥ (x => x(0))(1) -//│ ╔══[ERROR] Type error in integer literal with expected type α2_1 +//│ ╔══[ERROR] Type error in integer literal with expected type x4_1 //│ ║ l.13: (x => x(0))(1) //│ ║ ^ -//│ ╟── because: cannot constrain Int <: α2_1 -//│ ╟── because: cannot constrain Int <: α2_1 -//│ ╙── because: cannot constrain Int <: ¬(~{Int ->{α3_1} α4_1}) +//│ ╟── because: cannot constrain Int <: x4_1 +//│ ╟── because: cannot constrain Int <: x4_1 +//│ ╙── because: cannot constrain Int <: ¬(~{Int ->{α5_1} α6_1}) //│ Type: ⊥ (1).Foo#a() @@ -29,11 +29,11 @@ fun inc(x) = x + 1 inc("oops") -//│ ╔══[ERROR] Type error in string literal with expected type α9_1 +//│ ╔══[ERROR] Type error in string literal with expected type x11_1 //│ ║ l.31: inc("oops") //│ ║ ^^^^^^ -//│ ╟── because: cannot constrain Str <: α9_1 -//│ ╟── because: cannot constrain Str <: α9_1 +//│ ╟── because: cannot constrain Str <: x11_1 +//│ ╟── because: cannot constrain Str <: x11_1 //│ ╙── because: cannot constrain Str <: ¬¬Int //│ Type: Int @@ -42,7 +42,7 @@ inc : Int //│ ╔══[ERROR] Type error in selection with expected type Int //│ ║ l.41: inc : Int //│ ║ ^^^ -//│ ╙── because: cannot constrain α12_1 -> Int <: Int +//│ ╙── because: cannot constrain x14_1 -> Int <: Int //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls index 73df402a6..cc8edf8ce 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls @@ -7,9 +7,9 @@ fun f(y) = // * the parameter type of y is extruded. f -//│ Type: forall α1_2: α1_2 -> α1_2 +//│ Type: forall y3_2: y3_2 -> y3_2 //│ Where: -//│ α1_2 <: ⊤ -> Int +//│ y3_2 <: ⊤ -> Int fun foo: [A] -> A -> Int fun foo(x) = 0 @@ -27,17 +27,25 @@ fun g(y) = //│ Type: ⊤ g -//│ Type: (forall α17_2: (⊥) ->{⊥} Int) ->{⊥} forall α18_2: (⊤) ->{⊥} Int +//│ Type: (forall A21_2: (⊥) ->{⊥} Int) ->{⊥} forall A22_2: (⊤) ->{⊥} Int g(foo) //│ Type: (⊤) ->{⊥} Int :e y `=> (let t = run(x `=> x `+ y) in y) -//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+)) +//│ ╔══[ERROR] Type error in quoted term with expected type CodeBase[out T32_3, ⊥, ?] //│ ║ l.36: y `=> (let t = run(x `=> x `+ y) in y) -//│ ╙── ^ -//│ Type: CodeBase[out α26_3 -> α26_3, ⊥, ?] +//│ ║ ^^^^^^^^^^^^ +//│ ╟── because: cannot constrain CodeBase[out x33_5 -> α40_5, out α42_4, ?] <: CodeBase[out T32_3, ⊥, ?] +//│ ╟── because: cannot constrain D( α42_4 ) <: ⊥ +//│ ╟── because: cannot constrain α42_4 <: ¬() +//│ ╟── because: cannot constrain (¬⊥ ∧ ¬x43_4) ∧ 31_3 <: ¬() +//│ ╟── because: cannot constrain 31_3 <: x43_4 +//│ ╙── because: cannot constrain 31_3 <: ¬() +//│ Type: CodeBase[out y30_3 -> y30_3, ⊥, ?] +//│ Where: +//│ y30_3 <: Int class C[A](m: A, n: A -> Int) //│ Type: ⊤ @@ -45,11 +53,11 @@ class C[A](m: A, n: A -> Int) fun f: [A] -> ([B] -> (C[out B] & A) -> B) -> A -> Int f -//│ Type: forall α41_2: (forall α42_3: (C[out α42_3] ∧ α41_2) ->{⊥} α42_3) ->{⊥} (α41_2) ->{⊥} Int +//│ Type: forall A49_2: (forall B50_3: (C[out B50_3] ∧ A49_2) ->{⊥} B50_3) ->{⊥} (A49_2) ->{⊥} Int fun g: [D] -> C[in Int out D] -> D g -//│ Type: forall α43_2: (C[in Int out α43_2]) ->{⊥} α43_2 +//│ Type: forall D51_2: (C[in Int out D51_2]) ->{⊥} D51_2 f(g) @@ -68,13 +76,17 @@ f(g)(foo) :fixme // ??? f(g)(bar) -//│ ╔══[ERROR] Type error in selection with expected type α52_1 -//│ ║ l.70: f(g)(bar) +//│ ╔══[ERROR] Type error in selection with expected type A64_1 +//│ ║ l.78: f(g)(bar) //│ ║ ^^^ -//│ ╟── because: cannot constrain C[Int] <: α52_1 -//│ ╟── because: cannot constrain C[in D( Int ) out D( Int )] <: α52_1 -//│ ╟── because: cannot constrain C[in D( Int ) out D( Int )] <: ¬C[in D() out ¬⊥] ∨ C[in D( Int ) out ¬⊥ ∧ α55_1] -//│ ╟── because: cannot constrain (D( Int )) ∧ (D( )) <: ¬⊥ ∧ α55_1 -//│ ╟── because: cannot constrain Int <: α55_1 -//│ ╙── because: cannot constrain Int <: ⊥ +//│ ╟── because: cannot constrain C[Int] <: A64_1 +//│ ╟── because: cannot constrain C[in D( Int ) out D( Int )] <: A64_1 +//│ ╟── because: cannot constrain C[in D( Int ) out D( Int )] <: ¬C[in D() out ¬⊥ ∧ B67_1] ∨ C[in D( Int ) out ¬⊥ ∧ D68_1] +//│ ╟── because: cannot constrain (D( Int )) ∧ (D( B67_1 )) <: ¬⊥ ∧ D68_1 +//│ ╟── because: cannot constrain Int && B67_1 <: D68_1 +//│ ╟── because: cannot constrain Int && B67_1 <: B69_1 +//│ ╟── because: cannot constrain Int && B67_1 <: B69_1 +//│ ╟── because: cannot constrain Int && B67_1 <: ¬() +//│ ╟── because: cannot constrain B67_1 <: ¬(Int) +//│ ╙── because: cannot constrain <: ¬(Int) //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls b/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls index c2a653673..b93bac6ce 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls @@ -30,7 +30,7 @@ fun helper(a) = write(a) //│ Type: ⊤ helper -//│ Type: forall α21_2: Reg[out α21_2, ?] ->{α21_2} Int +//│ Type: forall Rg23_2: Reg[out Rg23_2, ?] ->{Rg23_2} Int subreg(basereg) of r0 => helper(r0) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls b/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls index 1ef078245..ac483fe82 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls @@ -4,7 +4,7 @@ fun f(x, y) = x(y) f -//│ Type: forall α2_2, α3_2, α4_2: (α2_2 ->{α3_2} α4_2, α2_2) ->{α3_2} α4_2 +//│ Type: forall y4_2, α5_2, α6_2: (y4_2 ->{α5_2} α6_2, y4_2) ->{α5_2} α6_2 f((x => x), 42) @@ -18,9 +18,9 @@ fun id: [A] -> A -> A //│ Type: ⊤ id : [A] -> A -> A -//│ Type: forall α16_2: (α16_2) ->{⊥} α16_2 +//│ Type: forall A18_2: (A18_2) ->{⊥} A18_2 id(id) : [A] -> A -> A -//│ Type: forall α19_2: (α19_2) ->{⊥} α19_2 +//│ Type: forall A21_2: (A21_2) ->{⊥} A21_2 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls index 1b726b808..91424396c 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls @@ -1,54 +1,48 @@ :bbml //│ Type: ⊤ -:fixme + fun power: [C] -> CodeBase[out Num, out C, out Any] -> Int -> CodeBase[out Num, out C, out Any] fun power(x) = case 0 then `1.0 n then x `*. power(x)(n - 1) power -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut),Lit(IntLit(0)),Else(Quoted(Lit(DecLit(1.0))))),Let(n,Ref(caseScrut),Else(Quoted(App(Ref(builtin:*),Tup(List(Fld(‹›,Unquoted(Ref(x)),None), Fld(‹›,Unquoted(App(App(Sel(Ref(globalThis:block#0),Ident(power)),Tup(List(Fld(‹›,Ref(x),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),None)))))))) (of class hkmc2.semantics.Split$Cons) +//│ Type: forall C3_2: (CodeBase[out Num, out C3_2, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Num, out C3_2, ?] fun id: [A] -> A -> A fun id(x) = x //│ Type: ⊤ -:fixme // FIXME[CY] + run(x `=> id(x) `* x) -//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(*)) -//│ ║ l.18: run(x `=> id(x) `* x) -//│ ╙── ^ -//│ Type: ⊤ +//│ Type: Int -> Int + -:fixme fun assertNotZero: [C] -> CodeBase[out Num, out C, out Any] -> CodeBase[out Num, out C, out Any] fun assertNotZero(x) = `if (x `== `0.0) then `error else x let checkedDiv = x `=> y `=> x `/. (assertNotZero(y)) run(checkedDiv) -//│ /!!!\ Uncaught error: scala.MatchError: IfElse(InfixApp(Unquoted(Quoted(App(Ident(==),Tup(List(Unquoted(Ident(x)), Unquoted(Quoted(DecLit(0.0)))))))),keyword 'then',Unquoted(Quoted(Ident(error)))),Unquoted(Ident(x))) (of class hkmc2.syntax.Tree$IfElse) +//│ Type: Num -> (Num -> Num) + -:todo // :fixme fun show: [T] -> CodeBase[out T, out Any, out Any] -> Str = s => "debug" show //│ Type: (CodeBase[?, ?, ?]) ->{⊥} Str -:fixme // FIXME[CY] + fun inc(dbg) = x `=> let c = x `+ `1 in let t = dbg(c) in c inc -//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+)) -//│ ║ l.41: x `=> let c = x `+ `1 in let t = dbg(c) in c -//│ ╙── ^ -//│ Type: forall α34_2: (CodeBase[⊥, ?, ?] ->{α34_2} ⊤) ->{α34_2} CodeBase[out ⊤ -> ⊥, ⊥, ?] +//│ Type: forall α85_2: (CodeBase[out Int, ?, ?] ->{α85_2} ⊤) ->{α85_2} CodeBase[out Int -> Int, ⊥, ?] inc(c => log(show(c))) -//│ Type: CodeBase[out ⊤ -> ⊥, ⊥, ?] +//│ Type: CodeBase[out Int -> Int, ⊥, ?] + -:fixme 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] fun body(x, y) = case 0 then x @@ -57,37 +51,44 @@ fun body(x, y) = case fun gib_naive(n) = (x, y) `=> body(x, y)(n) let gn5 = run(gib_naive(5)) -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut),Lit(IntLit(0)),Else(Ref(x))),Cons(Branch(Ref(caseScrut),Lit(IntLit(1)),Else(Ref(y))),Let(n,Ref(caseScrut),Else(App(App(Sel(Ref(globalThis:block#7),Ident(body)),Tup(List(Fld(‹›,Ref(y),None), Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x)),None), Fld(‹›,Unquoted(Ref(y)),None))))),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))))))) (of class hkmc2.semantics.Split$Cons) +//│ Type: ⊤ fun bind(rhs, k) = `let x = rhs `in k(x) bind -//│ Type: forall α69_2, α70_2, α74_2, α77_2, α80_2, α81_2: (CodeBase[out α69_2, out α70_2, ?], CodeBase[in α74_2 out α74_2 ∨ α69_2, ?, ⊥] ->{α77_2} CodeBase[out α80_2, out α81_2, ?]) ->{α77_2} CodeBase[out α80_2, out α70_2 ∨ α81_2, ?] +//│ Type: forall α153_2, α154_2, α158_2, α163_2, α166_2, α167_2: (CodeBase[out α153_2, out α154_2, ?], CodeBase[in α158_2 out α158_2 ∨ α153_2, ?, ⊥] ->{α163_2} CodeBase[out α166_2, out α167_2, ?]) ->{α163_2} CodeBase[out α166_2, out α154_2 ∨ α167_2, ?] :e -:fixme 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] -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut),Lit(IntLit(0)),Else(Ref(x))),Cons(Branch(Ref(caseScrut),Lit(IntLit(1)),Else(Ref(y))),Let(n,Ref(caseScrut),Else(App(Sel(Ref(globalThis:block#8),Ident(bind)),Tup(List(Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x)),None), Fld(‹›,Unquoted(Ref(y)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z,None)),App(App(Sel(Ref(globalThis:block#9),Ident(body)),Tup(List(Fld(‹›,Ref(y),None), Fld(‹›,Ref(z),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))),TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Ref(C))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))))))))))) (of class hkmc2.semantics.Split$Cons) +//│ ╔══[ERROR] Type error in application with expected type CodeBase[out Int, out 177_2, ?] +//│ ║ l.65: 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 α190_2, out α180_2 ∨ α193_2, ?] <: CodeBase[out Int, out 177_2, ?] +//│ ╟── because: cannot constrain D( α180_2 || α193_2 ) <: 177_2 +//│ ╟── because: cannot constrain α193_2 <: ¬(~177_2) +//│ ╟── because: cannot constrain α192_2 <: ¬(~177_2) +//│ ╟── because: cannot constrain α192_2 <: ¬(~177_2) +//│ ╙── because: cannot constrain <: ¬(~177_2) +//│ Type: ⊤ fun bind: [G] -> (CodeBase[out Int, out G, out Any], [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C | G, out Any]) -> CodeBase[out Int, out G, out Any] fun bind(rhs, k) = `let x = rhs `in k(x) bind -//│ Type: forall α92_2: (CodeBase[out Int, out α92_2, ?], forall α93_3: (CodeBase[out Int, out α93_3, ?]) ->{⊥} CodeBase[out Int, out α93_3 ∨ α92_2, ?]) ->{⊥} CodeBase[out Int, out α92_2, ?] +//│ Type: forall G212_2: (CodeBase[out Int, out G212_2, ?], forall C213_3: (CodeBase[out Int, out C213_3, ?]) ->{⊥} CodeBase[out Int, out C213_3 ∨ G212_2, ?]) ->{⊥} CodeBase[out Int, out G212_2, ?] -:fixme 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 Int, out C, out Any] body -//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut),Lit(IntLit(0)),Else(Ref(x))),Cons(Branch(Ref(caseScrut),Lit(IntLit(1)),Else(Ref(y))),Let(n,Ref(caseScrut),Else(App(Sel(Ref(globalThis:block#10),Ident(bind)),Tup(List(Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x)),None), Fld(‹›,Unquoted(Ref(y)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z,None)),App(App(Sel(Ref(globalThis:block#11),Ident(body)),Tup(List(Fld(‹›,Ref(y),None), Fld(‹›,Ref(z),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))),TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))))))))))) (of class hkmc2.semantics.Split$Cons) +//│ Type: forall G224_2: (CodeBase[out Int, out G224_2, ?], CodeBase[out Int, out G224_2, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Int, out G224_2, ?] fun gib(n) = (x, y) `=> body(x, y)(n) let g5 = run(gib(5)) g5 -//│ Type: ⊤ +//│ Type: (Int, Int) -> Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbId.mls b/hkmc2/shared/src/test/mlscript/bbml/bbId.mls index 16f9a19b3..544d45092 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbId.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbId.mls @@ -9,28 +9,28 @@ id(1) //│ Type: Int id -//│ Type: forall α1_2: α1_2 -> α1_2 +//│ Type: forall x3_2: x3_2 -> x3_2 id(true) //│ Type: Bool id -//│ Type: forall α1_2: α1_2 -> α1_2 +//│ Type: forall x3_2: x3_2 -> x3_2 fun id(x) = x //│ Type: ⊤ id : [A] -> A -> A -//│ Type: forall α6_2: (α6_2) ->{⊥} α6_2 +//│ Type: forall A8_2: (A8_2) ->{⊥} A8_2 (y => y) : [A] -> A -> A -//│ Type: forall α9_2: (α9_2) ->{⊥} α9_2 +//│ Type: forall A11_2: (A11_2) ->{⊥} A11_2 fun id(x) = x (y => id(y)) : [A] -> A -> A -//│ Type: forall α13_2: (α13_2) ->{⊥} α13_2 +//│ Type: forall A15_2: (A15_2) ->{⊥} A15_2 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls index 4c908e346..c954a5c7c 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls @@ -7,7 +7,7 @@ fun letreg: [E,Res] -> ([R] -> Region[R] ->{E | R} Res) ->{E} Res //│ Type: ⊤ letreg -//│ Type: forall α0_2, α1_2: (forall α2_3: (Region[α2_3]) ->{α0_2 ∨ α2_3} α1_2) ->{α0_2} α1_2 +//│ Type: forall E2_2, Res3_2: (forall R4_3: (Region[R4_3]) ->{E2_2 ∨ R4_3} Res3_2) ->{E2_2} Res3_2 letreg(r => r) //│ Type: Region[?] @@ -17,17 +17,23 @@ letreg(r => r).ref 1 //│ ╔══[ERROR] Type error in reference creation //│ ║ l.16: letreg(r => r).ref 1 //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α7_1 <: Region[α9_1] -//│ ╟── because: cannot constrain α7_1 <: ¬(~{Region[α9_1]}) -//│ ╟── because: cannot constrain Region[out ¬⊥] ∧ ¬⊥ <: ¬(~{Region[α9_1]}) -//│ ╟── because: cannot constrain D( ) <: α9_1 -//│ ╟── because: cannot constrain <: α9_1 +//│ ╟── because: cannot constrain Res11_1 <: Region[α15_1] +//│ ╟── because: cannot constrain Res11_1 <: ¬(~{Region[α15_1]}) +//│ ╟── because: cannot constrain Region[in ¬⊥ ∧ R13_1 out ¬⊥ ∧ R14_1] ∧ ¬⊥ <: ¬(~{Region[α15_1]}) +//│ ╟── because: cannot constrain D( R14_1 ) <: α15_1 +//│ ╟── because: cannot constrain R14_1 <: α15_1 +//│ ╟── because: cannot constrain R14_1 <: ¬(~R13_1) +//│ ╟── because: cannot constrain R14_1 <: ¬(~R13_1) +//│ ╟── because: cannot constrain <: ¬(~R13_1) +//│ ╟── because: cannot constrain <: R13_1 //│ ╙── because: cannot constrain <: ¬() //│ ╔══[ERROR] Type error in block //│ ║ l.16: letreg(r => r).ref 1 //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α9_1 ∨ α6_1 <: Alloc -//│ ╟── because: cannot constrain α9_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α15_1 ∨ E10_1 <: Alloc +//│ ╟── because: cannot constrain α15_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain R14_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain R14_1 <: ¬(~{Alloc}) //│ ╙── because: cannot constrain <: ¬(~{Alloc}) //│ Type: Ref[Int, ?] @@ -40,13 +46,15 @@ letreg(r => !(r.ref 1)) :e !letreg(r => r.ref 1) //│ ╔══[ERROR] Type error in block -//│ ║ l.41: !letreg(r => r.ref 1) +//│ ║ l.47: !letreg(r => r.ref 1) //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α26_1 ∨ α21_1 <: Alloc -//│ ╟── because: cannot constrain α26_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α25_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α25_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α34_1 ∨ E28_1 <: Alloc +//│ ╟── because: cannot constrain α34_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α32_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α32_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ R33_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain R33_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) //│ Type: Int letreg of r => @@ -59,21 +67,23 @@ let f = letreg(r => arg => r.ref arg) //│ Type: ⊤ f -//│ Type: α42_1 ->{⊤} Ref[α42_1, ?] +//│ Type: arg50_1 ->{⊤} Ref[arg50_1, ?] :e letreg(r => arg => r.ref arg)(0) //│ ╔══[ERROR] Type error in block -//│ ║ l.65: letreg(r => arg => r.ref arg)(0) +//│ ║ l.73: letreg(r => arg => r.ref arg)(0) //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α53_1 ∨ α45_1 <: Alloc -//│ ╟── because: cannot constrain α53_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α52_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α52_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) -//│ Type: Ref[α50_1, ?] +//│ ╟── because: cannot constrain α63_1 ∨ E54_1 <: Alloc +//│ ╟── because: cannot constrain α63_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α61_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α61_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ R62_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain R62_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ Type: Ref[arg59_1, ?] //│ Where: -//│ Int <: α50_1 +//│ Int <: arg59_1 @@ -84,30 +94,30 @@ fun letreg: [E,Res] -> ([R] -> Region[R] -> Res) ->{E} Res :e letreg(r => r.ref 1) -//│ ╔══[ERROR] Type error in function literal with expected type (Region[<α>60_2]) ->{⊥} α59_1 -//│ ║ l.86: letreg(r => r.ref 1) +//│ ╔══[ERROR] Type error in function literal with expected type (Region[70_2]) ->{⊥} Res69_1 +//│ ║ l.96: letreg(r => r.ref 1) //│ ║ ^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α61_2 <: ⊥ -//│ ╟── because: cannot constrain α61_2 <: ¬() -//│ ╙── because: cannot constrain <α>60_2 <: ¬() +//│ ╟── because: cannot constrain α71_2 <: ⊥ +//│ ╟── because: cannot constrain α71_2 <: ¬() +//│ ╙── because: cannot constrain 70_2 <: ¬() //│ Type: Ref[Int, ?] :e letreg(r => !(r.ref 1)) -//│ ╔══[ERROR] Type error in function literal with expected type (Region[<α>65_2]) ->{⊥} α64_1 -//│ ║ l.96: letreg(r => !(r.ref 1)) -//│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α67_2 ∨ α66_2 <: ⊥ -//│ ╟── because: cannot constrain α67_2 <: ¬() -//│ ╟── because: cannot constrain α66_2 <: ¬() -//│ ╟── because: cannot constrain α66_2 <: ¬() -//│ ╙── because: cannot constrain <α>65_2 <: ¬() -//│ ╔══[ERROR] Type error in function literal with expected type (Region[<α>65_2]) ->{⊥} α64_1 -//│ ║ l.96: letreg(r => !(r.ref 1)) -//│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α67_2 ∨ α66_2 <: ⊥ -//│ ╟── because: cannot constrain α66_2 <: ¬() -//│ ╙── because: cannot constrain <α>65_2 <: ¬() +//│ ╔══[ERROR] Type error in function literal with expected type (Region[76_2]) ->{⊥} Res75_1 +//│ ║ l.106: letreg(r => !(r.ref 1)) +//│ ║ ^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain α78_2 ∨ α77_2 <: ⊥ +//│ ╟── because: cannot constrain α78_2 <: ¬() +//│ ╟── because: cannot constrain α77_2 <: ¬() +//│ ╟── because: cannot constrain α77_2 <: ¬() +//│ ╙── because: cannot constrain 76_2 <: ¬() +//│ ╔══[ERROR] Type error in function literal with expected type (Region[76_2]) ->{⊥} Res75_1 +//│ ║ l.106: letreg(r => !(r.ref 1)) +//│ ║ ^^^^^^^^^^^^^^ +//│ ╟── because: cannot constrain α78_2 ∨ α77_2 <: ⊥ +//│ ╟── because: cannot constrain α77_2 <: ¬() +//│ ╙── because: cannot constrain 76_2 <: ¬() //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls index 028f2bb18..92ca159c9 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls @@ -50,7 +50,7 @@ fun mapi = s => f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, <α>50_2) ->{<α>51_2} <α>50_2) ->{Alloc ∨ <α>51_2} List[out <α>50_2] +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] //│ ║ l.49: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.50: f => map(s) of x => @@ -59,13 +59,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.52: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α66_2 ->{α74_2} List[out α73_2] <: ((Int, <α>50_2) ->{<α>51_2} <α>50_2) ->{Alloc ∨ <α>51_2} List[out <α>50_2] -//│ ╟── because: cannot constrain D( α74_2 ) <: Alloc ∨ <α>51_2 -//│ ╟── because: cannot constrain α74_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α75_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╟── because: cannot constrain α75_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc} && ~<α>51_2) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, <α>50_2) ->{<α>51_2} <α>50_2) ->{Alloc ∨ <α>51_2} List[out <α>50_2] +//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] +//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ 56_2 +//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~56_2) +//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~56_2) +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] //│ ║ l.49: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.50: f => map(s) of x => @@ -74,13 +76,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.52: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α66_2 ->{α74_2} List[out α73_2] <: ((Int, <α>50_2) ->{<α>51_2} <α>50_2) ->{Alloc ∨ <α>51_2} List[out <α>50_2] -//│ ╟── because: cannot constrain D( α74_2 ) <: Alloc ∨ <α>51_2 -//│ ╟── because: cannot constrain α74_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α75_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╟── because: cannot constrain α75_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc} && ~<α>51_2) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, <α>50_2) ->{<α>51_2} <α>50_2) ->{Alloc ∨ <α>51_2} List[out <α>50_2] +//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] +//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ 56_2 +//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~56_2) +//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~56_2) +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] //│ ║ l.49: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.50: f => map(s) of x => @@ -89,13 +93,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.52: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α66_2 ->{α74_2} List[out α73_2] <: ((Int, <α>50_2) ->{<α>51_2} <α>50_2) ->{Alloc ∨ <α>51_2} List[out <α>50_2] -//│ ╟── because: cannot constrain D( α74_2 ) <: Alloc ∨ <α>51_2 -//│ ╟── because: cannot constrain α74_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α75_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╟── because: cannot constrain α75_2 <: ¬(~{Alloc} && ~<α>51_2) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc} && ~<α>51_2) -//│ ╔══[ERROR] Type error in function literal with expected type (List[out <α>50_2]) ->{⊥} ((Int, <α>50_2) ->{<α>51_2} <α>50_2) ->{Alloc ∨ <α>51_2} List[out <α>50_2] +//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] +//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ 56_2 +//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~56_2) +//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~56_2) +//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~56_2) +//│ ╔══[ERROR] Type error in function literal with expected type (List[out 55_2]) ->{⊥} ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] //│ ║ l.47: fun mapi = s => //│ ║ ^^^^ //│ ║ l.48: region r in @@ -108,7 +114,7 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.52: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╙── because: cannot constrain α65_2 ∨ Alloc <: ⊥ +//│ ╙── because: cannot constrain α70_2 ∨ Alloc <: ⊥ //│ Type: ⊤ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls b/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls index 4d2998659..5c9747a5d 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls @@ -6,7 +6,7 @@ class Option[out A](inspect: [E, Res] -> (() ->{E} Res, A ->{E} Res) ->{E} Res) //│ Type: ⊤ opt => opt.Option#inspect -//│ Type: (Option[out α2_1]) ->{⊥} forall α3_2, α4_2: (() ->{α3_2} α4_2, (α2_1) ->{α3_2} α4_2) ->{α3_2} α4_2 +//│ Type: (Option[out α4_1]) ->{⊥} forall E5_2, Res6_2: (() ->{E5_2} Res6_2, (α4_1) ->{E5_2} Res6_2) ->{E5_2} Res6_2 opt => opt.Option#inspect( () => 42 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls index 4774da62b..550663668 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls @@ -18,26 +18,26 @@ fun id(x) = x //│ Type: ⊤ id -//│ Type: forall α5_2: (α5_2) ->{⊥} α5_2 +//│ Type: forall A7_2: (A7_2) ->{⊥} A7_2 :e (x => x + 1): [A] -> A -> A //│ ╔══[ERROR] Type error in reference with expected type Int //│ ║ l.24: (x => x + 1): [A] -> A -> A //│ ║ ^ -//│ ╙── because: cannot constrain <α>8_2 <: Int -//│ ╔══[ERROR] Type error in application with expected type <α>8_2 +//│ ╙── because: cannot constrain 10_2 <: Int +//│ ╔══[ERROR] Type error in application with expected type 10_2 //│ ║ l.24: (x => x + 1): [A] -> A -> A //│ ║ ^^^^^ -//│ ╙── because: cannot constrain Int <: <α>8_2 -//│ Type: forall α7_2: (α7_2) ->{⊥} α7_2 +//│ ╙── because: cannot constrain Int <: 10_2 +//│ Type: forall A9_2: (A9_2) ->{⊥} A9_2 (x => x): [A] -> A -> A -//│ Type: forall α9_2: (α9_2) ->{⊥} α9_2 +//│ Type: forall A11_2: (A11_2) ->{⊥} A11_2 id: [A] -> A -> A -//│ Type: forall α11_2: (α11_2) ->{⊥} α11_2 +//│ Type: forall A13_2: (A13_2) ->{⊥} A13_2 id: Int -> Int //│ Type: (Int) ->{⊥} Int @@ -49,7 +49,7 @@ myInc(id, 0) //│ Type: Int let t = 42 in ((x => x): [A] -> A -> A) -//│ Type: forall α17_2: (α17_2) ->{⊥} α17_2 +//│ Type: forall A19_2: (A19_2) ->{⊥} A19_2 id(42) @@ -63,10 +63,10 @@ class Pair[A, B](a: A, b: B) //│ Type: ⊤ new Pair(42, true) -//│ Type: Pair[α21_1, α22_1] +//│ Type: Pair[α23_1, α24_1] //│ Where: -//│ Int <: α21_1 -//│ Bool <: α22_1 +//│ Int <: α23_1 +//│ Bool <: α24_1 fun swap: [A, B] -> Pair[out A, out B] -> Pair[out B, out A] fun swap(p) = new Pair(p.Pair#b, p.Pair#a) @@ -74,7 +74,7 @@ fun swap(p) = new Pair(p.Pair#b, p.Pair#a) swap -//│ Type: forall α25_2, α26_2: (Pair[out α25_2, out α26_2]) ->{⊥} Pair[out α26_2, out α25_2] +//│ Type: forall A27_2, B28_2: (Pair[out A27_2, out B28_2]) ->{⊥} Pair[out B28_2, out A27_2] let t = new Pair(42, true) in swap(t) //│ Type: Pair[out Bool, out Int] @@ -83,17 +83,17 @@ let t = new Pair("114", "514") in swap(t) //│ Type: Pair[out Str, out Str] let id = ((x => x): [A] -> A -> A) in new Pair(id(42), id("42")) -//│ Type: Pair[α49_1, α50_1] +//│ Type: Pair[α51_1, α52_1] //│ Where: -//│ Int <: α49_1 -//│ Str <: α50_1 +//│ Int <: α51_1 +//│ Str <: α52_1 fun foo: ([A] -> A -> A) -> Int fun foo(x) = 42 //│ Type: ⊤ foo -//│ Type: (forall α54_2: (α54_2) ->{⊥} α54_2) ->{⊥} Int +//│ Type: (forall A56_2: (A56_2) ->{⊥} A56_2) ->{⊥} Int foo(id) //│ Type: Int @@ -119,9 +119,9 @@ class Bar[A](x: A, f: [B] -> B -> B) new Bar(0, id) -//│ Type: Bar[α68_1] +//│ Type: Bar[α70_1] //│ Where: -//│ Int <: α68_1 +//│ Int <: α70_1 let bar = new Bar(0, id) in bar.Bar#f(bar.Bar#x) //│ Type: Int @@ -130,9 +130,9 @@ class Some[A](value: A) //│ Type: ⊤ new Some((x => x): [A] -> A -> A) -//│ Type: Some[α82_1] +//│ Type: Some[α84_1] //│ Where: -//│ α85_1 -> α85_1 <: α82_1 +//│ x87_1 -> x87_1 <: α84_1 let s = new Some((x => x): [A] -> A -> A) in let t = s.Some#value(42) in s.Some#value(false) //│ Type: Bool ∨ Int @@ -143,11 +143,11 @@ fun gen(x) = //│ Type: ⊤ gen -//│ Type: (Int) ->{⊥} forall α99_2: (α99_2) ->{⊥} α99_2 +//│ Type: (Int) ->{⊥} forall A101_2: (A101_2) ->{⊥} A101_2 gen(42) -//│ Type: forall α99_2: (α99_2) ->{⊥} α99_2 +//│ Type: forall A101_2: (A101_2) ->{⊥} A101_2 // FIXME: toLoc :fixme @@ -163,4 +163,4 @@ fun cnt(x) = 42 //│ Type: ⊤ (x => x): [A] -> A -> A -//│ Type: forall α106_2: (α106_2) ->{⊥} α106_2 +//│ Type: forall A108_2: (A108_2) ->{⊥} A108_2 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPredef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPrelude.mls similarity index 58% rename from hkmc2/shared/src/test/mlscript/bbml/bbPredef.mls rename to hkmc2/shared/src/test/mlscript/bbml/bbPrelude.mls index 7fdf74f17..7dc6c9387 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbPredef.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbPrelude.mls @@ -6,20 +6,25 @@ class CodeBase[T, C, S] class Region[T] class Ref[T, S] -// the type here is fake. -fun run: Any -> Any -fun log: Any -> Str + +fun run: [T] -> CodeBase[out T, out Nothing, out Any] -> T +fun log: Str -> Any fun error: Nothing fun (+): (Int, Int) -> Int fun (-): (Int, Int) -> Int fun (*): (Int, Int) -> Int -fun (/): (Int, Int) -> Int +fun (/): (Int, Int) -> Num +fun (+.): (Num, Num) -> Num +fun (-.): (Num, Num) -> Num +fun (*.): (Num, Num) -> Num +fun (/.): (Num, Num) -> Num fun (<): (Int, Int) -> Bool fun (>): (Int, Int) -> Bool fun (<=): (Int, Int) -> Bool fun (>=): (Int, Int) -> Bool +fun (==): [T] -> (T, T) -> Bool fun (&&): (Bool, Bool) -> Bool fun (||): (Bool, Bool) -> Bool diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls index e9043d2c2..31fb2f5c2 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls @@ -6,16 +6,11 @@ //│ Type: CodeBase[out Int, ⊥, ?] :p -:fixme // this should created a quoted keyword `false //│ |`|false| //│ Parsed: -//│ Quoted(Ident(false)) -//│ ╔══[ERROR] Name not found: false -//│ ║ l.10: `false -//│ ╙── ^^^^^ -//│ ═══[ERROR] Cannot quote Error -//│ Type: CodeBase[⊥, ⊥, ?] +//│ Quoted(BoolLit(false)) +//│ Type: CodeBase[out Bool, ⊥, ?] `"rua" //│ Type: CodeBase[out Str, ⊥, ?] @@ -25,7 +20,7 @@ x `=> x -//│ Type: CodeBase[out α0_3 -> α0_3, ⊥, ?] +//│ Type: CodeBase[out x2_3 -> x2_3, ⊥, ?] x `=> `42 //│ Type: CodeBase[out ⊤ -> Int, ⊥, ?] @@ -33,43 +28,31 @@ x `=> `42 :e x `=> 42 //│ ╔══[ERROR] Type error in unquoted term -//│ ║ l.34: x `=> 42 +//│ ║ l.29: x `=> 42 //│ ║ ^^ -//│ ╙── because: cannot constrain Int <: CodeBase[out α12_3, out α13_3, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out α14_3, out α15_3, ?] //│ Type: CodeBase[out ⊤ -> ⊥, ⊥, ?] f `=> x `=> f`(x) -//│ Type: CodeBase[out (α25_3 -> α26_3) -> (α25_3 -> α26_3), ⊥, ?] +//│ Type: CodeBase[out (x27_3 -> α28_3) -> (x27_3 -> α28_3), ⊥, ?] + -:fixme // FIXME[CY] x `=> y `=> x `+ y -//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+)) -//│ ║ l.47: x `=> y `=> x `+ y -//│ ╙── ^ -//│ Type: CodeBase[out ⊤ -> (⊤ -> ⊥), ⊥, ?] +//│ Type: CodeBase[out Int -> (Int -> Int), ⊥, ?] + -:fixme // FIXME[CY] (x, y) `=> x `+ y -//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+)) -//│ ║ l.55: (x, y) `=> x `+ y -//│ ╙── ^ -//│ Type: CodeBase[out (⊤, ⊤) -> ⊥, ⊥, ?] +//│ Type: CodeBase[out (Int, Int) -> Int, ⊥, ?] + -:fixme // FIXME[CY] (x, y, z) `=> x `+ y `+ z -//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+)) -//│ ║ l.62: (x, y, z) `=> x `+ y `+ z -//│ ╙── ^ -//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+)) -//│ ║ l.62: (x, y, z) `=> x `+ y `+ z -//│ ╙── ^ -//│ Type: CodeBase[out (⊤, ⊤, ⊤) -> ⊥, ⊥, ?] +//│ Type: CodeBase[out (Int, Int, Int) -> Int, ⊥, ?] f `=> x `=> y `=> f`(x, y) -//│ Type: CodeBase[out ((α97_3, α99_3) -> α100_3) -> (α97_3 -> (α99_3 -> α100_3)), ⊥, ?] +//│ Type: CodeBase[out ((x101_3, y103_3) -> α104_3) -> (x101_3 -> (y103_3 -> α104_3)), ⊥, ?] `let x = `42 `in x //│ Type: CodeBase[out Int, ⊥, ?] @@ -77,49 +60,63 @@ f `=> x `=> y `=> f`(x, y) :e `let x = 42 `in x //│ ╔══[ERROR] Type error in unquoted term -//│ ║ l.78: `let x = 42 `in x +//│ ║ l.61: `let x = 42 `in x //│ ║ ^^ -//│ ╙── because: cannot constrain Int <: CodeBase[out α122_2, out α123_2, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out α129_2, out α130_2, ?] //│ Type: CodeBase[⊥, ⊥, ?] :e `let x = `0 `in 1 //│ ╔══[ERROR] Type error in unquoted term -//│ ║ l.86: `let x = `0 `in 1 +//│ ║ l.69: `let x = `0 `in 1 //│ ║ ^ -//│ ╙── because: cannot constrain Int <: CodeBase[out α131_3, out α132_3, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out α138_3, out α139_3, ?] //│ Type: CodeBase[⊥, ⊥, ?] -:fixme + `if `true then `true else `false -//│ /!!!\ Uncaught error: scala.MatchError: IfElse(InfixApp(Unquoted(Quoted(Ident(true))),keyword 'then',Unquoted(Quoted(Ident(true)))),Unquoted(Quoted(Ident(false)))) (of class hkmc2.syntax.Tree$IfElse) +//│ Type: CodeBase[out Bool, ⊥, ?] + -:fixme x `=> `if x `== `0.0 then `1.0 else x -//│ /!!!\ Uncaught error: scala.MatchError: IfElse(InfixApp(Unquoted(Quoted(App(Ident(==),Tup(List(Unquoted(Ident(x)), Unquoted(Quoted(DecLit(0.0)))))))),keyword 'then',Unquoted(Quoted(DecLit(1.0)))),Unquoted(Ident(x))) (of class hkmc2.syntax.Tree$IfElse) +//│ Type: CodeBase[out x147_3 -> (x147_3 ∨ Num), ⊥, ?] run(`1) -//│ Type: ⊤ +//│ Type: Int + -:breakme // FIXME[CY] :e run(1) -//│ Type: ⊤ +//│ ╔══[ERROR] Type error in integer literal with expected type CodeBase[out T165_1, ⊥, ?] +//│ ║ l.91: run(1) +//│ ║ ^ +//│ ╙── because: cannot constrain Int <: CodeBase[out T165_1, ⊥, ?] +//│ Type: ⊥ :e x `=> run(x) -//│ ╔══[ERROR] Type error in unquoted term -//│ ║ l.112: x `=> run(x) -//│ ║ ^^^^^^ -//│ ╙── because: cannot constrain ⊤ <: CodeBase[out α136_3, out α137_3, ?] -//│ Type: CodeBase[out ⊤ -> ⊥, ⊥, ?] +//│ ╔══[ERROR] Type error in reference with expected type CodeBase[out T168_3, ⊥, ?] +//│ ║ l.99: x `=> run(x) +//│ ║ ^ +//│ ╟── because: cannot constrain CodeBase[x166_3, 167_3, ⊥] <: CodeBase[out T168_3, ⊥, ?] +//│ ╙── because: cannot constrain D( 167_3 ) <: ⊥ +//│ Type: CodeBase[out CodeBase[out α169_3, ?, ?] -> α169_3, out α171_2, ?] :e `let x = `42 `in run(x) +//│ ╔══[ERROR] Type error in reference with expected type CodeBase[out T175_3, ⊥, ?] +//│ ║ l.108: `let x = `42 `in run(x) +//│ ║ ^ +//│ ╟── because: cannot constrain CodeBase[α172_2, 174_3, ⊥] <: CodeBase[out T175_3, ⊥, ?] +//│ ╙── because: cannot constrain D( 174_3 ) <: ⊥ //│ ╔══[ERROR] Type error in unquoted term -//│ ║ l.120: `let x = `42 `in run(x) +//│ ║ l.108: `let x = `42 `in run(x) //│ ║ ^^^^^^ -//│ ╙── because: cannot constrain ⊤ <: CodeBase[out α142_3, out α143_3, ?] +//│ ╟── because: cannot constrain T175_3 <: CodeBase[out α176_3, out α177_3, ?] +//│ ╟── because: cannot constrain T175_3 <: ¬(~{CodeBase[out α176_3, out α177_3, ?]}) +//│ ╟── because: cannot constrain α172_2 <: ¬(~{CodeBase[out α176_3, out α177_3, ?]}) +//│ ╟── because: cannot constrain α172_2 <: CodeBase[out α178_2, out α179_2, ?] +//│ ╙── because: cannot constrain Int <: CodeBase[out α178_2, out α179_2, ?] //│ Type: CodeBase[⊥, ⊥, ?] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls index 0bb02af69..1c66e1b04 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls @@ -11,9 +11,9 @@ fun f x = f fun f(x) = f f -//│ Type: forall α0_2: ⊤ -> (⊤ -> α0_2) +//│ Type: forall f2_2: ⊤ -> (⊤ -> f2_2) //│ Where: -//│ ⊤ -> α0_2 <: α0_2 +//│ ⊤ -> f2_2 <: f2_2 fun f(x) = f(x) f @@ -38,9 +38,9 @@ Foo(123) //│ Type: ⊥ new Foo(123) -//│ Type: Foo[α12_1] +//│ Type: Foo[α14_1] //│ Where: -//│ Int <: α12_1 +//│ Int <: α14_1 :todo proper error fun f(x) = f(Foo.a(x)) @@ -51,8 +51,8 @@ fun f(x) = f(Foo.a(x)) fun f(x) = f(x.Foo#a) f -//│ Type: forall α20_2: Foo[out α20_2] -> ⊥ +//│ Type: forall x22_2: Foo[out x22_2] -> ⊥ //│ Where: -//│ α20_2 <: Foo[out α20_2] +//│ x22_2 <: Foo[out x22_2] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls index a065d4f15..7674ef08b 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls @@ -24,11 +24,13 @@ let r = region x in x.ref 42 //│ ║ ^^^^^^^^ //│ ║ l.21: !r //│ ║ ^^ -//│ ╟── because: cannot constrain (α16_1 ∨ α14_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α16_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α15_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α15_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain (α23_1 ∨ α20_1) ∨ Alloc <: Alloc +//│ ╟── because: cannot constrain α23_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α21_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α21_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ x22_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain x22_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) //│ Type: Int fun mkRef() = region x in x.ref 42 @@ -38,17 +40,23 @@ mkRef :e let t = region x in x in t.ref 42 //│ ╔══[ERROR] Type error in reference creation -//│ ║ l.39: let t = region x in x in t.ref 42 +//│ ║ l.41: let t = region x in x in t.ref 42 //│ ║ ^^^^^^^^ -//│ ╟── because: cannot constrain Region[?] <: Region[α25_1] -//│ ╟── because: cannot constrain D( ) <: α25_1 -//│ ╟── because: cannot constrain <: α25_1 +//│ ╟── because: cannot constrain Region[in x33_1 out x34_1] <: Region[α35_1] +//│ ╟── because: cannot constrain D( x34_1 ) <: α35_1 +//│ ╟── because: cannot constrain x34_1 <: α35_1 +//│ ╟── because: cannot constrain x34_1 <: ¬(~x33_1) +//│ ╟── because: cannot constrain x34_1 <: ¬(~x33_1) +//│ ╟── because: cannot constrain <: ¬(~x33_1) +//│ ╟── because: cannot constrain <: x33_1 //│ ╙── because: cannot constrain <: ¬() //│ ╔══[ERROR] Type error in block -//│ ║ l.39: let t = region x in x in t.ref 42 +//│ ║ l.41: let t = region x in x in t.ref 42 //│ ║ ^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain (α25_1 ∨ α24_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α25_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain (α35_1 ∨ α32_1) ∨ Alloc <: Alloc +//│ ╟── because: cannot constrain α35_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain x34_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain x34_1 <: ¬(~{Alloc}) //│ ╙── because: cannot constrain <: ¬(~{Alloc}) //│ Type: Ref[Int, ?] @@ -62,15 +70,17 @@ let t = region x in x.ref 42 in t := 0 //│ ╔══[ERROR] Type error in block -//│ ║ l.62: x.ref 42 +//│ ║ l.70: x.ref 42 //│ ║ ^^^^^^^^ -//│ ║ l.63: in t := 0 +//│ ║ l.71: in t := 0 //│ ║ ^^^^^^^^^ -//│ ╟── because: cannot constrain (α34_1 ∨ α32_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α34_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α33_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α33_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain (α45_1 ∨ α42_1) ∨ Alloc <: Alloc +//│ ╟── because: cannot constrain α45_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α43_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α43_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ x44_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain x44_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) //│ Type: Int @@ -83,15 +93,17 @@ let t = region x in x.ref 42 in !t //│ ╔══[ERROR] Type error in block -//│ ║ l.83: x.ref 42 +//│ ║ l.93: x.ref 42 //│ ║ ^^^^^^^^ -//│ ║ l.84: in !t +//│ ║ l.94: in !t //│ ║ ^^^^^ -//│ ╟── because: cannot constrain (α45_1 ∨ α43_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α45_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α44_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α44_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain (α57_1 ∨ α54_1) ∨ Alloc <: Alloc +//│ ╟── because: cannot constrain α57_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α55_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α55_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ x56_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain x56_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) //│ Type: Int region x in @@ -107,23 +119,23 @@ fun rid(x) = fun rid: [A] -> A -> A fun rid(x) = let t = (region y in 42) in x -//│ ╔══[ERROR] Type error in function literal with expected type (<α>61_2) ->{⊥} <α>61_2 -//│ ║ l.108: fun rid(x) = +//│ ╔══[ERROR] Type error in function literal with expected type (73_2) ->{⊥} 73_2 +//│ ║ l.120: fun rid(x) = //│ ║ ^^^^ -//│ ║ l.109: let t = (region y in 42) in x +//│ ║ l.121: let t = (region y in 42) in x //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╙── because: cannot constrain α63_2 ∨ Alloc <: ⊥ +//│ ╙── because: cannot constrain α75_2 ∨ Alloc <: ⊥ //│ Type: ⊤ :e region x in (let dz = x.ref 42 in 42): [A] -> Int -//│ ╔══[ERROR] Type error in block with expected type forall α65_3: Int -//│ ║ l.120: (let dz = x.ref 42 in 42): [A] -> Int +//│ ╔══[ERROR] Type error in block with expected type forall A77_3: Int +//│ ║ l.132: (let dz = x.ref 42 in 42): [A] -> Int //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α67_3 <: ⊥ -//│ ╟── because: cannot constrain α67_3 <: ¬() -//│ ╙── because: cannot constrain <α>64_2 <: ¬() +//│ ╟── because: cannot constrain α79_3 <: ⊥ +//│ ╟── because: cannot constrain α79_3 <: ¬() +//│ ╙── because: cannot constrain 76_2 <: ¬() //│ Type: Int @@ -133,14 +145,16 @@ let t = y => x.ref y in t(42) //│ ╔══[ERROR] Type error in block -//│ ║ l.133: y => x.ref y +//│ ║ l.145: y => x.ref y //│ ║ ^^^^^^^^^^^^ -//│ ║ l.134: in t(42) +//│ ║ l.146: in t(42) //│ ║ ^^^^^^^^ -//│ ╟── because: cannot constrain (α77_1 ∨ α72_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α77_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~{Alloc}) -//│ Type: Ref[in α74_1 out α74_1 ∨ Int, ?] +//│ ╟── because: cannot constrain (α90_1 ∨ α84_1) ∨ Alloc <: Alloc +//│ ╟── because: cannot constrain α90_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain ¬⊥ ∧ x91_1 <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain x91_1 <: ¬(~{Alloc}) +//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ Type: Ref[in y86_1 out y86_1 ∨ Int, ?] fun foo: [A] -> Int ->{A | Alloc} Int fun foo(x) = @@ -150,7 +164,7 @@ fun foo(x) = region x in x.ref ((x => x): [A] -> A -> A) -//│ Type: Ref[α89_1 -> α89_1, ?] +//│ Type: Ref[A103_1 -> A103_1, ?] fun foo: [A extends Int] -> A -> A @@ -158,23 +172,23 @@ fun foo(x) = x //│ Type: ⊤ foo -//│ Type: forall α93_2: (α93_2) ->{⊥} α93_2 +//│ Type: forall A108_2: (A108_2) ->{⊥} A108_2 //│ Where: -//│ α93_2 <: Int +//│ A108_2 <: Int region x in x.ref foo -//│ Type: Ref[in α99_1 -> (α99_1 ∧ Int) out (α99_1 ∧ Int) -> α99_1, ?] +//│ Type: Ref[in A114_1 -> (A114_1 ∧ Int) out (A114_1 ∧ Int) -> A114_1, ?] fun bar: ([A] -> A -> A) -> Int fun bar(f) = f(42) //│ Type: ⊤ bar -//│ Type: (forall α103_2: (α103_2) ->{⊥} α103_2) ->{⊥} Int +//│ Type: (forall A119_2: (A119_2) ->{⊥} A119_2) ->{⊥} Int :e region x in x.ref bar -//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall α103_2: (α103_2) ->{⊥} α103_2) ->{⊥} Int found -//│ ║ l.176: region x in x.ref bar +//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall A119_2: (A119_2) ->{⊥} A119_2) ->{⊥} Int found +//│ ║ l.190: region x in x.ref bar //│ ╙── ^^^ //│ Type: Ref[⊥, ?] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls index 59d662f63..72854c1b3 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls @@ -11,9 +11,9 @@ fun f(x) = x(x) //│ Type: ⊤ f -//│ Type: forall α7_2, α8_2, α9_2: (α7_2 ->{α8_2} α9_2) ->{α8_2} α9_2 +//│ Type: forall x9_2, α10_2, α11_2: (x9_2 ->{α10_2} α11_2) ->{α10_2} α11_2 //│ Where: -//│ α7_2 <: α7_2 ->{α8_2} α9_2 +//│ x9_2 <: x9_2 ->{α10_2} α11_2 f(f) //│ Type: ⊥ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls index c00bb1d22..8c9680a1c 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls @@ -34,7 +34,7 @@ fun mapi = s => f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out <α>23_2, out <α>24_2] +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 25_2, out 26_2] //│ ║ l.33: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.34: map(s) of x => @@ -43,13 +43,15 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.36: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out α36_2, out α37_2] <: Seq[out <α>23_2, out <α>24_2] -//│ ╟── because: cannot constrain D( α37_2 ) <: <α>24_2 -//│ ╟── because: cannot constrain α37_2 <: ¬(~<α>24_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α38_2 <: ¬(~<α>24_2) -//│ ╟── because: cannot constrain α38_2 <: ¬(~<α>24_2) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~<α>24_2) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out <α>23_2, out <α>24_2] +//│ ╟── because: cannot constrain Seq[out B38_2, out E39_2] <: Seq[out 25_2, out 26_2] +//│ ╟── because: cannot constrain D( E39_2 ) <: 26_2 +//│ ╟── because: cannot constrain E39_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α40_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain α40_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r41_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain r41_2 <: ¬(~26_2) +//│ ╙── because: cannot constrain <: ¬(~26_2) +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 25_2, out 26_2] //│ ║ l.33: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.34: map(s) of x => @@ -58,13 +60,15 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.36: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out α36_2, out α37_2] <: Seq[out <α>23_2, out <α>24_2] -//│ ╟── because: cannot constrain D( α37_2 ) <: <α>24_2 -//│ ╟── because: cannot constrain α37_2 <: ¬(~<α>24_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α38_2 <: ¬(~<α>24_2) -//│ ╟── because: cannot constrain α38_2 <: ¬(~<α>24_2) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~<α>24_2) -//│ ╔══[ERROR] Type error in region expression with expected type Seq[out <α>23_2, out <α>24_2] +//│ ╟── because: cannot constrain Seq[out B38_2, out E39_2] <: Seq[out 25_2, out 26_2] +//│ ╟── because: cannot constrain D( E39_2 ) <: 26_2 +//│ ╟── because: cannot constrain E39_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α40_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain α40_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r41_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain r41_2 <: ¬(~26_2) +//│ ╙── because: cannot constrain <: ¬(~26_2) +//│ ╔══[ERROR] Type error in region expression with expected type Seq[out 25_2, out 26_2] //│ ║ l.33: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.34: map(s) of x => @@ -73,12 +77,14 @@ fun mapi = s => f => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.36: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain Seq[out α36_2, out α37_2] <: Seq[out <α>23_2, out <α>24_2] -//│ ╟── because: cannot constrain D( α37_2 ) <: <α>24_2 -//│ ╟── because: cannot constrain α37_2 <: ¬(~<α>24_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α38_2 <: ¬(~<α>24_2) -//│ ╟── because: cannot constrain α38_2 <: ¬(~<α>24_2) -//│ ╙── because: cannot constrain ¬⊥ <: ¬(~<α>24_2) +//│ ╟── because: cannot constrain Seq[out B38_2, out E39_2] <: Seq[out 25_2, out 26_2] +//│ ╟── because: cannot constrain D( E39_2 ) <: 26_2 +//│ ╟── because: cannot constrain E39_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α40_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain α40_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r41_2 <: ¬(~26_2) +//│ ╟── because: cannot constrain r41_2 <: ¬(~26_2) +//│ ╙── because: cannot constrain <: ¬(~26_2) //│ Type: ⊤ // * Notice the inferred type, which produces an unusable Sequence (of effect `?` ie `Any`) @@ -89,7 +95,7 @@ fun mapi = s => f => i := !i + 1 f(!i, x) mapi -//│ Type: forall α47_2, α48_2, α58_2, α59_2: Seq[out α47_2, out α48_2] -> (((Int, α47_2) ->{α59_2} α58_2) ->{Alloc} Seq[out α58_2, ?]) +//│ Type: forall A50_2, E51_2, α61_2, α62_2: Seq[out A50_2, out E51_2] -> (((Int, A50_2) ->{α62_2} α61_2) ->{Alloc} Seq[out α61_2, ?]) // * 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) ->{Alloc | E} Seq[out A, Nothing] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSyntax.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSyntax.mls index 6667f46d6..0f8619159 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSyntax.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSyntax.mls @@ -186,7 +186,7 @@ g`(`1, `2) `if x `== `0.0 then `1.0 else x //│ Parsed: -//│ Quoted(IfElse(InfixApp(Unquoted(Quoted(App(Ident(==),Tup(List(Unquoted(Ident(x)), Unquoted(Quoted(DecLit(0.0)))))))),keyword 'then',Unquoted(Quoted(DecLit(1.0)))),Unquoted(Ident(x)))) +//│ Quoted(IfLike(keyword 'if',Block(List(InfixApp(Unquoted(Quoted(App(Ident(==),Tup(List(Unquoted(Ident(x)), Unquoted(Quoted(DecLit(0.0)))))))),keyword 'then',Unquoted(Quoted(DecLit(1.0)))), Modified(keyword 'else',None,Unquoted(Ident(x))))))) x `=> if 0 == 0 then x else `0