Phantom equality. You know, for all those situations where you need it...

Phantom.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
-- | When your idea isn't even good enough for an @acme@ package...
module Data.Type.Phantom where

import Control.Category (Category(..))
import Data.Kind
import Data.Proxy
import Data.Type.Coercion (Coercion)
import Data.Type.Equality ((:~:), (:~~:))
import Type.Reflection (TypeRep)

-- | Phantom equality, the broadest notion of equality in GHC.
class Phantom (a :: j) (b :: k)
-- | Any two types are phantom equal. Any. Two. Types.
instance Phantom a b

-- | A witness for phantom equality. Named after the sound one might make after
-- one sees a phantom.
data Zoinks :: forall j k. j -> k -> Type where
  Zoinks :: Phantom a b => Zoinks a b

deriving instance Bounded (Zoinks a b)
deriving instance Eq      (Zoinks a b)
deriving instance Ord     (Zoinks a b)
deriving instance Read    (Zoinks a b)
deriving instance Show    (Zoinks a b)

instance Enum (Zoinks a b) where
  toEnum 0 = Zoinks
  toEnum _ = errorWithoutStackTrace "Zoinks.toEnum: bad argument"

  fromEnum _ = 0

instance Category Zoinks where
  id    = Zoinks
  _ . _ = Zoinks

-- | What can you do with phantom equality?
-- Well, you can, er, \"cast\" with it...
zoinksWith :: Zoinks a b -> Proxy a -> Proxy b
zoinksWith _ _ = Proxy

-- | Generalized form of type-safe cast using phantom equality.
gzoinksWith :: Zoinks a b -> (Phantom a b => r) -> r
gzoinksWith _ r = r

-- | Symmetry of phantom equality.
sym :: Zoinks a b -> Zoinks b a
sym _ = Zoinks

-- | Transitivity of phantom equality.
trans :: Zoinks a b -> Zoinks b c -> Zoinks a c
trans _ _ = Zoinks

-- | Apply one equality to another, respectively.
apply :: Zoinks f g -> Zoinks a b -> Zoinks (f a) (g b)
apply _ _ = Zoinks

-- | Extract equality of the arguments from an equality of applied types.
inner :: Zoinks (f a) (g b) -> Zoinks a b
inner _ = Zoinks

-- | Extract equality of type constructors from an equality of applied types.
outer :: Zoinks (f a) (g b) -> Zoinks f g
outer _ = Zoinks

-- | Convert propositional, homogeneous, nominal equality to phantom equality.
fromEq :: a :~: b -> Zoinks a b
fromEq _ = Zoinks

-- | Convert propositional, heterogeneous, nominal equality to phantom equality.
fromHEq :: a :~~: b -> Zoinks a b
fromHEq _ = Zoinks

-- | Convert propositional, representational equality to phantom equality.
fromCoercion :: Coercion a b -> Zoinks a b
fromCoercion _ = Zoinks

-- | Test two things for phantom equality. Possibly even more useless than
-- 'Phantom', which is quite an accomplishment.
class TestPhantom f where
  testPhantom :: f a -> f b -> Maybe (Zoinks a b)
instance TestPhantom (Zoinks a) where
  testPhantom _ _ = Just Zoinks
instance TestPhantom ((:~:) a) where
  testPhantom _ _ = Just Zoinks
instance TestPhantom ((:~~:) a) where
  testPhantom _ _ = Just Zoinks
instance TestPhantom (Coercion a) where
  testPhantom _ _ = Just Zoinks
instance TestPhantom TypeRep where
  testPhantom _ _ = Just Zoinks