    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE CPP #-}
    -- | Utilities for working with 'KnownChar' constraints.
    --
    -- This module is only available on GHC 9.2 or later.
    module Data.Constraint.Char
      ( CharToNat
      , NatToChar
      , charToNat
      , natToChar
      ) where

    import Data.Char
    import Data.Constraint
    import Data.Proxy
    import GHC.TypeLits
    #if MIN_VERSION_base(4,18,0)
    import Data.Constraint.Unsafe
    import qualified GHC.TypeNats as TN
    #else
    import Unsafe.Coerce
    #endif

    -- implementation details

    #if !MIN_VERSION_base(4,18,0)
    newtype Magic c = Magic (KnownChar c => Dict (KnownChar c))
    #endif

    magicCN :: forall c n. (Char -> Int) -> KnownChar c :- KnownNat n
    #if MIN_VERSION_base(4,18,0)
    magicCN :: forall (c :: Char) (n :: Nat).
    (Char -> Int) -> KnownChar c :- KnownNat n
    magicCN Char -> Int
    f = (KnownChar c => Dict (KnownNat n)) -> KnownChar c :- KnownNat n
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((KnownChar c => Dict (KnownNat n)) -> KnownChar c :- KnownNat n)
    -> (KnownChar c => Dict (KnownNat n)) -> KnownChar c :- KnownNat n
    forall a b. (a -> b) -> a -> b
    $ SNat n -> (KnownNat n => Dict (KnownNat n)) -> Dict (KnownNat n)
    forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
    TN.withKnownNat (forall (n :: Nat). Nat -> SNat n
    unsafeSNat @n (Int -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Char -> Int
    f (Proxy c -> Char
    forall (n :: Char) (proxy :: Char -> *).
    KnownChar n =>
    proxy n -> Char
    charVal (forall (t :: Char). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @c))))) Dict (KnownNat n)
    KnownNat n => Dict (KnownNat n)
    forall (a :: Constraint). a => Dict a
    Dict
    #else
    magicCN f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral @Int @Natural (f (charVal (Proxy @c))))
    #endif

    magicNC :: forall n c. (Int -> Char) -> KnownNat n :- KnownChar c
    #if MIN_VERSION_base(4,18,0)
    magicNC :: forall (n :: Nat) (c :: Char).
    (Int -> Char) -> KnownNat n :- KnownChar c
    magicNC Int -> Char
    f = (KnownNat n => Dict (KnownChar c)) -> KnownNat n :- KnownChar c
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((KnownNat n => Dict (KnownChar c)) -> KnownNat n :- KnownChar c)
    -> (KnownNat n => Dict (KnownChar c)) -> KnownNat n :- KnownChar c
    forall a b. (a -> b) -> a -> b
    $ SChar c
    -> (KnownChar c => Dict (KnownChar c)) -> Dict (KnownChar c)
    forall (c :: Char) r. SChar c -> (KnownChar c => r) -> r
    withKnownChar (forall (c :: Char). Char -> SChar c
    unsafeSChar @c (Int -> Char
    f (Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n))))) Dict (KnownChar c)
    KnownChar c => Dict (KnownChar c)
    forall (a :: Constraint). a => Dict a
    Dict
    #else
    magicNC f = Sub $ unsafeCoerce (Magic Dict) (f (fromIntegral (natVal (Proxy @n))))
    #endif

    -- operations

    charToNat :: forall c. KnownChar c :- KnownNat (CharToNat c)
    charToNat :: forall (c :: Char). KnownChar c :- KnownNat (CharToNat c)
    charToNat = (Char -> Int) -> KnownChar c :- KnownNat (CharToNat c)
    forall (c :: Char) (n :: Nat).
    (Char -> Int) -> KnownChar c :- KnownNat n
    magicCN Char -> Int
    ord

    -- NB: 0x10FFFF the maximum value for a Unicode code point. Calling `chr` on
    -- anything greater will throw an exception.
    natToChar :: forall n. (n <= 0x10FFFF, KnownNat n) :- KnownChar (NatToChar n)
    natToChar :: forall (n :: Nat).
    (n <= 1114111, KnownNat n) :- KnownChar (NatToChar n)
    natToChar = ((n <= 1114111, KnownNat n) => Dict (KnownChar (NatToChar n)))
    -> (n <= 1114111, KnownNat n) :- KnownChar (NatToChar n)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (((n <= 1114111, KnownNat n) => Dict (KnownChar (NatToChar n)))
     -> (n <= 1114111, KnownNat n) :- KnownChar (NatToChar n))
    -> ((n <= 1114111, KnownNat n) => Dict (KnownChar (NatToChar n)))
    -> (n <= 1114111, KnownNat n) :- KnownChar (NatToChar n)
    forall a b. (a -> b) -> a -> b
    $ case forall (n :: Nat) (c :: Char).
    (Int -> Char) -> KnownNat n :- KnownChar c
    magicNC @n @(NatToChar n) Int -> Char
    chr of Sub KnownNat n => Dict (KnownChar (NatToChar n))
    r -> Dict (KnownChar (NatToChar n))
    KnownNat n => Dict (KnownChar (NatToChar n))
    r