The following snippet of code borrows from the Haskell wiki to carry around a typeclass dictionary along with an existential type:
{-# language ExistentialQuantification #-}
module Experiment1 where
data Showable = forall x. Show x => Showable x
instance Show Showable where showsPrec p (Showable x) = showsPrec p x
resultStr :: String
resultStr = show (Showable ()) -- "()"
Is it possible to write a function f :: (forall x. x -> result) -> result that is able to take the Showable constructor (or any other data constructor to an existential type) as an argument?
One failed attempt at doing this looks like this:
{-# language ExistentialQuantification, RankNTypes, ConstraintKinds #-}
module Experiment2 where
-- import Data.Constraint (Dict(..), withDict)
data Showable = forall x. Show x => Showable x
instance Show Showable where showsPrec p (Showable x) = showsPrec p x
f :: (cxt (), cxt result) => (forall x. cxt x => x -> result) -> result
f mkResult = mkResult ()
resultStr :: String
resultStr = show (f Showable)
As implied by my commented import above, I have the impression that the constraints package might allow me to pass around the necessary proofs, but I can't see how that would work?
Your failed attempt works if you provide a way to determine cxt
import Data.Proxy
f :: (cxt (), cxt result) => p cxt -> (forall x. cxt x => x -> result) -> result
f _ mkResult = mkResult ()
resultStr :: String
resultStr = show (f (Proxy :: Proxy Show) Showable)