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.)

-Edward



On Sun, Dec 11, 2016 at 12:01 AM, David Feuer <david.feuer@gmail.com> wrote:
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