Skip to content

Fixed #264 - failure to typecheck GADTs #271

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Dec 19, 2014
Merged

Fixed #264 - failure to typecheck GADTs #271

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
16554c0
Fixed #264 - failure to typecheck GADTs
odersky Dec 11, 2014
009a1e6
Made gadt map better encapsulated.
odersky Dec 16, 2014
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 15 additions & 0 deletions src/dotty/tools/dotc/core/Contexts.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This encaspulates the ability to assign a new map, but leaves the door open for anyone to mutate GADTMap#bounds.

I'd prefer to see something like:

class GADTMap {
  private var bounds = new SimpleMap
  def narrowBounds(sym: Symbol, bounds: TypeBounds): Unit = {
    bounds = bounds.updated(symbol, bounds)
  }
  def apply(sym: Symbol): TypeBounds = bounds(sym)
}


/** 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
Expand Down Expand Up @@ -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)
}

Expand All @@ -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 {
Expand Down Expand Up @@ -593,6 +601,13 @@ object Contexts {
implicit val ctx: Context = initctx
}

class GADTMap(initBounds: SimpleMap[Symbol, TypeBounds]) {
private var myBounds = initBounds
def setBounds(sym: Symbol, b: TypeBounds): Unit =
myBounds = myBounds.updated(sym, b)
def bounds = myBounds
}

/** Initial size of superId table */
private final val InitialSuperIdsSize = 4096

Expand Down
5 changes: 1 addition & 4 deletions src/dotty/tools/dotc/core/Flags.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -301,9 +301,6 @@ object Flags {
/** Method is assumed to be stable */
final val Stable = termFlag(24, "<stable>")

/** Info can be refined during GADT pattern match */
final val GADTFlexType = typeFlag(24, "<gadt-flex-type>")

/** A case parameter accessor */
final val CaseAccessor = termFlag(25, "<caseaccessor>")

Expand Down Expand Up @@ -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)

Expand Down
25 changes: 0 additions & 25 deletions src/dotty/tools/dotc/core/Symbols.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand Down
22 changes: 14 additions & 8 deletions src/dotty/tools/dotc/core/TypeComparer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ =>
Expand All @@ -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)
Expand Down Expand Up @@ -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.setBounds(tr.symbol, bounds); true }

// Tests around `matches`

Expand Down
30 changes: 22 additions & 8 deletions src/dotty/tools/dotc/typer/Typer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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] = {
Expand All @@ -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)
Expand All @@ -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.setBounds(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") {
Expand Down
15 changes: 15 additions & 0 deletions tests/pos/i0268.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
package typespatmat

sealed trait Box2[T]
final case class Int2(x: Int) extends Box2[Int]
final case class Str2(x: String)
extends Box2[String]
final case class Gen[T](x: T) extends Box2[T]

object Box2 {
def double2[T](x: Box2[T]): T = x match {
case Int2(i) => i * 2
case Str2(s) => s + s
case Gen(x) => x
}
}