{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Taiwan.ID.Unchecked
  ( UncheckedID (..)
  , UncheckedIDTuple
  , FromTextError (..)
  , fromText
  , toText
  , checksum
  , checksumValidity
  , ChecksumValidity (..)
  , ValidID
  )
  where

import Control.Monad
  ( when )
import Data.Kind
  ( Constraint )
import Data.List.NonEmpty
  ( NonEmpty ((:|)) )
import Data.Text
  ( Text )
import Data.Type.Bool
  ( If )
import Data.Type.Equality
  ( type (==) )
import GHC.TypeError
  ( Assert, TypeError )
import GHC.TypeLits
  ( AppendSymbol, KnownSymbol, Symbol )
import GHC.TypeNats
  ( CmpNat, Mod, Nat, type (+) )
import Taiwan.ID.CharIndex
  ( CharIndex (..) )
import Taiwan.ID.CharSet
  ( CharSet (..) )
import Taiwan.ID.Digit
  ( Digit (..) )
import Taiwan.ID.Digit1289
  ( Digit1289 (..) )
import Taiwan.ID.Letter
  ( Letter (..) )
import Taiwan.ID.Utilities
  ( FromJust, Fst, ReplicateChar, Snd, SymbolLength, SymbolToCharList, guard )

import qualified Data.Set.NonEmpty as NESet
import qualified Data.Text as T
import qualified GHC.TypeError as TypeError
import qualified GHC.TypeNats as N
import qualified Taiwan.ID.Digit as Digit
import qualified Taiwan.ID.Digit1289 as Digit1289
import qualified Taiwan.ID.Letter as Letter

data UncheckedID = UncheckedID
  { UncheckedID -> Letter
c0 :: !Letter
  , UncheckedID -> Digit1289
c1 :: !Digit1289
  , UncheckedID -> Digit
c2 :: !Digit
  , UncheckedID -> Digit
c3 :: !Digit
  , UncheckedID -> Digit
c4 :: !Digit
  , UncheckedID -> Digit
c5 :: !Digit
  , UncheckedID -> Digit
c6 :: !Digit
  , UncheckedID -> Digit
c7 :: !Digit
  , UncheckedID -> Digit
c8 :: !Digit
  , UncheckedID -> Digit
c9 :: !Digit
  }
  deriving stock (UncheckedID -> UncheckedID -> Bool
(UncheckedID -> UncheckedID -> Bool)
-> (UncheckedID -> UncheckedID -> Bool) -> Eq UncheckedID
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UncheckedID -> UncheckedID -> Bool
== :: UncheckedID -> UncheckedID -> Bool
$c/= :: UncheckedID -> UncheckedID -> Bool
/= :: UncheckedID -> UncheckedID -> Bool
Eq, Eq UncheckedID
Eq UncheckedID =>
(UncheckedID -> UncheckedID -> Ordering)
-> (UncheckedID -> UncheckedID -> Bool)
-> (UncheckedID -> UncheckedID -> Bool)
-> (UncheckedID -> UncheckedID -> Bool)
-> (UncheckedID -> UncheckedID -> Bool)
-> (UncheckedID -> UncheckedID -> UncheckedID)
-> (UncheckedID -> UncheckedID -> UncheckedID)
-> Ord UncheckedID
UncheckedID -> UncheckedID -> Bool
UncheckedID -> UncheckedID -> Ordering
UncheckedID -> UncheckedID -> UncheckedID
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: UncheckedID -> UncheckedID -> Ordering
compare :: UncheckedID -> UncheckedID -> Ordering
$c< :: UncheckedID -> UncheckedID -> Bool
< :: UncheckedID -> UncheckedID -> Bool
$c<= :: UncheckedID -> UncheckedID -> Bool
<= :: UncheckedID -> UncheckedID -> Bool
$c> :: UncheckedID -> UncheckedID -> Bool
> :: UncheckedID -> UncheckedID -> Bool
$c>= :: UncheckedID -> UncheckedID -> Bool
>= :: UncheckedID -> UncheckedID -> Bool
$cmax :: UncheckedID -> UncheckedID -> UncheckedID
max :: UncheckedID -> UncheckedID -> UncheckedID
$cmin :: UncheckedID -> UncheckedID -> UncheckedID
min :: UncheckedID -> UncheckedID -> UncheckedID
Ord, Int -> UncheckedID -> ShowS
[UncheckedID] -> ShowS
UncheckedID -> String
(Int -> UncheckedID -> ShowS)
-> (UncheckedID -> String)
-> ([UncheckedID] -> ShowS)
-> Show UncheckedID
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UncheckedID -> ShowS
showsPrec :: Int -> UncheckedID -> ShowS
$cshow :: UncheckedID -> String
show :: UncheckedID -> String
$cshowList :: [UncheckedID] -> ShowS
showList :: [UncheckedID] -> ShowS
Show)

type UncheckedIDTuple =
  ( Letter
  , Digit1289
  , Digit
  , Digit
  , Digit
  , Digit
  , Digit
  , Digit
  , Digit
  , Digit
  )

data FromTextError
  = InvalidChar CharIndex CharSet
  | InvalidLength
  deriving stock (FromTextError -> FromTextError -> Bool
(FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> Bool) -> Eq FromTextError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FromTextError -> FromTextError -> Bool
== :: FromTextError -> FromTextError -> Bool
$c/= :: FromTextError -> FromTextError -> Bool
/= :: FromTextError -> FromTextError -> Bool
Eq, Eq FromTextError
Eq FromTextError =>
(FromTextError -> FromTextError -> Ordering)
-> (FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> FromTextError)
-> (FromTextError -> FromTextError -> FromTextError)
-> Ord FromTextError
FromTextError -> FromTextError -> Bool
FromTextError -> FromTextError -> Ordering
FromTextError -> FromTextError -> FromTextError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FromTextError -> FromTextError -> Ordering
compare :: FromTextError -> FromTextError -> Ordering
$c< :: FromTextError -> FromTextError -> Bool
< :: FromTextError -> FromTextError -> Bool
$c<= :: FromTextError -> FromTextError -> Bool
<= :: FromTextError -> FromTextError -> Bool
$c> :: FromTextError -> FromTextError -> Bool
> :: FromTextError -> FromTextError -> Bool
$c>= :: FromTextError -> FromTextError -> Bool
>= :: FromTextError -> FromTextError -> Bool
$cmax :: FromTextError -> FromTextError -> FromTextError
max :: FromTextError -> FromTextError -> FromTextError
$cmin :: FromTextError -> FromTextError -> FromTextError
min :: FromTextError -> FromTextError -> FromTextError
Ord, ReadPrec [FromTextError]
ReadPrec FromTextError
Int -> ReadS FromTextError
ReadS [FromTextError]
(Int -> ReadS FromTextError)
-> ReadS [FromTextError]
-> ReadPrec FromTextError
-> ReadPrec [FromTextError]
-> Read FromTextError
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS FromTextError
readsPrec :: Int -> ReadS FromTextError
$creadList :: ReadS [FromTextError]
readList :: ReadS [FromTextError]
$creadPrec :: ReadPrec FromTextError
readPrec :: ReadPrec FromTextError
$creadListPrec :: ReadPrec [FromTextError]
readListPrec :: ReadPrec [FromTextError]
Read, Int -> FromTextError -> ShowS
[FromTextError] -> ShowS
FromTextError -> String
(Int -> FromTextError -> ShowS)
-> (FromTextError -> String)
-> ([FromTextError] -> ShowS)
-> Show FromTextError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FromTextError -> ShowS
showsPrec :: Int -> FromTextError -> ShowS
$cshow :: FromTextError -> String
show :: FromTextError -> String
$cshowList :: [FromTextError] -> ShowS
showList :: [FromTextError] -> ShowS
Show)

type Parser a = Text -> Either FromTextError (Text, a)

fromText :: Text -> Either FromTextError UncheckedID
fromText :: Text -> Either FromTextError UncheckedID
fromText Text
text0 = do
    Bool -> Either FromTextError () -> Either FromTextError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Text -> Int
T.length Text
text0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Either FromTextError () -> Either FromTextError ())
-> Either FromTextError () -> Either FromTextError ()
forall a b. (a -> b) -> a -> b
$ FromTextError -> Either FromTextError ()
forall a b. a -> Either a b
Left FromTextError
InvalidLength
    (text1,  c0                             ) <- Parser Letter
parseLetter    Text
text0
    (text2,  c1                             ) <- parseDigit1289 text1
    (_____, (c2, c3, c4, c5, c6, c7, c8, c9)) <- parseDigits    text2
    pure UncheckedID {c0, c1, c2, c3, c4, c5, c6, c7, c8, c9}
  where
    parseLetter :: Parser Letter
    parseLetter :: Parser Letter
parseLetter Text
text = do
      (char, remainder) <- FromTextError
-> Maybe (Char, Text) -> Either FromTextError (Char, Text)
forall x y. x -> Maybe y -> Either x y
guard FromTextError
InvalidLength (Maybe (Char, Text) -> Either FromTextError (Char, Text))
-> Maybe (Char, Text) -> Either FromTextError (Char, Text)
forall a b. (a -> b) -> a -> b
$ Text -> Maybe (Char, Text)
T.uncons Text
text
      letter <- guard (InvalidChar 0 (CharRange 'A' 'Z')) (Letter.fromChar char)
      pure (remainder, letter)

    parseDigit1289 :: Parser Digit1289
    parseDigit1289 :: Parser Digit1289
parseDigit1289 Text
text = do
      (char, remainder) <- FromTextError
-> Maybe (Char, Text) -> Either FromTextError (Char, Text)
forall x y. x -> Maybe y -> Either x y
guard FromTextError
InvalidLength (Maybe (Char, Text) -> Either FromTextError (Char, Text))
-> Maybe (Char, Text) -> Either FromTextError (Char, Text)
forall a b. (a -> b) -> a -> b
$ Text -> Maybe (Char, Text)
T.uncons Text
text
      digit1289 <- guard
        (InvalidChar 1 (CharSet $ NESet.fromList $ '1' :| ['2', '8', '9']))
        (Digit1289.fromChar char)
      pure (remainder, digit1289)

    parseDigits :: d ~ Digit => Parser (d, d, d, d, d, d, d, d)
    parseDigits :: forall d. (d ~ Digit) => Parser (d, d, d, d, d, d, d, d)
parseDigits Text
text = do
        let (Text
chars, Text
remainder) = Int -> Text -> (Text, Text)
T.splitAt Int
8 Text
text
        digitList <- ((CharIndex, Char) -> Either FromTextError Digit)
-> [(CharIndex, Char)] -> Either FromTextError [Digit]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (CharIndex, Char) -> Either FromTextError Digit
parseIndexedDigit ([CharIndex] -> String -> [(CharIndex, Char)]
forall a b. [a] -> [b] -> [(a, b)]
zip [CharIndex
2 ..] (String -> [(CharIndex, Char)]) -> String -> [(CharIndex, Char)]
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
chars)
        digitTuple <- guard InvalidLength (listToTuple8 digitList)
        pure (remainder, digitTuple)
      where
        parseIndexedDigit :: (CharIndex, Char) -> Either FromTextError Digit
parseIndexedDigit (CharIndex
i, Char
c) =
          FromTextError -> Maybe Digit -> Either FromTextError Digit
forall x y. x -> Maybe y -> Either x y
guard (CharIndex -> CharSet -> FromTextError
InvalidChar CharIndex
i (Char -> Char -> CharSet
CharRange Char
'0' Char
'9')) (Char -> Maybe Digit
Digit.fromChar Char
c)

toText :: UncheckedID -> Text
toText :: UncheckedID -> Text
toText UncheckedID {Letter
c0 :: UncheckedID -> Letter
c0 :: Letter
c0, Digit1289
c1 :: UncheckedID -> Digit1289
c1 :: Digit1289
c1, Digit
c2 :: UncheckedID -> Digit
c2 :: Digit
c2, Digit
c3 :: UncheckedID -> Digit
c3 :: Digit
c3, Digit
c4 :: UncheckedID -> Digit
c4 :: Digit
c4, Digit
c5 :: UncheckedID -> Digit
c5 :: Digit
c5, Digit
c6 :: UncheckedID -> Digit
c6 :: Digit
c6, Digit
c7 :: UncheckedID -> Digit
c7 :: Digit
c7, Digit
c8 :: UncheckedID -> Digit
c8 :: Digit
c8, Digit
c9 :: UncheckedID -> Digit
c9 :: Digit
c9} =
  String -> Text
T.pack
    ( Letter -> Char
Letter.toChar Letter
c0
    Char -> ShowS
forall a. a -> [a] -> [a]
: Digit1289 -> Char
Digit1289.toChar Digit1289
c1
    Char -> ShowS
forall a. a -> [a] -> [a]
: (Digit -> Char) -> [Digit] -> String
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Digit -> Char
Digit.toChar [Digit
c2, Digit
c3, Digit
c4, Digit
c5, Digit
c6, Digit
c7, Digit
c8, Digit
c9]
    )

checksum :: UncheckedID -> Digit
checksum :: UncheckedID -> Digit
checksum (UncheckedID Letter
u0 (Digit1289 -> Digit
Digit1289.toDigit -> Digit
u1) Digit
u2 Digit
u3 Digit
u4 Digit
u5 Digit
u6 Digit
u7 Digit
u8 Digit
u9) =
  [Digit] -> Digit
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Digit] -> Digit) -> [Digit] -> Digit
forall a b. (a -> b) -> a -> b
$ (Digit -> Digit -> Digit) -> [Digit] -> [Digit] -> [Digit]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Digit -> Digit -> Digit
forall a. Num a => a -> a -> a
(*)
    [ Digit
1,  Digit
9,  Digit
8,  Digit
7,  Digit
6,  Digit
5,  Digit
4,  Digit
3,  Digit
2,  Digit
1,  Digit
1]
    [Digit
a0, Digit
a1, Digit
u1, Digit
u2, Digit
u3, Digit
u4, Digit
u5, Digit
u6, Digit
u7, Digit
u8, Digit
u9]
  where
    (Digit
a0, Digit
a1) = Letter -> (Digit, Digit)
checksumLetterToDigitPair Letter
u0

checksumLetterToDigitPair :: Letter -> (Digit, Digit)
checksumLetterToDigitPair :: Letter -> (Digit, Digit)
checksumLetterToDigitPair = \case
  Letter
A -> (Digit
1, Digit
0); Letter
N -> (Digit
2, Digit
2)
  Letter
B -> (Digit
1, Digit
1); Letter
O -> (Digit
3, Digit
5)
  Letter
C -> (Digit
1, Digit
2); Letter
P -> (Digit
2, Digit
3)
  Letter
D -> (Digit
1, Digit
3); Letter
Q -> (Digit
2, Digit
4)
  Letter
E -> (Digit
1, Digit
4); Letter
R -> (Digit
2, Digit
5)
  Letter
F -> (Digit
1, Digit
5); Letter
S -> (Digit
2, Digit
6)
  Letter
G -> (Digit
1, Digit
6); Letter
T -> (Digit
2, Digit
7)
  Letter
H -> (Digit
1, Digit
7); Letter
U -> (Digit
2, Digit
8)
  Letter
I -> (Digit
3, Digit
4); Letter
V -> (Digit
2, Digit
9)
  Letter
J -> (Digit
1, Digit
8); Letter
W -> (Digit
3, Digit
2)
  Letter
K -> (Digit
1, Digit
9); Letter
X -> (Digit
3, Digit
0)
  Letter
L -> (Digit
2, Digit
0); Letter
Y -> (Digit
3, Digit
1)
  Letter
M -> (Digit
2, Digit
1); Letter
Z -> (Digit
3, Digit
3)

data ChecksumValidity
  = ChecksumValid
  | ChecksumInvalid
  deriving stock (ChecksumValidity -> ChecksumValidity -> Bool
(ChecksumValidity -> ChecksumValidity -> Bool)
-> (ChecksumValidity -> ChecksumValidity -> Bool)
-> Eq ChecksumValidity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ChecksumValidity -> ChecksumValidity -> Bool
== :: ChecksumValidity -> ChecksumValidity -> Bool
$c/= :: ChecksumValidity -> ChecksumValidity -> Bool
/= :: ChecksumValidity -> ChecksumValidity -> Bool
Eq, Int -> ChecksumValidity -> ShowS
[ChecksumValidity] -> ShowS
ChecksumValidity -> String
(Int -> ChecksumValidity -> ShowS)
-> (ChecksumValidity -> String)
-> ([ChecksumValidity] -> ShowS)
-> Show ChecksumValidity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ChecksumValidity -> ShowS
showsPrec :: Int -> ChecksumValidity -> ShowS
$cshow :: ChecksumValidity -> String
show :: ChecksumValidity -> String
$cshowList :: [ChecksumValidity] -> ShowS
showList :: [ChecksumValidity] -> ShowS
Show)

checksumValidity :: UncheckedID -> ChecksumValidity
checksumValidity :: UncheckedID -> ChecksumValidity
checksumValidity UncheckedID
u =
  case UncheckedID -> Digit
checksum UncheckedID
u of
    Digit
0 -> ChecksumValidity
ChecksumValid
    Digit
_ -> ChecksumValidity
ChecksumInvalid

listToTuple8 :: [a] -> Maybe (a, a, a, a, a, a, a, a)
listToTuple8 :: forall a. [a] -> Maybe (a, a, a, a, a, a, a, a)
listToTuple8 = \case
  [a
a0, a
a1, a
a2, a
a3, a
a4, a
a5, a
a6, a
a7] ->
    (a, a, a, a, a, a, a, a) -> Maybe (a, a, a, a, a, a, a, a)
forall a. a -> Maybe a
Just (a
a0, a
a1, a
a2, a
a3, a
a4, a
a5, a
a6, a
a7)
  [a]
_ ->
    Maybe (a, a, a, a, a, a, a, a)
forall a. Maybe a
Nothing

type family ChecksumValid (id :: UncheckedIDTuple) :: Constraint where
  ChecksumValid id =
    Assert
      (ChecksumDigit id == D0)
      (TypeError (TypeError.Text "ID has invalid checksum."))

type family ChecksumDigit (id :: UncheckedIDTuple) :: Digit where
  ChecksumDigit id = ChecksumDigitFromNat (Mod (Checksum id) 10)

type family ChecksumDigitFromNat (n :: Nat) :: Digit where
  ChecksumDigitFromNat n =
    FromJust
      (Digit.FromNat n)
      (TypeError (TypeError.Text "Expected natural number between 0 and 9."))

type family Checksum (id :: UncheckedIDTuple) :: Nat where
  Checksum '(c0, c1, c2, c3, c4, c5, c6, c7, c8, c9) =
    (     (ChecksumLetterToNat0 c0 N.* 1)
      N.+ (ChecksumLetterToNat1 c0 N.* 9)
      N.+ (Digit1289.ToNat      c1 N.* 8)
      N.+ (Digit.ToNat          c2 N.* 7)
      N.+ (Digit.ToNat          c3 N.* 6)
      N.+ (Digit.ToNat          c4 N.* 5)
      N.+ (Digit.ToNat          c5 N.* 4)
      N.+ (Digit.ToNat          c6 N.* 3)
      N.+ (Digit.ToNat          c7 N.* 2)
      N.+ (Digit.ToNat          c8 N.* 1)
      N.+ (Digit.ToNat          c9 N.* 1)
    )

type family ChecksumLetterToNat0 (letter :: Letter) :: Nat where
  ChecksumLetterToNat0 x = Fst (ChecksumLetterToNatPair x)

type family ChecksumLetterToNat1 (letter :: Letter) :: Nat where
  ChecksumLetterToNat1 x = Snd (ChecksumLetterToNatPair x)

type family ChecksumLetterToNatPair (l :: Letter) :: (Nat, Nat) where
  ChecksumLetterToNatPair A = '(1, 0); ChecksumLetterToNatPair B = '(1, 1)
  ChecksumLetterToNatPair C = '(1, 2); ChecksumLetterToNatPair D = '(1, 3)
  ChecksumLetterToNatPair E = '(1, 4); ChecksumLetterToNatPair F = '(1, 5)
  ChecksumLetterToNatPair G = '(1, 6); ChecksumLetterToNatPair H = '(1, 7)
  ChecksumLetterToNatPair I = '(3, 4); ChecksumLetterToNatPair J = '(1, 8)
  ChecksumLetterToNatPair K = '(1, 9); ChecksumLetterToNatPair L = '(2, 0)
  ChecksumLetterToNatPair M = '(2, 1); ChecksumLetterToNatPair N = '(2, 2)
  ChecksumLetterToNatPair O = '(3, 5); ChecksumLetterToNatPair P = '(2, 3)
  ChecksumLetterToNatPair Q = '(2, 4); ChecksumLetterToNatPair R = '(2, 5)
  ChecksumLetterToNatPair S = '(2, 6); ChecksumLetterToNatPair T = '(2, 7)
  ChecksumLetterToNatPair U = '(2, 8); ChecksumLetterToNatPair V = '(2, 9)
  ChecksumLetterToNatPair W = '(3, 2); ChecksumLetterToNatPair X = '(3, 0)
  ChecksumLetterToNatPair Y = '(3, 1); ChecksumLetterToNatPair Z = '(3, 3)

type family SymbolToId (s :: Symbol) :: UncheckedIDTuple where
  SymbolToId s =
    IdFromCharList s (SymbolToCharList s)

type family
    IdFromCharList (id :: Symbol) (xs :: [Char]) :: UncheckedIDTuple
  where
    IdFromCharList id '[c0, c1, c2, c3, c4, c5, c6, c7, c8, c9] =
      '( LetterFromChar    id 0 c0
       , Digit1289FromChar id 1 c1
       , DigitFromChar     id 2 c2
       , DigitFromChar     id 3 c3
       , DigitFromChar     id 4 c4
       , DigitFromChar     id 5 c5
       , DigitFromChar     id 6 c6
       , DigitFromChar     id 7 c7
       , DigitFromChar     id 8 c8
       , DigitFromChar     id 9 c9
       )
    IdFromCharList _ _ =
      TypeError (TypeError.Text "An ID must have exactly 10 characters.")

type family
    DigitFromChar (id :: Symbol) (index :: Nat) (c :: Char) :: Digit
  where
    DigitFromChar id index c =
      FromJust
        (Digit.FromChar c)
        (InvalidCharError id index DigitTypeError)

type family
    Digit1289FromChar (id :: Symbol) (index :: Nat) (c :: Char) :: Digit1289
  where
    Digit1289FromChar id index c =
      FromJust
        (Digit1289.FromChar c)
        (InvalidCharError id index Digit1289TypeError)

type family
    LetterFromChar (id :: Symbol) (index :: Nat) (c :: Char) :: Letter
  where
    LetterFromChar id index c =
      FromJust
        (Letter.FromChar c)
        (InvalidCharError id index LetterTypeError)

type DigitTypeError =
  "Character at this position must be a digit in the range [0 .. 9]."

type Digit1289TypeError =
  "Character at this position must be a digit from the set {1, 2, 8, 9}."

type LetterTypeError =
  "Character at this position must be an uppercase letter."

type family InvalidCharError
    (invalidId :: Symbol) (charIndex :: Nat) (message :: Symbol)
  where
    InvalidCharError invalidId charIndex message =
      TypeError
        ( TypeError.ShowType invalidId
          TypeError.:$$:
          TypeError.Text (ReplicateChar (charIndex + 1) ' ' `AppendSymbol` "^")
          TypeError.:$$:
          TypeError.Text message
        )

type ValidID s =
  ( KnownSymbol s
  , ChecksumValid (SymbolToId (ConcreteSymbol s))
  ) :: Constraint

-- | Ensures the existence of a concrete symbol, or else raises a type error.
--
type family ConcreteSymbol (s :: Symbol) :: Symbol where
  -- If we can compute the symbol's length, then we have a concrete symbol.
  ConcreteSymbol s =
    If
      (CmpNat (SymbolLength s) 0 == GT)
      s
      (TypeError (TypeError.Text ConcreteSymbolError))

type ConcreteSymbolError =
  "Expected a type-level symbol of the form \"A123456789\"."