Scala 3 unimported given

Question
1

The code below fails to compile, with the following note at the end of the error message:

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

I tried adding import NatDividesH.given in all places I could think of, but the note remained.

Here is the original 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]
type _3 = Succ[_2]

Here is the code with given imports added everywhere, to no avail:

import NatDividesH.given

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

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

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

@main def main(): Unit =
  import NatDividesH.given
  summon[NatDivides[_2, _2]]

type _0 = Zero
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
1 Like
2

I’ve added

given [X <: Succ[NatT]]: NatDividesH[X, X, _0]()

under

object NatDividesH:

and it started to work, e.g.: Scastie - An interactive playground for Scala.

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]]: NatDividesH[X, X, _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 =
  println(summon[NatDivides[_2, _6]])

type _0 = Zero
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]
type _5 = Succ[_4]
type _6 = Succ[_5]
type _7 = Succ[_6]

The error you’ve got, i.e.:

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

was probably spurious and you could file it as a bug.

2 Likes
3

Thank you!

Do you understand why this additional rule helps? It seems to be admissible:

From the first rule in NatDividesH, we get NatDividesH[X, _0, _0], which can be converted to NatDividesH[X, _0, X] by the second rule (in my code), and then to NatDividesH[X, X, _0] via repeated application of the third rule.

Moreover, for NatDivides[_2, _2] at least, there seems to ever be only one rule applicable during construction of the proof by the compiler.

4

no :slight_smile:

note that for your original code IntelliJ shows inference of implicit arguments that matches your explanation:

image
image1009×774 91.4 KB

but for my modified code it fails:
image
image1020×832 129 KB

maybe there’s a bug in scala compiler then?

note that your original code will compile under scala compiler and also be correctly analyzed by intellij if you do a bit of micromanagement and change main method to explicitly state some arguments:

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 zzz1 [X <: Succ[NatT]]: NatDividesH[X, _0, _0]()
  given zzz2 [X <: Succ[NatT], Y <: NatT](using NatDividesH[X, Y, _0]): NatDividesH[X, Y, X]()
  given zzz3 [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 aaa1 [X <: Succ[NatT], Y <: NatT](using proof: NatDividesH[X, Y, _0]): NatDivides[X, Y]()

@main def main(): Unit =
  summon[NatDivides[_2, _2]](using NatDivides.aaa1(using NatDividesH.zzz3))

type _0 = Zero
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]
type _5 = Succ[_4]
type _6 = Succ[_5]
type _7 = Succ[_6]
2 Likes
5

Nice observations. It seems quite suspect indeed. I opened an issue.