VerifiedFunctor - prove map (map g) x = x

Question

I'm trying to prove a statement about VerifiedFunctor interface (a Functor which map method respects identity and composition):

interface Functor f => VerifiedFunctor (f : Type -> Type) where
    functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) ->
                      (x : f a) -> map g x = x

Here's the statement (which logically says that map . map for two given functors also respects identity):

functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
                         (g : a -> a) -> ((v : a) -> g v = v) ->
                         (x : f2 (f1 a)) -> map (map g) x = x
functorIdentityCompose fnId prId = functorIdentity (map fnId) (functorIdentity fnId prId)

However, I'm getting following error:

Type mismatch between
        (x : f1 a) -> map fnId x = x (Type of functorIdentity fnId prId)
and
        (v : f a) -> map fnId v = v (Expected type)

Specifically:
        Type mismatch between
                f1 a
        and
                f a

I tried to specify all implicit arguments:

functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
                         {a : Type} -> {f1 : Type -> Type} -> {f2 : Type -> Type} ->
                         (g : a -> a) -> ((v : a) -> g v = v) -> (x : f2 (f1 a)) ->
                         map {f=f2} {a=f1 a} {b=f1 a} (map {f=f1} {a=a} {b=a} g) x = x

... But got another error:

When checking argument func to function Prelude.Functor.map:
        Can't find implementation for Functor f15

So any ideas what is wrong here and how to prove this statement?

Answer 1

Here is a heuristic: when "obvious" things don't work... eta-expand! So this works:

functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
  (g : a -> a) -> ((v : a) -> g v = v) ->
  (x : f2 (f1 a)) -> map (map g) x = x
functorIdentityCompose fnId prId x =
  functorIdentity (map fnId) (\y => functorIdentity fnId prId y) x

It looks like full application triggers instance search.