Skip to content

Gadt unification #5611

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 8 commits into from
Dec 17, 2018
Merged

Gadt unification #5611

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
225aabc
Revert "Handle higher-kinded GADT bounds"
abgruszecki Dec 14, 2018
08ac0a0
Move TyperState.instType
abgruszecki Dec 14, 2018
04503d9
Allow overriding ConstraintHandling logs
abgruszecki Dec 14, 2018
4c41fc4
Reuse ConstraintHandling for GADTMap
abgruszecki Dec 14, 2018
de795a9
Add caching to GADTMap
abgruszecki Dec 14, 2018
6cca0a6
Clean up GADTMap#ctx
abgruszecki Dec 14, 2018
f75f58f
Address review comments
abgruszecki Dec 16, 2018
d1fa5d7
Simplify TypeComparer.explaining
abgruszecki Dec 17, 2018
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
1 change: 1 addition & 0 deletions compiler/src/dotty/tools/dotc/config/Printers.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
84 changes: 50 additions & 34 deletions compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,15 +18,18 @@ 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] {

implicit val ctx: Context
def constr_println(msg: => String): Unit = constr.println(msg)
def typr_println(msg: => String): Unit = typr.println(msg)

protected def isSubType(tp1: Type, tp2: Type): Boolean
protected def isSameType(tp1: Type, tp2: Type): Boolean
implicit def ctx(implicit ac: AbstractContext): Context

val state: TyperState
import state.constraint
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

private[this] var addConstraintInvocations = 0

Expand All @@ -50,7 +53,20 @@ trait ConstraintHandling {
*/
protected var comparedTypeLambdas: Set[TypeLambda] = Set.empty

protected def addOneBound(param: TypeParamRef, bound: Type, isUpper: Boolean): Boolean =
/** 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)(implicit actx: AbstractContext): Boolean =
!constraint.contains(param) || {
def occursIn(bound: Type): Boolean = {
val b = bound.dealias
Expand Down Expand Up @@ -100,34 +116,34 @@ 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}"
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 = {
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")
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
}

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)
Expand All @@ -136,20 +152,20 @@ 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
}

/** Make p2 = p1, transfer all bounds of p2 to p1
* @pre less(p1)(p2)
*/
private def unify(p1: TypeParamRef, p2: TypeParamRef): Boolean = {
constr.println(s"unifying $p1 $p2")
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)
val up = constraint.exclusiveUpper(p1, p2)
Expand All @@ -163,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
Expand All @@ -182,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) || {
Expand All @@ -207,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 =
Expand Down Expand Up @@ -247,7 +263,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")
Expand All @@ -261,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)
Expand Down Expand Up @@ -294,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
}
Expand All @@ -309,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 {
Expand All @@ -323,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 {
Expand All @@ -337,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 =>
Expand All @@ -346,7 +362,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 _ =>
Expand All @@ -365,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.
Expand All @@ -375,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") {
Expand Down Expand Up @@ -491,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) &&
Expand All @@ -501,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) {
Expand Down
Loading