Can't find implicit of refined type when path-dependent type is used

[DmytroMitin]

Minimized code

In Dotty 0.23.0-RC1 with

  sealed trait Nat
  case class Succ[N <: Nat](n: N) extends Nat
  case object Zero extends Nat
  type Zero = Zero.type
  type One = Succ[Zero]

  sealed trait HList
  case class HCons[+H, +T <: HList](head: H, tail: T) extends HList
  case object HNil extends HList
  type HNil = HNil.type
  
  trait Length[L <: HList] {
    type Out <: Nat
  }
  object Length {
    type Aux[L <: HList, Out0 <: Nat] = Length[L] { type Out = Out0 }
    def instance[L <: HList, Out0 <: Nat]: Aux[L, Out0] = new Length[L] { type Out = Out0 }
    
    given hnilLength as Aux[HNil, Zero] = instance
    given hconsLength[H, T <: HList] (using length: Length[T]) as Aux[HCons[H, T], Succ[length.Out]] = instance // (*)
//    given hconsLength[H, T <: HList, N <: Nat] (using length: Aux[T, N]) as Aux[HCons[H, T], Succ[N]] = instance // (**)
  }

Output

summon[Length.Aux[HCons[Int, HNil], One]] doesn't compile

Error: no implicit argument of type App.Length.Aux[App.HCons[Int, App.HNil], App.One] was found for parameter x of method summon in object DottyPredef.
I found:
    App.Length.hconsLength[H, T]
But method hconsLength in object Length does not match type App.Length.Aux[App.HCons[Int, App.HNil], App.One].
    summon[Length.Aux[HCons[Int, HNil], One]]

Expectation

summon[Length.Aux[HCons[Int, HNil], One]] should compile.

If we replace line (*) with (**) then summon[Length.Aux[HCons[Int, HNil], One]] compiles.

Also if we resolve implicits manually, summon[Length.Aux[HCons[Int, HNil], One]](using Length.hconsLength(using Length.hnilLength)) compiles.

[odersky]

This happens to be fixed by #8824 .