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@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