Re: can/should Functor have a quantified coercible constraint?

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