Nonsensical given error

[Bersier]

Compiler version

3.1.3

Minimized code

sealed trait NatT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT

sealed trait NatDividesH[X <: Succ[NatT], Y <: NatT, Z <: NatT]
object NatDividesH:
  given [X <: Succ[NatT]]: NatDividesH[X, _0, _0]()
  given [X <: Succ[NatT], Y <: NatT](using NatDividesH[X, Y, _0]): NatDividesH[X, Y, X]()
  given [X <: Succ[NatT], Y <: NatT, Z <: NatT](using NatDividesH[X, Y, Succ[Z]]): NatDividesH[X, Succ[Y], Z]()

sealed trait NatDivides[X <: Succ[NatT], Y <: NatT]
object NatDivides:
  given [X <: Succ[NatT], Y <: NatT](using proof: NatDividesH[X, Y, _0]): NatDivides[X, Y]()

@main def main(): Unit =
  summon[NatDivides[_2, _2]]

type _0 = Zero
type _1 = Succ[_0]
type _2 = Succ[_1]

Output

no given instance of type NatDivides[_2, _2] was found for parameter x of method summon in object Predef.
I found:

    NatDivides.given_NatDivides_X_Y[Succ[_1], Succ[_1]](
      NatDividesH.given_NatDividesH_X_Succ_Z[Succ[_1], Succ[_0], Zero](
        NatDividesH.given_NatDividesH_X_Y_X[X, Y]
      )
    )

But given instance given_NatDividesH_X_Y_X in object NatDividesH does not match type NatDividesH[Succ[_1], Succ[_0], Succ[Zero]].

Note: given instance given_NatDividesH_X_Succ_Z in object NatDividesH was not considered because it was not imported with `import given`.

Expectation

given instance given_NatDividesH_X_Succ_Z in object NatDividesH should have been considered. No import given can currently fix this error (see this thread).

[som-snytt]

Compare #15692