{-# LANGUAGE RankNTypes, PolyKinds, DataKinds, TypeOperators,
TypeFamilies, FlexibleContexts, UndecidableInstances,
GADTs, TypeApplications, StandaloneKindSignatures #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Data.Singletons.Decide (
SDecide(..),
(:~:)(..), Void, Refuted, Decision(..),
decideEquality, decideCoercion
) where
import Data.Kind
import Data.Singletons.Internal
import Data.Type.Coercion
import Data.Type.Equality
import Data.Void
type Refuted :: Type -> Type
type Refuted a = (a -> Void)
type Decision :: Type -> Type
data Decision a = Proved a
| Disproved (Refuted a)
type SDecide :: Type -> Constraint
class SDecide k where
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
infix 4 %~
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) 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
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) 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