troubles with sum.rec

sum.lean

import logic.function
open function
variables {α β γ : Type} (f : α → γ) (g : β → γ)

-- Want to get α ⊕ β → γ
#check sum.rec f g -- error
#check (sum.rec f g : α ⊕ β → γ) -- error
#check λ a, sum.rec f g a -- error
#check λ a, (sum.rec f g a : γ)
-- λ (a : α ⊕ β), sum.rec f g a : Π (a : α ⊕ β), (λ (_x : α ⊕ β), γ) a
#check ((λ a, sum.rec f g a) : α ⊕ β → γ)
-- λ (a : α ⊕ β), sum.rec f g a : Π (a : α ⊕ β), (λ (_x : α ⊕ β), γ) a

-- Now try to do something with it
#check surjective (λ a, (sum.rec f g a : γ)) -- error
#check surjective ((λ a, sum.rec f g a) : α ⊕ β → γ) -- still error!
/-
type mismatch at application
  surjective (λ (a : α ⊕ β), sum.rec f g a)
term
  λ (a : α ⊕ β), sum.rec f g a
has type
  Π (a : α ⊕ β), (λ (_x : α ⊕ β), γ) a : Type
but is expected to have type
  ?m_1 → ?m_2 : Sort (imax ? ?)
-/
#check surjective (@sum.rec _ _ (λ _, γ) f g) -- same error
#check @surjective (α ⊕ β) γ (λ a, sum.rec f g a) -- ok, but ugh

-- Make everything easy with a non-dependent version of sum.rec
def sum.rec' (a : α ⊕ β) : γ := sum.rec f g a

#check sum.rec' f g
-- either f g : α ⊕ β → γ
#check surjective (sum.rec' f g) -- ok