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

[DmytroMitin]

#8825 is resolved but if we rewrite code slightly the problem remains.

Minimized code

In Dotty 0.25.0-bin-20200504-11760ea-NIGHTLY 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 {
    given hnilLength as Length[HNil] {
      override type Out = Zero
    }
    given hconsLength[H, T <: HList](using length: Length[T]) as Length[HCons[H, T]] {
      override type Out = Succ[length.Out]
    } // (*)
//    given hconsLength[H, T <: HList, Out0 <: Nat](using length: Length[T] {type Out = Out0}) as Length[HCons[H, T]] {
//      override type Out = Succ[Out0]
//    } // (**)
  }

Output

summon[Length[HCons[Int, HNil]] { type Out = One}] doesn't compile

[error] -- Error: ...
[error] .. |  summon[Length[HCons[Int, HNil]] { type Out = One}]
[error]    |                                                    ^
[error]    |no implicit argument of type App.Length[App.HCons[Int, App.HNil]]{Out = App.One} was found for parameter x of method summon in object DottyPredef

Expectation

summon[Length[HCons[Int, HNil]] { type Out = One}] should compile.

If we replace line (*) with (**) then summon[Length[HCons[Int, HNil]] { type Out = One}] compiles.

If we resolve implicits manually, summon[Length[HCons[Int, HNil]] { type Out = One}](using Length.hconsLength[Int, HNil](using Length.hnilLength)) doesn't compile with (*) either

[error] -- [E007] Type Mismatch Error: ...
[error] .. |  summon[Length[HCons[Int, HNil]] { type Out = One}](using Length.hconsLength[Int, HNil](using Length.hnilLength))
[error]    |                                                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |       Found:    App.Length.hconsLength[Int, App.HNil]
[error]    |       Required: App.Length[App.HCons[Int, App.HNil]]{Out = App.One}

[prolativ]

Here's a workaround without an extra type parameter in hconsLength (for scala 3.0.0):

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 {
  given hnilLength: Length[HNil] with {
    override type Out = Zero
  }
  given hconsLength[H, T <: HList](using length: Length[T]): (Length[HCons[H, T]] { type Out = Succ[length.Out] }) = new Length[HCons[H, T]] {
    override type Out = Succ[length.Out]
  }
}

val l = summon[Length[HCons[Int, HNil]] { type Out = One }]

This looks like some limitation of given ... with syntax

[DmytroMitin]

Still reproducible in 3.3.0-RC3 https://scastie.scala-lang.org/DmytroMitin/3vDND7fzTnuU77hj9yhTfA/1

[prolativ]

Currently I don't really have time to actively work on fixing that but did some further investigations about the potential cause of the problem.
Here's a further minimization:

• This compiles

import scala.compiletime.ops.int.+

trait Length[T <: Tuple]:
  type Out <: Int

object Length:

  given lengthEmpty: Length[EmptyTuple] with
    override type Out = 0

  given lengthCons(using length: Length[EmptyTuple] { type Out = 0 }): Length[Int *: EmptyTuple] with
    override type Out = length.Out + 1

val a = summon[Length[Int *: EmptyTuple]]
val b = summon[a.Out =:= 1]
val c = summon[Length[Int *: EmptyTuple] {type Out = 1}]

• This doesn't compile

import scala.compiletime.ops.int.+

trait Length[T <: Tuple]:
  type Out <: Int

object Length:

  given lengthEmpty: Length[EmptyTuple] with
    override type Out = 0

  given lengthCons(using length: Length[EmptyTuple]): Length[Int *: EmptyTuple] with
    override type Out = length.Out + 1

val a = summon[Length[Int *: EmptyTuple]]
val b = summon[a.Out =:= 1]
val c = summon[Length[Int *: EmptyTuple] {type Out = 1}]

raising errors:

[error] Length.scala:15:28
[error] Cannot prove that a.Out =:= (1 : Int).
[error] val b = summon[a.Out =:= 1]
[error]                            ^
[error] Length.scala:16:57
[error] No given instance of type Length[Int *: EmptyTuple]{type Out = (1 : Int)} was found for parameter x of method summon in object Predef
[error] val c = summon[Length[Int *: EmptyTuple] {type Out = 1}]
[error]  

The difference in the snippets is in

(using length: Length[EmptyTuple] { type Out = 0 })

vs

(using length: Length[EmptyTuple])

After removing the invocations of summon and compiling the two variants with -Xprint:typer we get

package <empty> {
  import scala.compiletime.ops.int.+
  trait Length[T >: Nothing <: Tuple]() extends Object {
    T <: Tuple
    type Out >: Nothing <: Int
  }
  final lazy module val Length: Length = new Length()
  final module class Length() extends Object() { this: Length.type =>
    final lazy module given val lengthEmpty: Length.lengthEmpty =
      new Length.lengthEmpty()
    final module class lengthEmpty() extends Object(), Length[EmptyTuple] {
      this: Length.lengthEmpty.type =>
      override type Out = 0.type
    }
    given class lengthCons(using length: Length[EmptyTuple] { type Out = 0.type }) extends
      Object(), Length[*:[Int, EmptyTuple]] {
      protected given val length: Length[EmptyTuple] { type Out = (0 : Int) }
      override type Out =
        compiletime.ops.int.+[lengthCons.this.length.Out, 1.type]
    }
    final given def lengthCons(using length: Length[EmptyTuple] { type Out = 0.type }):
      Length.lengthCons = new Length.lengthCons(using length)()
    }
}

and

package <empty> {
  import scala.compiletime.ops.int.+
  trait Length[T >: Nothing <: Tuple]() extends Object {
    T <: Tuple
    type Out >: Nothing <: Int
  }
  final lazy module val Length: Length = new Length()
  final module class Length() extends Object() { this: Length.type =>
    final lazy module given val lengthEmpty: Length.lengthEmpty =
      new Length.lengthEmpty()
    final module class lengthEmpty() extends Object(), Length[EmptyTuple] {
      this: Length.lengthEmpty.type =>
      override type Out = 0.type
    }
    given class lengthCons(using length: Length[EmptyTuple]) extends
      Object(), Length[*:[Int, EmptyTuple]] {
      protected given val length: Length[EmptyTuple]
      override type Out =
        compiletime.ops.int.+[lengthCons.this.length.Out, 1.type]
    }
    final given def lengthCons(using length: Length[EmptyTuple]):
      Length.lengthCons = new Length.lengthCons(using length)()
  }
}

respectively.

Here we can see that the { type Out = 0.type } or { type Out = (0 : Int) } type refinement is lost and that the computation of Out in class lengthCons refers to lengthCons.this.length (class member) rather than to length (constructor parameter). The type of lengthCons.this.length in the second variant is just Length[EmptyTuple] without the { type Out = (0 : Int) } refinement so the compiler can't know that Out in lengthCons should eventually be 1.

As I mentioned in my previous comment the problem seems to be related to how given T with { ... } syntax works on the contrary to given T { ... } = .... In the latter case there's no auxiliary class generated during the desugaring. Because of that the compiler relies on the singleton type of a parameter of a given (corresponding to an implicit def in scala 2 world), which doesn't lose its type refinement, making all the type information propagate correctly.