Unpack Existentials in Existential Type

Question

I tried to write the following code:

{-# LANGUAGE GADTs #-}

module V where

data V a where
  V :: (c -> a) -> V a

down :: V (V a) -> V a
down (V f) = V $ \(c,d) -> case f c of
  V f' -> f' d

Then GHC answered type variable `c' would escape its scope.

I understand why it doesn't compile: it uses hidden type of existential out of case.

But actually the type is still hidden by V. so essentially function down has no problem I think.

Is there a way to write a compilable down function?

Answer 1

Here's the fundamental problem: f can have a peek at c and use the value of c to determine which type to hide in its existential. For example:

v :: V (V Int)
v = V $ \p -> case p of
     False -> V (id :: Int -> Int)
     True  -> V (fromEnum :: Char -> Int)

So d would need to be both a valid Int and a valid Char if we called down v! To be able to feed an existential that can be so variable, you'll need to ensure that its argument can take on all the types it may demand.

newtype Forall = Forall (forall a. a)

down :: V (V a) -> V a
down (V f) = V $ \(c, d_) -> case f c of
    V f' -> case d_ of
        Forall d -> f' d