diff --git a/compiler/src/dotty/tools/dotc/ast/Desugar.scala b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
index c7017a8f547c..5f42c748bd33 100644
--- a/compiler/src/dotty/tools/dotc/ast/Desugar.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
@@ -78,7 +78,7 @@ object desugar {
           case tp: NamedType if tp.symbol.exists && (tp.symbol.owner eq originalOwner) =>
             val defctx = ctx.outersIterator.dropWhile(_.scope eq ctx.scope).next()
             var local = defctx.denotNamed(tp.name ++ suffix).suchThat(_.isParamOrAccessor).symbol
-            if (local.exists) (defctx.owner.thisType select local).dealias
+            if (local.exists) (defctx.owner.thisType select local).dealiasKeepAnnots
             else {
               def msg =
                 s"no matching symbol for ${tp.symbol.showLocated} in ${defctx.owner} / ${defctx.effectiveScope.toList}"
diff --git a/compiler/src/dotty/tools/dotc/ast/Trees.scala b/compiler/src/dotty/tools/dotc/ast/Trees.scala
index 3fcc107bc8b1..9f72feb216b9 100644
--- a/compiler/src/dotty/tools/dotc/ast/Trees.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Trees.scala
@@ -213,6 +213,31 @@ object Trees {
 
     override def toText(printer: Printer) = printer.toText(this)
 
+    def sameTree(that: Tree[_]): Boolean = {
+      def isSame(x: Any, y: Any): Boolean =
+        x.asInstanceOf[AnyRef].eq(y.asInstanceOf[AnyRef]) || {
+          x match {
+            case x: Tree[_] =>
+              y match {
+                case y: Tree[_] => x.sameTree(y)
+                case _ => false
+              }
+            case x: List[_] =>
+              y match {
+                case y: List[_] => x.corresponds(y)(isSame)
+                case _ => false
+              }
+            case _ =>
+              false
+          }
+        }
+      this.getClass == that.getClass && {
+        val it1 = this.productIterator
+        val it2 = that.productIterator
+        it1.corresponds(it2)(isSame)
+      }
+    }
+
     override def hashCode(): Int = uniqueId // for debugging; was: System.identityHashCode(this)
     override def equals(that: Any) = this eq that.asInstanceOf[AnyRef]
 
diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala
index e77b56e4c27f..38ff20954c0a 100644
--- a/compiler/src/dotty/tools/dotc/ast/tpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala
@@ -963,7 +963,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
         val alternatives = ctx.typer.resolveOverloaded(allAlts, proto)
         assert(alternatives.size == 1,
           i"${if (alternatives.isEmpty) "no" else "multiple"} overloads available for " +
-          i"$method on ${receiver.tpe.widenDealias} with targs: $targs%, %; args: $args%, % of types ${args.tpes}%, %; expectedType: $expectedType." +
+          i"$method on ${receiver.tpe.widenDealiasKeepAnnots} with targs: $targs%, %; args: $args%, % of types ${args.tpes}%, %; expectedType: $expectedType." +
           i" isAnnotConstructor = $isAnnotConstructor.\n" +
           i"all alternatives: ${allAlts.map(_.symbol.showDcl).mkString(", ")}\n" +
           i"matching alternatives: ${alternatives.map(_.symbol.showDcl).mkString(", ")}.") // this is parsed from bytecode tree. there's nothing user can do about it
diff --git a/compiler/src/dotty/tools/dotc/core/Annotations.scala b/compiler/src/dotty/tools/dotc/core/Annotations.scala
index 2da8c95f0b71..3d66c876f6b7 100644
--- a/compiler/src/dotty/tools/dotc/core/Annotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/Annotations.scala
@@ -34,6 +34,9 @@ object Annotations {
     def isEvaluated: Boolean = true
 
     def ensureCompleted(implicit ctx: Context): Unit = tree
+
+    def sameAnnotation(that: Annotation)(implicit ctx: Context) =
+      symbol == that.symbol && tree.sameTree(that.tree)
   }
 
   case class ConcreteAnnotation(t: Tree) extends Annotation {
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index cfb11cde9fc0..0dccb26fa617 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -275,7 +275,7 @@ trait ConstraintHandling {
       case tp: OrType  => isFullyDefined(tp.tp1) && isFullyDefined(tp.tp2)
       case _ => true
     }
-    def isOrType(tp: Type): Boolean = tp.stripTypeVar.dealias match {
+    def isOrType(tp: Type): Boolean = tp.dealias match {
       case tp: OrType => true
       case tp: RefinedOrRecType => isOrType(tp.parent)
       case AndType(tp1, tp2) => isOrType(tp1) | isOrType(tp2)
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index c87ff6b059ba..49bb1e4eb26e 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -694,6 +694,8 @@ class Definitions {
   def ClassfileAnnotationClass(implicit ctx: Context) = ClassfileAnnotationType.symbol.asClass
   lazy val StaticAnnotationType        = ctx.requiredClassRef("scala.annotation.StaticAnnotation")
   def StaticAnnotationClass(implicit ctx: Context) = StaticAnnotationType.symbol.asClass
+  lazy val RefiningAnnotationType      = ctx.requiredClassRef("scala.annotation.RefiningAnnotation")
+  def RefiningAnnotationClass(implicit ctx: Context) = RefiningAnnotationType.symbol.asClass
 
   // Annotation classes
   lazy val AliasAnnotType = ctx.requiredClassRef("scala.annotation.internal.Alias")
diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 0eeb99e66928..086bb68064fd 100644
--- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
@@ -387,7 +387,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
    *  that are not top-level are not affected.
    */
   def replace(param: TypeParamRef, tp: Type)(implicit ctx: Context): OrderingConstraint = {
-    val replacement = tp.dealias.stripTypeVar
+    val replacement = tp.dealiasKeepAnnots.stripTypeVar
     if (param == replacement) this
     else {
       assert(replacement.isValueTypeOrLambda)
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index a8a53da9ffa5..95301176d78f 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -1208,7 +1208,7 @@ object SymDenotations {
       case tp: LambdaType => tp.paramInfos.exists(hasSkolems) || hasSkolems(tp.resType)
       case tp: AndType => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
       case tp: OrType  => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
-      case tp: AnnotatedType => hasSkolems(tp.tpe)
+      case tp: AnnotatedType => hasSkolems(tp.parent)
       case _ => false
     }
 
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 52c39ab473cc..4efcb0648c12 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -236,8 +236,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         compareWild
       case tp2: LazyRef =>
         !tp2.evaluating && recur(tp1, tp2.ref)
-      case tp2: AnnotatedType =>
-        recur(tp1, tp2.tpe) // todo: refine?
+      case tp2: AnnotatedType if !tp2.isRefining =>
+        recur(tp1, tp2.parent)
       case tp2: ThisType =>
         def compareThis = {
           val cls2 = tp2.cls
@@ -345,13 +345,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         // because that would cause an assertionError. Return false instead.
         // See i859.scala for an example where we hit this case.
         !tp1.evaluating && recur(tp1.ref, tp2)
-      case tp1: AnnotatedType =>
-        recur(tp1.tpe, tp2)
+      case tp1: AnnotatedType if !tp1.isRefining =>
+        recur(tp1.parent, tp2)
       case AndType(tp11, tp12) =>
         if (tp11.stripTypeVar eq tp12.stripTypeVar) recur(tp11, tp2)
         else thirdTry
       case tp1 @ OrType(tp11, tp12) =>
-        def joinOK = tp2.dealias match {
+        def joinOK = tp2.dealiasKeepRefiningAnnots match {
           case tp2: AppliedType if !tp2.tycon.typeSymbol.isClass =>
             // If we apply the default algorithm for `A[X] | B[Y] <: C[Z]` where `C` is a
             // type parameter, we will instantiate `C` to `A` and then fail when comparing
@@ -510,7 +510,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         }
         compareTypeLambda
       case OrType(tp21, tp22) =>
-        val tp1a = tp1.widenDealias
+        val tp1a = tp1.widenDealiasKeepRefiningAnnots
         if (tp1a ne tp1)
           // Follow the alias; this might avoid truncating the search space in the either below
           // Note that it's safe to widen here because singleton types cannot be part of `|`.
@@ -567,6 +567,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
             false
         }
         compareTypeBounds
+      case tp2: AnnotatedType if tp2.isRefining =>
+        (tp1.derivesAnnotWith(tp2.annot.sameAnnotation) || defn.isBottomType(tp1)) &&
+        recur(tp1, tp2.parent)
       case ClassInfo(pre2, cls2, _, _, _) =>
         def compareClassInfo = tp1 match {
           case ClassInfo(pre1, cls1, _, _, _) =>
@@ -641,7 +644,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         }
         compareHKLambda
       case AndType(tp11, tp12) =>
-        val tp2a = tp2.dealias
+        val tp2a = tp2.dealiasKeepRefiningAnnots
         if (tp2a ne tp2) // Follow the alias; this might avoid truncating the search space in the either below
           return recur(tp1, tp2a)
 
@@ -661,6 +664,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
           case _ =>
         }
         either(recur(tp11, tp2), recur(tp12, tp2))
+      case tp1: AnnotatedType if tp1.isRefining =>
+        isNewSubType(tp1.parent)
       case JavaArrayType(elem1) =>
         def compareJavaArray = tp2 match {
           case JavaArrayType(elem2) => isSubType(elem1, elem2)
@@ -685,13 +690,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
       */
       def isMatchingApply(tp1: Type): Boolean = tp1 match {
         case AppliedType(tycon1, args1) =>
-          tycon1.dealias match {
+          tycon1.dealiasKeepRefiningAnnots match {
             case tycon1: TypeParamRef =>
               (tycon1 == tycon2 ||
               canConstrain(tycon1) && tryInstantiate(tycon1, tycon2)) &&
               isSubArgs(args1, args2, tp1, tparams)
             case tycon1: TypeRef =>
-              tycon2.dealias match {
+              tycon2.dealiasKeepRefiningAnnots match {
                 case tycon2: TypeRef if tycon1.symbol == tycon2.symbol =>
                   isSubType(tycon1.prefix, tycon2.prefix) &&
                   isSubArgs(args1, args2, tp1, tparams)
@@ -700,7 +705,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
               }
             case tycon1: TypeVar =>
               isMatchingApply(tycon1.underlying)
-            case tycon1: AnnotatedType =>
+            case tycon1: AnnotatedType if !tycon1.isRefining =>
               isMatchingApply(tycon1.underlying)
             case _ =>
               false
@@ -811,7 +816,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
                 fourthTry
             }
           }
-        case _: TypeVar | _: AnnotatedType =>
+        case _: TypeVar =>
+          recur(tp1, tp2.superType)
+        case tycon2: AnnotatedType if !tycon2.isRefining =>
           recur(tp1, tp2.superType)
         case tycon2: AppliedType =>
           fallback(tycon2.lowerBound)
@@ -1097,11 +1104,10 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
    *  is some combination of TypeRefs that point to classes, where the
    *  combiners are AppliedTypes, RefinedTypes, RecTypes, And/Or-Types or AnnotatedTypes.
    */
-   private def isCovered(tp: Type): Boolean = tp.dealias.stripTypeVar match {
+   private def isCovered(tp: Type): Boolean = tp.dealiasKeepRefiningAnnots.stripTypeVar match {
     case tp: TypeRef => tp.symbol.isClass && tp.symbol != NothingClass && tp.symbol != NullClass
     case tp: AppliedType => isCovered(tp.tycon)
     case tp: RefinedOrRecType => isCovered(tp.parent)
-    case tp: AnnotatedType => isCovered(tp.underlying)
     case tp: AndType => isCovered(tp.tp1) && isCovered(tp.tp2)
     case tp: OrType  => isCovered(tp.tp1) && isCovered(tp.tp2)
     case _ => false
@@ -1546,7 +1552,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
       }
     case tp1: TypeVar if tp1.isInstantiated =>
       tp1.underlying & tp2
-    case tp1: AnnotatedType =>
+    case tp1: AnnotatedType if !tp1.isRefining =>
       tp1.underlying & tp2
     case _ =>
       NoType
@@ -1565,7 +1571,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
       ExprType(rt1 | tp2.widenExpr)
     case tp1: TypeVar if tp1.isInstantiated =>
       tp1.underlying | tp2
-    case tp1: AnnotatedType =>
+    case tp1: AnnotatedType if !tp1.isRefining =>
       tp1.underlying | tp2
     case _ =>
       NoType
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 3e85582bef81..b90a5bde2c98 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -152,7 +152,7 @@ object Types {
       case _: SingletonType | NoPrefix => true
       case tp: RefinedOrRecType => tp.parent.isStable
       case tp: ExprType => tp.resultType.isStable
-      case tp: AnnotatedType => tp.tpe.isStable
+      case tp: AnnotatedType => tp.parent.isStable
       case _ => false
     }
 
@@ -283,6 +283,15 @@ object Types {
       case _ => false
     }
 
+    /** Does this type have a supertype with an annotation satisfying given predicate `p`? */
+    def derivesAnnotWith(p: Annotation => Boolean)(implicit ctx: Context): Boolean = this match {
+      case tp: AnnotatedType => p(tp.annot) || tp.parent.derivesAnnotWith(p)
+      case tp: TypeProxy => tp.superType.derivesAnnotWith(p)
+      case AndType(l, r) => l.derivesAnnotWith(p) || r.derivesAnnotWith(p)
+      case OrType(l, r) => l.derivesAnnotWith(p) && r.derivesAnnotWith(p)
+      case _ => false
+    }
+
     /** Does this type occur as a part of type `that`? */
     final def occursIn(that: Type)(implicit ctx: Context): Boolean =
       that existsPart (this == _)
@@ -922,6 +931,11 @@ object Types {
       */
     def stripAnnots(implicit ctx: Context): Type = this
 
+    def rewrapAnnots(tp: Type)(implicit ctx: Context): Type = tp.stripTypeVar match {
+      case AnnotatedType(tp1, annot) => AnnotatedType(rewrapAnnots(tp1), annot)
+      case _ => this
+    }
+
     /** Strip PolyType prefix */
     def stripPoly(implicit ctx: Context): Type = this match {
       case tp: PolyType => tp.resType.stripPoly
@@ -1008,48 +1022,57 @@ object Types {
         this
     }
 
-    private def dealias1(keepAnnots: Boolean)(implicit ctx: Context): Type = this match {
+    private def dealias1(keep: AnnotatedType => Context => Boolean)(implicit ctx: Context): Type = this match {
       case tp: TypeRef =>
         if (tp.symbol.isClass) tp
         else tp.info match {
-          case TypeAlias(alias) => alias.dealias1(keepAnnots): @tailrec
+          case TypeAlias(alias) => alias.dealias1(keep): @tailrec
           case _ => tp
         }
       case app @ AppliedType(tycon, args) =>
-        val tycon1 = tycon.dealias1(keepAnnots)
-        if (tycon1 ne tycon) app.superType.dealias1(keepAnnots): @tailrec
+        val tycon1 = tycon.dealias1(keep)
+        if (tycon1 ne tycon) app.superType.dealias1(keep): @tailrec
         else this
       case tp: TypeVar =>
         val tp1 = tp.instanceOpt
-        if (tp1.exists) tp1.dealias1(keepAnnots): @tailrec else tp
+        if (tp1.exists) tp1.dealias1(keep): @tailrec else tp
       case tp: AnnotatedType =>
-        val tp1 = tp.tpe.dealias1(keepAnnots)
-        if (keepAnnots) tp.derivedAnnotatedType(tp1, tp.annot) else tp1
+        val tp1 = tp.parent.dealias1(keep)
+        if (keep(tp)(ctx)) tp.derivedAnnotatedType(tp1, tp.annot) else tp1
       case tp: LazyRef =>
-        tp.ref.dealias1(keepAnnots): @tailrec
+        tp.ref.dealias1(keep): @tailrec
       case _ => this
     }
 
+    /** Follow aliases and dereferences LazyRefs, annotated types and instantiated
+     *  TypeVars until type is no longer alias type, annotated type, LazyRef,
+     *  or instantiated type variable.
+     */
+    final def dealias(implicit ctx: Context): Type = dealias1(keepNever)
+
     /** Follow aliases and dereferences LazyRefs and instantiated TypeVars until type
      *  is no longer alias type, LazyRef, or instantiated type variable.
      *  Goes through annotated types and rewraps annotations on the result.
      */
-    final def dealiasKeepAnnots(implicit ctx: Context): Type =
-      dealias1(keepAnnots = true)
+    final def dealiasKeepAnnots(implicit ctx: Context): Type = dealias1(keepAlways)
 
-    /** Follow aliases and dereferences LazyRefs, annotated types and instantiated
-     *  TypeVars until type is no longer alias type, annotated type, LazyRef,
-     *  or instantiated type variable.
-     */
-    final def dealias(implicit ctx: Context): Type =
-      dealias1(keepAnnots = false)
+    /** Like `dealiasKeepAnnots`, but keeps only refining annotations */
+    final def dealiasKeepRefiningAnnots(implicit ctx: Context): Type = dealias1(keepIfRefining)
 
-    /** Perform successive widenings and dealiasings until none can be applied anymore */
-    @tailrec final def widenDealias(implicit ctx: Context): Type = {
-      val res = this.widen.dealias
-      if (res eq this) res else res.widenDealias
+    private def widenDealias1(keep: AnnotatedType => Context => Boolean)(implicit ctx: Context): Type = {
+      val res = this.widen.dealias1(keep)
+      if (res eq this) res else res.widenDealias1(keep)
     }
 
+    /** Perform successive widenings and dealiasings until none can be applied anymore */
+    final def widenDealias(implicit ctx: Context): Type = widenDealias1(keepNever)
+
+    /** Perform successive widenings and dealiasings while rewrapping annotations, until none can be applied anymore */
+    final def widenDealiasKeepAnnots(implicit ctx: Context): Type = widenDealias1(keepAlways)
+
+    /** Perform successive widenings and dealiasings while rewrapping refining annotations, until none can be applied anymore */
+    final def widenDealiasKeepRefiningAnnots(implicit ctx: Context): Type = widenDealias1(keepIfRefining)
+
     /** Widen from constant type to its underlying non-constant
      *  base type.
      */
@@ -1796,8 +1819,8 @@ object Types {
           case arg: TypeBounds =>
             val v = param.paramVariance
             val pbounds = param.paramInfo
-            if (v > 0 && pbounds.loBound.dealias.isBottomType) TypeAlias(arg.hiBound & rebase(pbounds.hiBound))
-            else if (v < 0 && pbounds.hiBound.dealias.isTopType) TypeAlias(arg.loBound | rebase(pbounds.loBound))
+            if (v > 0 && pbounds.loBound.dealiasKeepAnnots.isBottomType) TypeAlias(arg.hiBound & rebase(pbounds.hiBound))
+            else if (v < 0 && pbounds.hiBound.dealiasKeepAnnots.isTopType) TypeAlias(arg.loBound | rebase(pbounds.loBound))
             else arg recoverable_& rebase(pbounds)
           case arg => TypeAlias(arg)
         }
@@ -3679,22 +3702,33 @@ object Types {
   // ----- Annotated and Import types -----------------------------------------------
 
   /** An annotated type tpe @ annot */
-  case class AnnotatedType(tpe: Type, annot: Annotation) extends UncachedProxyType with ValueType {
+  case class AnnotatedType(parent: Type, annot: Annotation) extends UncachedProxyType with ValueType {
     // todo: cache them? but this makes only sense if annotations and trees are also cached.
 
-    override def underlying(implicit ctx: Context): Type = tpe
+    override def underlying(implicit ctx: Context): Type = parent
 
-    def derivedAnnotatedType(tpe: Type, annot: Annotation) =
-      if ((tpe eq this.tpe) && (annot eq this.annot)) this
-      else AnnotatedType(tpe, annot)
+    def derivedAnnotatedType(parent: Type, annot: Annotation) =
+      if ((parent eq this.parent) && (annot eq this.annot)) this
+      else AnnotatedType(parent, annot)
 
     override def stripTypeVar(implicit ctx: Context): Type =
-      derivedAnnotatedType(tpe.stripTypeVar, annot)
+      derivedAnnotatedType(parent.stripTypeVar, annot)
+
+    override def stripAnnots(implicit ctx: Context): Type = parent.stripAnnots
+
+    private[this] var isRefiningKnown = false
+    private[this] var isRefiningCache: Boolean = _
 
-    override def stripAnnots(implicit ctx: Context): Type = tpe.stripAnnots
+    def isRefining(implicit ctx: Context) = {
+      if (!isRefiningKnown) {
+        isRefiningCache = annot.symbol.derivesFrom(defn.RefiningAnnotationClass)
+        isRefiningKnown = true
+      }
+      isRefiningCache
+    }
 
     override def iso(that: Any, bs: BinderPairs): Boolean = that match {
-      case that: AnnotatedType => tpe.equals(that.tpe, bs) && (annot `eq` that.annot)
+      case that: AnnotatedType => parent.equals(that.parent, bs) && (annot `eq` that.annot)
       case _ => false
     }
     // equals comes from case class; no matching override is needed
@@ -4145,11 +4179,12 @@ object Types {
      */
     def tryWiden(tp: NamedType, pre: Type): Type = pre.member(tp.name) match {
       case d: SingleDenotation =>
-        d.info.dealias match {
+        val tp1 = d.info.dealiasKeepAnnots
+        tp1.stripAnnots match {
           case TypeAlias(alias) =>
             // if H#T = U, then for any x in L..H, x.T =:= U,
             // hence we can replace with U under all variances
-            reapply(alias)
+            reapply(alias.rewrapAnnots(tp1))
           case TypeBounds(lo, hi) =>
             // If H#T = _ >: S <: U, then for any x in L..H, S <: x.T <: U,
             // hence we can replace with S..U under all variances
@@ -4575,7 +4610,7 @@ object Types {
     case _ => false
   }
 
-  // ----- Decorator implicits --------------------------------------------
+  // ----- Helpers and Decorator implicits --------------------------------------
 
   implicit def decorateTypeApplications(tpe: Type): TypeApplications = new TypeApplications(tpe)
 
@@ -4588,4 +4623,8 @@ object Types {
         else tps2.nonEmpty && tps1.head.equals(tps2.head, bs) && tps1.tail.equalElements(tps2.tail, bs)
       }
   }
+
+  private val keepAlways: AnnotatedType => Context => Boolean = _ => _ => true
+  private val keepNever: AnnotatedType => Context => Boolean = _ => _ => false
+  private val keepIfRefining: AnnotatedType => Context => Boolean = tp => ctx => tp.isRefining(ctx)
 }
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index df0ebfd89b01..c2b22ade4ed6 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -236,7 +236,7 @@ class TreePickler(pickler: TastyPickler) {
       withLength { pickleType(tpe.lo, richTypes); pickleType(tpe.hi, richTypes) }
     case tpe: AnnotatedType =>
       writeByte(ANNOTATEDtype)
-      withLength { pickleType(tpe.tpe, richTypes); pickleTree(tpe.annot.tree) }
+      withLength { pickleType(tpe.parent, richTypes); pickleTree(tpe.annot.tree) }
     case tpe: AndType =>
       writeByte(ANDtype)
       withLength { pickleType(tpe.tp1, richTypes); pickleType(tpe.tp2, richTypes) }
diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index e69b237d5a84..e1c36b9395c3 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -302,7 +302,7 @@ class TreeChecker extends Phase with SymTransformer {
 
     /** Check that all methods have MethodicType */
     def isMethodType(pt: Type)(implicit ctx: Context): Boolean = pt match {
-      case at: AnnotatedType => isMethodType(at.tpe)
+      case at: AnnotatedType => isMethodType(at.parent)
       case _: MethodicType => true  // MethodType, ExprType, PolyType
       case _ => false
     }
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 7776d198f38b..11ed46942e08 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -46,7 +46,7 @@ object Applications {
     val ref = extractorMember(tp, name)
     if (ref.isOverloaded)
       errorType(i"Overloaded reference to $ref is not allowed in extractor", errorPos)
-    ref.info.widenExpr.annotatedToRepeated.dealias
+    ref.info.widenExpr.annotatedToRepeated.dealiasKeepAnnots
   }
 
   /** Does `tp` fit the "product match" conditions as an unapply result type
diff --git a/compiler/src/dotty/tools/dotc/typer/Implicits.scala b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
index 6f39e041322d..31fd2d2026e5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
@@ -763,7 +763,7 @@ trait Implicits { self: Typer =>
     tree match {
       case Select(qual, nme.apply) if defn.isFunctionType(qual.tpe.widen) =>
         val qt = qual.tpe.widen
-        val qt1 = qt.dealias
+        val qt1 = qt.dealiasKeepAnnots
         def addendum = if (qt1 eq qt) "" else (i"\nwhich is an alias of: $qt1")
         em"parameter of ${qual.tpe.widen}$addendum"
       case _ =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Inliner.scala b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
index 59b8c6a32f6e..beaa5b5af3ec 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inliner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
@@ -224,7 +224,7 @@ class Inliner(call: tpd.Tree, rhsToInline: tpd.Tree)(implicit ctx: Context) {
    */
   private def paramBindingDef(name: Name, paramtp: Type, arg: Tree,
                               bindingsBuf: mutable.ListBuffer[ValOrDefDef]): ValOrDefDef = {
-    val argtpe = arg.tpe.dealias
+    val argtpe = arg.tpe.dealiasKeepAnnots
     val isByName = paramtp.dealias.isInstanceOf[ExprType]
     val inlineFlag = if (paramtp.hasAnnotation(defn.InlineParamAnnot)) Inline else EmptyFlags
     val (bindingFlags, bindingType) =
diff --git a/compiler/src/dotty/tools/dotc/util/common.scala b/compiler/src/dotty/tools/dotc/util/common.scala
index d9798aec5ebe..7b81416a7f74 100644
--- a/compiler/src/dotty/tools/dotc/util/common.scala
+++ b/compiler/src/dotty/tools/dotc/util/common.scala
@@ -8,6 +8,7 @@ import core.Types.WildcardType
 object common {
 
   val alwaysTrue = Function.const(true) _
+  val alwaysFalse = Function.const(false) _
   val alwaysZero = Function.const(0) _
   val alwaysWildcardType = Function.const(WildcardType) _
 
diff --git a/doc-tool/src/dotty/tools/dottydoc/model/factories.scala b/doc-tool/src/dotty/tools/dottydoc/model/factories.scala
index 66f42eb6e740..968428e30056 100644
--- a/doc-tool/src/dotty/tools/dottydoc/model/factories.scala
+++ b/doc-tool/src/dotty/tools/dottydoc/model/factories.scala
@@ -183,7 +183,7 @@ object factories {
       paramLists(mp.underlying)
 
     case annot: AnnotatedType =>
-      paramLists(annot.tpe)
+      paramLists(annot.parent)
 
     case _ =>
       Nil // return types should not be in the paramlist
diff --git a/library/src/scala/annotation/RefiningAnnotation.scala b/library/src/scala/annotation/RefiningAnnotation.scala
new file mode 100644
index 000000000000..65761d5234d4
--- /dev/null
+++ b/library/src/scala/annotation/RefiningAnnotation.scala
@@ -0,0 +1,7 @@
+package scala.annotation
+
+/** A base trait for annotations that yield proper subtypes of the types they annotate.
+ *  Refining annotations are more "sticky" than normal ones. They are conceptually kept
+ *  around when normal refinements would also not be stripped away.
+ */
+trait RefiningAnnotation extends StaticAnnotation