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?