It strikes me as vaguely likely that something more like this formulation could have some efficiency advantages in some cases, as is usual for Tagged vs. Proxy based things of all sorts.
class Reifies s a | s -> a where
reflect2 :: Tagged s a
newtype Magic a r = Magic (forall (s :: *) . Reifies s a => Tagged s r)
-- I flipped this for minimalism; I don't really know how that affects efficiency.
reify2 :: forall a r . (forall (s :: *) . Reifies s a => Tagged s r) -> a -> r
reify2 k = unsafeCoerce (Magic k :: Magic a r)
{-# INLINE reify2 #-}
-- The usual interface can be implemented thus:
reflect :: forall s a proxy . Reifies s a => proxy s -> a
reflect _ = unTagged (reflect2 :: Tagged s a)
{-# INLINE reflect #-}
reify :: forall a r . a -> (forall (s :: *) . Reifies s a => Proxy s -> r) -> r
reify a k = reify2 tagged a
where
tagged :: forall (s :: *) . Reifies s a => Tagged s r
tagged = Tagged (k (Proxy :: Proxy s))
{-# INLINE reify #-}
It strikes me as vaguely likely that something more like this formulation could have some efficiency advantages in some cases, as is usual for
Taggedvs.Proxybased things of all sorts.