Type-level prime number validation

Prime.hs

{-# LANGUAGE GADTs, DataKinds, UndecidableInstances, KindSignatures, TypeOperators, TypeFamilies #-}
module Prime where
import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeLits
import Data.Kind
import Data.Proxy

type family IsFactorization (n :: Nat) (l :: [Nat]) :: Bool where
    IsFactorization 0 l = False
    IsFactorization 1 '[] = True
    IsFactorization 1 l = False
    IsFactorization n (p ': l) = Mod n p == 0 && IsFactorizationSub n p l (Mod n p)
type family IsFactorizationSub n p l m where
    IsFactorizationSub 0 _ _ _ = TypeError (Text "Invalid argument 0")
    IsFactorizationSub n p l 0 = IsFactorizationSub (Div n p) p l (Mod (Div n p) p)
    IsFactorizationSub n p l _ = IsFactorization n l

type family ModPow (a :: Nat) (d :: Nat) (n :: Nat) :: Nat where
    ModPow a 0 n = 1
    ModPow a d n = ModPowSub a d n (Mod d 2 == 0)

type family ModPowSub a d n b where
    ModPowSub a d n True = Square (ModPow a (Div d 2) n) n
    ModPowSub a d n False =
        Mod (Square (ModPow a (Div d 2) n) n GHC.TypeLits.* a) n

type family Square a n where
    Square 1 n = 1
    Square 0 n = 0
    Square a n = Mod (a GHC.TypeLits.* a) n

type family IsPrimeCert (n :: Nat) (l :: [Nat]) (a :: Nat) :: Bool
    where
    IsPrimeCert n l a = ModPow a (n - 1) n == 1 && IsPrimeCertSub n l a

type family IsPrimeCertSub n l a
    where
    IsPrimeCertSub n '[] a = True
    IsPrimeCertSub n (p ':l) a = 
        Not (ModPow a (Div (n - 1) p) n == 1) && IsPrimeCertSub n l a

type family CheckPrimeCert (n :: Nat) (l :: [Nat]) (a :: Nat) :: Constraint
    where
    CheckPrimeCert n l a =
        (
        ((IsFactorization (n - 1) l
          || TypeError (ShowType l :<>: Text " is not the prime factors of ":<>: ShowType n))
        &&
        (IsPrimeCert n l a
          || TypeError (ShowType a :<>: Text " is not a generator of the multiplicative group modulo " :<>: ShowType n))) ~ True)

type family KnownPrimes l :: Constraint where
    KnownPrimes '[] = () 
    KnownPrimes (p:ps) = (KnownPrime p, KnownPrimes ps)

class KnownPrime n where
  primeCert :: PrimeCert n

data PrimeCert (n :: Nat) where
  PrimeCert :: CheckPrimeCert n l a => Proxy l -> Proxy a -> PrimeCert n