Is it possible to implement Data.Reflection’s trick using type families instead of fundeps?

Question

The GHC implementation of Data.Reflection from the reflection package uses a trick involving unsafeCoerce that takes advantage of the way GHC compiles typeclasses using dictionary passing. The implementation is short, so I can reproduce it in its entirety here:

class Reifies s a | s -> a where
  reflect :: proxy s -> a

newtype Magic a r = Magic (forall (s :: *). Reifies s a => Proxy s -> r)

reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy

This makes it possible to reify a value at the type level, then reflect it back:

ghci> reify (42 :: Integer) (\p -> reflect p) :: Integer
42

I was interested in using this technique, but I thought it would be convenient for my purposes to use a type family with Reifies rather than a functional dependency, so I attempted to rewrite the implementation using the usual transformation:

class Reifies s where
  type Reflects s
  reflect :: Proxy s -> Reflects s

newtype Magic a r = Magic (forall (s :: *). (Reifies s, Reflects s ~ a) => Proxy s -> r)

reify :: forall a r. a -> (forall (s :: *). (Reifies s, Reflects s ~ a) => Proxy s -> r) -> r
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy

Sadly, however, this no longer works! This changes compilation significantly enough to break the unsafeCoerce trick:

ghci> reify (42 :: Integer) (\p -> reflect p) :: Integer
2199023255808

However, I’m not familiar enough with how GHC works to understand why. Is it possible to implement Data.Reflection using an associated type instead of a functional dependency? If so, what needs to change? If not, why not?

Answer 1

The unsafeCoerce trick takes advantage of the fact that

Reifies s a => Proxy s -> r

has exactly the same representation, at run-time, as

a -> Proxy s -> r

By enlarging the constraint to (Reifies s a, a ~ Reflects s), you violate this critical assumption. There are several ways to fix this. Here's one:

{-# language MultiParamTypeClasses, TypeFamilies, PolyKinds, KindSignatures,
       RankNTypes, ScopedTypeVariables, TypeOperators #-}
module TFReifies where
import Data.Proxy
import Unsafe.Coerce
import Data.Type.Equality

class Reifies s a where
  type Reflects s :: *
  reflect' :: proxy s -> a

reflect :: (Reifies s a, a ~ Reflects s) => proxy s -> a
reflect = reflect'


newtype Magic a r = Magic (forall (s :: *). (Reifies s a) => Proxy s -> r)

reify' :: forall a r. a -> (forall (s :: *). (Reifies s a) => Proxy s -> r) -> r
reify' a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy

reify :: forall a r. a -> (forall (s :: *). (Reifies s a, a ~ Reflects s) => Proxy s -> r) -> r
reify a f = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> f p)

---

Here's a version closer to yours:

class Reifies s where
  type Reflects s :: *
  reflect :: proxy s -> Reflects s

newtype Magic a r = Magic (forall (s :: *). (Reifies s) => Proxy s -> r)

reify :: forall a r. a -> (forall (s :: *). (Reifies s, a ~ Reflects s) => Proxy s -> r) -> r
reify a f = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> f p)
  where
    -- This function is totally bogus in other contexts, so we hide it.
    reify' :: forall a r. a -> (forall (s :: *). (Reifies s) => Proxy s -> r) -> r
    reify' a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy