Context function type reduction

I don’t understand the compiler error for the code below:

final case class Var(name: String)
(using t: Tuple, p: Contains[t.type, name.type] =:= true)

final class Scope(val vars: Tuple, val v: vars.type ?=> Var)

type Contains[L <: Tuple, U] <: Boolean = L match
  case EmptyTuple => false
  case U *: tail => true
  case _ *: tail => Contains[tail, U]

Scope(("one", "two"), Var("one"))


Cannot prove that Contains[t.type, ("one" : String)] =:= (true : Boolean).

Note: a match type could not be fully reduced:

  trying to reduce  Contains[t.type, ("one" : String)]
  failed since selector t.type
  does not match  case EmptyTuple => (false : Boolean)
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining cases

    case ("one" : String) *: tail => (true : Boolean)
    case _ *: tail => Contains[tail, ("one" : String)]

From the documentation on context functions, I would expect

Scope(("one", "two"), Var("one"))

to first get expanded to

Scope(("one", "two"), (x_1: ("one", "two")) ?=> Var("one"))

So t.type should be known to be ("one", "two"), which should allow

Contains[t.type, ("one" : String)]

to reduce.

However, from the error message, it seems that the compiler doesn’t know anyting about t.type