ExistentialGhosts.hs

{-# language
  ExistentialQuantification,
  MultiParamTypeClasses,
  FunctionalDependencies,
  FlexibleInstances,
  TypeOperators,
  RankNTypes
#-}

module ExistentialGhosts where

newtype (~~) a name = Named a

class The d a | d -> a where
  the :: d -> a

instance The (a ~~ name) a where
  the (Named a) = a

f :: (Bool ~~ name) -> (Bool ~~ name) -> Bool
f = const (not . the)

--

name1 :: a -> (forall name. (a ~~ name) -> t) -> t
name1 x k = k (Named x)

test1 :: Bool
test1 =
  name1
    False
    (\b1 ->
      name1
        False
        (\b2 ->
          f b1 b2
        )
    )

--

data ContainerOfNamed a = forall name. ContainerOfNamed (a ~~ name)

name2 :: a -> ContainerOfNamed a
name2 x = name1 x ContainerOfNamed

test2 :: Bool
test2 =
  case name2 False of
    ContainerOfNamed b1 ->
      case name2 False of
        ContainerOfNamed b2 -> f b1 b2

--

main :: IO ()
main = pure ()