WIP: Constraint-based GADT reasoning

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) {