can/should Functor have a quantified coercible constraint?

[Carter Schonwald]

So this actually is a very good point!

Happily, the technological steps needed to resolve issues that other
comments so far have raised point to a better fix!


Borrowing from the 2011 paper, we would write the following

‘’’
class Functor (f : Type/representational -> Type)  where
‘’’

Basically this then pushes the info into kind signatures.  As was
originally intended. And role inferred/ annotated kind signatures provides
a mechanism for gnd to work again for monad transformers and unvoxed vector


On Mon, Jan 4, 2021 at 5:50 AM Roman Cheplyaka <roma at ro-che.info> wrote:

> 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
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20210104/009c1373/attachment.html>