Type-safely Implementing an Arbitrary Degree Blackbird Combinator (B-n Combinator)

Question

As the title suggests I'm trying to implement an arbitrary degree blackbird combinator (something I'd always wanted but could never have in Haskell), that is:

bird : (n : Nat) -> (x -> y) -> (a1 -> a2 -> ... -> an -> x) -> a1 -> a2 -> ... -> an -> y
bird k f g x1 ... xk = f (g x1 ... xk)

bird 0 = (&)
bird 1 = (.)
bird 2 = (.:)

But I've been flailing around for an eternity trying to get this to work. This is my first time writing Idris, apologies for the ignorance that ensues:

import Data.Vect

args : Foldable t => Type -> t Type -> Type
args = foldr (\acc, t => acc -> t)

And then two different implementations of my combinator (not tested at the same time!):

bird : {ts : Vect n Type} -> (n : Nat) -> (a -> b) -> args a ts -> args b ts
bird  Z    f     = f
bird (S k) f g x = bird k f (g x)

bird : {ts : Vect n Type} -> (n : Nat) -> (a -> b) -> args a ts -> args b ts
bird k = foldr (.) id $ replicate k (.)

Yeilding this error

Error: While processing right hand side of bird. Can't solve constraint
between: a and foldrImpl (\acc, t => acc -> t) a id ts.

and this one,

Error: While processing right hand side of bird. When unifying:
    ?a -> a
and:
    a
Mismatch between: ?a -> a and a.

respectively. Frankly I think part of the problem might be Idris's odd treatment of composition, for example, (.) . (.) has a vastly different type then it does in Haskell, and frankly it seems to me that Haskell got it right, (.) . (.) : (?b -> ?c) -> (?a -> ?a -> ?b) -> ?a -> ?a -> ?c (Idris) instead of (.) . (.) :: (c -> d) -> (a -> b -> c) -> a -> b -> d (Haskell)

Thanks for your help!