{-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}
{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE PolyKinds #-}
#endif
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Safe #-}
#endif
{-# LANGUAGE ScopedTypeVariables #-}

module Data.GADT.Compare
    ( module Data.GADT.Compare
#if MIN_VERSION_base(4,7,0)
    , (:~:)(Refl)
#endif
    ) where

import Data.Maybe
import Data.GADT.Show
import Data.Typeable

#if MIN_VERSION_base(4,7,0)
-- |Backwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`.
type (:=) = (:~:)

#else

-- |A GADT witnessing equality of two types.  Its only inhabitant is 'Refl'.
data a := b where
    Refl :: a := a
    deriving Typeable

instance Eq (a := b) where
    Refl == Refl = True

instance Ord (a := b) where
    compare Refl Refl = EQ

instance Show (a := b) where
    showsPrec _ Refl = showString "Refl"

instance Read (a := a) where
    readsPrec _ s = case con of
        "Refl"  -> [(Refl, rest)]
        _       -> []
        where (con,rest) = splitAt 4 s

#endif

instance GShow ((:=) a) where
    gshowsPrec :: Int -> (a := a) -> ShowS
gshowsPrec _ Refl = String -> ShowS
showString "Refl"

instance GRead ((:=) a) where
    greadsPrec :: Int -> GReadS ((:=) a)
greadsPrec p :: Int
p s :: String
s = Int -> ReadS (a := a)
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
s [(a := a, String)]
-> ((a := a, String) -> [(GReadResult ((:=) a), String)])
-> [(GReadResult ((:=) a), String)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a := a, String) -> [(GReadResult ((:=) a), String)]
forall k (x :: k).
(x := x, String) -> [(GReadResult ((:=) x), String)]
f
        where
            f :: forall x. (x := x, String) -> [(GReadResult ((:=) x), String)]
            f :: (x := x, String) -> [(GReadResult ((:=) x), String)]
f (Refl, rest :: String
rest) = (GReadResult ((:=) x), String) -> [(GReadResult ((:=) x), String)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((forall b. (forall (a :: k). (x := a) -> b) -> b)
-> GReadResult ((:=) x)
forall k (t :: k -> *).
(forall b. (forall (a :: k). t a -> b) -> b) -> GReadResult t
GReadResult (\x :: forall (a :: k). (x := a) -> b
x -> (x := x) -> b
forall (a :: k). (x := a) -> b
x x := x
forall k (a :: k). a :~: a
Refl) , String
rest)

-- |A class for type-contexts which contain enough information
-- to (at least in some cases) decide the equality of types 
-- occurring within them.
class GEq f where
    -- |Produce a witness of type-equality, if one exists.
    -- 
    -- A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:
    -- 
    -- > extract :: GEq tag => tag a -> DSum tag -> Maybe a
    -- > extract t1 (t2 :=> x) = do
    -- >     Refl <- geq t1 t2
    -- >     return x
    -- 
    -- Or in a list comprehension:
    -- 
    -- > extractMany :: GEq tag => tag a -> [DSum tag] -> [a]
    -- > extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]
    --
    -- (Making use of the 'DSum' type from "Data.Dependent.Sum" in both examples)
    geq :: f a -> f b -> Maybe (a := b)

-- |If 'f' has a 'GEq' instance, this function makes a suitable default 
-- implementation of '(==)'.
defaultEq :: GEq f => f a -> f b -> Bool
defaultEq :: f a -> f b -> Bool
defaultEq x :: f a
x y :: f b
y = Maybe (a := b) -> Bool
forall a. Maybe a -> Bool
isJust (f a -> f b -> Maybe (a := b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a := b)
geq f a
x f b
y)

-- |If 'f' has a 'GEq' instance, this function makes a suitable default 
-- implementation of '(/=)'.
defaultNeq :: GEq f => f a -> f b -> Bool
defaultNeq :: f a -> f b -> Bool
defaultNeq x :: f a
x y :: f b
y = Maybe (a := b) -> Bool
forall a. Maybe a -> Bool
isNothing (f a -> f b -> Maybe (a := b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a := b)
geq f a
x f b
y)

instance GEq ((:=) a) where
    geq :: (a := a) -> (a := b) -> Maybe (a := b)
geq (a := a
Refl :: a := b) (a := b
Refl :: a := c) = (a := b) -> Maybe (a := b)
forall a. a -> Maybe a
Just (a := b
forall k (a :: k). a :~: a
Refl :: b := c)

-- This instance seems nice, but it's simply not right:
-- 
-- > instance GEq StableName where
-- >     geq sn1 sn2
-- >         | sn1 == unsafeCoerce sn2
-- >             = Just (unsafeCoerce Refl)
-- >         | otherwise     = Nothing
-- 
-- Proof:
-- 
-- > x <- makeStableName id :: IO (StableName (Int -> Int))
-- > y <- makeStableName id :: IO (StableName ((Int -> Int) -> Int -> Int))
-- > 
-- > let Just boom = geq x y
-- > let coerce :: (a := b) -> a -> b; coerce Refl = id
-- > 
-- > coerce boom (const 0) id 0
-- > let "Illegal Instruction" = "QED."
-- 
-- The core of the problem is that 'makeStableName' only knows the closure
-- it is passed to, not any type information.  Together with the fact that
-- the same closure has the same StableName each time 'makeStableName' is 
-- called on it, there is serious potential for abuse when a closure can 
-- be given many incompatible types.


-- |A type for the result of comparing GADT constructors; the type parameters
-- of the GADT values being compared are included so that in the case where 
-- they are equal their parameter types can be unified.
data GOrdering a b where
    GLT :: GOrdering a b
    GEQ :: GOrdering t t
    GGT :: GOrdering a b
    deriving Typeable

-- |TODO: Think of a better name
--
-- This operation forgets the phantom types of a 'GOrdering' value.
weakenOrdering :: GOrdering a b -> Ordering
weakenOrdering :: GOrdering a b -> Ordering
weakenOrdering GLT = Ordering
LT
weakenOrdering GEQ = Ordering
EQ
weakenOrdering GGT = Ordering
GT

instance Eq (GOrdering a b) where
    x :: GOrdering a b
x == :: GOrdering a b -> GOrdering a b -> Bool
== y :: GOrdering a b
y =
        GOrdering a b -> Ordering
forall k (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== GOrdering a b -> Ordering
forall k (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
y

instance Ord (GOrdering a b) where
    compare :: GOrdering a b -> GOrdering a b -> Ordering
compare x :: GOrdering a b
x y :: GOrdering a b
y = Ordering -> Ordering -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (GOrdering a b -> Ordering
forall k (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
x) (GOrdering a b -> Ordering
forall k (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
y)

instance Show (GOrdering a b) where
    showsPrec :: Int -> GOrdering a b -> ShowS
showsPrec _ GGT = String -> ShowS
showString "GGT"
    showsPrec _ GEQ = String -> ShowS
showString "GEQ"
    showsPrec _ GLT = String -> ShowS
showString "GLT"

instance GShow (GOrdering a) where
    gshowsPrec :: Int -> GOrdering a a -> ShowS
gshowsPrec = Int -> GOrdering a a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance GRead (GOrdering a) where
    greadsPrec :: Int -> GReadS (GOrdering a)
greadsPrec _ s :: String
s = case String
con of
        "GGT"   -> [((forall b. (forall (a :: k). GOrdering a a -> b) -> b)
-> GReadResult (GOrdering a)
forall k (t :: k -> *).
(forall b. (forall (a :: k). t a -> b) -> b) -> GReadResult t
GReadResult (\x :: forall (a :: k). GOrdering a a -> b
x -> GOrdering a Any -> b
forall (a :: k). GOrdering a a -> b
x GOrdering a Any
forall k (a :: k) (b :: k). GOrdering a b
GGT), String
rest)]
        "GEQ"   -> [((forall b. (forall (a :: k). GOrdering a a -> b) -> b)
-> GReadResult (GOrdering a)
forall k (t :: k -> *).
(forall b. (forall (a :: k). t a -> b) -> b) -> GReadResult t
GReadResult (\x :: forall (a :: k). GOrdering a a -> b
x -> GOrdering a a -> b
forall (a :: k). GOrdering a a -> b
x GOrdering a a
forall k (t :: k). GOrdering t t
GEQ), String
rest)]
        "GLT"   -> [((forall b. (forall (a :: k). GOrdering a a -> b) -> b)
-> GReadResult (GOrdering a)
forall k (t :: k -> *).
(forall b. (forall (a :: k). t a -> b) -> b) -> GReadResult t
GReadResult (\x :: forall (a :: k). GOrdering a a -> b
x -> GOrdering a Any -> b
forall (a :: k). GOrdering a a -> b
x GOrdering a Any
forall k (a :: k) (b :: k). GOrdering a b
GLT), String
rest)]
        _       -> []
        where (con :: String
con, rest :: String
rest) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt 3 String
s

-- |Type class for comparable GADT-like structures.  When 2 things are equal,
-- must return a witness that their parameter types are equal as well ('GEQ').
class GEq f => GCompare f where
    gcompare :: f a -> f b -> GOrdering a b

instance GCompare ((:=) a) where
    gcompare :: (a := a) -> (a := b) -> GOrdering a b
gcompare Refl Refl = GOrdering a b
forall k (t :: k). GOrdering t t
GEQ

defaultCompare :: GCompare f => f a -> f b -> Ordering
defaultCompare :: f a -> f b -> Ordering
defaultCompare x :: f a
x y :: f b
y = GOrdering a b -> Ordering
forall k (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering (f a -> f b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare f a
x f b
y)