Magical function to support reflection

[David Feuer]

The following proposal (with fancier formatting and some improved
wording) can be viewed at
https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport

Using the Data.Reflection has some runtime costs. Notably, there can
be no inlining or unboxing of reified values. I think it would be nice
to add a GHC special to support it. I'll get right to the point of
what I want, and then give a bit of background about why.

=== What I want

I propose the following absurdly over-general lie:

reify# :: (forall s . c s a => t s r) -> a -> r

`c` is assumed to be a single-method class with no superclasses whose
dictionary representation is exactly the same as the representation of
`a`, and `t s r` is assumed to be a newtype wrapper around `r`. In
desugaring, reify# f would be compiled to f at S, where S is a fresh
type. I believe it's necessary to use a fresh type to prevent
specialization from mixing up different reified values.

=== Background

Let me set up a few pieces. These pieces are slightly modified from
what the package actually does to make things cleaner under the hood,
but the differences are fairly shallow.

newtype Tagged s a = Tagged { unTagged :: a }

unproxy :: (Proxy s -> a) -> Tagged s a
unproxy f = Tagged (f Proxy)

class Reifies s a | s -> a where
  reflect' :: Tagged s a

-- For convenience
reflect :: forall s a proxy . Reifies s a => proxy s -> a
reflect _ = unTagged (reflect' :: Tagged s a)

-- The key function--see below regarding implementation
reify' :: (forall s . Reifies s a => Tagged s r) -> a -> r

-- For convenience
reify :: a -> (forall s . Reifies s a => Proxy s -> r) -> r
reify a f = reify' (unproxy f) a

The key idea of reify' is that something of type

forall s . Reifies s a => Tagged s r

is represented in memory exactly the same as a function of type

a -> r

So we can currently use unsafeCoerce to interpret one as the other.
Following the general approach of the library, we can do this as such:

newtype Magic a r = Magic (forall s . Reifies s a => Tagged s r)
reify' :: (forall s . Reifies s a => Tagged s r) -> a -> r
reify' f = unsafeCoerce (Magic f)

This certainly works. The trouble is that any knowledge about what is
reflected is totally lost. For instance, if I write

reify 12 $ \p -> reflect p + 3

then GHC will not see, at compile time, that the result is 15. If I write

reify (+1) $ \p -> reflect p x

then GHC will never inline the application of (+1). Etc.

I'd like to replace reify' with reify# to avoid this problem.

Thanks,
David Feuer