Pattern for existential types with typeclass constraints

MyExistsConstrained.purs

module Data.MyExistsConstrained where

import Prelude
import Unsafe.Coerce (unsafeCoerce)

-- Suppose you want to use an existentially-quantified type. You can use the
-- `exists` package, which defines `Exists` likes so:

foreign import data Exists :: (Type -> Type) -> Type

mkExists :: forall f a. f a -> Exists f
mkExists = unsafeCoerce

runExists :: forall f r. (forall a. f a -> r) -> Exists f -> r
runExists = unsafeCoerce

-- But, what if you want to _constrain_ the existentially quantified type with a
-- typeclass constraint? It turns out, naively defining your own version of
-- `Exists` with the constraint wedged in there won't work. Here's a pattern
-- that does work:

newtype ExistsShow = ExistsShow (forall r. ExistsShowK r -> r)
type ExistsShowK r = forall a. Show a => a -> r

mkExistsShow :: ExistsShowK ExistsShow
mkExistsShow a = ExistsShow \k -> k a

runExistsShow :: forall r. ExistsShowK r -> ExistsShow -> r
runExistsShow k1 (ExistsShow k2) = k2 k1

-- The generic form of this pattern is as follows, where `MyConstraint` is any
-- constraints.

class MyConstraint :: forall k. k -> Constraint
class MyConstraint a

newtype MyExistsConstrained = MyExistsConstrained (forall r. MyExistsConstrainedK r -> r)
type MyExistsConstrainedK r = forall a. MyConstraint a => a -> r

mkMyExistsConstrained :: MyExistsConstrainedK MyExistsConstrained
mkMyExistsConstrained a = MyExistsConstrained \k -> k a

runMyExistsConstrained :: forall r. MyExistsConstrainedK r -> MyExistsConstrained -> r
runMyExistsConstrained k1 (MyExistsConstrained k2) = k2 k1

-- Note that you can modify the definition of `MyExistsConstrainedK` to make
-- `MyExistsConstrained` existentially quantify any number of types of any kinds
-- with any number of type constraints (you will just have to handle the
-- quantified types as new parameters of `mkMyExistsConstrained`). For example:

newtype ExistsShowEqOrd2 = ExistsShowEqOrd2 (forall r. ExistsShowEqOrd2K r -> r)
type ExistsShowEqOrd2K r = forall a b. Show a => Eq a => Ord a => Show b => Eq b => Ord b => a -> b -> r

mkExistsShowEqOrd2 :: ExistsShowEqOrd2K ExistsShowEqOrd2
mkExistsShowEqOrd2 a b = ExistsShowEqOrd2 \k -> k a b

runExistsShowEqOrd2 :: forall r. ExistsShowEqOrd2K r -> ExistsShowEqOrd2 -> r
runExistsShowEqOrd2 k1 (ExistsShowEqOrd2 k2) = k2 k1