-----------------------------------------------------------------------------
-- |
-- 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 'Nat' and 'Symbol' 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,

  Nat, Symbol,
  SNat(..), SSymbol(..), withKnownNat, withKnownSymbol,
  Error, sError,
  ErrorWithoutStackTrace, sErrorWithoutStackTrace,
  Undefined, sUndefined,
  KnownNat, TN.natVal, KnownSymbol, symbolVal,
  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 Numeric.Natural (Natural)
import Unsafe.Coerce

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

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

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

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

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

-- SDecide instances:
instance SDecide Nat where
  (Sing a
SNat a
SNat :: Sing n) %~ :: forall (a :: Nat) (b :: Nat).
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 :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(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 Nat 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"

-- PEq instances
instance PEq Nat where
  type x == y = DefaultEq x y
instance PEq Symbol where
  type x == y = DefaultEq x y

-- need SEq instances for TypeLits kinds
instance SEq Nat where
  (Sing t
SNat t
SNat :: Sing n) %== :: forall (t :: Nat) (t :: Nat).
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 :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(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

-- POrd instances
instance POrd Nat where
  type (a :: Nat) `Compare` (b :: Nat) = a `TN.CmpNat` b

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

-- SOrd instances
instance SOrd Nat where
  Sing t
a sCompare :: forall (t :: Nat) (t :: Nat).
Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)
`sCompare` Sing t
b = case Sing t -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
a Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t -> Demote Nat
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 Text -> Text -> 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

-- 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 Nats
-- 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 :: Nat) (proxy :: Nat -> *).
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)
      )

-- Convenience functions

-- | Given a singleton for @Nat@, call something requiring a
-- @KnownNat@ instance.
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat :: forall (n :: Nat) 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

-- | 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 'Nat's.
(%^) :: Sing a -> Sing b -> Sing (a ^ 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 k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sa
      b :: Demote Nat
b = Sing b -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing b
sb
      ex :: SomeNat
ex = Natural -> SomeNat
TN.someNatVal (Natural
Demote Nat
a Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural
Demote Nat
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 :: Nat). 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 :: 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 {k} (a :: k). SingI a => Sing a
forall (a :: Nat). SingI a => Sing a
sing @x Sing x -> Sing t -> Sing (x ^ t)
forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a ^ b)
%^)

-- | The singleton analogue of 'TN.<=?'
--
-- Note that, because of historical reasons in GHC's 'TN.Nat' API, 'TN.<=?'
-- is incompatible (unification-wise) with 'O.<=' and the 'PEq', 'SEq',
-- 'POrd', and 'SOrd' instances for 'Nat'.  @(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 'Nat'.
(%<=?) :: Sing a -> Sing b -> Sing (a <=? b)
Sing a
sa %<=? :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
%<=? Sing b
sb = SBool (Case_6989586621679170817 a b (CmpNat a b))
-> SBool (a <=? b)
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 (<=?@#@$) where
  sing :: Sing (<=?@#@$)
sing = SingFunction2 (<=?@#@$) -> Sing (<=?@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 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 {k} (a :: k). SingI a => Sing a
forall (a :: Nat). SingI a => Sing a
sing @x Sing x -> Sing t -> Sing (x <=? t)
forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
%<=?)