Using givens with type members

Question
1

I have the following code in my lib:

trait Statement[A] {}

trait Derivation[B]:
  type Source
object Derivation:
  def make[A, B](using Statement[A]) =
    new Derivation[B]:
      type Source = A  

  def check[A, B](using Derivation[B] { type Source = A }): Unit = ()

case class Foo(a: Unit)
case class Bar(b: Unit)

given Statement[Foo] = new Statement[Foo] {}
given Derivation[Bar] = Derivation.make[Foo, Bar]

Now I want this code written by user to compile:

Derivation.check[Foo, Bar]

But it doesn’t because we erased Source in our given. User could write it as:

given Derivation[Bar] { type Source = Bar } = Derivation.make[Foo, Bar]

I don’t want to do that because it’s a user-facing code and looks ugly for someone who doesn’t want to know how the underlying lib works. The only option I have right now is to stick with Derivation[A, B]

I have two questions:

  1. Is there a way to avoid explicit type members and two type parameters?
  2. Is there a way to find all Derivations of Foo? Derivation.make establishes Bar-to-Foo relationship, but I want to know all relationships that point to Foo, i.e. all givens of Derivation where Foo is used.
1 Like
2
  1. Is there a way to avoid explicit type members and two type parameters?

Not yet, but there is an implemented proposal that would enable this: Pre-SIP: Improvements to Type Classes by odersky · Pull Request #19395 · lampepfl/dotty · GitHub

3

I could be wrong here, but is this not one of the things the Aux pattern is supposed to solve for?

4

Just as a shortcut for to those who don’t want to read the pre SIP: It uses a syntactically interesting alternative to the aux pattern using a helper type, that I adapted to apply to the original question:

infix type from[B <: {type Source <: AnyKind}, A <: AnyKind] = B { type Source = A }

given (Derivation[Bar] from Foo) = Derivation.make[Foo, Bar]

You can already use something like this (even without the pre-SIP), if that syntax seems reasonable to you.
see scastie: Scastie - An interactive playground for Scala.