Scala context bounds in generalized algebraic datatype

Question

Consider the following Scala 3 code, where Obj[_] refers to a type class and Context is a generalized algebraic datatype.

enum Context[T: Obj]:
  case Empty[U <: Unit: Obj]() extends Context[U]
  case Variable[A: Obj](x: A) extends Context[A]
  case Product[A: Obj, B: Obj](ctx1: Context[A], ctx2: Context[B])(using Obj[(A,B)]) extends Context[(A,B)]
  
def lookup[A: Obj, B: Obj](ctx: Context[A], x: B) =
  ctx match
    case Product(ctx1, ctx2): Context[(a1,b1)] =>
       // No implicit argument of type Obj[a1] was found for an implicit parameter of method lookup.
      lookup[a1,B](ctx1, x)
    ...

The Scala compiler is not able to infer that type a1 has the context bound Obj, even though the bound is declared in the Product case. Is there a way to solve this problem without passing the implicits explicitly everywhere?

Answer 1

Apparently, Scala doesn't extract the implicits of constructors. The solution is to extract them explicitly:

enum Context[T: Obj]:
  case Product[A, B](ctx1: Context[A], ctx2: Context[B])
                    (using val aObj: Obj[A], val bObj: Obj[B], val pObj: Obj[(A,B)])
                    extends Context[(A,B)]
  ...
import Context.*
  
def lookup[A: Obj, B: Obj](ctx: Context[A], x: B): Unit =
  ctx match
    case p @ Product(ctx1, ctx2): Context[(a1,b1)] =>
      given Obj[(a1, b1)] = p.pObj
      given Obj[a1] = p.aObj
      given Obj[b1] = p.bObj
      lookup[a1,B](ctx1, x)
    ...