Extracting existential from proxy

Question

Is it possible to write extractT?

{-# LANGUAGE ExistentialQuantification #-}
import Data.Proxy

data T = forall t. Show t => T (Proxy t)

extractT :: Proxy T -> T
extractT p = ...

I have tried

extractT p = T $ p >>= \(T t) -> t

but it does not work.

Answer 1

No, it is not possible (aside from “trivial” implementations like this one by melpomene that ignore the argument entirely).

A value of type Proxy a carries no more information at runtime than () does, which is to say it doesn’t carry any information at all. This is true no matter what a is.

Your type T carries more information than just () at runtime: it carries a Show method dictionary for some type around with it. This dictionary isn’t very useful, since by the time the existential is unpacked, you don’t have any way to obtain a value of type t to use show on, but the information is technically there.

Since constructing a T requires supplying a typeclass dictionary, but the dictionary (nor any means to obtain it) does not exist inside Proxy T, and there is not any static information about which type the dictionary should be for, it is impossible to obtain the dictionary necessary to construct a T. Put another way, constructing a value of type Proxy T does not pick a t—there is no type “inside” the T in Proxy T—since Proxy only carries around type-level information, but the t inside the T type only exists at the value level.