Regression in givens

[soronpo]

I actually first found this regression when upgrading from 3.4.0 to 3.4.1-RC1, but during minimization I reached a point where the error always surfaced until I went back to 3.0.0 and saw no error. Aux pattern can be used as a workaround. I bisected it to the versions below.

Compiler version

Last good release: 3.0.2-RC1-bin-20210609-fdbb94f-NIGHTLY
First bad release: 3.0.2-RC1-bin-20210610-fe2fcc4-NIGHTLY
bisect: ff8659e

Minimized code

trait Summon[R, T <: R]:
  type Out
object Summon:
  given [R, T <: R]: Summon[R, T] with
    type Out = R

trait DFTypeAny
trait DFBits[W <: Int] extends DFTypeAny
class DFVal[+T <: DFTypeAny]
type DFValAny = DFVal[DFTypeAny]
type DFValOf[+T <: DFTypeAny] = DFVal[T]
trait Candidate[R]:
  type OutW <: Int
object Candidate:
  type Aux[R, O <: Int] = Candidate[R] { type OutW = O }
  given [W <: Int, R <: DFValOf[DFBits[W]]]: Candidate[R] with
    type OutW = W

extension [L](lhs: L) def foo(using es: Summon[L, lhs.type]): Unit = ???
extension [L <: DFValAny](lhs: L)(using icL: Candidate[L]) def baz: DFValOf[DFBits[icL.OutW]] = ???
extension [L <: DFValAny, W <: Int](lhs: L)(using icL: Candidate.Aux[L, W])
  def bazAux: DFValOf[DFBits[W]] = ???

val x = new DFVal[DFBits[4]]
val works = x.bazAux.foo
val fails = x.baz.foo

Output

26 |val fails = x.baz.foo
   |            ^^^^^^^^^
   |value foo is not a member of DFVal[DFBits[?1.OutW]].
   |An extension method was tried, but could not be fully constructed:
   |
   |    foo[DFVal[DFBits[?1.OutW]]](
   |      baz[DFVal[DFBits[(4 : Int)]]](x)(Candidate.given_Candidate_R[(4 : Int), R])
   |    )(Summon.given_Summon_R_T[R, T])    failed with
   |
   |        no implicit argument of type Summon[DFVal[DFBits[?1.OutW]], (?2 : DFVal[DFBits[?1.OutW]])] was found for parameter es of method foo
   |
   |        where:    ?1 is an unknown value of type Candidate.given_Candidate_R[(4 : Int), DFVal[DFBits[(4 : Int)]]]
   |                  ?2 is an unknown value of type DFVal[DFBits[?1.OutW]]
   |        .
   |        I found:
   |
   |            Summon.given_Summon_R_T[R, T]
   |
   |        But given instance given_Summon_R_T in object Summon does not match type Summon[DFVal[DFBits[?1.OutW]], (?2 : DFVal[DFBits[?1.OutW]])].
   |
   |where:    ?1 is an unknown value of type Candidate.given_Candidate_R[(4 : Int), R]
1 error found

Expectation

No error.

[odersky]

I think that will have to await the improvements in the givens SIP. The second installment should handle tracked parameters. As far as I can see it only worked by accident for this very special case before.

[soronpo]

Why is it a special case? It's not like the problem with cascading givens, it's something different.

[soronpo]

If you are referring to #13580, it's not the same thing, IIUC. Notice how the given for candidate is defined. This prevents the given Out loss.

[odersky]

It's simply not supported. The previous wIldcards which were allowed by accident in constraints somehow must have given the illusion that it would work, but they never were meant to solve it, nor can I see how they would be a solution. To support it, we need quite a bit of machinery, all of it implemented in the typeclasses PR. Specifically, we need to track in a class instantiation what are the precise values given as arguments. Look for tracked in the commits and discussions.

If you are referring to #13580, it's not the same thing, IIUC. Notice how the given for candidate is defined. This prevents the given Out loss.

Maybe not. But the symptoms, i.e. a skolem type appearing in the error message and need for the Aux pattern to fix it, looks exactly like what tracked parameters are meant to solve.

[soronpo]

Maybe not. But the symptoms, i.e. a skolem type appearing in the error message and need for the Aux pattern to fix it, looks exactly like what tracked parameters are meant to solve.

On a hunch I did the following trick instead of using an Aux pattern:

import compiletime.ops.int.+
extension [L <: DFValAny](lhs: L)(using icL: Candidate[L]) def baz: DFValOf[DFBits[icL.OutW + 0]] = ???

This causes the code to compile successfully.
So this leads me to believe that this is NOT a type tracking problem, but something else.
(and FWIW, also tried the trick on #13580, and it didn't work)

[odersky]

I am not sure what it is. But the reason it worked before was that it used something that should never happen - wildcards in constraints.