{-# LANGUAGE ExistentialQuantification, RankNTypes, EmptyDataDecls #-}

-- Experiments with interchangeability of variously quantified types.
module E where

data E p = forall a. E (p a)

data E' p t = forall a. E' (p a -> t)

data E'' t p = forall a. E'' (t -> p a)

-- fail: a doesn't match a1
-- (exists a. p a -> t) -> (exists a. p a) -> t
-- e1 :: E' p t -> (E p -> t)
-- e1 (E' f) (E pa) = f pa

-- works
-- ((exists a. p a) -> t) -> (exists a. p a -> t)
e2 :: (E p -> t) -> E' p t
e2 f = E' (\pa -> f (E pa))

-- works
-- ((exists a. p a) -> t) <-> (forall a. p a -> t)
e3 :: (E p -> t) -> (forall a. p a -> t)
e3 f = \pa -> f (E pa)

e4 :: (forall a. p a -> t) -> (E p -> t)
e4 f (E pa) = f pa

-- fail: inferred type less polymorphic than expected
-- ((forall a. p a) -> t) -> (exists a. p a -> t)
-- e5 :: ((forall a. p a) -> t) -> E' p t
-- e5 f = E' (\pa -> f pa)

-- works
-- (exists a. p a -> t) -> ((forall a. p a) -> t)
e6 :: E' p t -> (forall a. p a) -> t
e6 (E' f) pa = f pa

-- fail: a doesn't match a1
-- ((forall a. p a) -> t) -> ((exists a. p a) -> t)
-- e7 :: ((forall a. p a) -> t) -> (E p -> t)
-- e7 f (E pa) = f pa

-- works, of course
-- ((exists a. p a) -> t) -> ((forall a. p a) -> t)
e8 :: (E p -> t) -> ((forall a. p a) -> t)
e8 f pa = f (E pa)
-- e8 f = e6 (e2 f)
-- e8 f = e9 (e3 f)

-- works
e9 :: (forall a. p a -> t) -> ((forall a. p a) -> t)
e9 f pa = f pa

-- fail: a1 does not match a
-- e10 :: ((forall a. p a) -> t) -> (forall a. p a -> t)
-- e10 f pa = f pa

-- fail: inferred type less polymorphic than expected
-- This seems like it could perhaps work, since E''
-- re-hides the 'a' but it doesn't, probably because there's
-- no way to type the enclosed lambda expression properly.
-- (t -> (exists a. p a)) -> (exists a. t -> p a)
--
-- as it turns out, this really shouldn't work, because
-- the former may produce values with a different a dependent
-- on t, whereas the latter is stuck with a uniform a for all
-- ts.
-- e11 :: (t -> E p) -> E'' t p
-- e11 f = E'' (\t -> case f t of E pa -> pa)

-- works
-- (exists a. t -> p a) -> (t -> (exists a. p a))
e12 :: E'' t p -> (t -> E p)
e12 (E'' f) t = E (f t)

-- works
e13 :: (forall a. t -> p a) -> (t -> (forall a. p a))
e13 f t = f t

-- works
e14 :: (t -> (forall a. p a)) -> (forall a. t -> p a)
e14 f t = f t

data Void

-- works
-- (exists a. p a) -> (not (forall a. not (p a)))
-- e15 :: E p -> (forall r. (forall a. p a -> r) -> r)
e15 :: E p -> (forall a. p a -> Void) -> Void
e15 (E pa) k = k pa


-- (not (forall a. not (p a))) -> exists a. p a
-- e16 :: (forall r. (forall a. p a -> r) -> r) -> E p -- works here
-- e16 :: ((forall a. p a -> Void) -> Void) -> E p -- fails here E p /= Void
-- e16 f = f E

-- works
-- (forall a. p a) -> (not (exists a. not (p a)))
-- e17 :: (forall a. p a) -> (forall r. E' p r -> r)
e17 :: (forall a. p a) -> (E' p Void -> Void)
e17 pa (E' f) = f pa

-- (not (exists a. not (p a))) -> (forall a. p a)
-- e18 :: (forall r. E' p r -> r) -> (forall a. p a) -- works
-- e18 :: (E' p Void -> Void) -> (forall a. p a) -- fail: Void /= p a
-- e18 f = f (E' id)

-- be careful about how you encode your negation, I guess. :)

-- works
-- (exists a. not (p a)) -> not (forall a. p a)
e19 :: (E' p Void) -> (forall a. p a) -> Void
e19 (E' f) pa = f pa

-- works
-- (forall a. not (p a)) -> not (exists a. p a)
e20 :: (forall a. p a -> Void) -> E p -> Void
e20 f (E pa) = f pa

-- works
-- (not (exists a. p a)) -> (forall a. not (p a))
e21 :: (E p -> Void) -> (forall a. p a -> Void)
e21 f pa = f (E pa)