diff --git a/compiler/src/dotty/tools/dotc/ast/Desugar.scala b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
index daf9aa7e5c3b..6d9e9bf3bf28 100644
--- a/compiler/src/dotty/tools/dotc/ast/Desugar.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
@@ -818,47 +818,6 @@ object desugar {
     }
   }
 
-  /** Expand
-   *
-   *    <mods> opaque type T = [Xs] =>> R
-   *
-   *  to
-   *
-   *    <mods> opaque type T = T.T
-   *    synthetic object T {
-   *      synthetic opaque type T >: [Xs] =>> R
-   *    }
-   *
-   *  The generated companion object will later (in Namer) be merged with the user-defined
-   *  companion object, and the synthetic opaque type member will go into the self type.
-   */
-  def opaqueAlias(tdef: TypeDef)(implicit ctx: Context): Tree =
-    if (lacksDefinition(tdef)) {
-      ctx.error(em"opaque type ${tdef.name} must be an alias type", tdef.sourcePos)
-      tdef.withFlags(tdef.mods.flags &~ Opaque)
-    }
-    else {
-      def completeForwarder(fwd: Tree) = tdef.rhs match {
-        case LambdaTypeTree(tparams, tpt) =>
-          val tparams1 =
-            for (tparam <- tparams)
-            yield tparam.withMods(tparam.mods | Synthetic)
-          lambdaAbstract(tparams1,
-            AppliedTypeTree(fwd, tparams.map(tparam => Ident(tparam.name))))
-        case _ =>
-          fwd
-      }
-      val moduleName = tdef.name.toTermName
-      val localRef = Select(Ident(moduleName), tdef.name).withAttachment(SuppressAccessCheck, ())
-      val aliasType = cpy.TypeDef(tdef)(rhs = completeForwarder(localRef)).withSpan(tdef.span.startPos)
-      val localType = tdef.withMods(Modifiers(Synthetic | Opaque).withPrivateWithin(tdef.name))
-
-      val companions = moduleDef(ModuleDef(
-        moduleName, Template(emptyConstructor, Nil, Nil, EmptyValDef, localType :: Nil))
-          .withFlags(Synthetic | Opaque))
-      Thicket(aliasType :: companions.toList)
-    }
-
   /** The normalized name of `mdef`. This means
    *   1. Check that the name does not redefine a Scala core class.
    *      If it does redefine, issue an error and return a mangled name instead of the original one.
@@ -1035,19 +994,51 @@ object desugar {
     Bind(name, Ident(nme.WILDCARD)).withSpan(tree.span)
   }
 
-  def defTree(tree: Tree)(implicit ctx: Context): Tree = tree match {
-    case tree: ValDef => valDef(tree)
-    case tree: TypeDef =>
-      if (tree.isClassDef) classDef(tree)
-      else if (tree.mods.is(Opaque, butNot = Synthetic)) opaqueAlias(tree)
-      else tree
-    case tree: DefDef =>
-      if (tree.name.isConstructorName) tree // was already handled by enclosing classDef
-      else defDef(tree)
-    case tree: ModuleDef => moduleDef(tree)
-    case tree: PatDef => patDef(tree)
+  /** The type of tests that check whether a MemberDef is OK for some flag.
+   *  The test succeeds if the partial function is defined and returns true.
+   */
+  type MemberDefTest = PartialFunction[MemberDef, Boolean]
+
+  val legalOpaque: MemberDefTest = {
+    case TypeDef(_, rhs) =>
+      def rhsOK(tree: Tree): Boolean = tree match {
+        case _: TypeBoundsTree | _: Template => false
+        case LambdaTypeTree(_, body) => rhsOK(body)
+        case _ => true
+      }
+      rhsOK(rhs)
   }
 
+  /** Check that modifiers are legal for the definition `tree`.
+   *  Right now, we only check for `opaque`. TODO: Move other modifier checks here.
+   */
+  def checkModifiers(tree: Tree)(implicit ctx: Context): Tree = tree match {
+    case tree: MemberDef =>
+      var tested: MemberDef = tree
+      def fail(msg: String) = ctx.error(msg, tree.sourcePos)
+      def checkApplicable(flag: FlagSet, test: MemberDefTest): Unit =
+        if (tested.mods.is(flag) && !test.applyOrElse(tree, _ => false)) {
+          fail(i"modifier `$flag` is not allowed for this definition")
+          tested = tested.withMods(tested.mods.withoutFlags(flag))
+        }
+      checkApplicable(Opaque, legalOpaque)
+      tested
+    case _ =>
+      tree
+  }
+
+  def defTree(tree: Tree)(implicit ctx: Context): Tree =
+    checkModifiers(tree) match {
+      case tree: ValDef => valDef(tree)
+      case tree: TypeDef =>
+        if (tree.isClassDef) classDef(tree) else tree
+      case tree: DefDef =>
+        if (tree.name.isConstructorName) tree // was already handled by enclosing classDef
+        else defDef(tree)
+      case tree: ModuleDef => moduleDef(tree)
+      case tree: PatDef => patDef(tree)
+    }
+
   /**     { stats; <empty > }
    *  ==>
    *      { stats; () }
diff --git a/compiler/src/dotty/tools/dotc/ast/Trees.scala b/compiler/src/dotty/tools/dotc/ast/Trees.scala
index 9ef16d2ee9cc..ecbd63bc35f4 100644
--- a/compiler/src/dotty/tools/dotc/ast/Trees.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Trees.scala
@@ -818,6 +818,8 @@ object Trees {
     extends ProxyTree[T] {
     type ThisTree[-T >: Untyped] = Annotated[T]
     def forwardTo: Tree[T] = arg
+    override def disableOverlapChecks = true
+      // disable overlaps checks since the WithBounds annotation swaps type and annotation.
   }
 
   trait WithoutTypeOrPos[-T >: Untyped] extends Tree[T] {
diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala
index 9db322bb5dc4..7b70bf2591a0 100644
--- a/compiler/src/dotty/tools/dotc/ast/tpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala
@@ -206,8 +206,12 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
   def DefDef(sym: TermSymbol, tparams: List[TypeSymbol], vparamss: List[List[TermSymbol]],
              resultType: Type, rhs: Tree)(implicit ctx: Context): DefDef =
     ta.assignType(
-      untpd.DefDef(sym.name, tparams map TypeDef, vparamss.nestedMap(ValDef(_)),
-                   TypeTree(resultType), rhs),
+      untpd.DefDef(
+        sym.name,
+        tparams.map(tparam => TypeDef(tparam).withSpan(tparam.span)),
+        vparamss.nestedMap(vparam => ValDef(vparam).withSpan(vparam.span)),
+        TypeTree(resultType),
+        rhs),
       sym)
 
   def DefDef(sym: TermSymbol, rhs: Tree = EmptyTree)(implicit ctx: Context): DefDef =
diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala
index b8885b6118b6..232bfb2a9385 100644
--- a/compiler/src/dotty/tools/dotc/ast/untpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala
@@ -198,6 +198,11 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
       if (this.flags == flags) this
       else copy(flags = flags)
 
+    def withoutFlags(flags: FlagSet): Modifiers =
+      if (this.is(flags))
+        Modifiers(this.flags &~ flags, this.privateWithin, this.annotations, this.mods.filterNot(_.flags.is(flags)))
+      else this
+
     def withAddedMod(mod: Mod): Modifiers =
       if (mods.exists(_ eq mod)) this
       else withMods(mods :+ mod)
diff --git a/compiler/src/dotty/tools/dotc/core/Annotations.scala b/compiler/src/dotty/tools/dotc/core/Annotations.scala
index 6a081898ed03..b74603d8bd44 100644
--- a/compiler/src/dotty/tools/dotc/core/Annotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/Annotations.scala
@@ -171,12 +171,27 @@ object Annotations {
 
       def unapply(ann: Annotation)(implicit ctx: Context): Option[Symbol] =
         if (ann.symbol == defn.ChildAnnot) {
-          val AppliedType(tycon, (arg: NamedType) :: Nil) = ann.tree.tpe
+          val AppliedType(_, (arg: NamedType) :: Nil) = ann.tree.tpe
           Some(arg.symbol)
         }
         else None
     }
 
+    /** Extractor for WithBounds[T] annotations */
+    object WithBounds {
+      def unapply(ann: Annotation)(implicit ctx: Context): Option[TypeBounds] =
+        if (ann.symbol == defn.WithBoundsAnnot) {
+          // We need to extract the type of the type tree in the New itself.
+          // The annotation's type has been simplified as the type of an expression,
+          // which means that `&` or `|` might have been lost.
+          // Test in pos/reference/opaque.scala
+          val Apply(TypeApply(Select(New(tpt), nme.CONSTRUCTOR), _), Nil) = ann.tree
+          val AppliedType(_, lo :: hi :: Nil) = tpt.tpe
+          Some(TypeBounds(lo, hi))
+        }
+        else None
+    }
+
     def makeSourceFile(path: String)(implicit ctx: Context): Annotation =
       apply(defn.SourceFileAnnot, Literal(Constant(path)))
   }
diff --git a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
index 0308b042fcc8..0102cc0471d1 100644
--- a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
+++ b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
@@ -145,25 +145,16 @@ class CheckRealizable(implicit ctx: Context) {
    */
   private def boundsRealizability(tp: Type) = {
 
-    def isOpaqueCompanionThis = tp match {
-      case tp: ThisType => tp.cls.isOpaqueCompanion
-      case _ => false
-    }
-
     val memberProblems =
-      for {
-        mbr <- tp.nonClassTypeMembers
-        if !(mbr.info.loBound <:< mbr.info.hiBound) && !mbr.symbol.isOpaqueHelper
-      }
+      for mbr <- tp.nonClassTypeMembers if !(mbr.info.loBound <:< mbr.info.hiBound)
       yield new HasProblemBounds(mbr.name, mbr.info)
 
     val refinementProblems =
-      for {
+      for
         name <- refinedNames(tp)
         if (name.isTypeName)
         mbr <- tp.member(name).alternatives
-        if !(mbr.info.loBound <:< mbr.info.hiBound) && !isOpaqueCompanionThis
-      }
+        if !(mbr.info.loBound <:< mbr.info.hiBound)
       yield new HasProblemBounds(name, mbr.info)
 
     def baseTypeProblems(base: Type) = base match {
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 76a3c997b07d..756541e101fa 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -877,6 +877,8 @@ class Definitions {
   def BodyAnnot(implicit ctx: Context): ClassSymbol = BodyAnnotType.symbol.asClass
   @threadUnsafe lazy val ChildAnnotType: TypeRef = ctx.requiredClassRef("scala.annotation.internal.Child")
   def ChildAnnot(implicit ctx: Context): ClassSymbol = ChildAnnotType.symbol.asClass
+  @threadUnsafe lazy val WithBoundsAnnotType: TypeRef = ctx.requiredClassRef("scala.annotation.internal.WithBounds")
+  def WithBoundsAnnot(implicit ctx: Context): ClassSymbol = WithBoundsAnnotType.symbol.asClass
   @threadUnsafe lazy val CovariantBetweenAnnotType: TypeRef = ctx.requiredClassRef("scala.annotation.internal.CovariantBetween")
   def CovariantBetweenAnnot(implicit ctx: Context): ClassSymbol = CovariantBetweenAnnotType.symbol.asClass
   @threadUnsafe lazy val ContravariantBetweenAnnotType: TypeRef = ctx.requiredClassRef("scala.annotation.internal.ContravariantBetween")
diff --git a/compiler/src/dotty/tools/dotc/core/Flags.scala b/compiler/src/dotty/tools/dotc/core/Flags.scala
index 9e91d5bb02cf..f10f3f5354af 100644
--- a/compiler/src/dotty/tools/dotc/core/Flags.scala
+++ b/compiler/src/dotty/tools/dotc/core/Flags.scala
@@ -268,7 +268,7 @@ object Flags {
   /** A mutable var */
   final val Mutable: FlagSet = termFlag(12, "mutable")
 
-  /** An opqaue type */
+  /** An opaque type or a class containing one */
   final val Opaque: FlagSet = typeFlag(12, "opaque")
 
   final val MutableOrOpaque: FlagSet = Mutable.toCommonFlags
@@ -550,13 +550,7 @@ object Flags {
     Accessor | AbsOverride | StableRealizable | Captured | Synchronized | Erased
 
   /** Flags that can apply to a module class */
-  final val RetainedModuleClassFlags: FlagSet = RetainedModuleValAndClassFlags |
-    Enum | Opaque
-
-  /** Flags that are copied from a synthetic companion to a user-defined one
-   *  when the two are merged. See: Namer.mergeCompanionDefs
-   */
-  final val RetainedSyntheticCompanionFlags: FlagSet = Opaque
+  final val RetainedModuleClassFlags: FlagSet = RetainedModuleValAndClassFlags | Enum
 
   /** Packages and package classes always have these flags set */
   final val PackageCreationFlags: FlagSet =
@@ -687,9 +681,6 @@ object Flags {
   /** A Java companion object */
   final val JavaModule: FlagConjunction = allOf(JavaDefined, Module)
 
-  /** An opaque companion object */
-  final val OpaqueModule: FlagConjunction = allOf(Opaque, Module)
-
   /** A Java companion object */
   final val JavaProtected: FlagConjunction = allOf(JavaDefined, Protected)
 
@@ -739,7 +730,6 @@ object Flags {
   final val SyntheticTermParam: FlagConjunction = allOf(Synthetic, TermParam)
   final val SyntheticTypeParam: FlagConjunction = allOf(Synthetic, TypeParam)
   final val SyntheticCase: FlagConjunction = allOf(Synthetic, Case)
-  final val SyntheticOpaque: FlagConjunction = allOf(Synthetic, Opaque)
 
   implicit def conjToFlagSet(conj: FlagConjunction): FlagSet =
     FlagSet(conj.bits)
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index 23a4d993aaee..d44316e38d09 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -372,18 +372,38 @@ object SymDenotations {
       case _ => unforcedDecls.openForMutations
     }
 
-    /** If this is a synthetic opaque type alias, mark it as Deferred with empty bounds
+    /** If this is a synthetic opaque type alias, mark it as Deferred with bounds
+     *  as given by the right hand side's `WithBounds` annotation, if one is present,
+     *  or with empty bounds of the right kind, otherwise.
+     *  At the same time, integrate the original alias as a refinement of the
+     *  self type of the enclosing class.
      */
     final def normalizeOpaque()(implicit ctx: Context) = {
       def abstractRHS(tp: Type): Type = tp match {
         case tp: HKTypeLambda => tp.derivedLambdaType(resType = abstractRHS(tp.resType))
         case _ => defn.AnyType
       }
-      if (isOpaqueHelper) {
+      if (isOpaqueAlias) {
         info match {
           case TypeAlias(alias) =>
-            info = TypeBounds(defn.NothingType, abstractRHS(alias))
+            val (refiningAlias, bounds) = alias match {
+              case AnnotatedType(alias1, Annotation.WithBounds(bounds)) =>
+              	(alias1, bounds)
+              case _ =>
+              	(alias, TypeBounds(defn.NothingType, abstractRHS(alias)))
+            }
+            def refineSelfType(selfType: Type) =
+              RefinedType(selfType, name, TypeAlias(refiningAlias))
+            val enclClassInfo = owner.asClass.classInfo
+            enclClassInfo.selfInfo match {
+              case self: Type =>
+                owner.info = enclClassInfo.derivedClassInfo(selfInfo = refineSelfType(self))
+              case self: Symbol =>
+                self.info = refineSelfType(self.info)
+            }
+            info = bounds
             setFlag(Deferred)
+            typeRef.recomputeDenot()
           case _ =>
         }
       }
@@ -553,18 +573,14 @@ object SymDenotations {
     final def isAbstractOrParamType(implicit ctx: Context): Boolean = this is DeferredOrTypeParam
 
     /** Is this symbol a user-defined opaque alias type? */
-    def isOpaqueAlias(implicit ctx: Context): Boolean = is(Opaque, butNot = Synthetic)
-
-    /** Is this symbol the companion of an opaque alias type? */
-    def isOpaqueCompanion(implicit ctx: Context): Boolean = is(OpaqueModule)
+    def isOpaqueAlias(implicit ctx: Context): Boolean = is(Opaque) && !isClass
 
-    /** Is this symbol a synthetic opaque type inside an opaque companion object? */
-    def isOpaqueHelper(implicit ctx: Context): Boolean = is(SyntheticOpaque, butNot = Module)
+    /** Is this symbol a module that contains opaque aliases? */
+    def containsOpaques(implicit ctx: Context): Boolean = is(Opaque) && isClass
 
-    /** Can this symbol have a companion module?
-     *  This is the case if it is a class or an opaque type alias.
-     */
-    final def canHaveCompanion(implicit ctx: Context) = isClass || isOpaqueAlias
+    def seesOpaques(implicit ctx: Context): Boolean =
+      containsOpaques ||
+      is(Module, butNot = Package) && owner.containsOpaques
 
     /** Is this the denotation of a self symbol of some class?
      *  This is the case if one of two conditions holds:
@@ -789,7 +805,7 @@ object SymDenotations {
      */
     def membersNeedAsSeenFrom(pre: Type)(implicit ctx: Context): Boolean =
       !(  this.isTerm
-       || this.isStaticOwner && !this.isOpaqueCompanion
+       || this.isStaticOwner && !this.seesOpaques
        || ctx.erasedTypes
        || (pre eq NoPrefix)
        || (pre eq thisType)
@@ -1029,16 +1045,6 @@ object SymDenotations {
      */
     final def companionModule(implicit ctx: Context): Symbol =
       if (is(Module)) sourceModule
-      else if (isOpaqueAlias) {
-        def reference(tp: Type): Symbol = tp match {
-          case TypeRef(prefix: TermRef, _) => prefix.termSymbol
-          case tp: HKTypeLambda => reference(tp.resType)
-          case tp: AppliedType => reference(tp.tycon)
-          case tp: ErrorType => registeredCompanion.sourceModule
-        }
-        val TypeAlias(alias) = info
-        reference(alias)
-      }
       else registeredCompanion.sourceModule
 
     private def companionType(implicit ctx: Context): Symbol =
@@ -1053,13 +1059,6 @@ object SymDenotations {
     final def companionClass(implicit ctx: Context): Symbol =
       companionType.suchThat(_.isClass).symbol
 
-    /** The opaque type with the same (type-) name as this module or module class,
-     *  and which is also defined in the same scope and compilation unit.
-     *  NoSymbol if this type does not exist.
-     */
-    final def companionOpaqueType(implicit ctx: Context): Symbol =
-      companionType.suchThat(_.isOpaqueAlias).symbol
-
     final def scalacLinkedClass(implicit ctx: Context): Symbol =
       if (this is ModuleClass) companionNamed(effectiveName.toTypeName)
       else if (this.isClass) companionNamed(effectiveName.moduleClassName).sourceModule.moduleClass
@@ -1109,15 +1108,17 @@ object SymDenotations {
     final def enclosingSubClass(implicit ctx: Context): Symbol =
       ctx.owner.ownersIterator.findSymbol(_.isSubClass(symbol))
 
-    /** The alias of a synthetic opaque type that's stored in the self type of the
+    /** The alias of an opaque type alias that's stored in the self type of the
      *  containing object.
      */
     def opaqueAlias(implicit ctx: Context): Type = {
-      if (isOpaqueHelper)
-        owner.asClass.classInfo.selfType match {
-          case RefinedType(_, _, bounds) => bounds.extractOpaqueAlias
-        }
-      else NoType
+      def recur(tp: Type): Type = tp match {
+        case RefinedType(parent, rname, TypeAlias(alias)) =>
+          if (rname == name) alias else recur(parent)
+        case _ =>
+          NoType
+      }
+      recur(owner.asClass.classInfo.selfType)
     }
 
     /** The non-private symbol whose name and type matches the type of this symbol
@@ -1974,7 +1975,7 @@ object SymDenotations {
 
     /** Register companion class */
     override def registerCompanion(companion: Symbol)(implicit ctx: Context) =
-      if (companion.canHaveCompanion && !unforcedIsAbsent && !companion.unforcedIsAbsent)
+      if (companion.isClass && !unforcedIsAbsent && !companion.unforcedIsAbsent)
         myCompanion = companion
 
     override def registeredCompanion(implicit ctx: Context) = { ensureCompleted(); myCompanion }
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index bdeb07cf5ea2..0a76ff9f240b 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -232,7 +232,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
         def compareNamed(tp1: Type, tp2: NamedType): Boolean = {
           implicit val ctx: Context = this.ctx
           tp2.info match {
-            case info2: TypeAlias => recur(tp1, info2.alias)
+            case info2: TypeAlias =>
+              recur(tp1, info2.alias)
             case _ => tp1 match {
               case tp1: NamedType =>
                 tp1.info match {
@@ -359,7 +360,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
         tp1.info match {
           case info1: TypeAlias =>
             if (recur(info1.alias, tp2)) return true
-            if (tp1.prefix.isStable) return false
+            if (tp1.prefix.isStable) return tryLiftedToThis1
           case _ =>
             if (tp1 eq NothingType) return true
         }
@@ -462,7 +463,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
               narrowGADTBounds(tp2, tp1, approx, isUpper = false)) &&
             { tp1.isRef(NothingClass) || GADTusage(tp2.symbol) }
         }
-        isSubApproxHi(tp1, info2.lo) || compareGADT || fourthTry
+        isSubApproxHi(tp1, info2.lo) || compareGADT || tryLiftedToThis2 || fourthTry
 
       case _ =>
         val cls2 = tp2.symbol
@@ -721,7 +722,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
                 narrowGADTBounds(tp1, tp2, approx, isUpper = true)) &&
                 { tp2.isRef(AnyClass) || GADTusage(tp1.symbol) }
             }
-            isSubType(hi1, tp2, approx.addLow) || compareGADT
+            isSubType(hi1, tp2, approx.addLow) || compareGADT || tryLiftedToThis1
           case _ =>
             def isNullable(tp: Type): Boolean = tp.widenDealias match {
               case tp: TypeRef => tp.symbol.isNullableClass
@@ -975,7 +976,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
               case _ =>
                 fourthTry
             }
-          }
+          } || tryLiftedToThis2
+
         case _: TypeVar =>
           recur(tp1, tp2.superType)
         case tycon2: AnnotatedType if !tycon2.isRefining =>
@@ -1002,9 +1004,11 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
             isSubType(bounds(param1).hi.applyIfParameterized(args1), tp2, approx.addLow)
         case tycon1: TypeRef =>
           val sym = tycon1.symbol
-          !sym.isClass && (
+          !sym.isClass && {
             defn.isCompiletime_S(sym) && compareS(tp1, tp2, fromBelow = false) ||
-            recur(tp1.superType, tp2))
+            recur(tp1.superType, tp2) ||
+            tryLiftedToThis1
+          }
         case tycon1: TypeProxy =>
           recur(tp1.superType, tp2)
         case _ =>
@@ -1045,6 +1049,16 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
     def isSubApproxHi(tp1: Type, tp2: Type): Boolean =
       tp1.eq(tp2) || tp2.ne(NothingType) && isSubType(tp1, tp2, approx.addHigh)
 
+    def tryLiftedToThis1: Boolean = {
+      val tp1a = liftToThis(tp1)
+      (tp1a ne tp1) && recur(tp1a, tp2)
+    }
+
+    def tryLiftedToThis2: Boolean = {
+      val tp2a = liftToThis(tp2)
+      (tp2a ne tp2) && recur(tp1, tp2a)
+    }
+
     // begin recur
     if (tp2 eq NoType) false
     else if (tp1 eq tp2) true
@@ -1074,6 +1088,41 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
     }
   }
 
+  /** If `tp` is an external reference to an enclosing module M that contains opaque types,
+   *  convert to M.this.
+   *  Note: It would be legal to do the lifting also if M does not contain opaque types,
+   *  but in this case the retries in tryLiftedToThis would be redundant.
+   */
+  private def liftToThis(tp: Type): Type = {
+
+    def findEnclosingThis(moduleClass: Symbol, from: Symbol): Type =
+      if ((from.owner eq moduleClass) && from.isPackageObject && from.is(Opaque)) from.thisType
+      else if (from.is(Package)) tp
+      else if ((from eq moduleClass) && from.is(Opaque)) from.thisType
+      else if (from eq NoSymbol) tp
+      else findEnclosingThis(moduleClass, from.owner)
+
+    tp match {
+      case tp: TermRef if tp.symbol.is(Module) =>
+        findEnclosingThis(tp.symbol.moduleClass, ctx.owner)
+      case tp: TypeRef =>
+        val pre1 = liftToThis(tp.prefix)
+        if (pre1 ne tp.prefix) tp.withPrefix(pre1) else tp
+      case tp: ThisType if tp.cls.is(Package) =>
+        findEnclosingThis(tp.cls, ctx.owner)
+      case tp: AppliedType =>
+        val tycon1 = liftToThis(tp.tycon)
+        if (tycon1 ne tp.tycon) tp.derivedAppliedType(tycon1, tp.args) else tp
+      case tp: TypeVar if tp.isInstantiated =>
+        liftToThis(tp.inst)
+      case tp: AnnotatedType =>
+        val parent1 = liftToThis(tp.parent)
+        if (parent1 ne tp.parent) tp.derivedAnnotatedType(parent1, tp.annot) else tp
+      case _ =>
+        tp
+    }
+  }
+
   /** Optionally, the `n` such that `tp <:< ConstantType(Constant(n: Int))` */
   def natValue(tp: Type): Option[Int] = constValue(tp) match {
     case Some(Constant(n: Int)) if n >= 0 => Some(n)
diff --git a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
index f5ceb84d7e85..79a5dfb9cce9 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
@@ -236,7 +236,7 @@ object TypeErasure {
    *  erased to `Object` instead of `Object[]`.
    */
   def isUnboundedGeneric(tp: Type)(implicit ctx: Context): Boolean = tp.dealias match {
-    case tp: TypeRef if !tp.symbol.isOpaqueHelper =>
+    case tp: TypeRef if !tp.symbol.isOpaqueAlias =>
       !tp.symbol.isClass &&
       !classify(tp).derivesFrom(defn.ObjectClass) &&
       !tp.symbol.is(JavaDefined)
@@ -253,7 +253,7 @@ object TypeErasure {
 
   /** Is `tp` an abstract type or polymorphic type parameter, or another unbounded generic type? */
   def isGeneric(tp: Type)(implicit ctx: Context): Boolean = tp.dealias match {
-    case tp: TypeRef if !tp.symbol.isOpaqueHelper => !tp.symbol.isClass
+    case tp: TypeRef if !tp.symbol.isOpaqueAlias => !tp.symbol.isClass
     case tp: TypeParamRef => true
     case tp: TypeProxy => isGeneric(tp.translucentSuperType)
     case tp: AndType => isGeneric(tp.tp1) || isGeneric(tp.tp2)
@@ -365,7 +365,7 @@ object TypeErasure {
    *  possible instantiations?
    */
   def hasStableErasure(tp: Type)(implicit ctx: Context): Boolean = tp match {
-    case tp: TypeRef if !tp.symbol.isOpaqueHelper =>
+    case tp: TypeRef if !tp.symbol.isOpaqueAlias =>
       tp.info match {
         case TypeAlias(alias) => hasStableErasure(alias)
         case _: ClassInfo => true
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 6ffd16066f43..4e1623bc2c20 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -95,7 +95,7 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
         tp match {
           case tp: NamedType =>
             val sym = tp.symbol
-            if (sym.isStatic && !sym.maybeOwner.isOpaqueCompanion || (tp.prefix `eq` NoPrefix)) tp
+            if (sym.isStatic && !sym.maybeOwner.seesOpaques || (tp.prefix `eq` NoPrefix)) tp
             else derivedSelect(tp, atVariance(variance max 0)(this(tp.prefix)))
           case tp: ThisType =>
             toPrefix(pre, cls, tp.cls)
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index a7ab3fad44f3..06765608430e 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1140,18 +1140,6 @@ object Types {
     /** Like `dealiasKeepAnnots`, but keeps only refining annotations */
     final def dealiasKeepRefiningAnnots(implicit ctx: Context): Type = dealias1(keepIfRefining)
 
-    /** If this is a synthetic opaque type seen from inside the opaque companion object,
-     *  its opaque alias, otherwise the type itself.
-     */
-    final def followSyntheticOpaque(implicit ctx: Context): Type = this match {
-      case tp: TypeProxy if tp.typeSymbol.is(SyntheticOpaque) =>
-        tp.superType match {
-          case AndType(alias, _) => alias   // in this case we are inside the companion object
-          case _ => this
-        }
-      case _ => this
-    }
-
     /** The result of normalization using `tryNormalize`, or the type itself if
      *  tryNormlize yields NoType
      */
@@ -1896,8 +1884,10 @@ object Types {
             finish(memberDenot(symd.initial.name, allowPrivate = false))
           else if (prefix.isArgPrefixOf(symd))
             finish(argDenot(sym.asType))
-          else if (infoDependsOnPrefix(symd, prefix))
+          else if (infoDependsOnPrefix(symd, prefix)) {
+            if (!symd.isClass && symd.is(Opaque, butNot = Deferred)) symd.normalizeOpaque()
             finish(memberDenot(symd.initial.name, allowPrivate = symd.is(Private)))
+          }
           else
             finish(symd.current)
       }
@@ -2323,7 +2313,8 @@ object Types {
     override def translucentSuperType(implicit ctx: Context) = info match {
       case TypeAlias(aliased) => aliased
       case TypeBounds(_, hi) =>
-        if (symbol.isOpaqueHelper) symbol.opaqueAlias.asSeenFrom(prefix, symbol.owner)
+        if (symbol.isOpaqueAlias)
+          symbol.opaqueAlias.asSeenFrom(prefix, symbol.owner).orElse(hi) // orElse can happen for malformed input
         else hi
       case _ => underlying
     }
@@ -3521,7 +3512,7 @@ object Types {
     }
 
     override def translucentSuperType(implicit ctx: Context): Type = tycon match {
-      case tycon: TypeRef if tycon.symbol.isOpaqueHelper =>
+      case tycon: TypeRef if tycon.symbol.isOpaqueAlias =>
         tycon.translucentSuperType.applyIfParameterized(args)
       case _ =>
         superType
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index c185d329c0ad..72ef5aecc939 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -419,7 +419,8 @@ class TreeUnpickler(reader: TastyReader,
       val prefix = readType()
       val res = NamedType(prefix, sym)
       prefix match {
-        case prefix: ThisType if prefix.cls eq sym.owner => res.withDenot(sym.denot)
+        case prefix: ThisType if (prefix.cls eq sym.owner) && !sym.is(Opaque) =>
+          res.withDenot(sym.denot)
           // without this precaution we get an infinite cycle when unpickling pos/extmethods.scala
           // the problem arises when a self type of a trait is a type parameter of the same trait.
         case _ => res
@@ -815,7 +816,7 @@ class TreeUnpickler(reader: TastyReader,
             if (companion.exists && isCodefined) sym.registerCompanion(companion)
             TypeDef(readTemplate(localCtx))
           } else {
-            sym.info = TypeBounds.empty // needed to avoid cyclic references when unpicklin rhs, see i3816.scala
+            sym.info = TypeBounds.empty // needed to avoid cyclic references when unpickling rhs, see i3816.scala
             sym.setFlag(Provisional)
             val rhs = readTpt()(localCtx)
             sym.info = new NoCompleter {
@@ -826,8 +827,8 @@ class TreeUnpickler(reader: TastyReader,
               case _: TypeBounds | _: ClassInfo => checkNonCyclic(sym, rhs.tpe, reportErrors = false)
               case _ => rhs.tpe.toBounds
             }
-            sym.resetFlag(Provisional)
             sym.normalizeOpaque()
+            sym.resetFlag(Provisional)
             TypeDef(rhs)
           }
         case PARAM =>
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index fcb019bef9a5..ad199ae8ba98 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -19,6 +19,7 @@ import ast.Trees._
 import StdNames._
 import util.Spans._
 import Constants._
+import Symbols.defn
 import ScriptParsers._
 import Decorators._
 import scala.tasty.util.Chars.isIdentifierStart
@@ -201,11 +202,11 @@ object Parsers {
       canStartExpressionTokens.contains(in.token) &&
       !in.isSoftModifierInModifierPosition
 
-    def isDefIntro(allowedMods: BitSet): Boolean =
+    def isDefIntro(allowedMods: BitSet, excludedSoftModifiers: Set[TermName] = Set.empty): Boolean =
       in.token == AT ||
       (defIntroTokens `contains` in.token) ||
       (allowedMods `contains` in.token) ||
-      in.isSoftModifierInModifierPosition
+      in.isSoftModifierInModifierPosition && !excludedSoftModifiers.contains(in.name)
 
     def isStatSep: Boolean =
       in.token == NEWLINE || in.token == NEWLINES || in.token == SEMI
@@ -955,7 +956,7 @@ object Parsers {
 
       in.token match {
         case ARROW => functionRest(t :: Nil)
-        case MATCH => matchType(EmptyTree, t)
+        case MATCH => matchType(t)
         case FORSOME => syntaxError(ExistentialTypesNoLongerSupported()); t
         case _ =>
           if (imods.is(ImplicitOrGiven) && !t.isInstanceOf[FunctionWithMods])
@@ -1481,9 +1482,9 @@ object Parsers {
 
     /**    `match' { TypeCaseClauses }
      */
-    def matchType(bound: Tree, t: Tree): MatchTypeTree =
-      atSpan((if (bound.isEmpty) t else bound).span.start, accept(MATCH)) {
-        inBraces(MatchTypeTree(bound, t, caseClauses(typeCaseClause)))
+    def matchType(t: Tree): MatchTypeTree =
+      atSpan(t.span.start, accept(MATCH)) {
+        inBraces(MatchTypeTree(EmptyTree, t, caseClauses(typeCaseClause)))
       }
 
     /** FunParams         ::=  Bindings
@@ -2075,6 +2076,7 @@ object Parsers {
      *  Modifier       ::= LocalModifier
      *                  |  AccessModifier
      *                  |  override
+     *                  |  opaque
      *  LocalModifier  ::= abstract | final | sealed | implicit | lazy | erased | inline
      */
     def modifiers(allowed: BitSet = modifierTokens, start: Modifiers = Modifiers()): Modifiers = {
@@ -2617,8 +2619,7 @@ object Parsers {
         Block(stats, Literal(Constant(())))
       }
 
-    /** TypeDcl ::=  id [TypeParamClause] (TypeBounds | ‘=’ Type)
-     *            |  id [TypeParamClause] <: Type = MatchType
+    /** TypeDcl ::=  id [TypeParamClause] TypeBounds [‘=’ Type]
      */
     def typeDefOrDcl(start: Offset, mods: Modifiers): Tree = {
       newLinesOpt()
@@ -2631,15 +2632,33 @@ object Parsers {
           case EQUALS =>
             in.nextToken()
             makeTypeDef(toplevelTyp())
-          case SUBTYPE =>
-            in.nextToken()
-            val bound = toplevelTyp()
+          case SUBTYPE | SUPERTYPE =>
+            val bounds = typeBounds()
             if (in.token == EQUALS) {
-              in.nextToken()
-              makeTypeDef(matchType(bound, infixType()))
+              val eqOffset = in.skipToken()
+              var rhs = toplevelTyp()
+              rhs match {
+                case mtt: MatchTypeTree =>
+                  bounds match {
+                    case TypeBoundsTree(EmptyTree, upper) =>
+                      rhs = MatchTypeTree(upper, mtt.selector, mtt.cases)
+                    case _ =>
+                      syntaxError(i"cannot combine lower bound and match type alias", eqOffset)
+                  }
+                case _ =>
+                  if (mods.is(Opaque)) {
+                    val annotType = AppliedTypeTree(
+                      TypeTree(defn.WithBoundsAnnotType),
+                        bounds.lo.orElse(TypeTree(defn.NothingType)) ::
+                        bounds.hi.orElse(TypeTree(defn.AnyType)) :: Nil)
+                    rhs = Annotated(rhs, ensureApplied(wrapNew(annotType)))
+                  }
+                  else syntaxError(i"cannot combine bound and alias", eqOffset)
+              }
+              makeTypeDef(rhs)
             }
-            else makeTypeDef(TypeBoundsTree(EmptyTree, bound))
-          case SUPERTYPE | SEMI | NEWLINE | NEWLINES | COMMA | RBRACE | EOF =>
+            else makeTypeDef(bounds)
+          case SEMI | NEWLINE | NEWLINES | COMMA | RBRACE | EOF =>
             makeTypeDef(typeBounds())
           case _ =>
             syntaxErrorOrIncomplete(ExpectedTypeBoundOrEquals(in.token))
@@ -3081,7 +3100,7 @@ object Parsers {
           stats += implicitClosure(in.offset, Location.InBlock, modifiers(closureMods))
         else if (isExprIntro)
           stats += expr(Location.InBlock)
-        else if (isDefIntro(localModifierTokens))
+        else if (isDefIntro(localModifierTokens, excludedSoftModifiers = Set(nme.`opaque`)))
           if (closureMods.contains(in.token)) {
             val start = in.offset
             var imods = modifiers(closureMods)
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index eb01aced829c..e077f7a27e0f 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -16,6 +16,7 @@ import scala.annotation.switch
 
 class PlainPrinter(_ctx: Context) extends Printer {
   protected[this] implicit def ctx: Context = _ctx.addMode(Mode.Printing)
+  protected[this] def printDebug = ctx.settings.YprintDebug.value
 
   private[this] var openRecs: List[RecType] = Nil
 
@@ -204,13 +205,13 @@ class PlainPrinter(_ctx: Context) extends Printer {
         toTextLocal(tpe) ~ " " ~ toText(annot)
       case tp: TypeVar =>
         if (tp.isInstantiated)
-          toTextLocal(tp.instanceOpt) ~ (Str("^") provided ctx.settings.YprintDebug.value)
+          toTextLocal(tp.instanceOpt) ~ (Str("^") provided printDebug)
         else {
           val constr = ctx.typerState.constraint
           val bounds =
             if (constr.contains(tp)) ctx.addMode(Mode.Printing).typeComparer.fullBounds(tp.origin)
             else TypeBounds.empty
-          if (bounds.isTypeAlias) toText(bounds.lo) ~ (Str("^") provided ctx.settings.YprintDebug.value)
+          if (bounds.isTypeAlias) toText(bounds.lo) ~ (Str("^") provided printDebug)
           else if (ctx.settings.YshowVarBounds.value) "(" ~ toText(tp.origin) ~ "?" ~ toText(bounds) ~ ")"
           else toText(tp.origin)
         }
@@ -428,7 +429,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
   def toText(sym: Symbol): Text =
     (kindString(sym) ~~ {
       if (sym.isAnonymousClass) toTextParents(sym.info.parents) ~~ "{...}"
-      else if (hasMeaninglessName(sym)) simpleNameString(sym.owner) + idString(sym)
+      else if (hasMeaninglessName(sym) && !printDebug) simpleNameString(sym.owner) + idString(sym)
       else nameString(sym)
     }).close
 
@@ -510,7 +511,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
       else
         Text()
 
-    nodeName ~ "(" ~ elems ~ tpSuffix ~ ")" ~ (Str(tree.sourcePos.toString) provided ctx.settings.YprintPos.value)
+    nodeName ~ "(" ~ elems ~ tpSuffix ~ ")" ~ (Str(tree.sourcePos.toString) provided printDebug)
   }.close // todo: override in refined printer
 
   def toText(pos: SourcePosition): Text = {
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 1788331bbbfa..33ae95b5fc7e 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -91,9 +91,9 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
 
   override def toTextRef(tp: SingletonType): Text = controlled {
     tp match {
-      case tp: ThisType =>
+      case tp: ThisType if !printDebug =>
         if (tp.cls.isAnonymousClass) return keywordStr("this")
-        if (tp.cls is ModuleClass) return fullNameString(tp.cls.sourceModule)
+        if (tp.cls.is(ModuleClass)) return fullNameString(tp.cls.sourceModule)
       case _ =>
     }
     super.toTextRef(tp)
@@ -101,7 +101,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
 
   override def toTextPrefix(tp: Type): Text = controlled {
     def isOmittable(sym: Symbol) =
-      if (ctx.settings.verbose.value) false
+      if (printDebug) false
       else if (homogenizedView) isEmptyPrefix(sym) // drop <root> and anonymous classes, but not scala, Predef.
       else isOmittablePrefix(sym)
     tp match {
@@ -182,7 +182,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         val cls = tycon.typeSymbol
         if (tycon.isRepeatedParam) return toTextLocal(args.head) ~ "*"
         if (defn.isFunctionClass(cls)) return toTextFunction(args, cls.name.isImplicitFunction, cls.name.isErasedFunction)
-        if (tp.tupleArity >= 2 && !ctx.settings.YprintDebug.value) return toTextTuple(tp.tupleElementTypes)
+        if (tp.tupleArity >= 2 && !printDebug) return toTextTuple(tp.tupleElementTypes)
         if (isInfixType(tp)) {
           val l :: r :: Nil = args
           val opName = tyconName(tycon)
@@ -197,7 +197,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case OrType(tp1, tp2) =>
         return toTextInfixType(tpnme.raw.BAR, tp1, tp2) { toText(tpnme.raw.BAR) }
 
-      case EtaExpansion(tycon) if !ctx.settings.YprintDebug.value =>
+      case EtaExpansion(tycon) if !printDebug =>
         return toText(tycon)
       case tp: RefinedType if defn.isFunctionType(tp) =>
         return toTextDependentFunction(tp.refinedInfo.asInstanceOf[MethodType])
@@ -237,7 +237,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         }
         return "[applied to " ~ (Str("given ") provided tp.isContextualMethod) ~ (Str("erased ") provided tp.isErasedMethod) ~ "(" ~ argsText ~ ") returning " ~ toText(resultType) ~ "]"
       case IgnoredProto(ignored) =>
-        return "?" ~ (("(ignored: " ~ toText(ignored) ~ ")") provided ctx.settings.verbose.value)
+        return "?" ~ (("(ignored: " ~ toText(ignored) ~ ")") provided printDebug)
       case tp @ PolyProto(targs, resType) =>
         return "[applied to [" ~ toTextGlobal(targs, ", ") ~ "] returning " ~ toText(resType)
       case _ =>
@@ -255,7 +255,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
     ("{" ~ toText(trees, "\n") ~ "}").close
 
   protected def typeApplyText[T >: Untyped](tree: TypeApply[T]): Text = {
-    val isQuote = !ctx.settings.YprintDebug.value && tree.fun.hasType && tree.fun.symbol == defn.InternalQuoted_typeQuote
+    val isQuote = !printDebug && tree.fun.hasType && tree.fun.symbol == defn.InternalQuoted_typeQuote
     val (open, close) = if (isQuote) (keywordStr("'["), keywordStr("]")) else ("[", "]")
     val funText = toTextLocal(tree.fun).provided(!isQuote)
     tree.fun match {
@@ -337,9 +337,9 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         if (name.isTypeName) typeText(txt)
         else txt
       case tree @ Select(qual, name) =>
-        if (!ctx.settings.YprintDebug.value && tree.hasType && tree.symbol == defn.QuotedType_splice) typeText("${") ~ toTextLocal(qual) ~ typeText("}")
+        if (!printDebug && tree.hasType && tree.symbol == defn.QuotedType_splice) typeText("${") ~ toTextLocal(qual) ~ typeText("}")
         else if (qual.isType) toTextLocal(qual) ~ "#" ~ typeText(toText(name))
-        else toTextLocal(qual) ~ ("." ~ nameIdText(tree) provided (name != nme.CONSTRUCTOR || ctx.settings.YprintDebug.value))
+        else toTextLocal(qual) ~ ("." ~ nameIdText(tree) provided (name != nme.CONSTRUCTOR || printDebug))
       case tree: This =>
         optDotPrefix(tree) ~ keywordStr("this") ~ idText(tree)
       case Super(qual: This, mix) =>
@@ -349,9 +349,9 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
           changePrec (GlobalPrec) {
             keywordStr("throw ") ~ toText(args.head)
           }
-        else if (!ctx.settings.YprintDebug.value && fun.hasType && fun.symbol == defn.InternalQuoted_exprQuote)
+        else if (!printDebug && fun.hasType && fun.symbol == defn.InternalQuoted_exprQuote)
           keywordStr("'{") ~ toTextGlobal(args, ", ") ~ keywordStr("}")
-        else if (!ctx.settings.YprintDebug.value && fun.hasType && fun.symbol == defn.InternalQuoted_exprSplice)
+        else if (!printDebug && fun.hasType && fun.symbol == defn.InternalQuoted_exprSplice)
           keywordStr("${") ~ toTextGlobal(args, ", ") ~ keywordStr("}")
         else if (app.isGivenApply && !homogenizedView)
           changePrec(InfixPrec) {
@@ -450,7 +450,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
           toTextLocal(tpt) ~ "[" ~ Text(args map argText, ", ") ~ "]"
       case LambdaTypeTree(tparams, body) =>
         changePrec(GlobalPrec) {
-          tparamsText(tparams) ~ " -> " ~ toText(body)
+          tparamsText(tparams) ~ " =>> " ~ toText(body)
         }
       case MatchTypeTree(bound, sel, cases) =>
         changePrec(GlobalPrec) {
@@ -519,7 +519,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case EmptyTree =>
         "<empty>"
       case TypedSplice(t) =>
-        if (ctx.settings.YprintDebug.value) "[" ~ toText(t) ~ "]#TS#"
+        if (printDebug) "[" ~ toText(t) ~ "]#TS#"
         else toText(t)
       case tree @ ModuleDef(name, impl) =>
         withEnclosingDef(tree) {
@@ -603,7 +603,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case Splice(tree) =>
         keywordStr("${") ~ toTextGlobal(dropBlock(tree)) ~ keywordStr("}")
       case tree: Applications.IntegratedTypeArgs =>
-        toText(tree.app) ~ Str("(with integrated type args)").provided(ctx.settings.YprintDebug.value)
+        toText(tree.app) ~ Str("(with integrated type args)").provided(printDebug)
       case Thicket(trees) =>
         "Thicket {" ~~ toTextGlobal(trees, "\n") ~~ "}"
       case _ =>
@@ -719,7 +719,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
     val (leading, paramss) =
       if (isExtension && vparamss.nonEmpty) (paramsText(vparamss.head) ~ " " ~ txt, vparamss.tail)
       else (txt, vparamss)
-    (txt /: paramss)((txt, params) =>
+    (leading /: paramss)((txt, params) =>
       txt ~
       (Str(" given ") provided params.nonEmpty && params.head.mods.is(Given)) ~
       paramsText(params))
@@ -785,8 +785,9 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
 
   protected def templateText(tree: TypeDef, impl: Template): Text = {
     val decl = modText(tree.mods, tree.symbol, keywordStr(if ((tree).mods is Trait) "trait" else "class"), isType = true)
-    decl ~~ typeText(nameIdText(tree)) ~ withEnclosingDef(tree) { toTextTemplate(impl) } ~
-      (if (tree.hasType && ctx.settings.verbose.value) i"[decls = ${tree.symbol.info.decls}]" else "")
+    ( decl ~~ typeText(nameIdText(tree)) ~ withEnclosingDef(tree) { toTextTemplate(impl) }
+    // ~ (if (tree.hasType && printDebug) i"[decls = ${tree.symbol.info.decls}]" else "") // uncomment to enable
+    )
   }
 
   protected def toTextPackageId[T >: Untyped](pid: Tree[T]): Text =
@@ -850,7 +851,9 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         case _ =>
       }
     def name =
-      if (sym.is(ModuleClass) && sym.isPackageObject && sym.name.stripModuleClassSuffix == tpnme.PACKAGE)
+      if (printDebug)
+        nameString(sym)
+      else if (sym.is(ModuleClass) && sym.isPackageObject && sym.name.stripModuleClassSuffix == tpnme.PACKAGE)
         nameString(sym.owner.name)
       else if (sym.is(ModuleClass))
         nameString(sym.name.stripModuleClassSuffix)
diff --git a/compiler/src/dotty/tools/dotc/transform/ElimOpaque.scala b/compiler/src/dotty/tools/dotc/transform/ElimOpaque.scala
index d72ef6f71db5..be2cb25ff673 100644
--- a/compiler/src/dotty/tools/dotc/transform/ElimOpaque.scala
+++ b/compiler/src/dotty/tools/dotc/transform/ElimOpaque.scala
@@ -31,21 +31,26 @@ class ElimOpaque extends MiniPhase with DenotTransformer {
   def transform(ref: SingleDenotation)(implicit ctx: Context): SingleDenotation = {
     val sym = ref.symbol
     ref match {
-      case ref: SymDenotation if sym.isOpaqueHelper =>
+      case ref: SymDenotation if sym.isOpaqueAlias =>
         ref.copySymDenotation(
           info = TypeAlias(ref.opaqueAlias),
           initFlags = ref.flags &~ (Opaque | Deferred))
-      case ref: SymDenotation if sym.isOpaqueCompanion =>
+      case ref: SymDenotation if sym.containsOpaques =>
+        def stripOpaqueRefinements(tp: Type): Type = tp match {
+          case RefinedType(parent, rname, TypeAlias(_))
+          if ref.info.decl(rname).symbol.isOpaqueAlias => stripOpaqueRefinements(parent)
+          case _ => tp
+        }
         val cinfo = sym.asClass.classInfo
-        val RefinedType(sourceRef, _, _) = cinfo.selfInfo
-        val ref1 = ref.copySymDenotation(
-          info = cinfo.derivedClassInfo(selfInfo = sourceRef),
+        val strippedSelfType = stripOpaqueRefinements(cinfo.selfType)
+        ref.copySymDenotation(
+          info = cinfo.derivedClassInfo(selfInfo = strippedSelfType),
           initFlags = ref.flags &~ Opaque)
-        ref1.registeredCompanion = NoSymbol
-        ref1
-      case _ if sym.isOpaqueHelper =>
-        ref.derivedSingleDenotation(sym, TypeAlias(ref.info.extractOpaqueAlias))
       case _ =>
+        // This is dubious as it means that we do not see the alias from an external reference
+        // which has type UniqueRefDenotation instead of SymDenotation. But to correctly recompute
+        // the alias we'd need a prefix, which we do not have here. To fix this, we'd have to
+        // maintain a prefix in UniqueRefDenotations and JointRefDenotations.
         ref
     }
   }
diff --git a/compiler/src/dotty/tools/dotc/transform/ExtensionMethods.scala b/compiler/src/dotty/tools/dotc/transform/ExtensionMethods.scala
index 753baad697ce..9ebd8e98b203 100644
--- a/compiler/src/dotty/tools/dotc/transform/ExtensionMethods.scala
+++ b/compiler/src/dotty/tools/dotc/transform/ExtensionMethods.scala
@@ -113,7 +113,16 @@ class ExtensionMethods extends MiniPhase with DenotTransformer with FullParamete
       }
       ref1
     case _ =>
-      ref
+      ref.info match {
+        case ClassInfo(pre, cls, _, _, _) if cls is ModuleClass =>
+          cls.linkedClass match {
+            case valueClass: ClassSymbol if isDerivedValueClass(valueClass) =>
+              val info1 = cls.denot(ctx.withPhase(ctx.phase.next)).asClass.classInfo.derivedClassInfo(prefix = pre)
+              ref.derivedSingleDenotation(ref.symbol, info1)
+            case _ => ref
+          }
+        case _ => ref
+      }
   }
 
   protected def rewiredTarget(target: Symbol, derived: Symbol)(implicit ctx: Context): Symbol =
@@ -210,13 +219,14 @@ object ExtensionMethods {
   def extensionMethod(imeth: Symbol)(implicit ctx: Context): TermSymbol =
     ctx.atPhase(ctx.extensionMethodsPhase.next) { implicit ctx =>
       // FIXME use toStatic instead?
-      val companionInfo = imeth.owner.companionModule.info
+      val companion = imeth.owner.companionModule
+      val companionInfo = companion.info
       val candidates = extensionNames(imeth) map (companionInfo.decl(_).symbol) filter (_.exists)
       val matching = candidates filter (c => FullParameterization.memberSignature(c.info) == imeth.signature)
       assert(matching.nonEmpty,
        i"""no extension method found for:
           |
-          |  $imeth:${imeth.info.show} with signature ${imeth.signature}
+          |  $imeth:${imeth.info.show} with signature ${imeth.signature} in ${companion.moduleClass}
           |
           | Candidates:
           |
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala b/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
index d197d2a45046..8b1a74ae63f1 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
@@ -58,18 +58,6 @@ object TypeUtils {
     def toNestedPairs(implicit ctx: Context): Type =
       TypeOps.nestedPairs(tupleElementTypes)
 
-    /** Extract opaque alias from TypeBounds type that combines it with the reference
-     *  to the opaque type itself
-     */
-    def extractOpaqueAlias(implicit ctx: Context): Type = self match {
-      case TypeBounds(lo, _) =>
-        def extractAlias(tp: Type): Type = tp match {
-          case OrType(alias, _) => alias
-          case self: HKTypeLambda => self.derivedLambdaType(resType = extractAlias(self.resType))
-        }
-        extractAlias(lo)
-    }
-
     def refinedWith(name: Name, info: Type)(implicit ctx: Context) = RefinedType(self, name, info)
 
     /** The TermRef referring to the companion of the underlying class reference
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index f1ad620ae180..736a3498faa7 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -441,7 +441,6 @@ object Checking {
     checkNoConflict(Lazy, ParamAccessor, s"parameter may not be `lazy`")
     if (sym.is(Inline)) checkApplicable(Inline, sym.isTerm && !sym.is(Mutable | Module))
     if (sym.is(Lazy)) checkApplicable(Lazy, !sym.is(Method | Mutable))
-    if (sym.is(Opaque, butNot = (Synthetic | Module))) checkApplicable(Opaque, sym.isAliasType)
     if (sym.isType && !sym.is(Deferred))
       for (cls <- sym.allOverriddenSymbols.filter(_.isClass)) {
         fail(CannotHaveSameNameAs(sym, cls, CannotHaveSameNameAs.CannotBeOverridden))
diff --git a/compiler/src/dotty/tools/dotc/typer/Implicits.scala b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
index 3597692a72fa..fd07e0f254fe 100644
--- a/compiler/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
@@ -492,15 +492,15 @@ trait ImplicitRunInfo { self: Run =>
       override implicit protected val ctx: Context = liftingCtx
       override def stopAtStatic = true
       def apply(tp: Type) = tp match {
-        case tp: TypeRef if !tp.symbol.canHaveCompanion =>
+        case tp: TypeRef if !tp.symbol.isClass =>
           val pre = tp.prefix
           def joinClass(tp: Type, cls: ClassSymbol) =
             AndType.make(tp, cls.typeRef.asSeenFrom(pre, cls.owner))
-          val lead = if (tp.prefix eq NoPrefix) defn.AnyType else apply(tp.prefix)
+          val lead = if (pre eq NoPrefix) defn.AnyType else apply(pre)
           (lead /: tp.classSymbols)(joinClass)
         case tp: TypeVar =>
           apply(tp.underlying)
-        case tp: AppliedType if !tp.tycon.typeSymbol.canHaveCompanion =>
+        case tp: AppliedType if !tp.tycon.typeSymbol.isClass =>
           def applyArg(arg: Type) = arg match {
             case TypeBounds(lo, hi) => AndType.make(lo, hi)
             case WildcardType(TypeBounds(lo, hi)) => AndType.make(lo, hi)
@@ -558,9 +558,7 @@ trait ImplicitRunInfo { self: Run =>
                 for (parent <- cls.classParents; ref <- iscopeRefs(tp.baseType(parent.classSymbol)))
                   addRef(ref)
               }
-              val underlyingTypeSym = tp.widen.typeSymbol
-              if (underlyingTypeSym.isOpaqueAlias) addCompanionOf(underlyingTypeSym)
-              else tp.classSymbols(liftingCtx).foreach(addClassScope)
+              tp.classSymbols(liftingCtx).foreach(addClassScope)
             }
           case _ =>
             for (part <- tp.namedPartsWith(_.isType)) comps ++= iscopeRefs(part)
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index d7ea2549774d..2b089c42761d 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -373,8 +373,11 @@ class Namer { typer: Typer =>
         val cctx = if (tree.name == nme.CONSTRUCTOR && !(tree.mods is JavaDefined)) ctx.outer else ctx
 
         val completer = tree match {
-          case tree: TypeDef => new TypeDefCompleter(tree)(cctx)
-          case _ => new Completer(tree)(cctx)
+          case tree: TypeDef =>
+            if (flags.is(Opaque) && ctx.owner.isClass) ctx.owner.setFlag(Opaque)
+            new TypeDefCompleter(tree)(cctx)
+          case _ =>
+            new Completer(tree)(cctx)
         }
         val info = adjustIfModule(completer, tree)
         createOrRefine[Symbol](tree, name, flags | deferred | method | higherKinded,
@@ -600,7 +603,7 @@ class Namer { typer: Typer =>
       if (fromCls.mods.is(Synthetic) && !toCls.mods.is(Synthetic)) {
         removeInExpanded(fromStat, fromCls)
         val mcls = mergeModuleClass(toStat, toCls, fromCls)
-        mcls.setMods(toCls.mods | (fromCls.mods.flags & RetainedSyntheticCompanionFlags))
+        mcls.setMods(toCls.mods)
         moduleClsDef(fromCls.name) = (toStat, mcls)
       }
 
@@ -661,7 +664,7 @@ class Namer { typer: Typer =>
       val moduleDef = mutable.Map[TypeName, TypeDef]()
 
       def updateCache(cdef: TypeDef): Unit =
-        if (cdef.isClassDef && !cdef.mods.is(Package) || cdef.mods.is(Opaque, butNot = Synthetic)) {
+        if (cdef.isClassDef && !cdef.mods.is(Package)) {
           if (cdef.mods.is(ModuleClass)) moduleDef(cdef.name) = cdef
           else classDef(cdef.name) = cdef
         }
@@ -1139,37 +1142,7 @@ class Namer { typer: Typer =>
         original.putAttachment(Deriver, deriver)
       }
 
-      val finalSelfInfo: TypeOrSymbol =
-        if (cls.isOpaqueCompanion) {
-          // The self type of an opaque companion is refined with the type-alias of the original opaque type
-          def refineOpaqueCompanionSelfType(mt: Type, stats: List[Tree]): Type = (stats: @unchecked) match {
-            case (td @ TypeDef(localName, rhs)) :: _
-            if td.mods.is(SyntheticOpaque) && localName == name.stripModuleClassSuffix =>
-              // create a context owned by the current opaque helper symbol,
-              // but otherwise corresponding to the context enclosing the opaque
-              // companion object, since that's where the rhs was defined.
-              val aliasCtx = ctx.outer.fresh.setOwner(symbolOfTree(td))
-              val alias = typedAheadType(rhs)(aliasCtx).tpe
-              val original = cls.companionOpaqueType.typeRef
-              val cmp = ctx.typeComparer
-              val bounds = TypeBounds(cmp.orType(alias, original), cmp.andType(alias, original))
-              RefinedType(mt, localName, bounds)
-            case _ :: stats1 =>
-              refineOpaqueCompanionSelfType(mt, stats1)
-            case _ =>
-              mt // can happen for malformed inputs.
-          }
-          selfInfo match {
-            case self: Type =>
-              refineOpaqueCompanionSelfType(self, rest)
-            case self: Symbol =>
-              self.info = refineOpaqueCompanionSelfType(self.info, rest)
-              self
-          }
-        }
-        else selfInfo
-
-      tempInfo.finalize(denot, parentTypes, finalSelfInfo)
+      tempInfo.finalize(denot, parentTypes, selfInfo)
 
       Checking.checkWellFormed(cls)
       if (isDerivedValueClass(cls)) cls.setFlag(Final)
@@ -1482,21 +1455,18 @@ class Namer { typer: Typer =>
       sym.info = NoCompleter
       sym.info = checkNonCyclic(sym, unsafeInfo, reportErrors = true)
     }
+    sym.normalizeOpaque()
     sym.resetFlag(Provisional)
 
     // Here we pay the price for the cavalier setting info to TypeBounds.empty above.
     // We need to compensate by reloading the denotation of references that might
     // still contain the TypeBounds.empty. If we do not do this, stdlib factories
     // fail with a bounds error in PostTyper.
-    def ensureUpToDate(tp: Type, outdated: Type) = tp match {
-      case tref: TypeRef if tref.info == outdated && sym.info != outdated =>
-        tref.recomputeDenot()
-      case _ =>
-    }
-    sym.normalizeOpaque()
+    def ensureUpToDate(tref: TypeRef, outdated: Type) =
+      if (tref.info == outdated && sym.info != outdated) tref.recomputeDenot()
     ensureUpToDate(sym.typeRef, dummyInfo1)
     if (dummyInfo2 `ne` dummyInfo1) ensureUpToDate(sym.typeRef, dummyInfo2)
-    ensureUpToDate(sym.typeRef.appliedTo(tparamSyms.map(_.typeRef)), TypeBounds.empty)
+
     sym.info
   }
 }
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 0199395c5ee7..8536f22a5a80 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -263,6 +263,18 @@ class Typer extends Namer
 
           val curOwner = ctx.owner
 
+          /** Is curOwner a package object that should be skipped?
+           *  A package object should always be skipped if we look for a term.
+           *  That way we make sure we consider all overloaded alternatives of
+           *  a definition, even if they are in different source files.
+           *  If we are looking for a type, a package object should ne skipped
+           *  only if it does not contain opaque definitions. Package objects
+           *  with opaque definitions are significant, since opaque aliases
+           *  are only seen if the prefix is the this-type of the package object.
+           */
+          def isTransparentPackageObject =
+            curOwner.isPackageObject && (name.isTermName || !curOwner.is(Opaque))
+
           // Can this scope contain new definitions? This is usually the first
           // context where either the scope or the owner changes wrt the
           // context immediately nested in it. But for package contexts, it's
@@ -279,11 +291,7 @@ class Typer extends Namer
           val isNewDefScope =
             if (curOwner.is(Package) && !curOwner.isRoot) curOwner ne ctx.outer.owner
             else ((ctx.scope ne lastCtx.scope) || (curOwner ne lastCtx.owner)) &&
-              !curOwner.isPackageObject
-              // Package objects are never searched directly. We wait until we
-              // hit the enclosing package. That way we make sure we consider
-              // all overloaded alternatives of a definition, even if they are
-              // in different source files.
+                  !isTransparentPackageObject
 
           if (isNewDefScope) {
             val defDenot = ctx.denotNamed(name, required)
@@ -777,7 +785,7 @@ class Typer extends Namer
       case _: WildcardType => untpd.TypeTree()
       case _ => untpd.TypeTree(tp)
     }
-    pt.stripTypeVar.dealias.followSyntheticOpaque match {
+    pt.stripTypeVar.dealias match {
       case pt1 if defn.isNonRefinedFunction(pt1) =>
         // if expected parameter type(s) are wildcards, approximate from below.
         // if expected result type is a wildcard, approximate from above.
@@ -1660,11 +1668,7 @@ class Typer extends Namer
     val parentsWithClass = ensureFirstTreeIsClass(parents.mapconserve(typedParent).filterConserve(!_.isEmpty), cdef.nameSpan)
     val parents1 = ensureConstrCall(cls, parentsWithClass)(superCtx)
 
-    var self1 = typed(self)(ctx.outer).asInstanceOf[ValDef] // outer context where class members are not visible
-    if (cls.isOpaqueCompanion && !ctx.isAfterTyper) {
-      // this is necessary to ensure selftype is correctly pickled
-      self1 = tpd.cpy.ValDef(self1)(tpt = TypeTree(cls.classInfo.selfType))
-    }
+    val self1 = typed(self)(ctx.outer).asInstanceOf[ValDef] // outer context where class members are not visible
     if (self1.tpt.tpe.isError || classExistsOnSelf(cls.unforcedDecls, self1)) {
       // fail fast to avoid typing the body with an error type
       cdef.withType(UnspecifiedErrorType)
@@ -1806,8 +1810,15 @@ class Typer extends Namer
   def typedAnnotated(tree: untpd.Annotated, pt: Type)(implicit ctx: Context): Tree = track("typedAnnotated") {
     val annot1 = typedExpr(tree.annot, defn.AnnotationType)
     val arg1 = typed(tree.arg, pt)
-    if (ctx.mode is Mode.Type)
-      assignType(cpy.Annotated(tree)(arg1, annot1), arg1, annot1)
+    if (ctx.mode is Mode.Type) {
+      val result = assignType(cpy.Annotated(tree)(arg1, annot1), arg1, annot1)
+      result.tpe match {
+        case AnnotatedType(rhs, Annotation.WithBounds(bounds)) =>
+          if (!bounds.contains(rhs)) ctx.error(em"type $rhs outside bounds $bounds", tree.sourcePos)
+        case _ =>
+      }
+      result
+    }
     else {
       val arg2 = arg1 match {
         case Typed(arg2, tpt: TypeTree) =>
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index 19349a044516..88489a38c9c4 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -17,3 +17,6 @@ i939.scala
 typelevel0.scala
 matchtype.scala
 6322.scala
+
+# Opaque type
+i5720.scala
diff --git a/compiler/test/dotty/tools/repl/TabcompleteTests.scala b/compiler/test/dotty/tools/repl/TabcompleteTests.scala
index be66b286f7b1..f45f59668249 100644
--- a/compiler/test/dotty/tools/repl/TabcompleteTests.scala
+++ b/compiler/test/dotty/tools/repl/TabcompleteTests.scala
@@ -130,6 +130,6 @@ class TabcompleteTests extends ReplTest {
   }
 
   @Test def i6415 = fromInitialState { implicit s =>
-    assertEquals(List("Predef"), tabComplete("opaque type T = Pre"))
+    assertEquals(List("Predef"), tabComplete("object Foo { opaque type T = Pre"))
   }
 }
diff --git a/docs/docs/internals/syntax.md b/docs/docs/internals/syntax.md
index 879d7c74eacb..9e55f0c4a0ac 100644
--- a/docs/docs/internals/syntax.md
+++ b/docs/docs/internals/syntax.md
@@ -324,12 +324,12 @@ Binding           ::=  (id | ‘_’) [‘:’ Type]
 Modifier          ::=  LocalModifier
                     |  AccessModifier
                     |  ‘override’
+                    |  ‘opaque’
 LocalModifier     ::=  ‘abstract’
                     |  ‘final’
                     |  ‘sealed’
                     |  ‘implicit’
                     |  ‘lazy’
-                    |  ‘opaque’
                     |  ‘inline’
                     |  ‘erased’
 AccessModifier    ::=  (‘private’ | ‘protected’) [AccessQualifier]
@@ -360,8 +360,7 @@ VarDcl            ::=  ids ‘:’ Type
 DefDcl            ::=  DefSig [‘:’ Type]                                        DefDef(_, name, tparams, vparamss, tpe, EmptyTree)
 DefSig            ::=  ‘(’ DefParam ‘)’ [nl] id
                        [DefTypeParamClause] DefParamClauses
-TypeDcl           ::=  id [TypeParamClause] (SubtypeBounds | ‘=’ Type)             TypeDefTree(_, name, tparams, bounds)
-                    |  id [TypeParamClause] <: Type = MatchType
+TypeDcl           ::=  id [TypeParamClause] SubtypeBounds [‘=’ Type]           TypeDefTree(_, name, tparams, bound
 
 Def               ::=  ‘val’ PatDef
                     |  ‘var’ VarDef
diff --git a/docs/docs/reference/contextual/query-types.md b/docs/docs/reference/contextual/query-types.md
index 89a1f4419117..013bbd9693d0 100644
--- a/docs/docs/reference/contextual/query-types.md
+++ b/docs/docs/reference/contextual/query-types.md
@@ -118,15 +118,10 @@ As a larger example, here is a way to define constructs for checking arbitrary p
 object PostConditions {
   opaque type WrappedResult[T] = T
 
-  private object WrappedResult {
-    def wrap[T](x: T): WrappedResult[T] = x
-    def unwrap[T](x: WrappedResult[T]): T = x
-  }
-
-  def result[T] given (r: WrappedResult[T]): T = WrappedResult.unwrap(r)
+  def result[T] given (r: WrappedResult[T]): T = f
 
   def (x: T) ensuring [T](condition: given WrappedResult[T] => Boolean): T = {
-    implied for WrappedResult[T] = WrappedResult.wrap(x)
+    implied for WrappedResult[T] = x
     assert(condition)
     x
   }
diff --git a/docs/docs/reference/other-new-features/opaques-details.md b/docs/docs/reference/other-new-features/opaques-details.md
new file mode 100644
index 000000000000..9467bae0070e
--- /dev/null
+++ b/docs/docs/reference/other-new-features/opaques-details.md
@@ -0,0 +1,63 @@
+---
+layout: doc-page
+title: "Opaque Type Aliases: More Details"
+---
+
+### Syntax
+
+```
+Modifier          ::=  ...
+                    |  ‘opaque’
+```
+`opaque` is a [soft modifier](../soft-modifier.html). It can still be used as a normal identifier when it is not in front of a definition keyword.
+
+Opaque type aliases must be members of classes, traits, or objects, or they are defined
+at the top-level. They cannot be defined in local blocks.
+
+### Type Checking
+
+The general form of a (monomorphic) opaque type alias is
+```scala
+opaque type T >: L <: U = R
+```
+where the lower bound `L` and the upper bound `U` may be missing, in which case they are assumed to be `scala.Nothing` and `scala.Any`, respectively. If bounds are given, it is checked that the right hand side `R` conforms to them, i.e. `L <: R` and `R <: U`.
+
+Inside the scope of the alias definition, the alias is transparent: `T` is treated
+as a normal alias of `R`. Outside its scope, the alias is treated as the abstract type
+```scala
+type T >: L <: U`
+```
+A special case arises if the opaque type is defined in an object. Example:
+```
+object o {
+  opaque type T = R
+}
+```
+In this case we have inside the object (also for non-opaque types) that `o.T` is equal to
+`T` or its expanded form `o.this.T`. Equality is understood here as mutual subtyping, i.e.
+`o.T <: o.this.T` and `o.this.T <: T`. Furthermore, we have by the rules of opaque types
+that `o.this.T` equals `R`. The two equalities compose. That is, inside `o`, it is
+also known that `o.T` is equal to `R`. This means the following code type-checks:
+```scala
+object o {
+  opaque type T = Int
+  val x: Int = id(2)
+}
+def id(x: o.T): o.T = x
+```
+
+### Relationship to SIP 35
+
+Opaque types in Dotty are an evolution from what is described in
+[Scala SIP 35](https://docs.scala-lang.org/sips/opaque-types.html).
+
+The differences compared to the state described in this SIP are:
+
+ 1. Opaque type aliases cannot be defined anymore in local statement sequences.
+ 2. The scope where an opaque type alias is visible is now the whole scope where
+    it is defined, instead of just a companion object.
+ 3. The notion of a companion object for opaque type aliases has been dropped.
+ 4. Opaque type aliases can have bounds.
+ 5. The notion of type equality involving opaque type aliases has been clarified. It was
+    strengthened with respect to the previous implementation of SIP 35.
+
diff --git a/docs/docs/reference/other-new-features/opaques.md b/docs/docs/reference/other-new-features/opaques.md
index 5b67dafcb084..25bdc2e8673f 100644
--- a/docs/docs/reference/other-new-features/opaques.md
+++ b/docs/docs/reference/other-new-features/opaques.md
@@ -6,39 +6,42 @@ title: "Opaque Type Aliases"
 Opaque types aliases provide type abstraction without any overhead. Example:
 
 ```scala
-opaque type Logarithm = Double
-```
-
-This introduces `Logarithm` as a new type, which is implemented as `Double` but is different from it. The fact that `Logarithm` is the same as `Double` is only known in the companion object of `Logarithm`. Here is a possible companion object:
+object Logarithms {
 
-```scala
-object Logarithm {
+  opaque type Logarithm = Double
 
-  // These are the ways to lift to the logarithm type
-  def apply(d: Double): Logarithm = math.log(d)
+  object Logarithm {
 
-  def safe(d: Double): Option[Logarithm] =
-    if (d > 0.0) Some(math.log(d)) else None
+    // These are the ways to lift to the logarithm type
+    def apply(d: Double): Logarithm = math.log(d)
 
-  // This is the first way to unlift the logarithm type
-  def exponent(l: Logarithm): Double = l
+    def safe(d: Double): Option[Logarithm] =
+      if (d > 0.0) Some(math.log(d)) else None
+  }
 
   // Extension methods define opaque types' public APIs
-  implicit class LogarithmOps(val `this`: Logarithm) extends AnyVal {
-    // This is the second way to unlift the logarithm type
-    def toDouble: Double = math.exp(`this`)
-    def +(that: Logarithm): Logarithm = Logarithm(math.exp(`this`) + math.exp(that))
-    def *(that: Logarithm): Logarithm = Logarithm(`this` + that)
+  implied LogarithmOps {
+    def (x: Logarithm) toDouble: Double = math.exp(x)
+    def (x: Logarithm) + (y: Logarithm): Logarithm = Logarithm(math.exp(x) + math.exp(y))
+    def (x: Logarithm) * (y: Logarithm): Logarithm = Logarithm(x + y)
   }
 }
 ```
 
-The companion object contains with the `apply` and `safe` methods ways to convert from doubles to `Logarithm` values. It also adds an `exponent` function and a decorator that implements `+` and `*` on logarithm values, as well as a conversion `toDouble`. All this is possible because within object `Logarithm`, the type `Logarithm` is just an alias of `Double`.
+This introduces `Logarithm` as a new type, which is implemented as `Double` but is different from it. The fact that `Logarithm` is the same as `Double` is only known in the scope where
+`Logarithm` is defined which in this case is object `Logarithms`.
+
+The public API of `Logarithm` consists of the `apply` and `safe` methods that convert from doubles to `Logarithm` values, an extension method `toDouble` that converts the other way,
+and operations `+` and `*` on logarithm values. The implementations of these functions
+type-check because within object `Logarithms`, the type `Logarithm` is just an alias of `Double`.
 
-Outside the companion object, `Logarithm` is treated as a new abstract type. So the
+Outside its scope, `Logarithm` is treated as a new abstract type. So the
 following operations would be valid because they use functionality implemented in the `Logarithm` object.
 
 ```scala
+  import Logarithms._
+  import Predef.{any2stringadd => _, _}
+
   val l = Logarithm(1.0)
   val l2 = Logarithm(2.0)
   val l3 = l * l2
@@ -54,6 +57,53 @@ But the following operations would lead to type errors:
   l / l2                  // error: `/` is not a member fo Logarithm
 ```
 
-`opaque` is a [soft modifier](../soft-modifier.html).
+Aside: the `any2stringadd => _` import suppression is necessary since otherwise the universal `+` operation in `Predef` would take precedence over the `+` extension method in `LogarithmOps`. We plan to resolve this wart by eliminating `any2stringadd`.
+
+### Bounds For Opaque Type Aliases
+
+Opaque type aliases can also come with bounds. Example:
+```scala
+object Access {
+
+  opaque type Permissions = Int
+  opaque type PermissionChoice = Int
+  opaque type Permission <: Permissions & PermissionChoice = Int
+
+  def (x: Permissions) & (y: Permissions): Permissions = x & y
+  def (x: PermissionChoice) | (y: PermissionChoice): PermissionChoice = x | y
+  def (x: Permissions) is (y: Permissions) = (x & y) == y
+  def (x: Permissions) isOneOf (y: PermissionChoice) = (x & y) != 0
+
+  val NoPermission: Permission = 0
+  val ReadOnly: Permission = 1
+  val WriteOnly: Permission = 2
+  val ReadWrite: Permissions = ReadOnly & WriteOnly
+  val ReadOrWrite: PermissionChoice = ReadOnly | WriteOnly
+}
+```
+The `Access` object defines three opaque types:
+
+ - `Permission`, representing a single permission,
+ - `Permissions`, representing a conjunction (logical "and") of permissions,
+ - `PermissionChoice`, representing a disjunction (logical "or") of permissions.
+
+All three opaque types have the same underlying representation type `Int`. The
+`Permission` type has an upper bound `Permissions & PermissionChoice`. This makes
+it known outside the `Access` object that `Permission` is a subtype of the other
+two types.  Hence, the following usage scenario type-checks.
+```scala
+object User {
+  import Access._
+
+  case class Item(rights: Permissions)
+
+  val x = Item(ReadOnly)  // OK, since Permission <: Permissions
+
+  assert( x.rights.is(ReadWrite) == false )
+  assert( x.rights.isOneOf(ReadOrWrite) == true )
+}
+```
+On the other hand, the call `x.rights.isOneOf(ReadWrite)` would give a type error
+since `Permissions` and `PermissionChoice` are different, unrelated types outside `Access`.
 
-For more details, see [Scala SIP 35](https://docs.scala-lang.org/sips/opaque-types.html).
+[More details](opaques-details.md)
diff --git a/library/src-3.x/scala/IArray.scala b/library/src-3.x/scala/IArray.scala
index 7cae3d163fb0..f3e8ee2fda40 100644
--- a/library/src-3.x/scala/IArray.scala
+++ b/library/src-3.x/scala/IArray.scala
@@ -6,24 +6,24 @@ import reflect.ClassTag
  */
 opaque type IArray[+T] = Array[_ <: T]
 
-object IArray {
+/** Defines extension methods for immutable arrays */
+implied arrayOps {
+
+  /** The selection operation on an immutable array.
+    *
+    *  @param arr the immutable array
+    *  @param n   the index of the element to select
+    *  @return    the element of the array at the given index
+    */
+  inline def (arr: IArray[T]) apply[T] (n: Int): T = arr.asInstanceOf[Array[T]].apply(n)
+
+  /** The number of elements in an immutable array
+    *  @param arr  the immutable array
+    */
+  inline def (arr: IArray[T]) length[T] : Int = arr.asInstanceOf[Array[T]].length
+}
 
-  /** Defines extension methods for immutable arrays */
-  implied arrayOps {
-
-    /** The selection operation on an immutable array.
-     *
-     *  @param arr the immutable array
-     *  @param n   the index of the element to select
-     *  @return    the element of the array at the given index
-     */
-    inline def (arr: IArray[T]) apply[T] (n: Int): T = arr.asInstanceOf[Array[T]].apply(n)
-
-    /** The number of elements in an immutable array
-     *  @param arr  the immutable array
-     */
-    inline def (arr: IArray[T]) length[T] : Int = arr.asInstanceOf[Array[T]].length
-  }
+object IArray {
 
   /** An immutable array of length 0.
    */
diff --git a/library/src/scala/annotation/internal/WithBounds.scala b/library/src/scala/annotation/internal/WithBounds.scala
new file mode 100644
index 000000000000..d60ff755b912
--- /dev/null
+++ b/library/src/scala/annotation/internal/WithBounds.scala
@@ -0,0 +1,8 @@
+package scala.annotation.internal
+
+import scala.annotation.Annotation
+
+/** An annotation to indicate a pair of type bounds that comes with a type.
+ *  Used to indicate optional bounds of an opaque type
+ */
+class WithBounds[Lo <: AnyKind, Hi <: AnyKind] extends Annotation
diff --git a/tests/neg/OpaqueEscape.scala b/tests/neg/OpaqueEscape.scala
index f88f0697ac68..974bb2c38aed 100644
--- a/tests/neg/OpaqueEscape.scala
+++ b/tests/neg/OpaqueEscape.scala
@@ -1,15 +1,15 @@
 object OpaqueEscape{
   opaque type Wrapped = Int
-  abstract class EscaperBase {
-    def unwrap(i:Wrapped):Int
-    def wrap(i:Int):Wrapped
-  }
-  class Escaper extends EscaperBase{  // error: needs to be abstract
-    override def unwrap(i:Int):Int = i // error overriding method unwrap
-    override def wrap(i:Int):Int = i  // error overriding method wrap
-  }
-
-  val e = new Escaper:EscaperBase
-  val w:Wrapped = e.wrap(1)
-  val u:Int = e.unwrap(w)
-}
\ No newline at end of file
+}
+import OpaqueEscape._
+abstract class EscaperBase {
+def unwrap(i:Wrapped):Int
+  def wrap(i:Int):Wrapped
+}
+class Escaper extends EscaperBase{  // error: needs to be abstract
+  override def unwrap(i:Int):Int = i // error overriding method unwrap
+  override def wrap(i:Int):Int = i  // error overriding method wrap
+}
+val e = new Escaper:EscaperBase
+val w:Wrapped = e.wrap(1)
+val u:Int = e.unwrap(w)
\ No newline at end of file
diff --git a/tests/neg/i5455.scala b/tests/neg/i5455.scala
index 13d44fa8058e..05c2c17cb4a8 100644
--- a/tests/neg/i5455.scala
+++ b/tests/neg/i5455.scala
@@ -10,10 +10,10 @@ object Library {
     def times(x: Nat, y: Nat): Nat = x * y
     def toInt(n: Nat): Int = n
 
-    implicit class NatOps(val self: Nat) extends AnyVal {
-      def *(other: Nat): Nat = self * other
-      def toInt: Int = self.asInstanceOf
-    }
+  }
+  implied NatOps {
+    def (x: Nat) * (y: Nat): Nat = x * y
+    def (x: Nat) toInt: Int = x
   }
 }
 
diff --git a/tests/neg/i5481.scala b/tests/neg/i5481.scala
index 274575689384..8d2b890267ae 100644
--- a/tests/neg/i5481.scala
+++ b/tests/neg/i5481.scala
@@ -15,6 +15,7 @@ object OpaqueType {
     def singleton[A](a: A): Set[A] = _ == a
     def singleton0[A](a: A): Set[A] = (_: A) == a
   }
-
+}
+object Test {
   def singleton[A](a: A): Set[A] = _ == a       // error: missing parameter type
 }
\ No newline at end of file
diff --git a/tests/neg/i5546.scala b/tests/neg/i5546.scala
index 4456feacc0ac..7984bb95b1fc 100644
--- a/tests/neg/i5546.scala
+++ b/tests/neg/i5546.scala
@@ -14,6 +14,9 @@ object O {
   object Feet { def apply(d: Double): Feet = d }
   implicit def eqF: Eql[Feet, Feet] = Eql.derived
 
+}
+object Test {
+  import O._
   def main(args: Array[String]): Unit = {
     println(Feet(3) == Meters(3)) // error: cannot compare
     println(Feet(3) == 3.0) // error: cannot compare
diff --git a/tests/neg/i6061.scala b/tests/neg/i6061.scala
index b1028d2889b3..5cc2a95cb212 100644
--- a/tests/neg/i6061.scala
+++ b/tests/neg/i6061.scala
@@ -1,2 +1,4 @@
-opaque object
-  // error
\ No newline at end of file
+opaque object // ...
+
+
+// error: modifier `opaque` not allowed // error
\ No newline at end of file
diff --git a/tests/neg/no-self-leaks.scala b/tests/neg/no-self-leaks.scala
new file mode 100644
index 000000000000..48de38c5b213
--- /dev/null
+++ b/tests/neg/no-self-leaks.scala
@@ -0,0 +1,18 @@
+trait C { this: { type T = Int } =>
+
+  type T
+  val x: T
+}
+
+class D extends C {
+  type T = Int
+  val x = 10
+}
+
+object Test {
+
+  val c: C = new D
+  val y: c.T = c.x
+  val x: Int = c.x   // error
+  val z: Int = y     // error
+}
\ No newline at end of file
diff --git a/tests/neg/opaque-bounds.scala b/tests/neg/opaque-bounds.scala
new file mode 100644
index 000000000000..4755f58bd70b
--- /dev/null
+++ b/tests/neg/opaque-bounds.scala
@@ -0,0 +1,48 @@
+class Test { // error: class Test cannot be instantiated
+
+  opaque type FlagSet = Int
+
+  opaque type Flag <: FlagSet = String  // error: type String outside bounds  <: Test.this.FlagSet
+
+  object Flag {
+    def make(s: String): Flag = s
+  }
+
+  val f: Flag = Flag.make("hello")
+  val g: FlagSet = f
+
+}
+
+object Access {
+
+  opaque type Permissions = Int
+  opaque type PermissionChoice = Int
+  opaque type Permission <: Permissions & PermissionChoice = Int
+
+  def (x: Permissions) & (y: Permissions): Permissions = x & y
+  def (x: PermissionChoice) | (y: PermissionChoice): PermissionChoice = x | y
+  def (x: Permissions) is (y: Permissions) = (x & y) == y
+  def (x: Permissions) isOneOf (y: PermissionChoice) = (x & y) != 0
+
+  val NoPermission: Permission = 0
+  val ReadOnly: Permission = 1
+  val WriteOnly: Permission = 2
+  val ReadWrite: Permissions = ReadOnly & WriteOnly
+  val ReadOrWrite: PermissionChoice = ReadOnly | WriteOnly
+}
+
+object User {
+  import Access._
+
+  case class Item(rights: Permissions)
+
+  val p1: Permissions = ReadOrWrite  // error
+  val p2: PermissionChoice = ReadWrite // error
+
+  val x = Item(ReadOnly)
+
+  assert( x.rights.is(ReadWrite) == false )
+  assert( x.rights.isOneOf(ReadOrWrite) == true )
+
+  assert( x.rights.isOneOf(ReadWrite) == true ) // error: found Permissions, required: PermissionChoice
+}
\ No newline at end of file
diff --git a/tests/neg/opaque-id.scala b/tests/neg/opaque-id.scala
index 434d7c1a5457..8a46380762fb 100644
--- a/tests/neg/opaque-id.scala
+++ b/tests/neg/opaque-id.scala
@@ -4,6 +4,9 @@ object Test {
     def f(x: T[Int]): Int = x // OK
     def g(x: Int): T[Int] = x // OK
   }
+}
+object Test2 {
+  import Test._
   val x: T[Int] = 2 // error
   val y: Int = x    // error
 }
diff --git a/tests/neg/opaque-immutable-array.scala b/tests/neg/opaque-immutable-array.scala
index 5677b0fa9ebb..82e55eb21f5d 100644
--- a/tests/neg/opaque-immutable-array.scala
+++ b/tests/neg/opaque-immutable-array.scala
@@ -41,6 +41,9 @@ object ia {
   }
 
   def xs: IArray[Long] = ???
+}
+object Test {
+  import ia._
 
   xs.length    // error: not a member
   xs.apply(2)  // error: not a member
diff --git a/tests/neg/opaque.scala b/tests/neg/opaque.scala
index 7da4427b1c74..921544abe5d4 100644
--- a/tests/neg/opaque.scala
+++ b/tests/neg/opaque.scala
@@ -4,20 +4,25 @@ object opaquetypes {
 
   opaque class Foo // error
 
+  opaque object Foo // error
+
   opaque type T // error
 
   opaque type U <: String // error
 
-  opaque type Fix[F[_]] = F[Fix[F]] // error: cyclic // error
+  opaque type Fix[F[_]] = F[Fix[F]] // error: cyclic
 
   opaque type O = String
 
-  val s: O = "" // error
+  val s: O = "" // should now be OK
 
   object O {
     val s: O = "" // should be OK
   }
 
+  def foo() = {
+    opaque type X = Int   // error
+  }
 }
 
 object logs {
@@ -42,7 +47,10 @@ object logs {
       def *(that: Logarithm): Logarithm = Logarithm(`this` + that)
     }
   }
+}
 
+object Test {
+  import logs._
   val l = Logarithm(2.0)
   val d: Double = l       // error: found: Logarithm, required: Double
   val l2: Logarithm = 1.0 // error: found: Double, required: Logarithm
diff --git a/tests/neg/simple-opaque.scala b/tests/neg/simple-opaque.scala
new file mode 100644
index 000000000000..a1f47fca94e8
--- /dev/null
+++ b/tests/neg/simple-opaque.scala
@@ -0,0 +1,24 @@
+object o {
+
+  opaque type T = Int
+  val x: T = 322
+
+  def toT(x: Int): T = x
+
+  object oo {
+    def apply222(x: Int): T = x
+  }
+}
+
+object Test {
+
+  val y: o.T = o.x
+  val x: Int = o.x   // error
+  val z: Int = y     // error
+
+  val t = o.toT(11)
+  val i: Int = t     // error
+
+  val t2: o.T = o.oo.apply222(22)
+  val i2: Int = t2   // error
+}
\ No newline at end of file
diff --git a/tests/neg/tagging.scala b/tests/neg/tagging.scala
index 6ad97fde3632..addf283aec05 100644
--- a/tests/neg/tagging.scala
+++ b/tests/neg/tagging.scala
@@ -36,6 +36,9 @@ object tagging {
   trait Meter
   trait Foot
   trait Fathom
+}
+object test {
+  import tagging._
 
   val x: Double @@ Meter = (1e7).tag[Meter]
   val y: Double @@ Foot = (123.0).tag[Foot]
diff --git a/tests/neg/toplevel-cyclic/defs_1.scala b/tests/neg/toplevel-cyclic/defs_1.scala
index 4c78584a5bdf..8f37d3887bd4 100644
--- a/tests/neg/toplevel-cyclic/defs_1.scala
+++ b/tests/neg/toplevel-cyclic/defs_1.scala
@@ -1,2 +1,2 @@
-type A = B  // error: recursion limit exceeded
+type A = B  // error: recursion limit exceeded // error: recursion limit exceeded
 
diff --git a/tests/pos/i6287.scala b/tests/pos/i6287.scala
index c9c6f8fca97f..0df6bc1ff42e 100644
--- a/tests/pos/i6287.scala
+++ b/tests/pos/i6287.scala
@@ -1,13 +1,5 @@
-object O{
-  def m() = {
-    opaque type T = Int
-    object T
-  }
-}
 object A {
-  {
     opaque type T = Int
     object T
     println
-  }
 }
\ No newline at end of file
diff --git a/tests/pos/opaque.scala b/tests/pos/opaque.scala
index a1f2b09ad3bc..7208d0b74889 100644
--- a/tests/pos/opaque.scala
+++ b/tests/pos/opaque.scala
@@ -13,17 +13,17 @@ object opaquetypes {
     // This is the first way to unlift the logarithm type
     def exponent(l: Logarithm): Double = l
 
-    // Extension methods define opaque types' public APIs
-    implicit class LogarithmOps(val `this`: Logarithm) extends AnyVal {
-      // This is the second way to unlift the logarithm type
-      def toDouble: Double = math.exp(`this`)
-      def +(that: Logarithm): Logarithm = Logarithm(math.exp(`this`) + math.exp(that))
-      def *(that: Logarithm): Logarithm = apply(`this` + that)
-    }
-
     assert(exponent(LL) == 1.0)
   }
 
+  // Extension methods define opaque types' public APIs
+  implicit class LogarithmOps(val `this`: Logarithm) extends AnyVal {
+    // This is the second way to unlift the logarithm type
+    def toDouble: Double = math.exp(`this`)
+    def +(that: Logarithm): Logarithm = Logarithm(math.exp(`this`) + math.exp(that))
+    def *(that: Logarithm): Logarithm = Logarithm(`this` + that)
+  }
+
   val LL: Logarithm = Logarithm(1)
 }
 object usesites {
diff --git a/tests/pos/postconditions.scala b/tests/pos/postconditions.scala
index 0ee5970f0d5a..9a8e53238e88 100644
--- a/tests/pos/postconditions.scala
+++ b/tests/pos/postconditions.scala
@@ -1,15 +1,10 @@
 object PostConditions {
   opaque type WrappedResult[T] = T
 
-  private object WrappedResult {
-    def wrap[T](x: T): WrappedResult[T] = x
-    def unwrap[T](x: WrappedResult[T]): T = x
-  }
-
-  def result[T] given (r: WrappedResult[T]): T = WrappedResult.unwrap(r)
+  def result[T] given (r: WrappedResult[T]): T = r
 
   def (x: T) ensuring [T](condition: given WrappedResult[T] => Boolean): T = {
-    implied for WrappedResult[T] = WrappedResult.wrap(x)
+    implied for WrappedResult[T] = x
     assert(condition)
     x
   }
diff --git a/tests/pos/reference/opaque.scala b/tests/pos/reference/opaque.scala
new file mode 100644
index 000000000000..7ffd50a06e6e
--- /dev/null
+++ b/tests/pos/reference/opaque.scala
@@ -0,0 +1,71 @@
+object Logarithms {
+
+  opaque type Logarithm = Double
+
+  object Logarithm {
+
+    // These are the ways to lift to the logarithm type
+    def apply(d: Double): Logarithm = math.log(d)
+
+    def safe(d: Double): Option[Logarithm] =
+      if (d > 0.0) Some(math.log(d)) else None
+  }
+
+  // Extension methods define opaque types' public APIs
+  implied LogarithmOps {
+    def (x: Logarithm) toDouble: Double = math.exp(x)
+    def (x: Logarithm) + (y: Logarithm): Logarithm = Logarithm(math.exp(x) + math.exp(y))
+    def (x: Logarithm) * (y: Logarithm): Logarithm = Logarithm(x + y)
+  }
+}
+
+object LogTest {
+  import Logarithms._
+  import Predef.{any2stringadd => _, _}
+
+  val l = Logarithm(1.0)
+  val l2 = Logarithm(2.0)
+  val l3 = l * l2
+  val l4 = l + l2
+}
+
+
+object Access {
+
+  opaque type Permissions = Int
+  opaque type PermissionChoice = Int
+  opaque type Permission <: Permissions & PermissionChoice = Int
+
+  def (x: Permissions) & (y: Permissions): Permissions = x & y
+  def (x: PermissionChoice) | (y: PermissionChoice): PermissionChoice = x | y
+  def (x: Permissions) is (y: Permissions) = (x & y) == y
+  def (x: Permissions) isOneOf (y: PermissionChoice) = (x & y) != 0
+
+  val NoPermission: Permission = 0
+  val ReadOnly: Permission = 1
+  val WriteOnly: Permission = 2
+  val ReadWrite: Permissions = ReadOnly & WriteOnly
+  val ReadOrWrite: PermissionChoice = ReadOnly | WriteOnly
+}
+
+object User {
+  import Access._
+
+  case class Item(rights: Permissions)
+
+  val x = Item(ReadOnly)  // OK, since Permission <: Permissions
+
+  assert( x.rights.is(ReadWrite) == false )
+  assert( x.rights.isOneOf(ReadOrWrite) == true )
+
+  // Would be a type error:
+  //   assert( x.rights.isOneOf(ReadWrite) == true )
+
+}
+
+object o {
+  opaque type T = Int
+  val x: Int = id(1)
+  val y: Int = identity(1)
+}
+def id(x: o.T): o.T = x
diff --git a/tests/run/i5455.scala b/tests/run/i5455.scala
index ba3a71ec587e..5e242e55a13f 100644
--- a/tests/run/i5455.scala
+++ b/tests/run/i5455.scala
@@ -9,11 +9,11 @@ object Library {
     }
     def times(x: Nat, y: Nat): Nat = x * y
     def toInt(n: Nat): Int = n
+  }
 
-    implicit class NatOps(val self: Nat) extends AnyVal {
-      def *(other: Nat): Nat = self * other
-      def toInt: Int = self.asInstanceOf
-    }
+  implicit class NatOps(val self: Nat) extends AnyVal {
+    def *(other: Nat): Nat = self * other
+    def toInt: Int = self.asInstanceOf
   }
 }
 
@@ -32,5 +32,5 @@ object Test extends App {
   assert(c.toInt == 6)
 
   def double1(n: Nat): Nat = n * Nat(2)
-  def double2(n: Nat): Nat = Nat.NatOps(n) * Nat(2)
+  def double2(n: Nat): Nat = NatOps(n) * Nat(2)
 }
\ No newline at end of file
diff --git a/tests/run/i5527.scala b/tests/run/i5527.scala
index 893938f94f48..bd3f4b37e4d3 100644
--- a/tests/run/i5527.scala
+++ b/tests/run/i5527.scala
@@ -9,16 +9,15 @@ object Library {
   object Set {
     def singleton[A](a: A): Set[A] =
       _ == a
+  }
 
-    implicit class SetOps[A](private val set: Set[A]) extends AnyVal {
-      def contains(a: A): Boolean =
-        set(a)
-    }
+  implicit class SetOps[A](private val set: Set[A]) extends AnyVal {
+    def contains(a: A): Boolean = set(a)
+  }
 
-    implicit val setContravariant: Contravariant[Set] = new Contravariant[Set] {
-      def contramap[A, B](fa: Set[A])(f: B => A): Set[B] =
-        b => fa(f(b))
-    }
+  implicit val setContravariant: Contravariant[Set] = new Contravariant[Set] {
+    def contramap[A, B](fa: Set[A])(f: B => A): Set[B] =
+      b => fa(f(b))
   }
 }
 
diff --git a/tests/run/implied-priority.scala b/tests/run/implied-priority.scala
index 9e3a32b31b96..1e7b83f376a3 100644
--- a/tests/run/implied-priority.scala
+++ b/tests/run/implied-priority.scala
@@ -127,13 +127,13 @@ def test4 = {
  *
  * It employs a more re-usable version of the result refinement trick.
  */
-opaque type HigherPriority = Any
 object HigherPriority {
-  def inject[T](x: T): T & HigherPriority = x
+  opaque type Type = Any
+  def inject[T](x: T): T & Type = x
 }
 
 object fallback5 {
-  implied [T] for (E[T] & HigherPriority) given (ev: E[T] = new E[T]("fallback")) = HigherPriority.inject(ev)
+  implied [T] for (E[T] & HigherPriority.Type) given (ev: E[T] = new E[T]("fallback")) = HigherPriority.inject(ev)
 }
 
 def test5 = {