can/should Functor have a quantified coercible constraint?

[David Feuer]

You're not being very imaginative at all. Try out, oh, `StateT s Maybe`. Or
play around with a nice fake functor like the magma used to implement
`traverseBia` in `bifunctors`—pretty sure that won't work out.

On Sun, Jan 3, 2021, 11:00 AM Carter Schonwald <carter.schonwald at gmail.com>
wrote:

> Hey everyone!
>
> for context, I have some code where I was seeing how far coerce lets me go
> to avoid doing wrappers for certain codes,
>
> i found i had to write the following (mapping an operation over to its
> newtyped sibling)
>
> ```
> -- > :t QRA.wither
> --- forall a b f . Applicative f => (a -> f (Maybe b)) -> RAList a -> f
> (RAList b)
> ---
> wither :: forall a b f . (Applicative f, (forall c d .  Coercible c d =>
> Coercible (f c) (f d))  ) =>
>         (a -> f (Maybe b)) -> RAList a -> f (RAList b)
> wither = \f la ->    coerce     $ QRA.wither f $ coerce la
> ```
>
> i'd much rather be able to write
> ```
> wither :: forall a b f . (Applicative f) =>
>         (a -> f (Maybe b)) -> RAList a -> f (RAList b)
> wither = \f la ->    coerce     $ QRA.wither f $ coerce la
> ```
>
>
> 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 ..
> ```
>
> is there any specific reason why this is not feasible? I cant think of a
> GADT where this wouldn't be totally safe to do (because unlike in foldable,
> f is in both the domain and co-domain), but maybe i'm not being imaginative
> enough?
>
> look forward to learning what our obstacles are to making this happen for
> ghc 9.2 :)
>
> -Carter
>
> _______________________________________________
> 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/20210103/6a1d2ece/attachment.html>