Skip to content

Weird interaction between type inference and implicit search #7586

Closed
@abgruszecki

Description

@abgruszecki

This was found when writing type-level addition of Nats 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 givens - 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.

/cc @anatoliykmetyuk @smarter

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions