Givens in ADT cases

Dotty
1

Hi,

Although it is possible to define a ADT where some term has a given parameter, it does not seem possible to use it:


trait Bar[A]:
  def hello(value: A): Int
​
  extension (value: A) def h: Int = hello(value)
​
object Bar:
  given Bar[String] with
    def hello(value: String) = value.length
​
enum Foo:
  case Case[A: Bar](value: A)

object Foo:
  val test: Foo = Case("world")
  test match
    case Case(value) => value.h // Compile error: value h is not a member of A$1

I tried pattern matching on the given

    case Case(value)(B @ given Bar[?])

But there is a syntax error: '=>' expected, but '(' found

Is this a bug, or am I using the feature wrong?

2

That’s not valid pattern matching syntax, but perhaps you could make the parameter explicit in the definition of Case?

3

… Yes :sweat_smile: It’s a bit disappointing, but I can live with that.

4

Depending on the use case, you could use a named context parameter instead of the context bound:

trait Bar[A]:
  def hello(value: A): Int
  extension (value: A) def h: Int = hello(value)

object Bar:
  given Bar[String] with
    def hello(value: String) = value.length

enum Foo:
  case Case[A: Bar](value: A)(using private[Foo] val ev: Bar[A])

object Foo:
  val test: Foo = Case("world")
  test match
    case c @ Case(value) => c.ev.h(value)

I’m not sure if this already too explicit. And it’s more verbose, admittedly.

1 Like
5

This is nice, but do you need the context bound? There’s a using anyway, right?

6

Yeah it works. It’s sad though, as it seems like all elements are there (even pattern match on givens).

7

Oops, I forgot to remove the context bound after experimenting with various ways.