{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, ConstraintKinds,
             GADTs, TypeApplications, TypeFamilies, UndecidableInstances,
             DataKinds, PolyKinds, StandaloneKindSignatures #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  GHC.TypeLits.Singletons
-- 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.
--
----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wno-orphans #-}

module GHC.TypeLits.Singletons (
  Natural, Symbol, Char,
  Sing, SNat(..), SSymbol(..), SChar(..),
  withKnownNat, withKnownSymbol, withKnownChar,
  Error, sError,
  ErrorWithoutStackTrace, sErrorWithoutStackTrace,
  Undefined, sUndefined,
  KnownNat, natVal,
  KnownSymbol, symbolVal,
  KnownChar, charVal,

  type (^), (%^),
  type (<=?), (%<=?),

  TN.Log2, sLog2,
  Div, sDiv, Mod, sMod, DivMod, sDivMod,
  Quot, sQuot, Rem, sRem, QuotRem, sQuotRem,

  consSymbol, ConsSymbol, sConsSymbol,
  unconsSymbol, UnconsSymbol, sUnconsSymbol,
  charToNat, CharToNat, sCharToNat,
  natToChar, NatToChar, sNatToChar,

  -- * Defunctionalization symbols
  ErrorSym0, ErrorSym1,
  ErrorWithoutStackTraceSym0, ErrorWithoutStackTraceSym1,
  UndefinedSym0,
  KnownNatSym0, KnownNatSym1,
  KnownSymbolSym0, KnownSymbolSym1,
  KnownCharSym0, KnownCharSym1,
  type (^@#@$), type (^@#@$$), type (^@#@$$$),
  type (<=?@#@$), type (<=?@#@$$), type (<=?@#@$$$),
  Log2Sym0, Log2Sym1,
  DivSym0, DivSym1, DivSym2,
  ModSym0, ModSym1, ModSym2,
  DivModSym0, DivModSym1, DivModSym2,
  QuotSym0, QuotSym1, QuotSym2,
  RemSym0, RemSym1, RemSym2,
  QuotRemSym0, QuotRemSym1, QuotRemSym2,
  ConsSymbolSym0, ConsSymbolSym1, ConsSymbolSym2,
  UnconsSymbolSym0, UnconsSymbolSym1,
  CharToNatSym0, CharToNatSym1,
  NatToCharSym0, NatToCharSym1
  ) where

import Data.Char (chr, ord)
import qualified Data.List as L (uncons)
import Data.Singletons
import Data.Singletons.TH
import Data.String (IsString(..))
import qualified Data.Text as T
import Data.Tuple.Singletons
import GHC.TypeLits ( CharToNat, ConsSymbol, NatToChar, SomeChar(..)
                    , SomeSymbol(..), UnconsSymbol, someCharVal, someSymbolVal )
import GHC.TypeLits.Singletons.Internal
import qualified GHC.TypeNats as TN
import GHC.TypeNats (Div, Mod, SomeNat(..))
import Unsafe.Coerce

-- | This bogus instance is helpful for people who want to define
-- functions over Symbols that will only be used at the type level or
-- as singletons.
instance Eq Symbol where
  == :: Symbol -> Symbol -> Bool
(==)        = Symbol -> Symbol -> Bool
forall a. a
no_term_level_syms

instance Ord Symbol where
  compare :: Symbol -> Symbol -> Ordering
compare     = Symbol -> Symbol -> Ordering
forall a. a
no_term_level_syms

instance IsString Symbol where
  fromString :: String -> Symbol
fromString  = String -> Symbol
forall a. a
no_term_level_syms

instance Semigroup Symbol where
  <> :: Symbol -> Symbol -> Symbol
(<>) = Symbol -> Symbol -> Symbol
forall a. a
no_term_level_syms

instance Monoid Symbol where
  mempty :: Symbol
mempty = Symbol
forall a. a
no_term_level_syms

instance Show Symbol where
  showsPrec :: Int -> Symbol -> ShowS
showsPrec = Int -> Symbol -> ShowS
forall a. a
no_term_level_syms

no_term_level_syms :: a
no_term_level_syms :: forall a. a
no_term_level_syms = String -> a
forall a. HasCallStack => String -> a
error String
"The kind `Symbol` may not be used at the term level."

-- These are often useful in TypeLits-heavy code
$(genDefunSymbols [''KnownNat, ''KnownSymbol, ''KnownChar])

------------------------------------------------------------
-- Log2, Div, Mod, DivMod, and friends
------------------------------------------------------------

{- | Adapted from GHC's source code.

Compute the logarithm of a number in the given base, rounded down to the
closest integer. -}
genLog2 :: Natural -> Natural
genLog2 :: Natural -> Natural
genLog2 Natural
x = Natural -> Natural -> Natural
forall {t} {t}. (Num t, Integral t) => t -> t -> t
exactLoop Natural
0 Natural
x
  where
  exactLoop :: t -> t -> t
exactLoop t
s t
i
    | t
i t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
1     = t
s
    | t
i t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
2      = t
s
    | Bool
otherwise  =
        let s1 :: t
s1 = t
s t -> t -> t
forall a. Num a => a -> a -> a
+ t
1
        in t
s1 t -> t -> t
`seq` case t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
divMod t
i t
2 of
                      (t
j,t
r)
                        | t
r t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0    -> t -> t -> t
exactLoop t
s1 t
j
                        | Bool
otherwise -> t -> t -> t
forall {t} {t}. (Num t, Integral t) => t -> t -> t
underLoop t
s1 t
j

  underLoop :: t -> t -> t
underLoop t
s t
i
    | t
i t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
2  = t
s
    | Bool
otherwise = let s1 :: t
s1 = t
s t -> t -> t
forall a. Num a => a -> a -> a
+ t
1 in t
s1 t -> t -> t
`seq` t -> t -> t
underLoop t
s1 (t -> t -> t
forall a. Integral a => a -> a -> a
div t
i t
2)


sLog2 :: Sing x -> Sing (TN.Log2 x)
sLog2 :: forall (x :: Natural). Sing x -> Sing (Log2 x)
sLog2 Sing x
sx =
    let x :: Demote Natural
x   = Sing x -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
    in case Demote Natural
x of
         Demote Natural
0 -> String -> SNat (Log2 x)
forall a. HasCallStack => String -> a
error String
"log2 of 0"
         Demote Natural
_ -> case Natural -> SomeNat
TN.someNatVal (Natural -> Natural
genLog2 Natural
Demote Natural
x) of
                SomeNat (Proxy n
_ :: Proxy res) -> SNat n -> SNat (Log2 x)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat :: Sing res)
$(genDefunSymbols [''TN.Log2])
instance SingI Log2Sym0 where
  sing :: Sing Log2Sym0
sing = SingFunction1 Log2Sym0 -> Sing Log2Sym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 forall (x :: Natural). Sing x -> Sing (Log2 x)
SingFunction1 Log2Sym0
sLog2

sDiv :: Sing x -> Sing y -> Sing (Div x y)
sDiv :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
sDiv Sing x
sx Sing y
sy =
    let x :: Demote Natural
x   = Sing x -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Natural
y   = Sing y -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
        res :: SomeNat
res = Natural -> SomeNat
TN.someNatVal (Natural
Demote Natural
x Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
Demote Natural
y)
    in case SomeNat
res of
         SomeNat (Proxy n
_ :: Proxy res) -> SNat n -> SNat (Div x y)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat :: Sing res)
infixl 7 `sDiv`
$(genDefunSymbols [''Div])
instance SingI DivSym0 where
  sing :: Sing DivSym0
sing = SingFunction2 DivSym0 -> Sing DivSym0
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
SingFunction2 DivSym0
sDiv
instance SingI x => SingI (DivSym1 x) where
  sing :: Sing (DivSym1 x)
sing = SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (DivSym1 x) -> Sing (DivSym1 x))
-> SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Div x t)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
sDiv (forall (a :: Natural). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x)
instance SingI1 DivSym1 where
  liftSing :: forall (x :: Natural). Sing x -> Sing (DivSym1 x)
liftSing Sing x
s = SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (DivSym1 x) -> Sing (DivSym1 x))
-> SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Div x t)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
sDiv Sing x
s

sMod :: Sing x -> Sing y -> Sing (Mod x y)
sMod :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
sMod Sing x
sx Sing y
sy =
    let x :: Demote Natural
x   = Sing x -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Natural
y   = Sing y -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
        res :: SomeNat
res = Natural -> SomeNat
TN.someNatVal (Natural
Demote Natural
x Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
Demote Natural
y)
    in case SomeNat
res of
         SomeNat (Proxy n
_ :: Proxy res) -> SNat n -> SNat (Mod x y)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat :: Sing res)
infixl 7 `sMod`
$(genDefunSymbols [''Mod])
instance SingI ModSym0 where
  sing :: Sing ModSym0
sing = SingFunction2 ModSym0 -> Sing ModSym0
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
SingFunction2 ModSym0
sMod
instance SingI x => SingI (ModSym1 x) where
  sing :: Sing (ModSym1 x)
sing = SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ModSym1 x) -> Sing (ModSym1 x))
-> SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Mod x t)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
sMod (Sing x -> Sing t -> Sing (Mod x t))
-> Sing x -> Sing t -> Sing (Mod x t)
forall a b. (a -> b) -> a -> b
$ forall (a :: Natural). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x
instance SingI1 ModSym1 where
  liftSing :: forall (x :: Natural). Sing x -> Sing (ModSym1 x)
liftSing Sing x
s = SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ModSym1 x) -> Sing (ModSym1 x))
-> SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Mod x t)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
sMod Sing x
s

$(promoteOnly [d|
  divMod :: Natural -> Natural -> (Natural, Natural)
  divMod x y = (div x y, mod x y)

  quotRem :: Natural -> Natural -> (Natural, Natural)
  quotRem = divMod

  quot :: Natural -> Natural -> Natural
  quot = div
  infixl 7 `quot`

  rem :: Natural -> Natural -> Natural
  rem = mod
  infixl 7 `rem`
  |])

sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
sDivMod :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (DivMod x y)
sDivMod Sing x
sx Sing y
sy =
    let x :: Demote Natural
x     = Sing x -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Natural
y     = Sing y -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
        (Natural
q,Natural
r) = Natural
Demote Natural
x Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` Natural
Demote Natural
y
        qRes :: SomeNat
qRes  = Natural -> SomeNat
TN.someNatVal Natural
q
        rRes :: SomeNat
rRes  = Natural -> SomeNat
TN.someNatVal Natural
r
    in case (SomeNat
qRes, SomeNat
rRes) of
         (SomeNat (Proxy n
_ :: Proxy q), SomeNat (Proxy n
_ :: Proxy r))
           -> STuple2 '(n, n) -> STuple2 '(Div x y, Mod x y)
forall a b. a -> b
unsafeCoerce (Sing n -> Sing n -> STuple2 '(n, n)
forall a b (n :: a) (n :: b). Sing n -> Sing n -> STuple2 '(n, n)
STuple2 (Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat :: Sing q) (Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat :: Sing r))

sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
sQuotRem :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (QuotRem x y)
sQuotRem = Sing x -> Sing y -> Sing (QuotRem x y)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (DivMod x y)
sDivMod

sQuot :: Sing x -> Sing y -> Sing (Quot x y)
sQuot :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Quot x y)
sQuot = Sing x -> Sing y -> Sing (Quot x y)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
sDiv
infixl 7 `sQuot`

sRem :: Sing x -> Sing y -> Sing (Rem x y)
sRem :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Rem x y)
sRem = Sing x -> Sing y -> Sing (Rem x y)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
sMod
infixl 7 `sRem`

consSymbol :: Char -> String -> String
consSymbol :: Char -> ShowS
consSymbol = (:)

sConsSymbol :: Sing x -> Sing y -> Sing (ConsSymbol x y)
sConsSymbol :: forall (x :: Char) (y :: Symbol).
Sing x -> Sing y -> Sing (ConsSymbol x y)
sConsSymbol Sing x
sx Sing y
sy =
    let x :: Demote Char
x   = Sing x -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: String
y   = Text -> String
T.unpack (Sing y -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy)
        res :: SomeSymbol
res = String -> SomeSymbol
someSymbolVal (Char -> ShowS
consSymbol Char
Demote Char
x String
y)
    in case SomeSymbol
res of
         SomeSymbol (Proxy n
_ :: Proxy res) -> SSymbol n -> SSymbol (ConsSymbol x y)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSym :: Sing res)
$(genDefunSymbols [''ConsSymbol])
instance SingI ConsSymbolSym0 where
  sing :: Sing ConsSymbolSym0
sing = SingFunction2 ConsSymbolSym0 -> Sing ConsSymbolSym0
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 forall (x :: Char) (y :: Symbol).
Sing x -> Sing y -> Sing (ConsSymbol x y)
SingFunction2 ConsSymbolSym0
sConsSymbol
instance SingI x => SingI (ConsSymbolSym1 x) where
  sing :: Sing (ConsSymbolSym1 x)
sing = SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x))
-> SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (ConsSymbol x t)
forall (x :: Char) (y :: Symbol).
Sing x -> Sing y -> Sing (ConsSymbol x y)
sConsSymbol (Sing x -> Sing t -> Sing (ConsSymbol x t))
-> Sing x -> Sing t -> Sing (ConsSymbol x t)
forall a b. (a -> b) -> a -> b
$ forall (a :: Char). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x
instance SingI1 ConsSymbolSym1 where
  liftSing :: forall (x :: Char). Sing x -> Sing (ConsSymbolSym1 x)
liftSing Sing x
s = SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x))
-> SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (ConsSymbol x t)
forall (x :: Char) (y :: Symbol).
Sing x -> Sing y -> Sing (ConsSymbol x y)
sConsSymbol Sing x
s

unconsSymbol :: String -> Maybe (Char, String)
unconsSymbol :: String -> Maybe (Char, String)
unconsSymbol = String -> Maybe (Char, String)
forall a. [a] -> Maybe (a, [a])
L.uncons

sUnconsSymbol :: Sing x -> Sing (UnconsSymbol x)
sUnconsSymbol :: forall (x :: Symbol). Sing x -> Sing (UnconsSymbol x)
sUnconsSymbol Sing x
sx =
    let x :: String
x   = Text -> String
T.unpack (Sing x -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx)
        res :: SomeSing (Maybe (Char, String))
res = Demote (Maybe (Char, String)) -> SomeSing (Maybe (Char, String))
forall k. SingKind k => Demote k -> SomeSing k
toSing (String -> Maybe (Char, String)
unconsSymbol String
x)
    in case SomeSing (Maybe (Char, String))
res of
         SomeSing Sing a
s -> SMaybe a -> SMaybe (UnconsSymbol x)
forall a b. a -> b
unsafeCoerce Sing a
SMaybe a
s
$(genDefunSymbols [''UnconsSymbol])
instance SingI UnconsSymbolSym0 where
  sing :: Sing UnconsSymbolSym0
sing = SingFunction1 UnconsSymbolSym0 -> Sing UnconsSymbolSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 forall (x :: Symbol). Sing x -> Sing (UnconsSymbol x)
SingFunction1 UnconsSymbolSym0
sUnconsSymbol

charToNat :: Char -> Natural
charToNat :: Char -> Natural
charToNat = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> (Char -> Int) -> Char -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord

sCharToNat :: Sing x -> Sing (CharToNat x)
sCharToNat :: forall (x :: Char). Sing x -> Sing (CharToNat x)
sCharToNat Sing x
sx =
    let x :: Demote Char
x   = Sing x -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        res :: SomeNat
res = Natural -> SomeNat
TN.someNatVal (Char -> Natural
charToNat Char
Demote Char
x)
    in case SomeNat
res of
         SomeNat (Proxy n
_ :: Proxy res) -> SNat n -> SNat (CharToNat x)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Natural). KnownNat n => SNat n
SNat :: Sing res)
$(genDefunSymbols [''CharToNat])
instance SingI CharToNatSym0 where
  sing :: Sing CharToNatSym0
sing = SingFunction1 CharToNatSym0 -> Sing CharToNatSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 forall (x :: Char). Sing x -> Sing (CharToNat x)
SingFunction1 CharToNatSym0
sCharToNat

natToChar :: Natural -> Char
natToChar :: Natural -> Char
natToChar = Int -> Char
chr (Int -> Char) -> (Natural -> Int) -> Natural -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral

sNatToChar :: Sing x -> Sing (NatToChar x)
sNatToChar :: forall (x :: Natural). Sing x -> Sing (NatToChar x)
sNatToChar Sing x
sx =
    let x :: Demote Natural
x   = Sing x -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        res :: SomeChar
res = Char -> SomeChar
someCharVal (Natural -> Char
natToChar Natural
Demote Natural
x)
    in case SomeChar
res of
         SomeChar (Proxy n
_ :: Proxy res) -> SChar n -> SChar (NatToChar x)
forall a b. a -> b
unsafeCoerce (Sing n
forall (c :: Char). KnownChar c => SChar c
SChar :: Sing res)
$(genDefunSymbols [''NatToChar])
instance SingI NatToCharSym0 where
  sing :: Sing NatToCharSym0
sing = SingFunction1 NatToCharSym0 -> Sing NatToCharSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 forall (x :: Natural). Sing x -> Sing (NatToChar x)
SingFunction1 NatToCharSym0
sNatToChar