Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Weird interaction between type inference and implicit search #7586

Closed
abgruszecki opened this issue Nov 20, 2019 · 5 comments
Closed

Weird interaction between type inference and implicit search #7586

abgruszecki opened this issue Nov 20, 2019 · 5 comments
Assignees
Labels
area:implicits related to implicits itype:bug

Comments

@abgruszecki
Copy link
Contributor

abgruszecki commented Nov 20, 2019

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

@abgruszecki abgruszecki added itype:bug area:implicits related to implicits labels Nov 20, 2019
@anatoliykmetyuk
Copy link
Contributor

This manifests also without given – see #7584.

@smarter
Copy link
Member

smarter commented Nov 22, 2019

Looks like this is related to the FunProto caching issues I'm currently working on, stay tuned.

EDIT: Actually no, I think the problem is the heuristic used in tvarsInParams to decide which type variables to instantiate before doing an implicit search, this is the same sort of issue as #7999 (also related: #15184 (comment))

@smarter smarter self-assigned this Nov 22, 2019
@mbovel
Copy link
Member

mbovel commented Dec 21, 2021

Some more tests with the new syntax:

Definitions
trait Nat

case object Z extends Nat
type Z = Z.type

case class S[N <: Nat](pred: N) extends Nat

case class Sum[N <: Nat, M <: Nat, R <: Nat](result: R)

given zero: Z = Z
given succ[N <: Nat](using n: N): S[N] = S(n)

given sumZ[N <: Nat](using n: N): Sum[Z, N, N] = Sum(n)

given sumS[N <: Nat, M <: Nat, R <: Nat](
  using sum: Sum[N, M, R]
): Sum[S[N], M, S[R]] = Sum(S(sum.result))

def add[N <: Nat, M <: Nat, R <: Nat](n: N, m: M)(
  using sum: Sum[N, M, R]
): R = sum.result

case class Prod[N <: Nat, M <: Nat, R <: Nat](result: R)
add(S(Z), S(S(Z)): S[S[Z]])(using
  sumS(using
    sumZ(using
      succ(using
        succ(using
            zero
        )
      )
    )
  )
)
// res0: S[S[S[Z]]] = S(S(S(Z)))

add(S(Z), S(S(Z)): S[S[Z]])(using
  sumS(using
    sumZ(using
      succ(using
        zero
      )
    )
  )
)
// res1: S[S[_ >: S[Z] & Z <: S[Z] | Z]] = S(S(Z))

add(S(Z), S(S(Z)))(using
  sumS(using
    sumZ(using S(S(Z))
    )
  )
)
// res2: S[S[S[Z]]] = S(S(S(Z)))

add(S(Z), S(S(Z)): S[S[Z]])
// res3: S[S[S[Z]]] = S(S(S(Z)))

add(S(Z), S(S(Z)))
// res4: S[S[Nat]] = S(S(Z))

@mbovel
Copy link
Member

mbovel commented Jun 10, 2023

Observation from @cpitclaudel: instead of defining sumZ as above, we can define:

given sumZZ: Sum[Z, Z, Z] = Sum(Z)
given sumZS[N <: Nat](using sum: Sum[Z, N, N]): Sum[Z, S[N], S[N]] = Sum(S(sum.result))

For which inference and implicit search work as expected:

add(S(Z), S(S(Z)): S[S[Z]])(using
  sumS(using
    sumZS(using
      sumZS(using
        sumZZ
      )
    )
  )
)
// res0: S[S[S[Z]]] = S(S(S(Z)))

add(S(Z), S(S(Z)): S[S[Z]])
// res1: S[S[S[Z]]] = S(S(S(Z)))

add(S(Z), S(S(Z)))
// res2: S[S[S[Z]]] = S(S(S(Z)))
Full worksheet
trait Nat

case object Z extends Nat
type Z = Z.type

case class S[N <: Nat](pred: N) extends Nat

case class Sum[N <: Nat, M <: Nat, R <: Nat](result: R)

given zero: Z = Z
given succ[N <: Nat](using n: N): S[N] = S(n)

given sumZZ: Sum[Z, Z, Z] = Sum(Z)

given sumZS[N <: Nat](using sum: Sum[Z, N, N]): Sum[Z, S[N], S[N]] = Sum(S(sum.result))

given sumS[N <: Nat, M <: Nat, R <: Nat](
  using sum: Sum[N, M, R]
): Sum[S[N], M, S[R]] = Sum(S(sum.result))

def add[N <: Nat, M <: Nat, R <: Nat](n: N, m: M)(
  using sum: Sum[N, M, R]
): R = sum.result

add(S(Z), S(S(Z)): S[S[Z]])(using
  sumS(using
    sumZS(using
      sumZS(using
        sumZZ
      )
    )
  )
)

add(S(Z), S(S(Z)): S[S[Z]])

add(S(Z), S(S(Z)))

@EugeneFlesselle
Copy link
Contributor

Fixed by #19096

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:implicits related to implicits itype:bug
Projects
None yet
Development

No branches or pull requests

5 participants