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
_______________________________________________