<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jan 3, 2021, at 1:02 PM, Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" class="">carter.schonwald@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="caret-color: rgb(0, 0, 0); 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; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">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 class=""><div class="">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 class=""><br class=""></div><div class="">> i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper...</div><div class=""><br class=""></div><div class="">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" class="">https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf</a>.</div><div class=""><br class=""></div><div class="">Roman writes:</div><div class=""><br class=""></div><div class="">> <span style="font-family: Menlo-Regular; font-size: 11px;" class="">I think it's important we keep the definitions of Functor and other</span></div><span style="font-family: Menlo-Regular; font-size: 11px;" class="">fundamental classes understandable by newcomers, and this change would</span><br style="font-family: Menlo-Regular; font-size: 11px;" class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class="">make the definition look scary for a marginal benefit.</span><div class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class=""><br class=""></span></div><div class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class="">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 class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class=""><br class=""></span></div><div class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class="">> type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)</span></div><div class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class=""><br class=""></span></div><div class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class="">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 class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class=""><br class=""></span></div><div class=""><span style="font-family: Menlo-Regular; font-size: 11px;" class="">Richard</span></div></body></html>