Member type inference loses refinement type from RHS

[erikerlandson]

Compiler version

3.3.0

Minimized code

object reprodefs:
    abstract class Test[T]:
        type D // a dependent type

    abstract class Meta[V]:
        val value: V

    // declare some context-vars using transparent inline to 
    // expose dependent type 'D'
    transparent inline given given_TestInt: Test[Int] =
        new Test[Int] { type D = String }

    transparent inline given given_MetaTestInt: Meta[Test[Int]] =
        new Meta[Test[Int]]:
            val value = new Test[Int] { type D = String }

object repro:
    import scala.compiletime.*
    import reprodefs.{*, given}

    // this will work as expected
    // 'transparent inline' exposes dependent type 'D'
    val test = summonInline[Test[Int]]
    val t1 = summonInline[test.D =:= String]

    // adding one more type "layer" loses the type of 'D'
    val meta = summonInline[Meta[Test[Int]]]
    // the following summon will cause compile error:
    // "Cannot prove that repro.meta.value.D =:= String"
    val m1 = summonInline[meta.value.D =:= String]

Output

The val m1 = ... line is a compile error:

[error] -- [E172] Type Error: 
[error] 332 |    val m1 = summonInline[meta.value.D =:= String]
[error]     |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]     |Cannot prove that repro.meta.value.D =:= String.

Expectation

I would expect the compiler to correctly infer that dependent type meta.value.D has type String, due to everything being transparent inline (including summonInline).

[erikerlandson]

This is a slightly different variation on the reproducer above:

object reprodefs:
    abstract class Test[T]:
        type D // a dependent type

    case class Meta[V](value: V)

    // declare some context-vars using transparent inline to 
    // expose dependent type 'D'
    transparent inline given given_TestInt: Test[Int] =
        new Test[Int] { type D = String }

    // this will somehow "lose" the type of 'D'
    transparent inline given given_MetaTestInt: Meta[Test[Int]] =
        Meta(new Test[Int] { type D = String })

object repro:
    import scala.compiletime.*
    import reprodefs.{*, given}

    // this will work as expected
    // 'transparent inline' exposes dependent type 'D'
    val test = summonInline[Test[Int]]
    val t1 = summonInline[test.D =:= String]

    // using the meta layer works when it is not 'given'
    val meta1 = Meta(new Test[Int] { type D = String })
    val m1 = summonInline[meta1.value.D =:= String]

    // meta layer as a 'given' loses the type of 'D'
    val meta2 = summonInline[Meta[Test[Int]]]
    // the following summon will cause compile error:
    // "Cannot prove that value.D =:= String"
    val m2 = summonInline[meta2.value.D =:= String]

[nicolasstucki]

Workaround

transparent inline given given_MetaTestInt: Meta[Test[Int]] =
  new Meta[Test[Int]]:
-    val value = new Test[Int] { type D = String }
+    val value: Test[Int] { type D = String } = new Test[Int] { type D = String }

[nicolasstucki]

Minimized

abstract class Test[T]:
  type D

abstract class Meta[V]:
  val value: V

def test: Unit =
    val meta =
      new Meta[Test[Int]]:
        val value /*: Test[Int]*/ = new Test[Int] { type D = String }

    summon[meta.value.D =:= String]

[nicolasstucki]

This is a case where we infer the correct type, but it could be more precise.

[prolativ]

@erikerlandson your second snippet will work if you make Meta covariant:

case class Meta[+V](value: V)

Covariance also almost fixes the first snippet but in this case you also need to explicitly write the refinement while instantiating Meta:

object reprodefs:
    abstract class Test[T]:
        type D // a dependent type

    abstract class Meta[+V]:
        val value: V

    // declare some context-vars using transparent inline to 
    // expose dependent type 'D'
    transparent inline given given_TestInt: Test[Int] =
        new Test[Int] { type D = String }

    transparent inline given given_MetaTestInt: Meta[Test[Int]] =
      new Meta[Test[Int] { type D = String }]:
        val value = new Test[Int] { type D = String }

object repro:
    import scala.compiletime.*
    import reprodefs.{*, given}

    val test = summonInline[Test[Int]]
    val t1 = summonInline[test.D =:= String]

    val meta = summonInline[Meta[Test[Int]]]
    val m1 = summonInline[meta.value.D =:= String]

And indeed type inference could be improved here as @nicolasstucki said. For comparison the following snippet compiles in scala 2.13.11 but not in any release of scala 3 so far:

object repro {
  abstract class Test[T] {
      type D
  }

  abstract class Meta[V] {
      val value: V
  }

  val meta = new Meta[Test[Int]] {
    val value = new Test[Int] { type D = String }
  }

  val m1 = implicitly[meta.value.D =:= String]
}

[erikerlandson]

@nicolasstucki @prolativ thanks, both of those workarounds cause my dependent type to become visible!