Basic subtyping and solver for qualified types

Author: mbovel

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

@@ -1437,6 +1437,19 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
     def unapply(ts: List[Tree]): Option[List[Tree]] =
       if ts.nonEmpty && ts.head.isType then Some(ts) else None
 
+
+  /** An extractor for trees that are constant values. */
+  object ConstantTree:
+    def unapply(tree: Tree)(using Context): Option[Constant] =
+      tree match
+        case Inlined(_, Nil, expr) => unapply(expr)
+        case Typed(expr, _) => unapply(expr)
+        case Literal(c) if c.tag == Constants.NullTag => Some(c)
+        case _ =>
+          tree.tpe.widenTermRefExpr.normalized.simplified match
+            case ConstantType(c) => Some(c)
+            case _ => None
+
   /** Split argument clauses into a leading type argument clause if it exists and
    *  remaining clauses
    */

compiler/src/dotty/tools/dotc/config/Printers.scala

@@ -51,6 +51,7 @@ object Printers {
   val overload = noPrinter
   val patmatch = noPrinter
   val pickling = noPrinter
+  val qualifiedTypes = noPrinter
   val quotePickling = noPrinter
   val plugins = noPrinter
   val recheckr = noPrinter

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

@@ -1036,6 +1036,7 @@ class Definitions {
   @tu lazy val DeprecatedAnnot: ClassSymbol = requiredClass("scala.deprecated")
   @tu lazy val DeprecatedOverridingAnnot: ClassSymbol = requiredClass("scala.deprecatedOverriding")
   @tu lazy val DeprecatedInheritanceAnnot: ClassSymbol = requiredClass("scala.deprecatedInheritance")
+  @tu lazy val QualifiedAnnot: ClassSymbol = requiredClass("scala.annotation.qualified")
   @tu lazy val ImplicitAmbiguousAnnot: ClassSymbol = requiredClass("scala.annotation.implicitAmbiguous")
   @tu lazy val ImplicitNotFoundAnnot: ClassSymbol = requiredClass("scala.annotation.implicitNotFound")
   @tu lazy val InferredDepFunAnnot: ClassSymbol = requiredClass("scala.caps.internal.inferredDepFun")

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

@@ -27,6 +27,7 @@ import Capabilities.Capability
 import NameKinds.WildcardParamName
 import MatchTypes.isConcrete
 import scala.util.boundary, boundary.break
+import qualified_types.{QualifiedType, QualifiedTypes}
 
 /** Provides methods to compare types.
  */
@@ -884,6 +885,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             println(i"assertion failed while compare captured $tp1 <:< $tp2")
             throw ex
         compareCapturing || fourthTry
+      case QualifiedType(parent2, qualifier2) =>
+        QualifiedTypes.typeImplies(tp1, qualifier2) && recur(tp1, parent2)
       case tp2: AnnotatedType if tp2.isRefining =>
         (tp1.derivesAnnotWith(tp2.annot.sameAnnotation) || tp1.isBottomType) &&
         recur(tp1, tp2.parent)
@@ -2110,7 +2113,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
    * since `T >: Int` is subsumed by both alternatives in the first match clause.
    *
    * However, the following should not:
-   * 
+   *
    *   def foo[T](e: Expr[T]): T = e match
    *     case I1(_) | B(_) => 42
    *

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

@@ -41,7 +41,7 @@ import compiletime.uninitialized
 import cc.*
 import CaptureSet.IdentityCaptRefMap
 import Capabilities.*
-
+import qualified_types.QualifiedType
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
 
@@ -56,7 +56,7 @@ object Types extends TypeUtils {
    *  The principal subclasses and sub-objects are as follows:
    *
    *  ```none
-   *  Type -+- ProxyType --+- NamedType ----+--- TypeRef
+   *  Type -+- TypeProxy --+- NamedType ----+--- TypeRef
    *        |              |                 \
    *        |              +- SingletonType-+-+- TermRef
    *        |              |                |
@@ -191,9 +191,10 @@ object Types extends TypeUtils {
 
     /** Is this type a (possibly refined, applied, aliased or annotated) type reference
      *  to the given type symbol?
-     *  @sym  The symbol to compare to. It must be a class symbol or abstract type.
+     *  @param sym  The symbol to compare to. It must be a class symbol or abstract type.
      *        It makes no sense for it to be an alias type because isRef would always
      *        return false in that case.
+     *  @param skipRefined  If true, skip refinements, annotated types and applied types.
      */
     def isRef(sym: Symbol, skipRefined: Boolean = true)(using Context): Boolean = this match {
       case this1: TypeRef =>
@@ -211,7 +212,7 @@ object Types extends TypeUtils {
         else this1.underlying.isRef(sym, skipRefined)
       case this1: TypeVar =>
         this1.instanceOpt.isRef(sym, skipRefined)
-      case this1: AnnotatedType =>
+      case this1: AnnotatedType if (!this1.isRefining || skipRefined) =>
         this1.parent.isRef(sym, skipRefined)
       case _ => false
     }
@@ -1567,6 +1568,7 @@ object Types extends TypeUtils {
         def apply(tp: Type) = /*trace(i"deskolemize($tp) at $variance", show = true)*/
           tp match {
             case tp: SkolemType => range(defn.NothingType, atVariance(1)(apply(tp.info)))
+            case QualifiedType(_, _) => tp
             case _ => mapOver(tp)
           }
       }
@@ -2102,7 +2104,7 @@ object Types extends TypeUtils {
     /** Is `this` isomorphic to `that`, assuming pairs of matching binders `bs`?
      *  It is assumed that `this.ne(that)`.
      */
-    protected def iso(that: Any, bs: BinderPairs): Boolean = this.equals(that)
+    def iso(that: Any, bs: BinderPairs): Boolean = this.equals(that)
 
     /** Equality used for hash-consing; uses `eq` on all recursive invocations,
      *  except where a BindingType is involved. The latter demand a deep isomorphism check.
@@ -3486,7 +3488,7 @@ object Types extends TypeUtils {
       case _ => false
     }
 
-    override protected def iso(that: Any, bs: BinderPairs) = that match
+    override def iso(that: Any, bs: BinderPairs) = that match
       case that: AndType => tp1.equals(that.tp1, bs) && tp2.equals(that.tp2, bs)
       case _ => false
   }
@@ -3640,7 +3642,7 @@ object Types extends TypeUtils {
       case _ => false
     }
 
-    override protected def iso(that: Any, bs: BinderPairs) = that match
+    override def iso(that: Any, bs: BinderPairs) = that match
       case that: OrType => tp1.equals(that.tp1, bs) && tp2.equals(that.tp2, bs) && isSoft == that.isSoft
       case _ => false
   }
@@ -4966,7 +4968,7 @@ object Types extends TypeUtils {
      *  anymore, or NoType if the variable can still be further constrained or a provisional
      *  instance type in the constraint can be retracted.
      */
-    private[core] def permanentInst = inst
+    def permanentInst = inst
     private[core] def setPermanentInst(tp: Type): Unit =
       inst = tp
       if tp.exists && owningState != null then

compiler/src/dotty/tools/dotc/qualified_types/QualifiedType.scala

@@ -0,0 +1,38 @@
+package dotty.tools.dotc.qualified_types
+
+import dotty.tools.dotc.ast.tpd
+import dotty.tools.dotc.core.Annotations.Annotation
+import dotty.tools.dotc.core.Contexts.{ctx, Context}
+import dotty.tools.dotc.core.Types.{AnnotatedType, Type}
+
+/** A qualified type is internally represented as a type annotated with a
+ *  `@qualified` annotation.
+ */
+object QualifiedType:
+  /** Extractor for qualified types.
+   *
+   *  @param tp
+   *    the type to deconstruct
+   *  @return
+   *    a pair containing the parent type and the qualifier tree (a lambda) on
+   *    success, [[None]] otherwise
+   */
+  def unapply(tp: Type)(using Context): Option[(Type, tpd.Tree)] =
+    tp match
+      case AnnotatedType(parent, annot) if annot.symbol == ctx.definitions.QualifiedAnnot =>
+        Some((parent, annot.argument(0).get))
+      case _ =>
+        None
+
+  /** Factory method to create a qualified type.
+   *
+   *  @param parent
+   *    the parent type
+   *  @param qualifier
+   *    the qualifier tree (a lambda)
+   *  @return
+   *    a qualified type
+   */
+  def apply(parent: Type, qualifier: tpd.Tree)(using Context): Type =
+    val annotTp = ctx.definitions.QualifiedAnnot.typeRef.appliedTo(parent)
+    AnnotatedType(parent, Annotation(tpd.New(annotTp, List(qualifier))))

compiler/src/dotty/tools/dotc/qualified_types/QualifiedTypes.scala

@@ -0,0 +1,115 @@
+package dotty.tools.dotc.qualified_types
+
+import dotty.tools.dotc.ast.tpd
+import dotty.tools.dotc.ast.tpd.{
+  Apply,
+  Block,
+  EmptyTree,
+  Ident,
+  If,
+  Lambda,
+  Literal,
+  New,
+  Select,
+  SeqLiteral,
+  This,
+  Throw,
+  Tree,
+  TypeApply,
+  Typed,
+  given
+}
+import dotty.tools.dotc.core.Atoms
+import dotty.tools.dotc.core.Constants.Constant
+import dotty.tools.dotc.core.Contexts.{ctx, Context}
+import dotty.tools.dotc.core.Decorators.{i, em, toTermName}
+import dotty.tools.dotc.core.StdNames.nme
+import dotty.tools.dotc.core.Symbols.{defn, Symbol}
+import dotty.tools.dotc.core.Types.{AndType, ConstantType, SkolemType, ErrorType, MethodType, OrType, TermRef, Type, TypeProxy}
+
+import dotty.tools.dotc.report
+import dotty.tools.dotc.reporting.trace
+import dotty.tools.dotc.config.Printers
+
+object QualifiedTypes:
+  /** Does the type `tp1` imply the qualifier `qualifier2`?
+   *
+   *  Used by [[dotty.tools.dotc.core.TypeComparer]] to compare qualified types.
+   *
+   *  Note: the logic here is similar to [[Type#derivesAnnotWith]] but
+   *  additionally handle comparisons with [[SingletonType]]s.
+   */
+  def typeImplies(tp1: Type, qualifier2: Tree)(using Context): Boolean =
+    trace(i"typeImplies $tp1  -->  $qualifier2", Printers.qualifiedTypes):
+      tp1 match
+        case QualifiedType(parent1, qualifier1) =>
+          QualifierSolver().implies(qualifier1, qualifier2)
+        case tp1: (ConstantType | TermRef) =>
+          QualifierSolver().implies(equalToPredicate(tpd.singleton(tp1)), qualifier2)
+          || typeImplies(tp1.underlying, qualifier2)
+        case tp1: TypeProxy =>
+          typeImplies(tp1.underlying, qualifier2)
+        case AndType(tp11, tp12) =>
+          typeImplies(tp11, qualifier2) || typeImplies(tp12, qualifier2)
+        case OrType(tp11, tp12) =>
+          typeImplies(tp11, qualifier2) && typeImplies(tp12, qualifier2)
+        case _ =>
+          false
+          // QualifierSolver().implies(truePredicate(), qualifier2)
+
+  /** Try to adapt the tree to the given type `pt`
+   *
+   *  Returns [[EmptyTree]] if `pt` does not contain qualifiers or if the tree
+   *  cannot be adapted, or the adapted tree otherwise.
+   *
+   *  Used by [[dotty.tools.dotc.core.Typer]].
+   */
+  def adapt(tree: Tree, pt: Type)(using Context): Tree =
+    trace(i"adapt $tree to $pt", Printers.qualifiedTypes):
+      if containsQualifier(pt) && isSimple(tree) then
+        val selfifiedTp = QualifiedType(tree.tpe, equalToPredicate(tree))
+        if selfifiedTp <:< pt then tree.cast(selfifiedTp) else EmptyTree
+      else
+        EmptyTree
+
+  def isSimple(tree: Tree)(using Context): Boolean =
+    tree match
+      case Apply(fn, args)      => isSimple(fn) && args.forall(isSimple)
+      case TypeApply(fn, args)  => isSimple(fn)
+      case SeqLiteral(elems, _) => elems.forall(isSimple)
+      case Typed(expr, _)       => isSimple(expr)
+      case Block(Nil, expr)     => isSimple(expr)
+      case _ => tpd.isIdempotentExpr(tree)
+
+  def containsQualifier(tp: Type)(using Context): Boolean =
+    tp match
+      case QualifiedType(_, _) => true
+      case tp: TypeProxy       => containsQualifier(tp.underlying)
+      case AndType(tp1, tp2)   => containsQualifier(tp1) || containsQualifier(tp2)
+      case OrType(tp1, tp2)    => containsQualifier(tp1) || containsQualifier(tp2)
+      case _                   => false
+
+  def checkContainsSkolem(tp: Type)(using Context): Boolean =
+    var res = true
+    tp.foreachPart:
+      case QualifiedType(_, qualifier) =>
+        qualifier.foreachSubTree: subTree =>
+          subTree.tpe.foreachPart:
+            case tp: SkolemType =>
+              report.error(em"The qualified type $qualifier cannot be checked at runtime", qualifier.srcPos)
+              res = false
+            case _ => ()
+      case _ => ()
+    res
+
+  private def equalToPredicate(tree: Tree)(using Context): Tree =
+    Lambda(
+      MethodType(List("v".toTermName))(_ => List(tree.tpe), _ => defn.BooleanType),
+      (args) => Ident(args(0).symbol.termRef).equal(tree)
+    )
+
+  private def truePredicate()(using Context): Tree =
+    Lambda(
+      MethodType(List("v".toTermName))(_ => List(defn.AnyType), _ => defn.BooleanType),
+      (args) => Literal(Constant(true))
+    )