From c08d1e71d66ba552e9e0f8a3dc68420ad21c8778 Mon Sep 17 00:00:00 2001 From: Meowcolm024 Date: Tue, 9 Apr 2024 18:46:47 +0800 Subject: [PATCH 1/2] fix type selection --- .../scala/mlscript/compiler/ClassLifter.scala | 2 +- .../scala/mlscript/ConstraintSolver.scala | 29 +- shared/src/main/scala/mlscript/NewLexer.scala | 5 +- .../src/main/scala/mlscript/NewParser.scala | 51 ++- .../src/main/scala/mlscript/NuTypeDefs.scala | 38 +- shared/src/main/scala/mlscript/TypeDefs.scala | 11 +- .../main/scala/mlscript/TypeSimplifier.scala | 6 +- shared/src/main/scala/mlscript/Typer.scala | 81 +++- .../main/scala/mlscript/TyperHelpers.scala | 6 +- shared/src/main/scala/mlscript/helpers.scala | 21 + shared/src/main/scala/mlscript/syntax.scala | 7 +- .../main/scala/mlscript/ucs/Desugarer.scala | 36 +- .../diff/codegen/AuxiliaryConstructors.mls | 4 +- .../src/test/diff/codegen/FieldOverride.mls | 2 +- .../test/diff/codegen/IndirectRecursion.mls | 8 +- shared/src/test/diff/codegen/Mixin.mls | 11 +- shared/src/test/diff/codegen/MixinCapture.mls | 2 +- shared/src/test/diff/codegen/Nested.mls | 30 +- shared/src/test/diff/codegen/NewMatching.mls | 25 +- shared/src/test/diff/fcp-lit/Leijen.mls | 2 +- .../test/diff/fcp-lit/variations_PolyML.mls | 2 +- shared/src/test/diff/fcp/Church_CT.mls | 14 +- shared/src/test/diff/fcp/FunnyId.mls | 12 +- shared/src/test/diff/fcp/ListBuild.mls | 2 +- shared/src/test/diff/fcp/NestedDataTypes.mls | 2 +- shared/src/test/diff/fcp/Paper.mls | 2 +- shared/src/test/diff/fcp/PaperTable.mls | 6 +- shared/src/test/diff/fcp/SystemF_2.mls | 18 +- .../src/test/diff/fcp/ToChurchSimplif_CT.mls | 6 +- shared/src/test/diff/gadt/Exp1.mls | 5 +- shared/src/test/diff/gadt/ThisMatching.mls | 37 +- shared/src/test/diff/mlf-examples/ex_demo.mls | 10 +- .../test/diff/mlf-examples/ex_predicative.mls | 32 +- .../src/test/diff/mlf-examples/ex_selfapp.mls | 10 +- shared/src/test/diff/mlscript/OccursCheck.mls | 2 +- shared/src/test/diff/mlscript/Scratch.mls | 6 + shared/src/test/diff/nu/AsOp.mls | 64 +++ shared/src/test/diff/nu/BasicClasses.mls | 73 ++- shared/src/test/diff/nu/CaseExpr.mls | 43 +- shared/src/test/diff/nu/ClassesInMixins.mls | 2 +- shared/src/test/diff/nu/Eval.mls | 4 +- shared/src/test/diff/nu/GADTMono.mls | 147 ++---- .../diff/nu/InferredInheritanceTypeArgs.mls | 20 +- shared/src/test/diff/nu/Lifted.mls | 78 ++++ shared/src/test/diff/nu/ListConsNil.mls | 2 +- shared/src/test/diff/nu/Metaprog.mls | 2 +- shared/src/test/diff/nu/MethodSignatures.mls | 24 +- shared/src/test/diff/nu/NestedClasses.mls | 6 +- shared/src/test/diff/nu/NewNew.mls | 2 +- shared/src/test/diff/nu/NuScratch.mls | 289 ++++++++++++ shared/src/test/diff/nu/NuScratch2.mls | 243 ++++++++++ shared/src/test/diff/nu/NuScratch3.mls | 19 + shared/src/test/diff/nu/NuScratch4.mls | 185 ++++++++ shared/src/test/diff/nu/Parens.mls | 4 +- shared/src/test/diff/nu/RawTypes.mls | 150 ++++++ .../test/diff/nu/RawUnionTraitSignatures.mls | 49 +- shared/src/test/diff/nu/TODO_Classes.mls | 33 +- shared/src/test/diff/nu/TypeMemberBounds.mls | 110 +++++ shared/src/test/diff/nu/TypeMembers.mls | 113 +++++ shared/src/test/diff/nu/TypeSel.mls | 431 ++++++++++++++++++ shared/src/test/diff/nu/TypeSelections.mls | 10 +- shared/src/test/diff/nu/TypeVariables.mls | 2 +- shared/src/test/diff/nu/TypreMembers.mls | 30 -- shared/src/test/diff/nu/WeirdUnions.mls | 4 +- shared/src/test/diff/nu/repro_EvalNegNeg.mls | 2 +- shared/src/test/diff/parser/IfThenElse.mls | 4 +- shared/src/test/diff/tapl/NuSimplyTyped.mls | 2 + shared/src/test/diff/tapl/NuUntyped.mls | 18 +- 68 files changed, 2253 insertions(+), 455 deletions(-) create mode 100644 shared/src/test/diff/nu/AsOp.mls create mode 100644 shared/src/test/diff/nu/Lifted.mls create mode 100644 shared/src/test/diff/nu/NuScratch2.mls create mode 100644 shared/src/test/diff/nu/NuScratch3.mls create mode 100644 shared/src/test/diff/nu/NuScratch4.mls create mode 100644 shared/src/test/diff/nu/RawTypes.mls create mode 100644 shared/src/test/diff/nu/TypeMemberBounds.mls create mode 100644 shared/src/test/diff/nu/TypeMembers.mls create mode 100644 shared/src/test/diff/nu/TypeSel.mls delete mode 100644 shared/src/test/diff/nu/TypreMembers.mls diff --git a/compiler/shared/main/scala/mlscript/compiler/ClassLifter.scala b/compiler/shared/main/scala/mlscript/compiler/ClassLifter.scala index 9caa97158d..149ac49254 100644 --- a/compiler/shared/main/scala/mlscript/compiler/ClassLifter.scala +++ b/compiler/shared/main/scala/mlscript/compiler/ClassLifter.scala @@ -747,7 +747,7 @@ class ClassLifter(logDebugMsg: Boolean = false) { val nTerms = termList.map(liftTerm(_)(using emptyCtx, nCache, globFuncs, nOuter)).unzip clsList.foreach(x => liftTypeDef(x)(using nCache, globFuncs, nOuter)) retSeq = retSeq.appended(NuTypeDef( - kind, nName, nTps.map((None, _)), kind match + kind, nName, nTps.map((TypeParamInfo(None, false, N, N), _)), kind match case Mod => None case _ => S(Tup(nParams)) , None, None, nPars._1, None, None, TypingUnit(nFuncs._1 ++ nTerms._1))(None, None, Nil)) diff --git a/shared/src/main/scala/mlscript/ConstraintSolver.scala b/shared/src/main/scala/mlscript/ConstraintSolver.scala index 54b7e91210..9d6ee7aade 100644 --- a/shared/src/main/scala/mlscript/ConstraintSolver.scala +++ b/shared/src/main/scala/mlscript/ConstraintSolver.scala @@ -29,12 +29,9 @@ class ConstraintSolver extends NormalForms { self: Typer => ErrorReport( msg"${info.decl.kind.str.capitalize} `${info.decl.name}` does not contain member `${fld.name}`" -> fld.toLoc :: Nil, newDefs) - def lookupMember(clsNme: Str, rfnt: Var => Opt[FieldType], fld: Var) - (implicit ctx: Ctx, raise: Raise) + def lookupMember(clsNme: Str, rfnt: Var => Opt[FieldType], fld: Var)(implicit ctx: Ctx, raise: Raise) : Either[Diagnostic, NuMember] - = { - val info = ctx.tyDefs2.getOrElse(clsNme, ???/*TODO*/) - + = ctx.tyDefs2.get(clsNme).toRight(ErrorReport(msg"Cannot find class ${clsNme}" -> N :: Nil, newDefs)) flatMap { info => if (info.isComputing) { ??? // TODO support? @@ -109,7 +106,7 @@ class ConstraintSolver extends NormalForms { self: Typer => Nil) S(p.ty) case S(m) => - S(err(msg"Access to ${m.kind.str} member not yet supported", fld.toLoc).toUpper(noProv)) + S(err(msg"Access to ${m.kind.str} member ${fld.name} not yet supported", fld.toLoc).toUpper(noProv)) case N => N } @@ -131,17 +128,20 @@ class ConstraintSolver extends NormalForms { self: Typer => implicit val shadows: Shadows = Shadows.empty info.tparams.foreach { case (tn, _tv, vi) => - val targ = rfnt(Var(info.decl.name + "#" + tn.name)) match { + val targ = rfnt(tparamField(TypeName(info.decl.name), tn, vi.visible)) match { // * TODO to avoid infinite recursion due to ever-expanding type args, // * we should set the shadows of the targ to be the same as that of the parameter it replaces... - case S(fty) if vi === S(VarianceInfo.co) => fty.ub - case S(fty) if vi === S(VarianceInfo.contra) => fty.lb.getOrElse(BotType) + case S(fty) if vi.varinfo === S(VarianceInfo.co) => + println(s"Lookup: Found $fty") + fty.ub + case S(fty) if vi.varinfo === S(VarianceInfo.contra) => + println(s"Lookup: Found $fty") + fty.lb.getOrElse(BotType) case S(fty) => - TypeBounds.mk( - fty.lb.getOrElse(BotType), - fty.ub, - ) + println(s"Lookup: Found $fty") + TypeBounds.mk(fty.lb.getOrElse(BotType), fty.ub) case N => + println(s"Lookup: field not found, creating new bounds") TypeBounds( // _tv.lowerBounds.foldLeft(BotType: ST)(_ | _), // _tv.upperBounds.foldLeft(TopType: ST)(_ & _), @@ -192,6 +192,9 @@ class ConstraintSolver extends NormalForms { self: Typer => }() + private val DummyTV: TV = freshVar(noProv, N, S(""), Nil, Nil, false)(-1) + + // * Each type has a shadow which identifies all variables created from copying // * variables that existed at the start of constraining. // * The intent is to make the total number of shadows in a given constraint diff --git a/shared/src/main/scala/mlscript/NewLexer.scala b/shared/src/main/scala/mlscript/NewLexer.scala index 0c6bc7d8e7..fbb27e408d 100644 --- a/shared/src/main/scala/mlscript/NewLexer.scala +++ b/shared/src/main/scala/mlscript/NewLexer.scala @@ -464,7 +464,7 @@ object NewLexer { "val", "var", // "is", - // "as", + "as", "of", // "and", // "or", @@ -498,7 +498,8 @@ object NewLexer { "undefined", "abstract", "constructor", - "virtual" + "virtual", + "restricts", ) def printToken(tl: TokLoc): Str = tl match { diff --git a/shared/src/main/scala/mlscript/NewParser.scala b/shared/src/main/scala/mlscript/NewParser.scala index a7837178e4..b77906319f 100644 --- a/shared/src/main/scala/mlscript/NewParser.scala +++ b/shared/src/main/scala/mlscript/NewParser.scala @@ -770,6 +770,9 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo case (KEYWORD("super"), l0) :: _ => consume exprCont(Super().withLoc(S(l0)), prec, allowNewlines = false) + case (IDENT("?", true), l0) :: _ => + consume + exprCont(Var("?").withLoc(S(l0)), prec, allowNewlines = false) case (IDENT("~", _), l0) :: _ => consume val rest = expr(prec, allowSpace = true) @@ -1080,7 +1083,7 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo else App(App(v, PlainTup(acc)), PlainTup(rhs)) }, prec, allowNewlines) } - case (KEYWORD(":"), l0) :: _ if prec <= NewParser.prec(':') => + case (KEYWORD("as" | ":"), l0) :: _ if prec <= NewParser.prec(':') => consume R(Asc(acc, typ(0))) case (KEYWORD("where"), l0) :: _ if prec <= 1 => @@ -1278,35 +1281,59 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo } // TODO support line-broken param lists; share logic with args/argsOrIf - def typeParams(implicit fe: FoundErr, et: ExpectThen): Ls[(Opt[VarianceInfo], TypeName)] = { + def typeParams(implicit fe: FoundErr, et: ExpectThen): Ls[(TypeParamInfo, TypeName)] = { + val visinfo = yeetSpaces match { + case (KEYWORD("type"), l0) :: _ => + consume + S(l0) + case _ => N + } val vinfo = yeetSpaces match { case (KEYWORD("in"), l0) :: (KEYWORD("out"), l1) :: _ => consume - S(VarianceInfo.in, l0 ++ l1) + S(VarianceInfo.in -> (l0++l1)) case (KEYWORD("in"), l0) :: _ => consume - S(VarianceInfo.contra, l0) + S(VarianceInfo.contra -> l0) case (KEYWORD("out"), l0) :: _ => consume - S(VarianceInfo.co, l0) - case _ => N + S(VarianceInfo.co -> l0) + case _ => + N } yeetSpaces match { case (IDENT(nme, false), l0) :: _ => consume val tyNme = TypeName(nme).withLoc(S(l0)) + + @inline def getTypeName(kw: String) = yeetSpaces match { + case (KEYWORD(k), l0) :: _ if k === kw => consume + yeetSpaces match { + case (IDENT(nme, false), l1) :: _ => + consume; S(TypeName(nme).withLoc(S(l1))) + case _ => err(msg"dangling $kw keyword" -> S(l0) :: Nil); N + } + case _ => N + } + val lb = getTypeName("restricts") + val ub = getTypeName("extends") + // TODO update `TypeParamInfo` to use lb and ub yeetSpaces match { case (COMMA, l0) :: _ => consume - vinfo.map(_._1) -> tyNme :: typeParams + TypeParamInfo(vinfo.map(_._1), visinfo.isDefined, lb, ub) -> tyNme :: typeParams case _ => - vinfo.map(_._1) -> tyNme :: Nil + TypeParamInfo(vinfo.map(_._1), visinfo.isDefined, lb, ub) -> tyNme :: Nil } case _ => - vinfo match { - case S((_, loc)) => + (visinfo, vinfo) match { + case (S(l1), S(_ -> l2)) => + err(msg"dangling type member and variance information" -> S(l1 ++ l2) :: Nil) + case (_, S(_ -> loc)) => err(msg"dangling variance information" -> S(loc) :: Nil) - case N => + case (S(loc), _) => + err(msg"dangling visible type member" -> S(loc) :: Nil) + case (N, N) => } Nil } @@ -1373,7 +1400,7 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo case (NEWLINE, _) :: _ => // TODO: | ... assert(seqAcc.isEmpty) acc.reverse - case (IDENT(nme, true), _) :: _ if nme =/= "-" => // TODO: | ... + case (IDENT(nme, true), _) :: _ if nme =/= "-" && nme =/= "?" => // TODO: | ... assert(seqAcc.isEmpty) acc.reverse case _ => diff --git a/shared/src/main/scala/mlscript/NuTypeDefs.scala b/shared/src/main/scala/mlscript/NuTypeDefs.scala index 0ce7f326c5..40fdffd278 100644 --- a/shared/src/main/scala/mlscript/NuTypeDefs.scala +++ b/shared/src/main/scala/mlscript/NuTypeDefs.scala @@ -13,7 +13,7 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => type Params = Ls[Var -> FieldType] - type TyParams = Ls[(TN, TV, Opt[VarianceInfo])] + type TyParams = Ls[(TN, TV, TypeParamInfo)] sealed abstract class NuDeclInfo @@ -174,8 +174,9 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => // TODO dedup with the one in TypedNuCls lazy val virtualMembers: Map[Str, NuMember] = members ++ tparams.map { - case (nme @ TypeName(name), tv, _) => - td.nme.name+"#"+name -> NuParam(nme, FieldType(S(tv), tv)(provTODO), isPublic = true)(level) + case (nme @ TypeName(name), tv, TypeParamInfo(_, v, _, _)) => + tparamField(td.nme, nme, v).name -> + NuParam(nme, FieldType(S(tv), tv)(provTODO), isPublic = true)(level) } ++ parentTP def freshenAbove(lim: Int, rigidify: Bool) @@ -239,8 +240,8 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => /** Includes class-name-coded type parameter fields. */ lazy val virtualMembers: Map[Str, NuMember] = members ++ tparams.map { - case (nme @ TypeName(name), tv, _) => - td.nme.name+"#"+name -> NuParam(nme, FieldType(S(tv), tv)(provTODO), isPublic = true)(level) + case (nme @ TypeName(name), tv, TypeParamInfo(_, v, _, _)) => + tparamField(td.nme, nme, v).name -> NuParam(nme, FieldType(S(tv), tv)(provTODO), isPublic = true)(level) } ++ parentTP // TODO @@ -283,7 +284,7 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => } // TODO check consistency with explicitVariances - val res = store ++ tparams.iterator.collect { case (_, tv, S(vi)) => tv -> vi } + val res = store ++ tparams.iterator.collect { case (_, tv, TypeParamInfo(S(vi), _, _, _)) => tv -> vi } _variances = S(res) @@ -356,9 +357,9 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => def isPublic = true // TODO lazy val virtualMembers: Map[Str, NuMember] = members ++ tparams.map { - case (nme @ TypeName(name), tv, _) => - td.nme.name+"#"+name -> NuParam(nme, FieldType(S(tv), tv)(provTODO), isPublic = false)(level) - } + case (nme @ TypeName(name), tv, TypeParamInfo(_, v, _, _)) => + tparamField(td.nme, nme, v).name -> NuParam(nme, FieldType(S(tv), tv)(provTODO), isPublic = false)(level) + } def freshenAbove(lim: Int, rigidify: Bool) (implicit ctx: Ctx, freshened: MutMap[TV,ST]) @@ -929,19 +930,23 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => lazy val tparams: TyParams = ctx.nest.nextLevel { implicit ctx => decl match { case td: NuTypeDef => - td.tparams.map(tp => - (tp._2, freshVar( + td.tparams.map(tp => { + val fv = freshVar( TypeProvenance(tp._2.toLoc, "type parameter", S(tp._2.name), isType = true), - N, S(tp._2.name)), tp._1)) + N, S(tp._2.name)) + // TODO assign the correct bounds (`typeType` causes cycle) + // fv.lowerBounds = tp._1.lb.toList.map(TypeRef(_, Nil)(provTODO)) + // fv.upperBounds = tp._1.ub.toList.map(TypeRef(_, Nil)(provTODO)) + (tp._2, fv, tp._1) }) case fd: NuFunDef => fd.tparams.map { tn => (tn, freshVar( TypeProvenance(tn.toLoc, "method type parameter", originName = S(tn.name), isType = true), - N, S(tn.name)), N) + N, S(tn.name)), TypeParamInfo(N, false, N, N)) } } } @@ -950,7 +955,7 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => } lazy val explicitVariances: VarianceStore = - MutMap.from(tparams.iterator.map(tp => tp._2 -> tp._3.getOrElse(VarianceInfo.in))) + MutMap.from(tparams.iterator.map(tp => tp._2 -> tp._3.varinfo.getOrElse(VarianceInfo.in))) def varianceOf(tv: TV)(implicit ctx: Ctx): VarianceInfo = // TODO make use of inferred vce if result is completed @@ -1541,7 +1546,7 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => val finalType = thisTV val tparamMems = tparams.map { case (tp, tv, vi) => // TODO use vi - val fldNme = td.nme.name + "#" + tp.name + val fldNme = tparamField(td.nme.name, tp.name, vi.visible) val skol = SkolemTag(tv)(tv.prov) NuParam(TypeName(fldNme).withLocOf(tp), FieldType(S(skol), skol)(tv.prov), isPublic = true)(lvl) } @@ -1921,7 +1926,8 @@ class NuTypeDefs extends ConstraintSolver { self: Typer => tv }) freshened += _tv -> tv - rawName+"#"+tn.name -> NuParam(tn, FieldType(S(tv), tv)(provTODO), isPublic = true)(ctx.lvl) + tparamField(rawName, tn.name, vi.visible) -> + NuParam(tn, FieldType(S(tv), tv)(provTODO), isPublic = true)(ctx.lvl) } freshened -> parTP.toMap diff --git a/shared/src/main/scala/mlscript/TypeDefs.scala b/shared/src/main/scala/mlscript/TypeDefs.scala index a33177486b..26623020cf 100644 --- a/shared/src/main/scala/mlscript/TypeDefs.scala +++ b/shared/src/main/scala/mlscript/TypeDefs.scala @@ -110,9 +110,11 @@ class TypeDefs extends NuTypeDefs { Typer: Typer => } } - - def tparamField(clsNme: TypeName, tparamNme: TypeName): Var = - Var(clsNme.name + "#" + tparamNme.name) + def tparamField(clsNme: TypeName, tparamNme: TypeName, visible: Bool): Var = + Var(tparamField(clsNme.name, tparamNme.name, visible)) + + def tparamField(clsNme: String, tparamNme: String, visible: Bool): String = + if (!visible) clsNme + "#" + tparamNme else tparamNme def clsNameToNomTag(td: NuTypeDef)(prov: TypeProvenance, ctx: Ctx): ClassTag = { require((td.kind is Cls) || (td.kind is Mod), td.kind) @@ -343,7 +345,8 @@ class TypeDefs extends NuTypeDefs { Typer: Typer => case _ => val fields = fieldsOf(td.bodyTy, paramTags = true) val tparamTags = td.tparamsargs.map { case (tp, tv) => - tparamField(td.nme, tp) -> FieldType(Some(tv), tv)(tv.prov) } + // `false` means using `C#A` (old type member names) + tparamField(td.nme, tp, false) -> FieldType(Some(tv), tv)(tv.prov) } val ctor = k match { case Cls => val nomTag = clsNameToNomTag(td)(originProv(td.nme.toLoc, "class", td.nme.name), ctx) diff --git a/shared/src/main/scala/mlscript/TypeSimplifier.scala b/shared/src/main/scala/mlscript/TypeSimplifier.scala index f444498dad..c7ba75b1ae 100644 --- a/shared/src/main/scala/mlscript/TypeSimplifier.scala +++ b/shared/src/main/scala/mlscript/TypeSimplifier.scala @@ -127,7 +127,7 @@ trait TypeSimplifier { self: Typer => else v -> default :: Nil } case S(trt: TypedNuTrt) => // TODO factor w/ above & generalize - trt.tparams.iterator.find(_._1.name === postfix).flatMap(_._3).getOrElse(VarianceInfo.in) match { + trt.tparams.iterator.find(_._1.name === postfix).flatMap(_._3.varinfo).getOrElse(VarianceInfo.in) match { case VarianceInfo(true, true) => Nil case VarianceInfo(co, contra) => if (co) v -> FieldType(S(BotType), process(fty.ub, N))(fty.prov) :: Nil @@ -248,7 +248,7 @@ trait TypeSimplifier { self: Typer => // * Reconstruct a TypeRef from its current structural components val typeRef = TypeRef(td.nme, td.tparamsargs.zipWithIndex.map { case ((tp, tv), tpidx) => - val fieldTagNme = tparamField(clsTyNme, tp) + val fieldTagNme = tparamField(clsTyNme, tp, false) val fromTyRef = trs2.get(clsTyNme).map(_.targs(tpidx) |> { ta => FieldType(S(ta), ta)(noProv) }) fromTyRef.++(rcd2.fields.iterator.filter(_._1 === fieldTagNme).map(_._2)) .foldLeft((BotType: ST, TopType: ST)) { @@ -358,7 +358,7 @@ trait TypeSimplifier { self: Typer => // * Reconstruct a TypeRef from its current structural components val typeRef = TypeRef(cls.td.nme, cls.tparams.zipWithIndex.map { case ((tp, tv, vi), tpidx) => - val fieldTagNme = tparamField(clsTyNme, tp) + val fieldTagNme = tparamField(clsTyNme, tp, vi.visible) val fromTyRef = trs2.get(clsTyNme).map(_.targs(tpidx) |> { ta => FieldType(S(ta), ta)(noProv) }) fromTyRef.++(rcd2.fields.iterator.filter(_._1 === fieldTagNme).map(_._2)) .foldLeft((BotType: ST, TopType: ST)) { diff --git a/shared/src/main/scala/mlscript/Typer.scala b/shared/src/main/scala/mlscript/Typer.scala index c3d03f82b5..cdd668da62 100644 --- a/shared/src/main/scala/mlscript/Typer.scala +++ b/shared/src/main/scala/mlscript/Typer.scala @@ -287,10 +287,11 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne "anything" -> TopType, "nothing" -> BotType) private val preludeLoc = Loc(0, 0, Origin("", 0, new FastParseHelpers(""))) + // private val DummyTV: TV = freshVar() val nuBuiltinTypes: Ls[NuTypeDef] = Ls( NuTypeDef(Cls, TN("Object"), Nil, N, N, N, Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), - NuTypeDef(Trt, TN("Eql"), (S(VarianceInfo.contra), TN("A")) :: Nil, N, N, N, Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), + NuTypeDef(Trt, TN("Eql"), (TypeParamInfo(S(VarianceInfo.contra), false, N, N), TN("A")) :: Nil, N, N, N, Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), NuTypeDef(Cls, TN("Num"), Nil, N, N, N, Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), NuTypeDef(Cls, TN("Int"), Nil, N, N, N, Var("Num") :: Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), NuTypeDef(Cls, TN("Bool"), Nil, N, N, S(Union(TN("true"), TN("false"))), Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), @@ -300,13 +301,13 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne NuTypeDef(Als, TN("undefined"), Nil, N, N, S(Literal(UnitLit(true))), Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), NuTypeDef(Als, TN("null"), Nil, N, N, S(Literal(UnitLit(false))), Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), NuTypeDef(Cls, TN("Annotation"), Nil, N, N, N, Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), - NuTypeDef(Cls, TN("Code"), (S(VarianceInfo.co) -> TN("T")) :: (S(VarianceInfo.co) -> TN("C")) :: Nil, N, N, N, Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), - NuTypeDef(Cls, TN("Var"), (S(VarianceInfo.in) -> TN("T")) :: (S(VarianceInfo.in) -> TN("C")) :: Nil, N, N, N, TyApp(Var("Code"), TN("T") :: TN("C") :: Nil) :: Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil) + NuTypeDef(Cls, TN("Code"), (TypeParamInfo(S(VarianceInfo.co), false, N, N) -> TN("T")) :: (TypeParamInfo(S(VarianceInfo.co), false, N, N) -> TN("C")) :: Nil, N, N, N, Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil), + NuTypeDef(Cls, TN("Var"), (TypeParamInfo(S(VarianceInfo.in), false, N, N) -> TN("T")) :: (TypeParamInfo(S(VarianceInfo.in), false, N, N) -> TN("C")) :: Nil, N, N, N, TyApp(Var("Code"), TN("T") :: TN("C") :: Nil) :: Nil, N, N, TypingUnit(Nil))(N, S(preludeLoc), Nil) // Not yet implemented, so we do not define it yet // NuTypeDef(Mod, TN("tailrec"), Nil, N, N, N, Var("Annotation") :: Nil, N, N, TypingUnit(Nil))(N, N, Nil), ) val builtinTypes: Ls[TypeDef] = - TypeDef(Cls, TN("?"), Nil, TopType, Nil, Nil, Set.empty, N, Nil) :: // * Dummy for pretty-printing unknown type locations + // TypeDef(Cls, TN("?"), Nil, TopType, Nil, Nil, Set.empty, N, Nil) :: // * Dummy for pretty-printing unknown type locations TypeDef(Cls, TN("int"), Nil, TopType, Nil, Nil, sing(TN("number")), N, Nil) :: TypeDef(Cls, TN("number"), Nil, TopType, Nil, Nil, semp, N, Nil) :: TypeDef(Cls, TN("bool"), Nil, TopType, Nil, Nil, semp, N, Nil) :: @@ -343,7 +344,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne val primitiveTypes: Set[Str] = builtinTypes.iterator.map(_.nme.name).flatMap(n => n.decapitalize :: n.capitalize :: Nil).toSet + "Object" + "Num" + "Str" - val reservedTypeNames: Set[Str] = primitiveTypes + "Eql" + val reservedTypeNames: Set[Str] = primitiveTypes + "Eql" + "?" def singleTup(ty: ST): ST = if (funkyTuples) ty else TupleType((N, ty.toUpper(ty.prov) ) :: Nil)(noProv) def pair(ty1: ST, ty2: ST): ST = @@ -486,7 +487,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne case Cls | Mod | Als | Trt => () case _ => err(msg"${k.str} ${nme} cannot be used as a type", loc); () } - def typeNamed(loc: Opt[Loc], name: Str): (() => ST) \/ (TypeDefKind, Int) = + def typeNamed(loc: Opt[Loc], name: Str, lift: Bool): (() => ST) \/ (TypeDefKind, Int) = newDefsInfo.get(name) .orElse(ctx.tyDefs.get(name).map(td => (td.kind, td.tparamsargs.size))) .orElse(ctx.get(name).flatMap { @@ -503,9 +504,24 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne case fd: NuFunDef => N } - case _ => N + case _ => + N }) - .toRight(() => err("type identifier not found: " + name, loc)(raise)) + .toRight(ctx.get(name) match { + case Some(VarSymbol(ty, vr)) => () => if (lift) { + println(s"ty var: $vr : $ty") // select type from variable + ty + } else err( + (msg"cannot lift variable $name to type" -> loc) :: + ty.prov.loco.toList.map(_ => (msg"as defined in" -> ty.prov.loco)) + )(raise) + case Some(CompletedTypeInfo(ty@TypedNuFun(_,_,_))) => () => if (lift) + ty.typeSignature + else err( + (msg"cannot lift expression $name to type" -> loc) :: + ty.toLoc.toList.map(_ => (msg"as defined in" -> ty.toLoc)) + )(raise) + case r => () => err(s"type identifier not found: " + name, loc)(raise) }) val localVars = mutable.Map.empty[TypeVar, TypeVariable] def tyTp(loco: Opt[Loc], desc: Str, originName: Opt[Str] = N) = TypeProvenance(loco, desc, originName, isType = true) @@ -575,11 +591,12 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne } case tn @ TypeTag(name) => rec(TypeName(name.decapitalize)) // TODO rm this hack // case tn @ TypeTag(name) => rec(TypeName(name)) + case wc @ TypeName("?") => err(msg"Invalid use of wildcard type `?` here", wc.toLoc) case tn @ TypeName(name) => val tyLoc = ty.toLoc val tpr = tyTp(tyLoc, "type reference") vars.getOrElse(name, { - typeNamed(tyLoc, name) match { + typeNamed(tyLoc, name, true) match { case R((_, tpnum)) => if (tpnum === 0) TypeRef(tn, Nil)(tpr) else ctx.tyDefs2.get(name) match { @@ -597,7 +614,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne } case L(e) => if (name.isEmpty || !name.head.isLower) e() - else (typeNamed(tyLoc, name.capitalize), ctx.tyDefs.get(name.capitalize)) match { + else (typeNamed(tyLoc, name.capitalize, false), ctx.tyDefs.get(name.capitalize)) match { case (R((kind, _)), S(td)) => kind match { case Cls => clsNameToNomTag(td)(tyTp(tyLoc, "class tag"), ctx) case Trt => trtNameToNomTag(td)(tyTp(tyLoc, "trait tag"), ctx) @@ -620,9 +637,15 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne } case AppliedType(base, targs) => val prov = tyTp(ty.toLoc, "applied type reference") - typeNamed(ty.toLoc, base.name) match { + typeNamed(ty.toLoc, base.name, false) match { case R((_, tpnum)) => - val realTargs = if (targs.size === tpnum) targs.map(rec) else { + val realTargs = if (targs.size === tpnum) targs.map{ + // case b@Bounds(lb, ub) if newDefs => WildcardArg(rec(lb), rec(ub))(tyTp(b.toLoc, "wildcard")) + // case w@TypeName("?") if newDefs => + // val prov: TypeProvenance = tyTp(w.toLoc, "wildcard") + // WildcardArg(ExtrType(true)(prov), ExtrType(false)(prov))(prov) + case ty => rec(ty) + } else { err(msg"Wrong number of type arguments – expected ${tpnum.toString}, found ${ targs.size.toString}", ty.toLoc)(raise) (targs.iterator.map(rec) ++ Iterator.continually(freshVar(noProv, N))).take(tpnum).toList @@ -632,11 +655,18 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne } case Selection(base, nme) => implicit val gl: GenLambdas = false - // val base_ty = typeTerm(base) val base_ty = rec(base) + def constrTB(ty: ST): TypeBounds = { + implicit val prov: TypeProvenance = tyTp(nme.toLoc, "type selection") + val lb = freshVar(prov, N, S(nme.name)) + val ub = freshVar(prov, N, S(nme.name)) + val res = RecordType.mk((nme.toVar, FieldType(S(lb), ub)(prov)) :: Nil)(prov) + println(s"Type selection : ${ty} <=< ${res}") + constrain(ty, res) + TypeBounds(lb, ub)(prov) + } def go(b_ty: ST, rfnt: Var => Opt[FieldType]): ST = b_ty.unwrapAll match { - case ct: TypeRef => die // TODO actually - case ClassTag(Var(clsNme), _) => + case ct@ClassTag(Var(clsNme), _) => // TODO we should still succeed even if the member is not completed... lookupMember(clsNme, rfnt, nme.toVar) match { case R(cls: TypedNuCls) => @@ -645,11 +675,9 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne case R(als: TypedNuAls) => if (als.tparams.nonEmpty) ??? // TODO als.body - case R(m) => err(msg"Illegal selection of ${m.kind.str} member in type position", nme.toLoc) - case L(d) => err(d) + case _ => constrTB(ct) // fallback } - case _ => - err(msg"Illegal prefix of type selection: ${b_ty.expPos}", base.toLoc) + case b_ty => constrTB(b_ty) } go(base_ty, _ => N) case Recursive(uv, body) => @@ -802,7 +830,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne } // TODO also prevent rebinding of "not" - val reservedVarNames: Set[Str] = Set("|", "&", "~", "neg", "and", "or", "is") + val reservedVarNames: Set[Str] = Set("|", "&", "~", "neg", "and", "or", "is", "?") object ValidVar { def unapply(v: Var)(implicit raise: Raise): S[Str] = S { @@ -907,6 +935,9 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne case v @ Var("_") => if (ctx.inPattern || funkyTuples) freshVar(tp(v.toLoc, "wildcard"), N) else err(msg"Widlcard in expression position.", v.toLoc) + + case w @ Var("?") => + err(msg"Cannot use ? as expression", w.toLoc) case Ann(ann, receiver) => val annType = typeTerm(ann) @@ -1640,8 +1671,8 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne RecordType.mk(dti.tparams.map { case (tn, tv, vi) => val nv = freshVar(tv.prov, S(tv), tv.nameHint) - (Var(nme+"#"+tn.name).withLocOf(tn), - FieldType.mk(vi.getOrElse(VarianceInfo.in), nv, nv)(provTODO)) + (Var(tparamField(nme, tn.name, vi.visible)).withLocOf(tn), + FieldType.mk(vi.varinfo.getOrElse(VarianceInfo.in), nv, nv)(provTODO)) })(provTODO) println(s"Match arm $nme: $tag & $ty") tag -> ty @@ -1651,8 +1682,8 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne RecordType.mk(cls.tparams.map { case (tn, tv, vi) => val nv = freshVar(tv.prov, S(tv), tv.nameHint) - (Var(nme+"#"+tn.name).withLocOf(tn), - FieldType.mk(vi.getOrElse(cls.varianceOf(tv)), nv, nv)(provTODO)) + (Var(tparamField(nme, tn.name, vi.visible)).withLocOf(tn), + FieldType.mk(vi.varinfo.getOrElse(cls.varianceOf(tv)), nv, nv)(provTODO)) })(provTODO) println(s"Match arm $nme: $tag & $ty") tag -> ty @@ -1857,7 +1888,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne } class ExpCtx(val tps: Map[TV, TN]) { - def apply(tparams: Ls[(TN, TV, Opt[VarianceInfo])]): ExpCtx = + def apply(tparams: Ls[(TN, TV, TypeParamInfo)]): ExpCtx = new ExpCtx(tps ++ tparams.iterator.map{case (tn, tv, vi) => tv -> tn}) } diff --git a/shared/src/main/scala/mlscript/TyperHelpers.scala b/shared/src/main/scala/mlscript/TyperHelpers.scala index e76d3a5a5b..d59efeff7b 100644 --- a/shared/src/main/scala/mlscript/TyperHelpers.scala +++ b/shared/src/main/scala/mlscript/TyperHelpers.scala @@ -1095,9 +1095,9 @@ abstract class TyperHelpers { Typer: Typer => ctx.tyDefs2.get(defn.name).map { info => lazy val mkTparamRcd = RecordType(info.tparams.lazyZip(targs).map { case ((tn, tv, vi), ta) => - val fldNme = defn.name + "#" + tn.name + val fldNme = tparamField(defn.name, tn.name, vi.visible) // TODO also use computed variance info when available! - Var(fldNme).withLocOf(tn) -> FieldType.mk(vi.getOrElse(VarianceInfo.in), ta, ta)(provTODO) + Var(fldNme).withLocOf(tn) -> FieldType.mk(vi.varinfo.getOrElse(VarianceInfo.in), ta, ta)(provTODO) })(provTODO) info.result match { case S(td: TypedNuAls) => @@ -1155,7 +1155,7 @@ abstract class TyperHelpers { Typer: Typer => lazy val tparamTags = if (paramTags) RecordType.mk(td.tparamsargs.map { case (tp, tv) => val tvv = td.getVariancesOrDefault - tparamField(defn, tp) -> FieldType( + tparamField(defn, tp, false) -> FieldType( Some(if (tvv(tv).isCovariant) BotType else tv), if (tvv(tv).isContravariant) TopType else tv)(prov) })(noProv) diff --git a/shared/src/main/scala/mlscript/helpers.scala b/shared/src/main/scala/mlscript/helpers.scala index 92cb588759..bb30152bcd 100644 --- a/shared/src/main/scala/mlscript/helpers.scala +++ b/shared/src/main/scala/mlscript/helpers.scala @@ -744,6 +744,8 @@ trait TermImpl extends StatementImpl { self: Term => case ty @ App(v @ Var("\\"), PlainTup(lhs, rhs)) => Inter(lhs.toType_!, Neg(rhs.toType_!).withLoc(Loc(v :: rhs :: Nil))).withLoc(ty.toCoveringLoc) case App(Var("~"), rhs) => Neg(rhs.toType_!) + case App(Var(".."), PlainTup(lhs, rhs)) => + Bounds(lhs.toType_!, rhs.toType_!) case Lam(lhs, rhs) => Function(lhs.toType_!, rhs.toType_!) case App(lhs, PlainTup(fs @ _*)) => lhs.toType_! match { @@ -1174,6 +1176,12 @@ trait CaseBranchesImpl extends Located { self: CaseBranches => case NoCases => "" } + def map(f: Term => Term): CaseBranches = this match { + case Case(pat, body, rest) => Case(pat, f(body), rest.map(f)) + case Wildcard(b) => Wildcard(f(b)) + case NoCases => this + } + def showIn(implicit ctx: ShowCtx): Str = this match { case Case(pat, body, rest) => ctx.lnIndStr + pat.showIn(false) + " => " + body.showIn(false) + rest.showIn @@ -1207,6 +1215,19 @@ trait IfBodyImpl extends Located { self: IfBody => case IfOpsApp(lhs, ops) => s"${lhs.showDbg} ‹${ops.iterator.map{case(v, r) => s"· ${v.showDbg} ${r.showDbg}"}.mkString("; ")}›" case IfLet(isRec, v, r, b) => s"${if (isRec) "rec " else ""}let ${v.showDbg} = ${r.showDbg} in ${b.showDbg}" } + + def map(f: Term => Term): IfBody = this match { + case IfThen(expr, rhs) => IfThen(expr, f(rhs)) + case IfElse(expr) => IfElse(f(expr)) + case IfLet(isRec, name, rhs, body) => IfLet(isRec, name, rhs, body.map(f)) + case IfOpApp(lhs, op, rhs) => IfOpApp(lhs, op, rhs.map(f)) + case IfOpsApp(lhs, opsRhss) => IfOpsApp(lhs, opsRhss.map(_.mapSecond(_.map(f)))) + case IfBlock(lines) => IfBlock(lines.map { + case Left(ifb) => Left(ifb.map(f)) + case r: Right[_, _] => r + }) + } + def showIn(implicit ctx: ShowCtx): Str = this match { case IfThen(lhs, rhs) => s"${lhs.showIn(!lhs.isInstanceOf[SimpleTerm])} then ${rhs.showIn(false)}" diff --git a/shared/src/main/scala/mlscript/syntax.scala b/shared/src/main/scala/mlscript/syntax.scala index eb6005b2b6..5702184aa9 100644 --- a/shared/src/main/scala/mlscript/syntax.scala +++ b/shared/src/main/scala/mlscript/syntax.scala @@ -157,7 +157,7 @@ final case class AppliedType(base: TypeName, targs: List[Type]) extends Type wit final case class Selection(base: Type, name: TypeName) extends Type final case class Neg(base: Type) extends Type final case class Rem(base: Type, names: Ls[Var]) extends Type -final case class Bounds(lb: Type, ub: Type) extends Type +final case class Bounds(lb: Type, ub: Type) extends Type // TODO repurpose to use as wildcard type arg final case class WithExtension(base: Type, rcd: Record) extends Type final case class Splice(fields: Ls[Either[Type, Field]]) extends Type final case class Constrained(base: TypeLike, tvBounds: Ls[TypeVar -> Bounds], where: Ls[Bounds]) extends Type @@ -201,7 +201,7 @@ sealed trait Outer { def kind: OuterKind } final case class NuTypeDef( kind: TypeDefKind, nme: TypeName, - tparams: Ls[(Opt[VarianceInfo], TypeName)], + tparams: Ls[(TypeParamInfo, TypeName)], params: Opt[Tup], // the specialized parameters for that type ctor: Opt[Constructor], sig: Opt[Type], @@ -248,7 +248,8 @@ final case class NuFunDef( final case class Constructor(params: Tup, body: Blk) extends DesugaredStatement with ConstructorImpl // constructor(...) { ... } - +// TODO lb and ub not handled in typing +final case class TypeParamInfo(varinfo: Opt[VarianceInfo], visible: Bool, lb: Opt[TypeName], ub: Opt[TypeName]) final case class VarianceInfo(isCovariant: Bool, isContravariant: Bool) { diff --git a/shared/src/main/scala/mlscript/ucs/Desugarer.scala b/shared/src/main/scala/mlscript/ucs/Desugarer.scala index 5afc766ddb..ff82ed102f 100644 --- a/shared/src/main/scala/mlscript/ucs/Desugarer.scala +++ b/shared/src/main/scala/mlscript/ucs/Desugarer.scala @@ -192,6 +192,10 @@ class Desugarer extends TypeDefs { self: Typer => Clause.MatchAny(scrutinee)(wildcard.toLoc.toList) :: Nil // If it's not top-level, wildcard means we don't care. case Var("_") => Nil + // We cannot use wildcard (type) for patterns + case wc @ Var("?") => throw new DesugaringException({ + msg"Cannot match on wildcard ?" + }, wc.toLoc) // This case handles literals. // x is true | x is false | x is 0 | x is "text" | ... case literal: Var if literal.name === "true" || literal.name === "false" => @@ -808,7 +812,32 @@ class Desugarer extends TypeDefs { self: Typer => case _ => visited.put(field, alias) } } - + /* + val als = extraAlias.toList + assert(fields.size === als.size) + + (fields, als).zip/* .distinctBy(_._1) */.flatMap { + case (_ -> Var("_"), _) => + case (_ -> Var(alias), _) => + + } + */ + + // /* + Let(false, Var("$unapp"), App(Sel(className, Var(unapplyMtd.name)), PlainTup(scrutinee.reference)), + // Let(false, Var("$tmp"), Sel(Var("$unapp"), Var("0")), + fields.distinctBy(_._1).zipWithIndex.foldRight( + extraAlias.toList.foldRight(consequent)((lt, rs) => Let(false, Var(lt._2), Var(lt._1), rs)) + )((field, rs) => { + val (_ -> Var(alias), index) = field + if (alias === "_") rs + else + Let(false, Var(alias), Sel(Var("$unapp"), Var(index.toString)), rs) + }) + ) + // */ + + /* App(Lam(Tup( N -> Fld(FldFlags.empty, Tup( fields.distinctBy(_._1).map { @@ -822,6 +851,11 @@ class Desugarer extends TypeDefs { self: Typer => Tup(N -> Fld(FldFlags.empty, scrutinee.reference) :: Nil)) ) :: Nil) ) + */ + + // ) + // ) + case _ => mkLetFromFields(scrutinee, fields.filter(_._2.name =/= "_").toList, consequent) } Case(className, body, rec2(next)) diff --git a/shared/src/test/diff/codegen/AuxiliaryConstructors.mls b/shared/src/test/diff/codegen/AuxiliaryConstructors.mls index 36b8a2c8fc..ac695bcccc 100644 --- a/shared/src/test/diff/codegen/AuxiliaryConstructors.mls +++ b/shared/src/test/diff/codegen/AuxiliaryConstructors.mls @@ -318,7 +318,7 @@ fun f(c) = //│ globalThis.f = function f(c) { //│ return ((() => { //│ let a; -//│ return a = c, a instanceof F.class ? (([x]) => x)(F.unapply(c)) : a instanceof G ? 2 : 0; +//│ return a = c, a instanceof F.class ? (($unapp) => ((x) => x)($unapp[0]))(F.unapply(c)) : a instanceof G ? 2 : 0; //│ })()); //│ }; //│ // End of generated code @@ -512,7 +512,7 @@ let hh = h(1) :e new hh(1) -//│ ╔══[ERROR] type identifier not found: hh +//│ ╔══[ERROR] Unexpected type `?a` after `new` keyword //│ ║ l.514: new hh(1) //│ ╙── ^^ //│ error diff --git a/shared/src/test/diff/codegen/FieldOverride.mls b/shared/src/test/diff/codegen/FieldOverride.mls index 0fb2afb424..10f51db49b 100644 --- a/shared/src/test/diff/codegen/FieldOverride.mls +++ b/shared/src/test/diff/codegen/FieldOverride.mls @@ -128,7 +128,7 @@ let c3 = C3(1) let c4 = c3.C4(2) c3.a c4.a -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member C4 not yet supported //│ ║ l.128: let c4 = c3.C4(2) //│ ╙── ^^^ //│ let c3: C3 diff --git a/shared/src/test/diff/codegen/IndirectRecursion.mls b/shared/src/test/diff/codegen/IndirectRecursion.mls index 0b431e1dfa..4b1f168c73 100644 --- a/shared/src/test/diff/codegen/IndirectRecursion.mls +++ b/shared/src/test/diff/codegen/IndirectRecursion.mls @@ -138,8 +138,8 @@ def z = (fun f -> (fun x -> f (fun v -> (x x) v)) (fun x -> f (fun v -> (x x) v))!) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> 'a -> ? -//│ <: 'a -> ? -> ? +//│ 'a :> 'a -> #? +//│ <: 'a -> #? -> #? //│ ╙── //│ (('a -> 'b) -> 'c & ('d -> 'e) -> ('d -> 'e & 'a -> 'b)) -> 'c //│ <: z: @@ -166,8 +166,8 @@ def z = (fun f -> (fun x -> f (fun v -> (x x) v)) (fun x -> f (fun v -> (x x) v))!) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> 'a -> ? -//│ <: 'a -> ? -> ? +//│ 'a :> 'a -> #? +//│ <: 'a -> #? -> #? //│ ╙── //│ (('a -> 'b) -> 'c & ('d -> 'e) -> ('d -> 'e & 'a -> 'b)) -> 'c //│ <: z: diff --git a/shared/src/test/diff/codegen/Mixin.mls b/shared/src/test/diff/codegen/Mixin.mls index 9179f28b54..e1be5ebd2a 100644 --- a/shared/src/test/diff/codegen/Mixin.mls +++ b/shared/src/test/diff/codegen/Mixin.mls @@ -87,10 +87,7 @@ mixin EvalBase { //│ const qualifier1 = this; //│ return ((() => { //│ let a; -//│ return (a = e, a instanceof Lit.class ? (([n]) => n)(Lit.unapply(e)) : a instanceof Add.class ? (([ -//│ l, -//│ r -//│ ]) => qualifier1.eval(l) + qualifier1.eval(r))(Add.unapply(e)) : (() => { +//│ return (a = e, a instanceof Lit.class ? (($unapp) => ((n) => n)($unapp[0]))(Lit.unapply(e)) : a instanceof Add.class ? (($unapp) => ((l) => ((r) => qualifier1.eval(l) + qualifier1.eval(r))($unapp[1]))($unapp[0]))(Add.unapply(e)) : (() => { //│ throw new Error("non-exhaustive case expression"); //│ })()); //│ })()); @@ -158,7 +155,7 @@ mixin EvalNeg { //│ eval(e) { //│ const qualifier1 = this; //│ return ((() => { -//│ return e instanceof Neg.class ? (([d]) => 0 - qualifier1.eval(d))(Neg.unapply(e)) : super.eval(e); +//│ return e instanceof Neg.class ? (($unapp) => ((d) => 0 - qualifier1.eval(d))($unapp[0]))(Neg.unapply(e)) : super.eval(e); //│ })()); //│ } //│ }); @@ -192,7 +189,7 @@ mixin EvalNegNeg { //│ eval(e) { //│ const qualifier1 = this; //│ return ((() => { -//│ return e instanceof Neg.class ? (([tmp0]) => tmp0 instanceof Neg.class ? (([d]) => qualifier1.eval(d))(Neg.unapply(tmp0)) : super.eval(e))(Neg.unapply(e)) : super.eval(e); +//│ return e instanceof Neg.class ? (($unapp) => ((tmp0) => tmp0 instanceof Neg.class ? (($unapp) => ((d) => qualifier1.eval(d))($unapp[0]))(Neg.unapply(tmp0)) : super.eval(e))($unapp[0]))(Neg.unapply(e)) : super.eval(e); //│ })()); //│ } //│ }); @@ -372,7 +369,7 @@ mixin Base { fun x = y } //│ ╔══[ERROR] identifier not found: y -//│ ║ l.372: fun x = y +//│ ║ l.369: fun x = y //│ ╙── ^ //│ mixin Base() { //│ fun x: error diff --git a/shared/src/test/diff/codegen/MixinCapture.mls b/shared/src/test/diff/codegen/MixinCapture.mls index cf721dcf60..da805abd98 100644 --- a/shared/src/test/diff/codegen/MixinCapture.mls +++ b/shared/src/test/diff/codegen/MixinCapture.mls @@ -26,7 +26,7 @@ mixin EvalAddLit { //│ eval(e) { //│ return ((() => { //│ let a; -//│ return (a = e, a instanceof qualifier.Lit.class ? (([n]) => n)(qualifier.Lit.unapply(e)) : (() => { +//│ return (a = e, a instanceof qualifier.Lit.class ? (($unapp) => ((n) => n)($unapp[0]))(qualifier.Lit.unapply(e)) : (() => { //│ throw new Error("non-exhaustive case expression"); //│ })()); //│ })()); diff --git a/shared/src/test/diff/codegen/Nested.mls b/shared/src/test/diff/codegen/Nested.mls index 10843c74aa..9760170426 100644 --- a/shared/src/test/diff/codegen/Nested.mls +++ b/shared/src/test/diff/codegen/Nested.mls @@ -69,7 +69,7 @@ module A { :js let bb = A.B(A.a) bb.b -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member B not yet supported //│ ║ l.70: let bb = A.B(A.a) //│ ╙── ^^ //│ let bb: error @@ -102,10 +102,10 @@ let c = b.C(1) c.outer1 let d = b.D(1) d.outer -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member C not yet supported //│ ║ l.101: let c = b.C(1) //│ ╙── ^^ -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member D not yet supported //│ ║ l.103: let d = b.D(1) //│ ╙── ^^ //│ class B(x: Int) { @@ -350,7 +350,7 @@ let es = E(1) let fff = es.F(2) let gg = fff.G(3) gg.sum -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member F not yet supported //│ ║ l.350: let fff = es.F(2) //│ ╙── ^^ //│ let es: E @@ -549,7 +549,7 @@ module G { let jj = G.H.J(42) let i = jj.ii(2) i.x -//│ ╔══[ERROR] Access to module member not yet supported +//│ ╔══[ERROR] Access to module member H not yet supported //│ ║ l.549: let jj = G.H.J(42) //│ ╙── ^^ //│ let jj: error @@ -657,7 +657,7 @@ module H { :js let j = H.J(42) j.i.x -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member J not yet supported //│ ║ l.658: let j = H.J(42) //│ ╙── ^^ //│ let j: error @@ -687,7 +687,7 @@ class I(x: Int) { let i = I(1) let ij = i.J(0) ij.incY -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member J not yet supported //│ ║ l.688: let ij = i.J(0) //│ ╙── ^^ //│ class I(x: Int) { @@ -878,10 +878,10 @@ module J { :js let m = J.M() let n = J.N(2) -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member M not yet supported //│ ║ l.879: let m = J.M() //│ ╙── ^^ -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member N not yet supported //│ ║ l.880: let n = J.N(2) //│ ╙── ^^ //│ let m: error @@ -922,7 +922,7 @@ module K { :e let m = K.L.M() m.f -//│ ╔══[ERROR] Access to module member not yet supported +//│ ╔══[ERROR] Access to module member L not yet supported //│ ║ l.923: let m = K.L.M() //│ ╙── ^^ //│ let m: error @@ -952,7 +952,7 @@ module L { :e let op = L.N.O.P(0) op.x -//│ ╔══[ERROR] Access to module member not yet supported +//│ ╔══[ERROR] Access to module member N not yet supported //│ ║ l.953: let op = L.N.O.P(0) //│ ╙── ^^ //│ let op: error @@ -979,10 +979,10 @@ module M { _ then 2 } M.N.op(M.P()) -//│ ╔══[ERROR] Access to module member not yet supported +//│ ╔══[ERROR] Access to module member N not yet supported //│ ║ l.981: M.N.op(M.P()) //│ ╙── ^^ -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member P not yet supported //│ ║ l.981: M.N.op(M.P()) //│ ╙── ^^ //│ module M { @@ -1165,7 +1165,7 @@ module N { :e N.O.P() -//│ ╔══[ERROR] Access to module member not yet supported +//│ ╔══[ERROR] Access to module member O not yet supported //│ ║ l.1167: N.O.P() //│ ╙── ^^ //│ error @@ -1181,7 +1181,7 @@ class I(x: Int) { } } I(1).J(3).a -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member J not yet supported //│ ║ l.1183: I(1).J(3).a //│ ╙── ^^ //│ class I(x: Int) { diff --git a/shared/src/test/diff/codegen/NewMatching.mls b/shared/src/test/diff/codegen/NewMatching.mls index 809dcb337d..b0ab8941c2 100644 --- a/shared/src/test/diff/codegen/NewMatching.mls +++ b/shared/src/test/diff/codegen/NewMatching.mls @@ -39,22 +39,7 @@ fun sum(v) = //│ globalThis.sum = function sum(v) { //│ return ((() => { //│ let a; -//│ return (a = v, a instanceof V0.class ? 0 : a instanceof V1.class ? (([a]) => a)(V1.unapply(v)) : a instanceof V2.class ? (([ -//│ a, -//│ b -//│ ]) => a + b)(V2.unapply(v)) : a instanceof Pos.class ? (([x]) => x > 0 === true ? x : -1)(Pos.unapply(v)) : a instanceof V22.class ? (([ -//│ tmp0, -//│ tmp1 -//│ ]) => tmp0 instanceof V2.class ? (([ -//│ x1, -//│ y1 -//│ ]) => tmp1 instanceof V2.class ? (([ -//│ x2, -//│ y2 -//│ ]) => x1 + y1 + x2 + y2)(V2.unapply(tmp1)) : -1)(V2.unapply(tmp0)) : -1)(V22.unapply(v)) : a instanceof Half.class ? (([ -//│ tmp2, -//│ x -//│ ]) => x)(Half.unapply(v)) : a instanceof None.class ? (([tmp3]) => 0)(None.unapply(v)) : -1); +//│ return a = v, a instanceof V0.class ? 0 : a instanceof V1.class ? (($unapp) => ((a) => a)($unapp[0]))(V1.unapply(v)) : a instanceof V2.class ? (($unapp) => ((a) => ((b) => a + b)($unapp[1]))($unapp[0]))(V2.unapply(v)) : a instanceof Pos.class ? (($unapp) => ((x) => x > 0 === true ? x : -1)($unapp[0]))(Pos.unapply(v)) : a instanceof V22.class ? (($unapp) => ((tmp0) => ((tmp1) => tmp0 instanceof V2.class ? (($unapp) => ((x1) => ((y1) => tmp1 instanceof V2.class ? (($unapp) => ((x2) => ((y2) => x1 + y1 + x2 + y2)($unapp[1]))($unapp[0]))(V2.unapply(tmp1)) : -1)($unapp[1]))($unapp[0]))(V2.unapply(tmp0)) : -1)($unapp[1]))($unapp[0]))(V22.unapply(v)) : a instanceof Half.class ? (($unapp) => ((x) => x)($unapp[1]))(Half.unapply(v)) : a instanceof None.class ? (($unapp) => 0)(None.unapply(v)) : -1; //│ })()); //│ }; //│ // End of generated code @@ -104,7 +89,7 @@ fun get1(s) = //│ globalThis.get1 = function get1(s) { //│ return ((() => { //│ let a; -//│ return (a = s, a instanceof Some.class ? (([tmp4]) => ((y) => tmp4 instanceof V1.class ? (([x]) => x)(V1.unapply(tmp4)) : y)(tmp4))(Some.unapply(s)) : (() => { +//│ return (a = s, a instanceof Some.class ? (($unapp) => ((tmp2) => ((y) => tmp2 instanceof V1.class ? (($unapp) => ((x) => x)($unapp[0]))(V1.unapply(tmp2)) : y)(tmp2))($unapp[0]))(Some.unapply(s)) : (() => { //│ throw new Error("non-exhaustive case expression"); //│ })()); //│ })()); @@ -136,7 +121,7 @@ fun foo(s) = //│ // Query 1 //│ globalThis.foo = function foo(s) { //│ return ((() => { -//│ return s instanceof Some.class ? (([t]) => ((b) => b + t.x)(s2.value))(Some.unapply(s)) : 0; +//│ return s instanceof Some.class ? (($unapp) => ((t) => ((b) => b + t.x)(s2.value))($unapp[0]))(Some.unapply(s)) : 0; //│ })()); //│ }; //│ // End of generated code @@ -219,7 +204,7 @@ fun ft(x) = FooBar(x) then x _ then 0 //│ ╔══[ERROR] class FooBar expects 0 parameter but found 1 parameter -//│ ║ l.219: FooBar(x) then x +//│ ║ l.204: FooBar(x) then x //│ ╙── ^^^^^^^^^ //│ fun ft: anything -> error //│ Code generation encountered an error: @@ -265,7 +250,7 @@ fun c(x) = VVC(x, y, z) then x + y + z _ then 0 //│ ╔══[ERROR] class VVC expects 2 parameters but found 3 parameters -//│ ║ l.265: VVC(x, y, z) then x + y + z +//│ ║ l.250: VVC(x, y, z) then x + y + z //│ ╙── ^^^^^^^^^^^^ //│ class VVC(v: Int, vc: Int) //│ fun c: anything -> error diff --git a/shared/src/test/diff/fcp-lit/Leijen.mls b/shared/src/test/diff/fcp-lit/Leijen.mls index e44fd04e4a..7300871067 100644 --- a/shared/src/test/diff/fcp-lit/Leijen.mls +++ b/shared/src/test/diff/fcp-lit/Leijen.mls @@ -425,7 +425,7 @@ app (map head) (single ids) (error : List['a -> 'a] -> int) (error : List[(forall 'd. 'd -> 'c) -> 'c]) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: ? -> 'a +//│ 'a <: #? -> 'a //│ ╙── //│ res: int diff --git a/shared/src/test/diff/fcp-lit/variations_PolyML.mls b/shared/src/test/diff/fcp-lit/variations_PolyML.mls index 9a971c8160..372093d13b 100644 --- a/shared/src/test/diff/fcp-lit/variations_PolyML.mls +++ b/shared/src/test/diff/fcp-lit/variations_PolyML.mls @@ -75,7 +75,7 @@ rec def mem x l = case l of } //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: {head: ?, tail: Cons[?] & 'a} +//│ 'a <: {head: #?, tail: Cons[?] & 'a} //│ ║ l.72: rec def mem x l = case l of //│ ╙── ^ //│ mem: anything -> 'a -> Bool diff --git a/shared/src/test/diff/fcp/Church_CT.mls b/shared/src/test/diff/fcp/Church_CT.mls index bcc8702053..6fde6cbffa 100644 --- a/shared/src/test/diff/fcp/Church_CT.mls +++ b/shared/src/test/diff/fcp/Church_CT.mls @@ -631,7 +631,7 @@ rec def to_ch_s n = else s (to_ch_s (n - 1)) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> forall 'b. (? & 'b) -> (forall 'b 'c 'd 'e 'f. ('f & 'c) -> ('f | 'e) +//│ 'a :> forall 'b. (#? & 'b) -> (forall 'b 'c 'd 'e 'f. ('f & 'c) -> ('f | 'e) //│ where //│ 'a <: 'b -> 'c -> 'd //│ 'b <: 'd -> 'e) @@ -653,7 +653,7 @@ rec def to_ch n = else s (to_ch (n - 1)) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> forall 'b. (? & 'b) -> (forall 'b 'c 'd 'e 'f. ('f & 'c) -> ('f | 'e) +//│ 'a :> forall 'b. (#? & 'b) -> (forall 'b 'c 'd 'e 'f. ('f & 'c) -> ('f | 'e) //│ where //│ 'a <: 'b -> 'c -> 'd //│ 'b <: 'd -> 'e) @@ -673,7 +673,7 @@ rec def to_ch n = to_church_ty = to_ch //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> forall 'b. (? & 'b) -> (forall 'b 'c 'd 'e 'f. ('f & 'c) -> ('f | 'e) +//│ 'a :> forall 'b. (#? & 'b) -> (forall 'b 'c 'd 'e 'f. ('f & 'c) -> ('f | 'e) //│ where //│ 'a <: 'b -> 'c -> 'd //│ 'b <: 'd -> 'e) @@ -812,7 +812,7 @@ rec def to_ch_A1 n = else s (to_ch_A1 (n - 1) : ChurchInt) //│ ╔══[ERROR] Inferred recursive type: 'to_ch_A1 //│ where -//│ 'to_ch_A1 :> forall 'to_ch_A1. int -> (forall 'a. (? & 'a) -> (forall 'a 'b 'c 'd 'e. ('b & 'e) -> ('d | 'e) +//│ 'to_ch_A1 :> forall 'to_ch_A1. int -> (forall 'a. (#? & 'a) -> (forall 'a 'b 'c 'd 'e. ('b & 'e) -> ('d | 'e) //│ where //│ ChurchInt <: 'a -> 'b -> 'c //│ 'a <: 'c -> 'd)) @@ -834,7 +834,7 @@ rec def to_ch_A1 n = to_church_ty = to_ch_A1 //│ ╔══[ERROR] Inferred recursive type: 'to_ch_A1 //│ where -//│ 'to_ch_A1 :> forall 'to_ch_A1. int -> (forall 'a. (? & 'a) -> (forall 'a 'b 'c 'd 'e. ('b & 'e) -> ('d | 'e) +//│ 'to_ch_A1 :> forall 'to_ch_A1. int -> (forall 'a. (#? & 'a) -> (forall 'a 'b 'c 'd 'e. ('b & 'e) -> ('d | 'e) //│ where //│ ChurchInt <: 'a -> 'b -> 'c //│ 'a <: 'c -> 'd)) @@ -1069,7 +1069,7 @@ rec def to_chD n = to_church_ty = to_ch //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> forall 'b 'c 'd 'e 'f. (? & 'b) -> (('f & 'c) -> ('f | 'e) +//│ 'a :> forall 'b 'c 'd 'e 'f. (#? & 'b) -> (('f & 'c) -> ('f | 'e) //│ where //│ 'a <: 'b -> 'c -> 'd //│ 'b <: 'd -> 'e) @@ -1169,7 +1169,7 @@ to_church_ty = to_ch_simplif to_church_ty = to_ch_A1 //│ ╔══[ERROR] Inferred recursive type: 'to_ch_A1 //│ where -//│ 'to_ch_A1 :> forall 'to_ch_A1. int -> (forall 'a 'b 'c 'd 'e. (? & 'a) -> (('b & 'e) -> ('d | 'e) +//│ 'to_ch_A1 :> forall 'to_ch_A1. int -> (forall 'a 'b 'c 'd 'e. (#? & 'a) -> (('b & 'e) -> ('d | 'e) //│ where //│ ChurchInt <: 'a -> 'b -> 'c //│ 'a <: 'c -> 'd)) diff --git a/shared/src/test/diff/fcp/FunnyId.mls b/shared/src/test/diff/fcp/FunnyId.mls index 1180173631..a303dc15a8 100644 --- a/shared/src/test/diff/fcp/FunnyId.mls +++ b/shared/src/test/diff/fcp/FunnyId.mls @@ -30,9 +30,9 @@ id_ty = id rec def id x = let tmp = id id x in x //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: 'b -> ? +//│ 'a <: 'b -> #? //│ 'b :> 'b -> 'b -//│ <: ? & 'a +//│ <: #? & 'a //│ ║ l.30: rec def id x = let tmp = id id x in x //│ ╙── ^^^^^ //│ id: 'a -> 'a @@ -46,9 +46,9 @@ rec def id x = let tmp = id id x in x id 1 //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: 'b -> ? +//│ 'a <: 'b -> #? //│ 'b :> 1 | 'b -> 'b -//│ <: ? & 'a +//│ <: #? & 'a //│ ║ l.30: rec def id x = let tmp = id id x in x //│ ╙── ^^^^^ //│ ╔══[ERROR] Type mismatch in application: @@ -74,9 +74,9 @@ id 1 id_ty = id //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: 'b -> ? +//│ 'a <: 'b -> #? //│ 'b :> 'b -> 'b -//│ <: ? & 'a +//│ <: #? & 'a //│ ║ l.30: rec def id x = let tmp = id id x in x //│ ╙── ^^^^^ //│ 'a -> 'a diff --git a/shared/src/test/diff/fcp/ListBuild.mls b/shared/src/test/diff/fcp/ListBuild.mls index 1dfe4f4548..a340ae8939 100644 --- a/shared/src/test/diff/fcp/ListBuild.mls +++ b/shared/src/test/diff/fcp/ListBuild.mls @@ -74,7 +74,7 @@ def build0 (g: forall 'b. ('a -> 'a -> 'b) -> 'b) = g (fun x -> fun y -> single( def build0 (g: forall 'b. ('a -> 'b -> 'b) -> 'b) = g (fun x -> fun y -> single((x, y))) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> Ls[(?, forall 'a. 'a,)] +//│ 'a :> Ls[(#?, forall 'a. 'a,)] //│ ║ l.74: def build0 (g: forall 'b. ('a -> 'b -> 'b) -> 'b) = g (fun x -> fun y -> single((x, y))) //│ ╙── ^^^^^^^^^^^^^^ //│ build0: (forall 'b. ('a -> 'b -> 'b) -> 'b) -> 'c diff --git a/shared/src/test/diff/fcp/NestedDataTypes.mls b/shared/src/test/diff/fcp/NestedDataTypes.mls index 9aa94da253..2acefb72bf 100644 --- a/shared/src/test/diff/fcp/NestedDataTypes.mls +++ b/shared/src/test/diff/fcp/NestedDataTypes.mls @@ -67,7 +67,7 @@ rec def map f tree = case tree of { } //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: {subTree: Leaf[?] & {value: ((?, (?, ?,),), ((?, ?,), ?,),)} | Node[?] & 'a} +//│ 'a <: {subTree: Leaf[?] & {value: ((#?, (#?, #?,),), ((#?, #?,), #?,),)} | Node[?] & 'a} //│ ║ l.64: rec def map f tree = case tree of { //│ ╙── ^^^^ //│ ╔══[ERROR] Cyclic-looking constraint while typing binding of lambda expression; a type annotation may be required diff --git a/shared/src/test/diff/fcp/Paper.mls b/shared/src/test/diff/fcp/Paper.mls index a9ab8da0d0..3de8758305 100644 --- a/shared/src/test/diff/fcp/Paper.mls +++ b/shared/src/test/diff/fcp/Paper.mls @@ -92,7 +92,7 @@ auto auto! //│ ╔══[ERROR] Inferred recursive type: 'a //│ where //│ 'a :> 'a -> 'b -//│ <: 'a -> (? & 'b) +//│ <: 'a -> (#? & 'b) //│ ╙── //│ res: nothing diff --git a/shared/src/test/diff/fcp/PaperTable.mls b/shared/src/test/diff/fcp/PaperTable.mls index 19921d0790..ea66f51e65 100644 --- a/shared/src/test/diff/fcp/PaperTable.mls +++ b/shared/src/test/diff/fcp/PaperTable.mls @@ -713,7 +713,7 @@ auto auto //│ ╔══[ERROR] Inferred recursive type: 'a //│ where //│ 'a :> 'a -> 'b -//│ <: 'a -> (? & 'b) +//│ <: 'a -> (#? & 'b) //│ ╙── //│ res: nothing //│ Runtime error: @@ -1120,7 +1120,7 @@ auto auto //│ ╔══[ERROR] Inferred recursive type: 'a //│ where //│ 'a :> 'a -> 'b -//│ <: 'a -> (? & 'b) +//│ <: 'a -> (#? & 'b) //│ ╙── //│ res: nothing //│ Runtime error: @@ -1499,7 +1499,7 @@ auto auto //│ ╔══[ERROR] Inferred recursive type: 'a //│ where //│ 'a :> 'a -> 'b -//│ <: 'a -> (? & 'b) +//│ <: 'a -> (#? & 'b) //│ ╙── //│ res: nothing //│ Runtime error: diff --git a/shared/src/test/diff/fcp/SystemF_2.mls b/shared/src/test/diff/fcp/SystemF_2.mls index 9df044c916..54adc33c72 100644 --- a/shared/src/test/diff/fcp/SystemF_2.mls +++ b/shared/src/test/diff/fcp/SystemF_2.mls @@ -38,7 +38,7 @@ id iter2 iter2 iter2 iter2 K //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> ? -> ? -> 'a +//│ 'a :> #? -> #? -> 'a //│ ╙── //│ res: 'a -> anything -> 'b //│ where @@ -97,7 +97,7 @@ c2 = succ (succ n0) c2 c2 K //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> ? -> 'a +//│ 'a :> #? -> 'a //│ ╙── //│ res: ('a & 'X) -> (anything -> 'a | 'X) //│ where @@ -127,10 +127,10 @@ c2_ c2_! c2_ c2_ K //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> ? -> ('a | 'b | 'c | 'd) -//│ 'c :> ? -> ('d | 'b) | ? -> ('b | 'c) -//│ 'd :> ? -> ('c | 'b) -//│ 'b :> ? -> ('a | 'b) +//│ 'a :> #? -> ('a | 'b | 'c | 'd) +//│ 'c :> #? -> ('d | 'b) | #? -> ('b | 'c) +//│ 'd :> #? -> ('c | 'b) +//│ 'b :> #? -> ('a | 'b) //│ ╙── //│ res: ('a & 'b & 'c) -> anything -> ('d | 'e) //│ where @@ -153,7 +153,7 @@ c2__ c2__ c2__ c2__ K //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> ? -> ? -> 'a +//│ 'a :> #? -> #? -> 'a //│ ╙── //│ res: 'a -> anything -> 'b //│ where @@ -327,7 +327,7 @@ c2 = succ (succ n0) c2 c2 K //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> ? -> 'a +//│ 'a :> #? -> 'a //│ ╙── //│ res: ('a & 'X) -> (anything -> 'a | 'X) //│ where @@ -370,7 +370,7 @@ c2_ c2_ c2_ c2_ K //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> forall 'b 'c 'd 'e. ('b & 'e) -> (? -> 'e | 'd) +//│ 'a :> forall 'b 'c 'd 'e. ('b & 'e) -> (#? -> 'e | 'd) //│ where //│ forall 'f. 'f -> (forall 'g 'h 'i. 'g -> 'i //│ where diff --git a/shared/src/test/diff/fcp/ToChurchSimplif_CT.mls b/shared/src/test/diff/fcp/ToChurchSimplif_CT.mls index 23bac46b06..de55cc0c98 100644 --- a/shared/src/test/diff/fcp/ToChurchSimplif_CT.mls +++ b/shared/src/test/diff/fcp/ToChurchSimplif_CT.mls @@ -555,7 +555,7 @@ rec def to_ch n = else s (to_ch (n - 1)) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> forall 'b 'c 'd 'e. (? & 'b) -> (('e & 'c) -> ('e | 'd) +//│ 'a :> forall 'b 'c 'd 'e. (#? & 'b) -> (('e & 'c) -> ('e | 'd) //│ where //│ 'a <: 'b -> 'c -> 'd) //│ ╙── @@ -572,7 +572,7 @@ rec def to_ch n = to_church = to_ch //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> forall 'b 'c 'd 'e. (? & 'b) -> (('e & 'c) -> ('e | 'd) +//│ 'a :> forall 'b 'c 'd 'e. (#? & 'b) -> (('e & 'c) -> ('e | 'd) //│ where //│ 'a <: 'b -> 'c -> 'd) //│ ╙── @@ -614,7 +614,7 @@ rec def to_ch_weird n = to_church = to_ch //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> forall 'b 'c 'd 'e. (? & 'b) -> (('e & 'c) -> ('e | 'd) +//│ 'a :> forall 'b 'c 'd 'e. (#? & 'b) -> (('e & 'c) -> ('e | 'd) //│ where //│ 'a <: 'b -> 'c -> 'd) //│ ╙── diff --git a/shared/src/test/diff/gadt/Exp1.mls b/shared/src/test/diff/gadt/Exp1.mls index 489ddea752..f08be7d36a 100644 --- a/shared/src/test/diff/gadt/Exp1.mls +++ b/shared/src/test/diff/gadt/Exp1.mls @@ -46,13 +46,10 @@ fun f(e) = if e is Pair(l: a, r) then let f(x: a) = x f(l) -//│ ╔══[ERROR] type identifier not found: a -//│ ║ l.47: let f(x: a) = x -//│ ╙── ^ //│ ╔══[ERROR] identifier not found: l //│ ║ l.48: f(l) //│ ╙── ^ -//│ fun f: Pair[anything, anything] -> error +//│ fun f: forall 'a. Pair['a, anything] -> (error | 'a) //│ Code generation encountered an error: //│ unresolved symbol l // fun f: forall 'lhs 'rhs. Pair['lhs, 'rhs] -> ('lhs, 'rhs,) diff --git a/shared/src/test/diff/gadt/ThisMatching.mls b/shared/src/test/diff/gadt/ThisMatching.mls index a279d6abd5..f27f1e5d20 100644 --- a/shared/src/test/diff/gadt/ThisMatching.mls +++ b/shared/src/test/diff/gadt/ThisMatching.mls @@ -165,11 +165,14 @@ class Pair(lhs: Exp, rhs: Exp) extends Exp //│ ╔══[ERROR] Indirectly-recursive member should have a type signature //│ ║ l.150: Pair(l, r) then l.test + r.test //│ ╙── ^^^^^ +//│ ╔══[ERROR] Indirectly-recursive member should have a type signature +//│ ║ l.150: Pair(l, r) then l.test + r.test +//│ ╙── ^^^^^ //│ abstract class Exp: Lit | Pair { -//│ fun test: Int | error +//│ fun test: Int //│ } //│ class Lit(n: Int) extends Exp { -//│ fun test: Int | error +//│ fun test: Int //│ } //│ class Pair(lhs: Exp, rhs: Exp) extends Exp @@ -184,17 +187,17 @@ abstract class Exp: (Pair | Lit) { class Lit(n: Int) extends Exp class Pair(lhs: Exp, rhs: Exp) extends Exp //│ ╔══[ERROR] Unhandled cyclic definition -//│ ║ l.178: abstract class Exp: (Pair | Lit) { +//│ ║ l.181: abstract class Exp: (Pair | Lit) { //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.179: fun test : Int +//│ ║ l.182: fun test : Int //│ ║ ^^^^^^^^^^^^^^^^ -//│ ║ l.180: fun test = if this is +//│ ║ l.183: fun test = if this is //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.181: Lit then 0 +//│ ║ l.184: Lit then 0 //│ ║ ^^^^^^^^^^^^^^ -//│ ║ l.182: Pair(l, r) then l.test + r.test +//│ ║ l.185: Pair(l, r) then l.test + r.test //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.183: } +//│ ║ l.186: } //│ ╙── ^ //│ abstract class Exp: Lit | Pair { //│ fun test: Int @@ -214,25 +217,25 @@ abstract class Exp[A]: (Pair | Lit) { class Lit(n: Int) extends Exp[Int] class Pair[L, R](lhs: L, rhs: R) extends Exp[[L, R]] //│ ╔══[ERROR] Unhandled cyclic definition -//│ ║ l.209: abstract class Exp[A]: (Pair | Lit) { +//│ ║ l.212: abstract class Exp[A]: (Pair | Lit) { //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.210: fun test = if this is +//│ ║ l.213: fun test = if this is //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.211: Lit then 0 +//│ ║ l.214: Lit then 0 //│ ║ ^^^^^^^^^^^^^^ -//│ ║ l.212: Pair then 1 +//│ ║ l.215: Pair then 1 //│ ║ ^^^^^^^^^^^^^^^ -//│ ║ l.213: } +//│ ║ l.216: } //│ ╙── ^ //│ ╔══[ERROR] Type error in `case` expression -//│ ║ l.210: fun test = if this is +//│ ║ l.213: fun test = if this is //│ ║ ^^^^^^^ -//│ ║ l.211: Lit then 0 +//│ ║ l.214: Lit then 0 //│ ║ ^^^^^^^^^^^^^^ -//│ ║ l.212: Pair then 1 +//│ ║ l.215: Pair then 1 //│ ║ ^^^^^^^^^^^^^^^ //│ ╟── type variable `L` leaks out of its scope -//│ ║ l.215: class Pair[L, R](lhs: L, rhs: R) extends Exp[[L, R]] +//│ ║ l.218: class Pair[L, R](lhs: L, rhs: R) extends Exp[[L, R]] //│ ╙── ^ //│ abstract class Exp[A]: Lit | Pair[anything, anything] { //│ fun test: 0 | 1 diff --git a/shared/src/test/diff/mlf-examples/ex_demo.mls b/shared/src/test/diff/mlf-examples/ex_demo.mls index cef2977fe3..a3b2f4d3d4 100644 --- a/shared/src/test/diff/mlf-examples/ex_demo.mls +++ b/shared/src/test/diff/mlf-examples/ex_demo.mls @@ -1073,7 +1073,7 @@ rec def c_fact_ n = (fun _ -> c_mul_ n (c_fact_ (c_pred_ n))) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: (forall 'b. ((forall 'c. ? -> 'c -> 'c) -> (forall 'c. ? -> 'c -> 'c) -> 'b) -> 'b) -> (forall 'd. 'd -> ? -> 'd) -> ((forall 'e. ? -> ? -> ((forall 'f. 'f -> 'f) -> 'e) -> 'e) -> (forall 'g. ((forall 'f. 'f -> 'f) -> 'g) -> ? -> 'g) -> (forall 'h 'i. ? -> ('h -> 'i) -> 'h -> 'i) -> (? -> 'j) -> 'k & (forall 'l. ((forall 'm 'n 'o 'p. ('m -> 'n -> 'o) -> ('p -> 'n & 'm) -> 'p -> 'o) -> 'k -> 'l) -> 'l) -> (forall 'c. ? -> 'c -> 'c) -> 'j & (forall 'q 'r 's 't 'u 'v. ((forall 'w. ? -> 'w -> 'w) -> ('q -> 'r -> 's & 't)) -> ('t -> (('u -> 'r & 'q) -> 'u -> 's) -> 'v) -> 'v) -> 'a) +//│ 'a <: (forall 'b. ((forall 'c. #? -> 'c -> 'c) -> (forall 'c. #? -> 'c -> 'c) -> 'b) -> 'b) -> (forall 'd. 'd -> #? -> 'd) -> ((forall 'e. #? -> #? -> ((forall 'f. 'f -> 'f) -> 'e) -> 'e) -> (forall 'g. ((forall 'f. 'f -> 'f) -> 'g) -> #? -> 'g) -> (forall 'h 'i. #? -> ('h -> 'i) -> 'h -> 'i) -> (#? -> 'j) -> 'k & (forall 'l. ((forall 'm 'n 'o 'p. ('m -> 'n -> 'o) -> ('p -> 'n & 'm) -> 'p -> 'o) -> 'k -> 'l) -> 'l) -> (forall 'c. #? -> 'c -> 'c) -> 'j & (forall 'q 'r 's 't 'u 'v. ((forall 'w. #? -> 'w -> 'w) -> ('q -> 'r -> 's & 't)) -> ('t -> (('u -> 'r & 'q) -> 'u -> 's) -> 'v) -> 'v) -> 'a) //│ ║ l.963: c_1_2_ (n s z) //│ ╙── ^^^ //│ c_fact_: 'a -> 'b @@ -1085,7 +1085,7 @@ rec def c_fact_ n = c_fact_A = c_fact_ //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: (forall 'b. ((forall 'c. ? -> 'c -> 'c) -> (forall 'c. ? -> 'c -> 'c) -> 'b) -> 'b) -> (forall 'd. 'd -> ? -> 'd) -> ((forall 'e. ? -> ? -> ((forall 'f. 'f -> 'f) -> 'e) -> 'e) -> (forall 'g. ((forall 'f. 'f -> 'f) -> 'g) -> ? -> 'g) -> (forall 'h 'i. ? -> ('h -> 'i) -> 'h -> 'i) -> (forall 'j. ? -> (? -> 'j -> 'j | 'k)) -> 'l & (forall 'm. ((forall 'n 'o 'p 'q. ('n -> 'o -> 'p) -> ('q -> 'o & 'n) -> 'q -> 'p) -> (forall 'r 's. ('r -> 's) -> 'r -> 's | 'l) -> 'm) -> 'm) -> (forall 'c. ? -> 'c -> 'c) -> 'k & (forall 't 'u 'v 'w 'x 'y. ((forall 'z. ? -> 'z -> 'z) -> ('t -> 'u -> 'v & 'w)) -> ('w -> (('x -> 'u & 't) -> 'x -> 'v) -> 'y) -> 'y) -> 'a) +//│ 'a <: (forall 'b. ((forall 'c. #? -> 'c -> 'c) -> (forall 'c. #? -> 'c -> 'c) -> 'b) -> 'b) -> (forall 'd. 'd -> #? -> 'd) -> ((forall 'e. #? -> #? -> ((forall 'f. 'f -> 'f) -> 'e) -> 'e) -> (forall 'g. ((forall 'f. 'f -> 'f) -> 'g) -> #? -> 'g) -> (forall 'h 'i. #? -> ('h -> 'i) -> 'h -> 'i) -> (forall 'j. #? -> (#? -> 'j -> 'j | 'k)) -> 'l & (forall 'm. ((forall 'n 'o 'p 'q. ('n -> 'o -> 'p) -> ('q -> 'o & 'n) -> 'q -> 'p) -> (forall 'r 's. ('r -> 's) -> 'r -> 's | 'l) -> 'm) -> 'm) -> (forall 'c. #? -> 'c -> 'c) -> 'k & (forall 't 'u 'v 'w 'x 'y. ((forall 'z. #? -> 'z -> 'z) -> ('t -> 'u -> 'v & 'w)) -> ('w -> (('x -> 'u & 't) -> 'x -> 'v) -> 'y) -> 'y) -> 'a) //│ ║ l.963: c_1_2_ (n s z) //│ ╙── ^^^ //│ 'a -> 'b @@ -1125,7 +1125,7 @@ def print_fact_ n = print_string "\n" //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: (forall 'b. ((forall 'c. ? -> 'c -> 'c) -> (forall 'c. ? -> 'c -> 'c) -> 'b) -> 'b) -> (forall 'd. 'd -> ? -> 'd) -> ((forall 'e. ? -> ? -> ((forall 'f. 'f -> 'f) -> 'e) -> 'e) -> (forall 'g. ((forall 'f. 'f -> 'f) -> 'g) -> ? -> 'g) -> (forall 'h 'i. ? -> ('h -> 'i) -> 'h -> 'i) -> (forall 'j. ? -> (? -> 'j -> 'j | 'k)) -> 'l & (forall 'm. ((forall 'n 'o 'p 'q. ('n -> 'o -> 'p) -> ('q -> 'o & 'n) -> 'q -> 'p) -> (forall 'r 's. ('r -> 's) -> 'r -> 's | 'l) -> 'm) -> 'm) -> (forall 'c. ? -> 'c -> 'c) -> 'k & (forall 't 'u 'v 'w 'x 'y. ((forall 'z. ? -> 'z -> 'z) -> ('t -> 'u -> 'v & 'w)) -> ('w -> (('x -> 'u & 't) -> 'x -> 'v) -> 'y) -> 'y) -> 'a) +//│ 'a <: (forall 'b. ((forall 'c. #? -> 'c -> 'c) -> (forall 'c. #? -> 'c -> 'c) -> 'b) -> 'b) -> (forall 'd. 'd -> #? -> 'd) -> ((forall 'e. #? -> #? -> ((forall 'f. 'f -> 'f) -> 'e) -> 'e) -> (forall 'g. ((forall 'f. 'f -> 'f) -> 'g) -> #? -> 'g) -> (forall 'h 'i. #? -> ('h -> 'i) -> 'h -> 'i) -> (forall 'j. #? -> (#? -> 'j -> 'j | 'k)) -> 'l & (forall 'm. ((forall 'n 'o 'p 'q. ('n -> 'o -> 'p) -> ('q -> 'o & 'n) -> 'q -> 'p) -> (forall 'r 's. ('r -> 's) -> 'r -> 's | 'l) -> 'm) -> 'm) -> (forall 'c. #? -> 'c -> 'c) -> 'k & (forall 't 'u 'v 'w 'x 'y. ((forall 'z. #? -> 'z -> 'z) -> ('t -> 'u -> 'v & 'w)) -> ('w -> (('x -> 'u & 't) -> 'x -> 'v) -> 'y) -> 'y) -> 'a) //│ ║ l.963: c_1_2_ (n s z) //│ ╙── ^^^ //│ ╔══[ERROR] Cyclic-looking constraint while typing application; a type annotation may be required @@ -1160,7 +1160,7 @@ def print_fact2_ n = (c_printint2_ (c_fact_ (to_church_ n))) )) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: (forall 'b. ((forall 'c. ? -> 'c -> 'c) -> (forall 'c. ? -> 'c -> 'c) -> 'b) -> 'b) -> (forall 'd. 'd -> ? -> 'd) -> ((forall 'e. ? -> ? -> ((forall 'f. 'f -> 'f) -> 'e) -> 'e) -> (forall 'g. ((forall 'f. 'f -> 'f) -> 'g) -> ? -> 'g) -> (forall 'h 'i. ? -> ('h -> 'i) -> 'h -> 'i) -> (forall 'j. ? -> (? -> 'j -> 'j | 'k)) -> 'l & (forall 'm. ((forall 'n 'o 'p 'q. ('n -> 'o -> 'p) -> ('q -> 'o & 'n) -> 'q -> 'p) -> (forall 'r 's. ('r -> 's) -> 'r -> 's | 'l) -> 'm) -> 'm) -> (forall 'c. ? -> 'c -> 'c) -> 'k & (forall 't 'u 'v 'w 'x 'y. ((forall 'z. ? -> 'z -> 'z) -> ('t -> 'u -> 'v & 'w)) -> ('w -> (('x -> 'u & 't) -> 'x -> 'v) -> 'y) -> 'y) -> 'a) +//│ 'a <: (forall 'b. ((forall 'c. #? -> 'c -> 'c) -> (forall 'c. #? -> 'c -> 'c) -> 'b) -> 'b) -> (forall 'd. 'd -> #? -> 'd) -> ((forall 'e. #? -> #? -> ((forall 'f. 'f -> 'f) -> 'e) -> 'e) -> (forall 'g. ((forall 'f. 'f -> 'f) -> 'g) -> #? -> 'g) -> (forall 'h 'i. #? -> ('h -> 'i) -> 'h -> 'i) -> (forall 'j. #? -> (#? -> 'j -> 'j | 'k)) -> 'l & (forall 'm. ((forall 'n 'o 'p 'q. ('n -> 'o -> 'p) -> ('q -> 'o & 'n) -> 'q -> 'p) -> (forall 'r 's. ('r -> 's) -> 'r -> 's | 'l) -> 'm) -> 'm) -> (forall 'c. #? -> 'c -> 'c) -> 'k & (forall 't 'u 'v 'w 'x 'y. ((forall 'z. #? -> 'z -> 'z) -> ('t -> 'u -> 'v & 'w)) -> ('w -> (('x -> 'u & 't) -> 'x -> 'v) -> 'y) -> 'y) -> 'a) //│ ║ l.963: c_1_2_ (n s z) //│ ╙── ^^^ //│ ╔══[ERROR] Cyclic-looking constraint while typing application; a type annotation may be required @@ -1276,7 +1276,7 @@ c_i9_ = c_pred_ c_i10_ c_99_ = c_add_ (c_mul_ c_i9_ c_i10_) c_i9_ //│ ╔══[ERROR] Inferred recursive type: 'b //│ where -//│ 'b <: (forall 'c 'd 'e 'f. ('c -> 'd -> 'e) -> ('f -> 'd & 'c) -> 'f -> 'e) -> ((forall 'a 'g 'a0 'a1 'a2. (('a | 'g) -> 'a & ('a0 | 'g) -> 'a0 & ('a1 | 'g) -> 'a1 & ('a2 | 'g) -> 'a2) -> 'g -> ('a | 'a0 | 'a1 | 'a2) | Fint) -> ? & (forall 'a3 'h 'a4. (('a3 | 'h) -> 'a3 & ('a4 | 'h) -> 'a4) -> 'h -> ('a3 | 'a4) | Fint) -> anything) +//│ 'b <: (forall 'c 'd 'e 'f. ('c -> 'd -> 'e) -> ('f -> 'd & 'c) -> 'f -> 'e) -> ((forall 'a 'g 'a0 'a1 'a2. (('a | 'g) -> 'a & ('a0 | 'g) -> 'a0 & ('a1 | 'g) -> 'a1 & ('a2 | 'g) -> 'a2) -> 'g -> ('a | 'a0 | 'a1 | 'a2) | Fint) -> #? & (forall 'a3 'h 'a4. (('a3 | 'h) -> 'a3 & ('a4 | 'h) -> 'a4) -> 'h -> ('a3 | 'a4) | Fint) -> anything) //│ ║ l.903: def c_succ_ n = fun f -> fun x -> n f (f x) //│ ╙── ^^^ //│ ╔══[ERROR] Cyclic-looking constraint while typing application; a type annotation may be required diff --git a/shared/src/test/diff/mlf-examples/ex_predicative.mls b/shared/src/test/diff/mlf-examples/ex_predicative.mls index e69de0364a..3321742ad8 100644 --- a/shared/src/test/diff/mlf-examples/ex_predicative.mls +++ b/shared/src/test/diff/mlf-examples/ex_predicative.mls @@ -197,15 +197,15 @@ t id succ 0 def t_ y = (fun h -> h (h (h (fun x -> y)))) (fun f -> fun n -> n (fun v -> k2) k app (fun g -> fun x -> n (f (n (fun p -> fun s -> s (p k2) (fun f -> fun x -> f (p k2 f x))) (fun s -> s k2 k2) k) g) x)) two //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: ? -> (forall 'b. 'b) -> 'c -//│ 'b :> forall 'd 'e. ((forall 'f. ? -> 'f -> 'f) -> (forall 'f. ? -> 'f -> 'f) -> 'd & 'e) -> (? -> 'e | 'd) | 'c +//│ 'a <: #? -> (forall 'b. 'b) -> 'c +//│ 'b :> forall 'd 'e. ((forall 'f. #? -> 'f -> 'f) -> (forall 'f. #? -> 'f -> 'f) -> 'd & 'e) -> (#? -> 'e | 'd) | 'c //│ 'c :> 'g -//│ <: (forall 'f. ? -> 'f -> 'f) -> (? -> ? -> ? & 'h) +//│ <: (forall 'f. #? -> 'f -> 'f) -> (#? -> #? -> #? & 'h) //│ 'g :> forall 'b 'i. 'i -> 'i | 'b -//│ <: (forall 'f. ? -> 'f -> 'f) -> (? -> ? -> ? & 'h) -//│ 'h <: (forall 'j. ? -> ? -> 'j -> 'j) -> (forall 'k. 'k -> ? -> 'k) -> (forall 'l 'm. ('l -> 'm) -> 'l -> 'm) -> (? -> 'n -> 'g) -> 'a & (forall 'o 'p 'q 'r 's. ((forall 'f. ? -> 'f -> 'f) -> ('o -> 'p -> 'q & 'r)) -> ('r -> (forall 't. ('q -> 't & 'o) -> 'p -> 't) -> 's) -> 's) -> (forall 'u. ((forall 'f. ? -> 'f -> 'f) -> (forall 'f. ? -> 'f -> 'f) -> 'u) -> 'u) -> (forall 'k. 'k -> ? -> 'k) -> ? & ? -> 'n -> 'g +//│ <: (forall 'f. #? -> 'f -> 'f) -> (#? -> #? -> #? & 'h) +//│ 'h <: (forall 'j. #? -> #? -> 'j -> 'j) -> (forall 'k. 'k -> #? -> 'k) -> (forall 'l 'm. ('l -> 'm) -> 'l -> 'm) -> (#? -> 'n -> 'g) -> 'a & (forall 'o 'p 'q 'r 's. ((forall 'f. #? -> 'f -> 'f) -> ('o -> 'p -> 'q & 'r)) -> ('r -> (forall 't. ('q -> 't & 'o) -> 'p -> 't) -> 's) -> 's) -> (forall 'u. ((forall 'f. #? -> 'f -> 'f) -> (forall 'f. #? -> 'f -> 'f) -> 'u) -> 'u) -> (forall 'k. 'k -> #? -> 'k) -> #? & #? -> 'n -> 'g //│ 'n :> forall 'b. 'b -//│ <: ? & 'g +//│ <: #? & 'g //│ ║ l.197: def t_ y = (fun h -> h (h (h (fun x -> y)))) (fun f -> fun n -> n (fun v -> k2) k app (fun g -> fun x -> n (f (n (fun p -> fun s -> s (p k2) (fun f -> fun x -> f (p k2 f x))) (fun s -> s k2 k2) k) g) x)) two //│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ ╔══[ERROR] Cyclic-looking constraint while typing application; a type annotation may be required @@ -283,7 +283,7 @@ def t y = (fun h -> h (h (h (fun x -> y)))) (fun f -> fun (n: ChurchInt) -> n (f :Fuel 6000 :e // occurs-check def t_ y = (fun h -> h (h (h (fun x -> y)))) (fun f -> fun n -> n (fun v -> k2) k app (fun g -> fun x -> n (f (n (fun p -> fun s -> s (p k2) (fun f -> fun x -> f (p k2 f x))) (fun s -> s k2 k2) k) g) x)) three -//│ ╔══[ERROR] Inferred recursive type: ? -> (((forall 'a. nothing -> ('a -> 'a | ?) | ?) | 'b) -> ((forall 'c. ? -> 'c -> 'c) -> nothing & 'd) & (forall 'e 'f. ((forall 'c. ? -> 'c -> 'c) -> (forall 'c. ? -> 'c -> 'c) -> 'e & 'f) -> (? -> 'f | 'e) | ? | 'd) -> ((forall 'c. ? -> 'c -> 'c) -> nothing & 'b)) +//│ ╔══[ERROR] Inferred recursive type: #? -> (((forall 'a. nothing -> ('a -> 'a | #?) | #?) | 'b) -> ((forall 'c. #? -> 'c -> 'c) -> nothing & 'd) & (forall 'e 'f. ((forall 'c. #? -> 'c -> 'c) -> (forall 'c. #? -> 'c -> 'c) -> 'e & 'f) -> (#? -> 'f | 'e) | #? | 'd) -> ((forall 'c. #? -> 'c -> 'c) -> nothing & 'b)) //│ ║ l.285: def t_ y = (fun h -> h (h (h (fun x -> y)))) (fun f -> fun n -> n (fun v -> k2) k app (fun g -> fun x -> n (f (n (fun p -> fun s -> s (p k2) (fun f -> fun x -> f (p k2 f x))) (fun s -> s k2 k2) k) g) x)) three //│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ t_: ('a -> ((forall 'b 'c. ((forall 'd. anything -> 'd -> 'd) -> (forall 'd. anything -> 'd -> 'd) -> 'b & 'c) -> (anything -> 'c | 'b) | 'e | 'f | 'g | 'h | 'i | 'j) -> 'g & 'k)) -> ('a & 'l) -> ((forall 'd. anything -> 'd -> 'd) -> ((forall 'm 'n 'o 'p 'q 'r. ((forall 'd. anything -> 'd -> 'd) -> ('m -> 'n -> 'o & 'p)) -> ('p -> (forall 's. ('o -> 's & 'm) -> 'n -> 's) -> 'q) -> ('r -> 'r | 'q) | 'k | 't) -> (forall 'u 'v. ((forall 'd. anything -> 'd -> 'd) -> (forall 'd. anything -> 'd -> 'd) -> 'u & 'v) -> (anything -> 'v | 'u) | 'f | 'g | 'h | 'i | 'w) -> 'e & 'x) & 'i) -> ('g | 'h) @@ -314,7 +314,7 @@ t_ id succ 0 //│ ╔══[ERROR] Inferred recursive type: 'a //│ where //│ 'a :> int -> int -//│ <: (forall 'b 'c 'd 'e 'f 'g 'h. ((forall 'i. ? -> 'i -> 'i) -> (forall 'i. ? -> 'i -> 'i) -> 'b & 'c) -> (? -> 'c | 'b) | ((forall 'i. ? -> 'i -> 'i) -> (forall 'i. ? -> 'i -> 'i) -> 'd & 'e & 'f) -> (? -> 'f | 'e | 'd) | nothing -> ('g -> 'g | ?) | 'j | ? | nothing -> ('h -> 'h | ?)) -> nothing +//│ <: (forall 'b 'c 'd 'e 'f 'g 'h. ((forall 'i. #? -> 'i -> 'i) -> (forall 'i. #? -> 'i -> 'i) -> 'b & 'c) -> (#? -> 'c | 'b) | ((forall 'i. #? -> 'i -> 'i) -> (forall 'i. #? -> 'i -> 'i) -> 'd & 'e & 'f) -> (#? -> 'f | 'e | 'd) | nothing -> ('g -> 'g | #?) | 'j | #? | nothing -> ('h -> 'h | #?)) -> nothing //│ ║ l.285: def t_ y = (fun h -> h (h (h (fun x -> y)))) (fun f -> fun n -> n (fun v -> k2) k app (fun g -> fun x -> n (f (n (fun p -> fun s -> s (p k2) (fun f -> fun x -> f (p k2 f x))) (fun s -> s k2 k2) k) g) x)) three //│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ ╔══[ERROR] Type mismatch in application: @@ -372,7 +372,7 @@ def t (z: nothing) = let x = fun (y: forall 't. 'a -> 't) -> y z in x x :e (fun f -> fun x -> f (f x)) (fun f -> fun x -> f (f x)) (fun v -> fun w -> v) -//│ ╔══[ERROR] Inferred recursive type: ? -> ? -> ? +//│ ╔══[ERROR] Inferred recursive type: #? -> #? -> #? //│ ║ l.374: (fun f -> fun x -> f (f x)) (fun f -> fun x -> f (f x)) (fun v -> fun w -> v) //│ ╙── ^^^ //│ res: 'a -> anything -> 'b @@ -396,7 +396,7 @@ def t (z: nothing) = let x = fun (y: forall 't. 'a -> 't) -> y z in x x :e (fun two -> fun k -> two two k) (fun f -> fun x -> f (f x)) (fun v -> fun w -> v) -//│ ╔══[ERROR] Inferred recursive type: ? -> ? -> ? +//│ ╔══[ERROR] Inferred recursive type: #? -> #? -> #? //│ ║ l.398: (fun two -> fun k -> two two k) (fun f -> fun x -> f (f x)) (fun v -> fun w -> v) //│ ╙── ^^^ //│ res: 'a -> anything -> 'b @@ -421,9 +421,9 @@ def t (z: nothing) = let x = fun (y: forall 't. 'a -> 't) -> y z in x x // :d :e (fun two -> fun k -> two two two k) (fun f -> fun x -> f (f x)) (fun v -> fun w -> v) -//│ ╔══[ERROR] Inferred recursive type: ? -> 'a +//│ ╔══[ERROR] Inferred recursive type: #? -> 'a //│ where -//│ 'a :> ? -> ('a | ?) +//│ 'a :> #? -> ('a | #?) //│ ║ l.423: (fun two -> fun k -> two two two k) (fun f -> fun x -> f (f x)) (fun v -> fun w -> v) //│ ╙── ^^^ //│ res: 'a -> anything -> 'b @@ -502,10 +502,10 @@ def t (z: nothing) = let x = fun (y: forall 't. 'a -> 't) -> y z in x x (fun h -> (fun x -> h (x x)) (fun x -> h (x x))) (fun f -> fun n -> n (fun v -> fun x -> fun y -> y) k (fun f -> fun x -> f x)(fun g -> fun x -> n (f (n (fun p -> fun s -> s (p (fun x -> fun y -> y)) (fun f -> fun x -> f (p (fun x -> fun y -> y) f x))) (fun s -> s (fun f -> fun x -> x) (fun f -> fun x -> x)) k) g) x)) (fun f -> fun x -> f (f x)) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: (nothing -> ('b | 'c) | 'd) -> 'e & (forall 'f 'g 'h 'i 'j. ((forall 'k. ? -> 'k -> 'k) -> 'f & (forall 'l. ? -> 'l -> 'l) -> 'g -> 'h -> 'i) -> ('f -> (forall 'm. ('i -> 'm & 'g) -> 'h -> 'm) -> 'j) -> 'j) -> (forall 'n. ((forall 'o. ? -> 'o -> 'o) -> (forall 'p. ? -> 'p -> 'p) -> 'n) -> 'n) -> (forall 'q. 'q -> ? -> 'q) -> 'a & (forall 'r. ? -> ? -> 'r -> 'r) -> (forall 'q. 'q -> ? -> 'q) -> (forall 's 't. ('s -> 't) -> 's -> 't) -> (((forall 'u. ? -> ? -> 'u -> 'u | ?) -> ((nothing -> ? -> ?) -> 'e & 'b) & (forall 'v. ? -> ? -> 'v -> 'v | ?) -> ((nothing -> ? -> ?) -> 'e & 'b) & (forall 'w. ? -> ? -> 'w -> 'w) -> (nothing -> ? -> ?) -> 'e & (forall 'x. ? -> ? -> 'x -> 'x | ?) -> ((nothing -> ? -> ?) -> 'e & 'b) & (forall 'y. ? -> ? -> 'y -> 'y | ?) -> ((nothing -> ? -> ?) -> 'e & 'b) & 'd & 'z) -> nothing -> 'c) -> 'z -> ((forall 'a1. ? -> ? -> 'a1 -> 'a1) -> (nothing -> ? -> ?) -> 'e & 'd) -//│ 'c :> forall 'b1 'c1. (? & 'b1) -> (? -> 'c1 -> 'c1 | 'b1 | ?) -//│ <: (nothing -> ? -> ?) -> 'e -//│ 'e <: (forall 'd1. ? -> ? -> 'd1 -> 'd1 | ?) -> 'c +//│ 'a <: (nothing -> ('b | 'c) | 'd) -> 'e & (forall 'f 'g 'h 'i 'j. ((forall 'k. #? -> 'k -> 'k) -> 'f & (forall 'l. #? -> 'l -> 'l) -> 'g -> 'h -> 'i) -> ('f -> (forall 'm. ('i -> 'm & 'g) -> 'h -> 'm) -> 'j) -> 'j) -> (forall 'n. ((forall 'o. #? -> 'o -> 'o) -> (forall 'p. #? -> 'p -> 'p) -> 'n) -> 'n) -> (forall 'q. 'q -> #? -> 'q) -> 'a & (forall 'r. #? -> #? -> 'r -> 'r) -> (forall 'q. 'q -> #? -> 'q) -> (forall 's 't. ('s -> 't) -> 's -> 't) -> (((forall 'u. #? -> #? -> 'u -> 'u | #?) -> ((nothing -> #? -> #?) -> 'e & 'b) & (forall 'v. #? -> #? -> 'v -> 'v | #?) -> ((nothing -> #? -> #?) -> 'e & 'b) & (forall 'w. #? -> #? -> 'w -> 'w) -> (nothing -> #? -> #?) -> 'e & (forall 'x. #? -> #? -> 'x -> 'x | #?) -> ((nothing -> #? -> #?) -> 'e & 'b) & (forall 'y. #? -> #? -> 'y -> 'y | #?) -> ((nothing -> #? -> #?) -> 'e & 'b) & 'd & 'z) -> nothing -> 'c) -> 'z -> ((forall 'a1. #? -> #? -> 'a1 -> 'a1) -> (nothing -> #? -> #?) -> 'e & 'd) +//│ 'c :> forall 'b1 'c1. (#? & 'b1) -> (#? -> 'c1 -> 'c1 | 'b1 | #?) +//│ <: (nothing -> #? -> #?) -> 'e +//│ 'e <: (forall 'd1. #? -> #? -> 'd1 -> 'd1 | #?) -> 'c //│ ║ l.502: (fun h -> (fun x -> h (x x)) (fun x -> h (x x))) (fun f -> fun n -> n (fun v -> fun x -> fun y -> y) k (fun f -> fun x -> f x)(fun g -> fun x -> n (f (n (fun p -> fun s -> s (p (fun x -> fun y -> y)) (fun f -> fun x -> f (p (fun x -> fun y -> y) f x))) (fun s -> s (fun f -> fun x -> x) (fun f -> fun x -> x)) k) g) x)) (fun f -> fun x -> f (f x)) //│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ ╔══[ERROR] Cyclic-looking constraint while typing application; a type annotation may be required diff --git a/shared/src/test/diff/mlf-examples/ex_selfapp.mls b/shared/src/test/diff/mlf-examples/ex_selfapp.mls index 47e22ccbdb..8b121a3873 100644 --- a/shared/src/test/diff/mlf-examples/ex_selfapp.mls +++ b/shared/src/test/diff/mlf-examples/ex_selfapp.mls @@ -135,7 +135,7 @@ def build_ = fun g -> g (fun x -> fun xs -> Cons (x, xs)) Nil build_ : forall 'a. (forall 'b. (('a -> 'b -> 'b) -> 'b -> 'b)) -> List['a] //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> Cons[?] with {tail: forall 'a. Nil | 'a} +//│ 'a :> Cons[#?] with {tail: forall 'a. Nil | 'a} //│ ║ l.130: def build_ = fun g -> g (fun x -> fun xs -> Cons (x, xs)) Nil //│ ╙── ^^^^^^^^^^^^ //│ ╔══[ERROR] Cyclic-looking constraint while typing type ascription; a type annotation may be required @@ -149,7 +149,7 @@ build_ : forall 'a. (forall 'b. (('a -> 'b -> 'b) -> 'b -> 'b)) -> List['a] def build = fun (g: forall 'b. ('a -> 'b -> 'b) -> 'b -> 'b) -> g (fun x -> fun xs -> Cons (x, xs)) Nil //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a :> Cons[?] with {tail: forall 'a. Nil | 'a} +//│ 'a :> Cons[#?] with {tail: forall 'a. Nil | 'a} //│ ║ l.149: def build = fun (g: forall 'b. ('a -> 'b -> 'b) -> 'b -> 'b) -> g (fun x -> fun xs -> Cons (x, xs)) Nil //│ ╙── ^^^^^^^^^^^^ //│ ╔══[ERROR] Cyclic-looking constraint while typing application; a type annotation may be required @@ -212,7 +212,7 @@ rec def foldr = fun k -> fun z -> fun xs -> Cons -> k xs.head (foldr k z xs.tail) //│ ╔══[ERROR] Inferred recursive type: 'a //│ where -//│ 'a <: {head: ?, tail: Cons[?] & 'a} +//│ 'a <: {head: #?, tail: Cons[?] & 'a} //│ ║ l.210: case xs of //│ ╙── ^^ //│ foldr: ('head -> 'a -> 'a) -> 'a -> 'b -> 'a @@ -491,7 +491,7 @@ k = k_ // nope //│ 'c :> 'e -> 'f -> 'd //│ <: 'g //│ 'e :> int -> 'g -> 'e -> 'f -> 'd -//│ <: int -> 'a & ? -> 'b -> 'b +//│ <: int -> 'a & #? -> 'b -> 'b //│ 'b :> 'e -> 'f -> 'd //│ <: 'g //│ 'g <: (int -> 'g -> 'e -> 'f -> 'd) -> Baa -> 'h @@ -516,7 +516,7 @@ k = k_ // nope rec def k_ = fun x -> fun xs -> fun c -> fun n -> c (x + 1) (xs k_ z_ c n) //│ ╔══[ERROR] Inferred recursive type: 'k_ //│ where -//│ 'k_ :> int -> ('k_ -> (forall 'a. ? -> 'a -> 'a) -> 'b -> 'c -> 'd) -> (int -> 'd -> 'e & 'b) -> 'c -> 'e +//│ 'k_ :> int -> ('k_ -> (forall 'a. #? -> 'a -> 'a) -> 'b -> 'c -> 'd) -> (int -> 'd -> 'e & 'b) -> 'c -> 'e //│ ╙── //│ k_: 'k_ //│ where diff --git a/shared/src/test/diff/mlscript/OccursCheck.mls b/shared/src/test/diff/mlscript/OccursCheck.mls index 86d6ca94f3..ea05c96fc8 100644 --- a/shared/src/test/diff/mlscript/OccursCheck.mls +++ b/shared/src/test/diff/mlscript/OccursCheck.mls @@ -14,7 +14,7 @@ rec def f x = f x rec def f x = f //│ ╔══[ERROR] Inferred recursive type: 'f //│ where -//│ 'f :> ? -> 'f +//│ 'f :> #? -> 'f //│ ╙── //│ f: 'f //│ where diff --git a/shared/src/test/diff/mlscript/Scratch.mls b/shared/src/test/diff/mlscript/Scratch.mls index e69de29bb2..72784a52f1 100644 --- a/shared/src/test/diff/mlscript/Scratch.mls +++ b/shared/src/test/diff/mlscript/Scratch.mls @@ -0,0 +1,6 @@ + +class Foo +//│ Defined class Foo + + + diff --git a/shared/src/test/diff/nu/AsOp.mls b/shared/src/test/diff/nu/AsOp.mls new file mode 100644 index 0000000000..4802824257 --- /dev/null +++ b/shared/src/test/diff/nu/AsOp.mls @@ -0,0 +1,64 @@ +:NewDefs + +abstract class Foo[type T]: Bar | Baz +class Bar extends Foo[Int] +class Baz[T](val x: Foo[T]) extends Foo[[T]] +//│ abstract class Foo[T]: Bar | Baz[?] +//│ class Bar extends Foo { +//│ constructor() +//│ } +//│ class Baz[T](x: Foo[T]) extends Foo + +// TODO +fun foo: Foo['T] -> Int +fun foo[T](f: Foo[T]): Int = if f is + Bar then 0 + Baz(x) then foo(x as Foo[x.T]) +//│ ╔══[ERROR] Type error in `case` expression +//│ ║ l.14: fun foo[T](f: Foo[T]): Int = if f is +//│ ║ ^^^^ +//│ ║ l.15: Bar then 0 +//│ ║ ^^^^^^^^^^^^^^ +//│ ║ l.16: Baz(x) then foo(x as Foo[x.T]) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── type variable `T` leaks out of its scope +//│ ║ l.5: class Baz[T](val x: Foo[T]) extends Foo[[T]] +//│ ╙── ^ +//│ fun foo: forall 'T. (f: Foo['T]) -> Int +//│ fun foo: forall 'T0. Foo['T0] -> Int + +1 as Int +"hi" as Str +//│ Str +//│ res +//│ = 1 +//│ res +//│ = 'hi' + +:e +1 as 2 +"hello" as Int +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.39: 1 as 2 +//│ ║ ^ +//│ ╟── integer literal of type `1` does not match type `2` +//│ ╟── Note: constraint arises from literal type: +//│ ║ l.39: 1 as 2 +//│ ╙── ^ +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.40: "hello" as Int +//│ ║ ^^^^^^^ +//│ ╟── string literal of type `"hello"` is not an instance of type `Int` +//│ ╟── Note: constraint arises from type reference: +//│ ║ l.40: "hello" as Int +//│ ╙── ^^^ +//│ Int +//│ res +//│ = 1 +//│ res +//│ = 'hello' + +0as Int +//│ Int +//│ res +//│ = 0 diff --git a/shared/src/test/diff/nu/BasicClasses.mls b/shared/src/test/diff/nu/BasicClasses.mls index 7d85a1150f..f55d2ca385 100644 --- a/shared/src/test/diff/nu/BasicClasses.mls +++ b/shared/src/test/diff/nu/BasicClasses.mls @@ -204,7 +204,74 @@ r.n //│ res //│ = 0 +:d r.go.n +//│ 0. Typing TypingUnit(List(Sel(Sel(Var(r),Var(go)),Var(n)))) +//│ | Typing unit statements +//│ | | 0. Typing term Sel(Sel(Var(r),Var(go)),Var(n)) +//│ | | | 0. Typing term Sel(Var(r),Var(go)) +//│ | | | | 0. Typing term Var(r) +//│ | | | | 0. : α179 +//│ | | | | CONSTRAIN α179 Rec <: {n: n181} & r180 +//│ r180 :> Rec +//│ n181 :> Int +//│ | | | | 0. C α179 {}) {} <: DNF(0, {go: go184}) +//│ | | | | | | | | | Possible: List({go: go184}) +//│ | | | | | | | | | 0. A #Rec{} % List() {} % List() {} % List() Rec <: go177'' +//│ go177'' :> Rec +//│ | | | | | | | | | | | | | Fresh[0] Rec.go : Some(‹∀ 1. α176''›) where Some( +//│ α176'' :> Rec <: go177'' +//│ go177'' :> Rec) +//│ | | | | | | | | | | | | | & None (from refinement) +//│ | | | | | | | | | | | | 0. C ‹∀ 1. α176''› Rec <: go177'' +//│ go177'' :> Rec +//│ go184 :> ‹∀ 1. α176''› +//│ | | | 0. C go184 {}) {} <: DNF(0, {n: n185}) +//│ | | | | | | | | | | Possible: List({n: n185}) +//│ | | | | | | | | | | 0. A #Rec{} % List() {} % List() {} % List() Int //│ Int //│ res //│ = 1 @@ -220,13 +287,13 @@ class Annots(base: 0 | 1) { //│ ╔══[WARNING] Expression in statement position should have type `()`. //│ ╟── Use a comma expression `... , ()` to explicitly discard non-unit values, making your intent clearer. //│ ╟── Type mismatch in type ascription: -//│ ║ l.217: a: Int +//│ ║ l.284: a: Int //│ ║ ^ //│ ╟── type `Int` does not match type `()` -//│ ║ l.217: a: Int +//│ ║ l.284: a: Int //│ ║ ^^^ //│ ╟── but it flows into expression in statement position with expected type `()` -//│ ║ l.217: a: Int +//│ ║ l.284: a: Int //│ ╙── ^ //│ class Annots(base: 0 | 1) { //│ fun a: 0 | 1 diff --git a/shared/src/test/diff/nu/CaseExpr.mls b/shared/src/test/diff/nu/CaseExpr.mls index 5b317fe937..40af35fb34 100644 --- a/shared/src/test/diff/nu/CaseExpr.mls +++ b/shared/src/test/diff/nu/CaseExpr.mls @@ -59,13 +59,20 @@ map(succ) of None //│ = None { class: [class None extends Option] } -:e // TODO support +// :pe // TODO support +// :e +// :w + +// TODO :: here `as` is used as @ fun map(f) = case Some(x) then Some(f(x)) None as n then n -//│ ╔══[ERROR] Illegal pattern `as` -//│ ║ l.65: None as n then n -//│ ╙── ^^ +//│ ╔══[PARSE ERROR] Expected an expression; found a 'then'/'else' clause instead +//│ ║ l.69: None as n then n +//│ ╙── ^^^^^^^^ +//│ ╔══[ERROR] Illegal interleaved statement Asc(Var(None),Literal(UnitLit(true))) +//│ ║ l.69: None as n then n +//│ ╙── ^^^^ //│ fun map: anything -> anything -> error //│ Code generation encountered an error: //│ if expression was not desugared @@ -74,10 +81,10 @@ fun map(f) = case :pe case 1 //│ ╔══[PARSE ERROR] Expected 'then'/'else' clause after 'case'; found integer literal instead -//│ ║ l.75: case 1 +//│ ║ l.82: case 1 //│ ║ ^ //│ ╟── Note: 'case' expression starts here: -//│ ║ l.75: case 1 +//│ ║ l.82: case 1 //│ ╙── ^^^^ //│ anything -> 1 //│ res @@ -86,13 +93,13 @@ case 1 :pe case (1 then true) //│ ╔══[PARSE ERROR] Unexpected 'then' keyword here -//│ ║ l.87: case (1 then true) +//│ ║ l.94: case (1 then true) //│ ╙── ^^^^ //│ ╔══[PARSE ERROR] Expected 'then'/'else' clause after 'case'; found integer literal instead -//│ ║ l.87: case (1 then true) +//│ ║ l.94: case (1 then true) //│ ║ ^^^^^^^^^^^^^ //│ ╟── Note: 'case' expression starts here: -//│ ║ l.87: case (1 then true) +//│ ║ l.94: case (1 then true) //│ ╙── ^^^^ //│ anything -> 1 //│ res @@ -106,16 +113,16 @@ case else 0 :pe case then 1 else 0 //│ ╔══[PARSE ERROR] Unexpected 'then' keyword in expression position -//│ ║ l.107: case then 1 else 0 +//│ ║ l.114: case then 1 else 0 //│ ╙── ^^^^ //│ ╔══[PARSE ERROR] Expected 'then'/'else' clause after 'case'; found integer literal instead -//│ ║ l.107: case then 1 else 0 +//│ ║ l.114: case then 1 else 0 //│ ║ ^ //│ ╟── Note: 'case' expression starts here: -//│ ║ l.107: case then 1 else 0 +//│ ║ l.114: case then 1 else 0 //│ ╙── ^^^^ //│ ╔══[PARSE ERROR] Expected end of input; found 'else' keyword instead -//│ ║ l.107: case then 1 else 0 +//│ ║ l.114: case then 1 else 0 //│ ╙── ^^^^ //│ anything -> 1 //│ res @@ -129,16 +136,16 @@ case then 1 else 0 :e case x, y then x + y //│ ╔══[PARSE ERROR] Expected an expression; found a 'then'/'else' clause instead -//│ ║ l.130: case x, y then x + y +//│ ║ l.137: case x, y then x + y //│ ╙── ^^^^^^^^^^^^ //│ ╔══[PARSE ERROR] Expected 'then'/'else' clause after 'case'; found operator application instead -//│ ║ l.130: case x, y then x + y +//│ ║ l.137: case x, y then x + y //│ ║ ^^^^^^^^^^^^^^^ //│ ╟── Note: 'case' expression starts here: -//│ ║ l.130: case x, y then x + y +//│ ║ l.137: case x, y then x + y //│ ╙── ^^^^ //│ ╔══[ERROR] identifier not found: x -//│ ║ l.130: case x, y then x + y +//│ ║ l.137: case x, y then x + y //│ ╙── ^ //│ anything -> () //│ Code generation encountered an error: @@ -147,7 +154,7 @@ case x, y then x + y :e case (x, y) then x + y //│ ╔══[ERROR] Illegal pattern `,` -//│ ║ l.148: case (x, y) then x + y +//│ ║ l.155: case (x, y) then x + y //│ ╙── ^^^^ //│ anything -> error //│ Code generation encountered an error: diff --git a/shared/src/test/diff/nu/ClassesInMixins.mls b/shared/src/test/diff/nu/ClassesInMixins.mls index ca2f3c647f..4fe735c80e 100644 --- a/shared/src/test/diff/nu/ClassesInMixins.mls +++ b/shared/src/test/diff/nu/ClassesInMixins.mls @@ -29,7 +29,7 @@ M.f.n :e M.Foo -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member Foo not yet supported //│ ║ l.31: M.Foo //│ ╙── ^^^^ //│ error diff --git a/shared/src/test/diff/nu/Eval.mls b/shared/src/test/diff/nu/Eval.mls index 7f3886971e..65a8a3b56f 100644 --- a/shared/src/test/diff/nu/Eval.mls +++ b/shared/src/test/diff/nu/Eval.mls @@ -260,11 +260,11 @@ fun eval(t, env) = if t is else err(String(pree) ++ " does not have field " ++ nme) Rcd(fs) then Rcd of fs |> Lists.map of {key, value} => {key, value: eval(value, env)} -//│ fun eval: forall 'a 'b 'c. ('a, Cons[{key: Eql[Str], value: 'b}] & {List#A <: {key: Eql[Str], value: 'b}} & List[{key: Eql[Str], value: 'b}] | Nil & {List#A <: {key: Eql[Str], value: 'b}} & List[{key: Eql[Str], value: 'b}]) -> 'c +//│ fun eval: forall 'a 'b 'c. ('a, Cons[{key: Eql[Str], value: 'b}] & {List#A <: {key: Eql[Str], value: 'b}} & List[{key: Eql[Str], value: 'b}] | Nil & {List#A <: {key: Eql[Str], value: 'b}} & List[{key: Eql[Str], value: 'b}]) -> ('b | 'c) //│ where //│ 'b :> 'c //│ <: Object & ~#Rcd | Rcd['b] -//│ 'c :> Lam | Lit[??A] | Rcd[Lam | Lit[??A] | 'c] | 'b +//│ 'c :> Lam | Lit[??A] | Rcd[Lam | Lit[??A] | 'b | 'c] | 'b //│ 'a <: App | Lam | Lit[anything] | Rcd['a] | Sel | Var eval : (Term, List[{key: Str, value: Value}]) -> Value diff --git a/shared/src/test/diff/nu/GADTMono.mls b/shared/src/test/diff/nu/GADTMono.mls index 0d8323d5fb..34a9a5a1d5 100644 --- a/shared/src/test/diff/nu/GADTMono.mls +++ b/shared/src/test/diff/nu/GADTMono.mls @@ -1,124 +1,39 @@ :NewDefs -trait Expr[A]: LitInt | LitBool | Add | Cond | Pair | Fst | Snd -class LitInt(n: Int) extends Expr[Int] -class LitBool(b: Bool) extends Expr[Bool] -class Add(x: Expr[Int], y: Expr[Int]) extends Expr[Int] -class Cond[T](p: Expr[Bool], t: Expr[T], e: Expr[T]) extends Expr[T] -class Pair[S, T](a: Expr[S], b: Expr[T]) extends Expr[[S, T]] -class Fst[S, T](p: Expr[[S, T]]) extends Expr[S] -class Snd[S, T](p: Expr[[S, T]]) extends Expr[T] -//│ trait Expr[A]: Add | Cond[?] | Fst[?, ?] | LitBool | LitInt | Pair[?, ?] | Snd[?, ?] -//│ class LitInt(n: Int) extends Expr -//│ class LitBool(b: Bool) extends Expr -//│ class Add(x: Expr[Int], y: Expr[Int]) extends Expr -//│ class Cond[T](p: Expr[Bool], t: Expr[T], e: Expr[T]) extends Expr -//│ class Pair[S, T](a: Expr[S], b: Expr[T]) extends Expr -//│ class Fst[S, T](p: Expr[[S, T]]) extends Expr -//│ class Snd[S, T](p: Expr[[S, T]]) extends Expr +abstract class Option[type T]: None | Some[T] +module None extends Option[nothing] +class Some[T](get: T) extends Option[T] +//│ abstract class Option[T]: None | Some[T] +//│ module None extends Option +//│ class Some[T](get: T) extends Option -let l1 = LitInt(1) -//│ let l1: LitInt -//│ l1 -//│ = LitInt {} +fun map(f, x) = if x is + None then None + Some(g) then Some(f(g)) +//│ fun map: forall 'a 'T. ('a -> 'T, None | Some['a]) -> (None | Some['T]) -// TODO -class Exp[type A] -//│ ╔══[PARSE ERROR] Unexpected 'type' keyword here -//│ ║ l.26: class Exp[type A] -//│ ╙── ^^^^ -//│ class Exp { -//│ constructor() -//│ } +fun map[A, B](f: A -> B, x: Option[A]) = if x is + None then None + Some(g) then Some(f(g)) +//│ fun map: forall 'A 'B. (f: 'A -> 'B, x: Option['A]) -> (None | Some['B]) -l1: Expr[Int] -//│ Expr[Int] -//│ res -//│ = LitInt {} +fun getOr(x, d) = if x is + None then d + Some(g) then g +//│ fun getOr: forall 'a. (None | Some['a], 'a) -> 'a -:e -l1: Expr[Bool] -//│ ╔══[ERROR] Type mismatch in type ascription: -//│ ║ l.40: l1: Expr[Bool] -//│ ║ ^^ -//│ ╟── type `Int` is not an instance of type `Bool` -//│ ║ l.4: class LitInt(n: Int) extends Expr[Int] -//│ ║ ^^^ -//│ ╟── Note: constraint arises from type reference: -//│ ║ l.40: l1: Expr[Bool] -//│ ╙── ^^^^ -//│ Expr[Bool] -//│ res -//│ = LitInt {} +fun getOr(x: Option['a], d) = if x is + None then d + Some(g) then g +//│ fun getOr: forall 'a 'b. (x: Option['a], 'b) -> ('b | 'a) -// FIXME -fun eval[A](e: Expr[A]): A = - if - e is LitInt(n) then n - e is LitBool(b) then b - e is Add(x, y) then eval(x) + eval(y) -//│ ╔══[ERROR] Type mismatch in `case` expression: -//│ ║ l.57: e is LitInt(n) then n -//│ ║ ^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.58: e is LitBool(b) then b -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.59: e is Add(x, y) then eval(x) + eval(y) -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── type `#Expr & (Add & {Expr#A = A} | Cond[?] & {Expr#A = A} | Fst[?, ?] & {Expr#A = A} | LitBool & {Expr#A = A} | LitInt & {Expr#A = A} | Pair[?, ?] & {Expr#A = A} | Snd[?, ?] & {Expr#A = A})` does not match type `Add | LitBool | LitInt` -//│ ║ l.55: fun eval[A](e: Expr[A]): A = -//│ ║ ^^^^^^^ -//│ ╟── but it flows into reference with expected type `Add | LitBool | LitInt` -//│ ║ l.57: e is LitInt(n) then n -//│ ╙── ^ -//│ ╔══[ERROR] Type mismatch in type ascription: -//│ ║ l.57: e is LitInt(n) then n -//│ ║ ^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.58: e is LitBool(b) then b -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.59: e is Add(x, y) then eval(x) + eval(y) -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── type `Int` does not match type `A` -//│ ║ l.4: class LitInt(n: Int) extends Expr[Int] -//│ ║ ^^^ -//│ ╟── but it flows into reference with expected type `A` -//│ ║ l.57: e is LitInt(n) then n -//│ ║ ^ -//│ ╟── Note: constraint arises from method type parameter: -//│ ║ l.55: fun eval[A](e: Expr[A]): A = -//│ ╙── ^ -//│ ╔══[ERROR] Type mismatch in definition: -//│ ║ l.55: fun eval[A](e: Expr[A]): A = -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.56: if -//│ ║ ^^^^^^^ -//│ ║ l.57: e is LitInt(n) then n -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.58: e is LitBool(b) then b -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.59: e is Add(x, y) then eval(x) + eval(y) -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── type `Int` does not match type `A` -//│ ║ l.6: class Add(x: Expr[Int], y: Expr[Int]) extends Expr[Int] -//│ ║ ^^^ -//│ ╟── Note: constraint arises from method type parameter: -//│ ║ l.55: fun eval[A](e: Expr[A]): A = -//│ ╙── ^ -//│ ╔══[ERROR] Type mismatch in definition: -//│ ║ l.55: fun eval[A](e: Expr[A]): A = -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.56: if -//│ ║ ^^^^^^^ -//│ ║ l.57: e is LitInt(n) then n -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.58: e is LitBool(b) then b -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.59: e is Add(x, y) then eval(x) + eval(y) -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── type `A` is not an instance of type `Int` -//│ ║ l.55: fun eval[A](e: Expr[A]): A = -//│ ║ ^ -//│ ╟── Note: constraint arises from type reference: -//│ ║ l.6: class Add(x: Expr[Int], y: Expr[Int]) extends Expr[Int] -//│ ╙── ^^^ -//│ fun eval: forall 'A. (e: Expr['A]) -> 'A +fun getOr[T](x: Option[T], d: T): T = if x is + None then d + Some(g) then g +//│ fun getOr: forall 'T. (x: Option['T], d: 'T) -> 'T +fun get(x) = if x is Some(r) then r else error +//│ fun get: forall 'a. (Object & ~#Some | Some['a]) -> 'a + +fun get(x: Option['a]): x.T = if x is Some(r) then r else error +//│ fun get: forall 'a. (x: Option['a]) -> 'a diff --git a/shared/src/test/diff/nu/InferredInheritanceTypeArgs.mls b/shared/src/test/diff/nu/InferredInheritanceTypeArgs.mls index b89c16cbd3..47a5c80d56 100644 --- a/shared/src/test/diff/nu/InferredInheritanceTypeArgs.mls +++ b/shared/src/test/diff/nu/InferredInheritanceTypeArgs.mls @@ -172,14 +172,8 @@ B.foo //│ res //│ = [Function: foo] - -// * TODO: when -:pe trait Foo[type A] { fun foo(x: A): A } -//│ ╔══[PARSE ERROR] Unexpected 'type' keyword here -//│ ║ l.178: trait Foo[type A] { fun foo(x: A): A } -//│ ╙── ^^^^ -//│ trait Foo { +//│ trait Foo[A] { //│ fun foo: (x: A) -> A //│ } @@ -228,22 +222,22 @@ class B extends Foo { fun foo(x) = x } :e class B extends Foo { fun foo(x) = x + 1 } //│ ╔══[ERROR] Type mismatch in definition of method foo: -//│ ║ l.229: class B extends Foo { fun foo(x) = x + 1 } +//│ ║ l.223: class B extends Foo { fun foo(x) = x + 1 } //│ ║ ^^^^^^^^^^^^^^ //│ ╟── type `A` is not an instance of type `Int` -//│ ║ l.217: trait Foo[A] { fun foo[A](x: A): A } +//│ ║ l.211: trait Foo[A] { fun foo[A](x: A): A } //│ ║ ^ //│ ╟── Note: constraint arises from reference: -//│ ║ l.229: class B extends Foo { fun foo(x) = x + 1 } +//│ ║ l.223: class B extends Foo { fun foo(x) = x + 1 } //│ ╙── ^ //│ ╔══[ERROR] Type mismatch in definition of method foo: -//│ ║ l.229: class B extends Foo { fun foo(x) = x + 1 } +//│ ║ l.223: class B extends Foo { fun foo(x) = x + 1 } //│ ║ ^^^^^^^^^^^^^^ //│ ╟── operator application of type `Int` does not match type `A` -//│ ║ l.229: class B extends Foo { fun foo(x) = x + 1 } +//│ ║ l.223: class B extends Foo { fun foo(x) = x + 1 } //│ ║ ^^^^^ //│ ╟── Note: constraint arises from method type parameter: -//│ ║ l.217: trait Foo[A] { fun foo[A](x: A): A } +//│ ║ l.211: trait Foo[A] { fun foo[A](x: A): A } //│ ╙── ^ //│ class B extends Foo { //│ constructor() diff --git a/shared/src/test/diff/nu/Lifted.mls b/shared/src/test/diff/nu/Lifted.mls new file mode 100644 index 0000000000..3b8f9efd62 --- /dev/null +++ b/shared/src/test/diff/nu/Lifted.mls @@ -0,0 +1,78 @@ +:NewDefs + +let y = 1 +//│ let y: 1 +//│ y +//│ = 1 + +1 : y +//│ 1 +//│ res +//│ = 1 + +let x: y = 1 +//│ let x: 1 +//│ x +//│ = 1 + +:e +let x: (1, 2) = (1, 2) +//│ ╔══[ERROR] cannot lift variable , to type +//│ ║ l.19: let x: (1, 2) = (1, 2) +//│ ╙── ^^^^^^ +//│ let x: error +//│ x +//│ = 2 + +:e +let x: (1, 2,) = (1, 2,) +//│ ╔══[ERROR] cannot lift variable , to type +//│ ║ l.28: let x: (1, 2,) = (1, 2,) +//│ ╙── ^^^^^^^ +//│ let x: error +//│ x +//│ = 2 + +class Foo[A, B] +//│ class Foo[A, B] { +//│ constructor() +//│ } + +let x: Foo[1, 2] = new Foo +//│ let x: Foo[1, 2] +//│ x +//│ = Foo {} + +let y: Foo = new Foo +//│ let y: Foo[?, ?] +//│ y +//│ = Foo {} + +:e +let z: y[1, 2] +//│ ╔══[ERROR] `let` bindings must have a right-hand side +//│ ║ l.52: let z: y[1, 2] +//│ ╙── ^^^^^^^^^^^^^^ +//│ ╔══[ERROR] cannot lift expression y to type +//│ ║ l.52: let z: y[1, 2] +//│ ║ ^^^^^^^ +//│ ╟── as defined in +//│ ║ l.46: let y: Foo = new Foo +//│ ╙── ^^^^^^^^^^^^^^^^ +//│ let z: error +//│ z +//│ = + +:e +2 : (1, 2) +//│ ╔══[ERROR] cannot lift variable , to type +//│ ║ l.67: 2 : (1, 2) +//│ ╙── ^^^^^^ +//│ error +//│ res +//│ = 2 + +1 : Int +//│ Int +//│ res +//│ = 1 diff --git a/shared/src/test/diff/nu/ListConsNil.mls b/shared/src/test/diff/nu/ListConsNil.mls index d1f1c147fe..98c5c115c9 100644 --- a/shared/src/test/diff/nu/ListConsNil.mls +++ b/shared/src/test/diff/nu/ListConsNil.mls @@ -114,7 +114,7 @@ fun test(x, l) = list_assoc(42, Cons(x, l)) fun test(x, l) = if l is Nil then list_assoc(42, Cons(x, l)) Cons(h, t) then list_assoc(42, Cons(h, t)) -//│ fun test: forall 'A 'A0. ({_1: anything, _2: 'A}, Cons[{_1: anything, _2: 'A0}] | Nil) -> (Cons['A] | Nil | Cons['A0]) +//│ fun test: forall 'A. ({_1: anything, _2: 'A}, Cons[{_1: anything, _2: 'A}] | Nil) -> (Cons['A] | Nil) diff --git a/shared/src/test/diff/nu/Metaprog.mls b/shared/src/test/diff/nu/Metaprog.mls index fda3779361..2ebfefbd3e 100644 --- a/shared/src/test/diff/nu/Metaprog.mls +++ b/shared/src/test/diff/nu/Metaprog.mls @@ -28,7 +28,7 @@ abstract class Test[C] { // * Represents what happens in "... ${input} ..." when a binding of C is in scope fun unquote: (input: Code['a, C | 'c]) -> Code[Int, 'c] fun getVar: Code[Int, C] - fun test0 = this.unquote of IntLit(1) + fun test0 = this.unquote of (IntLit(1) : Code['ia, 'ic]) // ? why ascription works here fun test1 = this.unquote of Add(this.getVar, IntLit(1)) } //│ abstract class Test[C] { diff --git a/shared/src/test/diff/nu/MethodSignatures.mls b/shared/src/test/diff/nu/MethodSignatures.mls index 583ddefb4a..25f496b3e0 100644 --- a/shared/src/test/diff/nu/MethodSignatures.mls +++ b/shared/src/test/diff/nu/MethodSignatures.mls @@ -164,7 +164,27 @@ module M { //│ ╔══[ERROR] undeclared `this` //│ ║ l.161: fun a: this.A //│ ╙── ^^^^ -//│ /!!!\ Uncaught error: scala.NotImplementedError: an implementation is missing +//│ ╔══[ERROR] Type mismatch in definition of method a: +//│ ║ l.162: fun a = 1 +//│ ║ ^^^^^ +//│ ╟── integer literal of type `1` does not match type `A` +//│ ║ l.162: fun a = 1 +//│ ║ ^ +//│ ╟── but it flows into definition of method a with expected type `A` +//│ ║ l.162: fun a = 1 +//│ ║ ^^^^^ +//│ ╟── Note: constraint arises from type selection: +//│ ║ l.161: fun a: this.A +//│ ║ ^^ +//│ ╟── from signature of member `a`: +//│ ║ l.161: fun a: this.A +//│ ╙── ^^^^^^^^^ +//│ module M { +//│ class A { +//│ constructor() +//│ } +//│ fun a: error +//│ } // FIXME similar module M { @@ -188,7 +208,7 @@ fun f(Int): Int :e fun f(x): Int //│ ╔══[ERROR] type identifier not found: x -//│ ║ l.189: fun f(x): Int +//│ ║ l.209: fun f(x): Int //│ ╙── ^ //│ fun f: error -> Int diff --git a/shared/src/test/diff/nu/NestedClasses.mls b/shared/src/test/diff/nu/NestedClasses.mls index d712fc8db9..65eac7c881 100644 --- a/shared/src/test/diff/nu/NestedClasses.mls +++ b/shared/src/test/diff/nu/NestedClasses.mls @@ -15,7 +15,7 @@ let c = C0() :e c.NC0 -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member NC0 not yet supported //│ ║ l.17: c.NC0 //│ ╙── ^^^^ //│ error @@ -37,7 +37,7 @@ module M0 { :e M0.NC0 -//│ ╔══[ERROR] Access to class member not yet supported +//│ ╔══[ERROR] Access to class member NC0 not yet supported //│ ║ l.39: M0.NC0 //│ ╙── ^^^^ //│ error @@ -54,7 +54,7 @@ module M1 { :e M1.NM1 -//│ ╔══[ERROR] Access to module member not yet supported +//│ ╔══[ERROR] Access to module member NM1 not yet supported //│ ║ l.56: M1.NM1 //│ ╙── ^^^^ //│ error diff --git a/shared/src/test/diff/nu/NewNew.mls b/shared/src/test/diff/nu/NewNew.mls index a2e039d7c3..c9826a0cf7 100644 --- a/shared/src/test/diff/nu/NewNew.mls +++ b/shared/src/test/diff/nu/NewNew.mls @@ -259,7 +259,7 @@ fun f(x) = {x} :e new f(1) -//│ ╔══[ERROR] type identifier not found: f +//│ ╔══[ERROR] Unexpected type `forall ?a. ?a -> {x: ?a}` after `new` keyword //│ ║ l.261: new f(1) //│ ╙── ^ //│ error diff --git a/shared/src/test/diff/nu/NuScratch.mls b/shared/src/test/diff/nu/NuScratch.mls index 539c23787c..dbb749d512 100644 --- a/shared/src/test/diff/nu/NuScratch.mls +++ b/shared/src/test/diff/nu/NuScratch.mls @@ -1,3 +1,292 @@ :NewDefs +// ?A' :> `S <: `S +// ?A :> ??S <: ??S and ?A' :> `S | ?A <: `S & ?A' +// the bounds of ??A are now eqt to ?A :> Top <: Bot +// which fails + + +class Box[type A](val get: A) +abstract class F[type A]: MkF +class MkF[T](t: T) extends F[Box[T]] +//│ class Box[A](get: A) +//│ abstract class F[A]: MkF[anything] +//│ class MkF[T](t: T) extends F + +// :d +// TODO +fun f[T](x: F[T]): T = if x is MkF(t) then Box(t) as x.A +//│ ╔══[ERROR] Type error in `case` expression +//│ ║ l.19: fun f[T](x: F[T]): T = if x is MkF(t) then Box(t) as x.A +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── type variable `T` leaks out of its scope +//│ ║ l.12: class MkF[T](t: T) extends F[Box[T]] +//│ ║ ^ +//│ ╙── into type `nothing` +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.19: fun f[T](x: F[T]): T = if x is MkF(t) then Box(t) as x.A +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── type `Box[?T]` does not match type `T` +//│ ║ l.12: class MkF[T](t: T) extends F[Box[T]] +//│ ║ ^^^^^^ +//│ ╟── Note: constraint arises from method type parameter: +//│ ║ l.19: fun f[T](x: F[T]): T = if x is MkF(t) then Box(t) as x.A +//│ ╙── ^ +//│ fun f: forall 'T. (x: F['T]) -> 'T + + +// TODO +fun f: Box[?] +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.40: fun f: Box[?] +//│ ╙── ^ +//│ fun f: Box[error] + +// :ds +f +//│ Box[error] +//│ res +//│ = +//│ f is not implemented + + +fun foo(b: Box['X]) = b.get + 1 +//│ fun foo: forall 'X. (b: Box['X]) -> Int +//│ where +//│ 'X <: Int + +fun foo(b: Box['X] & Box[Int]) = [b, b.get + 1] +//│ fun foo: (b: Box[Int]) -> [Box[Int], Int] + + +type List[out A] = Cons[A] +module Nil +class Cons[A](head: A, tail: List[A]) +//│ type List[A] = Cons[A] +//│ module Nil +//│ class Cons[A](head: A, tail: List[A]) + +fun listConcat(xs) = + if xs is + Cons(x, xs2) then Cons(x, listConcat(xs2)) +//│ fun listConcat: forall 'A. Cons['A] -> Cons['A] + + + + + +module T { + fun unapply(x) = [x] +} +//│ module T { +//│ fun unapply: forall 'a. 'a -> ['a] +//│ } + +:e +fun foo(a) = if a is T(x) then x else 0 +//│ ╔══[ERROR] module T expects 0 parameter but found 1 parameter +//│ ║ l.87: fun foo(a) = if a is T(x) then x else 0 +//│ ╙── ^^^^ +//│ fun foo: anything -> error +//│ Code generation encountered an error: +//│ if expression was not desugared + + + +class C(x: Int, y: Str) +//│ class C(x: Int, y: Str) + + +:d +fun foo(c) = if c is C(a, b) then [a, b] +//│ 0. Typing TypingUnit(List(NuFunDef(None,Var(foo),None,List(),Left(Lam(Tup(List((None,Fld(_,Var(c))))),If(IfThen(App(Var(is),Tup(List((None,Fld(_,Var(c))), (None,Fld(_,App(Var(C),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b))))))))))),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b)))))),None)))))) +//│ | 0. Created lazy type info for NuFunDef(None,Var(foo),None,List(),Left(Lam(Tup(List((None,Fld(_,Var(c))))),If(IfThen(App(Var(is),Tup(List((None,Fld(_,Var(c))), (None,Fld(_,App(Var(C),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b))))))))))),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b)))))),None)))) +//│ | Completing fun foo = (c,) => if (is(c, C(a, b,),)) then [a, b,] +//│ | | Type params +//│ | | Params +//│ | | Type foo polymorphically? true && (0 === 0 || false || false +//│ | | 1. Typing term Lam(Tup(List((None,Fld(_,Var(c))))),If(IfThen(App(Var(is),Tup(List((None,Fld(_,Var(c))), (None,Fld(_,App(Var(C),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b))))))))))),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b)))))),None)) +//│ | | | 1. Typing pattern Tup(List((None,Fld(_,Var(c))))) +//│ | | | | 1. Typing pattern Var(c) +//│ | | | | 1. : c165' +//│ | | | 1. : (c165',) +//│ | | | 1. Typing term If(IfThen(App(Var(is),Tup(List((None,Fld(_,Var(c))), (None,Fld(_,App(Var(C),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b))))))))))),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b)))))),None) +//│ | | | | [Desugarer.destructPattern] scrutinee = Var(c); pattern = App(Var(C),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b)))))) +//│ | | | | [Desugarer.destructPattern] Result: «c is Var(C)» +//│ | | | | Desugared term: case c of { C => let $unapp = (C).unapply(c,) in let a = ($unapp).0 in let b = ($unapp).1 in [a, b,] } +//│ | | | | 1. Typing term CaseOf(Var(c),Case(Var(C),Let(false,Var($unapp),App(Sel(Var(C),Var(unapply)),Tup(List((None,Fld(_,Var(c)))))),Let(false,Var(a),Sel(Var($unapp),Var(0)),Let(false,Var(b),Sel(Var($unapp),Var(1)),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b)))))))),NoCases)) +//│ | | | | | 1. Typing term Var(c) +//│ | | | | | 1. : c165' +//│ | | | | | CONSTRAIN c165' & ⊤ +//│ | | | | | 1. Typing term Let(false,Var($unapp),App(Sel(Var(C),Var(unapply)),Tup(List((None,Fld(_,Var(c)))))),Let(false,Var(a),Sel(Var($unapp),Var(0)),Let(false,Var(b),Sel(Var($unapp),Var(1)),Tup(List((None,Fld(_,Var(a))), (None,Fld(_,Var(b)))))))) +//│ | | | | | | 1. Typing term App(Sel(Var(C),Var(unapply)),Tup(List((None,Fld(_,Var(c)))))) +//│ | | | | | | | 1. Typing term Sel(Var(C),Var(unapply)) +//│ | | | | | | | | 1. Typing term Lam(Tup(List((None,Fld(_,Var(x))))),Let(false,Var(_),Asc(Var(x),TypeName(C)),Tup(List((None,Fld(_,Sel(Var(x),Var(#x)))), (None,Fld(_,Sel(Var(x),Var(#y)))))))) +//│ | | | | | | | | | TYPING POLY LAM +//│ | | | | | | | | | 2. Typing pattern Tup(List((None,Fld(_,Var(x))))) +//│ | | | | | | | | | | 2. Typing pattern Var(x) +//│ | | | | | | | | | | 2. : x166'' +//│ | | | | | | | | | 2. : (x166'',) +//│ | | | | | | | | | 2. Typing term Let(false,Var(_),Asc(Var(x),TypeName(C)),Tup(List((None,Fld(_,Sel(Var(x),Var(#x)))), (None,Fld(_,Sel(Var(x),Var(#y))))))) +//│ | | | | | | | | | | 2. Typing term Asc(Var(x),TypeName(C)) +//│ | | | | | | | | | | | 2. Typing term Var(x) +//│ | | | | | | | | | | | 2. : x166'' +//│ | | | | | | | | | | | Typing type TypeName(C) +//│ | | | | | | | | | | | | vars=Map() newDefsInfo=Map() +//│ | | | | | | | | | | | | 2. type TypeName(C) +//│ | | | | | | | | | | | | => C +//│ | | | | | | | | | | | => C ——— +//│ | | | | | | | | | | | CONSTRAIN x166'' (#x167'', #y168'',)) —— where +//│ x166'' <: {#y: #y168''} & {#x: #x167''} & C +//│ | | | | | | | | 1. : ‹∀ 1. (x166'' -> (#x167'', #y168'',))› +//│ | | | | | | | 1. : ‹∀ 1. (x166'' -> (#x167'', #y168'',))› +//│ | | | | | | | 1. Typing term Var(c) +//│ | | | | | | | 1. : #C +//│ | | | | | | | CONSTRAIN ‹∀ 1. (x166'' -> (#x167'', #y168'',))› -> α169') +//│ | | | | | | | where +//│ x166'' <: {#y: #y168''} & {#x: #x167''} & C +//│ | | | | | | | 1. C ‹∀ 1. (x166'' -> (#x167'', #y168'',))› -> α169') (0) +//│ | | | | | | | | could be distribbed: Set(#x167'', #y168'') +//│ | | | | | | | | cannot be distribbed: Set(x166'', #x167'', #y168'') +//│ | | | | | | | | INST [1] ‹∀ 1. (x166'' -> (#x167'', #y168'',))› +//│ | | | | | | | | where +//│ x166'' <: {#y: #y168''} & {#x: #x167''} & C +//│ | | | | | | | | TO [1] ~> (x166_170' -> (#x167_172', #y168_171',)) +//│ | | | | | | | | where +//│ x166_170' <: {#y: #y168_171'} & {#x: #x167_172'} & C +//│ | | | | | | | | 1. C (x166_170' -> (#x167_172', #y168_171',)) -> α169') (2) +//│ | | | | | | | | | 1. C (#C,) (8) +//│ | | | | | | | | | | | | | Already a subtype by <:< +//│ | | | | | | | | | 1. C (#x167_172', #y168_171',) (#x167_172', #y168_171',) +//│ #y168_171' :> Str +//│ #x167_172' :> Int +//│ | | | | | | | | 1. C α169' (#x167_172', #y168_171',) <: {0: α173'} +//│ #y168_171' :> Str +//│ #x167_172' :> Int <: α173' +//│ α173' :> Int +//│ | | | | | | | | | 1. C α169' +//│ | | | | | where +//│ c165' <: Object +//│ | | | | | 1. C c165' (0) +//│ | | | | | | NEW c165' UB (0) +//│ | | | | 1. : (α173', α174',) +//│ | | | 1. : (α173', α174',) +//│ | | 1. : (c165' -> (α173', α174',)) +//│ | | CONSTRAIN (c165' -> (α173', α174',)) & Object +//│ α173' :> Int +//│ α174' :> Str +//│ | | 1. C (c165' -> (α173', α174',)) (α173', α174',))) where +//│ c165' <: #C & Object +//│ α173' :> Int +//│ α174' :> Str +//│ | Typing unit statements +//│ | : None +//│ ======== TYPED ======== +//│ fun foo: ‹∀ 0. (c165' -> (α173', α174',))› where +//│ | c165' <: #C & Object +//│ | α173' :> Int +//│ | α174' :> Str +//│ fun foo: C -> [Int, Str] + + + + + + + + diff --git a/shared/src/test/diff/nu/NuScratch2.mls b/shared/src/test/diff/nu/NuScratch2.mls new file mode 100644 index 0000000000..c8c4aa14b5 --- /dev/null +++ b/shared/src/test/diff/nu/NuScratch2.mls @@ -0,0 +1,243 @@ +:NewDefs + +abstract class Foo0[type T] { + fun x: T +} +abstract class Bar0 extends Foo0[Int] +//│ abstract class Foo0[T] { +//│ fun x: T +//│ } +//│ abstract class Bar0 extends Foo0 { +//│ fun x: 'T +//│ } +//│ where +//│ 'T := Int + +abstract class Foo[type T]: (Bar | Baz) { + fun x: T + fun f: T -> Int +} +abstract class Bar extends Foo[Int] +abstract class Baz extends Foo[Str] +//│ abstract class Foo[T]: Bar | Baz { +//│ fun f: T -> Int +//│ fun x: T +//│ } +//│ abstract class Bar: Bar | Baz extends Foo { +//│ fun f: 'T -> Int +//│ fun x: 'T +//│ } +//│ abstract class Baz: Bar | Baz extends Foo { +//│ fun f: 'T0 -> Int +//│ fun x: 'T0 +//│ } +//│ where +//│ 'T0 := Str +//│ 'T := Int + +:e // Expected +fun test(f: Foo) = f.f(f.x) +//│ ╔══[ERROR] Type error in application +//│ ║ l.39: fun test(f: Foo) = f.f(f.x) +//│ ║ ^^^^^^^^ +//│ ╟── type variable `T` leaks out of its scope +//│ ║ l.17: fun x: T +//│ ║ ^^^^ +//│ ╟── back into type variable `T` +//│ ║ l.16: abstract class Foo[type T]: (Bar | Baz) { +//│ ╙── ^ +//│ fun test: (f: Foo[?]) -> (Int | error) + +:e +fun test(f: Foo) = if f is + Foo then f.f(f.x) +//│ ╔══[ERROR] Type error in `case` expression +//│ ║ l.52: fun test(f: Foo) = if f is +//│ ║ ^^^^ +//│ ║ l.53: Foo then f.f(f.x) +//│ ║ ^^^^^^^^^^^^^^^^^^^ +//│ ╟── type variable `T` leaks out of its scope +//│ ║ l.16: abstract class Foo[type T]: (Bar | Baz) { +//│ ╙── ^ +//│ fun test: (f: Foo[?]) -> (Int | error) + +:e +fun test(f: Foo) = if f is + Foo then f.x : f.T +//│ ╔══[ERROR] Type error in `case` expression +//│ ║ l.65: fun test(f: Foo) = if f is +//│ ║ ^^^^ +//│ ║ l.66: Foo then f.x : f.T +//│ ║ ^^^^^^^^^^^^^^ +//│ ╟── type variable `T` leaks out of its scope +//│ ║ l.16: abstract class Foo[type T]: (Bar | Baz) { +//│ ╙── ^ +//│ fun test: (f: Foo[?]) -> anything + +// FIXME +fun test(f: Foo['a]) = if f is + Foo then f.x : f.T +//│ /!!!\ Uncaught error: java.lang.StackOverflowError + +fun test(f: Foo0['a]) = if f is + Foo0 then f.x : f.T // here, locally we have f.T =:= `T & 'a where `T is the local skolem for x.T +//│ fun test: forall 'a. (f: Foo0['a]) -> nothing +//│ where +//│ 'a <: nothing + +// * NOTE: refined f.T =:= `T & 'a +fun test(f: Foo0['a]) = if f is + Foo0 then f.x : f.T + _ then error +//│ fun test: forall 'a. (f: Foo0['a]) -> nothing +//│ where +//│ 'a <: nothing + +// * TODO: why don't we get 'a in the result whereas we do in the Foo0 case above? +fun test(f: Foo0['a]) = if f is + Bar0 then 123 : f.T + _ then error +//│ fun test: forall 'a. (f: Foo0['a]) -> Int + +// ^ What's haoppening: +// Bar & {} <: { T: 'l..'u } +// ^ What SHOULD be haoppening: +// Bar & Foo0['a] <: { T: 'l..'u } +// Notice that field T in `Bar & Foo0['a]` should yield `'a | Int .. 'a & Int` +// Alternative (not great; not clear how to do it generally/in a principled way): +// Bar & {T: 'a .. 'a } <: { T: 'l..'u } + + +fun test(x: 'a, g: Foo0[x], f: Foo0[x]) = if f is + Bar0 then 123 : g.T + _ then error +//│ fun test: forall 'a. (x: 'a, g: Foo0['a], f: Foo0['a]) -> 'a +//│ where +//│ 'a :> 123 + +:e +fun test(f: Foo) = if f is + Foo then f.f(f.x : f.T) +//│ ╔══[ERROR] Type error in `case` expression +//│ ║ l.119: fun test(f: Foo) = if f is +//│ ║ ^^^^ +//│ ║ l.120: Foo then f.f(f.x : f.T) +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── type variable `T` leaks out of its scope +//│ ║ l.16: abstract class Foo[type T]: (Bar | Baz) { +//│ ╙── ^ +//│ fun test: (f: Foo[?]) -> (Int | error) + +fun test(f: Foo) = if f is + Bar then f.x + else error +//│ fun test: (f: Foo[?]) -> Int + +fun test(f: Foo) = if f is + Bar then f.x : f.T + else error +//│ fun test: (f: Foo[?]) -> Int + +// FIXME +fun test(f: Foo) = if f is + Bar then 123 : f.T + Baz then error +//│ ╔══[ERROR] Type mismatch in `case` expression: +//│ ║ l.142: fun test(f: Foo) = if f is +//│ ║ ^^^^ +//│ ║ l.143: Bar then 123 : f.T +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.144: Baz then error +//│ ║ ^^^^^^^^^^^^^^^^^^ +//│ ╟── type `Foo[?]` does not match type `Bar | Baz` +//│ ║ l.142: fun test(f: Foo) = if f is +//│ ║ ^^^ +//│ ╟── but it flows into reference with expected type `Bar | Baz` +//│ ║ l.142: fun test(f: Foo) = if f is +//│ ╙── ^ +//│ fun test: (f: Foo[?]) -> Int + +fun test(f: Foo) = if f is + Bar then 123 : f.T + Baz then "hello" : f.T + _ then error +//│ fun test: (f: Foo[?]) -> (Int | Str) + +// FIXME +fun test(f: Foo['a]) = if f is + Bar then 123 : f.T + Baz then "hello" : f.T + _ then error +//│ /!!!\ Uncaught error: java.lang.StackOverflowError + +fun test(f: Foo, x) = x : f.T +//│ fun test: (f: Foo[?], ??T) -> ??T0 + +// FIXME +fun test[A](f: Foo[A]): A = if f is + Bar then 123 : f.T + Baz then "hello" : f.T +//│ /!!!\ Uncaught error: java.lang.StackOverflowError + +// FIXME +fun test(f: Foo['a]): f.T = if f is + Bar then 123 : f.T + Baz then "hello" : f.T +//│ /!!!\ Uncaught error: java.lang.StackOverflowError + +// FIXME +:e // expected +test(error, 1) +//│ /!!!\ Uncaught error: java.lang.StackOverflowError + +// FIXME +fun test[T](f: Foo[T]): T = if f is + Bar then 123 : f.T + Baz then error +//│ /!!!\ Uncaught error: java.lang.StackOverflowError + +// FIXME +fun test(f: Foo['a]) = if f is + Foo then f.x +//│ /!!!\ Uncaught error: java.lang.StackOverflowError + +// * infinite loop in expand(Bar) (making Bar non abstract fixes the problem) +// * abstract Bar expands to `#Bar & (Bar | Baz)` +// * non abstract Bar expands to `#Bar` + +abstract class Foo[type T]: (Bar | Baz) { + fun x: T + fun f: T -> Int +} +class Bar(val x: Int) extends Foo[Int] { fun f(y) = this.x + y } +class Baz(val x: Str) extends Foo[Str] { fun f(y) = 0 } +//│ abstract class Foo[T]: Bar | Baz { +//│ fun f: T -> Int +//│ fun x: T +//│ } +//│ class Bar(x: Int) extends Foo { +//│ fun f: Int -> Int +//│ } +//│ class Baz(x: Str) extends Foo { +//│ fun f: anything -> 0 +//│ } + +fun test(f: Foo['a]) = if f is + Foo then f.x +//│ fun test: forall 'a. (f: Foo['a]) -> ('a & (Int | Str)) + +abstract class Foo[T]: Bar { fun x: T } +abstract class Bar extends Foo[Int] +//│ abstract class Foo[T]: Bar { +//│ fun x: T +//│ } +//│ abstract class Bar: Bar extends Foo { +//│ fun x: 'T +//│ } +//│ where +//│ 'T := Int + +// FIXME +fun test(f: Foo['a]) = if f is + Foo then f.x +//│ /!!!\ Uncaught error: java.lang.StackOverflowError diff --git a/shared/src/test/diff/nu/NuScratch3.mls b/shared/src/test/diff/nu/NuScratch3.mls new file mode 100644 index 0000000000..f84992ce4a --- /dev/null +++ b/shared/src/test/diff/nu/NuScratch3.mls @@ -0,0 +1,19 @@ +:NewDefs + + + +class Arr[A](xs: A -> A) +//│ class Arr[A](xs: A -> A) + +module N extends Arr[nothing](id) +//│ module N extends Arr + +fun test(k) = id(x => k(if true then N else Arr(x))) +//│ fun test: forall 'A 'A0 'a. ((Arr[in 'A out 'A | 'A0] | N) -> 'a) -> (forall 'A1. (('A | 'A1) -> ('A0 & 'A1)) -> 'a) + +test(x => x)(id) +//│ Arr['A] | N +//│ res +//│ = N { class: [class N extends Arr] } + + diff --git a/shared/src/test/diff/nu/NuScratch4.mls b/shared/src/test/diff/nu/NuScratch4.mls new file mode 100644 index 0000000000..670929491e --- /dev/null +++ b/shared/src/test/diff/nu/NuScratch4.mls @@ -0,0 +1,185 @@ +:NewDefs +:NoJS + + +class Ref[T](x: T -> T) +//│ class Ref[T](x: T -> T) + + +// fun refined[A](r: Ref[A]) +// fun refined[A, B](r: A): A & Ref[B] +fun refined: forall 'A, 'B: (r: 'A) -> ('A & Ref['B]) +//│ fun refined: forall 'A 'B. (r: 'A) -> (Ref['B] & 'A) + +fun test(x: 'x) = + let foo() = refined(x) + foo +//│ fun test: forall 'x. (x: 'x) -> (forall 'B. () -> (Ref['B] & 'x)) + +// fun refined: forall 'A, 'B, 'C: (r: 'A, s: 'B) -> ('A & 'B & Ref['C]) +fun refined: forall 'A, 'B, 'C: (r: 'A, s: 'B) -> ('A & 'B) +//│ fun refined: forall 'A 'B. (r: 'A, s: 'B) -> ('A & 'B) + +// fun test(x: 'x) = +// let foo(y: Ref['r] & 'y) = y +// foo(x) + +:d +fun test(x: 'x) = + let foo(y) = refined(x, y) : Ref['r] + foo +//│ 0. Typing TypingUnit(List(NuFunDef(None,Var(test),None,List(),Left(Lam(Tup(List((Some(Var(x)),Fld(_,Var('x))))),Blk(List(NuFunDef(Some(false),Var(foo),None,List(),Left(Lam(Tup(List((None,Fld(_,Var(y))))),Asc(App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))),AppliedType(TypeName(Ref),List('r)))))), Var(foo)))))))) +//│ | 0. Created lazy type info for NuFunDef(None,Var(test),None,List(),Left(Lam(Tup(List((Some(Var(x)),Fld(_,Var('x))))),Blk(List(NuFunDef(Some(false),Var(foo),None,List(),Left(Lam(Tup(List((None,Fld(_,Var(y))))),Asc(App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))),AppliedType(TypeName(Ref),List('r)))))), Var(foo)))))) +//│ | Completing fun test = (x: 'x,) => {let foo = (y,) => refined(x, y,) : Ref['r]; foo} +//│ | | Type params +//│ | | Params +//│ | | Type test polymorphically? true && (0 === 0 || false || false +//│ | | 1. Typing term Lam(Tup(List((Some(Var(x)),Fld(_,Var('x))))),Blk(List(NuFunDef(Some(false),Var(foo),None,List(),Left(Lam(Tup(List((None,Fld(_,Var(y))))),Asc(App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))),AppliedType(TypeName(Ref),List('r)))))), Var(foo)))) +//│ | | | 1. Typing pattern Tup(List((Some(Var(x)),Fld(_,Var('x))))) +//│ | | | | 1. Typing pattern Asc(Var(x),'x) +//│ | | | | | Typing type 'x +//│ | | | | | | vars=Map() newDefsInfo=Map() +//│ | | | | | | 1. type 'x +//│ | | | | | | => 'x93' +//│ | | | | | => 'x93' ——— 'x93' +//│ | | | | 1. : 'x93' +//│ | | | 1. : (x: 'x93',) +//│ | | | 1. Typing term Blk(List(NuFunDef(Some(false),Var(foo),None,List(),Left(Lam(Tup(List((None,Fld(_,Var(y))))),Asc(App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))),AppliedType(TypeName(Ref),List('r)))))), Var(foo))) +//│ | | | | 1. Typing TypingUnit(List(NuFunDef(Some(false),Var(foo),None,List(),Left(Lam(Tup(List((None,Fld(_,Var(y))))),Asc(App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))),AppliedType(TypeName(Ref),List('r)))))), Var(foo))) +//│ | | | | | 1. Created lazy type info for NuFunDef(Some(false),Var(foo),None,List(),Left(Lam(Tup(List((None,Fld(_,Var(y))))),Asc(App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))),AppliedType(TypeName(Ref),List('r)))))) +//│ | | | | | Completing let foo = (y,) => refined(x, y,) : Ref['r] +//│ | | | | | | Type params +//│ | | | | | | Params +//│ | | | | | | Type foo polymorphically? true && (1 === 0 || false || true +//│ | | | | | | 2. Typing term Lam(Tup(List((None,Fld(_,Var(y))))),Asc(App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))),AppliedType(TypeName(Ref),List('r)))) +//│ | | | | | | | 2. Typing pattern Tup(List((None,Fld(_,Var(y))))) +//│ | | | | | | | | 2. Typing pattern Var(y) +//│ | | | | | | | | 2. : y94'' +//│ | | | | | | | 2. : (y94'',) +//│ | | | | | | | 2. Typing term Asc(App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))),AppliedType(TypeName(Ref),List('r))) +//│ | | | | | | | | 2. Typing term App(Var(refined),Tup(List((None,Fld(_,Var(x))), (None,Fld(_,Var(y)))))) +//│ | | | | | | | | | 2. Typing term Var(refined) +//│ | | | | | | | | | 2. : ‹∀ 0. ‹∀ 1. ((r: 'A81'', s: 'B82'',) -> ('A81'' & 'B82''))›› +//│ | | | | | | | | | 2. Typing term Var(x) +//│ | | | | | | | | | 2. : 'x93' +//│ | | | | | | | | | 2. Typing term Var(y) +//│ | | | | | | | | | 2. : y94'' +//│ | | | | | | | | | CONSTRAIN ‹∀ 0. ‹∀ 1. ((r: 'A81'', s: 'B82'',) -> ('A81'' & 'B82''))›› α95'') +//│ | | | | | | | | | where +//│ | | | | | | | | | 2. C ‹∀ 0. ‹∀ 1. ((r: 'A81'', s: 'B82'',) -> ('A81'' & 'B82''))›› α95'') (0) +//│ | | | | | | | | | | 2. C ‹∀ 1. ((r: 'A81'', s: 'B82'',) -> ('A81'' & 'B82''))› α95'') (2) +//│ | | | | | | | | | | | could be distribbed: Set('A81'', 'B82'') +//│ | | | | | | | | | | | cannot be distribbed: Set('A81'', 'B82'') +//│ | | | | | | | | | | | INST [1] ‹∀ 1. ((r: 'A81'', s: 'B82'',) -> ('A81'' & 'B82''))› +//│ | | | | | | | | | | | where +//│ | | | | | | | | | | | TO [2] ~> ((r: 'A81_96'', s: 'B82_97'',) -> ('A81_96'' & 'B82_97'')) +//│ | | | | | | | | | | | where +//│ | | | | | | | | | | | 2. C ((r: 'A81_96'', s: 'B82_97'',) -> ('A81_96'' & 'B82_97'')) α95'') (4) +//│ | | | | | | | | | | | | 2. C ('x93', y94'',) 'r98'' +//│ | | | | | | | | | => Ref['r98''] +//│ | | | | | | | | => Ref['r98''] ——— 'r98'' +//│ | | | | | | | | CONSTRAIN α95'' ('A81_96'' & 'B82_97'') +//│ 'A81_96'' :> 'x93' +//│ | | | | | | | | 2. C α95'' & {Ref#T: mut 'r98''..'r98''}) (4) +//│ | | | | | | | | | | | 2. C ('A81_96'' & 'B82_97'') (6) +//│ | | | | | | | | | | | | 2. ARGH DNF(2, 'A81_96''∧'B82_97'') {}) +//│ | | | | | | | | | | | | | DNF DISCHARGE CONSTRAINTS +//│ | | | | | | | | | | | | | 2. C 'A81_96'' | ~('B82_97'')) (8) +//│ | | | | | | | | | | | | | | NEW 'A81_96'' UB (2) +//│ | | | | | | | | | | | | | | 2. C 'x93' | ~('B82_97'')) (10) +//│ | | | | | | | | | | | | | | | wrong level: 2 +//│ | | | | | | | | | | | | | | | RECONSTRAINING TVs +//│ | | | | | | | | | | | | | | | | Reconstraining 'B82_99' +//│ | | | | | | | | | | | | | | | EXTR RHS ~> (#Ref | ~('B82_99')) to 1 +//│ | | | | | | | | | | | | | | | where +//│ | | | | | | | | | | | | | | | 2. C 'x93' | ~('B82_99')) (12) +//│ | | | | | | | | | | | | | | | | NEW 'x93' UB (1) +//│ | | | | | | | | | | | 2. C ('A81_96'' & 'B82_97'') ({Ref#T: mut 'r98_100'..'r98_101'} | ~('B82_102')) to 1 +//│ | | | | | | | | | | | | | | | where +//│ 'r98_101' <: 'r98_100' +//│ | | | | | | | | | | | | | | | 2. C 'x93' Ref['r98'']) +//│ | | | | | | CONSTRAIN (y94'' -> Ref['r98'']) 'r98_101' <: 'r98_100' +//│ 'r98_101' <: 'r98_100' +//│ | | | | | | 2. C (y94'' -> Ref['r98'']) Ref['r98''])) where +//│ y94'' <: 'B82_97'' +//│ 'B82_97'' <: 'B82_102' & 'B82_99' +//│ 'r98'' :> 'r98_101' <: 'r98_100' +//│ 'r98_101' <: 'r98_100' +//│ | | | | | Typing unit statements +//│ | | | | | | 1. Typing term Var(foo) +//│ | | | | | | 1. : ‹∀ 1. (y94'' -> Ref['r98''])› +//│ | | | | | : Some(‹∀ 1. (y94'' -> Ref['r98''])›) +//│ | | | 1. : ‹∀ 1. (y94'' -> Ref['r98''])› +//│ | | 1. : ((x: 'x93',) -> ‹∀ 1. (y94'' -> Ref['r98''])›) +//│ | | CONSTRAIN ((x: 'x93',) -> ‹∀ 1. (y94'' -> Ref['r98''])›) | ~('B82_99')) +//│ y94'' <: 'B82_97'' +//│ 'B82_97'' <: 'B82_102' & 'B82_99' +//│ 'r98'' :> 'r98_101' <: 'r98_100' +//│ 'r98_101' <: 'r98_100' +//│ | | 1. C ((x: 'x93',) -> ‹∀ 1. (y94'' -> Ref['r98''])›) ‹∀ 1. (y94'' -> Ref['r98''])›)) where +//│ 'x93' <: ({Ref#T: mut 'r98_100'..'r98_101'} | ~('B82_102')) & (#Ref | ~('B82_99')) +//│ y94'' <: 'B82_97'' +//│ 'B82_97'' <: 'B82_102' & 'B82_99' +//│ 'r98'' :> 'r98_101' <: 'r98_100' +//│ 'r98_101' <: 'r98_100' +//│ | Typing unit statements +//│ | : None +//│ ======== TYPED ======== +//│ fun test: ‹∀ 0. ((x: 'x93',) -> ‹∀ 1. (y94'' -> Ref['r98''])›)› where +//│ | 'x93' <: ({Ref#T: mut 'r98_100'..'r98_101'} | ~('B82_102')) & (#Ref | ~('B82_99')) +//│ | y94'' <: 'B82_97'' +//│ | 'B82_97'' <: 'B82_102' & 'B82_99' +//│ | 'r98'' :> 'r98_101' <: 'r98_100' +//│ | 'r98_101' <: 'r98_100' +//│ fun test: forall 'B 'r. (x: Ref[?] & ~'B | Ref[in 'r out nothing] | ~'B) -> (forall 'r0. 'B -> Ref['r0]) +//│ where +//│ 'r0 <: 'r + + + + + diff --git a/shared/src/test/diff/nu/Parens.mls b/shared/src/test/diff/nu/Parens.mls index 12a9306ee0..b89ca91c6f 100644 --- a/shared/src/test/diff/nu/Parens.mls +++ b/shared/src/test/diff/nu/Parens.mls @@ -68,7 +68,7 @@ val x: (1,) :e val x: (1, 2) -//│ ╔══[ERROR] type identifier not found: , +//│ ╔══[ERROR] cannot lift variable , to type //│ ║ l.70: val x: (1, 2) //│ ╙── ^^^^^^ //│ val x: error @@ -77,7 +77,7 @@ val x: (1, 2) :e val x: (1, 2,) -//│ ╔══[ERROR] type identifier not found: , +//│ ╔══[ERROR] cannot lift variable , to type //│ ║ l.79: val x: (1, 2,) //│ ╙── ^^^^^^^ //│ val x: error diff --git a/shared/src/test/diff/nu/RawTypes.mls b/shared/src/test/diff/nu/RawTypes.mls new file mode 100644 index 0000000000..6ad8cdbfee --- /dev/null +++ b/shared/src/test/diff/nu/RawTypes.mls @@ -0,0 +1,150 @@ +:NewDefs + +// * currently +// Foo => Foo[?] ? is rigid can be uncovered in pattern matching +// * future +// Foo => Foo['a] can place bounds on 'a + +class Foo[type A](val a: A) +//│ class Foo[A](a: A) + +:e +fun foo(f: Foo): Int = f.a : f.A +//│ ╔══[ERROR] Type error in type ascription +//│ ║ l.12: fun foo(f: Foo): Int = f.a : f.A +//│ ║ ^^^ +//│ ╟── type variable `A` leaks out of its scope +//│ ║ l.12: fun foo(f: Foo): Int = f.a : f.A +//│ ║ ^^^ +//│ ╟── back into type variable `A` +//│ ║ l.12: fun foo(f: Foo): Int = f.a : f.A +//│ ╙── ^^ +//│ ╔══[ERROR] Type error in type ascription +//│ ║ l.12: fun foo(f: Foo): Int = f.a : f.A +//│ ║ ^^^ +//│ ╟── type variable `A` leaks out of its scope +//│ ║ l.12: fun foo(f: Foo): Int = f.a : f.A +//│ ║ ^^ +//│ ╟── into type `Int` +//│ ║ l.12: fun foo(f: Foo): Int = f.a : f.A +//│ ╙── ^^^ +//│ fun foo: (f: Foo[anything]) -> Int + +// :s +// :ds +// TODO +fun foo(f: Foo[?]) = f.a +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.36: fun foo(f: Foo[?]) = f.a +//│ ╙── ^ +//│ fun foo: (f: Foo[error]) -> error + +// TODO +fun foo(f: Foo[?]) = f.a : f.A +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.43: fun foo(f: Foo[?]) = f.a : f.A +//│ ╙── ^ +//│ fun foo: (f: Foo[error]) -> error + +foo(Foo(1)) +//│ error +//│ res +//│ = 1 + +fun foo(f: Foo) = f.a +//│ fun foo: (f: Foo[anything]) -> ??A + +fun foo(f: Foo[Int]) = f.a +//│ fun foo: (f: Foo[Int]) -> Int + +// TODO +fun foo(f: Foo[?]) = if f is Foo(a) then a : f.A +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.61: fun foo(f: Foo[?]) = if f is Foo(a) then a : f.A +//│ ╙── ^ +//│ fun foo: (f: Foo[error]) -> error + +:e +fun foo(f: Foo): Int = if f is Foo(a) then a : f.A +//│ ╔══[ERROR] Type error in `case` expression +//│ ║ l.68: fun foo(f: Foo): Int = if f is Foo(a) then a : f.A +//│ ║ ^^^^^^^^^^^^^^^^^^ +//│ ╟── type variable `A` leaks out of its scope +//│ ║ l.8: class Foo[type A](val a: A) +//│ ║ ^ +//│ ╟── into type `nothing` +//│ ║ l.68: fun foo(f: Foo): Int = if f is Foo(a) then a : f.A +//│ ║ ^^ +//│ ╟── Note: constraint arises from field selection: +//│ ║ l.8: class Foo[type A](val a: A) +//│ ╙── ^ +//│ ╔══[ERROR] Type error in type ascription +//│ ║ l.68: fun foo(f: Foo): Int = if f is Foo(a) then a : f.A +//│ ║ ^^^^^^^^^^^^^^^^^^ +//│ ╟── type variable `A` leaks out of its scope +//│ ║ l.68: fun foo(f: Foo): Int = if f is Foo(a) then a : f.A +//│ ║ ^^ +//│ ╟── into type `Int` +//│ ║ l.68: fun foo(f: Foo): Int = if f is Foo(a) then a : f.A +//│ ╙── ^^^ +//│ fun foo: (f: Foo[anything]) -> Int + +:e +fun foo(f: Foo[?]): Int = if f is Foo(a) then a : f.A else 0 +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.93: fun foo(f: Foo[?]): Int = if f is Foo(a) then a : f.A else 0 +//│ ╙── ^ +//│ fun foo: (f: Foo[error]) -> Int + +fun foo(f: Foo['a]) = f.a : f.A +//│ fun foo: forall 'a. (f: Foo['a]) -> 'a + +fun foo(a, f: Foo[a]): Int = f.a : f.A +//│ fun foo: forall 'a. ('a, f: Foo['a]) -> Int +//│ where +//│ 'a <: Int + +fun bar(f): Int = f.a : f.A +//│ fun bar: forall 'A. {A :> 'A <: Int, a: 'A} -> Int + +foo(2, Foo(1)) +//│ Int +//│ res +//│ = 1 + +bar(Foo(1)) +//│ Int +//│ res +//│ = 1 + +class Foo[A](val a: A -> A) +//│ class Foo[A](a: A -> A) + +fun foo(f: Foo) = f.a +//│ fun foo: (f: Foo[?]) -> ??A -> ??A0 + +fun foo(f: Foo) = () +//│ fun foo: (f: Foo[?]) -> () + +fun foo(f) = f : Foo +//│ fun foo: Foo[?] -> Foo[?] + +abstract class Foo[type T]: Bar +class Bar(val b: Int) extends Foo[Int] +//│ abstract class Foo[T]: Bar +//│ class Bar(b: Int) extends Foo + +// TODO +fun foo(x: Foo[?]) = if x is Bar then x.b : x.T +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.138: fun foo(x: Foo[?]) = if x is Bar then x.b : x.T +//│ ╙── ^ +//│ fun foo: (x: Foo[error]) -> Int + +foo(Bar(1)) +//│ Int +//│ res +//│ = 1 + +fun foo(x: Foo['a]) = if x is Bar then x.b : x.T +//│ fun foo: forall 'a. (x: Foo['a]) -> Int diff --git a/shared/src/test/diff/nu/RawUnionTraitSignatures.mls b/shared/src/test/diff/nu/RawUnionTraitSignatures.mls index d2671a4aef..6480b1b8cf 100644 --- a/shared/src/test/diff/nu/RawUnionTraitSignatures.mls +++ b/shared/src/test/diff/nu/RawUnionTraitSignatures.mls @@ -89,6 +89,7 @@ trait Base2: Foo['FigureItOut] //│ = [Function: res] // :e +// FIXME (b: Base2) => b : Foo['X] //│ forall 'X. (b: Base2) -> Foo['X] //│ where @@ -101,7 +102,7 @@ trait Base2: Foo['FigureItOut] :e class Impl extends Base2 //│ ╔══[ERROR] Type mismatch in type declaration: -//│ ║ l.102: class Impl extends Base2 +//│ ║ l.103: class Impl extends Base2 //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^ //│ ╟── expression of type `#Impl` is not an instance of type `Foo` //│ ╟── Note: constraint arises from applied type reference: @@ -117,19 +118,19 @@ class Impl extends Base2 :e (x: Impl) => x : Base2 //│ ╔══[ERROR] Type mismatch in type ascription: -//│ ║ l.118: (x: Impl) => x : Base2 +//│ ║ l.119: (x: Impl) => x : Base2 //│ ║ ^ //│ ╟── type `Impl` is not an instance of type `Foo` -//│ ║ l.118: (x: Impl) => x : Base2 +//│ ║ l.119: (x: Impl) => x : Base2 //│ ║ ^^^^ //│ ╟── but it flows into reference with expected type `#Foo` -//│ ║ l.118: (x: Impl) => x : Base2 +//│ ║ l.119: (x: Impl) => x : Base2 //│ ║ ^ //│ ╟── Note: constraint arises from applied type reference: //│ ║ l.78: trait Base2: Foo['FigureItOut] //│ ║ ^^^^^^^^^^^^^^^^^ //│ ╟── from type reference: -//│ ║ l.118: (x: Impl) => x : Base2 +//│ ║ l.119: (x: Impl) => x : Base2 //│ ╙── ^^^^^ //│ (x: Impl) -> Base2 //│ res @@ -138,13 +139,13 @@ class Impl extends Base2 :e class Impl() extends Base2, Foo //│ ╔══[ERROR] Type error in type declaration -//│ ║ l.139: class Impl() extends Base2, Foo +//│ ║ l.140: class Impl() extends Base2, Foo //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ ╟── type variable `'FigureItOut` leaks out of its scope //│ ║ l.78: trait Base2: Foo['FigureItOut] //│ ╙── ^^^^^^^^^^^^ //│ ╔══[ERROR] Member `x` is declared (or its declaration is inherited) but is not implemented in `Impl` -//│ ║ l.139: class Impl() extends Base2, Foo +//│ ║ l.140: class Impl() extends Base2, Foo //│ ║ ^^^^ //│ ╟── Declared here: //│ ║ l.5: trait Foo[A] { fun x: A } @@ -158,11 +159,11 @@ class Impl() extends Base2, Foo { fun x = 1 } //│ ╔══[ERROR] Type error in type declaration -//│ ║ l.157: class Impl() extends Base2, Foo { +//│ ║ l.158: class Impl() extends Base2, Foo { //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.158: fun x = 1 +//│ ║ l.159: fun x = 1 //│ ║ ^^^^^^^^^^^ -//│ ║ l.159: } +//│ ║ l.160: } //│ ║ ^ //│ ╟── type variable `'FigureItOut` leaks out of its scope //│ ║ l.78: trait Base2: Foo['FigureItOut] @@ -179,10 +180,10 @@ Impl().x :e Impl() : Base2 //│ ╔══[ERROR] Type error in type ascription -//│ ║ l.180: Impl() : Base2 +//│ ║ l.181: Impl() : Base2 //│ ║ ^^^^^^ //│ ╟── type variable `'FigureItOut` leaks out of its scope -//│ ║ l.158: fun x = 1 +//│ ║ l.159: fun x = 1 //│ ╙── ^ //│ Base2 //│ res @@ -191,10 +192,10 @@ Impl() : Base2 :e (Impl() : Base2).x //│ ╔══[ERROR] Type error in type ascription -//│ ║ l.192: (Impl() : Base2).x +//│ ║ l.193: (Impl() : Base2).x //│ ║ ^^^^^^ //│ ╟── type variable `'FigureItOut` leaks out of its scope -//│ ║ l.158: fun x = 1 +//│ ║ l.159: fun x = 1 //│ ╙── ^ //│ ??FigureItOut //│ res @@ -205,27 +206,27 @@ class Impl2() extends Base2, Foo[Int] { fun x = 1 } //│ ╔══[ERROR] Type error in type declaration -//│ ║ l.204: class Impl2() extends Base2, Foo[Int] { +//│ ║ l.205: class Impl2() extends Base2, Foo[Int] { //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.205: fun x = 1 +//│ ║ l.206: fun x = 1 //│ ║ ^^^^^^^^^^^ -//│ ║ l.206: } +//│ ║ l.207: } //│ ║ ^ //│ ╟── type variable `'FigureItOut` leaks out of its scope -//│ ║ l.204: class Impl2() extends Base2, Foo[Int] { +//│ ║ l.205: class Impl2() extends Base2, Foo[Int] { //│ ╙── ^^^ //│ ╔══[ERROR] Type error in type declaration -//│ ║ l.204: class Impl2() extends Base2, Foo[Int] { +//│ ║ l.205: class Impl2() extends Base2, Foo[Int] { //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.205: fun x = 1 +//│ ║ l.206: fun x = 1 //│ ║ ^^^^^^^^^^^ -//│ ║ l.206: } +//│ ║ l.207: } //│ ║ ^ //│ ╟── type variable `'FigureItOut` leaks out of its scope //│ ║ l.78: trait Base2: Foo['FigureItOut] //│ ║ ^^^^^^^^^^^^ //│ ╟── into type `Int` -//│ ║ l.204: class Impl2() extends Base2, Foo[Int] { +//│ ║ l.205: class Impl2() extends Base2, Foo[Int] { //│ ╙── ^^^ //│ class Impl2() extends Base2, Foo { //│ fun x: 1 @@ -234,10 +235,10 @@ class Impl2() extends Base2, Foo[Int] { :e (Impl2() : Base2).x //│ ╔══[ERROR] Type error in type ascription -//│ ║ l.235: (Impl2() : Base2).x +//│ ║ l.236: (Impl2() : Base2).x //│ ║ ^^^^^^^ //│ ╟── type variable `'FigureItOut` leaks out of its scope -//│ ║ l.204: class Impl2() extends Base2, Foo[Int] { +//│ ║ l.205: class Impl2() extends Base2, Foo[Int] { //│ ╙── ^^^ //│ ??FigureItOut //│ res diff --git a/shared/src/test/diff/nu/TODO_Classes.mls b/shared/src/test/diff/nu/TODO_Classes.mls index 03707081cf..d35c0bb4da 100644 --- a/shared/src/test/diff/nu/TODO_Classes.mls +++ b/shared/src/test/diff/nu/TODO_Classes.mls @@ -15,7 +15,7 @@ class D(x: Int) :e fun foo(c) = new c -//│ ╔══[ERROR] type identifier not found: c +//│ ╔══[ERROR] Unexpected type `?a` after `new` keyword //│ ║ l.17: fun foo(c) = new c //│ ╙── ^ //│ fun foo: anything -> error @@ -39,7 +39,7 @@ foo(C) :e fun bar(c) = new c(123) -//│ ╔══[ERROR] type identifier not found: c +//│ ╔══[ERROR] Unexpected type `?a` after `new` keyword //│ ║ l.41: fun bar(c) = new c(123) //│ ╙── ^ //│ fun bar: anything -> error @@ -100,10 +100,13 @@ let c = new Cls // FIXME let y: c.A = c.x -//│ ╔══[ERROR] type identifier not found: c +//│ ╔══[ERROR] Type `Cls[?A]` does not contain member `A` //│ ║ l.102: let y: c.A = c.x -//│ ╙── ^ -//│ /!!!\ Uncaught error: scala.NotImplementedError: an implementation is missing +//│ ╙── ^^ +//│ let y: error +//│ y +//│ Runtime error: +//│ RangeError: Maximum call stack size exceeded @@ -123,14 +126,14 @@ fun test(a: Object) = if a is Cls then a.x else error //│ ╔══[ERROR] Type error in `case` expression -//│ ║ l.122: fun test(a: Object) = if a is +//│ ║ l.125: fun test(a: Object) = if a is //│ ║ ^^^^ -//│ ║ l.123: Cls then a.x +//│ ║ l.126: Cls then a.x //│ ║ ^^^^^^^^^^^^^^ -//│ ║ l.124: else error +//│ ║ l.127: else error //│ ║ ^^^^^^^^^^^^ //│ ╟── type variable `A` leaks out of its scope -//│ ║ l.113: class Cls[A] { fun x: A = x; fun g: A -> Int; fun g = g } +//│ ║ l.116: class Cls[A] { fun x: A = x; fun g: A -> Int; fun g = g } //│ ╙── ^ //│ fun test: (a: Object) -> anything @@ -139,14 +142,14 @@ fun test(a: Object) = if a is Cls then a.g(a.x) // a.x : a.A ; a.g : a.A -> a.A else 0 //│ ╔══[ERROR] Type error in `case` expression -//│ ║ l.138: fun test(a: Object) = if a is +//│ ║ l.141: fun test(a: Object) = if a is //│ ║ ^^^^ -//│ ║ l.139: Cls then a.g(a.x) // a.x : a.A ; a.g : a.A -> a.A +//│ ║ l.142: Cls then a.g(a.x) // a.x : a.A ; a.g : a.A -> a.A //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.140: else 0 +//│ ║ l.143: else 0 //│ ║ ^^^^^^^^ //│ ╟── type variable `A` leaks out of its scope -//│ ║ l.113: class Cls[A] { fun x: A = x; fun g: A -> Int; fun g = g } +//│ ║ l.116: class Cls[A] { fun x: A = x; fun g: A -> Int; fun g = g } //│ ╙── ^ //│ fun test: (a: Object) -> Int @@ -210,11 +213,11 @@ fun test(f: ((IntLit | BoolLit) -> Int)) = :e class OopsLit() extends Expr[Bool] //│ ╔══[ERROR] Type mismatch in type declaration: -//│ ║ l.211: class OopsLit() extends Expr[Bool] +//│ ║ l.214: class OopsLit() extends Expr[Bool] //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ ╟── expression of type `#OopsLit` does not match type `BoolLit | IntLit` //│ ╟── Note: constraint arises from union type: -//│ ║ l.199: abstract class Expr[A]: (IntLit | BoolLit) {} +//│ ║ l.202: abstract class Expr[A]: (IntLit | BoolLit) {} //│ ╙── ^^^^^^^^^^^^^^^^^^ //│ class OopsLit() extends Expr diff --git a/shared/src/test/diff/nu/TypeMemberBounds.mls b/shared/src/test/diff/nu/TypeMemberBounds.mls new file mode 100644 index 0000000000..ef749a3f8d --- /dev/null +++ b/shared/src/test/diff/nu/TypeMemberBounds.mls @@ -0,0 +1,110 @@ +:NewDefs + +class Foo[] +//│ class Foo { +//│ constructor() +//│ } + +class Foo[A restricts Bool] +//│ class Foo[A] { +//│ constructor() +//│ } + +class Foo[A extends Int] +//│ class Foo[A] { +//│ constructor() +//│ } + +class Foo[type A restricts Int extends Int] +//│ class Foo[A] { +//│ constructor() +//│ } + +class Foo[in A restricts Int] +//│ class Foo[A] { +//│ constructor() +//│ } + + +class Foo[A restricts Bool, B extends Int] +//│ class Foo[A, B] { +//│ constructor() +//│ } + +:pe +class Foo[type restricts] +//│ ╔══[PARSE ERROR] dangling visible type member +//│ ║ l.35: class Foo[type restricts] +//│ ╙── ^^^^ +//│ ╔══[PARSE ERROR] Unexpected 'restricts' keyword here +//│ ║ l.35: class Foo[type restricts] +//│ ╙── ^^^^^^^^^ +//│ class Foo { +//│ constructor() +//│ } + +:pe +class Foo[type extends] +//│ ╔══[PARSE ERROR] dangling visible type member +//│ ║ l.47: class Foo[type extends] +//│ ╙── ^^^^ +//│ ╔══[PARSE ERROR] Unexpected 'extends' keyword here +//│ ║ l.47: class Foo[type extends] +//│ ╙── ^^^^^^^ +//│ class Foo { +//│ constructor() +//│ } + +:pe +class Foo[restricts Int] +//│ ╔══[PARSE ERROR] Unexpected 'restricts' keyword here +//│ ║ l.59: class Foo[restricts Int] +//│ ╙── ^^^^^^^^^ +//│ class Foo { +//│ constructor() +//│ } + +:pe +class Foo[restricts extends] +//│ ╔══[PARSE ERROR] Unexpected 'restricts' keyword here +//│ ║ l.68: class Foo[restricts extends] +//│ ╙── ^^^^^^^^^ +//│ class Foo { +//│ constructor() +//│ } + +:pe +class Foo[extends Int] +//│ ╔══[PARSE ERROR] Unexpected 'extends' keyword here +//│ ║ l.77: class Foo[extends Int] +//│ ╙── ^^^^^^^ +//│ class Foo { +//│ constructor() +//│ } + +:pe +class Foo[A extends] +//│ ╔══[PARSE ERROR] dangling extends keyword +//│ ║ l.86: class Foo[A extends] +//│ ╙── ^^^^^^^ +//│ class Foo[A] { +//│ constructor() +//│ } + +:pe +class Foo[B restricts] +//│ ╔══[PARSE ERROR] dangling restricts keyword +//│ ║ l.95: class Foo[B restricts] +//│ ╙── ^^^^^^^^^ +//│ class Foo[B] { +//│ constructor() +//│ } + +:pe +class Foo[extends] +//│ ╔══[PARSE ERROR] Unexpected 'extends' keyword here +//│ ║ l.104: class Foo[extends] +//│ ╙── ^^^^^^^ +//│ class Foo { +//│ constructor() +//│ } diff --git a/shared/src/test/diff/nu/TypeMembers.mls b/shared/src/test/diff/nu/TypeMembers.mls new file mode 100644 index 0000000000..d558ccdef0 --- /dev/null +++ b/shared/src/test/diff/nu/TypeMembers.mls @@ -0,0 +1,113 @@ +:NewDefs + +:AllowTypeErrors + +class Test { type T = Int } +//│ class Test { +//│ constructor() +//│ type T = Int +//│ } + +1 : Test.T +//│ Int + + +trait Test { type T = Int } +//│ trait Test { +//│ type T = Int +//│ } + +1 : Test.T +//│ ╔══[ERROR] Access to type alias member T not yet supported +//│ ║ l.20: 1 : Test.T +//│ ╙── ^^ +//│ ╔══[ERROR] Type mismatch in type selection: +//│ ║ l.20: 1 : Test.T +//│ ║ ^^ +//│ ╙── type `error` cannot be reassigned +//│ error + +// TODO inspect +class Foo[T](x: T) { + type T = T +} +//│ class Foo[T](x: T) { +//│ type T = T +//│ } + +1 : Foo(1).T +//│ ╔══[ERROR] Access to type alias member T not yet supported +//│ ║ l.38: 1 : Foo(1).T +//│ ╙── ^^ +//│ ╔══[ERROR] Type mismatch in type selection: +//│ ║ l.38: 1 : Foo(1).T +//│ ║ ^^ +//│ ╙── type `error` cannot be reassigned +//│ error + +:e +false : Foo(1).T +//│ ╔══[ERROR] Access to type alias member T not yet supported +//│ ║ l.49: false : Foo(1).T +//│ ╙── ^^ +//│ ╔══[ERROR] Type mismatch in type selection: +//│ ║ l.49: false : Foo(1).T +//│ ║ ^^ +//│ ╙── type `error` cannot be reassigned +//│ error + +// TODO +class Foo[type T](x: T) { + type T = T +} +//│ class Foo[T](x: T) { +//│ type T = T +//│ } + +// TODO +class Foo[type T](x: Int) { + type T = Int +} +//│ class Foo[T](x: Int) { +//│ type T = Int +//│ } + +abstract class Foo { type T = Int } +//│ abstract class Foo { +//│ type T = Int +//│ } + +:e +class Bar extends Foo { type T = Bool } +//│ ╔══[ERROR] Type alias member 'T' cannot override type alias member of the same name declared in parent +//│ ║ l.82: class Bar extends Foo { type T = Bool } +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── Originally declared here: +//│ ║ l.76: abstract class Foo { type T = Int } +//│ ╙── ^^^^^^ +//│ class Bar extends Foo { +//│ constructor() +//│ type T = Bool +//│ } + +abstract class Foo[type T] +//│ abstract class Foo[T] + +:e +class Bar extends Foo { type T = Bool } +//│ ╔══[ERROR] Type alias member 'T' cannot override type alias member of the same name declared in parent +//│ ║ l.98: class Bar extends Foo { type T = Bool } +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +//│ ╟── Originally declared here: +//│ ║ l.94: abstract class Foo[type T] +//│ ╙── ^ +//│ class Bar extends Foo { +//│ constructor() +//│ type T = Bool +//│ } + +// TODO +module Foo { type A = A } +//│ module Foo { +//│ type A = A +//│ } diff --git a/shared/src/test/diff/nu/TypeSel.mls b/shared/src/test/diff/nu/TypeSel.mls new file mode 100644 index 0000000000..4fd84201b4 --- /dev/null +++ b/shared/src/test/diff/nu/TypeSel.mls @@ -0,0 +1,431 @@ +:NewDefs + +// * To support: +// * - type parameter members +// * - accessing type members in variables (for now, no need for path dependence) +// * - Interpret absence of type parameters as some fresh type variables: `Foo` means `Foo['a]` + +// * For the future: +// * - Type refinement syntax, as in `Foo { A = Int }` +// * - Support wildcard type argument syntax: `Foo[?]` (for what we currently write `Foo`) +// * - `as` syntax for upcasting + +class Foo[A](val a: A) +//│ class Foo[A](a: A) + +:e +fun foo(f: Foo[Int]): f.A = f.a +//│ ╔══[ERROR] Type `Foo[Int]` does not contain member `A` +//│ ║ l.17: fun foo(f: Foo[Int]): f.A = f.a +//│ ╙── ^^ +//│ fun foo: (f: Foo[Int]) -> error + +class Foo[type A] { + fun f: A -> Int + fun f(x) = 1 +} +//│ class Foo[A] { +//│ constructor() +//│ fun f: A -> Int +//│ } + + +fun foo(f: Foo[Int], g: Foo[f.A], x: f.A) = g.f(f.f(x)) +//│ fun foo: (f: Foo[Int], g: Foo[Int], x: Int) -> Int + +class Bar(val f: Foo[Int]) +//│ class Bar(f: Foo[Int]) + +:e +fun foo(b: Bar): b.f.A = 1 +//│ ╔══[ERROR] Type mismatch in type selection: +//│ ║ l.40: fun foo(b: Bar): b.f.A = 1 +//│ ║ ^^ +//│ ╙── type `Foo[Int]` cannot be reassigned +//│ fun foo: (b: Bar) -> Int + +fun bar(b: Bar) = b.f.f(1) +//│ fun bar: (b: Bar) -> Int + +fun foo(b: Bar) = + let f = id(b).f + let g = x => f.f(x + 1) + g(1) : f.A +//│ fun foo: (b: Bar) -> Int + +:e +fun foo(f: Foo, x: f.A) = f.f(x) +//│ ╔══[ERROR] Type error in application +//│ ║ l.57: fun foo(f: Foo, x: f.A) = f.f(x) +//│ ║ ^^^^^^ +//│ ╟── type variable `A` leaks out of its scope +//│ ║ l.57: fun foo(f: Foo, x: f.A) = f.f(x) +//│ ║ ^^ +//│ ╟── back into type variable `A` +//│ ║ l.23: class Foo[type A] { +//│ ╙── ^ +//│ fun foo: (f: Foo[nothing], x: ??A) -> (Int | error) + +fun foo(f: Foo['a], x) = f.f(x) +//│ fun foo: forall 'a. (f: Foo['a], 'a) -> Int + +fun foo(p, q, f: (p,q) -> Int) = f(p,q) +//│ fun foo: forall 'a 'b. ('a, 'b, f: ('a, 'b) -> Int) -> Int + +foo(1, 0, (x, y) => x + y) +//│ Int +//│ res +//│ = 1 + +class Foo[type A](val a: A) +//│ class Foo[A](a: A) + +fun foo(f: Foo[Int]): Int = f.a : f.A +//│ fun foo: (f: Foo[Int]) -> Int + +fun foo[T](f: Foo[T]): T = f.a : f.A +//│ fun foo: forall 'T. (f: Foo['T]) -> 'T + +// raw type example +// TODO support +fun foo(f: Foo): Int = f.a : f.A +//│ ╔══[ERROR] Type error in type ascription +//│ ║ l.91: fun foo(f: Foo): Int = f.a : f.A +//│ ║ ^^^ +//│ ╟── type variable `A` leaks out of its scope +//│ ║ l.91: fun foo(f: Foo): Int = f.a : f.A +//│ ║ ^^^ +//│ ╟── back into type variable `A` +//│ ║ l.91: fun foo(f: Foo): Int = f.a : f.A +//│ ╙── ^^ +//│ ╔══[ERROR] Type error in type ascription +//│ ║ l.91: fun foo(f: Foo): Int = f.a : f.A +//│ ║ ^^^ +//│ ╟── type variable `A` leaks out of its scope +//│ ║ l.91: fun foo(f: Foo): Int = f.a : f.A +//│ ║ ^^ +//│ ╟── into type `Int` +//│ ║ l.91: fun foo(f: Foo): Int = f.a : f.A +//│ ╙── ^^^ +//│ fun foo: (f: Foo[anything]) -> Int + +:e +fun foo(f: Foo) = f.a : f.A +//│ ╔══[ERROR] Type error in type ascription +//│ ║ l.113: fun foo(f: Foo) = f.a : f.A +//│ ║ ^^^ +//│ ╟── type variable `A` leaks out of its scope +//│ ║ l.113: fun foo(f: Foo) = f.a : f.A +//│ ║ ^^^ +//│ ╟── back into type variable `A` +//│ ║ l.113: fun foo(f: Foo) = f.a : f.A +//│ ╙── ^^ +//│ fun foo: (f: Foo[anything]) -> ??A + +fun foo(f: Foo['a]): Int = f.a : f.A +//│ fun foo: forall 'a. (f: Foo['a]) -> Int +//│ where +//│ 'a <: Int + +:e +fun foo(f: Foo[?]): Int = f.a : f.A +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.131: fun foo(f: Foo[?]): Int = f.a : f.A +//│ ╙── ^ +//│ fun foo: (f: Foo[error]) -> Int + +fun foo(f) = f.a : f.A +//│ fun foo: forall 'A 'A0. {A :> 'A <: 'A0, a: 'A} -> 'A0 + +fun foo(f): Int = f.a : f.A +//│ fun foo: forall 'A. {A :> 'A <: Int, a: 'A} -> Int + +foo(Foo(1)) +//│ Int +//│ res +//│ = 1 + +:e +foo(Foo(true)) +//│ ╔══[ERROR] Type mismatch in application: +//│ ║ l.149: foo(Foo(true)) +//│ ║ ^^^^^^^^^^^^^^ +//│ ╟── reference of type `true` is not an instance of `Int` +//│ ║ l.149: foo(Foo(true)) +//│ ║ ^^^^ +//│ ╟── Note: constraint arises from type reference: +//│ ║ l.140: fun foo(f): Int = f.a : f.A +//│ ║ ^^^ +//│ ╟── from type selection: +//│ ║ l.140: fun foo(f): Int = f.a : f.A +//│ ╙── ^^ +//│ Int | error +//│ res +//│ = true + +abstract class Foo[type A]: Bar | Baz +module Bar extends Foo[Int] +module Baz extends Foo[Str] +//│ abstract class Foo[A]: Bar | Baz +//│ module Bar extends Foo +//│ module Baz extends Foo + +123 : Bar.A +//│ Int +//│ res +//│ = 123 + +:e +"bad": Bar.A +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.179: "bad": Bar.A +//│ ║ ^^^^^ +//│ ╟── string literal of type `"bad"` is not an instance of type `Int` +//│ ╟── Note: constraint arises from type reference: +//│ ║ l.167: module Bar extends Foo[Int] +//│ ║ ^^^ +//│ ╟── from type selection: +//│ ║ l.179: "bad": Bar.A +//│ ╙── ^^ +//│ Int +//│ res +//│ = 'bad' + +fun foo(f, x) = x : f.A +//│ fun foo: forall 'A 'A0. ({A :> 'A <: 'A0}, 'A) -> 'A0 + +foo(Bar, 123) +//│ Int +//│ res +//│ = 123 + +fun test(f) = if f is + Bar then 123 : f.A +//│ fun test: Bar -> Int + +fun test(f) = if f is + Bar then 123 : f.A + Baz then "hello" : f.A +//│ fun test: (Bar | Baz) -> (Int | Str) + +[test(Bar), test(Baz)] +//│ [Int | Str, Int | Str] +//│ res +//│ = [ 123, 'hello' ] + +fun test(f: Foo['a]) = if f is Bar then 123 : f.A else error +//│ fun test: forall 'a. (f: Foo['a]) -> Int + +fun test(f: Foo[Int]) = if f is Bar then 123 : f.A else error +//│ fun test: (f: Foo[Int]) -> Int + +fun test(f: Foo) = if f is Bar then 123 : f.A else error +//│ fun test: (f: Foo[?]) -> Int + +// TODO +fun test(f: Foo[?]) = if f is Bar then 123 : f.A else error +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.226: fun test(f: Foo[?]) = if f is Bar then 123 : f.A else error +//│ ╙── ^ +//│ fun test: (f: Foo[error]) -> Int + +:e +fun test(f: Foo) = if f is + Bar then 123 : f.A + Baz then "hello" : f.A +//│ ╔══[ERROR] Type mismatch in `case` expression: +//│ ║ l.233: fun test(f: Foo) = if f is +//│ ║ ^^^^ +//│ ║ l.234: Bar then 123 : f.A +//│ ║ ^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.235: Baz then "hello" : f.A +//│ ║ ^^^^^^^^^^^^^^^^^^ +//│ ╟── type `Foo[?]` does not match type `Bar | Baz` +//│ ║ l.233: fun test(f: Foo) = if f is +//│ ║ ^^^ +//│ ╟── but it flows into reference with expected type `Bar | Baz` +//│ ║ l.233: fun test(f: Foo) = if f is +//│ ╙── ^ +//│ fun test: (f: Foo[?]) -> (Int | Str) + +[test(Bar), test(Baz)] +//│ [Int | Str, Int | Str] +//│ res +//│ = [ 123, 'hello' ] + +// TODO +fun test(f: Foo[?]) = if f is + Bar then 123 : f.A + Baz then "hello" : f.A +//│ ╔══[ERROR] Invalid use of wildcard type `?` here +//│ ║ l.257: fun test(f: Foo[?]) = if f is +//│ ╙── ^ +//│ fun test: (f: Foo[error]) -> (Int | Str) + +// TODO +fun test[T](f: Foo[T]): T = if f is + Bar then 123 : f.A + Baz then "hello" : f.A +//│ ╔══[ERROR] Type mismatch in type ascription: +//│ ║ l.266: fun test[T](f: Foo[T]): T = if f is +//│ ║ ^^^^ +//│ ║ l.267: Bar then 123 : f.A +//│ ║ ^^^^^^^^^^^^^^^^^^^^ +//│ ║ l.268: Baz then "hello" : f.A +//│ ║ ^^^^^^^^^^^^^^^^^^ +//│ ╟── type `Int` does not match type `T` +//│ ║ l.167: module Bar extends Foo[Int] +//│ ║ ^^^ +//│ ╟── but it flows into type selection with expected type `T` +//│ ║ l.267: Bar then 123 : f.A +//│ ║ ^^ +//│ ╟── Note: constraint arises from method type parameter: +//│ ║ l.266: fun test[T](f: Foo[T]): T = if f is +//│ ╙── ^ +//│ fun test: forall 'T. (f: Foo['T]) -> 'T + +:e +class Foo[type A] +class Bar[type A] extends Foo[A] +//│ ╔══[ERROR] Inherited parameter named 'A' is not virtual and cannot be overridden +//│ ║ l.289: class Bar[type A] extends Foo[A] +//│ ║ ^ +//│ ╟── Originally declared here: +//│ ║ l.288: class Foo[type A] +//│ ╙── ^ +//│ class Foo[A] { +//│ constructor() +//│ } +//│ class Bar[A] extends Foo { +//│ constructor() +//│ } + +class Foo[type A] +//│ class Foo[A] { +//│ constructor() +//│ } + +:e +class Bar[type A] extends Foo[A -> A] +//│ ╔══[ERROR] Inherited parameter named 'A' is not virtual and cannot be overridden +//│ ║ l.309: class Bar[type A] extends Foo[A -> A] +//│ ║ ^ +//│ ╟── Originally declared here: +//│ ║ l.303: class Foo[type A] +//│ ╙── ^ +//│ class Bar[A] extends Foo { +//│ constructor() +//│ } + +:e +class Bar[type A] extends Foo[Int] +//│ ╔══[ERROR] Inherited parameter named 'A' is not virtual and cannot be overridden +//│ ║ l.321: class Bar[type A] extends Foo[Int] +//│ ║ ^ +//│ ╟── Originally declared here: +//│ ║ l.303: class Foo[type A] +//│ ╙── ^ +//│ class Bar[A] extends Foo { +//│ constructor() +//│ } + + + + +class Foo[A] +//│ class Foo[A] { +//│ constructor() +//│ } + +// FIXME +// Would be nice: +fun foo(x: Foo['a], y) = y : x.A // interpreted as `y : x.Foo#A` +//│ ╔══[ERROR] Type `Foo['a]` does not contain member `A` +//│ ║ l.342: fun foo(x: Foo['a], y) = y : x.A // interpreted as `y : x.Foo#A` +//│ ╙── ^^ +//│ fun foo: forall 'a. (x: Foo['a], error) -> error + +fun foo(x, y) = y : x.A +//│ fun foo: forall 'A 'A0. ({A :> 'A <: 'A0}, 'A) -> 'A0 + +// FIXME +fun bar(f: Foo['a], y) = foo(f, y) +//│ ╔══[ERROR] Type `Foo['a]` does not contain member `A` +//│ ║ l.348: fun foo(x, y) = y : x.A +//│ ╙── ^^ +//│ fun bar: forall 'a. (f: Foo['a], error) -> error + +class Bar(val A: Int) +//│ class Bar(A: Int) + +abstract class C[type A]: C1 | C2 +class C1(val s: Bool) extends C[Bool] +class C2(val i: Int) extends C[Int] +//│ abstract class C[A]: C1 | C2 +//│ class C1(s: Bool) extends C +//│ class C2(i: Int) extends C + +let f = (t, x: t.A) => x + t.i +//│ let f: forall 'A. ({A :> 'A <: Int, i: Int}, x: 'A) -> Int +//│ f +//│ = [Function: f] + +f(C2(1), 2) +//│ Int +//│ res +//│ = 3 + +let g = (t, x: t) => t && x +//│ let g: (Bool, x: Bool) -> Bool +//│ g +//│ = [Function: g] + +class Foo(val x: C1) { + fun foo(y: x.A) = y || y +} +//│ class Foo(x: C1) { +//│ fun foo: (y: Bool) -> Bool +//│ } + +Foo(C1(false)).foo(true) +//│ Bool +//│ res +//│ = true + +:pe +class Foo[in type] +//│ ╔══[PARSE ERROR] dangling variance information +//│ ║ l.396: class Foo[in type] +//│ ╙── ^^ +//│ ╔══[PARSE ERROR] Unexpected 'type' keyword here +//│ ║ l.396: class Foo[in type] +//│ ╙── ^^^^ +//│ class Foo { +//│ constructor() +//│ } + +:pe +class Foo[type] +//│ ╔══[PARSE ERROR] dangling visible type member +//│ ║ l.408: class Foo[type] +//│ ╙── ^^^^ +//│ class Foo { +//│ constructor() +//│ } + +:pe +class Foo[type in] +//│ ╔══[PARSE ERROR] dangling type member and variance information +//│ ║ l.417: class Foo[type in] +//│ ╙── ^^^^^^^ +//│ class Foo { +//│ constructor() +//│ } + +// FIXME crash +:pe +fun foo[typ](x) +//│ ╔══[PARSE ERROR] Expected ':' or '=' followed by a function body or signature; found end of input instead +//│ ║ l.427: fun foo[typ](x) +//│ ╙── ^ +//│ fun foo: anything -> () diff --git a/shared/src/test/diff/nu/TypeSelections.mls b/shared/src/test/diff/nu/TypeSelections.mls index 909a1eff52..ea3cad1180 100644 --- a/shared/src/test/diff/nu/TypeSelections.mls +++ b/shared/src/test/diff/nu/TypeSelections.mls @@ -29,10 +29,16 @@ foo(M.mkC(42)) :e 42 : M.mkC -//│ ╔══[ERROR] Illegal selection of value member in type position +//│ ╔══[ERROR] Type mismatch in type selection: +//│ ║ l.31: 42 : M.mkC +//│ ║ ^^^^ +//│ ╟── member of type `(n: Int) -> C` is not mutable +//│ ║ l.7: fun mkC = C +//│ ║ ^^^^^^^ +//│ ╟── but it flows into type selection with expected type `?mkC` //│ ║ l.31: 42 : M.mkC //│ ╙── ^^^^ -//│ error +//│ (n: Int) -> C //│ res //│ = 42 diff --git a/shared/src/test/diff/nu/TypeVariables.mls b/shared/src/test/diff/nu/TypeVariables.mls index 327b6ca005..70f9e30d8a 100644 --- a/shared/src/test/diff/nu/TypeVariables.mls +++ b/shared/src/test/diff/nu/TypeVariables.mls @@ -26,7 +26,7 @@ fun x: [Int -> Int] = [id : forall 'a: 'a -> 'a,] //│ ╔══[PARSE ERROR] Unexpected end of square bracket section; an expression was expected here //│ ║ l.25: fun x: [Int -> Int] = [id : forall 'a: 'a -> 'a,] //│ ╙── ^ -//│ ╔══[ERROR] type identifier not found: , +//│ ╔══[ERROR] cannot lift variable , to type //│ ║ l.25: fun x: [Int -> Int] = [id : forall 'a: 'a -> 'a,] //│ ╙── ^^^^^^^^^ //│ fun x: [Int -> Int] diff --git a/shared/src/test/diff/nu/TypreMembers.mls b/shared/src/test/diff/nu/TypreMembers.mls deleted file mode 100644 index af6a856b41..0000000000 --- a/shared/src/test/diff/nu/TypreMembers.mls +++ /dev/null @@ -1,30 +0,0 @@ -:NewDefs - - -class Test { type T = Int } -//│ class Test { -//│ constructor() -//│ type T = Int -//│ } - -1 : Test.T -//│ Int -//│ res -//│ = 1 - - -trait Test { type T = Int } -//│ trait Test { -//│ type T = Int -//│ } - -:e -1 : Test.T -//│ ╔══[ERROR] Illegal prefix of type selection: Test -//│ ║ l.22: 1 : Test.T -//│ ╙── ^^^^ -//│ error -//│ res -//│ = 1 - - diff --git a/shared/src/test/diff/nu/WeirdUnions.mls b/shared/src/test/diff/nu/WeirdUnions.mls index d5b600e875..d004621b2d 100644 --- a/shared/src/test/diff/nu/WeirdUnions.mls +++ b/shared/src/test/diff/nu/WeirdUnions.mls @@ -13,7 +13,7 @@ fun f: (Str | [Str, Int]) :e fun f: Str | (Str, Int) -//│ ╔══[ERROR] type identifier not found: , +//│ ╔══[ERROR] cannot lift variable , to type //│ ║ l.15: fun f: Str | (Str, Int) //│ ╙── ^^^^^^^^^^ //│ fun f: Str | error @@ -24,7 +24,7 @@ fun f: Str | ([Str, Int]) :e fun f: Str | ((Str, Int)) -//│ ╔══[ERROR] type identifier not found: , +//│ ╔══[ERROR] cannot lift variable , to type //│ ║ l.26: fun f: Str | ((Str, Int)) //│ ╙── ^^^^^^^^^^^^ //│ fun f: Str | error diff --git a/shared/src/test/diff/nu/repro_EvalNegNeg.mls b/shared/src/test/diff/nu/repro_EvalNegNeg.mls index f42ccd5a2b..ad71df6453 100644 --- a/shared/src/test/diff/nu/repro_EvalNegNeg.mls +++ b/shared/src/test/diff/nu/repro_EvalNegNeg.mls @@ -47,6 +47,6 @@ TestLang.eval(mk(0)) //│ = 0 //│ constrain calls : 179 //│ annoying calls : 51 -//│ subtyping calls : 1203 +//│ subtyping calls : 1194 diff --git a/shared/src/test/diff/parser/IfThenElse.mls b/shared/src/test/diff/parser/IfThenElse.mls index 7255013bc7..9af16127a4 100644 --- a/shared/src/test/diff/parser/IfThenElse.mls +++ b/shared/src/test/diff/parser/IfThenElse.mls @@ -440,8 +440,8 @@ let Some(x) = v //│ Parsed: {let Some = (x,) => v} v as Some(x) -//│ |v| |as| |Some|(|x|)| -//│ Parsed: {as(v,)(Some(x,),)} +//│ |v| |#as| |Some|(|x|)| +//│ Parsed: {v : Some[x]} diff --git a/shared/src/test/diff/tapl/NuSimplyTyped.mls b/shared/src/test/diff/tapl/NuSimplyTyped.mls index 65c3b0dba2..44adb5a78e 100644 --- a/shared/src/test/diff/tapl/NuSimplyTyped.mls +++ b/shared/src/test/diff/tapl/NuSimplyTyped.mls @@ -123,6 +123,7 @@ showTerm(App(Abs(Var("x"), _t("int"), Var("y")), Var("z"))) //│ res //│ = '((&x: int => z) z)' +// :e // FIXME recursion depth excess // Removing the return type annotation causes stack overflow. fun typeTerm(t: Term, ctx: TreeMap[Type]): Result[Type, Str] = if t is @@ -165,3 +166,4 @@ showTypeTerm(App(Var("f"), Lit("0", _t("int"))), insert(Empty, "f", _t("Str"))) //│ = 'Type error: expect the argument to be of type `int` but found `float`' //│ res //│ = 'Type error: cannot apply primitive type `Str`' + diff --git a/shared/src/test/diff/tapl/NuUntyped.mls b/shared/src/test/diff/tapl/NuUntyped.mls index a9427adc52..0811e4285f 100644 --- a/shared/src/test/diff/tapl/NuUntyped.mls +++ b/shared/src/test/diff/tapl/NuUntyped.mls @@ -1,4 +1,5 @@ :NewDefs +// :NoProvs fun (++) concatOp(a, b) = concat(a)(b) //│ fun (++) concatOp: (Str, Str) -> Str @@ -228,6 +229,20 @@ showHasFree(App(Abs(Var("x"), Var("x")), Var("x")), "y") //│ res //│ = '((&x. x) x) DOES NOT have free variable y' +// // :d +// fun fv(t) = +// if t is +// Var(name) then list1(error) +// App(lhs, rhs) then listConcat(error, fv(rhs)) + +// fun fv(t) = +// if t is +// Var(name) then list1(error) +// App(lhs, rhs) then listConcat(fv(lhs), fv(rhs)) + +:Fuel 100000 +// :d +// :ex fun fv(t) = if t is Var(name) then list1(name) @@ -236,6 +251,7 @@ fun fv(t) = //│ fun fv: forall 'A. (Abs | App | Var) -> (Cons['A] | Nil) //│ where //│ 'A :> Str +:ResetFuel fun showFv(t) = showTerm(t) ++ if fv(t) is @@ -319,7 +335,7 @@ fun subst(t, n, v) = _ then Abs(Var(name), subst(body, n, v)) App(lhs, rhs) then App(subst(lhs, n, v), subst(rhs, n, v)) _ then t -//│ fun subst: forall 'a. (Abs | App | Term & Object & 'a & ~#Abs & ~#App & ~#Var | Var, anything, Term & Object & 'a) -> ('a | Abs | App | Var) +//│ fun subst: forall 'a. (Abs | App | Term & Object & 'a & ~#Abs & ~#App & ~#Var | Var, anything, Term & Object & 'a) -> (Abs | App | Var | 'a) fun showSubst(t, n, v) = showTerm(t) ++ " [" ++ n ++ " / " ++ showTerm(v) ++ "]" ++ " => " ++ showTerm(subst(t, n, v)) From e02a2444c63036e5853fef522714e859c85e0f85 Mon Sep 17 00:00:00 2001 From: Meowcolm024 Date: Tue, 9 Apr 2024 18:47:58 +0800 Subject: [PATCH 2/2] cleanup --- shared/src/main/scala/mlscript/Typer.scala | 4 ---- shared/src/test/diff/nu/TypeMembers.mls | 8 ++++---- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/shared/src/main/scala/mlscript/Typer.scala b/shared/src/main/scala/mlscript/Typer.scala index cdd668da62..984048292f 100644 --- a/shared/src/main/scala/mlscript/Typer.scala +++ b/shared/src/main/scala/mlscript/Typer.scala @@ -640,10 +640,6 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool, val ne typeNamed(ty.toLoc, base.name, false) match { case R((_, tpnum)) => val realTargs = if (targs.size === tpnum) targs.map{ - // case b@Bounds(lb, ub) if newDefs => WildcardArg(rec(lb), rec(ub))(tyTp(b.toLoc, "wildcard")) - // case w@TypeName("?") if newDefs => - // val prov: TypeProvenance = tyTp(w.toLoc, "wildcard") - // WildcardArg(ExtrType(true)(prov), ExtrType(false)(prov))(prov) case ty => rec(ty) } else { err(msg"Wrong number of type arguments – expected ${tpnum.toString}, found ${ diff --git a/shared/src/test/diff/nu/TypeMembers.mls b/shared/src/test/diff/nu/TypeMembers.mls index d558ccdef0..9c9bd4c9b6 100644 --- a/shared/src/test/diff/nu/TypeMembers.mls +++ b/shared/src/test/diff/nu/TypeMembers.mls @@ -80,10 +80,10 @@ abstract class Foo { type T = Int } :e class Bar extends Foo { type T = Bool } //│ ╔══[ERROR] Type alias member 'T' cannot override type alias member of the same name declared in parent -//│ ║ l.82: class Bar extends Foo { type T = Bool } +//│ ║ l.81: class Bar extends Foo { type T = Bool } //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ ╟── Originally declared here: -//│ ║ l.76: abstract class Foo { type T = Int } +//│ ║ l.75: abstract class Foo { type T = Int } //│ ╙── ^^^^^^ //│ class Bar extends Foo { //│ constructor() @@ -96,10 +96,10 @@ abstract class Foo[type T] :e class Bar extends Foo { type T = Bool } //│ ╔══[ERROR] Type alias member 'T' cannot override type alias member of the same name declared in parent -//│ ║ l.98: class Bar extends Foo { type T = Bool } +//│ ║ l.97: class Bar extends Foo { type T = Bool } //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ ╟── Originally declared here: -//│ ║ l.94: abstract class Foo[type T] +//│ ║ l.93: abstract class Foo[type T] //│ ╙── ^ //│ class Bar extends Foo { //│ constructor()