Magical function to support reflection

David Feuer david.feuer at
Sun Dec 11 05:01:25 UTC 2016

The following proposal (with fancier formatting and some improved
wording) can be viewed at

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.

David Feuer

More information about the ghc-devs mailing list