From 9945ff1060d7dbbc73e8204397495b27fab8b3ce Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Sat, 17 Nov 2018 15:55:25 +0100 Subject: [PATCH 01/21] Revert "Handle higher-kinded GADT bounds" This reverts commit 756cd0a0ab8ba2d5f52be36c98206420732e2503. --- .../dotty/tools/dotc/core/TypeComparer.scala | 17 ++++++----------- compiler/src/dotty/tools/dotc/core/Types.scala | 2 +- 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 60ad1963ee29..e3fa098586ac 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -830,9 +830,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { * tp1 <:< tp2 using fourthTry (this might instantiate params in tp1) * tp1 <:< app2 using isSubType (this might instantiate params in tp2) */ - def compareLower(tycon2bounds: TypeBounds, followSuperType: Boolean): Boolean = + def compareLower(tycon2bounds: TypeBounds, tyconIsTypeRef: Boolean): Boolean = if ((tycon2bounds.lo `eq` tycon2bounds.hi) && !tycon2bounds.isInstanceOf[MatchAlias]) - if (followSuperType) recur(tp1, tp2.superType) + if (tyconIsTypeRef) recur(tp1, tp2.superType) else isSubApproxHi(tp1, tycon2bounds.lo.applyIfParameterized(args2)) else fallback(tycon2bounds.lo) @@ -841,15 +841,13 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { case param2: TypeParamRef => isMatchingApply(tp1) || canConstrain(param2) && canInstantiate(param2) || - compareLower(bounds(param2), followSuperType = false) + compareLower(bounds(param2), tyconIsTypeRef = false) case tycon2: TypeRef => isMatchingApply(tp1) || defn.isTypelevel_S(tycon2.symbol) && compareS(tp2, tp1, fromBelow = true) || { tycon2.info match { case info2: TypeBounds => - val gbounds2 = ctx.gadt.bounds(tycon2.symbol) - if (gbounds2 == null) compareLower(info2, followSuperType = true) - else compareLower(gbounds2 & info2, followSuperType = false) + compareLower(info2, tyconIsTypeRef = true) case info2: ClassInfo => tycon2.name.toString.startsWith("Tuple") && defn.isTupleType(tp2) && isSubType(tp1, tp2.toNestedPairs) || @@ -885,11 +883,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { case tycon1: TypeRef => val sym = tycon1.symbol !sym.isClass && ( - defn.isTypelevel_S(sym) && compareS(tp1, tp2, fromBelow = false) || { - val gbounds1 = ctx.gadt.bounds(tycon1.symbol) - if (gbounds1 == null) recur(tp1.superType, tp2) - else recur((gbounds1.hi & tycon1.info.bounds.hi).applyIfParameterized(args1), tp2) - }) + defn.isTypelevel_S(sym) && compareS(tp1, tp2, fromBelow = false) || + recur(tp1.superType, tp2)) case tycon1: TypeProxy => recur(tp1.superType, tp2) case _ => diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index b101ada545cb..183b1e7aa294 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -563,7 +563,7 @@ object Types { case _ => go(tp.superType) } - case tp: ThisType => + case tp: ThisType => // ??? inline goThis(tp) case tp: RefinedType => if (name eq tp.refinedName) goRefined(tp) else go(tp.parent) From fd94b218116521706f297be763cfe0a596fb776c Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Mon, 8 Oct 2018 14:58:04 +0200 Subject: [PATCH 02/21] Add GADT compilation tests --- .../test/dotty/tools/dotc/GadtTests.scala | 56 ++++++++++++ tests/gadt+checkOptions | 1 + tests/gadt+defaultOptions | 1 + tests/gadt+noCheckOptions | 1 + tests/gadt/NatsVects.ignore | 90 +++++++++++++++++++ tests/gadt/banal.scala | 15 ++++ tests/gadt/foo.scala | 11 +++ tests/gadt/injectivity.scala | 9 ++ tests/gadt/one.scala | 9 ++ tests/gadt/simpleEQ.scala | 13 +++ 10 files changed, 206 insertions(+) create mode 100644 compiler/test/dotty/tools/dotc/GadtTests.scala create mode 120000 tests/gadt+checkOptions create mode 120000 tests/gadt+defaultOptions create mode 120000 tests/gadt+noCheckOptions create mode 100644 tests/gadt/NatsVects.ignore create mode 100644 tests/gadt/banal.scala create mode 100644 tests/gadt/foo.scala create mode 100644 tests/gadt/injectivity.scala create mode 100644 tests/gadt/one.scala create mode 100644 tests/gadt/simpleEQ.scala diff --git a/compiler/test/dotty/tools/dotc/GadtTests.scala b/compiler/test/dotty/tools/dotc/GadtTests.scala new file mode 100644 index 000000000000..48791a2c68cd --- /dev/null +++ b/compiler/test/dotty/tools/dotc/GadtTests.scala @@ -0,0 +1,56 @@ +package dotty +package tools +package dotc + +import org.junit.{AfterClass, Test} +import vulpix._ + +import scala.concurrent.duration._ +import java.io.{File => JFile} + +class GadtTests extends ParallelTesting { + import TestConfiguration._ + import GadtTests._ + + // Test suite configuration -------------------------------------------------- + + def maxDuration = 30.seconds + def numberOfSlaves = 5 + def safeMode = Properties.testsSafeMode + def isInteractive = SummaryReport.isInteractive + def testFilter = Properties.testsFilter + + + // @Test def posTestFromTasty: Unit = { + // // Can be reproduced with + // // > sbt + // // > dotc -Ythrough-tasty -Ycheck:all + + // implicit val testGroup: TestGroup = TestGroup("posTestFromTasty") + // compileTastyInDir("tests/pos", defaultOptions, + // fromTastyFilter = FileFilter.exclude(TestSources.posFromTastyBlacklisted), + // decompilationFilter = FileFilter.exclude(TestSources.posDecompilationBlacklisted), + // recompilationFilter = FileFilter.include(TestSources.posRecompilationWhitelist) + // ).checkCompile() + // } + + @Test def compileGadtTests: Unit = { + implicit val testGroup: TestGroup = TestGroup("compileGadtTests") + compileFilesInDir("tests/gadt+noCheckOptions", TestFlags(basicClasspath, noCheckOptions)).checkCompile() + } + + @Test def compileGadtCheckOptionsTests: Unit = { + implicit val testGroup: TestGroup = TestGroup("compileGadtCheckOptionsTests") + compileFilesInDir("tests/gadt+checkOptions", TestFlags(basicClasspath, noCheckOptions ++ checkOptions)).checkCompile() + } + + @Test def compileGadtDefaultOptionsTests: Unit = { + implicit val testGroup: TestGroup = TestGroup("compileGadtDefaultOptionsTests") + compileFilesInDir("tests/gadt+defaultOptions", defaultOptions).checkCompile() + } +} + +object GadtTests { + implicit val summaryReport: SummaryReporting = new SummaryReport + @AfterClass def cleanup(): Unit = summaryReport.echoSummary() +} diff --git a/tests/gadt+checkOptions b/tests/gadt+checkOptions new file mode 120000 index 000000000000..7e0f18e54e9c --- /dev/null +++ b/tests/gadt+checkOptions @@ -0,0 +1 @@ +gadt \ No newline at end of file diff --git a/tests/gadt+defaultOptions b/tests/gadt+defaultOptions new file mode 120000 index 000000000000..7e0f18e54e9c --- /dev/null +++ b/tests/gadt+defaultOptions @@ -0,0 +1 @@ +gadt \ No newline at end of file diff --git a/tests/gadt+noCheckOptions b/tests/gadt+noCheckOptions new file mode 120000 index 000000000000..7e0f18e54e9c --- /dev/null +++ b/tests/gadt+noCheckOptions @@ -0,0 +1 @@ +gadt \ No newline at end of file diff --git a/tests/gadt/NatsVects.ignore b/tests/gadt/NatsVects.ignore new file mode 100644 index 000000000000..988661d1111b --- /dev/null +++ b/tests/gadt/NatsVects.ignore @@ -0,0 +1,90 @@ +object NatsVects { + sealed trait TNat + case class TZero() extends TNat + case class TSucc[N <: TNat] extends TNat + + object TNatSum { + sealed trait TSum[M, N, R] + case class TSumZero[N]() extends TSum[TZero, N, N] + case class TSumM[M <: TNat, N, R <: TNat](sum: TSum[M, N, R]) extends TSum[TSucc[M], N, TSucc[R]] + } + import TNatSum._ + + implicit def tSumZero[N]: TSum[TZero, N, N] = + TSumZero() + //new TSum[TZero, N, N]() {} + implicit def tSumM[M <: TNat, N, R <: TNat](implicit sum: TSum[M, N, R]): TSum[TSucc[M], N, TSucc[R]] = + TSumM(sum) + //new TSum[TSucc[M], N, TSucc[R]] {} + + sealed trait Vec[+T, N <: TNat] + case object VNil extends Vec[Nothing, TZero] // fails but in refchecks + case class VCons[T, N <: TNat](x: T, xs: Vec[T, N]) extends Vec[T, TSucc[N]] + + implicit class vecOps[T, M <: TNat]($this: Vec[T, M]) extends AnyVal { + def append[N <: TNat, R <: TNat](that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] = { + // tsum match { + // case _: TSumZero[N] => // Here N = R + // $this match { + // case VNil => + // //that + // that.asInstanceOf[Vec[T, R]] + // case VCons(x, xs) => + // ??? + // } + // case TSumM(sum) => + // ??? + // } + $this match { + case VNil => // M = TZero + tsum match { + case TSumZero() => that + //* case _: TSumZero[TZero] => + //* that + //* // that.asInstanceOf[Vec[T, R]] + case _: TSumM[_, _, _] => // Impossible, this forces M = TSucc[M1] + ??? + } + //* case vxs: VCons[T, m1] => // M = TSucc[m1], xs: Vec[T, m1] + //* val x = vxs.x + //* val xs = vxs.xs + //* //case VCons(x, xs) => + //* tsum match { + //* case _: TSumZero[TZero] => // impossible, since this forces M = TZero. + //* ??? + //* // fails + //* // case tsum1: TSumM[`m1`, n, r] => // M = TSucc[m1], R = TSucc[r] + //* // implicit val tsum2 = tsum1.sum + //* // val appended = xs append that + //* // VCons(x, appended) // Vec[T, TSucc[r]] + //* //works + //* case tsum1: TSumM[`m1`, N, r] => // M = TSucc[m1], R = TSucc[r] + //* implicit val tsum2 = tsum1.sum + //* // I should be able to return: + //* VCons(x, xs append that) // Vec[T, TSucc[r]] = Vec[T, R] + + //* // val vxs1 = xs append that + //* // val vxs2 = VCons(x, vxs1) + //* // vxs1 + //* // [error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/gadtVect.scala:65:14 + //* // [error] 65 | vxs1 + //* // [error] | ^^^^ + //* // [error] | found: NatsVects.Vec[T, r](vxs1) + //* // [error] | required: NatsVects.Vec[T, R] + //* // [error] | + //* // [error] | where: r is a type in method append with bounds <: NatsVects.TNat + //* // vxs2 + //* // [error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/gadtVect.scala:71:14 + //* // [error] 71 | vxs2 + //* // [error] | ^^^^ + //* // [error] | found: NatsVects.VCons[T, r](vxs2) + //* // [error] | required: NatsVects.Vec[T, R] + //* // [error] | + //* // [error] | where: r is a type in method append with bounds <: NatsVects.TNat + + //* // vxs2.asInstanceOf // sorry this works + //* } + } + } + } +} diff --git a/tests/gadt/banal.scala b/tests/gadt/banal.scala new file mode 100644 index 000000000000..a0efb73412fa --- /dev/null +++ b/tests/gadt/banal.scala @@ -0,0 +1,15 @@ +object banal { + sealed trait T[A] + final case class StrLit(v: String) extends T[String] + final case class IntLit(v: Int) extends T[Int] + + def eval[A](t: T[A]): A = t match { + case StrLit(v) => v + case IntLit(v) => v + } + + def evul[A](t: T[A]): A = t match { + case StrLit(_) => "" + case IntLit(_) => 0 + } +} diff --git a/tests/gadt/foo.scala b/tests/gadt/foo.scala new file mode 100644 index 000000000000..4966ce2cf3a5 --- /dev/null +++ b/tests/gadt/foo.scala @@ -0,0 +1,11 @@ +object foo { + sealed trait Exp[T] + case class Var[T](name: String) extends Exp[T] + + def env[T](x: Var[T]): T = ??? + + def eval[S](e: Exp[S]) = e match { + case v: Var[foo] => + env(v) + } +} diff --git a/tests/gadt/injectivity.scala b/tests/gadt/injectivity.scala new file mode 100644 index 000000000000..bd04d89ee025 --- /dev/null +++ b/tests/gadt/injectivity.scala @@ -0,0 +1,9 @@ +object injectivity { + sealed trait EQ[A, B] + final case class Refl[A](u: Unit) extends EQ[A, A] + + def conform[A, B, C, D](a: A, b: B, eq: EQ[(A, B), (C, D)]): C = + eq match { + case Refl(()) => a + } +} diff --git a/tests/gadt/one.scala b/tests/gadt/one.scala new file mode 100644 index 000000000000..b46d864166fc --- /dev/null +++ b/tests/gadt/one.scala @@ -0,0 +1,9 @@ +object one { + case class One[T](fst: T) + def bad[T](e: One[T]) = e match { + case foo: One[a] => + val t: T = e.fst + // val nok: Nothing = t // should not compile + val ok: a = t // does compile + } +} diff --git a/tests/gadt/simpleEQ.scala b/tests/gadt/simpleEQ.scala new file mode 100644 index 000000000000..03b5c0b27e6b --- /dev/null +++ b/tests/gadt/simpleEQ.scala @@ -0,0 +1,13 @@ +object simpleEQ { + sealed trait EQ[A, B] + final case class Refl[A](u: Unit) extends EQ[A, A] + + def conform[A, B](a: A, eq: EQ[A, B]): B = eq match { + case Refl(()) => a + } + + def conform2[A, B, C, D](a: A, b: B, eq: EQ[(A, B), (C, D)]): (C, D) = + eq match { + case Refl(()) => (a, b) + } +} From cfc0d5bea84a3567cc8aacf408c25b8856d56298 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Mon, 8 Oct 2018 14:59:17 +0200 Subject: [PATCH 03/21] TVar based implementation --- .../tools/dotc/core/ConstraintHandling.scala | 9 +- .../src/dotty/tools/dotc/core/Contexts.scala | 90 +++++++++++++++++-- .../dotty/tools/dotc/core/TypeComparer.scala | 7 +- .../src/dotty/tools/dotc/core/Types.scala | 2 +- .../tools/dotc/printing/Formatting.scala | 4 +- .../src/dotty/tools/dotc/typer/Typer.scala | 2 +- 6 files changed, 95 insertions(+), 19 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index aff9883cf294..1cfc50704ab8 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -20,13 +20,14 @@ import config.Printers.{constr, typr} */ trait ConstraintHandling { - implicit val ctx: Context + implicit def ctx: Context protected def isSubType(tp1: Type, tp2: Type): Boolean protected def isSameType(tp1: Type, tp2: Type): Boolean - val state: TyperState - import state.constraint + // val state: TyperState + protected def constraint: Constraint + protected def constraint_=(c: Constraint): Unit private[this] var addConstraintInvocations = 0 @@ -98,7 +99,7 @@ trait ConstraintHandling { } } - private def location(implicit ctx: Context) = "" // i"in ${ctx.typerState.stateChainStr}" // use for debugging + private def location(implicit ctx: Context) = i"in ${ctx.typerState.stateChainStr}" // use for debugging protected def addUpperBound(param: TypeParamRef, bound: Type): Boolean = { def description = i"constraint $param <: $bound to\n$constraint" diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 7ea68b0ae816..83e52240664b 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -480,7 +480,7 @@ object Contexts { def setTyper(typer: Typer): this.type = { this.scope = typer.scope; setTypeAssigner(typer) } def setImportInfo(importInfo: ImportInfo): this.type = { this.importInfo = importInfo; this } def setGadt(gadt: GADTMap): this.type = { this.gadt = gadt; this } - def setFreshGADTBounds: this.type = setGadt(new GADTMap(gadt.bounds)) + def setFreshGADTBounds: this.type = setGadt(gadt.derived) def setSearchHistory(searchHistory: SearchHistory): this.type = { this.searchHistory = searchHistory; this } def setTypeComparerFn(tcfn: Context => TypeComparer): this.type = { this.typeComparer = tcfn(this); this } private def setMoreProperties(moreProperties: Map[Key[Any], Any]): this.type = { this.moreProperties = moreProperties; this } @@ -708,14 +708,88 @@ object Contexts { else assert(thread == Thread.currentThread(), "illegal multithreaded access to ContextBase") } - class GADTMap(initBounds: SimpleIdentityMap[Symbol, TypeBounds]) { - private[this] var myBounds = initBounds - def setBounds(sym: Symbol, b: TypeBounds): Unit = - myBounds = myBounds.updated(sym, b) - def bounds: SimpleIdentityMap[Symbol, TypeBounds] = myBounds + sealed abstract class GADTMap { + def setBounds(sym: Symbol, b: TypeBounds)(implicit ctx: Context): Unit + def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds + def contains(sym: Symbol)(implicit ctx: Context): Boolean + def derived: GADTMap } - @sharable object EmptyGADTMap extends GADTMap(SimpleIdentityMap.Empty) { - override def setBounds(sym: Symbol, b: TypeBounds): Unit = unsupported("EmptyGADTMap.setBounds") + class SmartGADTMap( + private[this] var myConstraint: Constraint = new OrderingConstraint(SimpleIdentityMap.Empty, SimpleIdentityMap.Empty, SimpleIdentityMap.Empty), + private[this] var mapping: SimpleIdentityMap[Symbol, TypeVar] = SimpleIdentityMap.Empty + ) extends GADTMap with ConstraintHandling { + def log(str: String): Unit = { + import dotty.tools.dotc.config.Printers.gadts + gadts.println(s"GADTMap: $str") + } + + // TODO: dirty kludge - should this class be an inner class of TyperState instead? + private[this] var myCtx: Context = null + implicit override def ctx = myCtx + @forceInline private[this] final def inCtx[T](_ctx: Context)(op: => T) = { + val savedCtx = myCtx + myCtx = _ctx + try op finally myCtx = savedCtx + } + + override protected def constraint = myConstraint + override protected def constraint_=(c: Constraint) = myConstraint = c + + override def isSubType(tp1: Type, tp2: Type): Boolean = ctx.typeComparer.isSubType(tp1, tp2) + override def isSameType(tp1: Type, tp2: Type): Boolean = ctx.typeComparer.isSameType(tp1, tp2) + + private[this] def tvar(sym: Symbol)(implicit ctx: Context) = inCtx(ctx) { + val res = mapping(sym) match { + case tv: TypeVar => tv + case null => + log(i"creating tvar for: $sym") + val res = { + import NameKinds.DepParamName + // do not use newTypeVar: + // it registers the TypeVar with TyperState, we don't want that since it instantiates them (TODO: when?) + // (see pos/i3500.scala) + // it registers the TypeVar with TyperState Constraint, which we don't care for but it's needless + val poly = PolyType(DepParamName.fresh().toTypeName :: Nil)( + pt => TypeBounds.empty :: Nil, + pt => defn.AnyType) + // null out creatorState, we don't need it anyway (and TypeVar can null it too) + new TypeVar(poly.paramRefs.head, creatorState = null) + } + constraint = constraint.add(res.origin.binder, res :: Nil) + mapping = mapping.updated(sym, res) + res + } + log(i"tvar: $sym -> $res") + res + } + + override def setBounds(sym: Symbol, b: TypeBounds)(implicit ctx: Context): Unit = inCtx(ctx) { + val tv = tvar(sym) + log(i"setBounds `$sym` `$tv`: `$b`") + addUpperBound(tv.origin, b.hi) + addLowerBound(tv.origin, b.lo) + } + + override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = inCtx(ctx) { + mapping(sym) match { + case null => null + case tv => constraint.fullBounds(tv.origin) + } + } + + override def contains(sym: Symbol)(implicit ctx: Context) = mapping(sym) ne null + + override def derived: GADTMap = new SmartGADTMap( + this.myConstraint, + this.mapping + ) + } + + @sharable object EmptyGADTMap extends GADTMap { + override def setBounds(sym: Symbol, b: TypeBounds)(implicit ctx: Context) = unsupported("EmptyGADTMap.setBounds") + override def bounds(sym: Symbol)(implicit ctx: Context) = null + override def contains(sym: Symbol)(implicit ctx: Context) = false + override def derived = new SmartGADTMap } } diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index e3fa098586ac..a73cb5574db9 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -23,8 +23,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { import TypeComparer._ implicit val ctx: Context = initctx - val state: TyperState = ctx.typerState - import state.constraint + val state = ctx.typerState + def constraint: Constraint = state.constraint + def constraint_=(c: Constraint): Unit = state.constraint = c private[this] var pendingSubTypes: mutable.Set[(Type, Type)] = null private[this] var recCount = 0 @@ -136,7 +137,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { finally this.approx = saved } - protected def isSubType(tp1: Type, tp2: Type): Boolean = isSubType(tp1, tp2, NoApprox) + def isSubType(tp1: Type, tp2: Type): Boolean = isSubType(tp1, tp2, NoApprox) protected def recur(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)} $approx", subtyping) { diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 183b1e7aa294..bb0ba6c3e49f 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -3729,7 +3729,7 @@ object Types { def isBounded(tp: Type) = tp match { case tp: TypeParamRef => - case tp: TypeRef => ctx.gadt.bounds.contains(tp.symbol) + case tp: TypeRef => ctx.gadt.contains(tp.symbol) } def contextInfo(tp: Type): Type = tp match { diff --git a/compiler/src/dotty/tools/dotc/printing/Formatting.scala b/compiler/src/dotty/tools/dotc/printing/Formatting.scala index 1c4d9c3e1283..24c13791524b 100644 --- a/compiler/src/dotty/tools/dotc/printing/Formatting.scala +++ b/compiler/src/dotty/tools/dotc/printing/Formatting.scala @@ -168,7 +168,7 @@ object Formatting { s"is a reference to a value parameter" case sym: Symbol => val info = - if (ctx.gadt.bounds.contains(sym)) + if (ctx.gadt.contains(sym)) sym.info & ctx.gadt.bounds(sym) else sym.info @@ -189,7 +189,7 @@ object Formatting { case param: TermParamRef => false case skolem: SkolemType => true case sym: Symbol => - ctx.gadt.bounds.contains(sym) && ctx.gadt.bounds(sym) != TypeBounds.empty + ctx.gadt.contains(sym) && ctx.gadt.bounds(sym) != TypeBounds.empty case _ => assert(false, "unreachable") false diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index dca8c7137111..cf9971129af4 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -1023,7 +1023,7 @@ class Typer extends Namer def gadtContext(gadtSyms: Set[Symbol])(implicit ctx: Context): Context = { val gadtCtx = ctx.fresh.setFreshGADTBounds for (sym <- gadtSyms) - if (!gadtCtx.gadt.bounds.contains(sym)) + if (!gadtCtx.gadt.contains(sym)) gadtCtx.gadt.setBounds(sym, TypeBounds.empty) gadtCtx } From ea566c511b85dec78dca02ff7a8750f67cbe034a Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Wed, 24 Oct 2018 13:35:26 +0200 Subject: [PATCH 04/21] Substitute TypeParams on RHS with TypeVars Turns out this is quite important for correctness. Tests now pass with -Y-no-deep-subtypes, so GadtTests was simplified accordingly. GADTMap.setBound accepts a single type bound instead of TypeBounds to simplify the implementation. NatsVects tests was rewritten, as class parameters are known to not work with GADTs. --- .../tools/dotc/core/ConstraintHandling.scala | 3 +- .../src/dotty/tools/dotc/core/Contexts.scala | 115 ++++++++++++++---- .../src/dotty/tools/dotc/core/Symbols.scala | 6 +- .../dotty/tools/dotc/core/TypeComparer.scala | 18 ++- .../src/dotty/tools/dotc/typer/Inliner.scala | 6 +- .../src/dotty/tools/dotc/typer/Typer.scala | 10 +- .../test/dotty/tools/dotc/GadtTests.scala | 26 +--- tests/gadt+checkOptions | 1 - tests/gadt+defaultOptions | 1 - tests/gadt+noCheckOptions | 1 - tests/gadt/NatsVects.ignore | 90 -------------- tests/gadt/TailCalls.scala | 39 ++++++ tests/gadt/i3666.scala | 65 ++++++++++ tests/gadt/i4176.scala | 36 ++++++ tests/gadt/i5068.scala | 11 ++ 15 files changed, 271 insertions(+), 157 deletions(-) delete mode 120000 tests/gadt+checkOptions delete mode 120000 tests/gadt+defaultOptions delete mode 120000 tests/gadt+noCheckOptions delete mode 100644 tests/gadt/NatsVects.ignore create mode 100644 tests/gadt/TailCalls.scala create mode 100644 tests/gadt/i3666.scala create mode 100644 tests/gadt/i4176.scala create mode 100644 tests/gadt/i5068.scala diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 1cfc50704ab8..a587a43a5e14 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -25,7 +25,6 @@ trait ConstraintHandling { protected def isSubType(tp1: Type, tp2: Type): Boolean protected def isSameType(tp1: Type, tp2: Type): Boolean - // val state: TyperState protected def constraint: Constraint protected def constraint_=(c: Constraint): Unit @@ -99,7 +98,7 @@ trait ConstraintHandling { } } - private def location(implicit ctx: Context) = i"in ${ctx.typerState.stateChainStr}" // use for debugging + private def location(implicit ctx: Context) = "" // i"in ${ctx.typerState.stateChainStr}" // use for debugging protected def addUpperBound(param: TypeParamRef, bound: Type): Boolean = { def description = i"constraint $param <: $bound to\n$constraint" diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 83e52240664b..cc4fd4586bc9 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -709,20 +709,19 @@ object Contexts { } sealed abstract class GADTMap { - def setBounds(sym: Symbol, b: TypeBounds)(implicit ctx: Context): Unit + def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit + def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds def contains(sym: Symbol)(implicit ctx: Context): Boolean def derived: GADTMap } - class SmartGADTMap( + final class SmartGADTMap( private[this] var myConstraint: Constraint = new OrderingConstraint(SimpleIdentityMap.Empty, SimpleIdentityMap.Empty, SimpleIdentityMap.Empty), - private[this] var mapping: SimpleIdentityMap[Symbol, TypeVar] = SimpleIdentityMap.Empty + private[this] var mapping: SimpleIdentityMap[Symbol, TypeVar] = SimpleIdentityMap.Empty, + private[this] var reverseMapping: SimpleIdentityMap[TypeVar, Symbol] = SimpleIdentityMap.Empty ) extends GADTMap with ConstraintHandling { - def log(str: String): Unit = { - import dotty.tools.dotc.config.Printers.gadts - gadts.println(s"GADTMap: $str") - } + import dotty.tools.dotc.config.Printers.gadts // TODO: dirty kludge - should this class be an inner class of TyperState instead? private[this] var myCtx: Context = null @@ -739,56 +738,120 @@ object Contexts { override def isSubType(tp1: Type, tp2: Type): Boolean = ctx.typeComparer.isSubType(tp1, tp2) override def isSameType(tp1: Type, tp2: Type): Boolean = ctx.typeComparer.isSameType(tp1, tp2) - private[this] def tvar(sym: Symbol)(implicit ctx: Context) = inCtx(ctx) { + private[this] def tvar(sym: Symbol)(implicit ctx: Context): TypeVar = inCtx(ctx) { val res = mapping(sym) match { case tv: TypeVar => tv case null => - log(i"creating tvar for: $sym") val res = { import NameKinds.DepParamName - // do not use newTypeVar: - // it registers the TypeVar with TyperState, we don't want that since it instantiates them (TODO: when?) - // (see pos/i3500.scala) - // it registers the TypeVar with TyperState Constraint, which we don't care for but it's needless - val poly = PolyType(DepParamName.fresh().toTypeName :: Nil)( + // avoid registering the TypeVar with TyperState / TyperState#constraint + // TyperState TypeVars get instantiated when we don't want them to (see pos/i3500.scala) + // TyperState#constraint TypeVars can be narrowed in subtype checks - don't want that either + val poly = PolyType(DepParamName.fresh(sym.name.toTypeName) :: Nil)( pt => TypeBounds.empty :: Nil, pt => defn.AnyType) - // null out creatorState, we don't need it anyway (and TypeVar can null it too) + // null out creatorState as a precaution new TypeVar(poly.paramRefs.head, creatorState = null) } + gadts.println(i"GADTMap: created tvar $sym -> $res") constraint = constraint.add(res.origin.binder, res :: Nil) mapping = mapping.updated(sym, res) + reverseMapping = reverseMapping.updated(res, sym) res } - log(i"tvar: $sym -> $res") res } - override def setBounds(sym: Symbol, b: TypeBounds)(implicit ctx: Context): Unit = inCtx(ctx) { - val tv = tvar(sym) - log(i"setBounds `$sym` `$tv`: `$b`") - addUpperBound(tv.origin, b.hi) - addLowerBound(tv.origin, b.lo) + override def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit = tvar(sym) + + override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = inCtx(ctx) { + def isEmptyBounds(tp: Type) = tp match { + case TypeBounds(lo, hi) => (lo eq defn.NothingType) && (hi eq defn.AnyType) + case _ => false + } + + val symTvar = tvar(sym) + + def doAddOrdering(bound: TypeParamRef) = + if (isUpper) addLess(symTvar.origin, bound) else addLess(bound, symTvar.origin) + + def doAddBound(bound: Type) = + if (isUpper) addUpperBound(symTvar.origin, bound) else addLowerBound(symTvar.origin, bound) + + val tvarBound = (new TypeVarInsertingMap)(bound) + val res = tvarBound match { + case boundTvar: TypeVar => + if (boundTvar eq symTvar) true else doAddOrdering(boundTvar.origin) + // hack to normalize T and T[_] + case AppliedType(boundTvar: TypeVar, args) if args forall isEmptyBounds => + doAddOrdering(boundTvar.origin) + case tp => doAddBound(tp) + } + + gadts.println { + val descr = if (isUpper) "upper" else "lower" + val op = if (isUpper) "<:" else ">:" + i"adding $descr bound $sym $op $bound = $res\t( $symTvar $op $tvarBound )" + } + res } override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = inCtx(ctx) { mapping(sym) match { case null => null - case tv => constraint.fullBounds(tv.origin) + case tv => + val tb = constraint.fullBounds(tv.origin) + val res = { + val tm = new TypeVarRemovingMap + tb.derivedTypeBounds(tm(tb.lo), tm(tb.hi)) + } + gadts.println(i"gadt bounds $sym: $res\t( $tv: $tb )") + res } } - override def contains(sym: Symbol)(implicit ctx: Context) = mapping(sym) ne null + override def contains(sym: Symbol)(implicit ctx: Context): Boolean = mapping(sym) ne null override def derived: GADTMap = new SmartGADTMap( this.myConstraint, - this.mapping + this.mapping, + this.reverseMapping ) + + private final class TypeVarInsertingMap extends TypeMap { + override def apply(tp: Type): Type = tp match { + case tp: TypeRef => + val sym = tp.typeSymbol + if (contains(sym)) tvar(sym) else tp + case _ => + mapOver(tp) + } + } + + private final class TypeVarRemovingMap extends TypeMap { + override def apply(tp: Type): Type = tp match { + case tpr: TypeParamRef => + constraint.typeVarOfParam(tpr) match { + case tv: TypeVar => + reverseMapping(tv).typeRef + case unexpected => + // if we didn't get a TypeVar, it's likely to cause problems + gadts.println(i"GADTMap: unexpected typeVarOfParam($tpr) = `$unexpected` ${unexpected.getClass}") + tpr + } + case tv: TypeVar => + if (reverseMapping.contains(tv)) reverseMapping(tv).typeRef + else tv + case _ => + mapOver(tp) + } + } } @sharable object EmptyGADTMap extends GADTMap { - override def setBounds(sym: Symbol, b: TypeBounds)(implicit ctx: Context) = unsupported("EmptyGADTMap.setBounds") - override def bounds(sym: Symbol)(implicit ctx: Context) = null + override def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit = unsupported("EmptyGADTMap.addEmptyBounds") + override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = unsupported("EmptyGADTMap.addBound") + override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = null override def contains(sym: Symbol)(implicit ctx: Context) = false override def derived = new SmartGADTMap } diff --git a/compiler/src/dotty/tools/dotc/core/Symbols.scala b/compiler/src/dotty/tools/dotc/core/Symbols.scala index d6b6ed1efd1c..864407e51897 100644 --- a/compiler/src/dotty/tools/dotc/core/Symbols.scala +++ b/compiler/src/dotty/tools/dotc/core/Symbols.scala @@ -214,7 +214,11 @@ trait Symbols { this: Context => */ def newPatternBoundSymbol(name: Name, info: Type, pos: Position): Symbol = { val sym = newSymbol(owner, name, Case, info, coord = pos) - if (name.isTypeName) gadt.setBounds(sym, info.bounds) + if (name.isTypeName) { + val bounds = info.bounds + gadt.addBound(sym, bounds.lo, isUpper = false) + gadt.addBound(sym, bounds.hi, isUpper = true) + } sym } diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index a73cb5574db9..7876b9e7645c 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -106,8 +106,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { true } - protected def gadtBounds(sym: Symbol)(implicit ctx: Context): TypeBounds = ctx.gadt.bounds(sym) - protected def gadtSetBounds(sym: Symbol, b: TypeBounds): Unit = ctx.gadt.setBounds(sym, b) + protected def gadtBounds(sym: Symbol)(implicit ctx: Context) = ctx.gadt.bounds(sym) + protected def gadtAddLowerBound(sym: Symbol, b: Type): Boolean = ctx.gadt.addBound(sym, b, isUpper = false) + protected def gadtAddUpperBound(sym: Symbol, b: Type): Boolean = ctx.gadt.addBound(sym, b, isUpper = true) protected def typeVarInstance(tvar: TypeVar)(implicit ctx: Context): Type = tvar.underlying @@ -1217,8 +1218,10 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { val newBounds = if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound) else TypeBounds(oldBounds.lo | bound, oldBounds.hi) + // gadtMap can check its own satisfiability, but the subtype check is still necessary + // see tests/patmat/gadt-nontrivial2.scala isSubType(newBounds.lo, newBounds.hi) && - { gadtSetBounds(tparam, newBounds); true } + (if (isUpper) gadtAddUpperBound(tparam, bound) else gadtAddLowerBound(tparam, bound)) } } } @@ -1826,9 +1829,14 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { super.gadtBounds(sym) } - override def gadtSetBounds(sym: Symbol, b: TypeBounds): Unit = { + override def gadtAddLowerBound(sym: Symbol, b: Type): Boolean = { footprint += sym.typeRef - super.gadtSetBounds(sym, b) + super.gadtAddLowerBound(sym, b) + } + + override def gadtAddUpperBound(sym: Symbol, b: Type): Boolean = { + footprint += sym.typeRef + super.gadtAddUpperBound(sym, b) } override def typeVarInstance(tvar: TypeVar)(implicit ctx: Context): Type = { diff --git a/compiler/src/dotty/tools/dotc/typer/Inliner.scala b/compiler/src/dotty/tools/dotc/typer/Inliner.scala index 5b1c9fe47ec4..0b3b29b48fca 100644 --- a/compiler/src/dotty/tools/dotc/typer/Inliner.scala +++ b/compiler/src/dotty/tools/dotc/typer/Inliner.scala @@ -730,7 +730,11 @@ class Inliner(call: tpd.Tree, rhsToInline: tpd.Tree)(implicit ctx: Context) { for (tpt <- tpts) boundVars = getBoundVars(boundVars, tpt) case _ => } - for (bv <- boundVars) ctx.gadt.setBounds(bv, bv.info.bounds) + for (bv <- boundVars) { + val TypeBounds(lo, hi) = bv.info.bounds + ctx.gadt.addBound(bv, lo, isUpper = false) + ctx.gadt.addBound(bv, hi, isUpper = true) + } scrut <:< tpt.tpe && { for (bv <- boundVars) { bv.info = TypeAlias(ctx.gadt.bounds(bv).lo) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index cf9971129af4..262f1ac03917 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -1023,8 +1023,7 @@ class Typer extends Namer def gadtContext(gadtSyms: Set[Symbol])(implicit ctx: Context): Context = { val gadtCtx = ctx.fresh.setFreshGADTBounds for (sym <- gadtSyms) - if (!gadtCtx.gadt.contains(sym)) - gadtCtx.gadt.setBounds(sym, TypeBounds.empty) + if (!gadtCtx.gadt.contains(sym)) gadtCtx.gadt.addEmptyBounds(sym) gadtCtx } @@ -1502,8 +1501,11 @@ class Typer extends Namer // that their type parameters are aliases of the class type parameters. // See pos/i941.scala rhsCtx = ctx.fresh.setFreshGADTBounds - (tparams1, sym.owner.typeParams).zipped.foreach ((tdef, tparam) => - rhsCtx.gadt.setBounds(tdef.symbol, TypeAlias(tparam.typeRef))) + (tparams1, sym.owner.typeParams).zipped.foreach { (tdef, tparam) => + val tr = tparam.typeRef + rhsCtx.gadt.addBound(tdef.symbol, tr, isUpper = false) + rhsCtx.gadt.addBound(tdef.symbol, tr, isUpper = true) + } } if (sym.isInlineMethod) rhsCtx = rhsCtx.addMode(Mode.InlineableBody) val rhs1 = typedExpr(ddef.rhs, tpt1.tpe)(rhsCtx) diff --git a/compiler/test/dotty/tools/dotc/GadtTests.scala b/compiler/test/dotty/tools/dotc/GadtTests.scala index 48791a2c68cd..cf557a65f830 100644 --- a/compiler/test/dotty/tools/dotc/GadtTests.scala +++ b/compiler/test/dotty/tools/dotc/GadtTests.scala @@ -20,33 +20,9 @@ class GadtTests extends ParallelTesting { def isInteractive = SummaryReport.isInteractive def testFilter = Properties.testsFilter - - // @Test def posTestFromTasty: Unit = { - // // Can be reproduced with - // // > sbt - // // > dotc -Ythrough-tasty -Ycheck:all - - // implicit val testGroup: TestGroup = TestGroup("posTestFromTasty") - // compileTastyInDir("tests/pos", defaultOptions, - // fromTastyFilter = FileFilter.exclude(TestSources.posFromTastyBlacklisted), - // decompilationFilter = FileFilter.exclude(TestSources.posDecompilationBlacklisted), - // recompilationFilter = FileFilter.include(TestSources.posRecompilationWhitelist) - // ).checkCompile() - // } - @Test def compileGadtTests: Unit = { implicit val testGroup: TestGroup = TestGroup("compileGadtTests") - compileFilesInDir("tests/gadt+noCheckOptions", TestFlags(basicClasspath, noCheckOptions)).checkCompile() - } - - @Test def compileGadtCheckOptionsTests: Unit = { - implicit val testGroup: TestGroup = TestGroup("compileGadtCheckOptionsTests") - compileFilesInDir("tests/gadt+checkOptions", TestFlags(basicClasspath, noCheckOptions ++ checkOptions)).checkCompile() - } - - @Test def compileGadtDefaultOptionsTests: Unit = { - implicit val testGroup: TestGroup = TestGroup("compileGadtDefaultOptionsTests") - compileFilesInDir("tests/gadt+defaultOptions", defaultOptions).checkCompile() + compileFilesInDir("tests/gadt", defaultOptions).checkCompile() } } diff --git a/tests/gadt+checkOptions b/tests/gadt+checkOptions deleted file mode 120000 index 7e0f18e54e9c..000000000000 --- a/tests/gadt+checkOptions +++ /dev/null @@ -1 +0,0 @@ -gadt \ No newline at end of file diff --git a/tests/gadt+defaultOptions b/tests/gadt+defaultOptions deleted file mode 120000 index 7e0f18e54e9c..000000000000 --- a/tests/gadt+defaultOptions +++ /dev/null @@ -1 +0,0 @@ -gadt \ No newline at end of file diff --git a/tests/gadt+noCheckOptions b/tests/gadt+noCheckOptions deleted file mode 120000 index 7e0f18e54e9c..000000000000 --- a/tests/gadt+noCheckOptions +++ /dev/null @@ -1 +0,0 @@ -gadt \ No newline at end of file diff --git a/tests/gadt/NatsVects.ignore b/tests/gadt/NatsVects.ignore deleted file mode 100644 index 988661d1111b..000000000000 --- a/tests/gadt/NatsVects.ignore +++ /dev/null @@ -1,90 +0,0 @@ -object NatsVects { - sealed trait TNat - case class TZero() extends TNat - case class TSucc[N <: TNat] extends TNat - - object TNatSum { - sealed trait TSum[M, N, R] - case class TSumZero[N]() extends TSum[TZero, N, N] - case class TSumM[M <: TNat, N, R <: TNat](sum: TSum[M, N, R]) extends TSum[TSucc[M], N, TSucc[R]] - } - import TNatSum._ - - implicit def tSumZero[N]: TSum[TZero, N, N] = - TSumZero() - //new TSum[TZero, N, N]() {} - implicit def tSumM[M <: TNat, N, R <: TNat](implicit sum: TSum[M, N, R]): TSum[TSucc[M], N, TSucc[R]] = - TSumM(sum) - //new TSum[TSucc[M], N, TSucc[R]] {} - - sealed trait Vec[+T, N <: TNat] - case object VNil extends Vec[Nothing, TZero] // fails but in refchecks - case class VCons[T, N <: TNat](x: T, xs: Vec[T, N]) extends Vec[T, TSucc[N]] - - implicit class vecOps[T, M <: TNat]($this: Vec[T, M]) extends AnyVal { - def append[N <: TNat, R <: TNat](that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] = { - // tsum match { - // case _: TSumZero[N] => // Here N = R - // $this match { - // case VNil => - // //that - // that.asInstanceOf[Vec[T, R]] - // case VCons(x, xs) => - // ??? - // } - // case TSumM(sum) => - // ??? - // } - $this match { - case VNil => // M = TZero - tsum match { - case TSumZero() => that - //* case _: TSumZero[TZero] => - //* that - //* // that.asInstanceOf[Vec[T, R]] - case _: TSumM[_, _, _] => // Impossible, this forces M = TSucc[M1] - ??? - } - //* case vxs: VCons[T, m1] => // M = TSucc[m1], xs: Vec[T, m1] - //* val x = vxs.x - //* val xs = vxs.xs - //* //case VCons(x, xs) => - //* tsum match { - //* case _: TSumZero[TZero] => // impossible, since this forces M = TZero. - //* ??? - //* // fails - //* // case tsum1: TSumM[`m1`, n, r] => // M = TSucc[m1], R = TSucc[r] - //* // implicit val tsum2 = tsum1.sum - //* // val appended = xs append that - //* // VCons(x, appended) // Vec[T, TSucc[r]] - //* //works - //* case tsum1: TSumM[`m1`, N, r] => // M = TSucc[m1], R = TSucc[r] - //* implicit val tsum2 = tsum1.sum - //* // I should be able to return: - //* VCons(x, xs append that) // Vec[T, TSucc[r]] = Vec[T, R] - - //* // val vxs1 = xs append that - //* // val vxs2 = VCons(x, vxs1) - //* // vxs1 - //* // [error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/gadtVect.scala:65:14 - //* // [error] 65 | vxs1 - //* // [error] | ^^^^ - //* // [error] | found: NatsVects.Vec[T, r](vxs1) - //* // [error] | required: NatsVects.Vec[T, R] - //* // [error] | - //* // [error] | where: r is a type in method append with bounds <: NatsVects.TNat - //* // vxs2 - //* // [error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/gadtVect.scala:71:14 - //* // [error] 71 | vxs2 - //* // [error] | ^^^^ - //* // [error] | found: NatsVects.VCons[T, r](vxs2) - //* // [error] | required: NatsVects.Vec[T, R] - //* // [error] | - //* // [error] | where: r is a type in method append with bounds <: NatsVects.TNat - - //* // vxs2.asInstanceOf // sorry this works - //* } - } - } - } -} diff --git a/tests/gadt/TailCalls.scala b/tests/gadt/TailCalls.scala new file mode 100644 index 000000000000..8899216068ae --- /dev/null +++ b/tests/gadt/TailCalls.scala @@ -0,0 +1,39 @@ +// package scala.util.control +object TailCalls { + + abstract class TailRec[+A] { + + final def flatMap[B](f: A => TailRec[B]): TailRec[B] = + this match { + case Done(a) => Call(() => f(a)) + case c@Call(_) => Cont(c, f) + case c: Cont[a1, b1] => Cont(c.a, (x: a1) => c.f(x) flatMap f) + } + + @annotation.tailrec final def resume: Either[() => TailRec[A], A] = this match { + case Done(a) => Right(a) + case Call(k) => Left(k) + case Cont(a, f) => a match { + case Done(v) => f(v).resume + case Call(k) => Left(() => k().flatMap(f)) + case Cont(b, g) => b.flatMap(x => g(x) flatMap f).resume + } + } + + @annotation.tailrec final def result: A = this match { + case Done(a) => a + case Call(t) => t().result + case Cont(a, f) => a match { + case Done(v) => f(v).result + case Call(t) => t().flatMap(f).result + case Cont(b, g) => b.flatMap(x => g(x) flatMap f).result + } + } + } + + protected case class Call[A](rest: () => TailRec[A]) extends TailRec[A] + + protected case class Done[A](value: A) extends TailRec[A] + + protected case class Cont[A, B](a: TailRec[A], f: A => TailRec[B]) extends TailRec[B] +} diff --git a/tests/gadt/i3666.scala b/tests/gadt/i3666.scala new file mode 100644 index 000000000000..16614e9e949e --- /dev/null +++ b/tests/gadt/i3666.scala @@ -0,0 +1,65 @@ +object i3666 { + sealed trait Exp[T] + case class Num(n: Int) extends Exp[Int] + case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int] + case class Var[T](name: String) extends Exp[T] + case class Lambda[T, U](x: Var[T], e: Exp[U]) extends Exp[T => U] + case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U] + + abstract class Env { outer => + def apply[T](x: Var[T]): T + + def + [T](xe: (Var[T], T)) = new Env { + def apply[T](x: Var[T]): T = + if (x == xe._1) xe._2.asInstanceOf[T] + else outer(x) + } + } + + object Env { + val empty = new Env { + def apply[T](x: Var[T]): T = ??? + } + } + + object Test { + + val exp = App(Lambda(Var[Int]("x"), Plus(Var[Int]("x"), Num(1))), Var[Int]("2")) + + def eval[T](e: Exp[T])(env: Env): T = e match { + case Num(n) => n + case Plus(e1, e2) => eval(e1)(env) + eval(e2)(env) + case v: Var[_] => env(v) + case Lambda(x: Var[s], e) => ((y: s) => eval(e)(env + (x -> y))) + case App(f, e) => eval(f)(env)(eval(e)(env)) + } + + eval(exp)(Env.empty) + } +} +// A HOAS well-typed interpreter +object i3666Hoas { + sealed trait Exp[T] + case class IntLit(n: Int) extends Exp[Int] + case class BooleanLit(b: Boolean) extends Exp[Boolean] + + case class GenLit[T](t: T) extends Exp[T] + case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int] + case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T] + case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U] + + + def eval[T](e: Exp[T]): T = e match { + case IntLit(n) => n + case BooleanLit(b) => b + case GenLit(t) => t + case Plus(e1, e2) => eval(e1) + eval(e2) + case f: Fun[s, t] => + (v: s) => eval(f.f(GenLit(v))) + case App(f, e) => eval(f)(eval(e)) + } + + val exp = App(Fun[S = Int](x => Plus(x, IntLit(1))), IntLit(2)) + + eval(exp) +} diff --git a/tests/gadt/i4176.scala b/tests/gadt/i4176.scala new file mode 100644 index 000000000000..5c7efa6993c9 --- /dev/null +++ b/tests/gadt/i4176.scala @@ -0,0 +1,36 @@ +object i4176 { + sealed trait TNat + case class TZero() extends TNat + case class TSucc[N <: TNat] extends TNat + + object TNatSum { + sealed trait TSum[M, N, R] + case class TSumZero[N]() extends TSum[TZero, N, N] + case class TSumM[M <: TNat, N, R <: TNat](sum: TSum[M, N, R]) extends TSum[TSucc[M], N, TSucc[R]] + } + import TNatSum._ + + implicit def tSumZero[N]: TSum[TZero, N, N] = + TSumZero() + implicit def tSumM[M <: TNat, N, R <: TNat](implicit sum: TSum[M, N, R]): TSum[TSucc[M], N, TSucc[R]] = + TSumM(sum) + + sealed trait Vec[T, N <: TNat] + case object VNil extends Vec[Nothing, TZero] // fails but in refchecks + case class VCons[T, N <: TNat](x: T, xs: Vec[T, N]) extends Vec[T, TSucc[N]] + + def append0[T, M <: TNat, N <: TNat, R <: TNat]($this: Vec[T, M], that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] = + ($this, tsum) match { + case (VNil, TSumZero()) => that + case (VCons(x, xs), TSumM(sum)) => VCons(x, append0(xs, that)(sum)) + } + + def append[T, M <: TNat, N <: TNat, R <: TNat]($this: Vec[T, M], that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] = + tsum match { + case TSumZero() => + $this match { case VNil => that } + case TSumM(sum) => + $this match { case VCons(x, xs) => VCons(x, append(xs, that)(sum)) } + } + +} diff --git a/tests/gadt/i5068.scala b/tests/gadt/i5068.scala new file mode 100644 index 000000000000..727c53e9d097 --- /dev/null +++ b/tests/gadt/i5068.scala @@ -0,0 +1,11 @@ +object i5068 { + case class Box[F[_]](value: F[Int]) + sealed trait IsK[F[_], G[_]] + final case class ReflK[F[_]]() extends IsK[F, F] + + def foo[F[_], G[_]](r: F IsK G, a: Box[F]): Box[G] = r match { case ReflK() => a } + + def main(args: Array[String]): Unit = { + println(foo(ReflK(), Box(Option(10)))) + } +} From 9a0826c12191258e216fdebb8717f34858ff155d Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Sat, 27 Oct 2018 21:43:33 +0200 Subject: [PATCH 05/21] Allow overriding ConstraintHandling logs --- .../tools/dotc/core/ConstraintHandling.scala | 21 +++++++++++-------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index a587a43a5e14..4dfb71de2501 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -20,6 +20,9 @@ import config.Printers.{constr, typr} */ trait ConstraintHandling { + def constr_println(msg: => String): Unit = constr.println(msg) + def typr_println(msg: => String): Unit = typr.println(msg) + implicit def ctx: Context protected def isSubType(tp1: Type, tp2: Type): Boolean @@ -107,23 +110,23 @@ trait ConstraintHandling { if (Config.failOnInstantiationToNothing) assert(false, msg) else ctx.log(msg) } - constr.println(i"adding $description$location") + constr_println(i"adding $description$location") val lower = constraint.lower(param) val res = addOneBound(param, bound, isUpper = true) && lower.forall(addOneBound(_, bound, isUpper = true)) - constr.println(i"added $description = $res$location") + constr_println(i"added $description = $res$location") res } protected def addLowerBound(param: TypeParamRef, bound: Type): Boolean = { def description = i"constraint $param >: $bound to\n$constraint" - constr.println(i"adding $description") + constr_println(i"adding $description") val upper = constraint.upper(param) val res = addOneBound(param, bound, isUpper = false) && upper.forall(addOneBound(_, bound, isUpper = false)) - constr.println(i"added $description = $res$location") + constr_println(i"added $description = $res$location") res } @@ -136,12 +139,12 @@ trait ConstraintHandling { val up2 = p2 :: constraint.exclusiveUpper(p2, p1) val lo1 = constraint.nonParamBounds(p1).lo val hi2 = constraint.nonParamBounds(p2).hi - constr.println(i"adding $description down1 = $down1, up2 = $up2$location") + constr_println(i"adding $description down1 = $down1, up2 = $up2$location") constraint = constraint.addLess(p1, p2) down1.forall(addOneBound(_, hi2, isUpper = true)) && up2.forall(addOneBound(_, lo1, isUpper = false)) } - constr.println(i"added $description = $res$location") + constr_println(i"added $description = $res$location") res } @@ -149,7 +152,7 @@ trait ConstraintHandling { * @pre less(p1)(p2) */ private def unify(p1: TypeParamRef, p2: TypeParamRef): Boolean = { - constr.println(s"unifying $p1 $p2") + constr_println(s"unifying $p1 $p2") assert(constraint.isLess(p1, p2)) val down = constraint.exclusiveLower(p2, p1) val up = constraint.exclusiveUpper(p1, p2) @@ -247,7 +250,7 @@ trait ConstraintHandling { case _: TypeBounds => val bound = if (fromBelow) constraint.fullLowerBound(param) else constraint.fullUpperBound(param) val inst = avoidParam(bound) - typr.println(s"approx ${param.show}, from below = $fromBelow, bound = ${bound.show}, inst = ${inst.show}") + typr_println(s"approx ${param.show}, from below = $fromBelow, bound = ${bound.show}, inst = ${inst.show}") inst case inst => assert(inst.exists, i"param = $param\nconstraint = $constraint") @@ -346,7 +349,7 @@ trait ConstraintHandling { val lower = constraint.lower(param) val upper = constraint.upper(param) if (lower.nonEmpty && !bounds.lo.isRef(defn.NothingClass) || - upper.nonEmpty && !bounds.hi.isRef(defn.AnyClass)) constr.println(i"INIT*** $tl") + upper.nonEmpty && !bounds.hi.isRef(defn.AnyClass)) constr_println(i"INIT*** $tl") lower.forall(addOneBound(_, bounds.hi, isUpper = true)) && upper.forall(addOneBound(_, bounds.lo, isUpper = false)) case _ => From 6db7caa3524a9822d7372d42c51b4176e51de77a Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Sat, 27 Oct 2018 21:44:33 +0200 Subject: [PATCH 06/21] Move TyperState.instType --- .../tools/dotc/core/ConstraintHandling.scala | 13 +++++++++++++ .../src/dotty/tools/dotc/core/TyperState.scala | 15 +-------------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 4dfb71de2501..75785ee4d9ab 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -53,6 +53,19 @@ trait ConstraintHandling { */ protected var comparedTypeLambdas: Set[TypeLambda] = Set.empty + /** Gives for each instantiated type var that does not yet have its `inst` field + * set, the instance value stored in the constraint. Storing instances in constraints + * is done only in a temporary way for contexts that may be retracted + * without also retracting the type var as a whole. + */ + def instType(tvar: TypeVar): Type = constraint.entry(tvar.origin) match { + case _: TypeBounds => NoType + case tp: TypeParamRef => + var tvar1 = constraint.typeVarOfParam(tp) + if (tvar1.exists) tvar1 else tp + case tp => tp + } + protected def addOneBound(param: TypeParamRef, bound: Type, isUpper: Boolean): Boolean = !constraint.contains(param) || { def occursIn(bound: Type): Boolean = { diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala index 5a2fb0052e0d..83efc1329350 100644 --- a/compiler/src/dotty/tools/dotc/core/TyperState.scala +++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala @@ -79,19 +79,6 @@ class TyperState(previous: TyperState /* | Null */) { def ownedVars: TypeVars = myOwnedVars def ownedVars_=(vs: TypeVars): Unit = myOwnedVars = vs - /** Gives for each instantiated type var that does not yet have its `inst` field - * set, the instance value stored in the constraint. Storing instances in constraints - * is done only in a temporary way for contexts that may be retracted - * without also retracting the type var as a whole. - */ - def instType(tvar: TypeVar)(implicit ctx: Context): Type = constraint.entry(tvar.origin) match { - case _: TypeBounds => NoType - case tp: TypeParamRef => - var tvar1 = constraint.typeVarOfParam(tp) - if (tvar1.exists) tvar1 else tp - case tp => tp - } - /** The closest ancestor of this typer state (including possibly this typer state itself) * which is not yet committed, or which does not have a parent. */ @@ -173,7 +160,7 @@ class TyperState(previous: TyperState /* | Null */) { val toCollect = new mutable.ListBuffer[TypeLambda] constraint foreachTypeVar { tvar => if (!tvar.inst.exists) { - val inst = instType(tvar) + val inst = ctx.typeComparer.instType(tvar) if (inst.exists && (tvar.owningState.get eq this)) { tvar.inst = inst val lam = tvar.origin.binder From 49c4a01ecf609d25af37079d6ff9aef2e0f23cc8 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Sat, 27 Oct 2018 23:38:08 +0200 Subject: [PATCH 07/21] Refactor TypeComparer.explained TypeComparer.explain is easier to just drop where necessary. Also, debugging an ExplainingTypeComparer calls .toString, which destroyed the stack trace previously. --- .../dotty/tools/dotc/core/TypeComparer.scala | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 7876b9e7645c..80cd268978d9 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -1770,6 +1770,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { totalCount = 0 } } + + /** Returns last check's debug mode, if explicitly enabled. */ + def lastTrace(): String = "" } object TypeComparer { @@ -1801,11 +1804,21 @@ object TypeComparer { val NoApprox: ApproxState = new ApproxState(0) + def explain[T](say: String => Unit)(op: Context => T)(implicit ctx: Context): T = { + val (res, explanation) = underlyingExplained(op) + say(explanation) + res + } + /** Show trace of comparison operations when performing `op` as result string */ def explained[T](op: Context => T)(implicit ctx: Context): String = { + underlyingExplained(op)._2 + } + + private def underlyingExplained[T](op: Context => T)(implicit ctx: Context): (T, String) = { val nestedCtx = ctx.fresh.setTypeComparerFn(new ExplainingTypeComparer(_)) - op(nestedCtx) - nestedCtx.typeComparer.toString + val res = op(nestedCtx) + (res, nestedCtx.typeComparer.lastTrace()) } } @@ -1937,5 +1950,5 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) { override def copyIn(ctx: Context): ExplainingTypeComparer = new ExplainingTypeComparer(ctx) - override def toString: String = "Subtype trace:" + { try b.toString finally b.clear() } + override def lastTrace(): String = "Subtype trace:" + { try b.toString finally b.clear() } } From d1cc3034fe43ada755a4d2664a71a9c4c4621dab Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Sun, 28 Oct 2018 00:00:45 +0200 Subject: [PATCH 08/21] Handle TypeVar instantiation Since GADTMap is re-initialised each time it is used, it's not necessary to care about avoiding instantiations for shared TypeVars. --- .../src/dotty/tools/dotc/core/Contexts.scala | 126 ++++++++++++++---- .../tools/dotc/core/OrderingConstraint.scala | 4 +- .../src/dotty/tools/dotc/core/Types.scala | 7 +- .../dotty/tools/dotc/typer/Inferencing.scala | 6 +- tests/gadt/{one.scala => i4075.scala} | 5 +- tests/gadt/i4471.scala | 31 +++++ 6 files changed, 146 insertions(+), 33 deletions(-) rename tests/gadt/{one.scala => i4075.scala} (76%) create mode 100644 tests/gadt/i4471.scala diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index cc4fd4586bc9..c54097688121 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -713,16 +713,27 @@ object Contexts { def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds def contains(sym: Symbol)(implicit ctx: Context): Boolean + def debugBoundsDescription(implicit ctx: Context): String def derived: GADTMap } final class SmartGADTMap( private[this] var myConstraint: Constraint = new OrderingConstraint(SimpleIdentityMap.Empty, SimpleIdentityMap.Empty, SimpleIdentityMap.Empty), private[this] var mapping: SimpleIdentityMap[Symbol, TypeVar] = SimpleIdentityMap.Empty, - private[this] var reverseMapping: SimpleIdentityMap[TypeVar, Symbol] = SimpleIdentityMap.Empty + private[this] var reverseMapping: SimpleIdentityMap[TypeParamRef, Symbol] = SimpleIdentityMap.Empty ) extends GADTMap with ConstraintHandling { import dotty.tools.dotc.config.Printers.gadts + override def debugBoundsDescription(implicit ctx: Context): String = { + val sb = new mutable.StringBuilder + sb ++= constraint.show + sb += '\n' + mapping.foreachBinding { case (sym, _) => + sb ++= i"$sym: ${bounds(sym)}\n" + } + sb.result + } + // TODO: dirty kludge - should this class be an inner class of TyperState instead? private[this] var myCtx: Context = null implicit override def ctx = myCtx @@ -750,13 +761,12 @@ object Contexts { val poly = PolyType(DepParamName.fresh(sym.name.toTypeName) :: Nil)( pt => TypeBounds.empty :: Nil, pt => defn.AnyType) - // null out creatorState as a precaution new TypeVar(poly.paramRefs.head, creatorState = null) } gadts.println(i"GADTMap: created tvar $sym -> $res") constraint = constraint.add(res.origin.binder, res :: Nil) mapping = mapping.updated(sym, res) - reverseMapping = reverseMapping.updated(res, sym) + reverseMapping = reverseMapping.updated(res.origin, sym) res } res @@ -765,26 +775,93 @@ object Contexts { override def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit = tvar(sym) override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = inCtx(ctx) { + @annotation.tailrec def stripInst(tp: Type): Type = tp match { + case tv: TypeVar => + val inst = tv.inst orElse instType(tv) + if (inst.exists) stripInst(inst) else tv + case _ => tp + } + + def cautiousSubtype(tp1: Type, tp2: Type, isSubtype: Boolean, allowNarrowing: Boolean = false): Boolean = { + val externalizedTp1 = (new TypeVarRemovingMap)(tp1) + val externalizedTp2 = (new TypeVarRemovingMap)(tp2) + + def descr = { + def op = s"frozen_${if (isSubtype) "<:<" else ">:>"}" + def flex = s"GADTFlexible=$allowNarrowing" + i"$tp1 $op $tp2\n\t$externalizedTp1 $op $externalizedTp2 ($flex)" + } + // gadts.println(descr) + + val outerCtx = ctx + val res = { + implicit val ctx : Context = + if (allowNarrowing) outerCtx else outerCtx.fresh.retractMode(Mode.GADTflexible) + + // TypeComparer.explain[Boolean](gadts.println) { implicit ctx => + if (isSubtype) externalizedTp1 frozen_<:< externalizedTp2 + else externalizedTp2 frozen_<:< externalizedTp1 + // } + } + gadts.println(i"$descr = $res") + res + } + + val symTvar: TypeVar = stripInst(tvar(sym)) match { + case tv: TypeVar => tv + case inst => + gadts.println(i"instantiated: $sym -> $inst") + return cautiousSubtype(inst, bound, isSubtype = isUpper, allowNarrowing = true) + } + + def doAddBound(bound: Type): Boolean = { + val res = stripInst(bound) match { + case boundTvar: TypeVar => + if (boundTvar eq symTvar) true + else if (isUpper) addLess(symTvar.origin, boundTvar.origin) + else addLess(boundTvar.origin, symTvar.origin) + case bound => + if (cautiousSubtype(symTvar, bound, isSubtype = !isUpper)) { instantiate(symTvar, bound); true } + else if (isUpper) addUpperBound(symTvar.origin, bound) + else addLowerBound(symTvar.origin, bound) + } + + vacuum() + res + } + def isEmptyBounds(tp: Type) = tp match { case TypeBounds(lo, hi) => (lo eq defn.NothingType) && (hi eq defn.AnyType) case _ => false } - val symTvar = tvar(sym) - - def doAddOrdering(bound: TypeParamRef) = - if (isUpper) addLess(symTvar.origin, bound) else addLess(bound, symTvar.origin) + def instantiate(tv: TypeVar, tp: Type): Unit = { + // instantiating one TypeVar to another makes us actually lose information + // that is, we need to know that both TypeVars are equal to another + // *and* be able to record further bounds on either one + if (tp.isInstanceOf[TypeVar]) return + val externalizedTp = (new TypeVarRemovingMap)(tp) + gadts.println(i"instantiating $tv to $externalizedTp ( $tp )") + tv.inst = externalizedTp + constraint = constraint.replace(tv.origin, externalizedTp) + } - def doAddBound(bound: Type) = - if (isUpper) addUpperBound(symTvar.origin, bound) else addLowerBound(symTvar.origin, bound) + def vacuum(): Unit = { + constraint.foreachTypeVar { tv => + if (!tv.inst.exists) { + val inst = instType(tv) + if (inst.exists) instantiate(tv, inst) + } + } + } val tvarBound = (new TypeVarInsertingMap)(bound) val res = tvarBound match { case boundTvar: TypeVar => - if (boundTvar eq symTvar) true else doAddOrdering(boundTvar.origin) + doAddBound(boundTvar) // hack to normalize T and T[_] case AppliedType(boundTvar: TypeVar, args) if args forall isEmptyBounds => - doAddOrdering(boundTvar.origin) + doAddBound(boundTvar) case tp => doAddBound(tp) } @@ -800,12 +877,10 @@ object Contexts { mapping(sym) match { case null => null case tv => - val tb = constraint.fullBounds(tv.origin) - val res = { - val tm = new TypeVarRemovingMap - tb.derivedTypeBounds(tm(tb.lo), tm(tb.hi)) - } - gadts.println(i"gadt bounds $sym: $res\t( $tv: $tb )") + val tb = + if (tv.inst.exists) TypeAlias(tv.inst) else constraint.fullBounds(tv.origin) + val res = (new TypeVarRemovingMap)(tb).asInstanceOf[TypeBounds] + // gadts.println(i"gadt bounds $sym: $res\t( $tv: $tb )") res } } @@ -831,17 +906,15 @@ object Contexts { private final class TypeVarRemovingMap extends TypeMap { override def apply(tp: Type): Type = tp match { case tpr: TypeParamRef => - constraint.typeVarOfParam(tpr) match { - case tv: TypeVar => - reverseMapping(tv).typeRef - case unexpected => - // if we didn't get a TypeVar, it's likely to cause problems - gadts.println(i"GADTMap: unexpected typeVarOfParam($tpr) = `$unexpected` ${unexpected.getClass}") - tpr + reverseMapping(tpr) match { + case null => tpr + case sym => sym.typeRef } case tv: TypeVar => - if (reverseMapping.contains(tv)) reverseMapping(tv).typeRef - else tv + reverseMapping(tv.origin) match { + case null => tv + case sym => sym.typeRef + } case _ => mapOver(tp) } @@ -853,6 +926,7 @@ object Contexts { override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = unsupported("EmptyGADTMap.addBound") override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = null override def contains(sym: Symbol)(implicit ctx: Context) = false + override def debugBoundsDescription(implicit ctx: Context): String = "EmptyGADTMap" override def derived = new SmartGADTMap } } diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala index f128f4e2022b..e310c197c132 100644 --- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala +++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala @@ -325,8 +325,8 @@ class OrderingConstraint(private val boundsMap: ParamBounds, private def order(current: This, param1: TypeParamRef, param2: TypeParamRef)(implicit ctx: Context): This = if (param1 == param2 || current.isLess(param1, param2)) this else { - assert(contains(param1)) - assert(contains(param2)) + assert(contains(param1), i"$param1") + assert(contains(param2), i"$param2") val newUpper = param2 :: exclusiveUpper(param2, param1) val newLower = param1 :: exclusiveLower(param1, param2) val current1 = (current /: newLower)(upperLens.map(this, _, _, newUpper ::: _)) diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index bb0ba6c3e49f..405ffe86a8d4 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -3597,7 +3597,7 @@ object Types { private[core] def inst: Type = myInst private[core] def inst_=(tp: Type): Unit = { myInst = tp - if (tp.exists) { + if (tp.exists && (owningState ne null)) { owningState.get.ownedVars -= this owningState = null // no longer needed; null out to avoid a memory leak } @@ -3606,13 +3606,14 @@ object Types { /** The state owning the variable. This is at first `creatorState`, but it can * be changed to an enclosing state on a commit. */ - private[core] var owningState: WeakReference[TyperState] = new WeakReference(creatorState) + private[core] var owningState: WeakReference[TyperState] = + if (creatorState == null) null else new WeakReference(creatorState) /** The instance type of this variable, or NoType if the variable is currently * uninstantiated */ def instanceOpt(implicit ctx: Context): Type = - if (inst.exists) inst else ctx.typerState.instType(this) + if (inst.exists) inst else ctx.typeComparer.instType(this) /** Is the variable already instantiated? */ def isInstantiated(implicit ctx: Context): Boolean = instanceOpt.exists diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala index befc06112068..b610621d6298 100644 --- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala +++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala @@ -206,7 +206,11 @@ object Inferencing { } val widePt = if (ctx.scala2Mode || refinementIsInvariant(tp)) pt else widenVariantParams(pt) - tp <:< widePt + import dotty.tools.dotc.config.Printers.gadts + gadts.println(i"constraining pattern type $tp <:< $widePt") + val res = tp <:< widePt + gadts.println(i"constrained pattern type $tp <:< $widePt = $res\n${ctx.gadt.debugBoundsDescription}") + res } /** The list of uninstantiated type variables bound by some prefix of type `T` which diff --git a/tests/gadt/one.scala b/tests/gadt/i4075.scala similarity index 76% rename from tests/gadt/one.scala rename to tests/gadt/i4075.scala index b46d864166fc..4c49cee2d95b 100644 --- a/tests/gadt/one.scala +++ b/tests/gadt/i4075.scala @@ -1,9 +1,12 @@ -object one { +object i4075 { case class One[T](fst: T) def bad[T](e: One[T]) = e match { case foo: One[a] => val t: T = e.fst // val nok: Nothing = t // should not compile val ok: a = t // does compile + One(ok) } + + val one: One[Int] = bad(One(0)) } diff --git a/tests/gadt/i4471.scala b/tests/gadt/i4471.scala new file mode 100644 index 000000000000..ff57a6a30891 --- /dev/null +++ b/tests/gadt/i4471.scala @@ -0,0 +1,31 @@ +object i4471 { + sealed trait Shuffle[A1, A2] { + def andThen[A3](that: Shuffle[A2, A3]): Shuffle[A1, A3] = AndThen(this, that) + } + + case class Id[A]() extends Shuffle[A, A] + case class Swap[A, B]() extends Shuffle[(A, B), (B, A)] + case class AssocLR[A, B, C]() extends Shuffle[((A, B), C), (A, (B, C))] + case class AssocRL[A, B, C]() extends Shuffle[(A, (B, C)), ((A, B), C)] + case class Par[A1, B1, A2, B2](_1: Shuffle[A1, B1], _2: Shuffle[A2, B2]) extends Shuffle[(A1, A2), (B1, B2)] + case class AndThen[A1, A2, A3](_1: Shuffle[A1, A2], _2: Shuffle[A2, A3]) extends Shuffle[A1, A3] + + def rewrite3[A1, A2, A3, A4]( + op1: Shuffle[A1, A2], + op2: Shuffle[A2, A3], + op3: Shuffle[A3, A4] + ): Option[Shuffle[A1, A4]] = (op1, op2, op3) match { + case ( + _: Swap[x, y], + _: AssocRL[u, v, w], + op3_ : Par[p1, q1, p2, q2] + ) => op3_ match { + case Par(_: Swap[r, s], _: Id[p2_]) => + Some( + AssocLR[v, w, u]() andThen Par(Id[v](), Swap[w, u]()) andThen AssocRL[v, u, w]() + ) + case _ => None + } + case _ => None + } +} From 5df8b3e6301a955bafc24583cdb2ac01b4e2b623 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Wed, 7 Nov 2018 15:00:55 +0100 Subject: [PATCH 09/21] Do not instantiate GadtMap TypeVars Instead, record semi-instantiations in the constraint. Otherwise, since the TypeVars live long enough, the _second_ case of a nested pattern match would see bounds recorded by the _first_ one. --- .../src/dotty/tools/dotc/core/Contexts.scala | 29 +--- tests/gadt/GadtStlc.scala | 127 ++++++++++++++++++ tests/gadt/TypeSafeLambda.scala | 109 +++++++++++++++ tests/gadt/complexEQ.scala | 24 ++++ 4 files changed, 266 insertions(+), 23 deletions(-) create mode 100644 tests/gadt/GadtStlc.scala create mode 100644 tests/gadt/TypeSafeLambda.scala create mode 100644 tests/gadt/complexEQ.scala diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index c54097688121..5503ba39a36a 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -777,7 +777,7 @@ object Contexts { override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = inCtx(ctx) { @annotation.tailrec def stripInst(tp: Type): Type = tp match { case tv: TypeVar => - val inst = tv.inst orElse instType(tv) + val inst = instType(tv) if (inst.exists) stripInst(inst) else tv case _ => tp } @@ -821,12 +821,11 @@ object Contexts { else if (isUpper) addLess(symTvar.origin, boundTvar.origin) else addLess(boundTvar.origin, symTvar.origin) case bound => - if (cautiousSubtype(symTvar, bound, isSubtype = !isUpper)) { instantiate(symTvar, bound); true } + if (cautiousSubtype(symTvar, bound, isSubtype = !isUpper)) { unify(symTvar, bound); true } else if (isUpper) addUpperBound(symTvar.origin, bound) else addLowerBound(symTvar.origin, bound) } - vacuum() res } @@ -835,24 +834,9 @@ object Contexts { case _ => false } - def instantiate(tv: TypeVar, tp: Type): Unit = { - // instantiating one TypeVar to another makes us actually lose information - // that is, we need to know that both TypeVars are equal to another - // *and* be able to record further bounds on either one - if (tp.isInstanceOf[TypeVar]) return - val externalizedTp = (new TypeVarRemovingMap)(tp) - gadts.println(i"instantiating $tv to $externalizedTp ( $tp )") - tv.inst = externalizedTp - constraint = constraint.replace(tv.origin, externalizedTp) - } - - def vacuum(): Unit = { - constraint.foreachTypeVar { tv => - if (!tv.inst.exists) { - val inst = instType(tv) - if (inst.exists) instantiate(tv, inst) - } - } + def unify(tv: TypeVar, tp: Type): Unit = { + gadts.println(i"manually unifying $tv with $tp") + constraint = constraint.updateEntry(tv.origin, tp) } val tvarBound = (new TypeVarInsertingMap)(bound) @@ -877,8 +861,7 @@ object Contexts { mapping(sym) match { case null => null case tv => - val tb = - if (tv.inst.exists) TypeAlias(tv.inst) else constraint.fullBounds(tv.origin) + val tb = constraint.fullBounds(tv.origin) val res = (new TypeVarRemovingMap)(tb).asInstanceOf[TypeBounds] // gadts.println(i"gadt bounds $sym: $res\t( $tv: $tb )") res diff --git a/tests/gadt/GadtStlc.scala b/tests/gadt/GadtStlc.scala new file mode 100644 index 000000000000..32e6f5630d6b --- /dev/null +++ b/tests/gadt/GadtStlc.scala @@ -0,0 +1,127 @@ +object GadtStlc { + // creates type-level "strings" like M[M[M[W]]] + object W + type W = W.type + class M[A] + + + // variable with name A + // Var[W] + // Var[M[W]] + sealed trait Var[A] + object VarW extends Var[W] + case class VarM[A] extends Var[M[A]] + + // \s.e + sealed trait Abs[S, E] + case class AbsC[S, E](v: Var[S], b: E) extends Abs[Var[S], E] + + // e1 e2 + case class App[E1, E2](e1: E1, e2: E2) + + // T1 -> T2 + case class TyFun[T1, T2](t1: T1, t2: T2) + + // arbitrary base literal + case object Lit + type Lit = Lit.type + + // arbitrary base type + case object TyBase + type TyBase = TyBase.type + + // IN[G, (X, TY)] === evidence that binding (X, TY) is in environment G + // x: ty \in G + sealed trait IN[G, P] + case class INOne[G, X, TY]() extends IN[(G, (X,TY)), (X, TY)] + // this is wrong - we need evidence that A does not contain a binding for X + case class INShift[G0, A, X, TY](in: IN[G0, (X, TY)]) extends IN[(G0, A), (X, TY)] + + // DER[G, E, TY] === evidence that G |- E : TY + sealed trait DER[G, E, TY] + case class DVar[G, G0, X, TY]( + in: IN[(G, G0), (Var[X], TY)] + ) extends DER[(G, G0), Var[X], TY] + + case class DApp[G, E1, E2, TY1, TY2]( + d1: DER[G, E1, TyFun[TY1, TY2]], + d2: DER[G, E2, TY1] + ) extends DER[G, App[E1, E2], TY2] + + case class DAbs[G, X, E, TY1, TY2]( + d1: DER[(G, (Var[X], TY1)), E, TY2] + ) extends DER[G, Abs[Var[X], E], TyFun[TY1, TY2]] + + case class DLit[G]() extends DER[G, Lit, TyBase] + + // forall G, a. G |- \x.x : a -> a + def test1[G, TY]: DER[G, Abs[Var[W], Var[W]], TyFun[TY, TY]] = + DAbs(DVar(INOne())) + + // forall G. G |- \x.x : Lit -> Lit + def test2[G]: DER[G, App[Abs[Var[W], Var[W]], Lit], TyBase] = + DApp(DAbs(DVar(INOne())), DLit()) + + // forall G, c. G |- \x.\y. x y : (c -> c) -> c -> c + def test3[G, TY]: DER[G, + Abs[Var[W], + Abs[Var[M[W]], + App[Var[W], Var[M[W]]] + ] + ], + TyFun[TyFun[TY, TY], TyFun[TY, TY]] + ] = DAbs(DAbs(DApp(DVar(INShift(INOne())), DVar(INOne())))) + + + // evidence that E is a value + sealed trait ISVAL[E] + case class ISVAL_Abs[X, E]() extends ISVAL[Abs[Var[X], E]] + case object ISVAL_Lit extends ISVAL[Lit] + + // evidence that E1 reduces to E2 + sealed trait REDUDER[E1, E2] + case class EApp1[E1a, E1b, E2]( + ed: REDUDER[E1a, E1b] + ) extends REDUDER[App[E1a, E2], App[E1b, E2]] + + case class EApp2[V1, E2a, E2b]( + isval: ISVAL[V1], + ed: REDUDER[E2a, E2b] + ) extends REDUDER[App[V1, E2a], App[V1, E2b]] + + case class EAppAbs[X, E, V2, R]( + isval: ISVAL[V2] + // cheating - subst is hard + // , subst: SUBST[E, X, V2, R] + ) extends REDUDER[App[Abs[Var[X], E], V2], R] + + // evidence that V is a lambda + sealed trait ISLAMBDA[V] + case class ISLAMBDAC[X, E]() extends ISLAMBDA[Abs[Var[X], E]] + + // evidence that E reduces + type REDUCES[E] = REDUDER[E, _] + + def followsIsLambda[G, V, TY1, TY2]( + isval: ISVAL[V], + der: DER[G, V, TyFun[TY1, TY2]] + ): ISLAMBDA[V] = (isval, der) match { + case (_: ISVAL_Abs[x, e], _) => ISLAMBDAC[x, e]() + } + + // \empty |- E : TY ==> E is a value /\ E reduces to some E1 + def progress[E, TY](der: DER[Unit, E, TY]): Either[ISVAL[E], REDUCES[E]] = + der match { + case _: DAbs[g, a, e, ty1, ty2] => Left(ISVAL_Abs[a, e]()) + case DLit() => Left(ISVAL_Lit) + case dapp: DApp[Unit, a, b, ty1, ty2] => progress(dapp.d1) match { + case Right(r1) => Right(EApp1[E2 = b](r1)) + case Left(isv1) => progress(dapp.d2) match { + case Right(r2) => Right(EApp2(isv1, r2)) + case Left(isv2) => followsIsLambda(isv1, dapp.d1) match { + case _: ISLAMBDAC[x, e] => Right(EAppAbs[x, e, b, _](isv2)) + } + } + } + } +} diff --git a/tests/gadt/TypeSafeLambda.scala b/tests/gadt/TypeSafeLambda.scala new file mode 100644 index 000000000000..b9cbbc50757e --- /dev/null +++ b/tests/gadt/TypeSafeLambda.scala @@ -0,0 +1,109 @@ +object TypeSafeLambda { + + trait Category[Arr[_, _]] { + def id[A]: Arr[A, A] + def comp[A, B, C](ab: Arr[A, B], bc: Arr[B, C]): Arr[A, C] + } + + trait Terminal[Term, Arr[_, _]] extends Category[Arr] { + def terminal[A]: Arr[A, Term] + } + + trait ProductCategory[Prod[_, _], Arr[_, _]] extends Category[Arr] { + def first[A, B]: Arr[Prod[A, B], A] + def second[A, B]: Arr[Prod[A, B], B] + def pair[A, B, C](ab: Arr[A, B], ac: Arr[A, C]): Arr[A, Prod[B, C]] + } + + trait Exponential[Exp[_, _], Prod[_, _], Arr[_, _]] + extends ProductCategory[Prod, Arr] { + def eval[A, B]: Arr[Prod[Exp[A, B], A], B] + def curry[A, B, C](a: Arr[Prod[C, A], B]): Arr[C, Exp[A, B]] + } + + trait CartesianClosed[Term, Exp[_, _], Prod[_, _], Arr[_, _]] + extends Exponential[Exp, Prod, Arr] with Terminal[Term, Arr] + + sealed trait V[Prod[_, _], Env, R] + case class Zero[Prod[_, _], Env, R]() extends V[Prod, Prod[Env, R], R] + case class Succ[Prod[_, _], Env, R, X]( + v: V[Prod, Env, R] + ) extends V[Prod, Prod[Env, X], R] + + sealed trait Lambda[Terminal, Exp[_, _], Prod[_, _], Env, R] + + case class LUnit[Terminal, Exp[_, _], Prod[_, _], Env]() + extends Lambda[Terminal, Exp, Prod, Env, Terminal] + + case class Var[Terminal, Exp[_, _], Prod[_, _], Env, R]( + v: V[Prod, Env, R] + ) extends Lambda[Terminal, Exp, Prod, Env, R] + + case class Lam[Terminal, Exp[_, _], Prod[_, _], Env, R, A]( + lam: Lambda[Terminal, Exp, Prod, Prod[Env, A], R] + ) extends Lambda[Terminal, Exp, Prod, Env, Exp[A, R]] + + case class App[Terminal, Exp[_, _], Prod[_, _], Env, R, R_]( + f: Lambda[Terminal, Exp, Prod, Env, Exp[R, R_]], + a: Lambda[Terminal, Exp, Prod, Env, R] + ) extends Lambda[Terminal, Exp, Prod, Env, R_] + + def interp[Term, Exp[_, _], Prod[_, _], Arr[_, _], S, T]( + c: CartesianClosed[Term, Exp, Prod, Arr], + exp: Lambda[Term, Exp, Prod, S, T] + ): Arr[S, T] = exp match { + case LUnit() => c.terminal + case v: Var[t, e, var_p, env, r] => v.v match { + case _: Zero[z_p, z_env, z_r] => c.second[z_env, z_r] + case s: Succ[s_prod, s_env, s_r, x] => + c.comp[A = s_prod[s_env, x], C = s_r]( + c.first, + interp(c, Var[Term, Exp, Prod, s_env, s_r](s.v)) + ) + } + case Lam(lam) => c.curry(interp(c, lam)) + case app: App[t, e, p, env, r, r_] => + c.comp( + c.pair( + interp(c, app.f), + interp(c, app.a)), + c.eval[r, r_] + ) + } + + object example { + type Term = Unit + type Prod[A, B] = (A, B) + type Exp[A, B] = A => B + type Arr[A, B] = A => B + + val c = new CartesianClosed[Term, Exp, Prod, Arr] { + def id[A]: A => A = a => a + def comp[A, B, C](f: A => B, g: B => C): A => C = f andThen g + + def terminal[A]: A => Unit = a => () + + def first[A, B]: ((A, B)) => A = { case (a, _) => a } + def second[A, B]: ((A, B)) => B = { case (_, b) => b } + def pair[A, B, C](f: A => B, g: A => C): A => (B, C) = + a => (f(a), g(a)) + + def eval[A, B]: ((A => B, A)) => B = { case (f, a) => f(a) } + def curry[A, B, C](f: ((C, A)) => B): C => A => B = + c => a => f((c, a)) + } + + type Env = Unit Prod Int Prod (Int => String) + val exp = App[Term, Exp, Prod, Env, Int, String]( + // args to Var are RHS "indices" into Env + Var(Zero()), + Var(Succ(Zero())) + ) + + val interped: (Env) => String = + interp[Term, Exp, Prod, Arr, Env, String] (c, exp) + + interped((((), 1), { i: Int => i.toString })) : String // "1" + } + +} diff --git a/tests/gadt/complexEQ.scala b/tests/gadt/complexEQ.scala new file mode 100644 index 000000000000..991c838ad610 --- /dev/null +++ b/tests/gadt/complexEQ.scala @@ -0,0 +1,24 @@ +object complexEQ { + sealed trait EQ[A, B] + final case class Refl[A]() extends EQ[A, A] + + def m[A, B, C, D](e1: EQ[A, (B, C)], e2: EQ[A, (C, D)], d: D): A = + e1 match { + case Refl() => e2 match { + case Refl() => + val r1: (B, B) = (d, d) + val r2: (C, C) = r1 + val r3: (D, D) = r1 + r1 + } + } + + def m2[Z, A, B, C, D](e0: EQ[Z, A], e1: EQ[A, (B, C)], e2: EQ[Z, (C, D)], d: D): Z = + (e0, e1, e2) match { + case (Refl(), Refl(), Refl()) => + val r1: (B, B) = (d, d) + val r2: (C, C) = r1 + val r3: (D, D) = r1 + r1 + } +} From c23ff102f249a953f96ab0cef09fb1058e48a73c Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Wed, 7 Nov 2018 15:14:20 +0100 Subject: [PATCH 10/21] Remove unnecessary hack for HKT Apparently it was fixed along the way. --- .../src/dotty/tools/dotc/core/Contexts.scala | 8 -------- tests/gadt/i5068.scala | 19 ++++++++++++++++--- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 5503ba39a36a..6bd8b2a350fa 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -829,11 +829,6 @@ object Contexts { res } - def isEmptyBounds(tp: Type) = tp match { - case TypeBounds(lo, hi) => (lo eq defn.NothingType) && (hi eq defn.AnyType) - case _ => false - } - def unify(tv: TypeVar, tp: Type): Unit = { gadts.println(i"manually unifying $tv with $tp") constraint = constraint.updateEntry(tv.origin, tp) @@ -843,9 +838,6 @@ object Contexts { val res = tvarBound match { case boundTvar: TypeVar => doAddBound(boundTvar) - // hack to normalize T and T[_] - case AppliedType(boundTvar: TypeVar, args) if args forall isEmptyBounds => - doAddBound(boundTvar) case tp => doAddBound(tp) } diff --git a/tests/gadt/i5068.scala b/tests/gadt/i5068.scala index 727c53e9d097..b4fba06f3c53 100644 --- a/tests/gadt/i5068.scala +++ b/tests/gadt/i5068.scala @@ -4,8 +4,21 @@ object i5068 { final case class ReflK[F[_]]() extends IsK[F, F] def foo[F[_], G[_]](r: F IsK G, a: Box[F]): Box[G] = r match { case ReflK() => a } +} + +object i5068b { + type WeirdShape[A[_], B] = A[B] + // type WeirderShape[S[_[_], _], I, M] = Any + case class Box[ F[_[_[_], _], _, _[_]] ](value: F[WeirdShape, Int, Option]) + sealed trait IsK[F[_[_[_], _], _, _[_]], G[_[_[_], _], _, _[_]]] + final case class ReflK[ F[_[_[_], _], _, _[_]] ]() extends IsK[F, F] + + def foo[F[_[_[_], _], _, _[_]], G[_[_[_], _], _, _[_]]]( + r: F IsK G, + a: Box[F] + ): Box[G] = r match { case ReflK() => a } - def main(args: Array[String]): Unit = { - println(foo(ReflK(), Box(Option(10)))) - } + // def main(args: Array[String]): Unit = { + // println(foo(ReflK(), Box[WeirderShape](???))) + // } } From df2bc0547a572b9747a71e08e44ef92a179efcd3 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Wed, 7 Nov 2018 15:15:09 +0100 Subject: [PATCH 11/21] Add neg GADT test --- compiler/test/dotty/tools/dotc/GadtTests.scala | 5 +++++ tests/gadt-neg/banal-nested.scala | 12 ++++++++++++ tests/gadt-neg/banal.scala | 17 +++++++++++++++++ tests/gadt-neg/i4075.scala | 8 ++++++++ 4 files changed, 42 insertions(+) create mode 100644 tests/gadt-neg/banal-nested.scala create mode 100644 tests/gadt-neg/banal.scala create mode 100644 tests/gadt-neg/i4075.scala diff --git a/compiler/test/dotty/tools/dotc/GadtTests.scala b/compiler/test/dotty/tools/dotc/GadtTests.scala index cf557a65f830..ea8de0071122 100644 --- a/compiler/test/dotty/tools/dotc/GadtTests.scala +++ b/compiler/test/dotty/tools/dotc/GadtTests.scala @@ -24,6 +24,11 @@ class GadtTests extends ParallelTesting { implicit val testGroup: TestGroup = TestGroup("compileGadtTests") compileFilesInDir("tests/gadt", defaultOptions).checkCompile() } + + @Test def compileGadtNeg: Unit = { + implicit val testGroup: TestGroup = TestGroup("compileGadtNeg") + compileFilesInDir("tests/gadt-neg", defaultOptions).checkExpectedErrors() + } } object GadtTests { diff --git a/tests/gadt-neg/banal-nested.scala b/tests/gadt-neg/banal-nested.scala new file mode 100644 index 000000000000..3a098f69739a --- /dev/null +++ b/tests/gadt-neg/banal-nested.scala @@ -0,0 +1,12 @@ +object banal { + sealed trait T[A] + final case class StrLit(v: String) extends T[String] + final case class IntLit(v: Int) extends T[Int] + + def eval[A](t: T[A]): A = t match { + case _: T[a] => t match { + case StrLit(v) => v + case IntLit(_) => "" // error + } + } +} diff --git a/tests/gadt-neg/banal.scala b/tests/gadt-neg/banal.scala new file mode 100644 index 000000000000..a822c827d917 --- /dev/null +++ b/tests/gadt-neg/banal.scala @@ -0,0 +1,17 @@ +object banal { + final case class Box[A](a: A) + + sealed trait T[A] + final case class StrLit(v: String) extends T[String] + final case class IntLit(v: Int) extends T[Int] + + def evul[A](t: T[A]): A = t match { + case StrLit(v) => (v: Any) // error + case IntLit(v) => (??? : Nothing) + } + + def noeval[A](t: T[A]): Box[A] = t match { + case StrLit(v) => Box[Any](v) // error + case IntLit(v) => Box[Nothing](???) // error + } +} diff --git a/tests/gadt-neg/i4075.scala b/tests/gadt-neg/i4075.scala new file mode 100644 index 000000000000..7037fbc7d5d3 --- /dev/null +++ b/tests/gadt-neg/i4075.scala @@ -0,0 +1,8 @@ +object i4075 { + case class One[T](fst: T) + def bad[T](e: One[T]) = e match { + case foo: One[a] => + val nok: Nothing = foo.fst // error + ??? + } +} From 7f40ea0ad94442fcb21edba2da99027b0cda0f9e Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Wed, 7 Nov 2018 17:29:47 +0100 Subject: [PATCH 12/21] Fixx issue with GADTs using HKTs --- .../dotty/tools/dotc/core/TypeComparer.scala | 21 +++++++++++- tests/gadt/EQK.scala | 33 +++++++++++++++++++ 2 files changed, 53 insertions(+), 1 deletion(-) create mode 100644 tests/gadt/EQK.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 80cd268978d9..eecf18760205 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -740,9 +740,28 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { isSubArgs(args1, args2, tp1, tparams) case tycon1: TypeRef => tycon2.dealiasKeepRefiningAnnots match { - case tycon2: TypeRef if tycon1.symbol == tycon2.symbol => + case tycon2: TypeRef => + val tycon1sym = tycon1.symbol + val tycon2sym = tycon2.symbol + + var touchedGADTs = false + def gadtBoundsContain(sym: Symbol, tp: Type): Boolean = { + touchedGADTs = true + val b = gadtBounds(sym) + b != null && inFrozenConstraint { + (b.lo =:= tp) && (b.hi =:= tp) + } + } + + val res = ( + tycon1sym == tycon2sym || + gadtBoundsContain(tycon1sym, tycon2) || + gadtBoundsContain(tycon2sym, tycon1) + ) && isSubType(tycon1.prefix, tycon2.prefix) && isSubArgs(args1, args2, tp1, tparams) + if (res && touchedGADTs) GADTused = true + res case _ => false } diff --git a/tests/gadt/EQK.scala b/tests/gadt/EQK.scala new file mode 100644 index 000000000000..b713de2d833b --- /dev/null +++ b/tests/gadt/EQK.scala @@ -0,0 +1,33 @@ +object EQK { + sealed trait EQ[A, B] + final case class Refl[A]() extends EQ[A, A] + + sealed trait EQK[F[_], G[_]] + final case class ReflK[F[_]]() extends EQK[F, F] + + def m0[F[_], G[_], A](fa: F[A], eqk: EQK[F, G]): G[A] = + eqk match { case ReflK() => fa } + + def m1[F[_], G[_], A](fa: F[A], eq: EQ[A, Int], eqk: EQK[F, G]): G[Int] = + eqk match { + case ReflK() => eq match { + case Refl() => + val r1: F[Int] = fa + val r2: G[A] = fa + val r3: F[Int] = r2 + fa : G[Int] + } + } + + def m2[F[_], G[_], A](fa: F[A], a: A, eq: EQ[F[A], G[Int]], eqk: EQK[F, G]): Int = + eqk match { + case ReflK() => eq match { + case Refl() => + val r1: F[Int] = fa + val r2: G[A] = fa + val r3: F[Int] = r2 + a + } + } + +} From bb192182c946f077d4c0954b3a276e44a5066a41 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Sun, 11 Nov 2018 20:02:58 +0100 Subject: [PATCH 13/21] Add more GADT tests --- tests/gadt-neg/injectivity.scala | 17 +++++++++++++++++ tests/gadt/injectivity.scala | 9 +++++++-- 2 files changed, 24 insertions(+), 2 deletions(-) create mode 100644 tests/gadt-neg/injectivity.scala diff --git a/tests/gadt-neg/injectivity.scala b/tests/gadt-neg/injectivity.scala new file mode 100644 index 000000000000..d4f8373e102a --- /dev/null +++ b/tests/gadt-neg/injectivity.scala @@ -0,0 +1,17 @@ +object injectivity { + sealed trait EQ[A, B] + final case class Refl[A](u: Unit) extends EQ[A, A] + + def conform[A, B, C, D](a: A, b: B, eq: EQ[(A, B), (C, D)]): C = + eq match { + case _: Refl[a] => + val ab: (A, B) = (a, b) + val cd: (C, D) = ab + val bb: (B, B) = ab // error + val cc: (C, C) = cd // error + val dd: (D, D) = cd // error + val rab: a = ab + val rcd: a = cd + a + } +} diff --git a/tests/gadt/injectivity.scala b/tests/gadt/injectivity.scala index bd04d89ee025..525db2ce798c 100644 --- a/tests/gadt/injectivity.scala +++ b/tests/gadt/injectivity.scala @@ -1,9 +1,14 @@ object injectivity { sealed trait EQ[A, B] - final case class Refl[A](u: Unit) extends EQ[A, A] + final case class Refl[A]() extends EQ[A, A] def conform[A, B, C, D](a: A, b: B, eq: EQ[(A, B), (C, D)]): C = eq match { - case Refl(()) => a + case _: Refl[a] => + val ab: (A, B) = (a, b) + val cd: (C, D) = ab + val rab: a = ab + val rcd: a = cd + a } } From 7225ca2d27fcea04421f97b5cbeff9cca39b1c04 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Fri, 16 Nov 2018 23:01:08 +0100 Subject: [PATCH 14/21] Add caching to SmartGADTMap --- .../src/dotty/tools/dotc/core/Contexts.scala | 73 ++++++++++++++----- 1 file changed, 55 insertions(+), 18 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 6bd8b2a350fa..07d4fd7fec8b 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -717,13 +717,23 @@ object Contexts { def derived: GADTMap } - final class SmartGADTMap( - private[this] var myConstraint: Constraint = new OrderingConstraint(SimpleIdentityMap.Empty, SimpleIdentityMap.Empty, SimpleIdentityMap.Empty), - private[this] var mapping: SimpleIdentityMap[Symbol, TypeVar] = SimpleIdentityMap.Empty, - private[this] var reverseMapping: SimpleIdentityMap[TypeParamRef, Symbol] = SimpleIdentityMap.Empty + final class SmartGADTMap private ( + private[this] var myConstraint: Constraint, + private[this] var mapping: SimpleIdentityMap[Symbol, TypeVar], + private[this] var reverseMapping: SimpleIdentityMap[TypeParamRef, Symbol], + private[this] var boundCache: SimpleIdentityMap[Symbol, TypeBounds], + private[this] var dirtyFlag: Boolean ) extends GADTMap with ConstraintHandling { import dotty.tools.dotc.config.Printers.gadts + def this() = this( + myConstraint = new OrderingConstraint(SimpleIdentityMap.Empty, SimpleIdentityMap.Empty, SimpleIdentityMap.Empty), + mapping = SimpleIdentityMap.Empty, + reverseMapping = SimpleIdentityMap.Empty, + boundCache = SimpleIdentityMap.Empty, + dirtyFlag = false + ) + override def debugBoundsDescription(implicit ctx: Context): String = { val sb = new mutable.StringBuilder sb ++= constraint.show @@ -734,6 +744,8 @@ object Contexts { sb.result } + private[this] var checkInProgress = false + // TODO: dirty kludge - should this class be an inner class of TyperState instead? private[this] var myCtx: Context = null implicit override def ctx = myCtx @@ -749,9 +761,10 @@ object Contexts { override def isSubType(tp1: Type, tp2: Type): Boolean = ctx.typeComparer.isSubType(tp1, tp2) override def isSameType(tp1: Type, tp2: Type): Boolean = ctx.typeComparer.isSameType(tp1, tp2) - private[this] def tvar(sym: Symbol)(implicit ctx: Context): TypeVar = inCtx(ctx) { - val res = mapping(sym) match { - case tv: TypeVar => tv + private[this] def tvar(sym: Symbol)(implicit ctx: Context): TypeVar = { + mapping(sym) match { + case tv: TypeVar => + tv case null => val res = { import NameKinds.DepParamName @@ -769,12 +782,13 @@ object Contexts { reverseMapping = reverseMapping.updated(res.origin, sym) res } - res } override def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit = tvar(sym) - override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = inCtx(ctx) { + override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = try inCtx(ctx) { + dirtyFlag = true + checkInProgress = true @annotation.tailrec def stripInst(tp: Type): Type = tp match { case tv: TypeVar => val inst = instType(tv) @@ -795,8 +809,8 @@ object Contexts { val outerCtx = ctx val res = { - implicit val ctx : Context = - if (allowNarrowing) outerCtx else outerCtx.fresh.retractMode(Mode.GADTflexible) +// implicit val ctx : Context = +// if (allowNarrowing) outerCtx else outerCtx.fresh.retractMode(Mode.GADTflexible) // TypeComparer.explain[Boolean](gadts.println) { implicit ctx => if (isSubtype) externalizedTp1 frozen_<:< externalizedTp2 @@ -811,6 +825,7 @@ object Contexts { case tv: TypeVar => tv case inst => gadts.println(i"instantiated: $sym -> $inst") +// return true return cautiousSubtype(inst, bound, isSubtype = isUpper, allowNarrowing = true) } @@ -847,15 +862,35 @@ object Contexts { i"adding $descr bound $sym $op $bound = $res\t( $symTvar $op $tvarBound )" } res - } + } finally checkInProgress = false override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = inCtx(ctx) { mapping(sym) match { case null => null case tv => - val tb = constraint.fullBounds(tv.origin) - val res = (new TypeVarRemovingMap)(tb).asInstanceOf[TypeBounds] - // gadts.println(i"gadt bounds $sym: $res\t( $tv: $tb )") + def retrieveBounds: TypeBounds = { + val tb = constraint.fullBounds(tv.origin) + (new TypeVarRemovingMap)(tb).asInstanceOf[TypeBounds] + } + val res = +// retrieveBounds + if (checkInProgress || ctx.mode.is(Mode.GADTflexible)) retrieveBounds + else { + if (dirtyFlag) { + dirtyFlag = false + val bounds = retrieveBounds + boundCache = SimpleIdentityMap.Empty.updated(sym, bounds) + bounds + } else boundCache(sym) match { + case tb: TypeBounds => + tb + case null => + val bounds = retrieveBounds + boundCache = boundCache.updated(sym, bounds) + bounds + } + } + // gadts.println(i"gadt bounds $sym: $res") res } } @@ -863,9 +898,11 @@ object Contexts { override def contains(sym: Symbol)(implicit ctx: Context): Boolean = mapping(sym) ne null override def derived: GADTMap = new SmartGADTMap( - this.myConstraint, - this.mapping, - this.reverseMapping + myConstraint, + mapping, + reverseMapping, + boundCache, + dirtyFlag ) private final class TypeVarInsertingMap extends TypeMap { From 876cee630080bacddfdad136d80da3c6f5b4f792 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Thu, 22 Nov 2018 10:24:12 +0100 Subject: [PATCH 15/21] Clean up comments and remove useless code --- .../src/dotty/tools/dotc/core/Contexts.scala | 29 +++++++------------ .../dotty/tools/dotc/core/TypeComparer.scala | 2 -- 2 files changed, 11 insertions(+), 20 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 07d4fd7fec8b..9725a2801696 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -746,7 +746,7 @@ object Contexts { private[this] var checkInProgress = false - // TODO: dirty kludge - should this class be an inner class of TyperState instead? + // TODO: clean up this dirty kludge private[this] var myCtx: Context = null implicit override def ctx = myCtx @forceInline private[this] final def inCtx[T](_ctx: Context)(op: => T) = { @@ -769,8 +769,8 @@ object Contexts { val res = { import NameKinds.DepParamName // avoid registering the TypeVar with TyperState / TyperState#constraint - // TyperState TypeVars get instantiated when we don't want them to (see pos/i3500.scala) - // TyperState#constraint TypeVars can be narrowed in subtype checks - don't want that either + // - we don't want TyperState instantiating these TypeVars + // - we don't want TypeComparer constraining these TypeVars val poly = PolyType(DepParamName.fresh(sym.name.toTypeName) :: Nil)( pt => TypeBounds.empty :: Nil, pt => defn.AnyType) @@ -796,27 +796,22 @@ object Contexts { case _ => tp } - def cautiousSubtype(tp1: Type, tp2: Type, isSubtype: Boolean, allowNarrowing: Boolean = false): Boolean = { + def cautiousSubtype(tp1: Type, tp2: Type, isSubtype: Boolean): Boolean = { val externalizedTp1 = (new TypeVarRemovingMap)(tp1) val externalizedTp2 = (new TypeVarRemovingMap)(tp2) def descr = { def op = s"frozen_${if (isSubtype) "<:<" else ">:>"}" - def flex = s"GADTFlexible=$allowNarrowing" - i"$tp1 $op $tp2\n\t$externalizedTp1 $op $externalizedTp2 ($flex)" + i"$tp1 $op $tp2\n\t$externalizedTp1 $op $externalizedTp2" } // gadts.println(descr) - val outerCtx = ctx - val res = { -// implicit val ctx : Context = -// if (allowNarrowing) outerCtx else outerCtx.fresh.retractMode(Mode.GADTflexible) - + val res = // TypeComparer.explain[Boolean](gadts.println) { implicit ctx => - if (isSubtype) externalizedTp1 frozen_<:< externalizedTp2 + if (isSubtype) externalizedTp1 frozen_<:< externalizedTp2 else externalizedTp2 frozen_<:< externalizedTp1 // } - } + gadts.println(i"$descr = $res") res } @@ -825,8 +820,8 @@ object Contexts { case tv: TypeVar => tv case inst => gadts.println(i"instantiated: $sym -> $inst") -// return true - return cautiousSubtype(inst, bound, isSubtype = isUpper, allowNarrowing = true) + // this is wrong in general, but "correct" due to a subtype check in TypeComparer#narrowGadtBounds + return true } def doAddBound(bound: Type): Boolean = { @@ -873,7 +868,6 @@ object Contexts { (new TypeVarRemovingMap)(tb).asInstanceOf[TypeBounds] } val res = -// retrieveBounds if (checkInProgress || ctx.mode.is(Mode.GADTflexible)) retrieveBounds else { if (dirtyFlag) { @@ -882,8 +876,7 @@ object Contexts { boundCache = SimpleIdentityMap.Empty.updated(sym, bounds) bounds } else boundCache(sym) match { - case tb: TypeBounds => - tb + case tb: TypeBounds => tb case null => val bounds = retrieveBounds boundCache = boundCache.updated(sym, bounds) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index eecf18760205..912deda62e04 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -1237,8 +1237,6 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { val newBounds = if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound) else TypeBounds(oldBounds.lo | bound, oldBounds.hi) - // gadtMap can check its own satisfiability, but the subtype check is still necessary - // see tests/patmat/gadt-nontrivial2.scala isSubType(newBounds.lo, newBounds.hi) && (if (isUpper) gadtAddUpperBound(tparam, bound) else gadtAddLowerBound(tparam, bound)) } From 9ed0993f62eb7cfe8dfc91a2a0b201fc86457c70 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Thu, 22 Nov 2018 10:27:58 +0100 Subject: [PATCH 16/21] Add specialized printer for GADT constraint --- compiler/src/dotty/tools/dotc/config/Printers.scala | 1 + compiler/src/dotty/tools/dotc/core/Contexts.scala | 4 +++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/config/Printers.scala b/compiler/src/dotty/tools/dotc/config/Printers.scala index 0c888b849857..b1f2afe6e463 100644 --- a/compiler/src/dotty/tools/dotc/config/Printers.scala +++ b/compiler/src/dotty/tools/dotc/config/Printers.scala @@ -20,6 +20,7 @@ object Printers { val dottydoc: Printer = noPrinter val exhaustivity: Printer = noPrinter val gadts: Printer = noPrinter + val gadtsConstr: Printer = noPrinter val hk: Printer = noPrinter val implicits: Printer = noPrinter val implicitsDetailed: Printer = noPrinter diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 9725a2801696..3db26347b1de 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -724,7 +724,7 @@ object Contexts { private[this] var boundCache: SimpleIdentityMap[Symbol, TypeBounds], private[this] var dirtyFlag: Boolean ) extends GADTMap with ConstraintHandling { - import dotty.tools.dotc.config.Printers.gadts + import dotty.tools.dotc.config.Printers.{gadts, gadtsConstr} def this() = this( myConstraint = new OrderingConstraint(SimpleIdentityMap.Empty, SimpleIdentityMap.Empty, SimpleIdentityMap.Empty), @@ -734,6 +734,8 @@ object Contexts { dirtyFlag = false ) + override def constr_println(msg: => String): Unit = gadtsConstr.println(msg) + override def debugBoundsDescription(implicit ctx: Context): String = { val sb = new mutable.StringBuilder sb ++= constraint.show From f008bbc57f4c072811c5507c788af28882debffd Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Thu, 22 Nov 2018 10:45:56 +0100 Subject: [PATCH 17/21] Cleanup SmartGADTMap#ctx Parameterised ConstraintHandling on what context it needs. TypeComparer works by being manually cloned in Context#typeComparer whenever Context notices that TypeComparer#ctx is different from itself. Unlike TypeComparer, SmartGADTMap keeps its own internal variables, so we cannot apply the same trick. --- .../tools/dotc/core/ConstraintHandling.scala | 46 +++++++++---------- .../src/dotty/tools/dotc/core/Contexts.scala | 31 +++++-------- .../dotty/tools/dotc/core/TypeComparer.scala | 21 +++++---- 3 files changed, 48 insertions(+), 50 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 75785ee4d9ab..e8e7b534dc3e 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -18,15 +18,15 @@ import config.Printers.{constr, typr} * By comparison: Constraint handlers are parts of type comparers and can use their functionality. * Constraint handlers update the current constraint as a side effect. */ -trait ConstraintHandling { +trait ConstraintHandling[AbstractContext] { def constr_println(msg: => String): Unit = constr.println(msg) def typr_println(msg: => String): Unit = typr.println(msg) - implicit def ctx: Context + implicit def ctx(implicit ac: AbstractContext): Context - protected def isSubType(tp1: Type, tp2: Type): Boolean - protected def isSameType(tp1: Type, tp2: Type): Boolean + protected def isSubType(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Boolean + protected def isSameType(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Boolean protected def constraint: Constraint protected def constraint_=(c: Constraint): Unit @@ -66,7 +66,7 @@ trait ConstraintHandling { case tp => tp } - protected def addOneBound(param: TypeParamRef, bound: Type, isUpper: Boolean): Boolean = + protected def addOneBound(param: TypeParamRef, bound: Type, isUpper: Boolean)(implicit actx: AbstractContext): Boolean = !constraint.contains(param) || { def occursIn(bound: Type): Boolean = { val b = bound.dealias @@ -116,7 +116,7 @@ trait ConstraintHandling { private def location(implicit ctx: Context) = "" // i"in ${ctx.typerState.stateChainStr}" // use for debugging - protected def addUpperBound(param: TypeParamRef, bound: Type): Boolean = { + protected def addUpperBound(param: TypeParamRef, bound: Type)(implicit actx: AbstractContext): Boolean = { def description = i"constraint $param <: $bound to\n$constraint" if (bound.isRef(defn.NothingClass) && ctx.typerState.isGlobalCommittable) { def msg = s"!!! instantiated to Nothing: $param, constraint = ${constraint.show}" @@ -132,7 +132,7 @@ trait ConstraintHandling { res } - protected def addLowerBound(param: TypeParamRef, bound: Type): Boolean = { + protected def addLowerBound(param: TypeParamRef, bound: Type)(implicit actx: AbstractContext): Boolean = { def description = i"constraint $param >: $bound to\n$constraint" constr_println(i"adding $description") val upper = constraint.upper(param) @@ -143,7 +143,7 @@ trait ConstraintHandling { res } - protected def addLess(p1: TypeParamRef, p2: TypeParamRef): Boolean = { + protected def addLess(p1: TypeParamRef, p2: TypeParamRef)(implicit actx: AbstractContext): Boolean = { def description = i"ordering $p1 <: $p2 to\n$constraint" val res = if (constraint.isLess(p2, p1)) unify(p2, p1) @@ -164,7 +164,7 @@ trait ConstraintHandling { /** Make p2 = p1, transfer all bounds of p2 to p1 * @pre less(p1)(p2) */ - private def unify(p1: TypeParamRef, p2: TypeParamRef): Boolean = { + private def unify(p1: TypeParamRef, p2: TypeParamRef)(implicit actx: AbstractContext): Boolean = { constr_println(s"unifying $p1 $p2") assert(constraint.isLess(p1, p2)) val down = constraint.exclusiveLower(p2, p1) @@ -179,7 +179,7 @@ trait ConstraintHandling { } - protected def isSubType(tp1: Type, tp2: Type, whenFrozen: Boolean): Boolean = { + protected def isSubType(tp1: Type, tp2: Type, whenFrozen: Boolean)(implicit actx: AbstractContext): Boolean = { if (whenFrozen) isSubTypeWhenFrozen(tp1, tp2) else @@ -198,13 +198,13 @@ trait ConstraintHandling { } } - final def isSubTypeWhenFrozen(tp1: Type, tp2: Type): Boolean = inFrozenConstraint(isSubType(tp1, tp2)) - final def isSameTypeWhenFrozen(tp1: Type, tp2: Type): Boolean = inFrozenConstraint(isSameType(tp1, tp2)) + final def isSubTypeWhenFrozen(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Boolean = inFrozenConstraint(isSubType(tp1, tp2)) + final def isSameTypeWhenFrozen(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Boolean = inFrozenConstraint(isSameType(tp1, tp2)) /** Test whether the lower bounds of all parameters in this * constraint are a solution to the constraint. */ - protected final def isSatisfiable: Boolean = + protected final def isSatisfiable(implicit actx: AbstractContext): Boolean = constraint.forallParams { param => val TypeBounds(lo, hi) = constraint.entry(param) isSubType(lo, hi) || { @@ -223,7 +223,7 @@ trait ConstraintHandling { * @return the instantiating type * @pre `param` is in the constraint's domain. */ - final def approximation(param: TypeParamRef, fromBelow: Boolean): Type = { + final def approximation(param: TypeParamRef, fromBelow: Boolean)(implicit actx: AbstractContext): Type = { val avoidParam = new TypeMap { override def stopAtStatic = true def avoidInArg(arg: Type): Type = @@ -277,7 +277,7 @@ trait ConstraintHandling { * 2. If `tp` is a union type, yet upper bound is not a union type, * approximate the union type from above by an intersection of all common base types. */ - def widenInferred(tp: Type, bound: Type): Type = { + def widenInferred(tp: Type, bound: Type)(implicit actx: AbstractContext): Type = { def isMultiSingleton(tp: Type): Boolean = tp.stripAnnots match { case tp: SingletonType => true case AndType(tp1, tp2) => isMultiSingleton(tp1) | isMultiSingleton(tp2) @@ -310,7 +310,7 @@ trait ConstraintHandling { * a lower bound instantiation can be a singleton type only if the upper bound * is also a singleton type. */ - def instanceType(param: TypeParamRef, fromBelow: Boolean): Type = { + def instanceType(param: TypeParamRef, fromBelow: Boolean)(implicit actx: AbstractContext): Type = { val inst = approximation(param, fromBelow).simplified if (fromBelow) widenInferred(inst, constraint.fullUpperBound(param)) else inst } @@ -325,7 +325,7 @@ trait ConstraintHandling { * Both `c1` and `c2` are required to derive from constraint `pre`, possibly * narrowing it with further bounds. */ - protected final def subsumes(c1: Constraint, c2: Constraint, pre: Constraint): Boolean = + protected final def subsumes(c1: Constraint, c2: Constraint, pre: Constraint)(implicit actx: AbstractContext): Boolean = if (c2 eq pre) true else if (c1 eq pre) false else { @@ -339,7 +339,7 @@ trait ConstraintHandling { } /** The current bounds of type parameter `param` */ - def bounds(param: TypeParamRef): TypeBounds = { + def bounds(param: TypeParamRef)(implicit actx: AbstractContext): TypeBounds = { val e = constraint.entry(param) if (e.exists) e.bounds else { @@ -353,7 +353,7 @@ trait ConstraintHandling { * and propagate all bounds. * @param tvars See Constraint#add */ - def addToConstraint(tl: TypeLambda, tvars: List[TypeVar]): Boolean = + def addToConstraint(tl: TypeLambda, tvars: List[TypeVar])(implicit actx: AbstractContext): Boolean = checkPropagated(i"initialized $tl") { constraint = constraint.add(tl, tvars) tl.paramRefs.forall { param => @@ -381,7 +381,7 @@ trait ConstraintHandling { * This holds if `TypeVarsMissContext` is set unless `param` is a part * of a MatchType that is currently normalized. */ - final def assumedTrue(param: TypeParamRef): Boolean = + final def assumedTrue(param: TypeParamRef)(implicit actx: AbstractContext): Boolean = ctx.mode.is(Mode.TypevarsMissContext) && (caseLambda `ne` param.binder) /** Add constraint `param <: bound` if `fromBelow` is false, `param >: bound` otherwise. @@ -391,7 +391,7 @@ trait ConstraintHandling { * not be AndTypes and lower bounds may not be OrTypes. This is assured by the * way isSubType is organized. */ - protected def addConstraint(param: TypeParamRef, bound: Type, fromBelow: Boolean): Boolean = { + protected def addConstraint(param: TypeParamRef, bound: Type, fromBelow: Boolean)(implicit actx: AbstractContext): Boolean = { def description = i"constr $param ${if (fromBelow) ">:" else "<:"} $bound:\n$constraint" //checkPropagated(s"adding $description")(true) // DEBUG in case following fails checkPropagated(s"added $description") { @@ -507,7 +507,7 @@ trait ConstraintHandling { } /** Instantiate `param` to `tp` if the constraint stays satisfiable */ - protected def tryInstantiate(param: TypeParamRef, tp: Type): Boolean = { + protected def tryInstantiate(param: TypeParamRef, tp: Type)(implicit actx: AbstractContext): Boolean = { val saved = constraint constraint = if (addConstraint(param, tp, fromBelow = true) && @@ -517,7 +517,7 @@ trait ConstraintHandling { } /** Check that constraint is fully propagated. See comment in Config.checkConstraintsPropagated */ - def checkPropagated(msg: => String)(result: Boolean): Boolean = { + def checkPropagated(msg: => String)(result: Boolean)(implicit actx: AbstractContext): Boolean = { if (Config.checkConstraintsPropagated && result && addConstraintInvocations == 0) { inFrozenConstraint { for (p <- constraint.domainParams) { diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 3db26347b1de..35523dfbd8a9 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -723,7 +723,7 @@ object Contexts { private[this] var reverseMapping: SimpleIdentityMap[TypeParamRef, Symbol], private[this] var boundCache: SimpleIdentityMap[Symbol, TypeBounds], private[this] var dirtyFlag: Boolean - ) extends GADTMap with ConstraintHandling { + ) extends GADTMap with ConstraintHandling[Context] { import dotty.tools.dotc.config.Printers.{gadts, gadtsConstr} def this() = this( @@ -748,20 +748,13 @@ object Contexts { private[this] var checkInProgress = false - // TODO: clean up this dirty kludge - private[this] var myCtx: Context = null - implicit override def ctx = myCtx - @forceInline private[this] final def inCtx[T](_ctx: Context)(op: => T) = { - val savedCtx = myCtx - myCtx = _ctx - try op finally myCtx = savedCtx - } + implicit override def ctx(implicit ctx: Context): Context = ctx override protected def constraint = myConstraint override protected def constraint_=(c: Constraint) = myConstraint = c - override def isSubType(tp1: Type, tp2: Type): Boolean = ctx.typeComparer.isSubType(tp1, tp2) - override def isSameType(tp1: Type, tp2: Type): Boolean = ctx.typeComparer.isSameType(tp1, tp2) + override def isSubType(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = ctx.typeComparer.isSubType(tp1, tp2) + override def isSameType(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = ctx.typeComparer.isSameType(tp1, tp2) private[this] def tvar(sym: Symbol)(implicit ctx: Context): TypeVar = { mapping(sym) match { @@ -788,7 +781,7 @@ object Contexts { override def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit = tvar(sym) - override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = try inCtx(ctx) { + override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = try { dirtyFlag = true checkInProgress = true @annotation.tailrec def stripInst(tp: Type): Type = tp match { @@ -799,8 +792,8 @@ object Contexts { } def cautiousSubtype(tp1: Type, tp2: Type, isSubtype: Boolean): Boolean = { - val externalizedTp1 = (new TypeVarRemovingMap)(tp1) - val externalizedTp2 = (new TypeVarRemovingMap)(tp2) + val externalizedTp1 = (new TypeVarRemovingMap()(ctx))(tp1) + val externalizedTp2 = (new TypeVarRemovingMap()(ctx))(tp2) def descr = { def op = s"frozen_${if (isSubtype) "<:<" else ">:>"}" @@ -846,7 +839,7 @@ object Contexts { constraint = constraint.updateEntry(tv.origin, tp) } - val tvarBound = (new TypeVarInsertingMap)(bound) + val tvarBound = (new TypeVarInsertingMap()(ctx))(bound) val res = tvarBound match { case boundTvar: TypeVar => doAddBound(boundTvar) @@ -861,13 +854,13 @@ object Contexts { res } finally checkInProgress = false - override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = inCtx(ctx) { + override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = { mapping(sym) match { case null => null case tv => def retrieveBounds: TypeBounds = { val tb = constraint.fullBounds(tv.origin) - (new TypeVarRemovingMap)(tb).asInstanceOf[TypeBounds] + (new TypeVarRemovingMap()(ctx))(tb).asInstanceOf[TypeBounds] } val res = if (checkInProgress || ctx.mode.is(Mode.GADTflexible)) retrieveBounds @@ -900,7 +893,7 @@ object Contexts { dirtyFlag ) - private final class TypeVarInsertingMap extends TypeMap { + private final class TypeVarInsertingMap(implicit ctx: Context) extends TypeMap { override def apply(tp: Type): Type = tp match { case tp: TypeRef => val sym = tp.typeSymbol @@ -910,7 +903,7 @@ object Contexts { } } - private final class TypeVarRemovingMap extends TypeMap { + private final class TypeVarRemovingMap(implicit ctx: Context) extends TypeMap { override def apply(tp: Type): Type = tp match { case tpr: TypeParamRef => reverseMapping(tpr) match { diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 912deda62e04..0327614d70e5 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -17,11 +17,16 @@ import scala.util.control.NonFatal import typer.ProtoTypes.constrained import reporting.trace +final class AbsentContext +object AbsentContext { + implicit val absentContext: AbsentContext = new AbsentContext +} + /** Provides methods to compare types. */ -class TypeComparer(initctx: Context) extends ConstraintHandling { +class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] { import TypeComparer._ - implicit val ctx: Context = initctx + implicit def ctx(implicit nc: AbsentContext): Context = initctx val state = ctx.typerState def constraint: Constraint = state.constraint @@ -138,7 +143,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { finally this.approx = saved } - def isSubType(tp1: Type, tp2: Type): Boolean = isSubType(tp1, tp2, NoApprox) + def isSubType(tp1: Type, tp2: Type)(implicit nc: AbsentContext): Boolean = isSubType(tp1, tp2, NoApprox) protected def recur(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)} $approx", subtyping) { @@ -185,7 +190,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { def firstTry: Boolean = tp2 match { case tp2: NamedType => def compareNamed(tp1: Type, tp2: NamedType): Boolean = { - implicit val ctx = this.ctx + implicit val ctx: Context = this.ctx tp2.info match { case info2: TypeAlias => recur(tp1, info2.alias) case _ => tp1 match { @@ -1323,7 +1328,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling { // Type equality =:= /** Two types are the same if are mutual subtypes of each other */ - def isSameType(tp1: Type, tp2: Type): Boolean = + def isSameType(tp1: Type, tp2: Type)(implicit nc: AbsentContext): Boolean = if (tp1 eq NoType) false else if (tp1 eq tp2) true else isSubType(tp1, tp2) && isSubType(tp2, tp1) @@ -1844,12 +1849,12 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { val footprint: mutable.Set[Type] = mutable.Set[Type]() - override def bounds(param: TypeParamRef): TypeBounds = { + override def bounds(param: TypeParamRef)(implicit nc: AbsentContext): TypeBounds = { if (param.binder `ne` caseLambda) footprint += param super.bounds(param) } - override def addOneBound(param: TypeParamRef, bound: Type, isUpper: Boolean): Boolean = { + override def addOneBound(param: TypeParamRef, bound: Type, isUpper: Boolean)(implicit nc: AbsentContext): Boolean = { if (param.binder `ne` caseLambda) footprint += param super.addOneBound(param, bound, isUpper) } @@ -1960,7 +1965,7 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) { super.glb(tp1, tp2) } - override def addConstraint(param: TypeParamRef, bound: Type, fromBelow: Boolean): Boolean = + override def addConstraint(param: TypeParamRef, bound: Type, fromBelow: Boolean)(implicit nc: AbsentContext): Boolean = traceIndented(i"add constraint $param ${if (fromBelow) ">:" else "<:"} $bound $frozenConstraint, constraint = ${ctx.typerState.constraint}") { super.addConstraint(param, bound, fromBelow) } From 3084bf9b78ccbecc4df3d8a362f96f2722cb26e5 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Thu, 22 Nov 2018 11:30:20 +0100 Subject: [PATCH 18/21] Add test showing injectivity issue --- tests/gadt-neg/uninjectivity.scala | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/gadt-neg/uninjectivity.scala diff --git a/tests/gadt-neg/uninjectivity.scala b/tests/gadt-neg/uninjectivity.scala new file mode 100644 index 000000000000..f1d0fc59000a --- /dev/null +++ b/tests/gadt-neg/uninjectivity.scala @@ -0,0 +1,24 @@ +object uninjectivity { + sealed trait EQ[A, B] + final case class Refl[T]() extends EQ[T, T] + + def absurd1[F[_], X, Y](eq: EQ[F[X], F[Y]], x: X): Y = eq match { + case Refl() => + x // should be an error + } + + def absurd2[F[_], G[_]](eq: EQ[F[Int], G[Int]], fi: F[Int], fs: F[String]): G[Int] = eq match { + case Refl() => + val gs: G[String] = fs // error + // fi + ??? + } + + def absurd3[F[_], G[_], X, Y](eq: EQ[F[X], G[Y]], fx: F[X]): G[Y] = eq match { + case Refl() => + val gx: G[X] = fx // error + val fy: F[Y] = fx // error + // fx + ??? + } +} From b749b0f7439dc8a6eda2a9bc42be6de4858e3798 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Thu, 22 Nov 2018 12:35:15 +0100 Subject: [PATCH 19/21] Clean up SmartGADTMap#addBound --- .../src/dotty/tools/dotc/core/Contexts.scala | 40 +++++++------------ 1 file changed, 15 insertions(+), 25 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 35523dfbd8a9..0c40ff4966c4 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -811,6 +811,11 @@ object Contexts { res } + def unify(tv: TypeVar, tp: Type): Unit = { + gadts.println(i"manually unifying $tv with $tp") + constraint = constraint.updateEntry(tv.origin, tp) + } + val symTvar: TypeVar = stripInst(tvar(sym)) match { case tv: TypeVar => tv case inst => @@ -819,37 +824,22 @@ object Contexts { return true } - def doAddBound(bound: Type): Boolean = { - val res = stripInst(bound) match { - case boundTvar: TypeVar => - if (boundTvar eq symTvar) true - else if (isUpper) addLess(symTvar.origin, boundTvar.origin) - else addLess(boundTvar.origin, symTvar.origin) - case bound => - if (cautiousSubtype(symTvar, bound, isSubtype = !isUpper)) { unify(symTvar, bound); true } - else if (isUpper) addUpperBound(symTvar.origin, bound) - else addLowerBound(symTvar.origin, bound) - } - - res - } - - def unify(tv: TypeVar, tp: Type): Unit = { - gadts.println(i"manually unifying $tv with $tp") - constraint = constraint.updateEntry(tv.origin, tp) - } - - val tvarBound = (new TypeVarInsertingMap()(ctx))(bound) - val res = tvarBound match { + val internalizedBound = (new TypeVarInsertingMap()(ctx))(bound) + val res = stripInst(internalizedBound) match { case boundTvar: TypeVar => - doAddBound(boundTvar) - case tp => doAddBound(tp) + if (boundTvar eq symTvar) true + else if (isUpper) addLess(symTvar.origin, boundTvar.origin) + else addLess(boundTvar.origin, symTvar.origin) + case bound => + if (cautiousSubtype(symTvar, bound, isSubtype = !isUpper)) { unify(symTvar, bound); true } + else if (isUpper) addUpperBound(symTvar.origin, bound) + else addLowerBound(symTvar.origin, bound) } gadts.println { val descr = if (isUpper) "upper" else "lower" val op = if (isUpper) "<:" else ">:" - i"adding $descr bound $sym $op $bound = $res\t( $symTvar $op $tvarBound )" + i"adding $descr bound $sym $op $bound = $res\t( $symTvar $op $internalizedBound )" } res } finally checkInProgress = false From bc92ce88bc0747bb6b945536f789f6f178c4d949 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Thu, 22 Nov 2018 12:42:17 +0100 Subject: [PATCH 20/21] Apply substParam trick to SmartGADTMap TypeMaps Makes the code cleaner and does not allocate for trivial cases. --- .../src/dotty/tools/dotc/core/Contexts.scala | 52 ++++++++++--------- 1 file changed, 27 insertions(+), 25 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 0c40ff4966c4..65d0efee6bb4 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -792,8 +792,8 @@ object Contexts { } def cautiousSubtype(tp1: Type, tp2: Type, isSubtype: Boolean): Boolean = { - val externalizedTp1 = (new TypeVarRemovingMap()(ctx))(tp1) - val externalizedTp2 = (new TypeVarRemovingMap()(ctx))(tp2) + val externalizedTp1 = removeTypeVars(tp1) + val externalizedTp2 = removeTypeVars(tp2) def descr = { def op = s"frozen_${if (isSubtype) "<:<" else ">:>"}" @@ -824,7 +824,7 @@ object Contexts { return true } - val internalizedBound = (new TypeVarInsertingMap()(ctx))(bound) + val internalizedBound = insertTypeVars(bound) val res = stripInst(internalizedBound) match { case boundTvar: TypeVar => if (boundTvar eq symTvar) true @@ -850,7 +850,7 @@ object Contexts { case tv => def retrieveBounds: TypeBounds = { val tb = constraint.fullBounds(tv.origin) - (new TypeVarRemovingMap()(ctx))(tb).asInstanceOf[TypeBounds] + removeTypeVars(tb).asInstanceOf[TypeBounds] } val res = if (checkInProgress || ctx.mode.is(Mode.GADTflexible)) retrieveBounds @@ -883,31 +883,33 @@ object Contexts { dirtyFlag ) + private def insertTypeVars(tp: Type, map: TypeMap = null)(implicit ctx: Context) = tp match { + case tp: TypeRef => + val sym = tp.typeSymbol + if (contains(sym)) tvar(sym) else tp + case _ => + (if (map != null) map else new TypeVarInsertingMap()).mapOver(tp) + } private final class TypeVarInsertingMap(implicit ctx: Context) extends TypeMap { - override def apply(tp: Type): Type = tp match { - case tp: TypeRef => - val sym = tp.typeSymbol - if (contains(sym)) tvar(sym) else tp - case _ => - mapOver(tp) - } + override def apply(tp: Type): Type = insertTypeVars(tp, this) } + private def removeTypeVars(tp: Type, map: TypeMap = null)(implicit ctx: Context) = tp match { + case tpr: TypeParamRef => + reverseMapping(tpr) match { + case null => tpr + case sym => sym.typeRef + } + case tv: TypeVar => + reverseMapping(tv.origin) match { + case null => tv + case sym => sym.typeRef + } + case _ => + (if (map != null) map else new TypeVarRemovingMap()).mapOver(tp) + } private final class TypeVarRemovingMap(implicit ctx: Context) extends TypeMap { - override def apply(tp: Type): Type = tp match { - case tpr: TypeParamRef => - reverseMapping(tpr) match { - case null => tpr - case sym => sym.typeRef - } - case tv: TypeVar => - reverseMapping(tv.origin) match { - case null => tv - case sym => sym.typeRef - } - case _ => - mapOver(tp) - } + override def apply(tp: Type): Type = removeTypeVars(tp, this) } } From 856011ba5876a91f06a983857bd6fbb7560f76b8 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Fri, 7 Dec 2018 12:02:07 +0100 Subject: [PATCH 21/21] Make GADTMap member names clearer --- .../src/dotty/tools/dotc/core/Contexts.scala | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala index 65d0efee6bb4..a306816d9736 100644 --- a/compiler/src/dotty/tools/dotc/core/Contexts.scala +++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala @@ -480,7 +480,7 @@ object Contexts { def setTyper(typer: Typer): this.type = { this.scope = typer.scope; setTypeAssigner(typer) } def setImportInfo(importInfo: ImportInfo): this.type = { this.importInfo = importInfo; this } def setGadt(gadt: GADTMap): this.type = { this.gadt = gadt; this } - def setFreshGADTBounds: this.type = setGadt(gadt.derived) + def setFreshGADTBounds: this.type = setGadt(gadt.fresh) def setSearchHistory(searchHistory: SearchHistory): this.type = { this.searchHistory = searchHistory; this } def setTypeComparerFn(tcfn: Context => TypeComparer): this.type = { this.typeComparer = tcfn(this); this } private def setMoreProperties(moreProperties: Map[Key[Any], Any]): this.type = { this.moreProperties = moreProperties; this } @@ -714,7 +714,7 @@ object Contexts { def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds def contains(sym: Symbol)(implicit ctx: Context): Boolean def debugBoundsDescription(implicit ctx: Context): String - def derived: GADTMap + def fresh: GADTMap } final class SmartGADTMap private ( @@ -746,7 +746,7 @@ object Contexts { sb.result } - private[this] var checkInProgress = false + private[this] var boundAdditionInProgress = false implicit override def ctx(implicit ctx: Context): Context = ctx @@ -783,7 +783,7 @@ object Contexts { override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = try { dirtyFlag = true - checkInProgress = true + boundAdditionInProgress = true @annotation.tailrec def stripInst(tp: Type): Type = tp match { case tv: TypeVar => val inst = instType(tv) @@ -842,7 +842,7 @@ object Contexts { i"adding $descr bound $sym $op $bound = $res\t( $symTvar $op $internalizedBound )" } res - } finally checkInProgress = false + } finally boundAdditionInProgress = false override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = { mapping(sym) match { @@ -853,7 +853,7 @@ object Contexts { removeTypeVars(tb).asInstanceOf[TypeBounds] } val res = - if (checkInProgress || ctx.mode.is(Mode.GADTflexible)) retrieveBounds + if (boundAdditionInProgress || ctx.mode.is(Mode.GADTflexible)) retrieveBounds else { if (dirtyFlag) { dirtyFlag = false @@ -875,7 +875,7 @@ object Contexts { override def contains(sym: Symbol)(implicit ctx: Context): Boolean = mapping(sym) ne null - override def derived: GADTMap = new SmartGADTMap( + override def fresh: GADTMap = new SmartGADTMap( myConstraint, mapping, reverseMapping, @@ -919,6 +919,6 @@ object Contexts { override def bounds(sym: Symbol)(implicit ctx: Context): TypeBounds = null override def contains(sym: Symbol)(implicit ctx: Context) = false override def debugBoundsDescription(implicit ctx: Context): String = "EmptyGADTMap" - override def derived = new SmartGADTMap + override def fresh = new SmartGADTMap } }