{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-----------------------------------------------------------------------------

-- |

-- Module      :  GHC.TypeLits.Singletons.Internal

-- Copyright   :  (C) 2014 Richard Eisenberg

-- License     :  BSD-style (see LICENSE)

-- Maintainer  :  Ryan Scott

-- Stability   :  experimental

-- Portability :  non-portable

--

-- Defines and exports singletons useful for the 'Natural', 'TL.Symbol', and

-- 'Char' kinds. This exports the internal, unsafe constructors. Use import

-- "GHC.TypeLits.Singletons" for a safe interface.

--

----------------------------------------------------------------------------


module GHC.TypeLits.Singletons.Internal (
  Sing,

  Natural, TL.Symbol, Char,
  TN.SNat, pattern TN.SNat,
  TL.SSymbol, pattern TL.SSymbol, pattern SSym,
  TL.SChar, pattern TL.SChar,
  TN.withKnownNat, TL.withKnownSymbol, TL.withKnownChar,
  Error, sError,
  ErrorWithoutStackTrace, sErrorWithoutStackTrace,
  Undefined, sUndefined,
  TL.KnownNat, TN.natVal, TL.KnownSymbol, TL.symbolVal, TL.KnownChar, TL.charVal,
  type (TN.^), (%^),
  type (TN.<=?), (%<=?),

  -- * Defunctionalization symbols

  ErrorSym0, ErrorSym1,
  ErrorWithoutStackTraceSym0, ErrorWithoutStackTraceSym1,
  UndefinedSym0,
  type (^@#@$),  type (^@#@$$),  type (^@#@$$$),
  type (<=?@#@$),  type (<=?@#@$$),  type (<=?@#@$$$)
  ) where

import Data.Bool.Singletons
import Data.Eq.Singletons
import Data.Ord.Singletons as O
import Data.Semigroup.Singletons.Internal.Classes
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.TH
import Data.Type.Equality (TestEquality(..))
import GHC.Stack (HasCallStack)
import qualified GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
import Numeric.Natural (Natural)
import Unsafe.Coerce

import qualified Data.Text as T
import Data.Text ( Text )

----------------------------------------------------------------------

---- TypeLits singletons ---------------------------------------------

----------------------------------------------------------------------


-- SNat

type instance Sing = TN.SNat

instance TN.KnownNat n => SingI n where
  sing :: Sing n
sing = Sing n
SNat n
forall (n :: Nat). KnownNat n => SNat n
TN.natSing

instance SingKind Natural where
  type Demote Natural = Natural
  fromSing :: forall (a :: Nat). Sing a -> Demote Nat
fromSing = Sing a -> Demote Nat
SNat a -> Nat
forall (n :: Nat). SNat n -> Nat
TN.fromSNat
  toSing :: Demote Nat -> SomeSing Nat
toSing Demote Nat
n = Nat -> (forall (n :: Nat). SNat n -> SomeSing Nat) -> SomeSing Nat
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
TN.withSomeSNat Nat
Demote Nat
n Sing n -> SomeSing Nat
SNat n -> SomeSing Nat
forall (n :: Nat). SNat n -> SomeSing Nat
forall k (a :: k). Sing a -> SomeSing k
SomeSing

-- STL.Symbol

type instance Sing = TL.SSymbol

-- | An alias for the 'TL.SSymbol' pattern synonym.

pattern SSym :: forall s. () => TL.KnownSymbol s => TL.SSymbol s
pattern $mSSym :: forall {r} {s :: Symbol}.
SSymbol s -> (KnownSymbol s => r) -> ((# #) -> r) -> r
$bSSym :: forall (s :: Symbol). KnownSymbol s => SSymbol s
SSym = TL.SSymbol
{-# COMPLETE SSym #-}

instance TL.KnownSymbol n => SingI n where
  sing :: Sing n
sing = Sing n
SSymbol n
forall (s :: Symbol). KnownSymbol s => SSymbol s
TL.symbolSing

instance SingKind TL.Symbol where
  type Demote TL.Symbol = Text
  fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol
fromSing = String -> Text
T.pack (String -> Text) -> (SSymbol a -> String) -> SSymbol a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SSymbol a -> String
forall (s :: Symbol). SSymbol s -> String
TL.fromSSymbol
  toSing :: Demote Symbol -> SomeSing Symbol
toSing Demote Symbol
s = String
-> (forall (s :: Symbol). SSymbol s -> SomeSing Symbol)
-> SomeSing Symbol
forall r. String -> (forall (s :: Symbol). SSymbol s -> r) -> r
TL.withSomeSSymbol (Text -> String
T.unpack Demote Symbol
Text
s) Sing s -> SomeSing Symbol
SSymbol s -> SomeSing Symbol
forall k (a :: k). Sing a -> SomeSing k
forall (s :: Symbol). SSymbol s -> SomeSing Symbol
SomeSing

-- SChar

type instance Sing = TL.SChar

instance TL.KnownChar c => SingI c where
  sing :: Sing c
sing = Sing c
SChar c
forall (n :: Char). KnownChar n => SChar n
TL.charSing

instance SingKind Char where
  type Demote Char = Char
  fromSing :: forall (a :: Char). Sing a -> Demote Char
fromSing = Sing a -> Demote Char
SChar a -> Char
forall (c :: Char). SChar c -> Char
TL.fromSChar
  toSing :: Demote Char -> SomeSing Char
toSing Demote Char
c = Char
-> (forall (c :: Char). SChar c -> SomeSing Char) -> SomeSing Char
forall r. Char -> (forall (c :: Char). SChar c -> r) -> r
TL.withSomeSChar Char
Demote Char
c Sing c -> SomeSing Char
SChar c -> SomeSing Char
forall (c :: Char). SChar c -> SomeSing Char
forall k (a :: k). Sing a -> SomeSing k
SomeSing

-- SDecide instances:

instance SDecide Natural where
  Sing a
sn %~ :: forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
sm
    | Just a :~: b
r <- SNat a -> SNat b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Sing a
SNat a
sn Sing b
SNat b
sm
    = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: b
r
    | Bool
otherwise
    = Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
errStr)
    where errStr :: String
errStr = String
"Broken Natural singletons"

instance SDecide TL.Symbol where
  Sing a
sn %~ :: forall (a :: Symbol) (b :: Symbol).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
sm
    | Just a :~: b
r <- SSymbol a -> SSymbol b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Maybe (a :~: b)
testEquality Sing a
SSymbol a
sn Sing b
SSymbol b
sm
    = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: b
r
    | Bool
otherwise
    = Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
errStr)
    where errStr :: String
errStr = String
"Broken TL.Symbol singletons"

instance SDecide Char where
  Sing a
sn %~ :: forall (a :: Char) (b :: Char).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
sm
    | Just a :~: b
r <- SChar a -> SChar b -> Maybe (a :~: b)
forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Sing a
SChar a
sn Sing b
SChar b
sm
    = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: b
r
    | Bool
otherwise
    = Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
errStr)
    where errStr :: String
errStr = String
"Broken Char singletons"

-- PEq instances

instance PEq Natural where
  type x == y = DefaultEq x y
instance PEq TL.Symbol where
  type x == y = DefaultEq x y
instance PEq Char where
  type x == y = DefaultEq x y

-- need SEq instances for TypeLits kinds

instance SEq Natural where
  Sing t1
sn %== :: forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
sm
    = case SNat t1 -> SNat t2 -> Maybe (t1 :~: t2)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Sing t1
SNat t1
sn Sing t2
SNat t2
sm of
        Just t1 :~: t2
Refl -> Sing (Apply (Apply (==@#@$) t1) t2)
SBool 'True
STrue
        Maybe (t1 :~: t2)
Nothing   -> SBool 'False -> SBool (DefaultEq t1 t2)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

instance SEq TL.Symbol where
  Sing t1
sn %== :: forall (t1 :: Symbol) (t2 :: Symbol).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
sm
    = case SSymbol t1 -> SSymbol t2 -> Maybe (t1 :~: t2)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Maybe (a :~: b)
testEquality Sing t1
SSymbol t1
sn Sing t2
SSymbol t2
sm of
        Just t1 :~: t2
Refl -> Sing (Apply (Apply (==@#@$) t1) t2)
SBool 'True
STrue
        Maybe (t1 :~: t2)
Nothing   -> SBool 'False -> SBool (DefaultEq t1 t2)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

instance SEq Char where
  Sing t1
sn %== :: forall (t1 :: Char) (t2 :: Char).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
sm
    = case SChar t1 -> SChar t2 -> Maybe (t1 :~: t2)
forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Sing t1
SChar t1
sn Sing t2
SChar t2
sm of
        Just t1 :~: t2
Refl -> Sing (Apply (Apply (==@#@$) t1) t2)
SBool 'True
STrue
        Maybe (t1 :~: t2)
Nothing   -> SBool 'False -> SBool (DefaultEq t1 t2)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

-- POrd instances

instance POrd Natural where
  type (a :: Natural) `Compare` (b :: Natural) = a `TN.CmpNat` b

instance POrd TL.Symbol where
  type (a :: TL.Symbol) `Compare` (b :: TL.Symbol) = a `TL.CmpSymbol` b

instance POrd Char where
  type (a :: Char) `Compare` (b :: Char) = a `TL.CmpChar` b

-- SOrd instances

instance SOrd Natural where
  Sing t1
a sCompare :: forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
`sCompare` Sing t2
b = case Sing t1 -> Demote Nat
forall (a :: Nat). Sing a -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t1
a Demote Nat -> Demote Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t2 -> Demote Nat
forall (a :: Nat). Sing a -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t2
b of
                     Ordering
LT -> SOrdering 'LT -> SOrdering (CmpNat t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
                     Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpNat t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
                     Ordering
GT -> SOrdering 'GT -> SOrdering (CmpNat t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT

instance SOrd TL.Symbol where
  Sing t1
a sCompare :: forall (t1 :: Symbol) (t2 :: Symbol).
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
`sCompare` Sing t2
b = case Sing t1 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t1
a Demote Symbol -> Demote Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t2 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t2
b of
                     Ordering
LT -> SOrdering 'LT -> SOrdering (CmpSymbol t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
                     Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpSymbol t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
                     Ordering
GT -> SOrdering 'GT -> SOrdering (CmpSymbol t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT

instance SOrd Char where
  Sing t1
a sCompare :: forall (t1 :: Char) (t2 :: Char).
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
`sCompare` Sing t2
b = case Sing t1 -> Demote Char
forall (a :: Char). Sing a -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t1
a Demote Char -> Demote Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t2 -> Demote Char
forall (a :: Char). Sing a -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t2
b of
                     Ordering
LT -> SOrdering 'LT -> SOrdering (CmpChar t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
                     Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpChar t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
                     Ordering
GT -> SOrdering 'GT -> SOrdering (CmpChar t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT

-- PSemigroup instance


instance PSemigroup TL.Symbol where
  type a <> b = TL.AppendSymbol a b

-- SSemigroup instance


instance SSemigroup TL.Symbol where
  Sing t1
sa %<> :: forall (t1 :: Symbol) (t2 :: Symbol).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (<>@#@$) t1) t2)
%<> Sing t2
sb =
    let a :: Demote Symbol
a  = Sing t1 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t1
sa
        b :: Demote Symbol
b  = Sing t2 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t2
sb
    in String
-> (forall (s :: Symbol).
    SSymbol s -> SSymbol (AppendSymbol t1 t2))
-> SSymbol (AppendSymbol t1 t2)
forall r. String -> (forall (s :: Symbol). SSymbol s -> r) -> r
TL.withSomeSSymbol (Text -> String
T.unpack (Demote Symbol
Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Demote Symbol
Text
b)) SSymbol s -> SSymbol (AppendSymbol t1 t2)
forall a b. a -> b
forall (s :: Symbol). SSymbol s -> SSymbol (AppendSymbol t1 t2)
unsafeCoerce

-- Convenience functions


-- | A promoted version of 'error'. This implements 'Error' as a stuck type

-- family with a 'Symbol' argument. Depending on your needs, you might also

-- consider the following alternatives:

--

-- * "Data.Singletons.Base.PolyError" provides @PolyError@, which generalizes

--   the argument to be kind-polymorphic. This allows passing additional

--   information to the error besides raw 'Symbol's.

--

-- * "Data.Singletons.Base.TypeError" provides @TypeError@, a slightly modified

--   version of the custom type error machinery found in "GHC.TypeLits". This

--   allows emitting error messages as compiler errors rather than as stuck type

--   families.

type Error :: TL.Symbol -> a
type family Error (str :: TL.Symbol) :: a where {}
$(genDefunSymbols [''Error])
instance SingI (ErrorSym0 :: TL.Symbol ~> a) where
  sing :: Sing ErrorSym0
sing = SingFunction1 ErrorSym0 -> Sing ErrorSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (Apply ErrorSym0 t)
Sing t -> Sing (Error t)
SingFunction1 ErrorSym0
forall (str :: Symbol) a. HasCallStack => Sing str -> a
sError

-- | The singleton for 'error'.

sError :: HasCallStack => Sing (str :: TL.Symbol) -> a
sError :: forall (str :: Symbol) a. HasCallStack => Sing str -> a
sError Sing str
sstr = String -> a
forall a. HasCallStack => String -> a
error (Text -> String
T.unpack (Sing str -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing str
sstr))

-- | The promotion of 'errorWithoutStackTrace'.

type ErrorWithoutStackTrace :: TL.Symbol -> a
type family ErrorWithoutStackTrace (str :: TL.Symbol) :: a where {}
$(genDefunSymbols [''ErrorWithoutStackTrace])
instance SingI (ErrorWithoutStackTraceSym0 :: TL.Symbol ~> a) where
  sing :: Sing ErrorWithoutStackTraceSym0
sing = SingFunction1 ErrorWithoutStackTraceSym0
-> Sing ErrorWithoutStackTraceSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (Apply ErrorWithoutStackTraceSym0 t)
Sing t -> Sing (ErrorWithoutStackTrace t)
SingFunction1 ErrorWithoutStackTraceSym0
forall (str :: Symbol) a. Sing str -> a
sErrorWithoutStackTrace

-- | The singleton for 'errorWithoutStackTrace'.

sErrorWithoutStackTrace :: Sing (str :: TL.Symbol) -> a
sErrorWithoutStackTrace :: forall (str :: Symbol) a. Sing str -> a
sErrorWithoutStackTrace Sing str
sstr = String -> a
forall a. String -> a
errorWithoutStackTrace (Text -> String
T.unpack (Sing str -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing str
sstr))

-- | The promotion of 'undefined'.

type Undefined :: a
type family Undefined :: a where {}
$(genDefunSymbols [''Undefined])

-- | The singleton for 'undefined'.

sUndefined :: HasCallStack => a
sUndefined :: forall a. HasCallStack => a
sUndefined = a
forall a. HasCallStack => a
undefined

-- | The singleton analogue of '(TN.^)' for 'Natural's.

(%^) :: Sing a -> Sing b -> Sing (a TN.^ b)
Sing a
sa %^ :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a ^ b)
%^ Sing b
sb =
  let a :: Demote Nat
a = Sing a -> Demote Nat
forall (a :: Nat). Sing a -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sa
      b :: Demote Nat
b = Sing b -> Demote Nat
forall (a :: Nat). Sing a -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing b
sb
  in Nat -> (forall (n :: Nat). SNat n -> SNat (a ^ b)) -> SNat (a ^ b)
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
TN.withSomeSNat (Nat
Demote Nat
a Nat -> Nat -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
^ Nat
Demote Nat
b) SNat n -> SNat (a ^ b)
forall (n :: Nat). SNat n -> SNat (a ^ b)
forall a b. a -> b
unsafeCoerce
infixr 8 %^

-- Defunctionalization symbols for type-level (^)

$(genDefunSymbols [''(TN.^)])
instance SingI (^@#@$) where
  sing :: Sing (^@#@$)
sing = SingFunction2 (^@#@$) -> Sing (^@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (t1 ^ t2)
Sing t1 -> Sing t2 -> Sing (Apply (Apply (^@#@$) t1) t2)
forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a ^ b)
SingFunction2 (^@#@$)
(%^)
instance SingI x => SingI ((^@#@$$) x) where
  sing :: Sing ((^@#@$$) x)
sing = SingFunction1 ((^@#@$$) x) -> Sing ((^@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (forall (a :: Nat). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x %^)
instance SingI1 (^@#@$$) where
  liftSing :: forall (x :: Nat). Sing x -> Sing ((^@#@$$) x)
liftSing Sing x
s = SingFunction1 ((^@#@$$) x) -> Sing ((^@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (Sing x
s %^)

-- | The singleton analogue of 'TN.<=?'

--

-- Note that, because of historical reasons in GHC's 'Natural' API, 'TN.<=?'

-- is incompatible (unification-wise) with 'O.<=' and the 'PEq', 'SEq',

-- 'POrd', and 'SOrd' instances for 'Natural'.  @(a '<=?' b) ~ 'True@ does not

-- imply anything about @a 'O.<=' b@ or any other 'PEq' / 'POrd'

-- relationships.

--

-- (Be aware that 'O.<=' in the paragraph above refers to 'O.<=' from the

-- 'POrd' typeclass, exported from "Data.Ord.Singletons", and /not/

-- the 'TN.<=' from "GHC.TypeNats".  The latter is simply a type alias for

-- @(a 'TN.<=?' b) ~ 'True@.)

--

-- This is provided here for the sake of completeness and for compatibility

-- with libraries with APIs built around '<=?'.  New code should use

-- 'CmpNat', exposed through this library through the 'POrd' and 'SOrd'

-- instances for 'Natural'.

(%<=?) :: forall (a :: Natural) (b :: Natural). Sing a -> Sing b -> Sing (a TN.<=? b)
Sing a
sa %<=? :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
%<=? Sing b
sb = SBool (a <= b) -> SBool (OrdCond (CmpNat a b) 'True 'True 'False)
forall a b. a -> b
unsafeCoerce (Sing a
sa Sing a -> Sing b -> Sing (Apply (Apply (<=@#@$) a) b)
forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)
%<= Sing b
sb)
infix 4 %<=?

-- Defunctionalization symbols for (<=?)

$(genDefunSymbols [''(TN.<=?)])
instance SingI ((<=?@#@$) @Natural) where
  sing :: Sing (<=?@#@$)
sing = SingFunction2 (<=?@#@$) -> Sing (<=?@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=?@#@$) t1) t2)
Sing t1 -> Sing t2 -> Sing (t1 <=? t2)
SingFunction2 (<=?@#@$)
forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
(%<=?)
instance SingI x => SingI ((<=?@#@$$) @Natural x) where
  sing :: Sing ((<=?@#@$$) x)
sing = SingFunction1 ((<=?@#@$$) x) -> Sing ((<=?@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (forall (a :: Nat). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x %<=?)
instance SingI1 ((<=?@#@$$) @Natural) where
  liftSing :: forall (x :: Nat). Sing x -> Sing ((<=?@#@$$) x)
liftSing Sing x
s = SingFunction1 ((<=?@#@$$) x) -> Sing ((<=?@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (Sing x
s %<=?)