Edward Kmett has explained that this isn't sufficient when things go higher order. His suggested improvement is

liftCoercion :: Maybe (Coercion a b -> Coercion (f a) (f b))

David Feuer

Well-Typed, LLP

-------- Original message --------

From: Ryan Scott <ryan.gl.scott@gmail.com>

Date: 6/6/17 1:41 PM (GMT-05:00)

To: Richard Eisenberg <rae@cs.brynmawr.edu>

Cc: GHC developers <ghc-devs@haskell.org>, Eric Mertens <emertens@gmail.com>

Subject: Re: Hunting down a compilation performance regression involving type families

Hrm. It's a shame that supporting this map/coerce RULE causes such pain.

This makes me wonder: can we get rid of this RULE? Eric Mertens pointed out
a trick [1] that's used in the profunctors library to make mapping coerce
over certain Profunctors more efficient. To adapt this trick for Functor,
we'd need to add another class method:

    class Functor f where
        fmap :: (a -> b) -> f a -> f b
        (<#>) :: Coercible a b => (a -> b) -> f a -> f b
        (<#>) = \f -> \p -> p `seq` fmap f p

Now, when implementing Functor instances, if we are working with a datatype
whose role is representational or phantom, we can make (<#>) really fast:

    data List a = Nil | Cons a (List a)
    instance Functor List where
        fmap = ...
        (<#>) = coerce

Now, instead of relying on (map MkNewtype Nil) to rewrite to Nil, we can
just use (MkNewtype <#> Nil)! No map/coerce RULE necessary :)

OK, I realize that suggesting that we remove the RULE is perhaps a touch
too far. But it does sting that we have to pay hefty compilation penalties
because of its existence...

Ryan S.
-----
[1]
http://hackage.haskell.org/package/profunctors-5.2/docs/Data-Profunctor-Unsafe.html#v:-35-
.

On Wed, May 31, 2017 at 7:25 PM, Richard Eisenberg <rae@cs.brynmawr.edu>
wrote:

>
> > On May 31, 2017, at 5:21 PM, Ryan Scott <ryan.gl.scott@gmail.com> wrote:
> > Does you know what might be going on here?
>
> I think so, but I don't know how to fix it.
>
> The commit you found (thank you!) makes simple_opt_expr (the "simple
> optimizer", run directly after desugaring, even with -O0) a little more
> selective in what `case` expressions it throws away. Previous to that
> commit, the optimizer would throw away a `case error "deferred type error"
> of _ -> ...` which is terrible. It seems that you have discovered that we
> are now too timid in throwing away unhelpful cases. It would be interesting
> to know what the newly-retained cases look like, so that we might throw
> them away.
>
> But there remains a mystery: Why do we need this code at all? Reading Note
> [Getting the map/coerce RULE to work] closely, it seems we need to simplify
>
>   forall a b (co :: a ~R# b).
>     let dict = MkCoercible @* @a @b co in
>     case Coercible_SCSel @* @a @b dict of
>       _ [Dead] -> map @a @b (\(x :: a) -> case dict of
>          MkCoercible (co :: a ~R# b) -> x |> co) = let dict = ... in ...
>
> to
>
>   forall a b (co :: a ~R# b).
>     map @a @b (\(x :: a) -> x |> co) = \(x :: [a]) -> x |> [co]
>
> Part of doing so is to drop the `case Coercible_SCSel ...`, which gets in
> the way. The mystery is why this needs special code -- shouldn't the
> eliminate-case-of-known-constructor do the trick? This would require
> unfolding Coercible_SCSel. Does that happen? It would seem not... but maybe
> it should, which would remove the special-case code that I changed in that
> commit, and quite likely would simplify much more code besides.
>
> So: Is Coercible_SCSel unfolded during simple_opt? If not, what wonderful
> or terrible things happen if we do? If so, why does
> case-of-known-constructor not work here? My guess is that answering these
> questions may solve the original problem, but this guess could be wrong.
>
> Richard
>
>