{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE ConstraintKinds #-}
module Data.Profunctor.Phantom where

import Data.Profunctor
import qualified Data.Functor.Contravariant as C
import Data.Profunctor.Cayley

-- Once we have ImpredicativeTypes we can do this, which is nice :)
-- import Data.Void
-- type Phantom p = (forall q. C.Contravariant (p q), Profunctor p)
-- phantom :: (forall q. C.Contravariant (p q), Profunctor p) => p a x -> p a y
-- phantom = rmap absurd . C.contramap absurd

class Profunctor p => Phantom p where
    phantom :: p a x -> p a y

instance Phantom (Forget r) where
  phantom :: Forget r a x -> Forget r a y
phantom (Forget f :: a -> r
f) = (a -> r) -> Forget r a y
forall r a b. (a -> r) -> Forget r a b
Forget a -> r
f

instance (Functor f, C.Contravariant f) => Phantom (Star f) where
  phantom :: Star f a x -> Star f a y
phantom (Star f :: a -> f x
f) = (a -> f y) -> Star f a y
forall (f :: * -> *) d c. (d -> f c) -> Star f d c
Star (f x -> f y
forall (f :: * -> *) a b.
(Functor f, Contravariant f) =>
f a -> f b
C.phantom (f x -> f y) -> (a -> f x) -> a -> f y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f x
f)

instance (Functor f, Phantom p) => Phantom (Cayley f p) where
  phantom :: Cayley f p a x -> Cayley f p a y
phantom (Cayley fpab :: f (p a x)
fpab) = f (p a y) -> Cayley f p a y
forall (f :: * -> *) (p :: * -> * -> *) a b.
f (p a b) -> Cayley f p a b
Cayley ((p a x -> p a y) -> f (p a x) -> f (p a y)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p a x -> p a y
forall (p :: * -> * -> *) a x y. Phantom p => p a x -> p a y
phantom f (p a x)
fpab)