can/should Functor have a quantified coercible constraint?

[Richard Eisenberg]

> On Jan 3, 2021, at 1:02 PM, Carter Schonwald <carter.schonwald at gmail.com> wrote:
> 
> This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

Lifting the limitation would be nice, but it's a lot of work. First, we need an updated theory for Core, with a type safety proof. This proof is essential: it's what our safety as a language depends on. Then, we'd need to implement it. I'm more worried about the former than the latter.

> i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper...

Yes, that was originally true, but the current formulation goes beyond the 2011 paper in some respects. See section 7.1 of https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf <https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf>.

Roman writes:

> 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.

This is tough. I've considered a Functor definition like the one Carter proposes before. I would personally rather come up with the best definition first, then figure out how to make it palatable to newcomers second. For example, we could write (today)

> type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)

and then the class constraint looks more pleasant. Or we could create ways of suppressing confusing information. Or there are other solutions. Depending on the benefit of the change (here or elsewhere), I would advocate holding off on making the change until we can support it without disrupting the newcomer story. But I wouldn't want to abandon the idea of an improvement a priori just because of a disruption to the newcomer experience.

Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20210104/30265bd5/attachment.html>