<div dir="ltr">Ah yes, I believe you're referring to <a href="https://ghc.haskell.org/trac/ghc/ticket/8767" target="_blank">https://ghc.haskell.org/<wbr>trac/ghc/ticket/8767</a> (which I wasn't aware of). And yes, I do believe we'd need some combination of QuantifiedContexts/ImplicationConstraints to fully support everything.<div><br></div><div>But in any case, don't let this discussion side-track too much from the matter at hand (the type family compilation slowdown). My suggestion _was_ somewhat tongue-in-cheek, after all ;)</div><div><br></div><div>Ryan S.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 6, 2017 at 11:01 AM, David Feuer <span dir="ltr"><<a href="mailto:david@well-typed.com" target="_blank">david@well-typed.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div>Edward Kmett has explained that this isn't sufficient when things go higher order. His suggested improvement is</div><div><br></div><div>    liftCoercion :: Maybe (Coercion a b -> Coercion (f a) (f b))</div><span class="HOEnZb"><font color="#888888"><div><br></div><div><br></div><div><br></div><div id="m_-7045578596595729607composer_signature"><div style="font-size:85%;color:#575757">David Feuer</div><div style="font-size:85%;color:#575757">Well-Typed, LLP</div></div></font></span><div><div class="h5"><div><br></div><div style="font-size:100%;color:#000000"><div>-------- Original message --------</div><div>From: Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com" target="_blank">ryan.gl.scott@gmail.com</a>> </div><div>Date: 6/6/17  1:41 PM  (GMT-05:00) </div><div>To: Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>> </div><div>Cc: GHC developers <<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a>>, Eric Mertens <<a href="mailto:emertens@gmail.com" target="_blank">emertens@gmail.com</a>> </div><div>Subject: Re: Hunting down a compilation performance regression involving type families </div><div><br></div></div>Hrm. It's a shame that supporting this map/coerce RULE causes such pain.<br><br>This makes me wonder: can we get rid of this RULE? Eric Mertens pointed out<br>a trick [1] that's used in the profunctors library to make mapping coerce<br>over certain Profunctors more efficient. To adapt this trick for Functor,<br>we'd need to add another class method:<br><br>    class Functor f where<br>        fmap :: (a -> b) -> f a -> f b<br>        (<#>) :: Coercible a b => (a -> b) -> f a -> f b<br>        (<#>) = \f -> \p -> p `seq` fmap f p<br><br>Now, when implementing Functor instances, if we are working with a datatype<br>whose role is representational or phantom, we can make (<#>) really fast:<br><br>    data List a = Nil | Cons a (List a)<br>    instance Functor List where<br>        fmap = ...<br>        (<#>) = coerce<br><br>Now, instead of relying on (map MkNewtype Nil) to rewrite to Nil, we can<br>just use (MkNewtype <#> Nil)! No map/coerce RULE necessary :)<br><br>OK, I realize that suggesting that we remove the RULE is perhaps a touch<br>too far. But it does sting that we have to pay hefty compilation penalties<br>because of its existence...<br><br>Ryan S.<br>-----<br>[1]<br><a href="http://hackage.haskell.org/package/profunctors-5.2/docs/Data-Profunctor-Unsafe.html#v:-35-" target="_blank">http://hackage.haskell.org/<wbr>package/profunctors-5.2/docs/<wbr>Data-Profunctor-Unsafe.html#v:<wbr>-35-</a><br>.<br><br>On Wed, May 31, 2017 at 7:25 PM, Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>><br>wrote:<br><br>><br>> > On May 31, 2017, at 5:21 PM, Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com" target="_blank">ryan.gl.scott@gmail.com</a>> wrote:<br>> > Does you know what might be going on here?<br>><br>> I think so, but I don't know how to fix it.<br>><br>> The commit you found (thank you!) makes simple_opt_expr (the "simple<br>> optimizer", run directly after desugaring, even with -O0) a little more<br>> selective in what `case` expressions it throws away. Previous to that<br>> commit, the optimizer would throw away a `case error "deferred type error"<br>> of _ -> ...` which is terrible. It seems that you have discovered that we<br>> are now too timid in throwing away unhelpful cases. It would be interesting<br>> to know what the newly-retained cases look like, so that we might throw<br>> them away.<br>><br>> But there remains a mystery: Why do we need this code at all? Reading Note<br>> [Getting the map/coerce RULE to work] closely, it seems we need to simplify<br>><br>>   forall a b (co :: a ~R# b).<br>>     let dict = MkCoercible @* @a @b co in<br>>     case Coercible_SCSel @* @a @b dict of<br>>       _ [Dead] -> map @a @b (\(x :: a) -> case dict of<br>>          MkCoercible (co :: a ~R# b) -> x |> co) = let dict = ... in ...<br>><br>> to<br>><br>>   forall a b (co :: a ~R# b).<br>>     map @a @b (\(x :: a) -> x |> co) = \(x :: [a]) -> x |> [co]<br>><br>> Part of doing so is to drop the `case Coercible_SCSel ...`, which gets in<br>> the way. The mystery is why this needs special code -- shouldn't the<br>> eliminate-case-of-known-<wbr>constructor do the trick? This would require<br>> unfolding Coercible_SCSel. Does that happen? It would seem not... but maybe<br>> it should, which would remove the special-case code that I changed in that<br>> commit, and quite likely would simplify much more code besides.<br>><br>> So: Is Coercible_SCSel unfolded during simple_opt? If not, what wonderful<br>> or terrible things happen if we do? If so, why does<br>> case-of-known-constructor not work here? My guess is that answering these<br>> questions may solve the original problem, but this guess could be wrong.<br>><br>> Richard<br>><br>><br></div></div></div></blockquote></div><br></div>