<div dir="auto">Thx for  the link.  I’ll take a look at your suggested reading. </div><div dir="auto"><br></div><div dir="auto">What are ways I could help progress whatever’s needed to get to a nice ending?</div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Jan 4, 2021 at 9:00 AM Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><br><div><br><blockquote type="cite"><div>On Jan 3, 2021, at 1:02 PM, Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>> wrote:</div><br><div><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none;float:none;display:inline!important">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?</span></div></blockquote></div><br><div>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.</div><div><br></div><div>> i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper...</div><div><br></div><div>Yes, that was originally true, but the current formulation goes beyond the 2011 paper in some respects. See section 7.1 of <a href="https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf" target="_blank">https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf</a>.</div><div><br></div><div>Roman writes:</div><div><br></div><div>> <span style="font-family:Menlo-Regular;font-size:11px">I think it's important we keep the definitions of Functor and other</span></div><span style="font-family:Menlo-Regular;font-size:11px">fundamental classes understandable by newcomers, and this change would</span><br style="font-family:Menlo-Regular;font-size:11px"><span style="font-family:Menlo-Regular;font-size:11px">make the definition look scary for a marginal benefit.</span><div><span style="font-family:Menlo-Regular;font-size:11px"><br></span></div><div><span style="font-family:Menlo-Regular;font-size:11px">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)</span></div><div><span style="font-family:Menlo-Regular;font-size:11px"><br></span></div><div><span style="font-family:Menlo-Regular;font-size:11px">> type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)</span></div><div><span style="font-family:Menlo-Regular;font-size:11px"><br></span></div><div><span style="font-family:Menlo-Regular;font-size:11px">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.</span></div></div><div style="word-wrap:break-word;line-break:after-white-space"><div><span style="font-family:Menlo-Regular;font-size:11px"><br></span></div><div><span style="font-family:Menlo-Regular;font-size:11px">Richard</span></div></div></blockquote></div></div>