diff --git a/src/dotty/tools/dotc/typer/Implicits.scala b/src/dotty/tools/dotc/typer/Implicits.scala
index a3ddca5d99db..f79288e74384 100644
--- a/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/src/dotty/tools/dotc/typer/Implicits.scala
@@ -421,6 +421,7 @@ trait Implicits { self: Typer =>
     assert(!ctx.isAfterTyper,
       if (argument.isEmpty) i"missing implicit parameter of type $pt after typer"
       else i"type error: ${argument.tpe} does not conform to $pt${err.whyNoMatchStr(argument.tpe, pt)}")
+    val prevConstr = ctx.typerState.constraint
     ctx.traceIndented(s"search implicit ${pt.show}, arg = ${argument.show}: ${argument.tpe.show}", implicits, show = true) {
       assert(!pt.isInstanceOf[ExprType])
       val isearch =
@@ -435,6 +436,7 @@ trait Implicits { self: Typer =>
           val deepPt = pt.deepenProto
           if (deepPt ne pt) inferImplicit(deepPt, argument, pos) else result
         case _ =>
+          assert(prevConstr eq ctx.typerState.constraint)
           result
       }
     }
@@ -450,7 +452,7 @@ trait Implicits { self: Typer =>
         // Not clear whether we need to drop the `.widen` here. All tests pass with it in place, though.
 
     assert(argument.isEmpty || argument.tpe.isValueType || argument.tpe.isInstanceOf[ExprType],
-        d"found: ${argument.tpe}, expected: $pt")
+        d"found: $argument: ${argument.tpe}, expected: $pt")
 
     /** The expected type for the searched implicit */
     lazy val fullProto = implicitProto(pt, identity)
@@ -472,9 +474,11 @@ trait Implicits { self: Typer =>
 
     /** Search a list of eligible implicit references */
     def searchImplicits(eligible: List[TermRef], contextual: Boolean): SearchResult = {
+      val constr = ctx.typerState.constraint
 
       /** Try to typecheck an implicit reference */
       def typedImplicit(ref: TermRef)(implicit ctx: Context): SearchResult = track("typedImplicit") { ctx.traceIndented(i"typed implicit $ref, pt = $pt, implicitsEnabled == ${ctx.mode is ImplicitsEnabled}", implicits, show = true) {
+        assert(constr eq ctx.typerState.constraint)
         var generated: Tree = tpd.ref(ref).withPos(pos)
         if (!argument.isEmpty)
           generated = typedUnadapted(
@@ -483,7 +487,7 @@ trait Implicits { self: Typer =>
         val generated1 = adapt(generated, pt)
         lazy val shadowing =
           typed(untpd.Ident(ref.name) withPos pos.toSynthetic, funProto)
-               (nestedContext.addMode(Mode.ImplicitShadowing).setNewTyperState)
+               (nestedContext.addMode(Mode.ImplicitShadowing).setExploreTyperState)
         def refMatches(shadowing: Tree): Boolean =
           ref.symbol == closureBody(shadowing).symbol || {
             shadowing match {
diff --git a/src/dotty/tools/dotc/typer/ProtoTypes.scala b/src/dotty/tools/dotc/typer/ProtoTypes.scala
index 9a012c30e0b0..13011cb85ba8 100644
--- a/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -341,7 +341,8 @@ object ProtoTypes {
 
   /** The normalized form of a type
    *   - unwraps polymorphic types, tracking their parameters in the current constraint
-   *   - skips implicit parameters
+   *   - skips implicit parameters; if result type depends on implicit parameter,
+   *     replace with Wildcard.
    *   - converts non-dependent method types to the corresponding function types
    *   - dereferences parameterless method types
    *   - dereferences nullary method types provided the corresponding function type
@@ -356,17 +357,22 @@ object ProtoTypes {
   def normalize(tp: Type, pt: Type)(implicit ctx: Context): Type = Stats.track("normalize") {
     tp.widenSingleton match {
       case poly: PolyType => normalize(constrained(poly).resultType, pt)
-      case mt: MethodType if !mt.isDependent /*&& !pt.isInstanceOf[ApplyingProto]*/ =>
-        if (mt.isImplicit) mt.resultType
-        else {
-          val rt = normalize(mt.resultType, pt)
-          if (pt.isInstanceOf[ApplyingProto])
-            mt.derivedMethodType(mt.paramNames, mt.paramTypes, rt)
+      case mt: MethodType =>
+        if (mt.isImplicit)
+          if (mt.isDependent)
+            mt.resultType.substParams(mt, mt.paramTypes.map(Function.const(WildcardType)))
+          else mt.resultType
+        else
+          if (mt.isDependent) tp
           else {
-            val ft = defn.FunctionType(mt.paramTypes, rt)
-            if (mt.paramTypes.nonEmpty || ft <:< pt) ft else rt
+            val rt = normalize(mt.resultType, pt)
+            if (pt.isInstanceOf[ApplyingProto])
+              mt.derivedMethodType(mt.paramNames, mt.paramTypes, rt)
+            else {
+              val ft = defn.FunctionType(mt.paramTypes, rt)
+              if (mt.paramTypes.nonEmpty || ft <:< pt) ft else rt
+            }
           }
-        }
       case et: ExprType => et.resultType
       case _ => tp
     }
diff --git a/src/dotty/tools/dotc/typer/Typer.scala b/src/dotty/tools/dotc/typer/Typer.scala
index 97bd0f514aee..479eedd380a4 100644
--- a/src/dotty/tools/dotc/typer/Typer.scala
+++ b/src/dotty/tools/dotc/typer/Typer.scala
@@ -1279,10 +1279,37 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
       }
     }
 
+    /** If `tp` is a TypeVar which is fully constrained (i.e. its upper bound `hi` conforms
+     *  to its lower bound `lo`), replace `tp` by `hi`. This is necessary to
+     *  keep the right constraints for some implicit search problems. The paradigmatic case
+     *  is `implicitNums.scala`. Without the healing done in `followAlias`, we cannot infer
+     *  implicitly[_3], where _2 is the typelevel number 3. The problem here is that if a
+     *  prototype is, say, Succ[Succ[Zero]], we can infer that it's argument type is Succ[Zero].
+     *  But if the prototype is N? >: Succ[Succ[Zero]] <: Succ[Succ[Zero]], the same
+     *  decomposition does not work - we'd get a N?#M where M is the element type name of Succ
+     *  instead.
+     */
+    def followAlias(tp: Type)(implicit ctx: Context): Type = {
+      val constraint = ctx.typerState.constraint
+      def inst(tp: Type): Type = tp match {
+        case TypeBounds(lo, hi)
+        if (lo eq hi) || (hi <:< lo)(ctx.fresh.setExploreTyperState) =>
+          inst(lo)
+        case tp: PolyParam =>
+          constraint.typeVarOfParam(tp).orElse(tp)
+        case _ => tp
+      }
+      tp match {
+        case tp: TypeVar if constraint.contains(tp) => inst(constraint.entry(tp.origin))
+        case _ => tp
+      }
+    }
+
     def adaptNoArgs(wtp: Type): Tree = wtp match {
       case wtp: ExprType =>
         adaptInterpolated(tree.withType(wtp.resultType), pt, original)
-      case wtp: ImplicitMethodType if constrainResult(wtp, pt) =>
+      case wtp: ImplicitMethodType if constrainResult(wtp, followAlias(pt)) =>
+        val constr = ctx.typerState.constraint
         def addImplicitArgs = {
           def implicitArgError(msg: => String): Tree = {
             ctx.error(msg, tree.pos.endPos)
@@ -1292,14 +1319,15 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
             def where = d"parameter $pname of $methodStr"
             inferImplicit(formal, EmptyTree, tree.pos.endPos) match {
               case SearchSuccess(arg, _, _) =>
-                adapt(arg, formal)
+                arg
               case ambi: AmbiguousImplicits =>
                 implicitArgError(s"ambiguous implicits: ${ambi.explanation} of $where")
               case failure: SearchFailure =>
                 implicitArgError(d"no implicit argument of type $formal found for $where" + failure.postscript)
             }
           }
-          adapt(tpd.Apply(tree, args), pt)
+          if (args.exists(_.isEmpty)) { assert(constr eq ctx.typerState.constraint); tree }
+          else adapt(tpd.Apply(tree, args), pt)
         }
         if ((pt eq WildcardType) || original.isEmpty) addImplicitArgs
         else
diff --git a/test/dotc/tests.scala b/test/dotc/tests.scala
index 1aa35e3ee66b..f96e77f0026f 100644
--- a/test/dotc/tests.scala
+++ b/test/dotc/tests.scala
@@ -121,7 +121,7 @@ class tests extends CompilerTest {
   @Test def neg_t1843_variances = compileFile(negDir, "t1843-variances", xerrors = 1)
   @Test def neg_t2660_ambi = compileFile(negDir, "t2660", xerrors = 2)
   @Test def neg_t2994 = compileFile(negDir, "t2994", xerrors = 2)
-  @Test def neg_subtyping = compileFile(negDir, "subtyping", xerrors = 4)
+  @Test def neg_subtyping = compileFile(negDir, "subtyping", xerrors = 5)
   @Test def neg_variances = compileFile(negDir, "variances", xerrors = 2)
   @Test def neg_badAuxConstr = compileFile(negDir, "badAuxConstr", xerrors = 2)
   @Test def neg_typetest = compileFile(negDir, "typetest", xerrors = 1)
diff --git a/tests/pending/pos/depmet_implicit_chaining_zw.scala b/tests/pos/depmet_implicit_chaining_zw.scala
similarity index 85%
rename from tests/pending/pos/depmet_implicit_chaining_zw.scala
rename to tests/pos/depmet_implicit_chaining_zw.scala
index a9da1e9764bd..f0e8a373b954 100644
--- a/tests/pending/pos/depmet_implicit_chaining_zw.scala
+++ b/tests/pos/depmet_implicit_chaining_zw.scala
@@ -22,7 +22,11 @@ object ZipWith {
   // thus, I present ?: implicitly on steroids!
   def ?[T <: AnyRef](implicit w: T): w.type = w
 
+  type _0 = Zero
+  type _1 = Succ[Zero]
   type _2 = Succ[Succ[Zero]]
-  val zw = ?[ZipWith[_2, Int => String => Boolean]].x // : Stream[Int] => Stream[String] => Stream[Boolean]
+  val zw = ?[ZipWith[_2, Int => String => Boolean]](
+    SuccZipWith[_1, Int, String => Boolean](
+      SuccZipWith[_0, String, Boolean])).x
   // val zw = implicitly[ZipWith[Succ[Succ[Zero]], Int => String => Boolean]{type T = Stream[Int] => Stream[String] => Stream[Boolean]}].x
 }
diff --git a/tests/pos/implicitNums.scala b/tests/pos/implicitNums.scala
new file mode 100644
index 000000000000..48c5302f7fb3
--- /dev/null
+++ b/tests/pos/implicitNums.scala
@@ -0,0 +1,15 @@
+object Test {
+
+  trait Number
+  trait Zero extends Number
+  trait Succ[N <: Number](n: N) extends Number
+
+  implicit def succ[N <: Number](implicit n: N): Succ[N] = new Succ[N](n) {}
+  implicit def zero: Zero = new Zero{}
+
+  implicitly[Zero]
+  implicitly[Succ[Zero]]
+  implicitly[Succ[Succ[Zero]]]
+  implicitly[Succ[Succ[Succ[Zero]]]]
+
+}