diff --git a/compiler/src/dotty/tools/dotc/ast/Desugar.scala b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
index 3b27999cad35..2dce3a424914 100644
--- a/compiler/src/dotty/tools/dotc/ast/Desugar.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
@@ -310,6 +310,7 @@ object desugar {
     val isEnum = mods.isEnumClass && !mods.is(Module)
     def isEnumCase = mods.isEnumCase
     val isValueClass = parents.nonEmpty && isAnyVal(parents.head)
+    val dependentFlag = if (mods.is(Dependent)) Dependent else EmptyFlags
       // This is not watertight, but `extends AnyVal` will be replaced by `inline` later.
 
     val originalTparams = constr1.tparams
@@ -423,7 +424,7 @@ object desugar {
     // two errors without @uncheckedVariance, one of them spurious.
     val caseClassMeths = {
       def syntheticProperty(name: TermName, rhs: Tree) =
-        DefDef(name, Nil, Nil, TypeTree(), rhs).withMods(synthetic)
+        DefDef(name, Nil, Nil, TypeTree(), rhs).withMods(synthetic | dependentFlag)
       def productElemMeths = {
         val caseParams = constrVparamss.head.toArray
         for (i <- 0 until arity if nme.selectorName(i) `ne` caseParams(i).name)
@@ -553,12 +554,12 @@ object desugar {
           if (mods is Abstract) Nil
           else
             DefDef(nme.apply, derivedTparams, derivedVparamss, applyResultTpt, widenedCreatorExpr)
-              .withFlags(Synthetic | (constr1.mods.flags & DefaultParameterized)) :: widenDefs
+              .withFlags(Synthetic | dependentFlag | (constr1.mods.flags & DefaultParameterized)) :: widenDefs
         val unapplyMeth = {
           val unapplyParam = makeSyntheticParameter(tpt = classTypeRef)
           val unapplyRHS = if (arity == 0) Literal(Constant(true)) else Ident(unapplyParam.name)
           DefDef(nme.unapply, derivedTparams, (unapplyParam :: Nil) :: Nil, TypeTree(), unapplyRHS)
-            .withMods(synthetic)
+            .withMods(synthetic | dependentFlag)
         }
         companionDefs(companionParent, applyMeths ::: unapplyMeth :: companionMembers)
       }
diff --git a/compiler/src/dotty/tools/dotc/ast/Trees.scala b/compiler/src/dotty/tools/dotc/ast/Trees.scala
index e7fea191eeb7..896716e5531f 100644
--- a/compiler/src/dotty/tools/dotc/ast/Trees.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Trees.scala
@@ -228,8 +228,9 @@ object Trees {
                 case y: List[_] => x.corresponds(y)(isSame)
                 case _ => false
               }
+            case x: Constant => x == y
             case _ =>
-              false
+              throw new AssertionError(s"Unexpected Tree in Tree comparison $x (comparing to $y)")
           }
         }
       this.getClass == that.getClass && {
@@ -623,7 +624,7 @@ object Trees {
    */
   class TypeVarBinder[-T >: Untyped] extends TypeTree[T]
 
-  /** ref.type */
+  /** ref.type  or  { ref } */
   case class SingletonTypeTree[-T >: Untyped] private[ast] (ref: Tree[T])
     extends DenotingTree[T] with TypTree[T] {
     type ThisTree[-T >: Untyped] = SingletonTypeTree[T]
@@ -1243,7 +1244,7 @@ object Trees {
           case TypeTree() =>
             tree
           case SingletonTypeTree(ref) =>
-            cpy.SingletonTypeTree(tree)(transform(ref))
+            cpy.SingletonTypeTree(tree)(transform(ref)(ctx.enterTypeOf()))
           case AndTypeTree(left, right) =>
             cpy.AndTypeTree(tree)(transform(left), transform(right))
           case OrTypeTree(left, right) =>
diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala
index ec0884e6ee99..8a9383aeace2 100644
--- a/compiler/src/dotty/tools/dotc/ast/tpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala
@@ -570,7 +570,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
     override def If(tree: Tree)(cond: Tree, thenp: Tree, elsep: Tree)(implicit ctx: Context): If = {
       val tree1 = untpd.cpy.If(tree)(cond, thenp, elsep)
       tree match {
-        case tree: If if (thenp.tpe eq tree.thenp.tpe) && (elsep.tpe eq tree.elsep.tpe) => tree1.withTypeUnchecked(tree.tpe)
+        case tree: If if (cond.tpe eq tree.cond.tpe) && (thenp.tpe eq tree.thenp.tpe) && (elsep.tpe eq tree.elsep.tpe) => tree1.withTypeUnchecked(tree.tpe)
         case _ => ta.assignType(tree1, thenp, elsep)
       }
     }
@@ -587,7 +587,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
     override def Match(tree: Tree)(selector: Tree, cases: List[CaseDef])(implicit ctx: Context): Match = {
       val tree1 = untpd.cpy.Match(tree)(selector, cases)
       tree match {
-        case tree: Match if sameTypes(cases, tree.cases) => tree1.withTypeUnchecked(tree.tpe)
+        case tree: Match if (selector.tpe eq tree.selector.tpe) && sameTypes(cases, tree.cases) => tree1.withTypeUnchecked(tree.tpe)
         case _ => ta.assignType(tree1, cases)
       }
     }
diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala
index b2278088a6c8..87103fd8c365 100644
--- a/compiler/src/dotty/tools/dotc/ast/untpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala
@@ -137,6 +137,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
     case class Transparent() extends Mod(Flags.Transparent)
 
     case class Enum() extends Mod(Flags.Enum)
+
+    case class Dependent() extends Mod(Flags.Dependent)
   }
 
   /** Modifiers and annotations for definitions
diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index a8d09ba7b6d8..85069bd4c733 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -6,6 +6,7 @@ object Config {
   final val cacheAsSeenFrom = true
   final val cacheMemberNames = true
   final val cacheImplicitScopes = true
+  final val cacheNormalizedTypes = true
 
   final val checkCacheMembersNamed = false
 
diff --git a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
index ed113a73cb23..7d60b43fa0d7 100644
--- a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
+++ b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
@@ -146,6 +146,8 @@ class ScalaSettings extends Settings.SettingGroup {
 
   val YnoDecodeStacktraces = BooleanSetting("-Yno-decode-stacktraces", "Show raw StackOverflow stacktraces, instead of decoding them into triggering operations.")
 
+  val YtypeNormalizationFuel = IntSetting("-Ytype-normalization-fuel", "Maximal number of steps when evaluating type expressions.", 2222222)
+
   /** Dottydoc specific settings */
   val siteRoot = StringSetting(
     "-siteroot",
@@ -154,7 +156,6 @@ class ScalaSettings extends Settings.SettingGroup {
     sys.props("user.dir")
   )
 
-
   val projectName = StringSetting (
     "-project",
     "project title",
diff --git a/compiler/src/dotty/tools/dotc/core/Annotations.scala b/compiler/src/dotty/tools/dotc/core/Annotations.scala
index 6138b63ea8ac..5934047b306d 100644
--- a/compiler/src/dotty/tools/dotc/core/Annotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/Annotations.scala
@@ -32,6 +32,7 @@ object Annotations {
       for (ConstantType(c) <- argument(i) map (_.tpe)) yield c
 
     def isEvaluated: Boolean = true
+    def isEvaluating: Boolean = false
 
     def ensureCompleted(implicit ctx: Context): Unit = tree
 
@@ -85,6 +86,7 @@ object Annotations {
       myBody
     }
     override def isEvaluated = evaluated
+    override def isEvaluating = evaluated && myBody == null
   }
 
   object Annotation {
@@ -170,8 +172,10 @@ 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
-          Some(arg.symbol)
+          ann.tree.tpe match { // TODO: proper fix
+            case AppliedType(tycon, (arg: NamedType) :: Nil) => Some(arg.symbol)
+            case _ => None
+          }
         }
         else None
     }
diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala
index a80d25e16b04..ee3de5b898b5 100644
--- a/compiler/src/dotty/tools/dotc/core/Contexts.scala
+++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala
@@ -116,6 +116,11 @@ object Contexts {
     protected def owner_=(owner: Symbol) = _owner = owner
     def owner: Symbol = _owner
 
+    /** The owner at the point of entering TypeOf (for SingletonTypeTrees) */
+    private[this] var _inTypeOfOwner: Symbol = _
+    protected def inTypeOfOwner_=(owner: Symbol) = _inTypeOfOwner = owner
+    def inTypeOfOwner: Symbol = _inTypeOfOwner
+
     /** The current tree */
     private[this] var _tree: Tree[_ >: Untyped]= _
     protected def tree_=(tree: Tree[_ >: Untyped]) = _tree = tree
@@ -162,6 +167,32 @@ object Contexts {
       _typeComparer
     }
 
+    /** Is this context dependent? */
+    private[this] var _dependentInit: Boolean = true // NOTE: This initial value only applies to InitialContext
+    private[this] var _dependent: Boolean = false
+    final def isDependent: Boolean = {
+      def isDepOwner(owner: Symbol): Boolean =
+        if ((owner eq NoSymbol) || owner.isClass) false
+        else if (owner.flagsUNSAFE.is(Flags.Dependent)) true
+        else isDepOwner(owner.owner)
+
+      /** NOTE: The initialization of `_dependent` is rather tricky: We do need to make sure that any
+        *       enclosing context's `_dependent` has been computed, since the property is inherited. In case the
+        *       outer's `dependent` has been accessed before, we inherit the value by way of clone() in fresh(),
+        *       (and as a result `_dependentInit` will be true as well).
+        *       Otherwise we force the enclosing context's `_dependent` here, and, if the outer turns out not to be
+        *       dependent, we finally also compute `_dependent` based on this context.
+        */
+      if (!_dependentInit) {
+        _dependent = this.isInTypeOf || isDepOwner(this.owner)
+        _dependentInit = true
+      }
+      _dependent
+    }
+
+    final def isInTypeOf: Boolean =
+      this.inTypeOfOwner == this.owner
+
     /** A map in which more contextual properties can be stored
      *  Typically used for attributes that are read and written only in special situations.
      */
@@ -411,6 +442,9 @@ object Contexts {
       this.phasedCtxs = null
       // See comment related to `creationTrace` in this file
       // setCreationTrace()
+      // The _dependent member was cloned, but is monotonic anyways, so we *could* only recompute in case
+      // _dependentInit is false, but it turns out that branching here is very costly.
+      this._dependentInit = false
       this
     }
 
@@ -475,6 +509,7 @@ object Contexts {
     def setPeriod(period: Period): this.type = { this.period = period; this }
     def setMode(mode: Mode): this.type = { this.mode = mode; this }
     def setOwner(owner: Symbol): this.type = { assert(owner != NoSymbol); this.owner = owner; this }
+    def enterTypeOf(): this.type = { assert(this.owner != NoSymbol); this.inTypeOfOwner = this.owner; this }
     def setTree(tree: Tree[_ >: Untyped]): this.type = { this.tree = tree; this }
     def setScope(scope: Scope): this.type = { this.scope = scope; this }
     def setNewScope: this.type = { this.scope = newScope; this }
@@ -539,6 +574,8 @@ object Contexts {
     final def addMode(mode: Mode): Context = withModeBits(c.mode | mode)
     final def maskMode(mode: Mode): Context = withModeBits(c.mode & mode)
     final def retractMode(mode: Mode): Context = withModeBits(c.mode &~ mode)
+
+    final def enterTypeOf(): Context = if (c.isInTypeOf) c else c.fresh.enterTypeOf()
   }
 
   implicit class FreshModeChanges(val c: FreshContext) extends AnyVal {
@@ -613,6 +650,7 @@ object Contexts {
     def initialize()(implicit ctx: Context): Unit = {
       _platform = newPlatform
       definitions.init()
+      typeNormalizationFuel = settings.YtypeNormalizationFuel.value
     }
 
     def squashed(p: Phase): Phase = {
@@ -712,6 +750,8 @@ object Contexts {
     def checkSingleThreaded() =
       if (thread == null) thread = Thread.currentThread()
       else assert(thread == Thread.currentThread(), "illegal multithreaded access to ContextBase")
+
+    private[dotc] var typeNormalizationFuel: Int = 0
   }
 
   class GADTMap(initBounds: SimpleIdentityMap[Symbol, TypeBounds]) {
diff --git a/compiler/src/dotty/tools/dotc/core/Flags.scala b/compiler/src/dotty/tools/dotc/core/Flags.scala
index 41ab40f36acc..2722b98d6472 100644
--- a/compiler/src/dotty/tools/dotc/core/Flags.scala
+++ b/compiler/src/dotty/tools/dotc/core/Flags.scala
@@ -369,6 +369,9 @@ object Flags {
   /** Labeled with `erased` modifier (erased value)  */
   final val Erased = termFlag(42, "erased")
 
+  /** Labelled with `dependent` modifier */
+  final val Dependent = commonFlag(43, "dependent")
+
   // Flags following this one are not pickled
 
   /** Symbol is not a member of its owner */
@@ -436,7 +439,7 @@ object Flags {
 
   /** Flags representing source modifiers */
   final val SourceModifierFlags =
-    commonFlags(Private, Protected, Abstract, Final, Rewrite | Transparent,
+    commonFlags(Private, Protected, Abstract, Final, Rewrite | Transparent, Dependent,
      Sealed, Case, Implicit, Override, AbsOverride, Lazy, JavaStatic, Erased)
 
   /** Flags representing modifiers that can appear in trees */
@@ -457,7 +460,7 @@ object Flags {
     Scala2ExistentialCommon | Mutable.toCommonFlags | Touched | JavaStatic |
     CovariantOrOuter | ContravariantOrLabel | CaseAccessor.toCommonFlags |
     NonMember | ImplicitCommon | Permanent | Synthetic |
-    SuperAccessorOrScala2x | Rewrite | Transparent
+    SuperAccessorOrScala2x | Rewrite | Transparent | Dependent
 
   /** Flags that are not (re)set when completing the denotation, or, if symbol is
    *  a top-level class or object, when completing the denotation once the class
@@ -551,8 +554,8 @@ object Flags {
   /** Assumed to be pure */
   final val StableOrErased = Stable | Erased
 
-  /** Labeled `private`, `final`, `rewrite` or `transparent` */
-  final val EffectivelyFinal = Private | Final | Rewrite | Transparent
+  /** Labeled `private`, `final`, or `transparent` */
+  final val EffectivelyFinal = Private | Final | Rewrite | Transparent | Dependent
 
   /** A private method */
   final val PrivateMethod = allOf(Private, Method)
@@ -566,6 +569,12 @@ object Flags {
   /** A rewrite method */
   final val RewriteMethod = allOf(Rewrite, Method)
 
+  /** A dependent method */
+  final val DependentMethod = allOf(Dependent, Method)
+
+  /** A transparent implicit method */
+  final val TransparentImplicitMethod = allOf(Transparent, Rewrite, Implicit, Method)
+
   /** An implicit rewrite method */
   final val ImplicitRewriteMethod = allOf(Rewrite, Implicit, Method)
 
diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala
index 9dc4e92df3f7..b24045e56f77 100644
--- a/compiler/src/dotty/tools/dotc/core/Mode.scala
+++ b/compiler/src/dotty/tools/dotc/core/Mode.scala
@@ -100,4 +100,7 @@ object Mode {
 
   /** Read comments from definitions when unpickling from TASTY */
   val ReadComments = newMode(22, "ReadComments")
+
+  /** We are in TypeOf, e.g. to type a SingletonTypeTree or to compute a derived TypeOf */
+  val InTypeOf = newMode(23, "InTypeOf")
 }
diff --git a/compiler/src/dotty/tools/dotc/core/Normalize.scala b/compiler/src/dotty/tools/dotc/core/Normalize.scala
new file mode 100644
index 000000000000..abe7a24c4446
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/core/Normalize.scala
@@ -0,0 +1,278 @@
+package dotty.tools
+package dotc
+package core
+
+import config.Config
+import Contexts._
+import Decorators._
+import Denotations._
+import Flags._
+import Names._
+import Symbols._
+import Types._
+import reporting.trace
+import reporting.diagnostic.Message
+import typer.Inferencing._
+import typer.ErrorReporting.errorType
+import typer.ForceDegree
+import ast.tpd._
+import scala.annotation.tailrec
+import scala.collection.mutable
+import scala.annotation.internal.sharable
+
+object Normalize {
+  @sharable var track = true
+}
+
+private final class NormalizeMap(implicit ctx: Context) extends TypeMap {
+  private[this] var canReduce: Boolean = true
+
+  /** To be called in branches that correspond to the evaluation context in which evaluation gets stuck.
+    * For instance, if after applying the congruence rule of `if` we have not reduced the conditional to either
+    * true or false, we cannot apply any further rules, i.e., we get stuck.
+    * //In auxiliary methods (i.e. outside `apply`) we may return `NoType` to indicate that the type has remained
+    * //unchanged.
+    */
+  private def Stuck(at: Type): Type = {
+    canReduce = false
+    at
+  }
+
+  /** To be called in branches that did not match any rule. The returned value will be caught in the calling
+    * context (i.e. `NormalizeMap#apply`) and allow others rules to be tried.
+    */
+  private def NotApplicable: Type = NoType
+
+  /** Get the normalized form of a type or force and cache its computation */
+  private def normalizedType(tp: Type): Type =
+    if (Config.cacheNormalizedTypes) {
+      assert(canReduce, "Trying to compute normalized type in an already stuck state")
+      assert(tp._myNormalized != null, i"Cyclic normalization of $tp")
+      if (tp._myNormalized eq NoType) {
+        tp._myNormalized = null
+        tp._myNormalized = bigStep(tp)
+        tp._myNormalizedStuck = canReduce
+      }
+      canReduce = tp._myNormalizedStuck
+      tp._myNormalized
+    } else {
+      bigStep(tp)
+    }
+
+  /** Infrastructure for beta-reduction at the type-level, to be cached per dependent method. */
+  class Unfolder(fnSym: Symbol, body: Tree) {
+    private[this] val paramPos = mutable.ArrayBuffer[Name]()
+    private[this] var params: Array[Symbol] = _
+
+    private def computeParamPositions(tp: Type): Unit = tp match {
+      case tp: MethodOrPoly =>
+        paramPos ++= tp.paramNames
+        computeParamPositions(tp.resultType)
+      case _ =>
+    }
+
+    private def computeOrderedParams = {
+      def registerType(tp: Type): Unit = tp match {
+        case tp: NamedType if tp.symbol.is(Param) && tp.symbol.owner == fnSym =>
+          params(paramPos.indexOf(tp.name)) = tp.symbol
+        case _ =>
+      }
+
+      params = Array.fill[Symbol](paramPos.length)(NoSymbol)
+      body.tpe.foreachPart(registerType, stopAtStatic = true)
+    }
+
+    /** Performs beta-reduction for a given list of arguments, as seen from the given prefix. */
+    def unfold(pre: Type, args: List[Type]): Type = {
+      @tailrec def substPairs(paramPos: Int, args: List[Type],
+                              from: List[Symbol], to: List[Type]): (List[Symbol], List[Type]) =
+        if (paramPos == params.length)
+          (from, to)
+        else
+          if (params(paramPos).exists) substPairs(paramPos + 1, args.tail, params(paramPos) :: from, args.head :: to)
+          else                         substPairs(paramPos + 1, args.tail, from, to)
+
+      assert(args.length == params.length)
+      val (from, to) = substPairs(0, args, Nil, Nil)
+      body.tpe.subst(from, to).asSeenFrom(pre, fnSym.enclosingClass)  // TODO: Check whether enclosingClass makes sense
+    }
+
+    // TODO: Cache this per dependent method
+    computeParamPositions(fnSym.info)
+    computeOrderedParams
+  }
+
+  private def assertOneArg(argss: List[List[Type]]): Unit =
+    assert(argss.length == 1 && argss.head.length == 1, i"Expected one argument, got: $argss")
+
+  private def asType(b: Boolean) = ConstantType(Constants.Constant(b))
+
+  // actual.isInstanceOf[testedTp], where actualTp and testedTp are erased
+  private def typeTest(actualTp: Type, testedTp: Type): Option[Boolean] = {
+    val actualCls = actualTp.classSymbol
+    val testedCls = testedTp.classSymbol
+    if (!actualCls.isClass || !testedCls.isClass)         None
+    else if (!isFullyDefined(actualTp, ForceDegree.none)) None // Approximating for now... // TODO: does this even make sense on erased types?
+    else if (!isFullyDefined(testedTp, ForceDegree.none)) None
+    else if (actualTp.derivesFrom(testedCls))             Some(true)
+    else if (testedTp.derivesFrom(actualCls))             None
+    else                                                  Some(false)
+  }
+
+  /** The body type of dependent method `sym` if the body itself is not currently being type-checked,
+    * error otherwise.
+    */
+  private def defUnfolder(fnSym: Symbol): Unfolder = {
+    assert(fnSym.isTerm && fnSym.isDependentMethod && fnSym.hasAnnotation(defn.BodyAnnot), s"Tried to illegally unfold $fnSym with flags")
+    val body: Tree = fnSym.getAnnotation(defn.BodyAnnot) match {
+      case Some(annot) =>
+        if (annot.isEvaluating)
+          throw CyclicReference(fnSym)  // TODO: Better error message?
+        annot.tree
+      case None =>
+        throw new AssertionError(s"Expected dependent method $fnSym to have a body annotation!")
+    }
+    new Unfolder(fnSym, body)
+  }
+
+  /** Normalizes applications of various kinds:
+    *  - If `fn` is a unary or binary method of a value class, perform constant-folding.
+    *  - If `fn` is a dependent method, beta-reduce.
+    *  - If `tp` is `pre.isInstanceOf[T]` and `pre: S`, evaluate to the outcome of `erased(S) <: erased(T)`.
+    *    In case the result is not yet determined, get stuck.
+    *  - If `tp` is `pre.asInstanceOf[T]` and `pre: S`, evaluate to `pre` if `erased(S) <: erased(T)`.
+    *    In case the result is not yet determined or the subtype-relation simply doesn't hold, get stuck.
+    * @param tp  The original application type before decomposition into `fn` and `argss`.
+    * @param fn  The method referred to by `tp`.
+    * @param argss  The list of arguments lists of `tp`.
+    * @return The reduced application, if applicable, NoType otherwise.
+    */
+  private def normalizeApp(tp: Type, fn: TermRef, argss: List[List[Type]]): Type = {
+    import dotc.typer.ConstFold
+
+    val realApplication = tp ne fn
+    val fnSym = fn.symbol
+    // TODO: Replace `Stable` requirement by some other special case
+    if (fnSym.is(Method)) {
+      if (defn.ScalaValueClasses().contains(fnSym.owner) || fnSym == defn.Any_== || fnSym == defn.Any_!=) {
+        argss match {
+          case List() if realApplication => ConstFold(fn)
+          case List(List(arg))           => ConstFold(fn, arg)
+          case _                         => NoType  // TODO: error/stuck/impossible?
+        }
+      }
+      else if (fnSym.isDependentMethod) {
+        // Semantically, this is what we want to do:
+        // if (fnSym.isCompleting)
+        //   if (ctx.isDependent) Stuck(tp)
+        //   else throw CyclicReference(fnSym)
+        // else { ... }
+
+        // Reduction step
+        // TODO(gsps): Also reduce if fnSym's finalResultType is singleton (or do this in TypeAssigner?)
+        val unfolder = defUnfolder(fnSym)
+        if (realApplication || fnSym.info.isInstanceOf[ExprType])
+          apply(unfolder.unfold(fn.prefix, argss.flatten))
+        else
+          NotApplicable
+      }
+      else if (realApplication && ((fnSym eq defn.Any_isInstanceOf) || (fnSym eq defn.Any_asInstanceOf))) {
+        import TypeErasure.erasure
+        assertOneArg(argss)
+        val isSubTypeOpt = typeTest(erasure(fn.prefix), erasure(argss.head.head))
+        if (fnSym eq defn.Any_isInstanceOf)
+          isSubTypeOpt map asType getOrElse Stuck(tp)
+        else
+          isSubTypeOpt match {
+            case Some(true) => apply(fn.prefix)
+            case _          => Stuck(tp)
+          }
+      }
+      else NotApplicable
+    }
+    else NotApplicable
+  }
+
+  private def normalizeTermParamSel(tp: TermRef): Type = {
+    def selectTermParam(cnstrSym: Symbol, args: List[Type]): Type =
+      cnstrSym.info.widen.stripMethodPrefix match {
+        case m: MethodType =>
+          m.paramNamess.flatten.indexOf(tp.name) match {
+            case -1 => throw new AssertionError(s"Cannot find parameter ${tp.name} in constructor $m")
+            case index => args(index)
+          }
+        case x =>
+          throw new AssertionError("Unexpected constructor type $x")
+      }
+
+    @tailrec def revealNewAndSelect(pre: Type): Type = pre match {
+      case TypeOf.New(cnstrSym, _, args) =>
+        selectTermParam(cnstrSym, args)
+      case pre: TypeProxy =>
+        revealNewAndSelect(pre.underlying)
+      case _ =>
+        NoType  // TODO: stuck?
+    }
+
+    val sym = tp.symbol
+    if (sym.is(ParamAccessor) && sym.isStable)
+      revealNewAndSelect(tp.prefix)
+    else
+      NotApplicable
+  }
+
+  private def bigStep(tp: Type): Type = tp match {
+    case tp if tp eq defn.NullType =>
+      Stuck(tp)
+
+    case tp @ TypeOf.If(cond, thenb, elseb) =>
+      apply(cond) match {
+        case ConstantType(c) if c.tag == Constants.BooleanTag =>
+          if (c.value.asInstanceOf[Boolean]) apply(thenb)
+          else                               apply(elseb)
+        case cond1 =>
+          Stuck( TypeOf.If.derived(tp)(cond1, thenb, elseb) )
+      }
+
+    case tp @ TypeOf.Match(selector, cases) =>
+      tp  // TODO
+
+    case tp =>
+      mapOver(tp) match {
+        case _ if !canReduce =>
+          tp
+
+        case tp: TermRef =>
+          normalizeApp(tp, tp, Nil) orElse normalizeTermParamSel(tp) orElse {
+            tp.underlying match {
+              case underTp: SingletonType => apply(underTp)
+              case _ => tp  // TODO: stuck?
+            }
+          }
+
+        // Defer unfolding until all type and term arguments are known
+        case tp if !tp.widen.isInstanceOf[MethodOrPoly] =>
+          tp match {
+            case tp @ TypeOf.Call(fn, argss) =>
+              assert(argss.forall(_.forall(defn.NullType.ne)), s"Unexpected nulls in arguments: $argss")
+              normalizeApp(tp, fn, argss) orElse tp
+            case tp => tp  // TODO: stuck?
+          }
+
+        case tp =>
+//          val tp1 = tp.stripTypeVar.dealias.widenExpr
+//          if (tp eq tp1) tp else apply(tp1)
+          tp  // TODO: stuck?
+      }
+  }
+
+  def apply(tp: Type): Type = trace.conditionally(Normalize.track, i"normalize($tp)", show = true) {
+    if (ctx.base.typeNormalizationFuel == 0)
+      errorType(i"Diverged while normalizing $tp (${ctx.settings.YtypeNormalizationFuel.value} steps)", ctx.tree.pos)
+    else if (canReduce) {
+      if (ctx.base.typeNormalizationFuel > 0)
+        ctx.base.typeNormalizationFuel -= 1
+      normalizedType(tp)
+    } else tp
+  }
+}
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index 8dad726672af..d6a80eb25aba 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -781,6 +781,9 @@ object SymDenotations {
     def isTransparentMethod(implicit ctx: Context): Boolean =
       is(TransparentMethod, butNot = AccessorOrSynthetic)
 
+    def isDependentMethod(implicit ctx: Context): Boolean =
+      is(DependentMethod)
+
     def isRewriteMethod(implicit ctx: Context): Boolean =
       is(RewriteMethod, butNot = AccessorOrSynthetic)
 
@@ -800,6 +803,9 @@ object SymDenotations {
       is(Erased) ||
       isRewriteMethod && unforcedAnnotation(defn.ForceInlineAnnot).isEmpty
 
+    def requiresInlineInfo(implicit ctx: Context): Boolean =
+      isInlineable || isDependentMethod
+
     /** ()T and => T types should be treated as equivalent for this symbol.
      *  Note: For the moment, we treat Scala-2 compiled symbols as loose matching,
      *  because the Scala library does not always follow the right conventions.
@@ -1221,6 +1227,7 @@ object SymDenotations {
       case tp: LambdaType => tp.paramInfos.exists(hasSkolems) || hasSkolems(tp.resType)
       case tp: AndType => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
       case tp: OrType  => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
+      case TypeOf.Generic(args) => args.exists(hasSkolems)
       case tp: AnnotatedType => hasSkolems(tp.parent)
       case _ => false
     }
@@ -2095,20 +2102,20 @@ object SymDenotations {
   private abstract class InheritedCacheImpl(val createdAt: Period) extends InheritedCache {
     protected def sameGroup(p1: Phase, p2: Phase): Boolean
 
-    private[this] var dependent: WeakHashMap[InheritedCache, Unit] = null
+    private[this] var dependentMap: WeakHashMap[InheritedCache, Unit] = null
     private[this] var checkedPeriod: Period = Nowhere
 
     protected def invalidateDependents() = {
-      if (dependent != null) {
-        val it = dependent.keySet.iterator()
+      if (dependentMap != null) {
+        val it = dependentMap.keySet.iterator()
         while (it.hasNext()) it.next().invalidate()
       }
-      dependent = null
+      dependentMap = null
     }
 
     protected def addDependent(dep: InheritedCache) = {
-      if (dependent == null) dependent = new WeakHashMap
-      dependent.put(dep, ())
+      if (dependentMap == null) dependentMap = new WeakHashMap
+      dependentMap.put(dep, ())
     }
 
     def isValidAt(phase: Phase)(implicit ctx: Context) =
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 0f54da0573a2..a3a534394f39 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -130,7 +130,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
 
   protected def isSubType(tp1: Type, tp2: Type): Boolean = isSubType(tp1, tp2, NoApprox)
 
-  protected def recur(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)} $approx", subtyping) {
+  protected def recur(tp1Unnorm: Type, tp2Unnorm: Type): Boolean = trace(s"isSubType ${traceInfo(tp1Unnorm, tp2Unnorm)} $approx", subtyping) {
+    // TODO: Cache normalized forms
+    def normalize(tp: Type): Type = tp match {
+      case _: TermRef | _: TypeOf => ctx.normalizedType(tp)
+      case _ => tp
+    }
+    val tp1 = normalize(tp1Unnorm)
+    val tp2 = normalize(tp2Unnorm)
 
     def monitoredIsSubType = {
       if (pendingSubTypes == null) {
@@ -236,6 +243,23 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
         compareWild
       case tp2: LazyRef =>
         !tp2.evaluating && recur(tp1, tp2.ref)
+      case tp2: TypeOf =>
+        def comparePointwise(tp1norm: TypeOf) =
+          if (tp1norm.tree.getClass eq tp2.tree.getClass)
+            (tp1norm, tp2) match {
+              case (TypeOf.Generic(args1), TypeOf.Generic(args2)) =>
+                args1.zip(args2).forall { case (arg1, arg2) => recur(arg1, arg2) }
+              case _ => false
+            }
+          else
+            false
+        if (ctx.phase.id > ctx.picklerPhase.id)
+          recur(tp1, tp2.underlyingTp)
+        else
+          tp1 match {
+            case tp1: TypeOf => comparePointwise(tp1) || secondTry
+            case _ => secondTry
+          }
       case tp2: AnnotatedType if !tp2.isRefining =>
         recur(tp1, tp2.parent)
       case tp2: ThisType =>
@@ -665,6 +689,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
           case _ =>
         }
         either(recur(tp11, tp2), recur(tp12, tp2))
+      case tp1: TypeOf =>
+        recur(tp1.underlyingTp, tp2)
       case tp1: AnnotatedType if tp1.isRefining =>
         isNewSubType(tp1.parent)
       case JavaArrayType(elem1) =>
diff --git a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
index be59b0eb8849..43690a260504 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
@@ -521,7 +521,7 @@ class TypeErasure(isJava: Boolean, semiEraseVCs: Boolean, isConstructor: Boolean
         val sym = tp.symbol
         if (!sym.isClass) {
           val info = tp.info
-          if (!info.exists) assert(false, "undefined: $tp with symbol $sym")
+          if (!info.exists) assert(false, s"undefined: $tp with symbol $sym")
           return sigName(info)
         }
         if (isDerivedValueClass(sym)) {
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 91703bb22dbf..051dfc24e0e5 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -115,6 +115,14 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
     def apply(tp: Type) = simplify(tp, this)
   }
 
+  /** Normalize */
+  final def normalize(tp: Type): Type =
+    new NormalizeMap().apply(tp)
+
+  /** Normalize the type as far as possible, if we are in an opaque context before erasure. */
+  final def normalizedType(tp: Type): Type =
+    if (erasedTypes || isDependent) tp else normalize(tp)
+
   /** Approximate union type by intersection of its dominators.
    *  That is, replace a union type Tn | ... | Tn
    *  by the smallest intersection type of base-class instances of T1,...,Tn.
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 40b843cee067..22b161535506 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -21,7 +21,7 @@ import util.Stats._
 import util.{DotClass, SimpleIdentitySet}
 import reporting.diagnostic.Message
 import ast.tpd._
-import ast.TreeTypeMap
+import ast.{Trees, TreeTypeMap}
 import printing.Texts._
 import ast.untpd
 import dotty.tools.dotc.transform.Erasure
@@ -133,6 +133,10 @@ object Types {
       accu.apply(false, this)
     }
 
+    /** Normalized variant of this type */
+    @sharable private[dotc] var _myNormalized: Type = NoType
+    @sharable private[dotc] var _myNormalizedStuck: Boolean = _
+
     /** Is this type different from NoType? */
     final def exists: Boolean = this.ne(NoType)
 
@@ -305,14 +309,14 @@ object Types {
     /** Is this the type of a method that has a repeated parameter type as
      *  last parameter type?
      */
-    def isVarArgsMethod(implicit ctx: Context): Boolean = stripPoly match {
+    def isVarArgsMethod(implicit ctx: Context): Boolean = stripMethodPrefix match {
       case mt: MethodType => mt.paramInfos.nonEmpty && mt.paramInfos.last.isRepeatedParam
       case _ => false
     }
 
     /** Is this the type of a method with a leading empty parameter list?
      */
-    def isNullaryMethod(implicit ctx: Context): Boolean = stripPoly match {
+    def isNullaryMethod(implicit ctx: Context): Boolean = stripMethodPrefix match {
       case MethodType(Nil) => true
       case _ => false
     }
@@ -938,9 +942,10 @@ object Types {
       case _ => this
     }
 
-    /** Strip PolyType prefix */
-    def stripPoly(implicit ctx: Context): Type = this match {
-      case tp: PolyType => tp.resType.stripPoly
+    /** Strip PolyType and TypeOf prefix */
+    def stripMethodPrefix(implicit ctx: Context): Type = this match {
+      case tp: TypeOf => tp.underlyingTp.stripMethodPrefix
+      case tp: PolyType => tp.resType.stripMethodPrefix
       case _ => this
     }
 
@@ -955,6 +960,7 @@ object Types {
      */
     final def widen(implicit ctx: Context): Type = widenSingleton match {
       case tp: ExprType => tp.resultType.widen
+      case tp: TypeOf => tp.underlyingTp.widen
       case tp => tp
     }
 
@@ -1106,6 +1112,8 @@ object Types {
         else NoType
       case tp: AppliedType =>
         tp.superType.underlyingClassRef(refinementOK)
+      case tp: TypeOf =>
+        tp.underlying.underlyingClassRef(refinementOK)
       case tp: AnnotatedType =>
         tp.underlying.underlyingClassRef(refinementOK)
       case tp: RefinedType =>
@@ -1260,26 +1268,26 @@ object Types {
     }
 
     /** The parameter types of a PolyType or MethodType, Empty list for others */
-    final def paramInfoss(implicit ctx: Context): List[List[Type]] = stripPoly match {
+    final def paramInfoss(implicit ctx: Context): List[List[Type]] = stripMethodPrefix match {
       case mt: MethodType => mt.paramInfos :: mt.resultType.paramInfoss
       case _ => Nil
     }
 
     /** The parameter names of a PolyType or MethodType, Empty list for others */
-    final def paramNamess(implicit ctx: Context): List[List[TermName]] = stripPoly match {
+    final def paramNamess(implicit ctx: Context): List[List[TermName]] = stripMethodPrefix match {
       case mt: MethodType => mt.paramNames :: mt.resultType.paramNamess
       case _ => Nil
     }
 
 
     /** The parameter types in the first parameter section of a generic type or MethodType, Empty list for others */
-    final def firstParamTypes(implicit ctx: Context): List[Type] = stripPoly match {
+    final def firstParamTypes(implicit ctx: Context): List[Type] = stripMethodPrefix match {
       case mt: MethodType => mt.paramInfos
       case _ => Nil
     }
 
-    /** Is this either not a method at all, or a parameterless method? */
-    final def isParameterless(implicit ctx: Context): Boolean = stripPoly match {
+    /** Is this either not a method at all, or a method without value parameters? */
+    final def isParameterless(implicit ctx: Context): Boolean = stripMethodPrefix match {
       case mt: MethodType => false
       case _ => true
     }
@@ -1290,7 +1298,7 @@ object Types {
     /** The final result type of a PolyType, MethodType, or ExprType, after skipping
      *  all parameter sections, the type itself for all others.
      */
-    def finalResultType(implicit ctx: Context): Type = resultType.stripPoly match {
+    def finalResultType(implicit ctx: Context): Type = resultType.stripMethodPrefix match {
       case mt: MethodType => mt.resultType.finalResultType
       case _ => resultType
     }
@@ -3741,7 +3749,7 @@ object Types {
 
     override def underlying(implicit ctx: Context): Type = parent
 
-    def derivedAnnotatedType(parent: Type, annot: Annotation) =
+    def derivedAnnotatedType(parent: Type, annot: Annotation)(implicit ctx: Context) =
       if ((parent eq this.parent) && (annot eq this.annot)) this
       else AnnotatedType(parent, annot)
 
@@ -3877,7 +3885,7 @@ object Types {
   object SAMType {
     def zeroParamClass(tp: Type)(implicit ctx: Context): Type = tp match {
       case tp: ClassInfo =>
-        def zeroParams(tp: Type): Boolean = tp.stripPoly match {
+        def zeroParams(tp: Type): Boolean = tp.stripMethodPrefix match {
           case mt: MethodType => mt.paramInfos.isEmpty && !mt.resultType.isInstanceOf[MethodType]
           case et: ExprType => true
           case _ => false
@@ -3963,6 +3971,285 @@ object Types {
       else None
   }
 
+  // ----- TypeOf -------------------------------------------------------------------------
+
+  /** Type that represents the precise type of a given term.
+   *  Precision is only kept for Apply, TypeApply, If and Match trees.
+   *
+   *  The idea behind this type is to be able to compute more precise types
+   *  when more information is available.
+   *
+   *  TypeOfs are represented by an underlying type and a tree. The top level
+   *  node of the tree must be one of the nodes mentioned above, and is only
+   *  used as a "marker" node, meaning that we will never look at its type.
+   *
+   *  In a sense, TypeOf types are isomorphic to the following 4 types:
+   *
+   *  TypeOf(u, Apply(fun, args))       ~ SuspendedApply(u, fun, args)
+   *  TypeOf(u, TypeApply(fun, args))   ~ SuspendedTypeApply(u, fun, args)
+   *  TypeOf(u, If(cond, thenp, elsep)) ~ SuspendedIf(u, cond, thenp, elsep)
+   *  TypeOf(u, Match(selector, cases)) ~ SuspendedMatch(u, selector, cases)
+   *
+   *  Where u is the type that the tree would have had otherwise.
+   *
+   *  It should be the case that whenever two TypeOfs are equal, so are their
+   *  underlying types.
+   */
+  abstract class TypeOf protected (val underlyingTp: Type, val tree: Tree) extends CachedProxyType with ValueType {
+    assert(TypeOf.isLegalTopLevelTree(tree), s"Illegal top-level tree in TypeOf: $tree")
+
+    override def underlying(implicit ctx: Context): Type = underlyingTp
+
+    override def iso(that: Any, bs: BinderPairs): Boolean = false  // TODO?
+
+    override def equals(that: Any): Boolean = that == null
+
+    override def eql(that: Type): Boolean = {
+      that match {
+        case that: TypeOf =>
+          @tailrec
+          def compareArgs[T <: Tree](args1: List[T], args2: List[T]): Boolean =
+            args1 match {
+              case head1 :: tail1 =>
+                args2 match {
+                  case head2 :: tail2 => head1.tpe.eql(head2.tpe) && compareArgs(tail1, tail2)
+                  case nil => false
+                }
+              case nil => args2.isEmpty
+            }
+          (this.tree, that.tree) match {
+            case (t1: Apply, t2: Apply) =>
+              (t1.fun.tpe eql t2.fun.tpe) && compareArgs(t1.args, t2.args)
+            case (t1: TypeApply, t2: TypeApply) =>
+              (t1.fun.tpe eql t2.fun.tpe) && compareArgs(t1.args, t2.args)
+            case (t1: If, t2: If) =>
+              (t1.cond.tpe eql t2.cond.tpe) && (t1.thenp.tpe eql t2.thenp.tpe) && (t1.elsep.tpe eql t2.elsep.tpe)
+            case (t1: Match, t2: Match) =>
+              (t1.selector.tpe eql t2.selector.tpe) && compareArgs(t1.cases, t2.cases)
+            case (t1, t2) =>
+              false
+          }
+        case _ => false
+      }
+    }
+
+    override def toString(): String = s"TypeOf($underlyingTp, $tree)"
+
+    override def computeHash(bs: Hashable.Binders) = {
+      val delta = tree match {
+        case _: If        => 11
+        case _: Match     => 17
+        case _: Apply     => 23
+        case _: TypeApply => 29
+      }
+      this match {
+        case TypeOf.Generic(tp :: tps) =>
+          addDelta(doHash(bs, tp, tps), delta)
+      }
+    }
+  }
+
+  final class CachedTypeOf(underlyingTp: Type, tree: Tree) extends TypeOf(underlyingTp, tree)
+
+  object TypeOf {
+    import typer.ProtoTypes.dummyTreeOfType
+
+    def apply(underlyingTp: Type, tree: untpd.Tree)(implicit ctx: Context): TypeOf = {
+      assert(!ctx.erasedTypes)
+      val tree1 = tree.clone.asInstanceOf[Tree]
+      // This is a safety net to keep us from touching a TypeOf's tree's type.
+      // Assuming we never look at this type, it would be safe to simply reuse
+      // tree without cloning. The invariant is currently enforced in Ycheck.
+      // To disable this safety net we will also have to update the pickler
+      // to ignore the type of the TypeOf tree's.
+      tree1.overwriteType(NoType)
+      unique(new CachedTypeOf(underlyingTp, tree1))
+    }
+
+    def unapply(to: TypeOf): Option[(Type, Tree)] = Some((to.underlyingTp, to.tree))
+
+    def isLegalTopLevelTree(tree: Tree): Boolean = tree match {
+      case _: TypeApply | _: Apply | _: If | _: Match => true
+      case _ => false
+    }
+
+    private def treeWithTpe[ThisTree <: Tree](tree: ThisTree, tp: Type): ThisTree =
+      if (tree.tpe eq tp) tree else tree.withTypeUnchecked(tp).asInstanceOf[ThisTree]
+
+    private def treesWithTpes[ThisTree <: Tree](trees: List[ThisTree], tps: List[Type]): List[ThisTree] = {
+      assert(tps.length == trees.length)
+      var currentType = tps
+      trees.mapConserve[ThisTree] { tree =>
+        val tp      = currentType.head
+        currentType = currentType.tail
+        if (tree.tpe eq tp) tree else tree.withTypeUnchecked(tp).asInstanceOf[ThisTree]
+      }
+    }
+
+    private def finalizeDerived(tp: TypeOf, tree1: Tree)(implicit ctx: Context): Type =
+      if (tp.tree ne tree1) {
+        assert(tp.underlyingTp.exists || tree1.tpe.exists,
+          i"Derived TypeOf's type of $tree1: ${tree1.tpe} became NoType")
+        assert(tree1.tpe.isError || tree1.tpe.isInstanceOf[TypeOf],
+          i"Derived TypeOf's type of $tree1: ${tree1.tpe} is not a TypeOf")
+        tree1.tpe
+      } else
+        tp
+
+    object If {
+      def apply(underlyingTp: Type, condTp: Type, thenTp: Type, elseTp: Type)(implicit ctx: Context): TypeOf =
+        TypeOf(underlyingTp, untpd.If(
+          dummyTreeOfType(condTp),
+          dummyTreeOfType(thenTp),
+          dummyTreeOfType(elseTp)
+        ))
+
+      def unapply(to: TypeOf): Option[(Type, Type, Type)] = to.tree match {
+        case Trees.If(cond, thenb, elseb) => Some((cond.tpe, thenb.tpe, elseb.tpe))
+        case _ => None
+      }
+
+      def derived(to: TypeOf)(condTp: Type, thenTp: Type, elseTp: Type)(implicit ctx: Context): Type =
+        finalizeDerived(to, to.tree match {
+          case Trees.If(cond, thenp, elsep) =>
+            cpy.If(to.tree)(
+              treeWithTpe(cond, condTp),
+              treeWithTpe(thenp, thenTp),
+              treeWithTpe(elsep, elseTp)
+            )(ctx.enterTypeOf())
+        })
+    }
+
+    object Match {
+      def apply(underlyingTp: Type, selectorTp: Type, caseTps: List[Type])(implicit ctx: Context): TypeOf =
+        ???.asInstanceOf[TypeOf] // TODO
+
+      def unapply(to: TypeOf): Option[(Type, List[Type])] = to.tree match {
+        case Trees.Match(selector, cases) =>
+          // TODO: We only look at .body.tpe for now, eventually we should
+          // also take the guard and the pattern into account. (see also Generic.unapply below)
+          Some((selector.tpe, cases.map(_.body.tpe)))
+        case _ => None
+      }
+
+      def derived(to: TypeOf)(selectorTp: Type, caseTps: List[Type])(implicit ctx: Context): Type =
+        finalizeDerived(to, to.tree match {
+          case Trees.Match(selector, cases) =>
+            cpy.Match(to.tree)(treeWithTpe(selector, selectorTp), treesWithTpes(cases, caseTps))(ctx.enterTypeOf())
+        })
+    }
+
+    object Apply {
+      def apply(underlyingTp: Type, funTp: Type, argTps: List[Type])(implicit ctx: Context): TypeOf =
+        TypeOf(underlyingTp, untpd.Apply(
+          dummyTreeOfType(funTp),
+          argTps.map(x => dummyTreeOfType(x))
+        ))
+
+      def unapply(to: TypeOf): Option[(Type, List[Type])] = to.tree match {
+        case Trees.Apply(fn, args) => Some((fn.tpe, args.map(_.tpe)))
+        case _ => None
+      }
+
+      def derived(to: TypeOf)(funTp: Type, argTps: List[Type])(implicit ctx: Context): Type =
+        finalizeDerived(to, to.tree match {
+          case Trees.Apply(fun, args) =>
+            cpy.Apply(to.tree)(treeWithTpe(fun, funTp), treesWithTpes(args, argTps))(ctx.enterTypeOf())
+        })
+    }
+
+    object TypeApply {
+      def apply(underlyingTp: Type, funTp: Type, argTps: List[Type])(implicit ctx: Context): TypeOf =
+        TypeOf(underlyingTp, untpd.TypeApply(
+          dummyTreeOfType(funTp),
+          argTps.map(x => dummyTreeOfType(x))
+        ))
+
+      def unapply(to: TypeOf): Option[(Type, List[Type])] = to.tree match {
+        case Trees.TypeApply(fn, args) => Some((fn.tpe, args.map(_.tpe)))
+        case _ => None
+      }
+
+      def derived(to: TypeOf)(funTp: Type, argTps: List[Type])(implicit ctx: Context): Type =
+        finalizeDerived(to, to.tree match {
+          case Trees.TypeApply(fun, args) =>
+            cpy.TypeApply(to.tree)(treeWithTpe(fun, funTp), treesWithTpes(args, argTps))(ctx.enterTypeOf())
+        })
+    }
+
+    object Call {
+      @tailrec private [this] def loop(tp: Type, argss: List[List[Type]]): (TermRef, List[List[Type]]) =
+        tp match {
+          case TypeOf(_, tree) =>
+            tree match {
+              case Trees.Apply(fn, args) =>
+                loop(fn.tpe, args.tpes :: argss)
+              case Trees.TypeApply(fn, targs) =>
+                loop(fn.tpe, targs.tpes :: argss)
+              case _ => throw new AssertionError(s"Unexpected tree in method call $tree")
+            }
+          case tp: TermRef =>
+            (tp, argss)
+          case _ => throw new AssertionError(s"Unexpected type in method call $tp")
+        }
+
+      /** Decompose a call fn[targs](vargs_1)...(vargs_n)
+       *  into its constituents (fn, targs ::: vargss).
+       *
+       *  Type-level counter part of TypedTreeInfo.decomposeCall.
+       */
+      def unapply(to: TypeOf): Option[(TermRef, List[List[Type]])] = to.tree match {
+        case _: Apply | _: TypeApply => Some(loop(to, Nil))
+        case _ => None
+      }
+    }
+
+    object New {
+      /** Extracts the class symbol, list of type parameters and list of
+       *  value parameters from the TypeOf of a new.
+       */
+      def unapply(to: TypeOf)(implicit ctx: Context): Option[(Symbol, List[Type], List[Type])] = {
+        def loop(to: TypeOf, targsAcc: List[Type], argsAcc: List[Type]): Option[(Symbol, List[Type], List[Type])] = {
+          to.tree match {
+            case Trees.Apply(fn, args) =>
+              fn.tpe match {
+                case fnTpe: TypeOf =>
+                  loop(fnTpe, targsAcc, args.tpes ::: argsAcc)
+                case fnTpe: TermRef =>
+                  if (fnTpe.symbol.isPrimaryConstructor)
+                    Some((fnTpe.symbol, targsAcc, args.tpes ::: argsAcc))
+                  else
+                    None
+              }
+
+            case Trees.TypeApply(fn, targs) =>
+              fn.tpe match {
+                case fnTpe: TypeOf =>
+                  loop(fnTpe, targs.tpes ::: targsAcc, argsAcc)
+                case fnTpe: TermRef =>
+                  if (fnTpe.symbol.isPrimaryConstructor)
+                    Some((fnTpe.symbol, targsAcc ::: targs.tpes, argsAcc))
+                  else
+                    None
+              }
+
+            case _ => None
+          }
+        }
+        loop(to, Nil, Nil)
+      }
+    }
+
+    object Generic {
+      def unapply(to: TypeOf): Option[List[Type]] = to.tree match {
+        case Trees.If(cond, thenb, elseb) => Some(cond.tpe :: thenb.tpe :: elseb.tpe :: Nil)
+        case Trees.Match(selector, cases) => Some(selector.tpe :: cases.map(_.body.tpe))
+        case Trees.Apply(fn, args)        => Some(fn.tpe :: args.map(_.tpe))
+        case Trees.TypeApply(fn, args)    => Some(fn.tpe :: args.map(_.tpe))
+      }
+    }
+  }
+
   // ----- TypeMaps --------------------------------------------------------------------
 
   /** Common base class of TypeMap and TypeAccumulator */
@@ -4103,6 +4390,20 @@ object Types {
         case tp: SkolemType =>
           tp
 
+        case tp: TypeOf =>
+          tp.tree match {
+            case tree: TypeApply =>
+              TypeOf.TypeApply.derived(tp)(this(tree.fun.tpe), tree.args.map(t => this(t.tpe)))
+            case tree: Apply =>
+              TypeOf.Apply.derived(tp)(this(tree.fun.tpe), tree.args.map(t => this(t.tpe)))
+            case tree: If =>
+              TypeOf.If.derived(tp)(this(tree.cond.tpe), this(tree.thenp.tpe), this(tree.elsep.tpe))
+            case tree: Match =>
+              TypeOf.Match.derived(tp)(this(tree.selector.tpe), tree.cases.map(t => this(t.tpe)))
+            case tree =>
+              throw new AssertionError(s"TypeOf shouldn't contain $tree as top-level node.")
+          }
+
         case tp @ AnnotatedType(underlying, annot) =>
           val underlying1 = this(underlying)
           if (underlying1 eq underlying) tp
@@ -4367,6 +4668,7 @@ object Types {
           if (underlying.isBottomType) underlying
           else tp.derivedAnnotatedType(underlying, annot)
       }
+
     override protected def derivedWildcardType(tp: WildcardType, bounds: Type) = {
       tp.derivedWildcardType(rangeToBounds(bounds))
     }
@@ -4474,6 +4776,25 @@ object Types {
       case tp: OrType =>
         this(this(x, tp.tp1), tp.tp2)
 
+      case tp: TypeOf =>
+        @tailrec def foldTrees(x: T, ts: List[Tree]): T = ts match {
+          case t :: ts1 => foldTrees(apply(x, t.tpe), ts1)
+          case nil => x
+        }
+
+        tp.tree match {
+          case tree: TypeApply =>
+            foldTrees(this(x, tree.fun.tpe), tree.args)
+          case tree: Apply =>
+            foldTrees(this(x, tree.fun.tpe), tree.args)
+          case tree: If =>
+            this(this(this(x, tree.cond.tpe), tree.thenp.tpe), tree.elsep.tpe)
+          case tree: Match =>
+            foldTrees(this(x, tree.selector.tpe), tree.cases)
+          case tree =>
+            throw new AssertionError(s"TypeOf shouldn't contain $tree as top-level node.")
+        }
+
       case AnnotatedType(underlying, annot) =>
         this(applyToAnnot(x, annot), underlying)
 
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala b/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
index 724f32463069..7fdfcf9d4e34 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
@@ -279,6 +279,13 @@ object TastyFormat {
   }
   object NameTags extends NameTags
 
+  object TypeOfTags {
+    final val If        = 1
+    final val Match     = 2
+    final val Apply     = 3
+    final val TypeApply = 4
+  }
+
   // AST tags
   // Cat. 1:    tag
 
@@ -320,6 +327,7 @@ object TastyFormat {
   final val PARAMsetter = 36
   final val EMPTYTREE = 37
   final val EMPTYTYPETREE = 38
+  final val DEPENDENT = 39
 
   // Cat. 2:    tag Nat
 
@@ -430,6 +438,7 @@ object TastyFormat {
   final val IMPLICITMETHODtype = 177
   final val ERASEDMETHODtype = 178
   final val ERASEDIMPLICITMETHODtype = 179
+  final val TYPEOF = 180
 
   final val UNTYPEDSPLICE = 199
 
@@ -454,11 +463,11 @@ object TastyFormat {
 
   /** Useful for debugging */
   def isLegalTag(tag: Int) =
-    firstSimpleTreeTag <= tag && tag <= EMPTYTYPETREE ||
+    firstSimpleTreeTag <= tag && tag <= DEPENDENT ||
     firstNatTreeTag <= tag && tag <= SYMBOLconst ||
     firstASTTreeTag <= tag && tag <= SINGLETONtpt ||
     firstNatASTTreeTag <= tag && tag <= NAMEDARG ||
-    firstLengthTreeTag <= tag && tag <= TYPEREFin ||
+    firstLengthTreeTag <= tag && tag <= TYPEOF ||
     tag == HOLE
 
   def isParamTag(tag: Int) = tag == PARAM || tag == TYPEPARAM
@@ -553,6 +562,7 @@ object TastyFormat {
     case PARAMsetter => "PARAMsetter"
     case EMPTYTREE => "EMPTYTREE"
     case EMPTYTYPETREE => "EMPTYTYPETREE"
+    case DEPENDENT => "DEPENDENT"
 
     case SHAREDterm => "SHAREDterm"
     case SHAREDtype => "SHAREDtype"
@@ -626,6 +636,7 @@ object TastyFormat {
     case SUPERtype => "SUPERtype"
     case TERMREFin => "TERMREFin"
     case TYPEREFin => "TYPEREFin"
+    case TYPEOF => "TYPEOF"
 
     case REFINEDtype => "REFINEDtype"
     case REFINEDtpt => "REFINEDtpt"
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TastyPrinter.scala b/compiler/src/dotty/tools/dotc/core/tasty/TastyPrinter.scala
index 65724cfd8142..4acdc1be0524 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TastyPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TastyPrinter.scala
@@ -75,13 +75,13 @@ class TastyPrinter(bytes: Array[Byte])(implicit ctx: Context) {
               until(end) { printName(); printTree() }
             case PARAMtype =>
               printNat(); printNat()
+            case TYPEOF =>
+              printTree(); until(end) { printTree() }
             case _ =>
               printTrees()
           }
-          if (currentAddr != end) {
-            println(s"incomplete read, current = $currentAddr, end = $end")
-            goto(end)
-          }
+          if (currentAddr != end)
+            throw new AssertionError(s"incomplete read, current = $currentAddr, end = $end, tag = $tag")
         }
         else if (tag >= firstNatASTTreeTag) {
           tag match {
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index 51b410020217..9fea6a7cfc8b 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -153,12 +153,31 @@ class TreePickler(pickler: TastyPickler) {
     }
   }
 
+  private def pickleTypeOf(to: TypeOf)(implicit ctx: Context): Unit = {
+    writeByte(TYPEOF)
+    withLength {
+      val treeKind = to.tree match {
+        case _: If        => TypeOfTags.If
+        case _: Match     => TypeOfTags.Match
+        case _: Apply     => TypeOfTags.Apply
+        case _: TypeApply => TypeOfTags.TypeApply
+      }
+      writeByte(treeKind)
+      pickleType(to.underlying, richTypes = true)
+      to match {
+        case TypeOf.Generic(types) =>
+          types.foreach(tp => pickleType(tp, richTypes = true))
+      }
+    }
+  }
+
   private def pickleNewType(tpe: Type, richTypes: Boolean)(implicit ctx: Context): Unit = tpe match {
     case AppliedType(tycon, args) =>
       writeByte(APPLIEDtype)
       withLength { pickleType(tycon); args.foreach(pickleType(_)) }
     case ConstantType(value) =>
       pickleConstant(value)
+    case tpe: TypeOf => pickleTypeOf(tpe)
     case tpe: NamedType =>
       val sym = tpe.symbol
       def pickleExternalRef(sym: Symbol) = {
@@ -603,6 +622,7 @@ class TreePickler(pickler: TastyPickler) {
     if (flags is Case) writeByte(CASE)
     if (flags is Override) writeByte(OVERRIDE)
     if (flags is Transparent) writeByte(TRANSPARENT)
+    if (flags is Dependent) writeByte(DEPENDENT)
     if (flags is Rewrite) writeByte(REWRITE)
     if (flags is Macro) writeByte(MACRO)
     if (flags is JavaStatic) writeByte(STATIC)
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index 40cfba553bcd..7a8a277d160b 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -294,6 +294,24 @@ class TreeUnpickler(reader: TastyReader,
           result.asInstanceOf[LT]
         }
 
+        def readTypeOf(): Type = {
+          val treeKind = readByte()
+          val underlying = readType()
+          val types = until(end)(readType())
+          val TT = TypeOfTags
+          (treeKind, types) match {
+            case (TT.If, List(cond, thenb, elseb)) =>
+              TypeOf.If(underlying, cond, thenb, elseb)
+            case (TT.Match, sel :: cases) =>
+              TypeOf.Match(underlying, sel, cases)
+            case (TT.Apply, fn :: args) =>
+              TypeOf.Apply(underlying, fn, args)
+            case (TT.TypeApply, fn :: args) =>
+              TypeOf.TypeApply(underlying, fn, args)
+            case _ => throw new AssertionError(s"Inconsistant types in TypeOf: $types")
+          }
+        }
+
         val result =
           (tag: @switch) match {
             case TERMREFin =>
@@ -328,6 +346,8 @@ class TreeUnpickler(reader: TastyReader,
               TypeBounds(readType(), readType())
             case ANNOTATEDtype =>
               AnnotatedType(readType(), Annotation(readTerm()))
+            case TYPEOF =>
+              readTypeOf()
             case ANDtype =>
               AndType(readType(), readType())
             case ORtype =>
@@ -587,6 +607,7 @@ class TreeUnpickler(reader: TastyReader,
           case LAZY => addFlag(Lazy)
           case OVERRIDE => addFlag(Override)
           case TRANSPARENT => addFlag(Transparent)
+          case DEPENDENT => addFlag(Dependent)
           case REWRITE => addFlag(Rewrite)
           case MACRO => addFlag(Macro)
           case STATIC => addFlag(JavaStatic)
@@ -1020,7 +1041,7 @@ class TreeUnpickler(reader: TastyReader,
         case THROW =>
           Throw(readTerm())
         case SINGLETONtpt =>
-          SingletonTypeTree(readTerm())
+          SingletonTypeTree(readTerm()(ctx.enterTypeOf()))
         case BYNAMEtpt =>
           ByNameTypeTree(readTpt())
         case NAMEDARG =>
@@ -1135,6 +1156,10 @@ class TreeUnpickler(reader: TastyReader,
               readHole(end, isType = false)
             case UNTYPEDSPLICE =>
               tpd.UntypedSplice(readUntyped()).withType(readType())
+            case TYPEDEF | VALDEF | DEFDEF =>
+              goto(start)
+              symbolAtCurrent()
+              readNewDef()
             case _ =>
               readPathTerm()
           }
diff --git a/compiler/src/dotty/tools/dotc/fromtasty/ReadTastyTreesFromClasses.scala b/compiler/src/dotty/tools/dotc/fromtasty/ReadTastyTreesFromClasses.scala
index 0153ba932044..efd3209e6069 100644
--- a/compiler/src/dotty/tools/dotc/fromtasty/ReadTastyTreesFromClasses.scala
+++ b/compiler/src/dotty/tools/dotc/fromtasty/ReadTastyTreesFromClasses.scala
@@ -70,7 +70,7 @@ class ReadTastyTreesFromClasses extends FrontEnd {
           def moduleClass = clsd.owner.info.member(className.moduleClassName).symbol
           compilationUnit(clsd.classSymbol).orElse(compilationUnit(moduleClass))
         case _ =>
-          cannotUnpickle(s"no class file was found")
+          cannotUnpickle(s"no class file was found for class $className")
       }
   }
 }
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index f4abf16104bf..52d62123ab72 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -894,7 +894,7 @@ object Parsers {
           makeTupleOrParens(inParens(argTypes(namedOK = false, wildOK = true)))
         }
       else if (in.token == LBRACE)
-        atPos(in.offset) { RefinedTypeTree(EmptyTree, refinement()) }
+        atPos(in.offset) { inBraces(refinementOnEmptyOrSingleton()) }
       else if (isSimpleLiteral) { SingletonTypeTree(literal()) }
       else if (in.token == USCORE) {
         val start = in.skipToken()
@@ -908,6 +908,12 @@ object Parsers {
       }
     }
 
+    /** A refinement on an empty tree or a singleton type tree. */
+    def refinementOnEmptyOrSingleton(): Tree = {
+      if (!isStatSeqEnd && !isDclIntro) SingletonTypeTree(expr1())
+      else RefinedTypeTree(EmptyTree, refineStatSeq())
+    }
+
     val handleSingletonType: Tree => Tree = t =>
       if (in.token == TYPE) {
         in.nextToken()
@@ -1758,6 +1764,7 @@ object Parsers {
       case ERASED      => Mod.Erased()
       case REWRITE     => Mod.Rewrite()
       case TRANSPARENT => Mod.Transparent()
+      case DEPENDENT   => Mod.Dependent()
       case LAZY        => Mod.Lazy()
       case OVERRIDE    => Mod.Override()
       case PRIVATE     => Mod.Private()
diff --git a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
index 1482e8a7cdd0..fb93c2c142c0 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
@@ -181,6 +181,7 @@ object Tokens extends TokensCommon {
   final val TRANSPARENT = 63;      enter(TRANSPARENT, "transparent")
   final val ENUM = 64;             enter(ENUM, "enum")
   final val ERASED = 65;           enter(ERASED, "erased")
+  final val DEPENDENT = 66;        enter(DEPENDENT, "dependent")
 
   /** special symbols */
   final val NEWLINE = 78;          enter(NEWLINE, "end of statement", "new line")
@@ -201,7 +202,7 @@ object Tokens extends TokensCommon {
   /** XML mode */
   final val XMLSTART = 96;         enter(XMLSTART, "$XMLSTART$<") // TODO: deprecate
 
-  final val alphaKeywords = tokenRange(IF, ERASED)
+  final val alphaKeywords = tokenRange(IF, DEPENDENT)
   final val symbolicKeywords = tokenRange(USCORE, VIEWBOUND)
   final val symbolicTokens = tokenRange(COMMA, VIEWBOUND)
   final val keywords = alphaKeywords | symbolicKeywords
@@ -229,7 +230,7 @@ object Tokens extends TokensCommon {
   final val defIntroTokens = templateIntroTokens | dclIntroTokens
 
   final val localModifierTokens = BitSet(
-    ABSTRACT, FINAL, SEALED, IMPLICIT, REWRITE, TRANSPARENT, LAZY, ERASED)
+    ABSTRACT, FINAL, SEALED, IMPLICIT, REWRITE, TRANSPARENT, LAZY, ERASED, DEPENDENT)
 
   final val accessModifierTokens = BitSet(
     PRIVATE, PROTECTED)
diff --git a/compiler/src/dotty/tools/dotc/printing/DecompilerPrinter.scala b/compiler/src/dotty/tools/dotc/printing/DecompilerPrinter.scala
index fe03355800e5..927be407ad92 100644
--- a/compiler/src/dotty/tools/dotc/printing/DecompilerPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/DecompilerPrinter.scala
@@ -76,6 +76,6 @@ class DecompilerPrinter(_ctx: Context) extends RefinedPrinter(_ctx) {
   override protected def typeApplyText[T >: Untyped](tree: TypeApply[T]): Text = {
     if (tree.symbol eq defn.QuotedExpr_apply) "'"
     else if (tree.symbol eq defn.QuotedType_apply) "'[" ~ toTextGlobal(tree.args, ", ") ~ "]"
-    else super.typeApplyText(tree)
+    else super.typeApplyText(tree.fun, tree.args)
   }
 }
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 778650f1ba1b..4f398a660ab1 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -18,6 +18,13 @@ class PlainPrinter(_ctx: Context) extends Printer {
   protected[this] implicit def ctx: Context = _ctx.addMode(Mode.Printing)
 
   private[this] var openRecs: List[RecType] = Nil
+  protected[this] var isInTypeOf: Boolean = false
+
+  protected final def inTypeOf(op: => Text): Text = {
+    val saved = isInTypeOf
+    isInTypeOf = true
+    try { op } finally { isInTypeOf = saved }
+  }
 
   protected def maxToTextRecursions = 100
 
@@ -147,7 +154,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case tp: TypeParamRef =>
         ParamRefNameString(tp) ~ lambdaHash(tp.binder)
       case tp: SingletonType =>
-        toTextLocal(tp.underlying) ~ "(" ~ toTextRef(tp) ~ ")"
+        if (isInTypeOf)
+          toTextRef(tp)
+        else
+          toTextLocal(tp.underlying) ~ "(" ~ toTextRef(tp) ~ ")"
       case AppliedType(tycon, args) =>
         (toTextLocal(tycon) ~ "[" ~ argsText(args) ~ "]").close
       case tp: RefinedType =>
@@ -188,6 +198,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
           (Str(" => ") provided !tp.resultType.isInstanceOf[MethodType]) ~
           toTextGlobal(tp.resultType)
         }
+      case TypeOf(underlyingTp, _) =>
+        "{ ... <: " ~ toText(underlyingTp) ~ " }"
       case AnnotatedType(tpe, annot) =>
         toTextLocal(tpe) ~ " " ~ toText(annot)
       case tp: TypeVar =>
@@ -488,9 +500,12 @@ class PlainPrinter(_ctx: Context) extends Printer {
     val nodeName = tree.productPrefix
     val elems =
       Text(tree.productIterator.map(toTextElem).toList, ", ")
-    val tpSuffix =
-      if (ctx.settings.XprintTypes.value && tree.hasType)
-        " | " ~ toText(tree.typeOpt)
+    val tpSuffix: Text =
+      if (ctx.settings.XprintTypes.value && tree.hasType && !isInTypeOf)
+        tree.typeOpt match {
+          case tp: TypeOf => " | <idem>"
+          case tp => " | " ~ toText(tree.typeOpt)
+        }
       else
         Text()
 
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 5f42fa346f27..0a5b6b0f8ba6 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -216,6 +216,30 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         return toTextParents(tp.parents) ~ "{...}"
       case JavaArrayType(elemtp) =>
         return toText(elemtp) ~ "[]"
+      case tp @ TypeOf(underlyingTp, tree) =>
+        import tpd._
+        val underlying: Text = " <: " ~ toText(underlyingTp) provided ctx.settings.XprintTypes.value
+        def treeText = tp match {
+          case TypeOf.New(cnstrSym, targs, args) =>
+            (keywordStr("new ")
+              ~ nameString(cnstrSym.owner)
+              ~ ("[" ~ Text(targs.map(argText), ", ") ~ "]").provided(targs.nonEmpty)
+              ~ "(" ~ Text(args.map(toText), ", ") ~ ")"
+            )
+          case _ =>
+            tree match {
+              case TypeApply(fun, args) =>
+                typeApplyText(fun.tpe, args.tpes)
+              case Apply(fun, args) =>
+                applyText(fun.tpe, args.tpes)
+              case If(cond, thenp, elsep) =>
+                val elze = if (elsep.isEmpty) None else Some(elsep.tpe)
+                ifText(cond.tpe, thenp.tpe, elze)
+              case Match(sel, cases) =>
+                matchText(sel, cases, showType = true)
+            }
+        }
+        return typeText("{ ") ~ inTypeOf { treeText } ~ underlying ~ typeText(" }")
       case tp: AnnotatedType if homogenizedView =>
         // Positions of annotations in types are not serialized
         // (they don't need to because we keep the original type tree with
@@ -253,7 +277,40 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
     ("{" ~ toText(trees, "\n") ~ "}").close
 
   protected def typeApplyText[T >: Untyped](tree: TypeApply[T]): Text =
-    toTextLocal(tree.fun) ~ "[" ~ toTextGlobal(tree.args, ", ") ~ "]"
+    typeApplyText(tree.fun, tree.args)
+
+  protected def typeApplyText(fun: Showable, args: List[Showable]): Text =
+    toTextLocal(fun) ~ "[" ~ toTextGlobal(args, ", ") ~ "]"
+
+  protected def applyText(fun: Showable, args: List[Showable]): Text =
+    toTextLocal(fun) ~ "(" ~ toTextGlobal(args, ", ") ~ ")"
+
+  protected def ifText(cond: Showable, thenp: Showable, elsep: Option[Showable]): Text =
+    changePrec(GlobalPrec) (
+      keywordStr("if ")
+        ~ cond.toText(this)
+        ~ (keywordText(" then") provided !cond.isInstanceOf[untpd.Parens])
+        ~~ thenp.toText(this)
+        ~ elsep.map(keywordStr(" else ") ~ _.toText(this)).getOrElse("")
+    )
+
+  protected def caseDefText[T >: Untyped](cd: CaseDef[T], showType: Boolean): Text = {
+    val CaseDef(pat, guard, body) = cd
+    val bodyText = body match {
+      case body if showType => toText(List(body.asInstanceOf[tpd.Tree].tpe), "\n")
+      case Block(stats, expr) => toText(stats :+ expr, "\n")
+      case expr => toText(expr)
+    }
+    keywordStr("case ") ~ inPattern(toText(pat)) ~ optText(guard)(keywordStr(" if ") ~ _) ~ " => " ~ bodyText
+  }
+
+  protected def matchText[T >: Untyped](sel: Tree[T], cases: List[CaseDef[T]], showType: Boolean): Text = {
+    val selText = if (showType) toText(sel.asInstanceOf[tpd.Tree].tpe) else toText(sel)
+    if (sel.isEmpty) blockText(cases)
+    else changePrec(GlobalPrec) { selText ~ keywordStr(" match ") ~
+      ("{" ~ Text(cases.map(c => caseDefText(c, showType)), "\n") ~ "}").close
+    }
+  }
 
   protected def toTextCore[T >: Untyped](tree: Tree[T]): Text = {
     import untpd.{modsDeco => _, _}
@@ -265,11 +322,6 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
 
     def optDotPrefix(tree: This) = optText(tree.qual)(_ ~ ".") provided !isLocalThis(tree)
 
-    def caseBlockText(tree: Tree): Text = tree match {
-      case Block(stats, expr) => toText(stats :+ expr, "\n")
-      case expr => toText(expr)
-    }
-
     // Dotty deviation: called with an untpd.Tree, so cannot be a untpd.Tree[T] (seems to be a Scala2 problem to allow this)
     // More deviations marked below as // DD
     def enumText(tree: untpd.Tree) = tree match { // DD
@@ -333,7 +385,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
             keywordStr("throw ") ~ toText(args.head)
           }
         else
-          toTextLocal(fun) ~ "(" ~ toTextGlobal(args, ", ") ~ ")"
+          applyText(fun, args)
       case tree: TypeApply =>
         typeApplyText(tree)
       case Literal(c) =>
@@ -361,17 +413,15 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case block: Block =>
         blockToText(block)
       case If(cond, thenp, elsep) =>
-        changePrec(GlobalPrec) {
-          keywordStr("if ") ~ toText(cond) ~ (keywordText(" then") provided !cond.isInstanceOf[Parens]) ~~ toText(thenp) ~ optText(elsep)(keywordStr(" else ") ~ _)
-        }
+        val elze = if (elsep.isEmpty) None else Some(elsep)
+        ifText(cond, thenp, elze)
       case Closure(env, ref, target) =>
         "closure(" ~ (toTextGlobal(env, ", ") ~ " | " provided env.nonEmpty) ~
         toTextGlobal(ref) ~ (":" ~ toText(target) provided !target.isEmpty) ~ ")"
       case Match(sel, cases) =>
-        if (sel.isEmpty) blockText(cases)
-        else changePrec(GlobalPrec) { toText(sel) ~ keywordStr(" match ") ~ blockText(cases) }
-      case CaseDef(pat, guard, body) =>
-        keywordStr("case ") ~ inPattern(toText(pat)) ~ optText(guard)(keywordStr(" if ") ~ _) ~ " => " ~ caseBlockText(body)
+        matchText(sel, cases, showType = false)
+      case cd: CaseDef =>
+        caseDefText(cd, showType = false)
       case Labeled(bind, expr) =>
         changePrec(GlobalPrec) { toText(bind.name) ~ keywordStr("[") ~ toText(bind.symbol.info) ~ keywordStr("]: ") ~ toText(expr) }
       case Return(expr, from) =>
@@ -399,7 +449,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case TypeTree() =>
         typeText(toText(tree.typeOpt))
       case SingletonTypeTree(ref) =>
-        toTextLocal(ref) ~ "." ~ keywordStr("type")
+        typeText("{") ~~ toTextLocal(ref) ~~ typeText("}")
       case AndTypeTree(l, r) =>
         changePrec(AndTypePrec) { toText(l) ~ " & " ~ atPrec(AndTypePrec + 1) { toText(r) } }
       case OrTypeTree(l, r) =>
@@ -556,7 +606,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
     var txt = toTextCore(tree)
 
     def suppressTypes =
-      tree.isType || tree.isDef || // don't print types of types or defs
+      tree.isType || isInTypeOf || tree.isDef || // don't print types of types or defs
       homogenizedView && ctx.mode.is(Mode.Pattern)
         // When comparing pickled info, disregard types of patterns.
         // The reason is that GADT matching can rewrite types of pattern trees
@@ -571,23 +621,24 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
 
     if (ctx.settings.XprintTypes.value && tree.hasType) {
       // add type to term nodes; replace type nodes with their types unless -Yprint-pos is also set.
-      def tp = tree.typeOpt match {
-        case tp: TermRef if tree.isInstanceOf[RefTree] && !tp.denot.isOverloaded => tp.underlying
+      def tpText: Text = tree.typeOpt match {
+        case tp: TermRef if tree.isInstanceOf[RefTree] && !tp.denot.isOverloaded => toText(tp.underlying)
         case tp: ConstantType if homogenizedView =>
           // constant folded types are forgotten in Tasty, are reconstituted subsequently in FirstTransform.
           // Therefore we have to gloss over this when comparing before/after pickling by widening to
           // underlying type `T`, or, if expression is a unary primitive operation, to `=> T`.
-          tree match {
+          toText(tree match {
             case Select(qual, _) if qual.typeOpt.widen.typeSymbol.isPrimitiveValueClass =>
               ExprType(tp.widen)
             case _ => tp.widen
-          }
-        case tp => tp
+          })
+        case tp: TypeOf => "<idem>"
+        case tp => toText(tp)
       }
       if (!suppressTypes)
-        txt = ("<" ~ txt ~ ":" ~ toText(tp) ~ ">").close
+        txt = ("<" ~ txt ~ ":" ~ tpText ~ ">").close
       else if (tree.isType && !homogenizedView)
-        txt = toText(tp)
+        txt = tpText
     }
     if (!suppressPositions) {
       if (printPos) {
@@ -756,8 +807,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
   def optText[T >: Untyped](tree: Tree[T])(encl: Text => Text): Text =
     if (tree.isEmpty) "" else encl(toText(tree))
 
-  def optText[T >: Untyped](tree: List[Tree[T]])(encl: Text => Text): Text =
-    if (tree.exists(!_.isEmpty)) encl(blockText(tree)) else ""
+  def optText[T >: Untyped](trees: List[Tree[T]])(encl: Text => Text): Text =
+    if (trees.exists(!_.isEmpty)) encl(blockText(trees)) else ""
 
   override protected def ParamRefNameString(name: Name): String =
     name.invariantName.toString
diff --git a/compiler/src/dotty/tools/dotc/printing/SyntaxHighlighting.scala b/compiler/src/dotty/tools/dotc/printing/SyntaxHighlighting.scala
index 6c6348e80a03..1261b0b96a64 100644
--- a/compiler/src/dotty/tools/dotc/printing/SyntaxHighlighting.scala
+++ b/compiler/src/dotty/tools/dotc/printing/SyntaxHighlighting.scala
@@ -31,7 +31,7 @@ object SyntaxHighlighting {
   private val tripleQs = Console.RED_B + "???" + NoColor
 
   private val keywords: Seq[String] = for {
-    index <- IF to ERASED // All alpha keywords
+    index <- IF to DEPENDENT // All alpha keywords
   } yield tokenString(index)
 
   private val interpolationPrefixes =
diff --git a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
index ce3ce629a70a..55859336a92d 100644
--- a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
+++ b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
@@ -162,10 +162,14 @@ private class ExtractAPICollector(implicit val ctx: Context) extends ThunkHolder
    */
   private def withMarker(tp: api.Type, marker: api.Annotation) =
     api.Annotated.of(tp, Array(marker))
-  private def marker(name: String) =
+  private def marker(name: String): api.Annotation =
     api.Annotation.of(api.Constant.of(Constants.emptyType, name), Array())
   val orMarker = marker("Or")
   val byNameMarker = marker("ByName")
+  val typeOfIfMarker = marker("If")
+  val typeOfMatchMarker = marker("Match")
+  val typeOfTypeApplyMarker = marker("TypeApply")
+  val typeOfApplyMarker = marker("Apply")
 
 
   /** Extract the API representation of a source file */
@@ -509,6 +513,16 @@ private class ExtractAPICollector(implicit val ctx: Context) extends ThunkHolder
         withMarker(apiType(resultType), byNameMarker)
       case ConstantType(constant) =>
         api.Constant.of(apiType(constant.tpe), constant.stringValue)
+      case to @ TypeOf(_, tree) =>
+        val marker = to.tree match {
+          case _: If        => typeOfIfMarker
+          case _: Match     => typeOfMatchMarker
+          case _: TypeApply => typeOfTypeApplyMarker
+          case _: Apply     => typeOfApplyMarker
+        }
+        to match {
+          case TypeOf.Generic(args) => withMarker(combineApiTypes(args.map(apiType): _*), marker)
+        }
       case AnnotatedType(tpe, annot) =>
         api.Annotated.of(apiType(tpe), Array(apiAnnotation(annot)))
       case tp: ThisType =>
diff --git a/compiler/src/dotty/tools/dotc/tastyreflect/TypeOrBoundsOpsImpl.scala b/compiler/src/dotty/tools/dotc/tastyreflect/TypeOrBoundsOpsImpl.scala
index 6fdffc033137..363ff8d606bd 100644
--- a/compiler/src/dotty/tools/dotc/tastyreflect/TypeOrBoundsOpsImpl.scala
+++ b/compiler/src/dotty/tools/dotc/tastyreflect/TypeOrBoundsOpsImpl.scala
@@ -111,6 +111,13 @@ trait TypeOrBoundsOpsImpl extends scala.tasty.reflect.TypeOrBoundsOps with Tasty
       }
     }
 
+    object TypeOf extends TypeOfExtractor {
+      def unapply(x: TypeOrBounds)(implicit ctx: Context): Option[(Type, Term)] = x match {
+        case Types.TypeOf(underlying, tree) => Some((underlying.stripTypeVar, tree))
+        case _ => None
+      }
+    }
+
     object AndType extends AndTypeExtractor {
       def unapply(x: TypeOrBounds)(implicit ctx: Context): Option[(Type, Type)] = x match {
         case Types.AndType(left, right) => Some(left.stripTypeVar, right.stripTypeVar)
diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index 69bded663ee5..8af1699e58f3 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -508,7 +508,7 @@ object Erasure {
             case mt: MethodType =>
               val outers = outer.args(fun.asInstanceOf[tpd.Tree]) // can't use fun1 here because its type is already erased
               val ownArgs = if (mt.paramNames.nonEmpty && !mt.isErasedMethod) args else Nil
-              var args0 = outers ::: ownArgs ::: protoArgs(pt, tree.typeOpt)
+              var args0 = outers ::: ownArgs ::: protoArgs(pt, tree.typeOpt.stripMethodPrefix)
 
               if (args0.length > MaxImplementedFunctionArity && mt.paramInfos.length == 1) {
                 val bunchedArgs = untpd.JavaSeqLiteral(args0, TypeTree(defn.ObjectType))
diff --git a/compiler/src/dotty/tools/dotc/transform/FullParameterization.scala b/compiler/src/dotty/tools/dotc/transform/FullParameterization.scala
index b636b8476fa4..6c1b8d44b92f 100644
--- a/compiler/src/dotty/tools/dotc/transform/FullParameterization.scala
+++ b/compiler/src/dotty/tools/dotc/transform/FullParameterization.scala
@@ -233,7 +233,7 @@ trait FullParameterization {
     else {
       // this type could have changed on forwarding. Need to insert a cast.
       originalDef.vparamss.foldLeft(fun)((acc, vparams) => {
-        val meth = acc.tpe.asInstanceOf[MethodType]
+        val meth = acc.tpe.stripMethodPrefix.asInstanceOf[MethodType]
         val paramTypes = meth.instantiateParamInfos(vparams.map(_.tpe))
         acc.appliedToArgs(
           (vparams, paramTypes).zipped.map((vparam, paramType) => {
diff --git a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
index d12420f1313b..236896722f7b 100644
--- a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
+++ b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
@@ -102,9 +102,13 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase
       annot.derivedAnnotation(transformAnnot(annot.tree))
 
     private def transformMemberDef(tree: MemberDef)(implicit ctx: Context): Unit = {
+      def transformAnnotWithAdaptedCtx(annot: Annotation): Annotation = annot match {
+        case annot: BodyAnnotation => transformAnnot(annot)(localCtx(tree))
+        case _ => transformAnnot(annot)
+      }
       val sym = tree.symbol
       sym.registerIfChild()
-      sym.transformAnnotations(transformAnnot)
+      sym.transformAnnotations(transformAnnotWithAdaptedCtx)
     }
 
     private def transformSelect(tree: Select, targs: List[Tree])(implicit ctx: Context): Tree = {
@@ -282,12 +286,12 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase
           Checking.checkAppliedType(tree, boundsCheck = !ctx.mode.is(Mode.Pattern))
           super.transform(tree)
         case SingletonTypeTree(ref) =>
-          Checking.checkRealizable(ref.tpe, ref.pos.focus)
+         // Checking.checkRealizable(ref.tpe, ref.pos.focus) // TODO
           super.transform(tree)
         case tree: TypeTree =>
           tree.withType(
             tree.tpe match {
-              case AnnotatedType(tpe, annot) => AnnotatedType(tpe, transformAnnot(annot))
+              case tpe: AnnotatedType => tpe.derivedAnnotatedType(tpe.parent, transformAnnot(tpe.annot))
               case tpe => tpe
             }
           )
diff --git a/compiler/src/dotty/tools/dotc/transform/TailRec.scala b/compiler/src/dotty/tools/dotc/transform/TailRec.scala
index fb8160c5a146..1e0c67a5e88b 100644
--- a/compiler/src/dotty/tools/dotc/transform/TailRec.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TailRec.scala
@@ -90,7 +90,7 @@ class TailRec extends MiniPhase with FullParameterization {
     val name = TailLabelName.fresh()
 
     if (method.owner.isClass)
-      ctx.newSymbol(method, name.toTermName, labelFlags, fullyParameterizedType(method.info, method.enclosingClass.asClass, abstractOverClass, liftThisType = false))
+      ctx.newSymbol(method, name.toTermName, labelFlags, fullyParameterizedType(method.info, method.enclosingClass.asClass, abstractOverClass, liftThisType = false)(ctx.withOwner(method)))
     else ctx.newSymbol(method, name.toTermName, labelFlags, method.info)
   }
 
@@ -110,50 +110,53 @@ class TailRec extends MiniPhase with FullParameterization {
 
           var rewrote = false
 
-          // Note: this can be split in two separate transforms(in different groups),
-          // than first one will collect info about which transformations and rewritings should be applied
-          // and second one will actually apply,
-          // now this speculatively transforms tree and throws away result in many cases
-          val rhsSemiTransformed = {
-            val transformer = new TailRecElimination(origMeth, dd.tparams, owner, thisTpe, mandatory, label, abstractOverClass = defIsTopLevel)
-            val rhs = transformer.transform(dd.rhs)
-            rewrote = transformer.rewrote
-            rhs
-          }
+          def finish(implicit ctx: Context) = {
+            // Note: this can be split in two separate transforms(in different groups),
+            // than first one will collect info about which transformations and rewritings should be applied
+            // and second one will actually apply,
+            // now this speculatively transforms tree and throws away result in many cases
+            val rhsSemiTransformed = {
+              val transformer = new TailRecElimination(origMeth, dd.tparams, owner, thisTpe, mandatory, label, abstractOverClass = defIsTopLevel)
+              val rhs = transformer.transform(dd.rhs)
+              rewrote = transformer.rewrote
+              rhs
+            }
 
-          if (rewrote) {
-            val dummyDefDef = cpy.DefDef(tree)(rhs = rhsSemiTransformed)
-            if (tree.symbol.owner.isClass) {
-              val labelDef = fullyParameterizedDef(label, dummyDefDef, abstractOverClass = defIsTopLevel)
-              val call = forwarder(label, dd, abstractOverClass = defIsTopLevel, liftThisType = true)
-              Block(List(labelDef), call)
-            } else { // inner method. Tail recursion does not change `this`
-              val labelDef = polyDefDef(label, trefs => vrefss => {
-                val origMeth = tree.symbol
-                val origTParams = tree.tparams.map(_.symbol)
-                val origVParams = tree.vparamss.flatten map (_.symbol)
-                new TreeTypeMap(
-                  typeMap = identity(_)
-                    .subst(origTParams ++ origVParams, trefs ++ vrefss.flatten.map(_.tpe)),
-                  oldOwners = origMeth :: Nil,
-                  newOwners = label :: Nil
-                ).transform(rhsSemiTransformed)
-              })
-              val callIntoLabel = (
-                  if (dd.tparams.isEmpty) ref(label)
-                  else ref(label).appliedToTypes(dd.tparams.map(_.tpe))
-                ).appliedToArgss(vparamss0.map(_.map(x=> ref(x.symbol))))
-              Block(List(labelDef), callIntoLabel)
-          }} else {
-            if (mandatory) ctx.error(
-              "TailRec optimisation not applicable, method not tail recursive",
-              // FIXME: want to report this error on `dd.namePos`, but
-              // because of extension method getting a weird pos, it is
-              // better to report on symbol so there's no overlap
-              sym.pos
-            )
-            dd.rhs
+            if (rewrote) {
+              val dummyDefDef = cpy.DefDef(tree)(rhs = rhsSemiTransformed)
+              if (tree.symbol.owner.isClass) {
+                val labelDef = fullyParameterizedDef(label, dummyDefDef, abstractOverClass = defIsTopLevel)
+                val call = forwarder(label, dd, abstractOverClass = defIsTopLevel, liftThisType = true)
+                Block(List(labelDef), call)
+              } else { // inner method. Tail recursion does not change `this`
+                val labelDef = polyDefDef(label, trefs => vrefss => {
+                  val origMeth = tree.symbol
+                  val origTParams = tree.tparams.map(_.symbol)
+                  val origVParams = tree.vparamss.flatten map (_.symbol)
+                  new TreeTypeMap(
+                    typeMap = identity(_)
+                      .subst(origTParams ++ origVParams, trefs ++ vrefss.flatten.map(_.tpe)),
+                    oldOwners = origMeth :: Nil,
+                    newOwners = label :: Nil
+                  ).transform(rhsSemiTransformed)
+                })
+                val callIntoLabel = (
+                    if (dd.tparams.isEmpty) ref(label)
+                    else ref(label).appliedToTypes(dd.tparams.map(_.tpe))
+                  ).appliedToArgss(vparamss0.map(_.map(x=> ref(x.symbol))))
+                Block(List(labelDef), callIntoLabel)
+            }} else {
+              if (mandatory) ctx.error(
+                "TailRec optimisation not applicable, method not tail recursive",
+                // FIXME: want to report this error on `dd.namePos`, but
+                // because of extension method getting a weird pos, it is
+                // better to report on symbol so there's no overlap
+                sym.pos
+              )
+              dd.rhs
+            }
           }
+          finish(ctx.withOwner(sym))
         })
       case d: DefDef if d.symbol.hasAnnotation(defn.TailrecAnnot) || methodsWithInnerAnnots.contains(d.symbol) =>
         ctx.error(TailrecNotApplicable(sym), sym.pos)
diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index d46d2dbcc510..32152661de35 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -509,7 +509,7 @@ object TreeChecker {
   /** - Check that TypeParamRefs and MethodParams refer to an enclosing type.
    *  - Check that all type variables are instantiated.
    */
-  def checkNoOrphans(tp0: Type, tree: untpd.Tree = untpd.EmptyTree)(implicit ctx: Context) = new TypeMap() {
+  def checkNoOrphans(tp0: Type)(implicit ctx: Context) = new TypeMap() {
     val definedBinders = new java.util.IdentityHashMap[Type, Any]
     def apply(tp: Type): Type = {
       tp match {
@@ -518,10 +518,14 @@ object TreeChecker {
           mapOver(tp)
           definedBinders.remove(tp)
         case tp: ParamRef =>
-          assert(definedBinders.get(tp.binder) != null, s"orphan param: ${tp.show}, hash of binder = ${System.identityHashCode(tp.binder)}, tree = ${tree.show}, type = $tp0")
+          assert(definedBinders.get(tp.binder) != null, s"orphan param: ${tp.show}, hash of binder = ${System.identityHashCode(tp.binder)}, type = $tp0")
         case tp: TypeVar =>
-          assert(tp.isInstantiated, s"Uninstantiated type variable: ${tp.show}, tree = ${tree.show}")
+          assert(tp.isInstantiated, s"Uninstantiated type variable: ${tp.show}")
           apply(tp.underlying)
+        case tp: TypeOf =>
+          assert(tp.tree.tpe eq NoType, s"See note in TypeOf.apply")
+          apply(tp.underlyingTp)
+          mapOver(tp)
         case _ =>
           mapOver(tp)
       }
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
index 1bffe1372586..cebeab01a0be 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
@@ -156,7 +156,10 @@ object TypeTestsCasts {
           fun.symbol == defn.Any_typeTest ||  // new scheme
           expr.symbol.is(Case)                // old scheme
 
-        def transformIsInstanceOf(expr:Tree, testType: Type, flagUnrelated: Boolean): Tree = {
+
+        // `expr` is a typed unerased tree
+        // `testType` is erased
+        def transformIsInstanceOf(expr: Tree, testType: Type, flagUnrelated: Boolean): Tree = {
           def testCls = testType.classSymbol
 
           def unreachable(why: => String) =
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 34e4fa1375cc..e13a55815168 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1373,7 +1373,7 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
           case x => x
         }
 
-        def sizeFits(alt: TermRef, tp: Type): Boolean = tp.stripPoly match {
+        def sizeFits(alt: TermRef, tp: Type): Boolean = tp.stripMethodPrefix match {
           case tp: MethodType =>
             val ptypes = tp.paramInfos
             val numParams = ptypes.length
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index 260e0753aa69..a838045a3c81 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -408,7 +408,10 @@ object Checking {
     checkCombination(Private, Protected)
     checkCombination(Abstract, Override)
     checkCombination(Lazy, Transparent)
+    checkCombination(Module, Transparent)
     checkCombination(Rewrite, Transparent)
+    checkCombination(Rewrite, Dependent)
+    checkCombination(Dependent, Transparent) // TODO: Add further restrictions on Dependent
     checkNoConflict(Lazy, ParamAccessor, s"parameter may not be `lazy`")
     if (sym.is(Transparent)) checkApplicable(Transparent, sym.isTerm && !sym.is(Mutable | Module))
     if (sym.is(Rewrite)) checkApplicable(Rewrite, sym.is(Method, butNot = Accessor))
@@ -606,7 +609,7 @@ trait Checking {
   /** If `sym` is an implicit conversion, check that implicit conversions are enabled.
    *  @pre  sym.is(Implicit)
    */
-  def checkImplicitConversionDefOK(sym: Symbol)(implicit ctx: Context): Unit = sym.info.stripPoly match {
+  def checkImplicitConversionDefOK(sym: Symbol)(implicit ctx: Context): Unit = sym.info.stripMethodPrefix match {
     case mt @ MethodType(_ :: Nil)
     if !mt.isImplicitMethod && !sym.is(Synthetic) => // it's a conversion
       checkFeature(
diff --git a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
index 68a5d05f5f26..becb322fd544 100644
--- a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
@@ -59,6 +59,30 @@ object ConstFold {
                                             // compiler itself crashing
     }
 
+
+  def apply(fn: TermRef)(implicit ctx: Context): Type = finish {
+    fn.prefix.widenTermRefExpr match {
+      case ConstantType(x) => foldUnop(fn.name, x)
+      case _               => null
+    }
+  }
+
+  def apply(fn: TermRef, arg: Type)(implicit ctx: Context): Type = finish {
+    (fn.prefix.widenTermRefExpr, arg.widenTermRefExpr) match {
+      case (ConstantType(x), ConstantType(y)) => foldBinop(fn.name, x, y)
+      case _                                  => null
+    }
+  }
+
+  private def finish(compX: => Constant)(implicit ctx: Context): Type =
+    try {
+      val x = compX
+      if (x ne null) ConstantType(x) else NoType
+    } catch {
+      case _: ArithmeticException => NoType
+    }
+
+
   private def foldUnop(op: Name, x: Constant): Constant = (op, x.tag) match {
     case (nme.UNARY_!, BooleanTag) => Constant(!x.booleanValue)
 
diff --git a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
index 923425800e93..3657cc071a66 100644
--- a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
@@ -80,7 +80,7 @@ object ErrorReporting {
       if (tree.tpe.widen.exists)
         i"${exprStr(tree)} does not take ${kind}parameters"
       else
-        i"undefined: $tree # ${tree.uniqueId}: ${tree.tpe.toString} at ${ctx.phase}"
+        i"undefined takesNoParamsStr: $tree # ${tree.uniqueId}: ${tree.tpe.toString} at ${ctx.phase}"
 
     def patternConstrStr(tree: Tree): String = ???
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Implicits.scala b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
index e7faf156ad0c..7d1a23a4e592 100644
--- a/compiler/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
@@ -134,7 +134,7 @@ object Implicits {
             !(isFunctionInS2 || isImplicitConverter || isConforms)
         }
 
-        def discardForValueType(tpw: Type): Boolean = tpw.stripPoly match {
+        def discardForValueType(tpw: Type): Boolean = tpw.stripMethodPrefix match {
           case tpw: MethodType => !tpw.isImplicitMethod
           case _ => false
         }
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index 001a100f2a96..9dbd4da1e0e5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -760,7 +760,7 @@ class Namer { typer: Typer =>
     }
 
     private def addInlineInfo(sym: Symbol) = original match {
-      case original: untpd.DefDef if sym.isInlineable =>
+      case original: untpd.DefDef if sym.requiresInlineInfo =>
         PrepareInlineable.registerInlineInfo(
             sym,
             original.rhs,
@@ -1080,11 +1080,15 @@ class Namer { typer: Typer =>
       // Widen rhs type and eliminate `|' but keep ConstantTypes if
       // definition is inline (i.e. final in Scala2) and keep module singleton types
       // instead of widening to the underlying module class types.
-      def widenRhs(tp: Type): Type = tp.widenTermRefExpr match {
-        case ctp: ConstantType if isTransparentVal => ctp
-        case ref: TypeRef if ref.symbol.is(ModuleClass) => tp
-        case _ => tp.widen.widenUnion
-      }
+      def widenRhs(tp: Type): Type =
+        if (ctx.isDependent)
+          tp
+        else
+          tp.widenTermRefExpr match {
+            case ctp: ConstantType if isTransparentVal => ctp
+            case ref: TypeRef if ref.symbol.is(ModuleClass) => tp
+            case _ => tp.widen.widenUnion
+          }
 
       // Replace aliases to Unit by Unit itself. If we leave the alias in
       // it would be erased to BoxedUnit.
diff --git a/compiler/src/dotty/tools/dotc/typer/PrepareInlineable.scala b/compiler/src/dotty/tools/dotc/typer/PrepareInlineable.scala
index d98096c63f3b..87ef638367d2 100644
--- a/compiler/src/dotty/tools/dotc/typer/PrepareInlineable.scala
+++ b/compiler/src/dotty/tools/dotc/typer/PrepareInlineable.scala
@@ -240,12 +240,17 @@ object PrepareInlineable {
           inlined.updateAnnotation(LazyBodyAnnotation { _ =>
             implicit val ctx = inlineCtx
             val rawBody = treeExpr(ctx)
-            val typedBody =
-              if (ctx.reporter.hasErrors) rawBody
-              else ctx.compilationUnit.inlineAccessors.makeInlineable(rawBody)
-            val inlineableBody = addReferences(inlined, originalBody, typedBody)
-            inlining.println(i"Body to inline for $inlined: $inlineableBody")
-            inlineableBody
+            if (inlined.is(Transparent | Rewrite)) {
+              val typedBody =
+                if (ctx.reporter.hasErrors) rawBody
+                else ctx.compilationUnit.inlineAccessors.makeInlineable(rawBody)
+              val inlineableBody = addReferences(inlined, originalBody, typedBody)
+              inlining.println(i"Body to inline for $inlined: $inlineableBody")
+              inlineableBody
+            } else {
+              assert(inlined.is(Dependent))
+              rawBody
+            }
           })
         }
     }
@@ -428,4 +433,4 @@ object PrepareInlineable {
     val untpdSplice = tpd.UntypedSplice(addRefs.transform(original)).withType(typed.tpe)
     seq(implicitBindings, untpdSplice)
   }
-}
\ No newline at end of file
+}
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 1f2a7a4813d1..57164c537460 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -93,7 +93,7 @@ trait TypeAssigner {
       def apply(tp: Type): Type = tp match {
         case tp: TermRef
         if toAvoid(tp.symbol) || partsToAvoid(mutable.Set.empty, tp.info).nonEmpty =>
-          tp.info.widenExpr.dealias match {
+          tp.info.widenExpr.dealiasKeepRefiningAnnots match {
             case info: SingletonType => apply(info)
             case info => range(defn.NothingType, apply(info))
           }
@@ -130,17 +130,25 @@ trait TypeAssigner {
        *   3. Finally, we need to handle the case where the prefix type does not have a member
        *      named `tp.name` anymmore. In that case, we need to fall back to Bot..Top.
        */
-      override def derivedSelect(tp: NamedType, pre: Type) =
-        if (pre eq tp.prefix)
-          tp
-        else tryWiden(tp, tp.prefix).orElse {
-          if (tp.isTerm && variance > 0 && !pre.isSingleton)
-          	apply(tp.info.widenExpr)
-          else if (upper(pre).member(tp.name).exists)
+      override def derivedSelect(tp: NamedType, pre: Type) = {
+        def default =
+          if (upper(pre).member(tp.name).exists)
             super.derivedSelect(tp, pre)
           else
             range(defn.NothingType, defn.AnyType)
-        }
+
+        if (pre eq tp.prefix)
+          tp
+        else if (ctx.isDependent)
+          default
+        else
+          tryWiden(tp, tp.prefix).orElse {
+            if (tp.isTerm && variance > 0 && !pre.isSingleton)
+              apply(tp.info.widenExpr)
+            else
+              default
+          }
+      }
     }
 
     widenMap(tp)
@@ -364,10 +372,14 @@ trait TypeAssigner {
   def assignType(tree: untpd.Apply, fn: Tree, args: List[Tree])(implicit ctx: Context) = {
     val ownType = fn.tpe.widen match {
       case fntpe: MethodType =>
-        if (sameLength(fntpe.paramInfos, args) || ctx.phase.prev.relaxedTyping)
-          if (fntpe.isResultDependent) safeSubstParams(fntpe.resultType, fntpe.paramRefs, args.tpes)
-          else fntpe.resultType
-        else
+        if (sameLength(fntpe.paramInfos, args) || ctx.phase.prev.relaxedTyping) {
+          val tpe =
+            if (fntpe.isResultDependent) safeSubstParams(fntpe.resultType, fntpe.paramRefs, args.tpes)
+            else fntpe.resultType
+          if (!ctx.erasedTypes && (fn.symbol.isDependentMethod || ctx.isDependent))
+            ctx.normalizedType(TypeOf(tpe, tree))
+          else tpe
+        } else
           errorType(i"wrong number of arguments at ${ctx.phase.prev} for $fntpe: ${fn.tpe}, expected: ${fntpe.paramInfos.length}, found: ${args.length}", tree.pos)
       case t =>
         errorType(err.takesNoParamsStr(fn, ""), tree.pos)
@@ -424,7 +436,12 @@ trait TypeAssigner {
         }
         else {
           val argTypes = args.tpes
-          if (sameLength(argTypes, paramNames)) pt.instantiate(argTypes)
+          if (sameLength(argTypes, paramNames)) {
+            val tpe = pt.instantiate(argTypes)
+            if (!ctx.erasedTypes && (fn.symbol.isDependentMethod || ctx.isDependent))
+              ctx.normalizedType(TypeOf(tpe, tree))
+            else tpe
+          }
           else wrongNumberOfTypeArgs(fn.tpe, pt.typeParams, args, tree.pos)
         }
       case err: ErrorType =>
@@ -452,8 +469,13 @@ trait TypeAssigner {
   def assignType(tree: untpd.Inlined, bindings: List[Tree], expansion: Tree)(implicit ctx: Context) =
     tree.withType(avoidingType(expansion, bindings))
 
-  def assignType(tree: untpd.If, thenp: Tree, elsep: Tree)(implicit ctx: Context) =
-    tree.withType(thenp.tpe | elsep.tpe)
+  def assignType(tree: untpd.If, thenp: Tree, elsep: Tree)(implicit ctx: Context) = {
+    val underlying = thenp.tpe | elsep.tpe
+    if (!ctx.erasedTypes && ctx.isDependent)
+      tree.withType(TypeOf(underlying, tree))
+    else
+      tree.withType(underlying)
+  }
 
   def assignType(tree: untpd.Closure, meth: Tree, target: Tree)(implicit ctx: Context) =
     tree.withType(
@@ -463,8 +485,13 @@ trait TypeAssigner {
   def assignType(tree: untpd.CaseDef, body: Tree)(implicit ctx: Context) =
     tree.withType(body.tpe)
 
-  def assignType(tree: untpd.Match, cases: List[CaseDef])(implicit ctx: Context) =
-    tree.withType(ctx.typeComparer.lub(cases.tpes))
+  def assignType(tree: untpd.Match, cases: List[CaseDef])(implicit ctx: Context) = {
+    val underlying = ctx.typeComparer.lub(cases.tpes)
+    if (!ctx.erasedTypes && ctx.isDependent)
+      tree.withType(TypeOf(underlying, tree))
+    else
+      tree.withType(underlying)
+  }
 
   def assignType(tree: untpd.Labeled)(implicit ctx: Context) =
     tree.withType(tree.bind.symbol.info)
@@ -484,8 +511,21 @@ trait TypeAssigner {
     tree.withType(ownType)
   }
 
-  def assignType(tree: untpd.SingletonTypeTree, ref: Tree)(implicit ctx: Context) =
-    tree.withType(ref.tpe)
+  def assignType(tree: untpd.SingletonTypeTree, ref: Tree)(implicit ctx: Context) = {
+    val tp = ref match {
+      case _: Literal | _: Ident | _: Select | _: Block | _: This | _: Super => ref.tpe
+      case _ =>
+        if (TypeOf.isLegalTopLevelTree(ref))
+          if (ref.tpe.isInstanceOf[TypeOf] ||
+              ref.tpe.isInstanceOf[ConstantType]) // Can happen because of typer's constant folding
+            ctx.normalizedType(ref.tpe)
+          else
+            errorType(i"Non-sensical singleton-type expression: $ref: ${ref.tpe}", ref.pos)
+        else
+          throw new AssertionError(i"Tree $ref is not a valid reference for a singleton type tree.")
+    }
+    tree.withType(tp)
+  }
 
   def assignType(tree: untpd.AndTypeTree, left: Tree, right: Tree)(implicit ctx: Context) =
     tree.withType(AndType(left.tpe, right.tpe))
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index dfed1555eb68..13c02ebf199a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -709,11 +709,17 @@ class Typer extends Namer
   }
 
   def typedIf(tree: untpd.If, pt: Type)(implicit ctx: Context): Tree = track("typedIf") {
+    val (condProto, thenProto, elseProto) =
+      pt match {
+        case TypeOf.If(c, t ,e) => (c, t, e)
+        case _ => (defn.BooleanType, pt.notApplied, pt.notApplied)
+      }
+
     if (tree.isInstanceOf[untpd.RewriteIf]) checkInRewriteContext("rewrite if", tree.pos)
-    val cond1 = typed(tree.cond, defn.BooleanType)
+    val cond1 = typed(tree.cond, condProto)
     val thenp2 :: elsep2 :: Nil = harmonic(harmonize) {
-      val thenp1 = typed(tree.thenp, pt.notApplied)
-      val elsep1 = typed(tree.elsep orElse (untpd.unitLiteral withPos tree.pos), pt.notApplied)
+      val thenp1 = typed(tree.thenp, thenProto)
+      val elsep1 = typed(tree.elsep orElse (untpd.unitLiteral withPos tree.pos), elseProto)
       thenp1 :: elsep1 :: Nil
     }
     assignType(cpy.If(tree)(cond1, thenp2, elsep2), thenp2, elsep2)
@@ -979,6 +985,11 @@ class Typer extends Namer
         val sel1 = id.withType(defn.ImplicitScrutineeTypeRef)
         typedMatchFinish(tree, sel1, sel1.tpe, pt)
       case _ =>
+        val selectProto = pt match {
+          case TypeOf.Match(s, _) => s
+          case _ => WildcardType
+        }
+
         if (tree.isInstanceOf[untpd.RewriteMatch]) checkInRewriteContext("rewrite match", tree.pos)
         val sel1 = typedExpr(tree.selector)
         val selType = fullyDefinedType(sel1.tpe, "pattern selector", tree.pos).widen
@@ -1024,7 +1035,12 @@ class Typer extends Namer
 
   def typedCases(cases: List[untpd.CaseDef], selType: Type, pt: Type)(implicit ctx: Context) = {
     val gadts = gadtSyms(selType)
-    cases.mapconserve(typedCase(_, selType, pt, gadts))
+    pt match {
+      case TypeOf.Match(_, cs) if cs.length == cases.length =>
+        cases.zip(cs).mapconserve { case (c, p) => typedCase(c, selType, p, gadts) }
+      case _ =>
+        cases.mapconserve(typedCase(_, selType, pt, gadts))
+    }
   }
 
   /** Type a case. */
@@ -1194,8 +1210,9 @@ class Typer extends Namer
   }
 
   def typedSingletonTypeTree(tree: untpd.SingletonTypeTree)(implicit ctx: Context): SingletonTypeTree = track("typedSingletonTypeTree") {
-    val ref1 = typedExpr(tree.ref)
-    checkStable(ref1.tpe, tree.pos)
+    val ref1 = typedExpr(tree.ref)(ctx.enterTypeOf())
+    // TODO: Discuss stability requirements of singleton type trees and potentially reenable check
+    // checkStable(ref1.tpe, tree.pos)
     assignType(cpy.SingletonTypeTree(tree)(ref1), ref1)
   }
 
@@ -1465,7 +1482,7 @@ class Typer extends Namer
     if (sym.isInlineable) rhsCtx = rhsCtx.addMode(Mode.InlineableBody)
     val rhs1 = typedExpr(ddef.rhs, tpt1.tpe)(rhsCtx)
 
-    if (sym.isInlineable) PrepareInlineable.registerInlineInfo(sym, ddef.rhs, _ => rhs1)
+    if (sym.requiresInlineInfo) PrepareInlineable.registerInlineInfo(sym, ddef.rhs, _ => rhs1)
 
     if (sym.isConstructor && !sym.isPrimaryConstructor)
       for (param <- tparams1 ::: vparamss1.flatten)
@@ -1504,7 +1521,7 @@ class Typer extends Namer
      *  @param psym  Its type symbol
      *  @param cinfo The info of its constructor
      */
-    def maybeCall(ref: Tree, psym: Symbol, cinfo: Type): Tree = cinfo.stripPoly match {
+    def maybeCall(ref: Tree, psym: Symbol, cinfo: Type): Tree = cinfo.stripMethodPrefix match {
       case cinfo @ MethodType(Nil) if cinfo.resultType.isImplicitMethod =>
         typedExpr(untpd.New(untpd.TypedSplice(ref)(superCtx), Nil))(superCtx)
       case cinfo @ MethodType(Nil) if !cinfo.resultType.isInstanceOf[MethodType] =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Variances.scala b/compiler/src/dotty/tools/dotc/typer/Variances.scala
index e0e6b79b44a7..b383cadfeeda 100644
--- a/compiler/src/dotty/tools/dotc/typer/Variances.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Variances.scala
@@ -94,6 +94,8 @@ object Variances {
             v
         }
       varianceInArgs(varianceInType(tycon)(tparam), args, tycon.typeParams)
+    case TypeOf.Generic(args) =>
+      varianceInTypes(args)(tparam)
     case AnnotatedType(tp, annot) =>
       varianceInType(tp)(tparam) & varianceInAnnot(annot)(tparam)
     case AndType(tp1, tp2) =>
diff --git a/compiler/src/dotty/tools/repl/JLineTerminal.scala b/compiler/src/dotty/tools/repl/JLineTerminal.scala
index 22e44e4a5c36..41be7f89b98f 100644
--- a/compiler/src/dotty/tools/repl/JLineTerminal.scala
+++ b/compiler/src/dotty/tools/repl/JLineTerminal.scala
@@ -141,7 +141,7 @@ final class JLineTerminal extends java.io.Closeable {
               defaultParsedLine
           }
 
-        case _ =>
+        case _ | null =>
           incomplete()
       }
     }
diff --git a/compiler/src/dotty/tools/repl/ReplDriver.scala b/compiler/src/dotty/tools/repl/ReplDriver.scala
index 536c5fccd2c1..3cedcaae3eb5 100644
--- a/compiler/src/dotty/tools/repl/ReplDriver.scala
+++ b/compiler/src/dotty/tools/repl/ReplDriver.scala
@@ -13,7 +13,7 @@ import dotty.tools.dotc.core.NameOps._
 import dotty.tools.dotc.core.Names.Name
 import dotty.tools.dotc.core.StdNames._
 import dotty.tools.dotc.core.Symbols.{Symbol, defn}
-import dotty.tools.dotc.core.Types._
+import dotty.tools.dotc.core.Types.{TypeOf => _, _}
 import dotty.tools.dotc.interactive.Interactive
 import dotty.tools.dotc.printing.SyntaxHighlighting
 import dotty.tools.dotc.reporting.MessageRendering
diff --git a/compiler/test/dotc/pos-from-tasty.blacklist b/compiler/test/dotc/pos-from-tasty.blacklist
index a78823e99acd..9af35a94ebec 100644
--- a/compiler/test/dotc/pos-from-tasty.blacklist
+++ b/compiler/test/dotc/pos-from-tasty.blacklist
@@ -13,5 +13,9 @@ annot-bootstrap.scala
 # ScalaRunTime cannot be unpickled because it is already loaded
 repeatedArgs213.scala
 
+# Wildcard assigned to something else while unpickling
+from-tasty-wildcard.scala
+dependent5.scala
+
 # Error printing parent constructors that are blocks
 default-super.scala
diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala
index 6820fa8bb6f4..0c0a7dd5eed4 100644
--- a/compiler/test/dotty/tools/dotc/CompilationTests.scala
+++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala
@@ -182,6 +182,13 @@ class CompilationTests extends ParallelTesting {
 
   @Test def pickling: Unit = {
     implicit val testGroup: TestGroup = TestGroup("testPickling")
+    compileFile("tests/pos/dependent-patterns.scala", picklingOptions) +
+    compileFile("tests/pos/dependent.scala", picklingOptions) +
+    compileFile("tests/pos/dependent2.scala", picklingOptions) +
+    compileFile("tests/pos/dependent3.scala", picklingOptions) +
+    compileFile("tests/pos/dependent4.scala", picklingOptions) +
+    compileFile("tests/pos/dependent5-min.scala", picklingOptions) +
+    compileFile("tests/pos/dependent5.scala", picklingOptions) +
     compileFilesInDir("tests/new", picklingOptions) +
     compileFilesInDir("tests/pickling", picklingOptions)
   }.checkCompile()
diff --git a/doc-tool/src/dotty/tools/dottydoc/model/factories.scala b/doc-tool/src/dotty/tools/dottydoc/model/factories.scala
index 968428e30056..4228e37df6fb 100644
--- a/doc-tool/src/dotty/tools/dottydoc/model/factories.scala
+++ b/doc-tool/src/dotty/tools/dottydoc/model/factories.scala
@@ -95,6 +95,9 @@ object factories {
       case t: ThisType =>
         expandTpe(t.underlying)
 
+      case t: TypeOf =>
+        expandTpe(t.underlying)
+
       case AnnotatedType(t, _) =>
         expandTpe(t)
 
@@ -182,6 +185,9 @@ object factories {
     case mp: TermParamRef =>
       paramLists(mp.underlying)
 
+    case to: TypeOf =>
+      paramLists(to.underlying)
+
     case annot: AnnotatedType =>
       paramLists(annot.parent)
 
diff --git a/docs/docs/internals/syntax.md b/docs/docs/internals/syntax.md
index 4dd9c3e8ff20..24ebd99bc6bc 100644
--- a/docs/docs/internals/syntax.md
+++ b/docs/docs/internals/syntax.md
@@ -137,6 +137,7 @@ SimpleType        ::=  SimpleType TypeArgs
                     |  ‘(’ ArgTypes ‘)’                                         Tuple(ts)
                     |  ‘_’ TypeBounds
                     |  Refinement                                               RefinedTypeTree(EmptyTree, refinement)
+                    |  TypeOf                                                   TypeOfTypeTree(expr)
                     |  SimpleLiteral                                            SingletonTypeTree(l)
 ArgTypes          ::=  Type {‘,’ Type}
                     |  NamedTypeArg {‘,’ NamedTypeArg}
@@ -148,6 +149,7 @@ TypeArgs          ::=  ‘[’ ArgTypes ‘]’
 NamedTypeArg      ::=  id ‘=’ Type                                              NamedArg(id, t)
 NamedTypeArgs     ::=  ‘[’ NamedTypeArg {‘,’ NamedTypeArg} ‘]’                  nts
 Refinement        ::=  ‘{’ [RefineDcl] {semi [RefineDcl]} ‘}’                   ds
+TypeOf            ::=  ‘{’ Expr1 ‘}’                                            expr
 TypeBounds        ::=  [‘>:’ Type] [‘<:’ Type] | INT                            TypeBoundsTree(lo, hi)
 TypeParamBounds   ::=  TypeBounds {‘<%’ Type} {‘:’ Type}                        ContextBounds(typeBounds, tps)
 ```
diff --git a/library/src/scala/tasty/reflect/TypeOrBoundsOps.scala b/library/src/scala/tasty/reflect/TypeOrBoundsOps.scala
index 946467ec0644..70e3e153f37e 100644
--- a/library/src/scala/tasty/reflect/TypeOrBoundsOps.scala
+++ b/library/src/scala/tasty/reflect/TypeOrBoundsOps.scala
@@ -82,6 +82,11 @@ trait TypeOrBoundsOps extends TastyCore {
       def unapply(typeOrBounds: TypeOrBounds)(implicit ctx: Context): Option[(Type, Term)]
     }
 
+    val TypeOf: TypeOfExtractor
+    abstract class TypeOfExtractor {
+      def unapply(typeOrBounds: TypeOrBounds)(implicit ctx: Context): Option[(Type, Term)]
+    }
+
     val AndType: AndTypeExtractor
     abstract class AndTypeExtractor {
       def unapply(typeOrBounds: TypeOrBounds)(implicit ctx: Context): Option[(Type, Type)]
diff --git a/library/src/scala/tasty/util/ShowExtractors.scala b/library/src/scala/tasty/util/ShowExtractors.scala
index 22da8dd63343..d1394f7a434f 100644
--- a/library/src/scala/tasty/util/ShowExtractors.scala
+++ b/library/src/scala/tasty/util/ShowExtractors.scala
@@ -173,6 +173,8 @@ class ShowExtractors[T <: Tasty with Singleton](tasty0: T) extends Show[T](tasty
         this += "Type.AppliedType(" += tycon += ", " ++= args += ")"
       case Type.AnnotatedType(underlying, annot) =>
         this += "Type.AnnotatedType(" += underlying += ", " += annot += ")"
+      case Type.TypeOf(underlying, tree) =>
+        this += "Type.TypeOf(" += underlying += ", " += tree += ")"
       case Type.AndType(left, right) =>
         this += "Type.AndType(" += left += ", " += right += ")"
       case Type.OrType(left, right) =>
diff --git a/library/src/scala/tasty/util/ShowSourceCode.scala b/library/src/scala/tasty/util/ShowSourceCode.scala
index f67d8c8bc8dc..4daf7b260bce 100644
--- a/library/src/scala/tasty/util/ShowSourceCode.scala
+++ b/library/src/scala/tasty/util/ShowSourceCode.scala
@@ -877,6 +877,9 @@ class ShowSourceCode[T <: Tasty with Singleton](tasty0: T) extends Show[T](tasty
         this += " "
         printAnnotation(annot)
 
+      case Type.TypeOf(tp, tree) =>
+        this += "{ ??? }" // TODO
+
       case Type.AndType(left, right) =>
         printType(left)
         this += " & "
diff --git a/tests/disabled/reflect/run/t7974/Symbols.scala b/tests/disabled/reflect/run/t7974/Symbols-test.scala
similarity index 100%
rename from tests/disabled/reflect/run/t7974/Symbols.scala
rename to tests/disabled/reflect/run/t7974/Symbols-test.scala
diff --git a/tests/neg/dependent-match.scala b/tests/neg/dependent-match.scala
new file mode 100644
index 000000000000..a622cb160527
--- /dev/null
+++ b/tests/neg/dependent-match.scala
@@ -0,0 +1,15 @@
+object Test {
+  trait Bar
+  trait Foo extends Bar
+
+  dependent def test(t: Any) =
+    t match {
+      case x: Bar => "a"
+      case _ => 1
+    }
+
+  // def f1[T <: Foo](t: T): "a" = test(t) // Do we want this?
+  //def f1[T <: Foo](t: T): Any = test(t)
+  def f2(x: Foo): "a"  = test(x)  // error: matches are not supported yet
+  // def f3(x: String): 1 = test(x)
+}
diff --git a/tests/neg/dependent.scala b/tests/neg/dependent.scala
new file mode 100644
index 000000000000..4e86c4e1ba42
--- /dev/null
+++ b/tests/neg/dependent.scala
@@ -0,0 +1,77 @@
+object Invalid {
+  dependent def f(x: Int) = x + 1
+  f(1): String  // error
+  f(1): {0}  // error
+
+  // val y: Int = ???
+  // type YPlusOne = {while}  // TODO: errror: Non-sensical singleton-type expression: ...
+}
+
+object Foo {
+  dependent def foo(b: Boolean): { if (b) 1 else 2 } =
+    if (b) 1 else 2
+
+  foo(true):  { if(true) 2 else 1 }  // error
+  foo(false): { if(false) 2 else 1 }  // error
+
+  var b: Boolean = true
+  foo(b): { 1 }  // error
+}
+
+object NullTests {
+  dependent def f(x: String): Boolean = x == null
+  val a1: false = f("aa")  // error: can't reduce in the presence of null
+  val a2: true  = f(null)  // error: can't reduce in the presence of null
+  val a3: true  = f("aa")  // error: can't reduce in the presence of null
+  val a4: false = f(null)  // error: can't reduce in the presence of null
+  val a5: { "aa" == null } = f("aa")
+
+  dependent def g(x: String): Boolean = x.isInstanceOf[String]
+  val b1: true  = g("aa")
+  val b2: true  = g(null)  // error: can't reduce in the presence of null
+  val b3: false = g(null)  // error: can't reduce in the presence of null
+
+  dependent def h(x: String): String = x + "A"
+  val x: { h(null) } = h(null)
+  val y = h(null)
+
+  dependent def hTest: Unit = {
+    val y = h(null)
+    val z: { h(null) } = y
+  }
+}
+
+// object CyclicTransparenType {
+//   dependent def trans(j: Int): Int = {
+//     println(opaque(j))
+//     2 * j
+//   }
+
+//   def opaque(i: Int) = {trans(2): { 2 * 2 }} + i
+// }
+
+// object SimpleEqs {
+//   val x = 1
+//   val y: {x} = x
+//   implicitly[{x + 1} =:= {y}]  // errror
+//   implicitly[{x + 1} =:= {y + 2}]  // errror
+//   implicitly[{x + 1} =:= {1 + y}]  // errror: TypeComparer doesn't know about commutativity
+
+//   val b = true
+//   implicitly[{b} =:= {b}]
+//   implicitly[{!b} =:= {!b}]
+//   implicitly[{!b} =:= {b}]  // errror
+// }
+
+
+// object Stability {
+//   def f1(x: Int): Int = x
+//   def f2(x: Int): {x} = x
+
+//   val x = 1
+//   implicitly[{f1(x)} =:= {x}]  // errror: f1 is not considered stable  // errror: f1's result type is not precise enough
+//   implicitly[{f1(x)} =:= {f1(x)}]  // errror: f1 is not considered stable  // errror: f1 is not considered stable
+//   implicitly[{f2(x)} =:= {x}]
+//   implicitly[{f2(x)} =:= {f2(x)}]
+//   implicitly[{f1(x)} =:= {f2(x)}]  // errror: f1 is not considered stable  // errror: f1's result type is not precise enough
+// }
diff --git a/tests/neg/i3901.scala b/tests/neg/i3901.scala
deleted file mode 100644
index 8e1451d4628e..000000000000
--- a/tests/neg/i3901.scala
+++ /dev/null
@@ -1,4 +0,0 @@
-object Crash {
-  def f(cond: => Boolean): cond.type = ???  // error: cond is not stable
-  f(true)
-}
diff --git a/tests/patmat/sealed-java-enums.scala b/tests/pending/sealed-java-enums.scala
similarity index 100%
rename from tests/patmat/sealed-java-enums.scala
rename to tests/pending/sealed-java-enums.scala
diff --git a/tests/pos/dependent-hlist-bench.scala b/tests/pos/dependent-hlist-bench.scala
new file mode 100644
index 000000000000..d3dfefcbf92d
--- /dev/null
+++ b/tests/pos/dependent-hlist-bench.scala
@@ -0,0 +1,43 @@
+sealed trait HList {
+  dependent def ++(that: HList): HList =
+    if (this.isInstanceOf[HNil.type]) that
+    else HCons(this.asInstanceOf[HCons].head, this.asInstanceOf[HCons].tail ++ that)
+
+  dependent def apply(index: Int): Int =
+    if (index <= 0) this.asInstanceOf[HCons].head
+    else this.asInstanceOf[HCons].tail.apply(index - 1)
+}
+dependent case class HCons(head: Int, tail: HList) extends HList
+dependent case object HNil extends HList
+
+object Test extends App {
+  def main() = {
+    dependent def xs0 = HCons(1, HCons(2, HCons(3, HCons(4, HCons(5, HCons(6, HCons(7, HCons(8, HCons(9, HCons(10, HCons(11, HCons(12, HCons(13, HCons(14, HCons(15, HCons(16, HNil))))))))))))))))
+    xs0(15): 16
+
+    dependent def xs1 = xs0 ++ xs0
+    xs1(31): 16
+
+    dependent def xs2 = xs1 ++ xs1
+    xs2(63): 16
+
+    dependent def xs3 = xs2 ++ xs2
+    xs3(127): 16
+
+    dependent def xs4 = xs3 ++ xs3
+    xs4(255): 16
+
+    // Add -Xss4M to javaOptions to compile with larger types...
+    // dependent def xs5 = xs4 ++ xs4
+    // xs5(511): 16
+
+    // dependent def xs6 = xs5 ++ xs5
+    // xs6(1023): 16
+
+    // dependent def xs7 = xs6 ++ xs6
+    // xs7(2047): 16
+
+    // dependent def xs8 = xs7 ++ xs7
+    // xs8(4095): 16 // ~5s
+  }
+}
diff --git a/tests/pos/dependent-patterns.scala b/tests/pos/dependent-patterns.scala
new file mode 100644
index 000000000000..69c1bd28877d
--- /dev/null
+++ b/tests/pos/dependent-patterns.scala
@@ -0,0 +1,188 @@
+// (x: Any) match {
+//   case _: T         => // x.iIO[T]
+//   case _: T | _: U  => // x.iIO[T] || x.iIO[U]
+//   // case _: p.type    => // x eq p
+//   case _: T[A1, A2] => // x.iIO[T[_, _]]
+//   case 1            => // 1 == x // Overloading?
+//   case Nil          => // Nil == x
+
+//   case UnapplyBooleanT(_)   => // x.iIO[T] && UnapplyBooleanT.unapply(x.aIO)
+//   case UnapplyProductT(_)   => // x.iIO[T]
+//   // case UnapplyNameBasedT(_) => // x.iIO[T] && !UnapplyNameBasedT.unapply(x.aIO).isEmpty
+// }
+
+trait F[X]
+trait T
+trait U
+object NIL
+
+object UnapplyBooleanT {
+  def unapply(t: T): Boolean = ???
+}
+object UnapplyBooleanT_true {
+  dependent def unapply(t: T): Boolean = true
+}
+object UnapplyBooleanT_false {
+  dependent def unapply(t: T): Boolean = false
+}
+
+object UnapplyProductT {
+  def unapply(t: T): Tuple2[Int, String] = (1, "")
+}
+
+object UnapplyNameBasedT {
+  def unapply(t: T): Option[String] = ???
+}
+object UnapplyNameBasedT_None {
+  dependent def unapply(t: T): Option[String] = None
+}
+object UnapplyNameBasedT_Some {
+  dependent def unapply(t: T): Option[String] = Some("")
+}
+
+object Test {
+  var any: Any = null
+
+  // --------------------------------------------------------------------------
+  // dependent def typePattern(x: Any) =
+  //   x match {
+  //     case _: T => 1
+  //     case _    => 2
+  //   }
+  dependent def typeDesugared(x: Any) =
+    if (x.isInstanceOf[T]) 1 else 2
+
+  // typePattern(any): { typeDesugared(any) } //-
+  // typePattern(new T{})   : 1 //-
+  val t: T = new T{}
+  typeDesugared(t) : 1 //-
+  // typePattern("")        : 2 //-
+  typeDesugared("")      : 2 //-
+
+  // --------------------------------------------------------------------------
+  // dependent def typedHKPattern(x: Any) =
+  //   x match {
+  //     case _: F[Int] => 1
+  //     case _         => 2
+  //   }
+  dependent def typedHKDesugared(x: Any) =
+    if (x.isInstanceOf[F[Int]]) 1 else 2
+
+  // typedHK(any): { typedHKDesugared(any) } //-
+  // typedHK(new F[Int]{})             : 1 //-
+  typedHKDesugared(new F[String]{}) : 1 //-
+  // typedHK("")                       : 2 //-
+  typedHKDesugared("")              : 2 //-
+
+  // --------------------------------------------------------------------------
+  // dependent def alternativePattern(x: Any) =
+  //   x match {
+  //     case _: T | _: U => 1
+  //     case _           => 2
+  //   }
+  dependent def alternativeDesugared(x: Any) =
+    if (x.isInstanceOf[T] || x.isInstanceOf[U]) 1 else 2
+
+  // alternativePattern(any): { alternativeDesugared(any) } //-
+  // alternativePattern(new T{})          : 1 //-
+  alternativeDesugared(new T{}) : 1 //-
+  // alternativePattern(new U{})          : 1 //-
+  alternativeDesugared(new U{}) : 1 //-
+  // alternativePattern("")               : 2 //-
+  alternativeDesugared("")      : 2 //-
+
+  // --------------------------------------------------------------------------
+  // dependent def stablePattern(x: Any) =
+  //   x match {
+  //     case NIL => 1
+  //     case _   => 2
+  //   }
+  dependent def stableDesugared(x: Any) =
+    if (NIL == x) 1 else 2
+
+  // stablePattern(any): { stableDesugared(any) } //-
+  // // For these cases we would need to dependentify AnyRef.== (to `eq`) //-
+  // // and prove that there is only one value of `NIL`. //-
+  // stablePattern(NIL)          : 1 //-
+  // stableDesugared(NIL) : 1 //-
+  // stablePattern("")           : 2 //-
+  // stableDesugared("")  : 2 //-
+
+  // --------------------------------------------------------------------------
+  // dependent def literalPattern(x: Any) =
+  //   x match {
+  //     case 0 => 1
+  //     case _ => 2
+  //   }
+  dependent def literalDesugared(x: Any) =
+    if (0 == x) 1 else 2
+
+  // literalPattern(any): { literalDesugared(any) } //-
+  // literalPattern(0)           : 1 //-
+  literalDesugared(0)  : 1 //-
+  // These two get stuck on `0 == ""`, which is not simplifed to false by the constant folder...
+  // literalPattern("")   : 2 //-
+  // literalDesugared("") : 2 //-
+
+  // --------------------------------------------------------------------------
+  // dependent def unapplyBoolPattern(x: Any) =
+  //   x match {
+  //     case UnapplyBooleanT() => 1
+  //     case _                  => 2
+  //   }
+  // dependent def unapplyTruePattern(x: Any) =
+  //   x match {
+  //     case UnapplyBooleanT_true() => 1
+  //     case _                       => 2
+  //   }
+  // dependent def unapplyFalsePattern(x: Any) =
+  //   x match {
+  //     case UnapplyBooleanT_false() => 1
+  //     case _                        => 2
+  //   }
+
+  dependent def unapplyBoolDesugared(x: Any) =
+    if (x.isInstanceOf[T] && UnapplyBooleanT.unapply(x.asInstanceOf[T])) 1 else 2
+
+  dependent def unapplyTrueDesugared(x: Any) =
+    if (x.isInstanceOf[T] && UnapplyBooleanT_true.unapply(x.asInstanceOf[T])) 1 else 2
+
+  dependent def unapplyFalseDesugared(x: Any) =
+    if (x.isInstanceOf[T] && UnapplyBooleanT_false.unapply(x.asInstanceOf[T])) 1 else 2
+
+  // unapplyBoolPattern(any): { unapplyBoolDesugared(any) } //-
+  // unapplyTruePattern(any): { unapplyTrueDesugared(any) } //-
+  // unapplyFalsePattern(any): { unapplyFalseDesugared(any) } //-
+
+  // unapplyBoolPattern("")         : 2 //-
+  // unapplyTruePattern("")         : 2 //-
+  // unapplyFalsePattern("")        : 2 //-
+  // These 3 cases require the normalizer to implement the short circuit semantic of &&:
+  // unapplyBoolDesugared("")       : 2 //-
+  // unapplyTrueDesugared("")       : 2 //-
+  // unapplyFalseDesugared("")      : 2 //-
+
+  // unapplyTruePattern(new T{})    : 1 //-
+  unapplyTrueDesugared(new T{})  : 1 //-
+  // unapplyFalsePattern(new T{})   : 2 //-
+  unapplyFalseDesugared(new T{}) : 2 //-
+
+  // dependent def unapplyProductPattern(x: Any) =
+  //   x match {
+  //     case UnapplyProductT(_, _) => 1
+  //     case _                     => 2
+  //   }
+  dependent def unapplyProductDesugared(x: Any) =
+    if (x.isInstanceOf[T]) 1 else 2
+
+  // unapplyProductPattern(any): { unapplyProductDesugared(any) } //-
+  // unapplyProductPattern(new T{})   : 1 //-
+  unapplyProductDesugared(new T{}) : 1 //-
+  // unapplyProductPattern("")        : 2 //-
+  unapplyProductDesugared("")      : 2 //-
+
+  // TODO
+  // case UnapplyNameBasedT(_) => 1
+  // case UnapplyNameBasedT_None(_) => 1
+  // case UnapplyNameBasedT_Some(_) => 1
+}
diff --git a/tests/pos/dependent.scala b/tests/pos/dependent.scala
new file mode 100644
index 000000000000..358b6295154a
--- /dev/null
+++ b/tests/pos/dependent.scala
@@ -0,0 +1,184 @@
+object SimpleEqs {
+  val x = 1
+  val y: {x} = x
+  // val z: {y + 1} = y + 1
+}
+
+object Call {
+  dependent def foo(x: Int) = 123
+  foo(1): { foo(1) }
+  foo(1): Int
+}
+
+object ITE {
+  dependent def foo1(b: Boolean) = {
+    val res = if (b)
+      1
+    else
+      2
+    identity[{ if (b) 1 else 2 }](res)
+    res
+  }
+
+  dependent def foo2(b: Boolean): { if (b) 1 else 2 } =
+    if (b) 1 else 2
+
+  var b: Boolean = true
+
+  // Beta-reduce
+  foo1(true):  { if(true) 1 else 2 }
+  foo1(false): { if(false) 1 else 2 }
+  foo1(b):     { if (b) 1 else 2 }
+
+  foo1(true):  { 1 }
+  foo1(false): { 2 }
+
+  foo2(true):  { if(true) 1 else 2 }
+  foo2(false): { if(false) 1 else 2 }
+  foo2(b):     { if (b) 1 else 2 }
+}
+
+// object Match { TODO
+//   dependent def foo1(b: Boolean) = {
+//     val res = b match {
+//       case true => 1
+//       case false => 2
+//     }
+//     identity[{ b match { case true => 1; case false => 2 } }](res)
+//     res
+//   }
+
+//   dependent def foo(b: Boolean): Int =
+//     b match { case true => 1; case false => 2 }
+// }
+
+object Applied {
+  dependent def foo1(b: Boolean) = ???
+  dependent def foo2(b: Boolean): { foo1(b) } = foo1(b)
+  val a: { foo2(true) } = foo2(true)
+}
+
+object Approx1 {
+  dependent def foo(x: Any): { x } = x
+  class A {
+    dependent def bar(i: Int): Int = i + 1
+    val v: { bar(foo(1)) } = bar(foo(1))
+  }
+
+  val a = new A {}
+  val b: { a.bar(foo(1)) } = a.v
+
+  var c = new A {}
+  val d: { c.bar(foo(1)) } = c.v
+}
+
+object Approx2 {
+  dependent def foo(x: Any): { x } = x
+  class A {
+    dependent def bar(i: Int): Int = i + 1
+    val v: { foo(bar(1)) } = foo(bar(1))
+  }
+
+  val a = new A {}
+  val b: { foo(a.bar(1)) }= a.v
+
+  val c = new A {}
+  val d: { foo(c.bar(1)) }= c.v
+}
+
+object SimpleType {
+  type A = { 2 * 2 }
+}
+
+
+object Ignored {
+  val a = 1
+  dependent def plus(a: Int, b: Int) = a + b
+
+  type Foo = {{
+    case class Bar(i: Int)
+    println(Bar(1))
+    plus(a, a)
+  }}
+
+  type Bar = { plus(a, a) }
+
+  val foo: Foo = ???
+  identity[Foo](identity[Bar](foo))
+
+  implicitly[Foo =:= Bar]
+}
+
+// object AvoidLocalRefs {
+//   type Id[T] = T
+
+//   val x = 1
+//   def y = { val a: {x} = x; val t: Id[{a + 1}] = a + 1; t }
+//   def z: {x + 1} = { val a: {x} = x; val t: Id[{a + 1}] = a + 1; t }
+
+//   { val a = 0; a + 1 }
+//   { val a = 0; 1 + a }
+// }
+
+
+// object Bounds {
+//   @annotation.implicitNotFound(msg = "Cannot prove that ${B} holds.")
+//   sealed abstract class P[B <: Boolean](val b: B)
+//   private[this] val prop_singleton = new P[true](true) {}
+//   object P {
+//     def assume(b: Boolean): P[b.type] = prop_singleton.asInstanceOf[P[b.type]]
+//   }
+
+//   def if_(cond: Boolean): (implicit (ev: P[cond.type]) => Unit) => Unit =
+//     thn => if (cond) thn(P.assume(cond))
+
+
+//   // Bounds-checked
+
+//   def index(k: Int)(implicit ev: P[{k >= 0}]): Int = k
+
+//   def run(i: Int) =
+//     if_(i >= 0) {
+//       index(i)
+//     }
+
+
+//   // Boxed value with a predicate
+
+//   class PredBox[T, B <: Boolean](val v: T)(val p: P[B])
+//   object PredBox {
+//     def apply[T, B <: Boolean](v: T)(implicit ev: P[B]) = new PredBox[T, B](v)(ev)
+//   }
+
+//   def run2(i: Int) =
+//     if_(i != 0) {
+//       PredBox[Int, {i != 0}](i)
+//     }
+// }
+
+
+// object ArithmeticIdentities {
+//   type SInt = Int & Singleton
+
+//   class DecomposeHelper[V <: SInt](val v: V) {
+//     import DecomposeHelper._
+//     def asSumOf[X <: SInt, Y <: SInt](x: X, y: Y)(implicit ev: {v} =:= {x + y}): SumOf[{x}, {y}] = SumOf(x, y)(ev(v))
+//   }
+
+//   object DecomposeHelper {
+//     /* Axioms */
+//     sealed trait Decomposition[V <: SInt]
+//     case class SumOf[X <: SInt, Y <: SInt](x: X, y: Y)(val v: {x + y}) extends Decomposition[{v}] {
+//       def commuted: SumOf[Y, X] = SumOf(y, x)(v.asInstanceOf[{y + x}])
+//     }
+//   }
+
+//   implicit def toDecomposeHelper[V <: Int](v: V): DecomposeHelper[v.type] = new DecomposeHelper(v)
+
+
+//   // Let's "show" that x + 1 == 1 + x
+
+//   val x = 123
+//   (x + 1).asSumOf(x, 1).v: {x + 1}
+//   (x + 1).asSumOf(x, 1).commuted.v: {1 + x}
+// }
diff --git a/tests/pos/dependent2.scala b/tests/pos/dependent2.scala
new file mode 100644
index 000000000000..cb8271d86826
--- /dev/null
+++ b/tests/pos/dependent2.scala
@@ -0,0 +1,52 @@
+object DepNats {
+  sealed trait Nat { val pred: Nat }
+  dependent case object Zero extends Nat { val pred: Nat = Zero }
+  dependent case class Succ(pred: Nat) extends Nat
+
+  dependent def asNat(i: Int): Nat =
+    if (i == 0) Zero
+    else        Succ(asNat(i - 1))
+
+  type Nat0 = {Zero}
+  type Nat1 = {Succ(Zero)}
+  type Nat2 = {Succ(Succ(Zero))}
+
+  val Nat0: Nat0 = asNat(0)
+  val Nat1: Nat1 = asNat(1)
+  val Nat2: Nat2 = asNat(2)
+
+  dependent def isZero(a: Nat): Boolean =
+    a.isInstanceOf[Zero.type]
+
+  dependent def isZeroT[T](a: T): Boolean =
+    a.isInstanceOf[Zero.type]
+
+  val v1: true =  isZero(Zero)
+  val v2: false = isZero(Succ(Zero))
+  val v3: true =  isZeroT(Zero)
+  val v4: false = isZeroT(Succ(Zero))
+
+  implicitly[{isZero(Nat0)} =:= true]
+
+  def forward1[T <: Nat](t: T): { t.isInstanceOf[Zero.type] } = isZeroT(t)
+  def forward2[T <: Zero.type](t: T): true = isZeroT(t)
+  def forward3[T <: Succ](t: T): false = isZeroT(t)
+
+  // val s5: { isZeroT(n) } = forward(Zero)
+  // var n: Nat = Zero
+
+  val _0a: {Zero}       = Succ(Zero).pred
+  val _0b: {Zero}       = Nat1.pred
+  val _1a: {Succ(Zero)} = Nat2.pred
+  val _1b: Nat1         = Nat2.pred
+//  val _1c: {Nat1}        = Nat2.pred
+
+  dependent def plus(n: Nat, m: Nat): Nat =
+    if (isZero(m)) n
+    else           plus(Succ(n), m.pred)
+
+  plus(Zero, Zero)       : Nat0
+  plus(Succ(Zero), Zero) : Nat1
+  plus(Zero, Succ(Zero)) : Nat1
+  plus(Nat1, Nat1)       : Nat2
+}
diff --git a/tests/pos/dependent3.scala b/tests/pos/dependent3.scala
new file mode 100644
index 000000000000..44b51037ed0d
--- /dev/null
+++ b/tests/pos/dependent3.scala
@@ -0,0 +1,71 @@
+object BooleanListLengthFunction {
+  dependent def length(l: LIST): Int =
+    if (l.isInstanceOf[NIL.type]) 0
+    else 1 + length(l.asInstanceOf[CONS].tail)
+
+  sealed trait LIST
+  dependent case object NIL extends LIST
+  dependent case class CONS(head: Boolean, tail: LIST) extends LIST
+
+  val a: 0 = length(NIL)
+  val b: 1 = length(CONS(true, NIL))
+  val c: 2 = length(CONS(true, CONS(false, NIL)))
+  val d: 3 = length(CONS(true, CONS(false, CONS(true, NIL))))
+}
+
+object GenericListInstanceOf {
+  sealed trait LIST[+T]
+  dependent case object NIL extends LIST[Nothing]
+  dependent case class CONS[+T](head: T, tail: LIST[T]) extends LIST[T]
+
+  dependent def iioNIL(x: Any) = x.isInstanceOf[NIL.type]
+  dependent def iioCONS(x: Any) = x.isInstanceOf[CONS[_]]
+
+  val x1: true  = iioNIL(NIL)
+  val x2: false = iioCONS(NIL)
+  val x3: false = iioNIL(CONS(true, NIL))
+  val x4: true  = iioCONS(CONS(true, NIL))
+
+  dependent def iioNIL_T[T](x: LIST[T]) = x.isInstanceOf[NIL.type]
+  dependent def iioCONS_T[T](x: LIST[T]) = x.isInstanceOf[CONS[_]]
+
+  val x5: true  = iioNIL_T(NIL)
+  val x6: false = iioCONS_T(NIL)
+  val x7: false = iioNIL_T(CONS(true, NIL))
+  val x8: true  = iioCONS_T(CONS(true, NIL))
+}
+
+object G {
+  sealed trait LIST[+T]
+  dependent case object NIL extends LIST[Nothing]
+  dependent case class CONS[+T](head: T, tail: LIST[T]) extends LIST[T]
+
+  dependent def AIO_tail(l: Any) = l.asInstanceOf[CONS[Boolean]].tail
+  val nil: NIL.type = AIO_tail(CONS(true, NIL))
+}
+
+object GenericListLengthFunction {
+  dependent def length[T](l: LIST[T]): Int =
+    if (l.isInstanceOf[NIL.type]) 0
+    else 1 + length(l.asInstanceOf[CONS[T]].tail)
+
+  sealed trait LIST[+T]
+  dependent case object NIL extends LIST[Nothing]
+  dependent case class CONS[+T](head: T, tail: LIST[T]) extends LIST[T]
+
+  val x1: 0 = length(NIL)
+  val x2: 1 = length(CONS(true, NIL))
+}
+
+object GenericListLengthMethod {
+  sealed trait LIST[+T] {
+    dependent def length: Int =
+      if (this.isInstanceOf[NIL.type]) 0
+      else 1 + this.asInstanceOf[CONS[T]].tail.length
+  }
+  dependent case object NIL extends LIST[Nothing]
+  dependent case class CONS[+T](head: T, tail: LIST[T]) extends LIST[T]
+
+  val x1: 0 = NIL.length
+  val x2: 1 = CONS(true, NIL).length
+}
diff --git a/tests/pos/dependent4.scala b/tests/pos/dependent4.scala
new file mode 100644
index 000000000000..85f63bfae669
--- /dev/null
+++ b/tests/pos/dependent4.scala
@@ -0,0 +1,52 @@
+object ListIntConcat {
+  sealed trait List {
+    dependent def ++(that: List): List =
+      if (this.isInstanceOf[Nil.type]) that
+      else Cons(this.asInstanceOf[Cons].head, this.asInstanceOf[Cons].tail ++ that)
+  }
+  dependent case object Nil extends List
+  dependent case class Cons(head: Int, tail: List) extends List
+
+  val x1: Nil.type = Nil ++ Nil
+  val x2: { Cons(1, Nil) } = Cons(1, Nil) ++ Nil
+  val x3: { Cons(1, Nil) } = Nil ++ Cons(1, Nil)
+  val x4: { Cons(1, Cons(2, Nil)) } = Cons(1, Nil) ++ Cons(2, Nil)
+  val x4extra: { Cons(1, Cons(1, Nil)) } = x2 ++ x2
+  val x5: { Cons(1, Cons(2, Cons(3, Nil))) } = Cons(1, Nil) ++ Cons(2, Cons(3, Nil))
+  val x6: { Cons(1, Cons(2, Cons(3, Nil))) } = Cons(1, Cons(2, Nil)) ++ Cons(3, Nil)
+}
+
+object ListGenericConcat {
+  sealed trait List[T] {
+    dependent def ++(that: List[T]): List[T] =
+      if (this.isInstanceOf[Nil[T]]) that
+      else Cons(this.asInstanceOf[Cons[T]].head, this.asInstanceOf[Cons[T]].tail ++ that)
+  }
+  dependent case class Nil[T]() extends List[T]
+  dependent case class Cons[T](head: T, tail: List[T]) extends List[T]
+
+  val nil = new Nil[Int]()
+
+  val x1: Nil[Int] = nil ++ nil
+  val x2: { Cons(1, nil) } = Cons(1, nil) ++ nil
+  val x3: { Cons(1, nil) } = nil ++ Cons(1, nil)
+  val x4: { Cons(1, Cons(2, nil)) } = Cons(1, nil) ++ Cons(2, nil)
+  val x5: { Cons(1, Cons(2, Cons(3, nil))) } = Cons(1, nil) ++ Cons(2, Cons(3, nil))
+  // val x6: { Cons(1, Cons(2, Cons(3, nil))) } = Cons(1, Cons(2, nil)) ++ Cons(3, nil) // needs 230 steps
+}
+
+object ListCovariantConcat {
+  sealed trait List[+T] {
+    dependent def ++[TT >: T](that: List[TT]): List[TT] =
+      if (this.isInstanceOf[Nil.type]) that
+      else Cons(this.asInstanceOf[Cons[T]].head, this.asInstanceOf[Cons[T]].tail ++ that)
+  }
+  dependent case object Nil extends List[Nothing]
+  dependent case class Cons[+T](head: T, tail: List[T]) extends List[T]
+
+  val x2: { Cons(1, Nil) } = Cons(1, Nil) ++ Nil
+  val x3: { Cons(1, Nil) } = Nil ++ Cons(1, Nil)
+  val x4: { Cons(1, Cons(2, Nil)) } = Cons(1, Nil) ++ Cons(2, Nil)
+  val x5: { Cons(1, Cons(2, Cons(3, Nil))) } = Cons(1, Nil) ++ Cons(2, Cons(3, Nil))
+  // val x6: { Cons(1, Cons(2, Cons(3, Nil))) } = Cons(1, Cons(2, Nil)) ++ Cons(3, Nil) // needs 230 steps
+}
diff --git a/tests/pos/dependent5-min.scala b/tests/pos/dependent5-min.scala
new file mode 100644
index 000000000000..12388da5d35b
--- /dev/null
+++ b/tests/pos/dependent5-min.scala
@@ -0,0 +1,4 @@
+object Test {
+  dependent def foo(x: Option[Int]): Option[Int] =
+    foo(x)
+}
diff --git a/tests/pos/dependent5.scala b/tests/pos/dependent5.scala
new file mode 100644
index 000000000000..83ba5d0878d9
--- /dev/null
+++ b/tests/pos/dependent5.scala
@@ -0,0 +1,166 @@
+object IdrisVect {
+  dependent def þ [T] : T = ??? : T
+
+  sealed trait Nat { val pred: Nat }
+  dependent case object Zero extends Nat { val pred: Nat = Zero }
+  dependent case class Succ(pred: Nat) extends Nat
+
+  // case class Fin(n: Nat, m: Nat, ev: [n < m])
+
+  sealed trait Fin { def bound: Nat }
+  dependent case class FinZero(val bound: Succ) extends Fin
+  dependent case class FinSucc(f: Fin) extends Fin {
+    val bound: { Succ(f.bound) } = Succ(f.bound)
+  }
+
+  object Nat {
+    type _0 = { Zero }
+    type _1 = { Succ(Zero) }
+    type _2 = { Succ(Succ(Zero)) }
+    type _3 = { Succ(Succ(Succ(Zero))) }
+  }
+  import Nat._
+
+  sealed trait  Vect[T] { def length: Nat }
+  dependent case class Nil[T](length: Zero.type) extends Vect[T]
+  dependent case class Cons[T](head: T, tail: Vect[T], length: Nat) extends Vect[T]
+
+  object Vect {
+    dependent def sized[T](n: Nat) = Cons(þ[T], þ[Vect[T]], n)
+    dependent def nil = Nil[Int](Zero)
+    dependent def cons(head: Int, tail: Vect[Int]): Vect[Int] = Cons(head, tail, Succ(tail.length))
+  }
+  import Vect._
+
+  val y0: _0 = nil.length
+  val y1: _1 = cons(1, nil).length
+  val y2: _2 = cons(1, cons(2, nil)).length
+  val y3: _3 = cons(1, cons(2, cons(3, nil))).length
+
+  dependent def concat(v1: Vect[Int], v2: Vect[Int]): Vect[Int] = {
+    if (v1.isInstanceOf[Nil[Int]]) v2
+    else {
+      val vv1 = v1.asInstanceOf[Cons[Int]]
+      cons(vv1.head, concat(vv1.tail, v2))
+    }
+  }
+
+  val x1: { nil }                            = concat(nil, nil)
+  val x2: { cons(1, nil) }                   = concat(cons(1, nil), nil)
+  val x3: { cons(1, nil) }                   = concat(nil, cons(1, nil))
+  val x4: { cons(1, cons(2, nil)) }          = concat(cons(1, nil), cons(2, nil))
+  val x5: { cons(1, cons(2, cons(3, nil))) } = concat(cons(1, nil), cons(2, cons(3, nil)))
+
+
+  val x1b: { Nil(þ[Zero.type]) } = concat(nil, nil)
+  val x5b: { Cons(þ, þ, þ[_3]) } = concat(cons(1, nil), cons(2, cons(3, nil)))
+  val x5c: { sized(þ[_3]) }      = concat(cons(1, nil), cons(2, cons(3, nil)))
+
+  /** Calculate the length of a `Vect`. */
+  dependent def length[T](xs: Vect[T]): Nat =
+    if (xs.isInstanceOf[Nil[_]]) Zero
+    else {
+      val xs1 = xs.asInstanceOf[Cons[_]].tail
+      Succ(length(xs1))
+    }
+
+  val l1_member: _0 = x1.length
+  val l2_member: _1 = x2.length
+  val l3_member: _1 = x3.length
+  val l4_member: _2 = x4.length
+  val l5_member: _3 = x5.length
+
+  val l1: _0 = length(x1)
+  val l2: _1 = length(x2)
+  val l3: _1 = length(x3)
+  val l4: _2 = length(x4)
+  val l5: _3 = length(x5)
+
+  // val _: { Vect.sized[Int](Succ(þ[Nat])) } = "abc"
+  def f[T](x: { Vect.sized[T](Succ(þ[Nat])) }, y: Int) = ???
+  // f(x2)
+  // /** All but the first element of the vector */
+  // dependent def tail[T](v: { Vect.sized[T](Succ(þ[Nat])) }): Vect[T] =
+  //   v.asInstanceOf[Cons[T]].tail
+
+  // // val t1: { nil }                   = tail(x1) // error: stuck on failing asInstanceOf, as expected!
+  // val t2: { nil }                   = tail(x2)
+  // val t3: { nil }                   = tail(x3)
+  // val t4: { cons(2, nil) }          = tail(x4)
+  // val t5: { cons(2, cons(3, nil)) } = tail(x5)
+
+  /** Only the first element of the vector */
+  dependent def head[T](v: Vect[T]): T =
+    v.asInstanceOf[Cons[T]].head
+
+  // val h1: 1 = head[Int](x1) // error: stuck on failing asInstanceOf, as expected!
+  val h2: 1 = head[Int](x2)
+  val h3: 1 = head[Int](x3) // TODO: inference fucks it up when we don't put the explicit [Int]
+  val h4: 1 = head[Int](x4)
+  val h5: 1 = head[Int](x5)
+
+  dependent def headSafe[T](v: { Vect.sized[T](Succ(þ[Nat])) }): T =
+    v.asInstanceOf[Cons[T]].head
+
+  // val hs1: 1 = headSafe[Int](x1) // error: not a subtype
+  val hs2: 1 = headSafe[Int](x2)
+  val hs3: 1 = headSafe[Int](x3) // TODO: inference fucks it up when we don't put the explicit [Int]
+  val hs4: 1 = headSafe[Int](x4)
+  val hs5: 1 = headSafe[Int](x5)
+
+  def headSafeOpaque[T](v: { Vect.sized[T](Succ(þ[Nat])) }): T =
+    v.asInstanceOf[Cons[T]].head
+
+  // val hso1: Int = headSafeOpaque[Int](x1) // error: not a subtype
+  val hso2: Int = headSafeOpaque[Int](x2)
+  val hso3: Int = headSafeOpaque[Int](x3) // TODO: inference fucks it up when we don't put the explicit [Int]
+  val hso4: Int = headSafeOpaque[Int](x4)
+  val hso5: Int = headSafeOpaque[Int](x5)
+
+  // TODO
+  // def headSafeOpaquePrecise[T](v: { Vect.sized[T](Succ(þ[Nat])) }): { headSafe(v) } =
+  //   v.asInstanceOf[Cons[T]].head
+
+  // val hsop1: 1 = head[Int](x1) // error: not a subtype
+  val hsop2: 1 = head[Int](x2)
+  val hsop3: 1 = head[Int](x3) // TODO: inference fucks it up when we don't put the explicit [Int]
+  val hsop4: 1 = head[Int](x4)
+  val hsop5: 1 = head[Int](x5)
+
+  /** The last element of the vector */
+  dependent def last[T](v: Vect[T]): T = {
+    val h = v.asInstanceOf[Cons[T]].head
+    val t = v.asInstanceOf[Cons[T]].tail
+    if (t.isInstanceOf[Nil[T]])
+      h
+    else
+      last[T](t)
+  }
+
+  // val a1: 1 = last(x1) // error: stuck on failing asInstanceOf, as expected!
+  val a2: 1 = last[Int](x2)
+  val a3: 1 = last[Int](x3) // TODO: inference fucks it up when we don't put the explicit [Int]
+  val a4: 2 = last[Int](x4)
+  val a5: 3 = last[Int](x5)
+
+  // /** Extract a particular element from a vector */
+  // dependent def index(i: Nat, v: { sized(i) }): T
+  // index FZ     (x::xs) = x
+  // index (FS k) (x::xs) = index k xs
+
+}
+
+object IdrisVect2 {
+  def length(x: Int) = {
+    // At some point x became a shared tree in pickling
+    val y = x
+    identity(x)
+  }
+}
+
+object MatchError129 {
+  dependent def length[T](x: Unit): Unit = {
+    val y = x
+    length(y)
+  }
+}
diff --git a/tests/pos/from-tasty-wildcard.scala b/tests/pos/from-tasty-wildcard.scala
new file mode 100644
index 000000000000..e48358d9f900
--- /dev/null
+++ b/tests/pos/from-tasty-wildcard.scala
@@ -0,0 +1,7 @@
+object IdrisVect {
+  sealed trait Vect[T]
+  case class Cons[Q](head: Q, tail: Vect[Q]) extends Vect[Q]
+
+  def length[S](xs: Vect[S]): Unit =
+    length(xs.asInstanceOf[Cons[_]].tail)
+}
diff --git a/tests/pos/i3901.scala b/tests/pos/i3901.scala
new file mode 100644
index 000000000000..6d574cb6e60b
--- /dev/null
+++ b/tests/pos/i3901.scala
@@ -0,0 +1,4 @@
+object Crash {
+  def f(cond: => Boolean): cond.type = ???
+  f(true)
+}
diff --git a/tests/pos/tailcall/t6574.scala b/tests/pos/tailcall/t6574.scala
index d8377ddbc799..dcafbaa31a15 100644
--- a/tests/pos/tailcall/t6574.scala
+++ b/tests/pos/tailcall/t6574.scala
@@ -12,8 +12,8 @@ class Bad[X, Y](val v: Int) extends AnyVal {
     else {(); new Bad[X, Y](0)}.differentReceiver2
   }
 
-  @annotation.tailrec final def dependent[Z](a: Int)(b: String): b.type = {
-    this.dependent[Z](a)(b)
+  @annotation.tailrec final def dependentf[Z](a: Int)(b: String): b.type = {
+    this.dependentf[Z](a)(b)
   }
 }