Type infererence regression in `pityka/lamp`

[WojciechMazur]

Based on OpenCB failure for pityka/lamp - builds logs

In latest versions of the compiler the inferred types used for implicit search has changed. In this project, depending either we call .unflit on local variable or directly on the result of StatefulSeq5.apply method the infered type would be different.

Compiler version

Last good release: 3.6.0-RC1-bin-20240912-8e9ded0-NIGHTLY First bad release: 3.6.0-RC1-bin-20240913-e5be3a1-NIGHTLY Bisect points to d0ea3b0546bfae0c10e0f97937ff3a17a2de5860

Minimized code

trait TrainingMode[M]
trait GenericModule[A, B]
sealed trait Variable

type Module = GenericModule[Variable, Variable]
type StatefulModule[A, B, C] = GenericModule[(A, C), (B, C)]
type StatefulModule2[A, B, C, D] = GenericModule[(A, C), (B, D)]

case class Embedding() extends Module
object Embedding {
  implicit val trainingMode: TrainingMode[Embedding] = ???
}
case class LSTM() extends StatefulModule[Variable, Variable, Option[(Variable, Variable)]]
object LSTM {
  implicit val trainingMode: TrainingMode[LSTM] = ???
  implicit val is: InitState[LSTM, Option[(Variable, Variable)]] = ???
}
case class Fun() extends Module
object Fun {
  implicit val trainingMode: TrainingMode[Fun] = ???
}
case class SeqLinear() extends Module
object SeqLinear {
  implicit val trainingMode: TrainingMode[SeqLinear] = ???
}
case class StatefulSeq5[
    T1,T2,T3,T4,T5,T6,
    S1,S2,S3,S4,S5,
    M1 <: StatefulModule[T1, T2, S1],
    M2 <: StatefulModule[T2, T3, S2],
    M3 <: StatefulModule[T3, T4, S3],
    M4 <: StatefulModule[T4, T5, S4],
    M5 <: StatefulModule[T5, T6, S5]
](
    m1: M1 & StatefulModule[T1, T2, S1],
    m2: M2 & StatefulModule[T2, T3, S2],
    m3: M3 & StatefulModule[T3, T4, S3],
    m4: M4 & StatefulModule[T4, T5, S4],
    m5: M5 & StatefulModule[T5, T6, S5]
) extends StatefulModule[T1, T6, (S1, S2, S3, S4, S5)]
object StatefulSeq5 {
  implicit def trainingMode[
    T1,T2,T3,T4,T5,T6,
    S1,S2,S3,S4,S5,
    M1 <: StatefulModule[T1, T2, S1]: TrainingMode,
    M2 <: StatefulModule[T2, T3, S2]: TrainingMode,
    M3 <: StatefulModule[T3, T4, S3]: TrainingMode,
    M4 <: StatefulModule[T4, T5, S4]: TrainingMode,
    M5 <: StatefulModule[T5, T6, S5]: TrainingMode
  ]: TrainingMode[StatefulSeq5[T1,T2,T3,T4,T5,T6,S1,S2,S3,S4,S5,M1,M2,M3,M4,M5]] = ???

  implicit def initState[
    T1,T2,T3,T4,T5,T6,
    S1,S2,S3,S4,S5,
    M1 <: StatefulModule[T1, T2, S1],
    M2 <: StatefulModule[T2, T3, S2],
    M3 <: StatefulModule[T3, T4, S3],
    M4 <: StatefulModule[T4, T5, S4],
    M5 <: StatefulModule[T5, T6, S5]
  ](implicit
      is1: InitState[M1, S1],
      is2: InitState[M2, S2],
      is3: InitState[M3, S3],
      is4: InitState[M4, S4],
      is5: InitState[M5, S5]
  ): InitState[StatefulSeq5[T1, T2, T3, T4, T5, T6, S1, S2, S3, S4, S5, M1, M2, M3, M4, M5], (S1, S2, S3, S4, S5)] = ???
}

implicit class ToLift[M <: Module](mod: M & Module) {
  def lift = LiftedModule(mod)
}
case class LiftedModule[M <: Module](mod: M & Module) extends StatefulModule[Variable, Variable, Unit]
object LiftedModule {
  implicit def trainingMode[M <: Module: TrainingMode]: TrainingMode[LiftedModule[M]] = ???
  implicit def initState[M <: Module]: InitState[LiftedModule[M], Unit] = ???
}

implicit class ToUnlift[A, B, C, D, M <: StatefulModule2[A, B, C, D]](
    mod: M & StatefulModule2[A, B, C, D]
)(implicit is: InitState[M, C]) {
  def unlift = UnliftedModule(mod)(is)
}
case class UnliftedModule[A, B, C, D, M <: StatefulModule2[A, B, C, D]](
    statefulModule: M & StatefulModule2[A, B, C, D]
)(implicit init: InitState[M, C])
    extends GenericModule[A, B]
object UnliftedModule {
  implicit def trainingMode[A, B, C, D, M <: StatefulModule2[A, B, C, D]](implicit
      t: TrainingMode[M],
      is: InitState[M, C]
  ): TrainingMode[UnliftedModule[A, B, C, D, M]] = ???
}
trait InitState[M, C]

case class SupervisedModel[I, M <: GenericModule[I, Variable]](
    module: M & GenericModule[I, Variable]
)(implicit tm: TrainingMode[M])

val model = {
  val net =
    StatefulSeq5(
      Embedding().lift,
      LSTM(),
      Fun().lift,
      SeqLinear().lift,
      Fun().lift
    ).unlift
  SupervisedModel(net) // error, compiles if `unlift` is called on local variable
}

Output

- [E172] Type Error: /Users/wmazur/projects/sandbox/test.scala:108:22 --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
108 |  SupervisedModel(net)
    |                      ^
    |No given instance of type TrainingMode[
    |  UnliftedModule[Variable, Variable, (Unit, Option[(Variable, Variable)], Unit, Unit, Unit), (Unit, Option[(Variable, Variable)], Unit, Unit, Unit),
    |    StatefulSeq5[Variable, Variable, Variable, Variable, Variable, Variable, Unit, Option[(Variable, Variable)], Unit, Unit, Unit, LiftedModule[GenericModule[Variable, Variable]], LSTM, LiftedModule[GenericModule[Variable, Variable]], LiftedModule[GenericModule[Variable, Variable]], LiftedModule[GenericModule[Variable, Variable]]]]
    |] was found for parameter tm of method apply in object SupervisedModel.
    |I found:
    |
    |    UnliftedModule.trainingMode[Variable, Variable, (Unit, Option[(Variable, Variable)], Unit, Unit, Unit), (Unit, Option[(Variable, Variable)], Unit, Unit, Unit),
    |      StatefulSeq5[Variable, Variable, Variable, Variable, Variable, Variable, Unit, Option[(Variable, Variable)], Unit, Unit, Unit, LiftedModule[GenericModule[Variable, Variable]], LSTM, LiftedModule[GenericModule[Variable, Variable]], LiftedModule[GenericModule[Variable, Variable]], LiftedModule[GenericModule[Variable, Variable]]]](
    |      StatefulSeq5.trainingMode²[Variable, Variable, Variable, Variable, Variable, Variable, Unit, Option[(Variable, Variable)], Unit, Unit, Unit, LiftedModule[GenericModule[Variable, Variable]], LSTM, LiftedModule[GenericModule[Variable, Variable]], LiftedModule[GenericModule[Variable, Variable]],
    |        LiftedModule[GenericModule[Variable, Variable]]](LiftedModule.trainingMode³[GenericModule[Variable, Variable]](/* missing */summon[TrainingMode[GenericModule[Variable, Variable]]]), ???, ???, ???, ???),
    |    ???)
    |
    |But no implicit values were found that match type TrainingMode[GenericModule[Variable, Variable]]
    |
    |where:    trainingMode  is a method in object UnliftedModule
    |          trainingMode² is a method in object StatefulSeq5
    |          trainingMode³ is a method in object LiftedModule
    |

Expectation

Should compile

[Gedochao]

cc @odersky

[odersky]

I played with it a bit. The program generates a constraint M >: M & Module where M is a type variable. Previously this constraint was taken to be unsatisfiable. But this is wrong. The constraint has solutions: M = Module is one, M = Nothing is the other. So we now succeed the subtyping test at this point, and this seems to nudge the system onto a path where we get type errors.

So I think https://github.com/scala/scala3/issues/21632#:~:text=Bisect%20points%20to-,d0ea3b0,-Minimized%20code was a bugfix and we need to change the open CB project to work with it.