-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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
Comments
This manifests also without |
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)) |
Some more tests with the new syntax: Definitionstrait 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)) |
Observation from @cpitclaudel: instead of defining 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 worksheettrait 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))) |
Fixed by #19096 |
This was found when writing type-level addition of
Nat
s usinggiven
, and best explained with that. Given the (typical) definitions below:The following work correctly:
However,
add
stops working correctly if the second argument is more than 1:However, if we explicitly type the second argument, everything works correctly:
Note that the size of the first argument does not matter as long as the second is typed explicitly:
Minimized
The actual problem lies with
given
definitions forNat
itself:Note how we lose precision above. The weird part about this is that the only part that loses precision is looking up
Nat
withgiven
s - the definitions forSum
recurse in much the same way as the definitions forNat
, but they always work correctly.But wait, there's more!
If instead of trying to look up
Nat
, we look up a wrappedNat
like this:Then the problem from above does not appear:
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
The text was updated successfully, but these errors were encountered: