Function overloading issue

Stream: lean4

[Tomas Skrivan]

I'm trying to do function overloading with typeclasses but I have encountered a problem when using a bit more complicated lambda functions.

class Foo (α : Type) (β : outParam Type) where
  foo : α → β

export Foo (foo)

instance {X Y : Type} : Foo (X → Y) (X → X → Y) where
  foo f _ dx := f dx

instance : Foo Nat (Nat → Nat) where
  foo n := λ m => n + m

variable {X Y Z : Type} (f : X → Y → Z) (g : X → Y)

#check foo 1 -- works: foo 1 : Nat → Nat
#check foo g -- works: foo g : X → X → Y
#check_failure foo (λ ((x,y) : X×Y) => f x y)     -- does not work
#check foo (α := _→Z) (λ ((x,y) : X×Y) => f x y) -- works

It gives an error:

stuck at solving universe constraint
  1 =?= imax 1 ?u.246
while trying to unify
  (x : X × Y) → ?m.249 x : Sort (imax 1 ?u.246)
with
  (x : X × Y) → ?m.249 x : Sort (imax 1 ?u.246)

I really do not understand why are universes involved? Also why is ?m.249 x not inferred to be Z when the type of f is fixed.

[Tomas Skrivan]

Ohh the notation (λ (x,y) => f x y) expands to a match, so this fails:

#check_failure foo (fun x => match x with | (x, y) => f x y)

Looks like the output type of this match can't be inferred automatically for some reason.