    {-# LANGUAGE RankNTypes, PolyKinds, DataKinds, TypeOperators,
                 TypeFamilies, FlexibleContexts, UndecidableInstances,
                 GADTs, TypeApplications #-}
    {-# OPTIONS_GHC -Wno-orphans #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.Decide
    -- Copyright   :  (C) 2013 Richard Eisenberg
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Defines the class 'SDecide', allowing for decidable equality over singletons.
    --
    ----------------------------------------------------------------------------

    module Data.Singletons.Decide (
      -- * The SDecide class
      SDecide(..),

      -- * Supporting definitions
      (:~:)(..), Void, Refuted, Decision(..),
      decideEquality, decideCoercion
      ) where

    import Data.Singletons.Internal
    import Data.Type.Coercion
    import Data.Type.Equality
    import Data.Void

    ----------------------------------------------------------------------
    ---- SDecide ---------------------------------------------------------
    ----------------------------------------------------------------------

    -- | Because we can never create a value of type 'Void', a function that type-checks
    -- at @a -> Void@ shows that objects of type @a@ can never exist. Thus, we say that
    -- @a@ is 'Refuted'
    type Refuted a = (a -> Void)

    -- | A 'Decision' about a type @a@ is either a proof of existence or a proof that @a@
    -- cannot exist.
    data Decision a = Proved a               -- ^ Witness for @a@
                    | Disproved (Refuted a)  -- ^ Proof that no @a@ exists

    -- | Members of the 'SDecide' "kind" class support decidable equality. Instances
    -- of this class are generated alongside singleton definitions for datatypes that
    -- derive an 'Eq' instance.
    class SDecide k where
      -- | Compute a proof or disproof of equality, given two singletons.
      (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
      infix 4 %~

    -- | A suitable default implementation for 'testEquality' that leverages
    -- 'SDecide'.
    decideEquality :: forall k (a :: k) (b :: k). SDecide k
                   => Sing a -> Sing b -> Maybe (a :~: b)
    decideEquality :: Sing a -> Sing b -> Maybe (a :~: b)
    decideEquality a :: Sing a
    a b :: Sing b
    b =
      case Sing a
    a Sing a -> Sing b -> Decision (a :~: b)
    forall k (a :: k) (b :: k).
    SDecide k =>
    Sing a -> Sing b -> Decision (a :~: b)
    %~ Sing b
    b of
        Proved Refl -> (a :~: a) -> Maybe (a :~: a)
    forall a. a -> Maybe a
    Just a :~: a
    forall k (a :: k). a :~: a
    Refl
        Disproved _ -> Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    instance SDecide k => TestEquality (WrappedSing @k) where
      testEquality :: WrappedSing a -> WrappedSing b -> Maybe (a :~: b)
    testEquality (WrapSing s1 :: Sing a
    s1) (WrapSing s2 :: Sing b
    s2) = Sing a -> Sing b -> Maybe (a :~: b)
    forall k (a :: k) (b :: k).
    SDecide k =>
    Sing a -> Sing b -> Maybe (a :~: b)
    decideEquality Sing a
    s1 Sing b
    s2

    -- | A suitable default implementation for 'testCoercion' that leverages
    -- 'SDecide'.
    decideCoercion :: forall k (a :: k) (b :: k). SDecide k
                   => Sing a -> Sing b -> Maybe (Coercion a b)
    decideCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)
    decideCoercion a :: Sing a
    a b :: Sing b
    b =
      case Sing a
    a Sing a -> Sing b -> Decision (a :~: b)
    forall k (a :: k) (b :: k).
    SDecide k =>
    Sing a -> Sing b -> Decision (a :~: b)
    %~ Sing b
    b of
        Proved Refl -> Coercion a b -> Maybe (Coercion a b)
    forall a. a -> Maybe a
    Just Coercion a b
    forall k (a :: k) (b :: k). Coercible a b => Coercion a b
    Coercion
        Disproved _ -> Maybe (Coercion a b)
    forall a. Maybe a
    Nothing

    instance SDecide k => TestCoercion (WrappedSing @k) where
      testCoercion :: WrappedSing a -> WrappedSing b -> Maybe (Coercion a b)
    testCoercion (WrapSing s1 :: Sing a
    s1) (WrapSing s2 :: Sing b
    s2) = Sing a -> Sing b -> Maybe (Coercion a b)
    forall k (a :: k) (b :: k).
    SDecide k =>
    Sing a -> Sing b -> Maybe (Coercion a b)
    decideCoercion Sing a
    s1 Sing b
    s2