[Agda] A problem with instance arguments and function application.

[effectfully]

Hello. I encountered a problem while playing with instance arguments.
I have a usual hierarchy Monad <: Applicative <: Functor. Here is the
definition of the Monad for example:


record Monad {α} (M : Set α -> Set α) : Set (suc α) where
  infixl 1 _>>=_

  field
    return : ∀ {A} -> A -> M A
    _>>=_  : ∀ {A B} -> M A -> (A -> M B) -> M B

  instance
    Monad<:Applicative : Applicative M
    Monad<:Applicative = record { pure = return ; _<*>_ = λ mf mx ->
mf >>= λ f -> mx >>= return ∘ f }
open Monad {{...}}


I wrote a polyvariadic variant of the liftA function:


record _~>_ {α β} (A : Set α) (B : Set β) : Set (α ⊔ β) where
  constructor rec
  field apply : A -> B

instance
  Id : ∀ {α} {A : Set α} -> A ~> A
  Id = rec id

  Fmap : ∀ {α γ} {A B : Set α} {C : Set γ} {F : Set α -> Set α}
       -> {{_ : F B ~> C}} {{_ : Applicative F}} -> (A -> B) ~> (F A -> C)
  Fmap {{rec r}} = (λ f x -> r (f <$> x))

  Ap : ∀ {α γ} {A B : Set α} {C : Set γ} {F : Set α -> Set α}
     -> {{_ : F B ~> C}} {{_ : Applicative F}} -> F (A -> B) ~> (F A -> C)
  Ap {{rec r}} = (λ f x -> r (f <*> x))

liftA : ∀ {α γ} {A B : Set α} {C : Set γ} {F : Set α -> Set α}
      -> {{_ : F B ~> C}} {{_ : Applicative F}} -> (A -> B) -> F A -> C
liftA = _~>_.apply Fmap


I.e. lift a function using _<$>_ and then apply _<*>_ to all arguments
recursively until the type becomes (A -> A) for some A. Agda happily
accepts these definitions:

    test-1 : List ℕ -> List ℕ
    test-1 = liftA suc

    test-2 : List ℕ -> List ℕ -> List ℕ
    test-2 = liftA _+_

But

    test-3 : List (ℕ × ℕ)
    test-3 = liftA _,_ (1 ∷ 2 ∷ 3 ∷ []) (4 ∷ 5 ∷ [])

results in unresolved metas. Which can surprisingly be fixed by
inserting _$_ like this:

    test-3 : List (ℕ × ℕ)
    test-3 = (liftA _,_ $ (1 ∷ 2 ∷ 3 ∷ [])) $ (4 ∷ 5 ∷ [])

I.e. (f x y) doesn't typecheck, while (f x $ y) typechecks. (f x) has
a functional type, and _$_ explicitly clarifies that, but it should be
clear from the fact that (f x) is applied to (y). So is it a
unification defect?

I'm using Agda 2.4.2.2. The code:
https://github.com/effectfully/random-stuff/blob/master/stuff/liftA.agda

Thanks for the attention.