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

#if __GLASGOW_HASKELL__ < 806
{-# LANGUAGE TypeInType #-}
#endif

#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif

-----------------------------------------------------------------------------
-- |
-- 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.Kind
import Data.Singletons
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'
#if __GLASGOW_HASKELL__ >= 810
type Refuted :: Type -> Type
#endif
type Refuted a = (a -> Void)

-- | A 'Decision' about a type @a@ is either a proof of existence or a proof that @a@
-- cannot exist.
#if __GLASGOW_HASKELL__ >= 810
type Decision :: Type -> Type
#endif
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.
#if __GLASGOW_HASKELL__ >= 810
type SDecide :: Type -> Constraint
#endif
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 Sing a
a 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 a :~: b
Refl -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
    Disproved Refuted (a :~: b)
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance SDecide k => TestEquality (WrappedSing :: k -> Type) where
  testEquality :: WrappedSing a -> WrappedSing b -> Maybe (a :~: b)
testEquality (WrapSing Sing a
s1) (WrapSing 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 Sing a
a 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 a :~: b
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 Refuted (a :~: b)
_ -> Maybe (Coercion a b)
forall a. Maybe a
Nothing

instance SDecide k => TestCoercion (WrappedSing :: k -> Type) where
  testCoercion :: WrappedSing a -> WrappedSing b -> Maybe (Coercion a b)
testCoercion (WrapSing Sing a
s1) (WrapSing 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