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"))
Error:
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…