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@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries