Magical function to support reflection

Edward Kmett ekmett at
Mon Dec 12 18:15:46 UTC 2016

A few thoughts in no particular order:

Unlike this proposal, the existing 'reify' itself as core can actually be
made well typed.

Tagged in the example could be replaced with explicit type application if
backwards compatibility isn't a concern. OTOH, it is.

The form of reify' there is actually an uncomfortable middle ground between
the current implementation and perhaps the more "ghc-like" implementation
that uses a type family to determine 'a'. On the other hand, giving the
type above with the type family in it would be rather awkward, and
generalizing it further without it would make it even more brittle. On the
other other hand, if you're going to be magic, you might as well go all the
way to something like:

reify# :: (p => r) -> a -> r

and admit both fundep and TF forms. I mean, if you're going to lie you
might as well lie big. It'd be nice to show that this can be used to reify
KnownNat, Typeable, KnownSymbol, etc. and other commonly hacked
dictionaries as well as Reifies.

There are a very large number of instances out there scattered across
dozens of packages that would be broken by switching from Proxy to Tagged
or explicit type application internally. (I realize that this is a lesser
concern that can be resolved by a major version bump and some community
friction, but it does mean pragmatically that migrating to something like
this would need a plan.)


On Sun, Dec 11, 2016 at 12:01 AM, David Feuer <david.feuer at> wrote:

> 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.
> Thanks,
> David Feuer
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list