Unified PredicateRefinedType with RefinedType, i.e., made it a subclass and thus shared type traversal / type mapping / pickling logic.

Author: gsps

compiler/src/dotty/tools/dotc/ast/tpd.scala

@@ -146,6 +146,9 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
   def RefinedTypeTree(parent: Tree, refinements: List[Tree], refineCls: ClassSymbol)(implicit ctx: Context): Tree =
     ta.assignType(untpd.RefinedTypeTree(parent, refinements), parent, refinements, refineCls)
 
+  def PredicateTypeTree(subjectVd: ValDef, pred: Tree)(implicit ctx: Context): PredicateTypeTree =
+    ta.assignType(untpd.PredicateTypeTree(subjectVd, pred), subjectVd, pred)
+
   def AppliedTypeTree(tycon: Tree, args: List[Tree])(implicit ctx: Context): AppliedTypeTree =
     ta.assignType(untpd.AppliedTypeTree(tycon, args), tycon, args)
 

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

@@ -365,6 +365,10 @@ object NameKinds {
   val ModuleClassName = new SuffixNameKind(OBJECTCLASS, "$", optInfoString = "ModuleClass")
   val ImplMethName = new SuffixNameKind(IMPLMETH, "$")
   val AdaptedClosureName = new SuffixNameKind(ADAPTEDCLOSURE, "$adapted") { override def definesNewName = true }
+  val PredicateSubjectName = new SuffixNameKind(FIELD, "$subject") {
+    override def definesNewName = true
+    override def mkString(underlying: TermName, info: ThisInfo) = underlying.toString
+  }
 
   /** A name together with a signature. Used in Tasty trees. */
   object SignedName extends NameKind(SIGNED) {

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

@@ -34,6 +34,8 @@ object NameTags extends TastyFormat.NameTags {
   final val IMPLMETH = 30       // Used to define methods in implementation classes
                                 // (can probably be removed).
 
+  final val PREDICATESUBJECT = 31  // Used by PredicateRefinedTypes to encode their predicate subject's name
+
   def nameTagToString(tag: Int): String = tag match {
     case UTF8 => "UTF8"
     case QUALIFIED => "QUALIFIED"

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

@@ -147,7 +147,7 @@ trait Substituters { this: Context =>
           .mapOver(tp)
     }
 
-  final def substRecThis(tp: Type, from: Type, to: Type, theMap: SubstRecThisMap): Type =
+  final def substRecThis(tp: Type, from: RecType, to: Type, theMap: SubstRecThisMap): Type =
     tp match {
       case tp @ RecThis(binder) =>
         if (binder eq from) to else tp
@@ -161,6 +161,20 @@ trait Substituters { this: Context =>
           .mapOver(tp)
     }
 
+  final def substPredicateThis(tp: Type, from: PredicateRefinedType, to: Type, theMap: SubstPredicateThisMap): Type =
+    tp match {
+      case tp @ PredicateThis(binder) =>
+        if (binder eq from) to else tp
+      case tp: NamedType =>
+        if (tp.currentSymbol.isStatic) tp
+        else tp.derivedSelect(substPredicateThis(tp.prefix, from, to, theMap))
+      case _: ThisType | _: BoundType | NoPrefix =>
+        tp
+      case _ =>
+        (if (theMap != null) theMap else new SubstPredicateThisMap(from, to))
+          .mapOver(tp)
+    }
+
   final def substParam(tp: Type, from: ParamRef, to: Type, theMap: SubstParamMap): Type =
     tp match {
       case tp: BoundType =>
@@ -222,10 +236,14 @@ trait Substituters { this: Context =>
     def apply(tp: Type): Type = substThis(tp, from, to, this)
   }
 
-  final class SubstRecThisMap(from: Type, to: Type) extends DeepTypeMap {
+  final class SubstRecThisMap(from: RecType, to: Type) extends DeepTypeMap {
     def apply(tp: Type): Type = substRecThis(tp, from, to, this)
   }
 
+  final class SubstPredicateThisMap(from: PredicateRefinedType, to: Type) extends DeepTypeMap {
+    def apply(tp: Type): Type = substPredicateThis(tp, from, to, this)
+  }
+
   final class SubstParamMap(from: ParamRef, to: Type) extends DeepTypeMap {
     def apply(tp: Type) = substParam(tp, from, to, this)
   }

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

@@ -432,9 +432,10 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
             (name2 == nme.WILDCARD || hasMatchingMember(name2, tp1, tp2))
         }
         def compareRefined: Boolean = {
+          // FIXME(gsps): Does handle case where PredicateRefinedType is skipped via skipMatching below correctly
+          if (tp2.isInstanceOf[PredicateRefinedType])
+            return isPredicateSubType(tp1, tp2.asInstanceOf[PredicateRefinedType])
           val tp1w = tp1.widen
-          if (tp1w.isInstanceOf[RefinedType] && (tp2.refinedName eq nme.PRED))
-            return false  // Would have succeeded one-level up when the types were wrapped in RecTypes
           val skipped2 = skipMatching(tp1w, tp2)
           if ((skipped2 eq tp2) || !Config.fastPathForRefinedSubtype)
             tp1 match {
@@ -1097,18 +1098,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         tp1.parent.asInstanceOf[RefinedType], tp2.parent.asInstanceOf[RefinedType], limit))
   }
 
-  // PredicateType related checking
-
-  protected def isPredicateSubType(tp1: Type, tp2: Type): Boolean = {
-    tp1 match {
-      case PredicateType.Fixed(parent1, pred1) =>
-        tp2 match {
-          case PredicateType.Fixed(parent2, pred2) if parent1 <:< parent2 => true
-          case _ => false
-        }
-      case _ => false
-    }
-  }
+  /* Skips refinement checks for PredicateRefinedTypes -- this is overridden in PreciseTyping. */
+  protected def isPredicateSubType(tp1: Type, tp2: PredicateRefinedType): Boolean =
+//    tp2 match {
+//      case PredicateRefinedType(parent2, pred2) => tp1 <:< parent2
+//      case _ => false
+//    }
+    tp1 <:< tp2.parent
 
   /** A type has been covered previously in subtype checking if it
    *  is some combination of TypeRefs that point to classes, where the
@@ -1547,7 +1543,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     case tp1: RefinedType =>
       tp2 match {
         case tp2: RefinedType if tp1.refinedName == tp2.refinedName =>
-          PredicateType.mergePredicates(tp1, tp2, isAnd = true) orElse {
+          PredicateRefinedType.mergePredicates(tp1, tp2, isAnd = true) orElse {
             tp1.derivedRefinedType(tp1.parent & tp2.parent, tp1.refinedName,
               tp1.refinedInfo & tp2.refinedInfo)
           }
@@ -1587,7 +1583,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     case tp1: AnnotatedType =>
       tp1.underlying | tp2
     case _ =>
-      PredicateType.mergePredicates(tp1, tp2, isAnd = false)
+      PredicateRefinedType.mergePredicates(tp1, tp2, isAnd = false)
   }
 
   /** Show type, handling type types better than the default */

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

@@ -1336,6 +1336,10 @@ object Types {
     final def substRecThis(binder: RecType, tp: Type)(implicit ctx: Context): Type =
       ctx.substRecThis(this, binder, tp, null)
 
+    /** Substitute all occurrences of `PredicateThis(binder)` by `tp` */
+    final def substPredicateThis(binder: PredicateRefinedType, tp: Type)(implicit ctx: Context): Type =
+      ctx.substPredicateThis(this, binder, tp, null)
+
     /** Substitute a bound type by some other type */
     final def substParam(from: ParamRef, to: Type)(implicit ctx: Context): Type =
       ctx.substParam(this, from, to, null)
@@ -1539,6 +1543,9 @@ object Types {
     def isOverloaded(implicit ctx: Context) = false
   }
 
+  /** A marker trait for types that may act as stable term-level reference types. */
+  trait RefType extends SingletonType
+
   /** A trait for types that bind other types that refer to them.
    *  Instances are: LambdaType, RecType.
    */
@@ -2090,7 +2097,7 @@ object Types {
 
   abstract case class TermRef(override val prefix: Type,
                               private var myDesignator: Designator)
-    extends NamedType with SingletonType with ImplicitRef {
+    extends NamedType with RefType with ImplicitRef {
 
     type ThisType = TermRef
     type ThisName = TermName
@@ -2346,10 +2353,9 @@ object Types {
    *  @param infoFn: A function that produces the info of the refinement declaration,
    *                 given the refined type itself.
    */
-  abstract case class RefinedType(parent: Type, refinedName: Name, refinedInfo: Type) extends RefinedOrRecType {
+  abstract class RefinedType(val parent: Type, val refinedName: Name) extends RefinedOrRecType {
+    val refinedInfo: Type
 
-    if (refinedName.isTermName) assert(refinedInfo.isInstanceOf[TermType])
-    else assert(refinedInfo.isInstanceOf[TypeType], this)
     assert(!refinedName.is(NameKinds.ExpandedName), this)
 
     override def underlying(implicit ctx: Context) = parent
@@ -2387,10 +2393,17 @@ object Types {
       case _ => false
     }
     // equals comes from case class; no matching override is needed
+
+    // TODO(gsps): Add equals(that: Any) and hashCode() which consider refinedInfo?
   }
 
-  class CachedRefinedType(parent: Type, refinedName: Name, refinedInfo: Type)
-  extends RefinedType(parent, refinedName, refinedInfo)
+  class CachedRefinedType(parent: Type, refinedName: Name, _refinedInfo: Type)
+  extends RefinedType(parent, refinedName) {
+    val refinedInfo: Type = _refinedInfo
+
+    if (refinedName.isTermName) assert(refinedInfo.isInstanceOf[TermType], s"Expected TermType, got $refinedInfo")
+    else assert(refinedInfo.isInstanceOf[TypeType], this)
+  }
 
   object RefinedType {
     @tailrec def make(parent: Type, names: List[Name], infos: List[Type])(implicit ctx: Context): Type =
@@ -2401,6 +2414,12 @@ object Types {
       assert(!ctx.erasedTypes)
       unique(new CachedRefinedType(parent, name, info)).checkInst
     }
+
+    // TODO(gsps): This might be unreasonably slow
+    def unapply(tp: RefinedType): Option[(Type, Name, Type)] = tp match {
+      case tp: RefinedType => Some((tp.parent, tp.refinedName, tp.refinedInfo))
+      case _ => None
+    }
   }
 
   class RecType(parentExp: RecType => Type) extends RefinedOrRecType with BindingType {
@@ -2499,33 +2518,74 @@ object Types {
     }
   }
 
-  // --- PredicateType (encoding) -----------------------------------------------------
+  // --- PredicateRefinedType ---------------------------------------------------------
+
+  class PredicateRefinedType(val subjectName: TermName, parent: Type)(predicateBuilder: PredicateRefinedType => Type)
+    extends RefinedType(parent, NameKinds.PredicateSubjectName(subjectName))
+  {
+    val refinedInfo: Type = predicateBuilder(PredicateRefinedType.this)
+    def predicate: Type = this.refinedInfo
+
+    def predicateThis: PredicateThis = new PredicateThis(this) {}
+
+    override def derivedRefinedType(parent: Type, refinedName: Name, refinedInfo: Type)(implicit ctx: Context): Type = {
+      if (refinedName ne this.refinedName)
+        throw new UnsupportedOperationException("Cannot change refinement name on derived PredicateRefinedType.")
+      else if ((parent eq this.parent) && (refinedInfo eq this.refinedInfo))
+        this
+      else
+        new PredicateRefinedType(subjectName, parent)(prt => refinedInfo.substPredicateThis(this, prt.predicateThis))
+    }
+  }
+
+//  /** Encapsulates a predicate P[v: T] where `P` is a (typically precise) Boolean dependent on a stable value of
+//    * subject type `T`. Can be thought of as a dependent pair `(x: T, P[x])`. */
+//  case class PredicateType private(subjectTp: Type, subjectName: Name)(infoBuilder: PredicateType => Type)
+//    extends UncachedProxyType with ValueType with SingletonType with BindingType
+//  {
+//    val info: Type = infoBuilder(this)
+//
+//    override def underlying(implicit ctx: Context): Type = defn.BooleanType
+//
+//    override def hashCode: Int = identityHash
+//    override def equals(that: Any) = this.eq(that.asInstanceOf[AnyRef])
+//
+//    def predicateThis: PredicateThis = new PredicateThis(this) {}
+//
+//    override def toString = s"PredicateType($subjectTp, $hashCode)"
+//  }
+
+  abstract case class PredicateThis(binder: PredicateRefinedType) extends BoundType with SingletonType {
+    type BT = PredicateRefinedType  // PredicateType
+    override def underlying(implicit ctx: Context): Type = binder.parent  // binder.subjectTp
+    def copyBoundType(bt: BT) = bt.predicateThis
+
+    override def computeHash = addDelta(binder.identityHash, 41)
+
+    override def equals(that: Any) = that match {
+      case that: PredicateThis => binder.eq(that.binder)
+      case _ => false
+    }
+
+    override def toString =
+      try s"PredicateThis(${binder.hashCode})"
+      catch {
+        case ex: NullPointerException => s"PredicateThis(<under construction>)"
+      }
+  }
 
-  object PredicateType {
+  object PredicateRefinedType {
     def apply(subject: ValDef, pred: Type)(implicit ctx: Context): Type = {
       assertUnerased()
       val parentTpe = subject.tpt.tpe
       if (parentTpe.isError || pred.isError) parentTpe
-      else RecType(rt => RefinedType(parentTpe, nme.PRED, pred).subst(List(subject.symbol), List(rt.recThis)))
+      else new PredicateRefinedType(subject.name, parentTpe)(prt =>
+        pred.subst(List(subject.symbol), List(prt.predicateThis)))
     }
 
-    def unapply(tp: Type)(implicit ctx: Context): Option[(Type, Type)] = tp match {
-      case recTp: RecType =>
-        recTp.parent match {
-          case refTp @ RefinedType(parent, nme.PRED, pred) => Some((parent, pred))
-          case _ => None
-        }
-      case _ => None
-    }
 
-    object Fixed {
-      // Matches PredicateTypes whose RecThis has already been fixed
-      def unapply(tp: Type)(implicit ctx: Context): Option[(Type, Type)] = tp match {
-        case refTp @ RefinedType(parent, nme.PRED, pred) => Some((parent, pred))
-        case _ => None
-      }
-    }
 
+    /*
     object PseudoDnf {
       def unapply(tp: Type)(implicit ctx: Context): Option[List[List[Type]]] = {
         def isAndFn(fn: TermRef): Boolean = fn.symbol eq defn.Boolean_&&
@@ -2568,6 +2628,10 @@ object Types {
         case _ => NoType
       }
     }
+    */
+
+    // FIXME(gsps): Reimplement (unsound now)
+    def mergePredicates(tp1: Type, tp2: Type, isAnd: Boolean)(implicit ctx: Context): Type = tp1
   }
 
   // --- AndType/OrType ---------------------------------------------------------------
@@ -3410,7 +3474,7 @@ object Types {
   /** Only created in `binder.paramRefs`. Use `binder.paramRefs(paramNum)` to
    *  refer to `TermParamRef(binder, paramNum)`.
    */
-  abstract case class TermParamRef(binder: TermLambda, paramNum: Int) extends ParamRef with SingletonType {
+  abstract case class TermParamRef(binder: TermLambda, paramNum: Int) extends ParamRef with RefType {
     type BT = TermLambda
     def kindString = "Term"
     def copyBoundType(bt: BT) = bt.paramRefs(paramNum)
@@ -3465,7 +3529,7 @@ object Types {
   // ----- Skolem types -----------------------------------------------
 
   /** A skolem type reference with underlying type `binder`. */
-  case class SkolemType(info: Type) extends UncachedProxyType with ValueType with SingletonType {
+  case class SkolemType(info: Type) extends UncachedProxyType with ValueType with RefType {
     override def underlying(implicit ctx: Context) = info
     def derivedSkolemType(info: Type)(implicit ctx: Context) =
       if (info eq this.info) this else SkolemType(info)
@@ -4115,6 +4179,9 @@ object Types {
         case tp: RefinedType =>
           derivedRefinedType(tp, this(tp.parent), this(tp.refinedInfo))
 
+//        case tp: PredicateType =>
+//          PredicateType(this(tp.subjectTp), tp.subjectName)(predTp => this(tp.info).subst(tp, predTp))
+
         case tp: TypeAlias =>
           derivedTypeAlias(tp, atVariance(0)(this(tp.alias)))
 
@@ -4574,6 +4641,9 @@ object Types {
       case tp: SkolemType =>
         this(x, tp.info)
 
+//      case tp: PredicateType =>
+//        this(this(x, tp.subjectTp), tp.info)
+
       case SuperType(thistp, supertp) =>
         this(this(x, thistp), supertp)
 

compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala

@@ -322,6 +322,7 @@ object TastyFormat {
   final val IMPORTED = 65
   final val RENAMED = 66
   final val SYMBOLconst = 67
+  final val PREDICATEthis = 68
 
   // Cat. 3:    tag AST
 
@@ -417,7 +418,7 @@ object TastyFormat {
   }
 
   final val APPLIEDTERMREF = 180
-  final val PREDICATEtpt = 177
+  final val PREDICATEtpt = 177  // TODO(gsps): Rename to PREDICATEREFINEDtpt?
   final val HOLE = 255
 
   final val firstNatTreeTag = SHAREDterm
@@ -484,7 +485,8 @@ object TastyFormat {
        | ANDtpt
        | ORtpt
        | BYNAMEtpt
-       | BIND => true
+       | BIND
+       | PREDICATEtpt => true
     case _ => false
   }
 
@@ -619,6 +621,8 @@ object TastyFormat {
     case PRIVATEqualified => "PRIVATEqualified"
     case PROTECTEDqualified => "PROTECTEDqualified"
     case HOLE => "HOLE"
+    case PREDICATEtpt => "PREDICATEtpt"
+    case PREDICATEthis => "PREDICATEthis"
   }
 
   /** @return If non-negative, the number of leading references (represented as nats) of a length/trees entry.