diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index c389742a62e9..103a6275a2a6 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -615,14 +615,20 @@ class Definitions {
   lazy val QuotedExprType = ctx.requiredClassRef("scala.quoted.Expr")
   def QuotedExprClass(implicit ctx: Context) = QuotedExprType.symbol.asClass
 
-    def QuotedExpr_~(implicit ctx: Context) = QuotedExprClass.requiredMethod(nme.UNARY_~)
-    def QuotedExpr_run(implicit ctx: Context) = QuotedExprClass.requiredMethod(nme.run)
+    lazy val QuotedExpr_spliceR = QuotedExprClass.requiredMethod(nme.UNARY_~)
+    def QuotedExpr_~(implicit ctx: Context) = QuotedExpr_spliceR.symbol
+    lazy val QuotedExpr_runR = QuotedExprClass.requiredMethodRef(nme.run)
+    def QuotedExpr_run(implicit ctx: Context) = QuotedExpr_runR.symbol
 
   lazy val QuotedTypeType = ctx.requiredClassRef("scala.quoted.Type")
   def QuotedTypeClass(implicit ctx: Context) = QuotedTypeType.symbol.asClass
 
-    def QuotedType_~(implicit ctx: Context) =
-      QuotedTypeClass.info.member(tpnme.UNARY_~).symbol.asType
+    lazy val QuotedType_spliceR = QuotedTypeClass.requiredType(tpnme.UNARY_~).typeRef
+    def QuotedType_~ = QuotedType_spliceR.symbol
+
+  lazy val QuotedTypeModule = QuotedTypeClass.companionModule
+    lazy val QuotedType_applyR = QuotedTypeModule.requiredMethodRef(nme.apply)
+    def QuotedType_apply(implicit ctx: Context) = QuotedType_applyR.symbol
 
   def Unpickler_unpickleExpr = ctx.requiredMethod("scala.runtime.quoted.Unpickler.unpickleExpr")
   def Unpickler_unpickleType = ctx.requiredMethod("scala.runtime.quoted.Unpickler.unpickleType")
diff --git a/compiler/src/dotty/tools/dotc/core/Denotations.scala b/compiler/src/dotty/tools/dotc/core/Denotations.scala
index 4614f5e325ca..70517a5ec7ad 100644
--- a/compiler/src/dotty/tools/dotc/core/Denotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/Denotations.scala
@@ -313,6 +313,9 @@ object Denotations {
     def requiredClass(name: PreName)(implicit ctx: Context): ClassSymbol =
       info.member(name.toTypeName).requiredSymbol(_.isClass).asClass
 
+    def requiredType(name: PreName)(implicit ctx: Context): TypeSymbol =
+      info.member(name.toTypeName).requiredSymbol(_.isType).asType
+
     /** The alternative of this denotation that has a type matching `targetType` when seen
      *  as a member of type `site`, `NoDenotation` if none exists.
      */
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala b/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
index d0b5f03dc7b6..ded5386b2446 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
@@ -102,7 +102,7 @@ Standard-Section: "ASTs" TopLevelStat*
                   REFINEDtpt     Length underlying_Term refinement_Stat*
                   APPLIEDtpt     Length tycon_Term arg_Term*
                   POLYtpt        Length TypeParam* body_Term
-                  TYPEBOUNDStpt  Length low_Term high_Term
+                  TYPEBOUNDStpt  Length low_Term high_Term?
                   ANNOTATEDtpt   Length underlying_Term fullAnnotation_Term
                   ANDtpt         Length left_Term right_Term
                   ORtpt          Length left_Term right_Term
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index da299fc61bf3..374d3fd4ddfb 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -552,7 +552,10 @@ class TreePickler(pickler: TastyPickler) {
           withLength { pickleParams(tparams); pickleTree(body) }
         case TypeBoundsTree(lo, hi) =>
           writeByte(TYPEBOUNDStpt)
-          withLength { pickleTree(lo); pickleTree(hi) }
+          withLength {
+            pickleTree(lo);
+            if (hi ne lo) pickleTree(hi)
+          }
         case Hole(idx, args) =>
           writeByte(HOLE)
           withLength {
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index 38ffe3963f05..f892837288b7 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -1038,7 +1038,9 @@ class TreeUnpickler(reader: TastyReader,
               val body = readTpt()
               LambdaTypeTree(tparams, body)
             case TYPEBOUNDStpt =>
-              TypeBoundsTree(readTpt(), readTpt())
+              val lo = readTpt()
+              val hi = if (currentAddr == end) lo else readTpt()
+              TypeBoundsTree(lo, hi)
             case HOLE =>
               readHole(end)
             case _ =>
diff --git a/compiler/src/dotty/tools/dotc/transform/ReifyQuotes.scala b/compiler/src/dotty/tools/dotc/transform/ReifyQuotes.scala
index 8b02aa8e63fb..9c496d4ddfec 100644
--- a/compiler/src/dotty/tools/dotc/transform/ReifyQuotes.scala
+++ b/compiler/src/dotty/tools/dotc/transform/ReifyQuotes.scala
@@ -13,6 +13,7 @@ import tasty.TreePickler.Hole
 import MegaPhase.MiniPhase
 import SymUtils._
 import NameKinds.OuterSelectName
+import typer.Implicits.SearchFailureType
 
 import scala.collection.mutable
 import dotty.tools.dotc.core.StdNames._
@@ -22,7 +23,7 @@ import dotty.tools.dotc.core.quoted._
 /** Translates quoted terms and types to `unpickle` method calls.
  *  Checks that the phase consistency principle (PCP) holds.
  */
-class ReifyQuotes extends MacroTransform {
+class ReifyQuotes extends MacroTransformWithImplicits {
   import ast.tpd._
 
   override def phaseName: String = "reifyQuotes"
@@ -101,7 +102,7 @@ class ReifyQuotes extends MacroTransform {
    *  @param  level      the current level, where quotes add one and splices subtract one level
    *  @param  levels     a stacked map from symbols to the levels in which they were defined
    */
-  private class Reifier(inQuote: Boolean, val outer: Reifier, val level: Int, levels: LevelInfo) extends Transformer {
+  private class Reifier(inQuote: Boolean, val outer: Reifier, val level: Int, levels: LevelInfo) extends ImplicitsTransformer {
     import levels._
 
     /** A nested reifier for a quote (if `isQuote = true`) or a splice (if not) */
@@ -114,12 +115,12 @@ class ReifyQuotes extends MacroTransform {
     /** A list of embedded quotes (if `inSplice = true`) or splices (if `inQuote = true`) */
     val embedded = new mutable.ListBuffer[Tree]
 
-    /** A map from type ref T to "expression of type `quoted.Type[T]`".
+    /** A map from type ref T to expressions of type `quoted.Type[T]`".
      *  These will be turned into splices using `addTags`
      */
-    val importedTypes = new mutable.LinkedHashSet[TypeRef]()
+    val importedTags = new mutable.LinkedHashMap[TypeRef, Tree]()
 
-    /** Assuming typeTagOfRef = `Type1 -> tag1, ..., TypeN -> tagN`, the expression
+    /** Assuming importedTags = `Type1 -> tag1, ..., TypeN -> tagN`, the expression
      *
      *      { type <Type1> = <tag1>.unary_~
      *        ...
@@ -127,16 +128,15 @@ class ReifyQuotes extends MacroTransform {
      *        <expr>
      *      }
      *
-     *  where all references to `TypeI` in `expr` are rewired to point to the locally
+     *  references to `TypeI` in `expr` are rewired to point to the locally
      *  defined versions. As a side effect, prepend the expressions `tag1, ..., `tagN`
-     *  as splices to `buf`.
+     *  as splices to `embedded`.
      */
     def addTags(expr: Tree)(implicit ctx: Context): Tree =
-      if (importedTypes.isEmpty) expr
+      if (importedTags.isEmpty) expr
       else {
-        val trefs = importedTypes.toList
-        val typeDefs = for (tref <- trefs) yield {
-          val tag = New(defn.QuotedTypeType.appliedTo(tref), Nil) // FIXME: should be an implicitly inferred defn.QuotedTypeType.appliedTo(tref)
+        val itags = importedTags.toList
+        val typeDefs = for ((tref, tag) <- itags) yield {
           val rhs = transform(tag.select(tpnme.UNARY_~))
           val alias = ctx.typeAssigner.assignType(untpd.TypeBoundsTree(rhs, rhs), rhs, rhs)
           val original = tref.symbol.asType
@@ -146,9 +146,9 @@ class ReifyQuotes extends MacroTransform {
             info = TypeAlias(tag.tpe.select(tpnme.UNARY_~)))
           ctx.typeAssigner.assignType(untpd.TypeDef(original.name, alias), local)
         }
-        importedTypes.clear()
+        importedTags.clear()
         Block(typeDefs,
-          new SubstMap(substFrom = trefs.map(_.symbol), substTo = typeDefs.map(_.symbol))
+          new SubstMap(substFrom = itags.map(_._1.symbol), substTo = typeDefs.map(_.symbol))
             .apply(expr))
       }
 
@@ -180,6 +180,29 @@ class ReifyQuotes extends MacroTransform {
     def spliceOutsideQuotes(pos: Position)(implicit ctx: Context) =
       ctx.error(i"splice outside quotes", pos)
 
+    /** Try to heal phase-inconsistent reference to type `T` using a local type definition.
+     *  @return None      if successful
+     *  @return Some(msg) if unsuccessful where `msg` is a potentially empty error message
+     *                    to be added to the "inconsistent phase" message.
+     */
+    def tryHeal(tp: Type, pos: Position)(implicit ctx: Context): Option[String] = tp match {
+      case tp: TypeRef =>
+        val reqType = defn.QuotedTypeType.appliedTo(tp)
+        val tag = ctx.typer.inferImplicitArg(reqType, pos)
+        tag.tpe match {
+          case fail: SearchFailureType =>
+            Some(i"""
+                    |
+                    | The access would be accepted with the right type tag, but
+                    | ${ctx.typer.missingArgMsg(tag, reqType, "")}""")
+          case _ =>
+            importedTags(tp) = nested(isQuote = false).transform(tag)
+            None
+        }
+      case _ =>
+        Some("")
+    }
+
     /** Check reference to `sym` for phase consistency, where `tp` is the underlying type
      *  by which we refer to `sym`.
      */
@@ -192,14 +215,10 @@ class ReifyQuotes extends MacroTransform {
       if (!isThis && sym.maybeOwner.isType)
         check(sym.owner, sym.owner.thisType, pos)
       else if (sym.exists && !sym.isStaticOwner && !levelOK(sym))
-        tp match {
-          case tp: TypeRef =>
-            importedTypes += tp
-          case _ =>
-            ctx.error(em"""access to $symStr from wrong staging level:
-                          | - the definition is at level ${levelOf(sym)},
-                          | - but the access is at level $level.""", pos)
-        }
+        for (errMsg <- tryHeal(tp, pos))
+          ctx.error(em"""access to $symStr from wrong staging level:
+                        | - the definition is at level ${levelOf(sym)},
+                        | - but the access is at level $level.$errMsg""", pos)
     }
 
     /** Check all named types and this-types in a given type for phase consistency. */
@@ -209,7 +228,7 @@ class ReifyQuotes extends MacroTransform {
           case tp: NamedType if tp.symbol.isSplice =>
             if (inQuote) outer.checkType(pos).foldOver(acc, tp)
             else {
-              spliceOutsideQuotes(pos)
+              if (tp.isTerm) spliceOutsideQuotes(pos)
               tp
             }
           case tp: NamedType =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Implicits.scala b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
index c49331f43883..f167f2a45ff0 100644
--- a/compiler/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
@@ -553,34 +553,54 @@ trait Implicits { self: Typer =>
   }
 
   /** Find an implicit argument for parameter `formal`.
-   *  @param error  An error handler that gets an error message parameter
-   *                which is itself parameterized by another string,
-   *                indicating where the implicit parameter is needed
+   *  Return a failure as a SearchFailureType in the type of the returned tree.
    */
   def inferImplicitArg(formal: Type, pos: Position)(implicit ctx: Context): Tree = {
 
     /** If `formal` is of the form ClassTag[T], where `T` is a class type,
      *  synthesize a class tag for `T`.
    	 */
-    def synthesizedClassTag(formal: Type)(implicit ctx: Context): Tree =
-      formal.argInfos match {
-        case arg :: Nil =>
-          fullyDefinedType(arg, "ClassTag argument", pos) match {
-            case defn.ArrayOf(elemTp) =>
-              val etag = inferImplicitArg(defn.ClassTagType.appliedTo(elemTp), pos)
-              if (etag.tpe.isError) EmptyTree else etag.select(nme.wrap)
-            case tp if hasStableErasure(tp) && !defn.isBottomClass(tp.typeSymbol) =>
-              ref(defn.ClassTagModule)
-                .select(nme.apply)
-                .appliedToType(tp)
-                .appliedTo(clsOf(erasure(tp)))
-                .withPos(pos)
-            case tp =>
-              EmptyTree
+    def synthesizedClassTag(formal: Type): Tree = formal.argInfos match {
+      case arg :: Nil =>
+        fullyDefinedType(arg, "ClassTag argument", pos) match {
+          case defn.ArrayOf(elemTp) =>
+            val etag = inferImplicitArg(defn.ClassTagType.appliedTo(elemTp), pos)
+            if (etag.tpe.isError) EmptyTree else etag.select(nme.wrap)
+          case tp if hasStableErasure(tp) && !defn.isBottomClass(tp.typeSymbol) =>
+            ref(defn.ClassTagModule)
+              .select(nme.apply)
+              .appliedToType(tp)
+              .appliedTo(clsOf(erasure(tp)))
+              .withPos(pos)
+          case tp =>
+            EmptyTree
+        }
+      case _ =>
+        EmptyTree
+    }
+
+    def synthesizedTypeTag(formal: Type): Tree = formal.argInfos match {
+      case arg :: Nil =>
+        object bindFreeVars extends TypeMap {
+          var ok = true
+          def apply(t: Type) = t match {
+            case t @ TypeRef(NoPrefix, _) =>
+              inferImplicit(defn.QuotedTypeType.appliedTo(t), EmptyTree, pos) match {
+                case SearchSuccess(tag, _, _) if tag.tpe.isStable =>
+                  tag.tpe.select(defn.QuotedType_~)
+                case _ =>
+                  ok = false
+                  t
+              }
+            case _ => t
           }
-        case _ =>
-          EmptyTree
-      }
+        }
+        val tag = bindFreeVars(arg)
+        if (bindFreeVars.ok) ref(defn.typeQuoteMethod).appliedToType(tag)
+        else EmptyTree
+      case _ =>
+        EmptyTree
+    }
 
     /** If `formal` is of the form Eq[T, U], where no `Eq` instance exists for
      *  either `T` or `U`, synthesize `Eq.eqAny[T, U]` as solution.
@@ -644,6 +664,8 @@ trait Implicits { self: Typer =>
           tree
         else if (formalValue.isRef(defn.ClassTagClass))
           synthesizedClassTag(formalValue).orElse(tree)
+        else if (formalValue.isRef(defn.QuotedTypeClass))
+          synthesizedTypeTag(formalValue).orElse(tree)
         else if (formalValue.isRef(defn.EqClass))
           synthesizedEq(formalValue).orElse(tree)
         else
diff --git a/docs/docs/reference/symmetric-meta-programming.md b/docs/docs/reference/principled-meta-programming.md
similarity index 90%
rename from docs/docs/reference/symmetric-meta-programming.md
rename to docs/docs/reference/principled-meta-programming.md
index 95141f1a0ce1..1adc3f8ce89d 100644
--- a/docs/docs/reference/symmetric-meta-programming.md
+++ b/docs/docs/reference/principled-meta-programming.md
@@ -1,11 +1,11 @@
 ---
 layout: doc-page
-title: "Symmetric Meta Programming"
+title: "Principled Meta Programming"
 ---
 
-# Symmetric Meta Programming
+# Principled Meta Programming
 
-Symmetric meta programming is a new framework for staging and for some
+Principled meta programming is a new framework for staging and for some
 forms of macros. It is expressed as strongly and statically typed
 code using two fundamental operations: quotations and splicing. A
 novel aspect of the approach is that these two operations are
@@ -16,7 +16,7 @@ splices in exactly the same way.
 
 ### Quotes and Splices
 
-Symmetric meta programming is built on two well-known fundamental
+Principled meta programming is built on two well-known fundamental
 operations: quotation and splicing.  Quotation is expressed as
 `'(...)` or `'{...}` for expressions (both forms are equivalent) and
 as `'[...]` for types. Splicing is expressed as a prefix `~` operator.
@@ -72,13 +72,18 @@ The two types can be defined in package `scala.quoted` as follows:
 
     package scala.quoted
 
-    abstract class Expr[T] {
+    sealed abstract class Expr[T] {
       def unary_~: T   // splice operation
     }
-    class Type[T] {
+    sealed abstract class Type[T] {
       type unary_~ = T  // splice type
     }
 
+Both `Expr` and `Type` are abstract and sealed, so all constructors for
+these types are provided by the system. One way to construct values of
+these types is by quoting, the other is by type-specific lifting
+operations that will be discussed later on.
+
 ### The Phase Consistency Principle
 
 A fundamental *phase consistency principle* (PCP) regulates accesses
@@ -108,13 +113,13 @@ create nor remove quotes or splices individually. So the PCP ensures
 that program elaboration will lead to neither of the two unwanted
 situations described above.
 
-In what concerns the range of features it covers, symmetric meta programming is
+In what concerns the range of features it covers, principled meta programming is
 quite close to the MetaML family of languages. One difference is that MetaML does
 not have an equivalent of the PCP - quoted code in MetaML _can_ access
 variables in its immediately enclosing environment, with some
 restrictions and caveats since such accesses involve serialization.
 However, this does not constitute a fundamental gain in
-expressiveness. Symmetric meta programming allows to define a `Liftable`
+expressiveness. Principled meta programming allows to define a `Liftable`
 type-class which can implement such accesses within the confines of the
 PCP. This is explained further in a later section.
 
@@ -163,14 +168,57 @@ quote but no splice between the parameter binding of `T` and its
 usage. But the code can be made phase correct by adding a binding
 of a `Type[T]` tag:
 
-    def reflect[T, U](f: Expr[T] => Expr[U]): Expr[T => U] = {
-      val Ttag = new Type[T]
-      ’{ (x: ~Ttag) => ~f(’(x))
-    }
+    def reflect[T, U](f: Expr[T] => Expr[U])(implicit t: Type[T]): Expr[T => U] =
+      ’{ (x: ~t) => ~f(’(x)) }
+
+In this version of `reflect`, the type of `x` is now the result of
+splicing the `Type` value `t`. This operation _is_ splice correct -- there
+is one quote and one splice between the use of `t` and its definition.
+
+To avoid clutter, the Scala implementation tries to convert any phase-incorrect
+reference to a type `T` to a type-splice, by rewriting `T` to `~implicitly[Type[T]]`.
+For instance, the user-level definition of `reflect`:
+
+    def reflect[T: Type, U](f: Expr[T] => Expr[U]) Expr[T => U] =
+      ’{ (x: T) => ~f(’(x)) }
+
+would be rewritten to
+
+    def reflect[T: Type, U](f: Expr[T] => Expr[U]) Expr[T => U] =
+      ’{ (x: ~implicitly[Type[T]]) => ~f(’(x)) }
+
+The `implicitly` query succeeds because there is an implicit value of
+type `Type[T]` available (namely the evidence parameter corresponding
+to the context bound `: Type`), and the reference to that value is
+phase-correct. If that was not the case, the phase inconsistency for
+`T` would be reported as an error.
+
+### Lifting Types
+
+The previous section has shown that the metaprogramming framework has
+to be able to take a type `T` and convert it to a type tree of type
+`Type[T]` that can be reified. This means that all free variables of
+the type tree refer to types and values defined in the current stage.
+
+For a reference to a global class, this is easy: Just issue the fully
+qualified name of the class. Members of reifiable types are handled by
+just reifying the containing type together with the member name. But
+what to do for references to type parameters or local type definitions
+that are not defined in the current stage? Here, we cannot construct
+the `Type[T]` tree directly, so we need to get it from a recursive
+implicit search. For instance, to implemenent
+
+    implicitly[Type[List[T]]]
+
+where `T` is not defined in the current stage, we construct the type constructor
+of `List` applied to the splice of the result of searching for an implicit `Type[T]`:
+
+    '[List[~implicitly[Type[T]]]]
 
-To avoid clutter, the Scala implementation will add these tags
-automatically in the case of a PCP violation involving types. As a consequence,
-types can be effectively ignored for phase consistency checking.
+This is in exactly the algorithm that Scala 2 uses to search for type tags.
+In fact Scala 2's type tag feature can be understood as a more ad-hoc version of
+`quoted.Type`. As was the case for type tags, the implicit search for a `quoted.Type`
+is handled by the compiler, using the algorithm sketched above.
 
 ### Example Expansion
 
@@ -259,7 +307,7 @@ Here’s an application of `map` and how it rewrites to optimized code:
 
 ### Relationship with Inline and Macros
 
-Seen by itself, symmetric meta-programming looks more like a
+Seen by itself, principled meta-programming looks more like a
 framework for staging than one for compile-time meta programming with
 macros. But combined with Dotty’s `inline` it can be turned into a
 compile-time system.  The idea is that macro elaboration can be
@@ -529,7 +577,9 @@ a `List` is liftable if its element type is:
 
 In the end, `Liftable` resembles very much a serialization
 framework. Like the latter it can be derived systematically for all
-collections, case classes and enums.
+collections, case classes and enums. Note also that the implicit synthesis
+of "type-tag" values of type `Type[T]` is essentially the type-level
+analogue of lifting.
 
 Using lifting, we can now give the missing definition of `showExpr` in the introductory example:
 
diff --git a/docs/docs/reference/simple-smp.md b/docs/docs/reference/simple-smp.md
index 733810d4cd19..bc7b4b68c617 100644
--- a/docs/docs/reference/simple-smp.md
+++ b/docs/docs/reference/simple-smp.md
@@ -8,7 +8,7 @@ title: "The Meta-theory of Symmetric Meta-programming"
 23.12.2017
 
 This note presents a simplified variant of
-[symmetric meta-programming](./symmetric-meta-programming.md)
+[principled meta-programming](./principled-meta-programming.md)
 and sketches its soundness proof. The variant treats only dialogues
 between two stages. A program can have quotes which can contain
 splices (which can contain quotes, which can contain splices, and so
diff --git a/docs/sidebar.yml b/docs/sidebar.yml
index baca398e3e89..caa4d3c5b921 100644
--- a/docs/sidebar.yml
+++ b/docs/sidebar.yml
@@ -47,8 +47,8 @@ sidebar:
               url: docs/reference/trait-parameters.html
             - title: Inline
               url: docs/reference/inline.html
-            - title: Symmetric Meta Programming
-              url: docs/reference/symmetric-meta-programming.html
+            - title: Meta Programming
+              url: docs/reference/principled-meta-programming.html
             - title: By-Name Implicits
               url: docs/reference/implicit-by-name-parameters.html
             - title: Auto Parameter Tupling
diff --git a/tests/neg/quote-0.scala b/tests/neg/quote-0.scala
index 37e2fe02c141..6ee4c560c1a4 100644
--- a/tests/neg/quote-0.scala
+++ b/tests/neg/quote-0.scala
@@ -15,7 +15,11 @@ class Test {
   '((y: Expr[Int]) => ~y )  // error: wrong staging level
 
   def f[T](t: Type[T], x: Expr[T]) = '{
-    val z2 = ~x   // OK
+    val z2 = ~x   // error: wrong staging level
+  }
+
+  def g[T](implicit t: Type[T], x: Expr[T]) = '{
+    val z2 = ~x   // ok
   }
 
 }
diff --git a/tests/pos/quote-1.scala b/tests/pos/quote-1.scala
index 8d2a3ee243a8..669a0037b6bf 100644
--- a/tests/pos/quote-1.scala
+++ b/tests/pos/quote-1.scala
@@ -2,7 +2,7 @@ import scala.quoted._
 
 object Test {
 
-  def f[T](x: Expr[T])(t: Type[T]) = '{
+  def f[T](x: Expr[T])(implicit t: Type[T]) = '{
     val y: t.unary_~ = x.unary_~
     val z = ~x
   }
@@ -13,3 +13,4 @@ object Test {
   def g(es: Expr[String], t: Type[String]) =
     f('{ (~es + "!") :: Nil })('[List[~t]])
 }
+
diff --git a/tests/pos/quote-liftable.scala b/tests/pos/quote-liftable.scala
index d3dd2ff57bf5..0388a1da6432 100644
--- a/tests/pos/quote-liftable.scala
+++ b/tests/pos/quote-liftable.scala
@@ -17,7 +17,7 @@ object Test {
       if (b) '(true) else '(false)
   }
 
-  implicit def ListIsLiftable[T: Liftable]: Liftable[List[T]] = new {
+  implicit def ListIsLiftable[T: Liftable: Type]: Liftable[List[T]] = new {
     def toExpr(xs: List[T]): Expr[List[T]] = xs match {
       case x :: xs1 => '{ ~implicitly[Liftable[T]].toExpr(x) :: ~toExpr(xs1) }
       case Nil => '(Nil: List[T])
diff --git a/tests/pos/typetags.scala b/tests/pos/typetags.scala
new file mode 100644
index 000000000000..509ccb6087d0
--- /dev/null
+++ b/tests/pos/typetags.scala
@@ -0,0 +1,11 @@
+import scala.quoted._
+
+object Test {
+
+  def f[T: Type] = {
+    implicitly[Type[Int]]
+    implicitly[Type[List[Int]]]
+    implicitly[Type[T]]
+    implicitly[Type[List[T]]]
+  }
+}
diff --git a/tests/run-with-compiler/i3823-c.check b/tests/run-with-compiler/i3823-c.check
index ff7845fd9de5..7f63de0f0622 100644
--- a/tests/run-with-compiler/i3823-c.check
+++ b/tests/run-with-compiler/i3823-c.check
@@ -1,4 +1,7 @@
 {
-  val z: Int = 2
-  ()
+  type T = Int
+  {
+    val z: T = 2
+    ()
+  }
 }
diff --git a/tests/run-with-compiler/i3823-c.scala b/tests/run-with-compiler/i3823-c.scala
index 0c288b091b9f..a6162b49439b 100644
--- a/tests/run-with-compiler/i3823-c.scala
+++ b/tests/run-with-compiler/i3823-c.scala
@@ -5,8 +5,7 @@ object Test {
     def f[T](x: Expr[T])(implicit t: Type[T]) = '{
       val z = ~x
     }
-    // FIXME uncomment next line
-    // println(f('(2))(Type.IntTag).show)
-    println("{\n  val z: Int = 2\n  ()\n}") // TODO remove line
+    println(f('(2))(Type.IntTag).show)
   }
-}
\ No newline at end of file
+}
+