-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.TypeLits.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 Data.Singletons.TypeLits
-- for a safe interface.
--
----------------------------------------------------------------------------

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

module Data.Singletons.TypeLits.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.Kind
import Data.Singletons.Promote
import Data.Singletons.Internal
import Data.Singletons.Prelude.Eq
import Data.Singletons.Prelude.Ord as O
import Data.Singletons.Decide
import Data.Singletons.Prelude.Bool
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 = 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 :: Sing a -> Demote Nat
fromSing (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 = 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 :: Sing a -> Demote Symbol
fromSing (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)

-- SDecide instances:
instance SDecide Nat where
  (SNat :: Sing n) %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ (SNat :: Sing m)
    | Just a :~: b
r <- Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Proxy a -> Proxy 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
_ -> String -> Void
forall a. HasCallStack => String -> a
error String
errStr)
    where errStr :: String
errStr = String
"Broken Nat singletons"

instance SDecide Symbol where
  (SSym :: Sing n) %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ (SSym :: Sing m)
    | Just a :~: b
r <- Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
(KnownSymbol a, KnownSymbol b) =>
Proxy a -> Proxy 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
_ -> String -> Void
forall a. HasCallStack => String -> a
error String
errStr)
    where errStr :: String
errStr = String
"Broken Symbol singletons"

-- PEq instances
instance PEq Nat
instance PEq Symbol

-- need SEq instances for TypeLits kinds
instance SEq Nat where
  (SNat :: Sing n) %== :: Sing a -> Sing b -> Sing (a == b)
%== (SNat :: Sing m)
    = case Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy n) (Proxy b
forall k (t :: k). Proxy t
Proxy :: Proxy m) of
        Just a :~: b
Refl -> Sing (a == b)
SBool 'True
STrue
        Maybe (a :~: b)
Nothing   -> SBool 'False -> SBool (DefaultEq a b)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

instance SEq Symbol where
  (SSym :: Sing n) %== :: Sing a -> Sing b -> Sing (a == b)
%== (SSym :: Sing m)
    = case Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
(KnownSymbol a, KnownSymbol b) =>
Proxy a -> Proxy 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) of
        Just a :~: b
Refl -> Sing (a == b)
SBool 'True
STrue
        Maybe (a :~: b)
Nothing   -> SBool 'False -> SBool (DefaultEq a b)
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 :: 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 :: 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

-- Convenience functions

-- | Given a singleton for @Nat@, call something requiring a
-- @KnownNat@ instance.
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat Sing 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 :: Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing 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 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 :: 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 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 :: 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 where {}
$(genDefunSymbols [''Undefined])

-- | The singleton for 'undefined'.
sUndefined :: HasCallStack => a
sUndefined :: 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 %^ :: 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 (SingI x => Sing x
forall k (a :: k). 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.Singletons.Prelude.Ord", 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 %<=? :: Sing a -> Sing b -> Sing (a <=? b)
%<=? Sing b
sb = SBool (Case_6989586621679383722 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 (SingI x => Sing x
forall k (a :: k). 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)
%<=?)