can/should Functor have a quantified coercible constraint?

[Carter Schonwald]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20210103/72cb70eb/attachment.html>