-----------------------------------------------------------------------------
-- |
-- 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', 'Symbol', and
-- 'Char' kinds. This exports the internal, unsafe constructors. Use import
-- "GHC.TypeLits.Singletons" for a safe interface.
--
----------------------------------------------------------------------------

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, FlexibleInstances,
             UndecidableInstances, ScopedTypeVariables, RankNTypes,
             GADTs, FlexibleContexts, TypeOperators, ConstraintKinds,
             TemplateHaskell, TypeApplications, StandaloneKindSignatures #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module GHC.TypeLits.Singletons.Internal (
  Sing,

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

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

import Data.Bool.Singletons
import Data.Eq.Singletons
import Data.Kind
import Data.Ord.Singletons as O
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.TH
import GHC.Show (appPrec, appPrec1)
import GHC.Stack (HasCallStack)
import GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
import Unsafe.Coerce

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

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

type SNat :: Natural -> Type
data SNat (n :: Natural) = KnownNat n => SNat
type instance Sing = SNat

instance KnownNat n => SingI n where
  sing :: Sing n
sing = Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat

instance SingKind Natural where
  type Demote Natural = Natural
  fromSing :: forall (a :: Natural). Sing a -> Demote Natural
fromSing (Sing a
SNat a
SNat :: Sing n) = Proxy a -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
TN.natVal (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
  toSing :: Demote Natural -> SomeSing Natural
toSing Demote Natural
n = case Natural -> SomeNat
TN.someNatVal Natural
Demote Natural
n of
               SomeNat (Proxy n
_ :: Proxy n) -> Sing n -> SomeSing Natural
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat :: Sing n)

type SSymbol :: Symbol -> Type
data SSymbol (n :: Symbol) = KnownSymbol n => SSym
type instance Sing = SSymbol

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

instance SingKind Symbol where
  type Demote Symbol = Text
  fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol
fromSing (Sing a
SSymbol a
SSym :: Sing n) = String -> Text
T.pack (Proxy a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  toSing :: Demote Symbol -> SomeSing Symbol
toSing Demote Symbol
s = case String -> SomeSymbol
someSymbolVal (Text -> String
T.unpack Text
Demote Symbol
s) of
               SomeSymbol (Proxy n
_ :: Proxy n) -> Sing n -> SomeSing Symbol
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSym :: Sing n)

type SChar :: Char -> Type
data SChar (c :: Char) = KnownChar c => SChar
type instance Sing = SChar

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

instance SingKind Char where
  type Demote Char = Char
  fromSing :: forall (a :: Char). Sing a -> Demote Char
fromSing (Sing a
SChar a
SChar :: Sing c) = Proxy a -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy c)
  toSing :: Demote Char -> SomeSing Char
toSing Demote Char
sc = case Char -> SomeChar
someCharVal Char
Demote Char
sc of
                SomeChar (Proxy n
_ :: Proxy c) -> Sing n -> SomeSing Char
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing n
forall (c :: Char). KnownChar c => SChar c
SChar :: Sing c)

-- SDecide instances:
instance SDecide Natural where
  (Sing a
SNat a
SNat :: Sing n) %~ :: forall (a :: Natural) (b :: Natural).
Sing a -> Sing b -> Decision (a :~: b)
%~ (Sing b
SNat b
SNat :: Sing m)
    | Just a :~: b
r <- Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
TN.sameNat (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
    = (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 Symbol where
  (Sing a
SSymbol a
SSym :: Sing n) %~ :: forall (a :: Symbol) (b :: Symbol).
Sing a -> Sing b -> Decision (a :~: b)
%~ (Sing b
SSymbol b
SSym :: Sing m)
    | Just a :~: b
r <- Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
    = (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 Symbol singletons"

instance SDecide Char where
  (Sing a
SChar a
SChar :: Sing n) %~ :: forall (a :: Char) (b :: Char).
Sing a -> Sing b -> Decision (a :~: b)
%~ (Sing b
SChar b
SChar :: Sing m)
    | Just a :~: b
r <- Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameChar (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
    = (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 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 t
SNat t
SNat :: Sing n) %== :: forall (t :: Natural) (t :: Natural).
Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)
%== (Sing t
SNat t
SNat :: Sing m)
    = case Proxy t -> Proxy t -> Maybe (t :~: t)
forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy m) of
        Just t :~: t
Refl -> Sing (Apply (Apply (==@#@$) t) t)
SBool 'True
STrue
        Maybe (t :~: t)
Nothing   -> SBool 'False -> SBool (DefaultEq t t)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

instance SEq Symbol where
  (Sing t
SSymbol t
SSym :: Sing n) %== :: forall (t :: Symbol) (t :: Symbol).
Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)
%== (Sing t
SSymbol t
SSym :: Sing m)
    = case Proxy t -> Proxy t -> Maybe (t :~: t)
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy m) of
        Just t :~: t
Refl -> Sing (Apply (Apply (==@#@$) t) t)
SBool 'True
STrue
        Maybe (t :~: t)
Nothing   -> SBool 'False -> SBool (DefaultEq t t)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

instance SEq Char where
  (Sing t
SChar t
SChar :: Sing n) %== :: forall (t :: Char) (t :: Char).
Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)
%== (Sing t
SChar t
SChar :: Sing m)
    = case Proxy t -> Proxy t -> Maybe (t :~: t)
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameChar (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy m) of
        Just t :~: t
Refl -> Sing (Apply (Apply (==@#@$) t) t)
SBool 'True
STrue
        Maybe (t :~: t)
Nothing   -> SBool 'False -> SBool (DefaultEq t t)
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 Symbol where
  type (a :: Symbol) `Compare` (b :: 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 t
a sCompare :: forall (t :: Natural) (t :: Natural).
Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)
`sCompare` Sing t
b = case Sing t -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
a Demote Natural -> Demote Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
b of
                     Ordering
LT -> SOrdering 'LT -> SOrdering (CmpNat t t)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
                     Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpNat t t)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
                     Ordering
GT -> SOrdering 'GT -> SOrdering (CmpNat t t)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT

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

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

-- Show instances

-- These are a bit special because the singleton constructor does not uniquely
-- determine the type being used in the constructor's return type (e.g., all Naturals
-- have the same singleton constructor, SNat). To compensate for this, we display
-- the type being used using visible type application. (Thanks to @cumber on #179
-- for suggesting this implementation.)

instance Show (SNat n) where
  showsPrec :: Int -> SNat n -> ShowS
showsPrec Int
p n :: SNat n
n@SNat n
SNat
    = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
      ( String -> ShowS
showString String
"SNat @"
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 (SNat n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
TN.natVal SNat n
n)
      )

instance Show (SSymbol s) where
  showsPrec :: Int -> SSymbol s -> ShowS
showsPrec Int
p s :: SSymbol s
s@SSymbol s
SSym
    = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
      ( String -> ShowS
showString String
"SSym @"
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 (SSymbol s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal SSymbol s
s)
      )

instance Show (SChar c) where
  showsPrec :: Int -> SChar c -> ShowS
showsPrec Int
p s :: SChar c
s@SChar c
SChar
    = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
      ( String -> ShowS
showString String
"SChar @"
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 (SChar c -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal SChar c
s)
      )

-- Convenience functions

-- | Given a singleton for @Nat@, call something requiring a
-- @KnownNat@ instance.
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat :: forall (n :: Natural) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
SNat n
SNat KnownNat n => r
f = r
KnownNat n => r
f

-- | Given a singleton for @Symbol@, call something requiring
-- a @KnownSymbol@ instance.
withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol :: forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing n
SSymbol n
SSym KnownSymbol n => r
f = r
KnownSymbol n => r
f

-- | Given a singleton for @Char@, call something requiring
-- a @KnownChar@ instance.
withKnownChar :: Sing n -> (KnownChar n => r) -> r
withKnownChar :: forall (n :: Char) r. Sing n -> (KnownChar n => r) -> r
withKnownChar Sing n
SChar n
SChar KnownChar n => r
f = r
KnownChar n => r
f

-- | The promotion of 'error'. This version is more poly-kinded for
-- easier use.
type Error :: k0 -> k
type family Error (str :: k0) :: k where {}
$(genDefunSymbols [''Error])
instance SingI (ErrorSym0 :: Symbol ~> a) where
  sing :: Sing ErrorSym0
sing = SingFunction1 ErrorSym0 -> Sing ErrorSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 SingFunction1 ErrorSym0
forall (str :: Symbol) a. HasCallStack => Sing str -> a
sError

-- | The singleton for 'error'
sError :: HasCallStack => Sing (str :: 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
fromSing Sing str
sstr))

-- | The promotion of 'errorWithoutStackTrace'. This version is more
-- poly-kinded for easier use.
type ErrorWithoutStackTrace :: k0 -> k
type family ErrorWithoutStackTrace (str :: k0) :: k where {}
$(genDefunSymbols [''ErrorWithoutStackTrace])
instance SingI (ErrorWithoutStackTraceSym0 :: Symbol ~> a) where
  sing :: Sing ErrorWithoutStackTraceSym0
sing = SingFunction1 ErrorWithoutStackTraceSym0
-> Sing ErrorWithoutStackTraceSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 SingFunction1 ErrorWithoutStackTraceSym0
forall (str :: Symbol) a. Sing str -> a
sErrorWithoutStackTrace

-- | The singleton for 'errorWithoutStackTrace'.
sErrorWithoutStackTrace :: Sing (str :: 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
fromSing Sing str
sstr))

-- | The promotion of 'undefined'.
type Undefined :: k
type family Undefined :: k 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 ^ b)
Sing a
sa %^ :: forall (a :: Natural) (b :: Natural).
Sing a -> Sing b -> Sing (a ^ b)
%^ Sing b
sb =
  let a :: Demote Natural
a = Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sa
      b :: Demote Natural
b = Sing b -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing b
sb
      ex :: SomeNat
ex = Natural -> SomeNat
TN.someNatVal (Natural
Demote Natural
a Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural
Demote Natural
b)
  in
  case SomeNat
ex of
    SomeNat (Proxy n
_ :: Proxy ab) -> SNat n -> SNat (a ^ b)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat :: Sing ab)
infixr 8 %^

-- Defunctionalization symbols for type-level (^)
$(genDefunSymbols [''(^)])
instance SingI (^@#@$) where
  sing :: Sing (^@#@$)
sing = SingFunction2 (^@#@$) -> Sing (^@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 forall (a :: Natural) (b :: Natural).
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 :: Natural). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x Sing x -> Sing t -> Sing (x ^ t)
forall (a :: Natural) (b :: Natural).
Sing a -> Sing b -> Sing (a ^ b)
%^)
instance SingI1 (^@#@$$) where
  liftSing :: forall (x :: Natural). 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 Sing x -> Sing t -> Sing (x ^ t)
forall (a :: Natural) (b :: Natural).
Sing a -> Sing b -> Sing (a ^ b)
%^)

-- | 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 <=? b)
Sing a
sa %<=? :: forall (a :: Natural) (b :: Natural).
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 a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)
%<= Sing b
sb)
infix 4 %<=?

-- Defunctionalization symbols for (<=?)
$(genDefunSymbols [''(<=?)])
instance SingI ((<=?@#@$) @Natural) where
  sing :: Sing (<=?@#@$)
sing = SingFunction2 (<=?@#@$) -> Sing (<=?@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 forall (a :: Natural) (b :: Natural).
Sing a -> Sing b -> Sing (a <=? b)
SingFunction2 (<=?@#@$)
(%<=?)
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 :: Natural). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x Sing x -> Sing t -> Sing (x <=? t)
forall (a :: Natural) (b :: Natural).
Sing a -> Sing b -> Sing (a <=? b)
%<=?)
instance SingI1 ((<=?@#@$$) @Natural) where
  liftSing :: forall (x :: Natural). 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 Sing x -> Sing t -> Sing (x <=? t)
forall (a :: Natural) (b :: Natural).
Sing a -> Sing b -> Sing (a <=? b)
%<=?)