Why Applicative_Fun instance is local?

[vzaliva]

We have Local Instance Applicative_Fun in ExtLib/Data/Fun.v. This makes it undiscoverable during typeclass search and I have to write:

liftA2 (AT:=(Applicative_Fun _)) f x y

instead of just:

liftA2 f x y

[gmalecha]

Let's try to make it global. I think I was potentially worried about it unifying too many places and therefore being difficult to use.

[vzaliva]

what about Functor_Fun and the rest of the instances in Fun.v?