Chain of two given...with fail to fetch dependent type

[soronpo]

Chain of two given..with dependencies fail to fetch dependent type. If IntCandidate in the example below uses transparent inline given then there is no error.

Compiler version

v3.1.0-RC2

Minimized code

scastie:
https://scastie.scala-lang.org/k7wmGYQOQtCteA4IrDmJ7g

trait IntWidth {type Out}
given IntWidth with {type Out = 155}

trait IntCandidate {type Out}
given (using w: IntWidth): IntCandidate with {type Out = w.Out}

val x = summon[IntCandidate]
val xx = summon[x.Out =:= 155]

Output

Cannot prove that x.Out =:= (155 : Int).

Expectation

No error.

[esse-byte]

Note: the Aux pattern works here scastie: aux pattern

[soronpo]

@odersky I can try to take this on myself. Any hint were I should start looking?

[odersky]

I'd first try to pass explicit arguments to the summon to find out exactly what given does not get inferred.

[soronpo]

For the following code:

trait IntWidth {type Out}
trait IntCandidate {type Out}
given g(using w: IntWidth): IntCandidate with {type Out = w.Out}

val x : IntCandidate{type Out = 155} = g(using new IntWidth {type Out = 155})

It fails with:

[error] 5 |val x : IntCandidate{type Out = 155} = g(using new IntWidth {type Out = 155})
[error]   |                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]   |                                 Found:    g
[error]   |                                 Required: IntCandidate{Out = (155 : Int)}

[odersky]

That's a useful observation. I played some more with it:

trait IntWidth {type Out}
trait IntCandidate {type Out}

// This works:

def g1(w: IntWidth) = new IntCandidate {type Out = w.Out}
val x1 : IntCandidate{type Out = 155} = g1(new IntWidth {type Out = 155})

// This is generated from the given definitions:

class G(val w: IntWidth) extends Object(), IntCandidate {
  type Out = w.Out
}

val x2 : IntCandidate{type Out = 155} = g2(new IntWidth {type Out = 155})
  // |                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  // |                               Found:    G
  // |                               Required: IntCandidate{Out = (155 : Int)}

def g2(w: IntWidth): G = new G(w)

// Trying to refine the output type of `g3`:

def g3(w1: IntWidth): G {type Out = w1.Out} = new G(w1)
  // error: Found: G
  //        Required: G{Out = w1.Out²}


val x3 : IntCandidate{type Out = 155} = g3(new IntWidth {type Out = 155})

So, what this is is the "old" problem that Scala loses dependencies across class construction. We type

new G(w1): G

where it could also be

new G(w1): G { val w: w1.type }

If we chose the latter typing, the problem would be solved, or be close to it.

Doing this is one of the cornerstones of making Scala more dependent. So it's not a simple "fix" but a rather fundamental generalization, with associated risks. /cc @mbovel who also wants to work on this.

[soronpo]

And here I thought it could be a simple fix... 😢
@odersky since it works if we change given X with {} to transparent inline given X = new X {}, what do you think about the underlying given with mechanism relying on the transparent inline mechanism?

[odersky]

That sounds scary. I think it should remain opt-in.

But the underlying problem of dependent class constructors is definitely worth attacking!

[odersky]

Another possible angle of attack would be to generate the anonymous class like this:

def g1(w: IntWidth) = new IntCandidate {type Out = w.Out}

But then we could not define new members that are not already defined in IntCandidate. Or rather we could do this only if we opt in to reflection-based dispatch, and that's also not possible.

[soronpo]

The thing that worries me most is that currently, until this (lack of feature) is resolved, then it's very tempting to use it as I did, and it takes a while to understand why things fail. Do you think it's somehow simple to detect this case and issue a warning/error?

[LPTK]

So it looks like this issue is a duplicate of #10929

I'd say the issue is more pronounced here than in the general case, because dependent givens "feel like" dependent methods, not classes, so we don't expect that they would lose information about their parameter types.

[soronpo]

Revisiting this issue, the proper workaround is this:

trait IntWidth {type Out}
given IntWidth with {type Out = 155}

trait IntCandidate {type Out}
given [W <: IntWidth](using w: W): IntCandidate with {type Out = w.Out}

val x = summon[IntCandidate]
val xx = summon[x.Out =:= 155]

[odersky]

I verified that using tracked paramerers (as in #18958) would also solve this issue. The necessary change would be:

given (using tracked val w: IntWidth): IntCandidate with {type Out = w.Out}