"unreify" combinator

[mitchellwrosen]

Hi, I'm playing around with reflection for the first time in some production code (eep) and I found a need for this function...

unreify :: forall a f r. (forall s. f s -> r) -> (forall s. Reifies s a => f s) -> r
unreify k x = reify (error "unreify: impossible?!" :: a) (\p -> k (x `asProxyOf` p))

asProxyOf :: f s -> Proxy s -> f s
asProxyOf x _ = x

My use-case is trying to Show a data type that looks like this:

data Foo = Foo (forall s. Reifies s Bar => What s)

instance Show (What s)  -- doesn't need a 'Reifies s Bar'

instance Show Foo where
  show (Foo x) = ???

In ???, I have an x :: Reifies s Bar => What s, and I thus I need to pick some s such that Reifies s Bar (i.e. reify a Bar), but I don't have a Bar around, and I also know that I don't need one to show a What s (because I can provide a forall s. What s -> String function - show!)

I was wondering if this combinator makes sense, not necessarily for the library proper, but more as some sort of proof by parametricity that the undefined can't possibly be forced.

Thanks!

[treeowl]

No, this does not seem to make sense. You don't need Reifies s Bar to show What s, but that doesn't mean the function of type forall s. Reifies s a => f s doesn't actually use the reified value to construct the What s.