Description
This was found when writing type-level addition of Nat
s using given
, and best explained with that. Given the (typical) definitions below:
sealed trait Nat
case object Z extends Nat
case class S[N <: Nat](pred: N) extends Nat
type Z = Z.type
given [N <: Nat](given n: N) as S[N] = S(n)
given zero as Z = Z
case class Sum[N <: Nat, M <: Nat, R <: Nat](r: R)
given [N <: Nat](using n: N) as Sum[Z, N, N] = Sum(n)
given [N <: Nat, M <: Nat, R <: Nat](
using sum: Sum[N, M, R]
) as Sum[S[N], M, S[R]] = Sum(S(sum.r))
def add[N <: Nat, M <: Nat, R <: Nat]( n: N, m: M )(using sum: Sum[N, M, R]): R = sum.r
The following work correctly:
add(Z, S(Z)) // ===> S(Z) : S[Z]
add(S(S(Z)), S(Z)) // ===> S(S(S(Z))) : S[S[S[Z]]]
add(S(S(S(S(S(Z))))), S(Z)) // ===> S(S(S(S(S(S(Z)))))) : S[S[S[S[S[S[Z]]]]]]
However, add
stops working correctly if the second argument is more than 1:
add(S(Z), S(S(Z))) // ===> S(S(Z)) : S[S[Nat & Product & Serializable]]
However, if we explicitly type the second argument, everything works correctly:
add(S(Z), S(S(Z)) : S[S[Z]]) // ===> S(S(S(Z))) : S[S[S[Z]]]
Note that the size of the first argument does not matter as long as the second is typed explicitly:
add(S(S(S(S(S(Z))))), S(S(Z)) : S[S[Z]])
val res10: S[S[S[S[S[S[S[Z]]]]]]] = S(S(S(S(S(S(S(Z)))))))
Minimized
The actual problem lies with given
definitions for Nat
itself:
def lookup[N <: Nat](n: N)(using m: N) = m
lookup(S(S(Z))) // ===> S(Z) : S[Nat & Product & Serializable]
Note how we lose precision above. The weird part about this is that the only part that loses precision is looking up Nat
with given
s - the definitions for Sum
recurse in much the same way as the definitions for Nat
, but they always work correctly.
But wait, there's more!
If instead of trying to look up Nat
, we look up a wrapped Nat
like this:
given [N <: Nat](using wn: Wrapped[N]) as Wrapped[S[N]] = Wrapped(S(wn.n))
given Wrapped[Z] = Wrapped(Z)
given [N <: Nat](using wn: Wrapped[N]) as Sum[Z, N, N] = Sum(wn.n)
// ... rest of the definitions as above
Then the problem from above does not appear:
scala> add(S(S(S(S(S(Z))))), S(S(Z)))
val res2: S[S[S[S[S[S[S[Z.type]]]]]]] = S(S(S(S(S(S(S(Z)))))))
Concluding
Recursing on a type argument in given
search behaves differently than recursing on a top-level type. This looks like a bug. I don't know if it's a bug, but at the very least it's weird and unintuitive behaviour.