Gadt unification

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

compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala

@@ -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
 
@@ -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
@@ -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)
@@ -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)
@@ -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
@@ -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) || {
@@ -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 =
@@ -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")
@@ -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)
@@ -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
  }
@@ -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 {
@@ -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 {
@@ -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 =>
@@ -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 _ =>
@@ -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.
@@ -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") {
@@ -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) &&
@@ -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) {