can/should Functor have a quantified coercible constraint?

[Roman Cheplyaka]

On 03/01/2021 17.59, Carter Schonwald wrote:
> this seems like it'd be best done via something like changing the
> functor class definition to
> 
> ```
> class (forall c d .  Coercible c d => Coercible (f c) (f d))  ) =>
> Functor f where ..
> ```

I think it's important we keep the definitions of Functor and other
fundamental classes understandable by newcomers, and this change would
make the definition look scary for a marginal benefit.

Roman