From 16554c0efe2d09ab3ef760522f0811a964f7ee84 Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Thu, 11 Dec 2014 18:47:18 +0100 Subject: Fixed #264 - failure to typecheck GADTs The previous scheme derived the right bounds, but then failed to use them because a TypeRef already has a set info (its bounds). Changing the bounds in the symbol by a side effect does not affect that. This is good! But it showed that the previous scheme was too fragile because it used a sneaky side effect when updating the symbol info which failed to propgate into the cached info in TypeRef. We now keep GADT computed bounds separate form the symbol info in a map `gadt` in the current context. --- src/dotty/tools/dotc/core/Contexts.scala | 10 ++++++++++ src/dotty/tools/dotc/core/Flags.scala | 5 +---- src/dotty/tools/dotc/core/Symbols.scala | 25 ----------------------- src/dotty/tools/dotc/core/TypeComparer.scala | 22 ++++++++++++-------- src/dotty/tools/dotc/typer/Typer.scala | 30 ++++++++++++++++++++-------- 5 files changed, 47 insertions(+), 45 deletions(-) (limited to 'src/dotty/tools') diff --git a/src/dotty/tools/dotc/core/Contexts.scala b/src/dotty/tools/dotc/core/Contexts.scala index 805b7660c..2477fd4a4 100644 --- a/src/dotty/tools/dotc/core/Contexts.scala +++ b/src/dotty/tools/dotc/core/Contexts.scala @@ -146,6 +146,11 @@ object Contexts { protected def diagnostics_=(diagnostics: Option[StringBuilder]) = _diagnostics = diagnostics def diagnostics: Option[StringBuilder] = _diagnostics + /** The current bounds in force for type parameters appearing in a GADT */ + private var _gadt: GADTMap = _ + protected def gadt_=(gadt: GADTMap) = _gadt = gadt + def gadt: GADTMap = _gadt + /** A map in which more contextual properties can be stored */ private var _moreProperties: Map[String, Any] = _ protected def moreProperties_=(moreProperties: Map[String, Any]) = _moreProperties = moreProperties @@ -418,6 +423,8 @@ object Contexts { def setSetting[T](setting: Setting[T], value: T): this.type = setSettings(setting.updateIn(sstate, value)) + def setFreshGADTBounds: this.type = { this.gadt = new GADTMap(gadt.bounds); this } + def setDebug = setSetting(base.settings.debug, true) } @@ -439,6 +446,7 @@ object Contexts { moreProperties = Map.empty typeComparer = new TypeComparer(this) searchHistory = new SearchHistory(0, Map()) + gadt = new GADTMap(SimpleMap.Empty) } object NoContext extends Context { @@ -593,6 +601,8 @@ object Contexts { implicit val ctx: Context = initctx } + class GADTMap(var bounds: SimpleMap[Symbol, TypeBounds]) + /** Initial size of superId table */ private final val InitialSuperIdsSize = 4096 diff --git a/src/dotty/tools/dotc/core/Flags.scala b/src/dotty/tools/dotc/core/Flags.scala index 0e86a2936..53beae838 100644 --- a/src/dotty/tools/dotc/core/Flags.scala +++ b/src/dotty/tools/dotc/core/Flags.scala @@ -301,9 +301,6 @@ object Flags { /** Method is assumed to be stable */ final val Stable = termFlag(24, "") - /** Info can be refined during GADT pattern match */ - final val GADTFlexType = typeFlag(24, "") - /** A case parameter accessor */ final val CaseAccessor = termFlag(25, "") @@ -553,7 +550,7 @@ object Flags { /** A Java interface, potentially with default methods */ final val JavaTrait = allOf(JavaDefined, Trait, NoInits) - + /** A Java interface */ final val JavaInterface = allOf(JavaDefined, Trait) diff --git a/src/dotty/tools/dotc/core/Symbols.scala b/src/dotty/tools/dotc/core/Symbols.scala index 9be75c11a..2be97691f 100644 --- a/src/dotty/tools/dotc/core/Symbols.scala +++ b/src/dotty/tools/dotc/core/Symbols.scala @@ -450,31 +450,6 @@ object Symbols { */ def pos: Position = if (coord.isPosition) coord.toPosition else NoPosition -// -------- GADT handling ----------------------------------------------- - - /** Perform given operation `op` where this symbol allows tightening of - * its type bounds. - */ - private[dotc] def withGADTFlexType[T](op: () => T)(implicit ctx: Context): () => T = { () => - assert((denot is TypeParam) && denot.owner.isTerm) - val saved = denot - denot = denot.copySymDenotation(initFlags = denot.flags | GADTFlexType) - try op() - finally denot = saved - } - - /** Disallow tightening of type bounds for this symbol from now on */ - private[dotc] def resetGADTFlexType()(implicit ctx: Context): Unit = { - assert(denot is GADTFlexType) - denot = denot.copySymDenotation(initFlags = denot.flags &~ GADTFlexType) - } - - /** Change info of this symbol to new, tightened type bounds */ - private[core] def changeGADTInfo(bounds: TypeBounds)(implicit ctx: Context): Unit = { - assert(denot is GADTFlexType) - denot = denot.copySymDenotation(info = bounds) - } - // -------- Printing -------------------------------------------------------- /** The prefix string to be used when displaying this symbol without denotation */ diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala index 42af31553..5cb384361 100644 --- a/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/src/dotty/tools/dotc/core/TypeComparer.scala @@ -617,9 +617,12 @@ class TypeComparer(initctx: Context) extends DotClass { secondTry(OrType.make(derivedRef(tp11), derivedRef(tp12)), tp2) */ case TypeBounds(lo1, hi1) => - if ((ctx.mode is Mode.GADTflexible) && (tp1.symbol is GADTFlexType) && - !isSubTypeWhenFrozen(hi1, tp2)) - trySetType(tp1, TypeBounds(lo1, hi1 & tp2)) + val gbounds1 = ctx.gadt.bounds(tp1.symbol) + if (gbounds1 != null) + isSubTypeWhenFrozen(gbounds1.hi, tp2) || + (ctx.mode is Mode.GADTflexible) && + narrowGADTBounds(tp1, TypeBounds(gbounds1.lo, gbounds1.hi & tp2)) || + tryRebase2nd else if (lo1 eq hi1) isSubType(hi1, tp2) else tryRebase2nd case _ => @@ -636,9 +639,12 @@ class TypeComparer(initctx: Context) extends DotClass { } def compareNamed: Boolean = tp2.info match { case TypeBounds(lo2, hi2) => - if ((ctx.mode is Mode.GADTflexible) && (tp2.symbol is GADTFlexType) && - !isSubTypeWhenFrozen(tp1, lo2)) - trySetType(tp2, TypeBounds(lo2 | tp1, hi2)) + val gbounds2 = ctx.gadt.bounds(tp2.symbol) + if (gbounds2 != null) + isSubTypeWhenFrozen(tp1, gbounds2.lo) || + (ctx.mode is Mode.GADTflexible) && + narrowGADTBounds(tp2, TypeBounds(gbounds2.lo | tp1, gbounds2.hi)) || + tryRebase3rd else ((frozenConstraint || !isCappable(tp1)) && isSubType(tp1, lo2) || tryRebase3rd) @@ -911,9 +917,9 @@ class TypeComparer(initctx: Context) extends DotClass { tp.exists && !tp.isLambda } - def trySetType(tr: NamedType, bounds: TypeBounds): Boolean = + def narrowGADTBounds(tr: NamedType, bounds: TypeBounds): Boolean = isSubType(bounds.lo, bounds.hi) && - { tr.symbol.changeGADTInfo(bounds); true } + { ctx.gadt.bounds = ctx.gadt.bounds.updated(tr.symbol, bounds); true } // Tests around `matches` diff --git a/src/dotty/tools/dotc/typer/Typer.scala b/src/dotty/tools/dotc/typer/Typer.scala index f6027165b..624a86c1c 100644 --- a/src/dotty/tools/dotc/typer/Typer.scala +++ b/src/dotty/tools/dotc/typer/Typer.scala @@ -628,10 +628,10 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit def typedCases(cases: List[untpd.CaseDef], selType: Type, pt: Type)(implicit ctx: Context) = { /** gadtSyms = "all type parameters of enclosing methods that appear - * non-variantly in the selector type" todo: should typevars - * which appear with variances +1 and -1 (in different - * places) be considered as well? - */ + * non-variantly in the selector type" todo: should typevars + * which appear with variances +1 and -1 (in different + * places) be considered as well? + */ val gadtSyms: Set[Symbol] = ctx.traceIndented(i"GADT syms of $selType", gadts) { val accu = new TypeAccumulator[Set[Symbol]] { def apply(tsyms: Set[Symbol], t: Type): Set[Symbol] = { @@ -650,9 +650,13 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit cases mapconserve (typedCase(_, pt, selType, gadtSyms)) } + /** Type a case. Overridden in ReTyper, that's why it's separate from + * typedCases. + */ def typedCase(tree: untpd.CaseDef, pt: Type, selType: Type, gadtSyms: Set[Symbol])(implicit ctx: Context): CaseDef = track("typedCase") { + val originalCtx = ctx + def caseRest(pat: Tree)(implicit ctx: Context) = { - gadtSyms foreach (_.resetGADTFlexType) pat foreachSubTree { case b: Bind => if (ctx.scope.lookup(b.name) == NoSymbol) ctx.enter(b.symbol) @@ -661,11 +665,21 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit } val guard1 = typedExpr(tree.guard, defn.BooleanType) val body1 = typedExpr(tree.body, pt) + .ensureConforms(pt)(originalCtx) // insert a cast if body does not conform to expected type if we disregard gadt bounds assignType(cpy.CaseDef(tree)(pat, guard1, body1), body1) } - val doCase: () => CaseDef = - () => caseRest(typedPattern(tree.pat, selType))(ctx.fresh.setNewScope) - (doCase /: gadtSyms)((op, tsym) => tsym.withGADTFlexType(op))() + + val gadtCtx = + if (gadtSyms.isEmpty) ctx + else { + val c = ctx.fresh.setFreshGADTBounds + for (sym <- gadtSyms) + if (!c.gadt.bounds.contains(sym)) + c.gadt.bounds = c.gadt.bounds.updated(sym, TypeBounds.empty) + c + } + val pat1 = typedPattern(tree.pat, selType)(gadtCtx) + caseRest(pat1)(gadtCtx.fresh.setNewScope) } def typedReturn(tree: untpd.Return)(implicit ctx: Context): Return = track("typedReturn") { -- cgit v1.2.3