    {-# LANGUAGE TypeOperators, DataKinds, PolyKinds, TypeFamilies,
                 RankNTypes, FlexibleContexts, TemplateHaskell,
                 UndecidableInstances, GADTs, DefaultSignatures,
                 ScopedTypeVariables, TypeApplications #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.Prelude.Eq
    -- Copyright   :  (C) 2013 Richard Eisenberg
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Defines the SEq singleton version of the Eq type class.
    --
    -----------------------------------------------------------------------------

    module Data.Singletons.Prelude.Eq (
      PEq(..), SEq(..),
      DefaultEq,

      -- * Defunctionalization symbols
      type (==@#@$), type (==@#@$$), type (==@#@$$$),
      type (/=@#@$), type (/=@#@$$), type (/=@#@$$$),
      DefaultEqSym0, DefaultEqSym1, DefaultEqSym2
      ) where

    import Data.Singletons.Internal
    import Data.Singletons.Prelude.Bool
    import Data.Singletons.Single
    import Data.Singletons.Prelude.Instances
    import Data.Singletons.Util
    import Data.Singletons.Promote
    import qualified Data.Type.Equality as DTE ()

    -- NB: These must be defined by hand because of the custom handling of the
    -- default for (==) to use DefaultEq

    -- | The promoted analogue of 'Eq'. If you supply no definition for '(==)',
    -- then it defaults to a use of 'DefaultEq'.
    class PEq a where
      type (==) (x :: a) (y :: a) :: Bool
      type (/=) (x :: a) (y :: a) :: Bool

      type (x :: a) == (y :: a) = x `DefaultEq` y
      type (x :: a) /= (y :: a) = Not (x == y)

      infix 4 ==
      infix 4 /=

    -- | A sensible way to compute Boolean equality for types of any kind. Note
    -- that this definition is slightly different from the '(DTE.==)' type family
    -- from "Data.Type.Equality" in @base@, as '(DTE.==)' attempts to distinguish
    -- applications of type constructors from other types. As a result,
    -- @a == a@ does not reduce to 'True' for every @a@, but @'DefaultEq' a a@
    -- /does/ reduce to 'True' for every @a@. The latter behavior is more desirable
    -- for @singletons@' purposes, so we use it instead of '(DTE.==)'.
    type family DefaultEq (a :: k) (b :: k) :: Bool where
      DefaultEq a a = 'True
      DefaultEq a b = 'False

    $(genDefunSymbols [''(==), ''(/=), ''DefaultEq])

    -- | The singleton analogue of 'Eq'. Unlike the definition for 'Eq', it is required
    -- that instances define a body for '(%==)'. You may also supply a body for '(%/=)'.
    class SEq k where
      -- | Boolean equality on singletons
      (%==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a == b)
      infix 4 %==

      -- | Boolean disequality on singletons
      (%/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a /= b)
      default (%/=) :: forall (a :: k) (b :: k).
                       ((a /= b) ~ Not (a == b))
                    => Sing a -> Sing b -> Sing (a /= b)
      a :: Sing a
    a %/= b :: Sing b
    b = Sing (a == b) -> Sing (Not (a == b))
    forall (a :: Bool). Sing a -> Sing (Not a)
    sNot (Sing a
    a Sing a -> Sing b -> Sing (a == b)
    forall k (a :: k) (b :: k).
    SEq k =>
    Sing a -> Sing b -> Sing (a == b)
    %== Sing b
    b)
      infix 4 %/=

    $(singEqInstances basicTypes)

    instance SEq a => SingI ((==@#@$) :: a ~> a ~> Bool) where
      sing :: Sing (==@#@$)
    sing = SingFunction2 (==@#@$) -> Sing (==@#@$)
    forall k2 k3 k (f :: k2 ~> (k3 ~> k)). SingFunction2 f -> Sing f
    singFun2 SingFunction2 (==@#@$)
    forall k (a :: k) (b :: k).
    SEq k =>
    Sing a -> Sing b -> Sing (a == b)
    (%==)
    instance (SEq a, SingI x) => SingI ((==@#@$$) x :: a ~> Bool) where
      sing :: Sing ((==@#@$$) x)
    sing = SingFunction1 ((==@#@$$) x) -> Sing ((==@#@$$) x)
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 (SingI x => Sing x
    forall k (a :: k). SingI a => Sing a
    sing @x Sing x -> Sing t -> Sing (x == t)
    forall k (a :: k) (b :: k).
    SEq k =>
    Sing a -> Sing b -> Sing (a == b)
    %==)

    instance SEq a => SingI ((/=@#@$) :: a ~> a ~> Bool) where
      sing :: Sing (/=@#@$)
    sing = SingFunction2 (/=@#@$) -> Sing (/=@#@$)
    forall k2 k3 k (f :: k2 ~> (k3 ~> k)). SingFunction2 f -> Sing f
    singFun2 SingFunction2 (/=@#@$)
    forall k (a :: k) (b :: k).
    SEq k =>
    Sing a -> Sing b -> Sing (a /= b)
    (%/=)
    instance (SEq a, SingI x) => SingI ((/=@#@$$) x :: a ~> Bool) where
      sing :: Sing ((/=@#@$$) x)
    sing = SingFunction1 ((/=@#@$$) x) -> Sing ((/=@#@$$) x)
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 (SingI x => Sing x
    forall k (a :: k). SingI a => Sing a
    sing @x Sing x -> Sing t -> Sing (x /= t)
    forall k (a :: k) (b :: k).
    SEq k =>
    Sing a -> Sing b -> Sing (a /= b)
    %/=)