    -----------------------------------------------------------------------
    -- |
    -- Module           : What4.BaseTypes
    -- Description      : This module exports the types used in solver expressions.
    -- Copyright        : (c) Galois, Inc 2014-2020
    -- License          : BSD3
    -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
    -- Stability        : provisional
    --
    -- This module exports the types used in solver expressions.
    --
    -- These types are largely used as indexes to various GADTs and type
    -- families as a way to let the GHC typechecker help us keep expressions
    -- used by solvers apart.
    --
    -- In addition, we provide a value-level reification of the type
    -- indices that can be examined by pattern matching, called 'BaseTypeRepr'.
    ------------------------------------------------------------------------
    {-# LANGUAGE ConstraintKinds#-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    module What4.BaseTypes
      ( -- * BaseType data kind
        type BaseType
        -- ** Constructors for kind BaseType
      , BaseBoolType
      , BaseIntegerType
      , BaseRealType
      , BaseStringType
      , BaseBVType
      , BaseFloatType
      , BaseComplexType
      , BaseStructType
      , BaseArrayType
        -- * StringInfo data kind
      , StringInfo
        -- ** Constructors for StringInfo
      , Char8
      , Char16
      , Unicode
        -- * FloatPrecision data kind
      , type FloatPrecision
      , type FloatPrecisionBits
        -- ** Constructors for kind FloatPrecision
      , FloatingPointPrecision
        -- ** FloatingPointPrecision aliases
      , Prec16
      , Prec32
      , Prec64
      , Prec80
      , Prec128
        -- * Representations of base types
      , BaseTypeRepr(..)
      , FloatPrecisionRepr(..)
      , StringInfoRepr(..)
      , arrayTypeIndices
      , arrayTypeResult
      , floatPrecisionToBVType
      , lemmaFloatPrecisionIsPos
      , module Data.Parameterized.NatRepr

        -- * KnownRepr
      , KnownRepr(..)  -- Re-export from 'Data.Parameterized.Classes'
      , KnownCtx
      ) where

    import           Data.Hashable
    import           Data.Kind
    import           Data.Parameterized.Classes
    import qualified Data.Parameterized.Context as Ctx
    import           Data.Parameterized.NatRepr
    import           Data.Parameterized.TH.GADT
    import           GHC.TypeNats as TypeNats
    import           Prettyprinter

    --------------------------------------------------------------------------------
    -- KnownCtx

    -- | A Context where all the argument types are 'KnownRepr' instances
    type KnownCtx f = KnownRepr (Ctx.Assignment f)

    ------------------------------------------------------------------------
    -- StringInfo

    data StringInfo
         -- | 8-bit characters
       = Char8
         -- | 16-bit characters
       | Char16
         -- | Unicode code-points
       | Unicode

    type Char8   = 'Char8   -- ^ @:: 'StringInfo'@.
    type Char16  = 'Char16  -- ^ @:: 'StringInfo'@.
    type Unicode = 'Unicode -- ^ @:: 'StringInfo'@.

    ------------------------------------------------------------------------
    -- BaseType

    -- | This data kind enumerates the Crucible solver interface types,
    -- which are types that may be represented symbolically.
    data BaseType
         -- | @BaseBoolType@ denotes Boolean values.
       = BaseBoolType
         -- | @BaseIntegerType@ denotes an integer.
       | BaseIntegerType
         -- | @BaseRealType@ denotes a real number.
       | BaseRealType
         -- | @BaseBVType n@ denotes a bitvector with @n@-bits.
       | BaseBVType TypeNats.Nat
         -- | @BaseFloatType fpp@ denotes a floating-point number with @fpp@
         -- precision.
       | BaseFloatType FloatPrecision
         -- | @BaseStringType@ denotes a sequence of Unicode codepoints
       | BaseStringType StringInfo
         -- | @BaseComplexType@ denotes a complex number with real components.
       | BaseComplexType
         -- | @BaseStructType tps@ denotes a sequence of values with types @tps@.
       | BaseStructType (Ctx.Ctx BaseType)
         -- | @BaseArrayType itps rtp@ denotes a function mapping indices @itps@
         -- to values of type @rtp@.
         --
         -- It does not have bounds as one would normally expect from an
         -- array in a programming language, but the solver does provide
         -- operations for doing pointwise updates.
       | BaseArrayType  (Ctx.Ctx BaseType) BaseType

    type BaseBoolType    = 'BaseBoolType    -- ^ @:: 'BaseType'@.
    type BaseIntegerType = 'BaseIntegerType -- ^ @:: 'BaseType'@.
    type BaseRealType    = 'BaseRealType    -- ^ @:: 'BaseType'@.
    type BaseBVType      = 'BaseBVType      -- ^ @:: 'TypeNats.Nat' -> 'BaseType'@.
    type BaseFloatType   = 'BaseFloatType   -- ^ @:: 'FloatPrecision' -> 'BaseType'@.
    type BaseStringType  = 'BaseStringType  -- ^ @:: 'BaseType'@.
    type BaseComplexType = 'BaseComplexType -- ^ @:: 'BaseType'@.
    type BaseStructType  = 'BaseStructType  -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType'@.
    type BaseArrayType   = 'BaseArrayType   -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType' -> 'BaseType'@.

    -- | This data kind describes the types of floating-point formats.
    -- This consist of the standard IEEE 754-2008 binary floating point formats.
    data FloatPrecision where
      FloatingPointPrecision :: TypeNats.Nat   -- number of bits for the exponent field
                             -> TypeNats.Nat   -- number of bits for the significand field
                             -> FloatPrecision
    type FloatingPointPrecision = 'FloatingPointPrecision -- ^ @:: 'GHC.TypeNats.Nat' -> 'GHC.TypeNats.Nat' -> 'FloatPrecision'@.

    -- | This computes the number of bits occupied by a floating-point format.
    type family FloatPrecisionBits (fpp :: FloatPrecision) :: Nat where
      FloatPrecisionBits (FloatingPointPrecision eb sb) = eb + sb

    -- | Floating-point precision aliases
    type Prec16  = FloatingPointPrecision  5  11
    type Prec32  = FloatingPointPrecision  8  24
    type Prec64  = FloatingPointPrecision 11  53
    type Prec80  = FloatingPointPrecision 15  65
    type Prec128 = FloatingPointPrecision 15 113

    ------------------------------------------------------------------------
    -- BaseTypeRepr

    -- | A runtime representation of a solver interface type. Parameter @bt@
    -- has kind 'BaseType'.
    data BaseTypeRepr (bt::BaseType) :: Type where
       BaseBoolRepr    :: BaseTypeRepr BaseBoolType
       BaseBVRepr      :: (1 <= w) => !(NatRepr w) -> BaseTypeRepr (BaseBVType w)
       BaseIntegerRepr :: BaseTypeRepr BaseIntegerType
       BaseRealRepr    :: BaseTypeRepr BaseRealType
       BaseFloatRepr   :: !(FloatPrecisionRepr fpp) -> BaseTypeRepr (BaseFloatType fpp)
       BaseStringRepr  :: StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
       BaseComplexRepr :: BaseTypeRepr BaseComplexType

       -- The representation of a struct type.
       BaseStructRepr :: !(Ctx.Assignment BaseTypeRepr ctx)
                      -> BaseTypeRepr (BaseStructType ctx)

       BaseArrayRepr :: !(Ctx.Assignment BaseTypeRepr (idx Ctx.::> tp))
                     -> !(BaseTypeRepr xs)
                     -> BaseTypeRepr (BaseArrayType (idx Ctx.::> tp) xs)

    data FloatPrecisionRepr (fpp :: FloatPrecision) where
      FloatingPointPrecisionRepr
        :: (2 <= eb, 2 <= sb)
        => !(NatRepr eb)
        -> !(NatRepr sb)
        -> FloatPrecisionRepr (FloatingPointPrecision eb sb)

    data StringInfoRepr (si::StringInfo) where
      Char8Repr     :: StringInfoRepr Char8
      Char16Repr    :: StringInfoRepr Char16
      UnicodeRepr   :: StringInfoRepr Unicode

    -- | Return the type of the indices for an array type.
    arrayTypeIndices :: BaseTypeRepr (BaseArrayType idx tp)
                     -> Ctx.Assignment BaseTypeRepr idx
    arrayTypeIndices :: forall (idx :: Ctx BaseType) (tp :: BaseType).
    BaseTypeRepr (BaseArrayType idx tp) -> Assignment BaseTypeRepr idx
    arrayTypeIndices (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    i BaseTypeRepr xs
    _) = Assignment BaseTypeRepr idx
    Assignment BaseTypeRepr (idx ::> tp)
    i

    -- | Return the result type of an array type.
    arrayTypeResult :: BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp
    arrayTypeResult :: forall (idx :: Ctx BaseType) (tp :: BaseType).
    BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp
    arrayTypeResult (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    _ BaseTypeRepr xs
    rtp) = BaseTypeRepr tp
    BaseTypeRepr xs
    rtp

    floatPrecisionToBVType
      :: FloatPrecisionRepr (FloatingPointPrecision eb sb)
      -> BaseTypeRepr (BaseBVType (eb + sb))
    floatPrecisionToBVType :: forall (eb :: Nat) (sb :: Nat).
    FloatPrecisionRepr (FloatingPointPrecision eb sb)
    -> BaseTypeRepr (BaseBVType (eb + sb))
    floatPrecisionToBVType fpp :: FloatPrecisionRepr (FloatingPointPrecision eb sb)
    fpp@(FloatingPointPrecisionRepr NatRepr eb
    eb NatRepr sb
    sb)
      | LeqProof 1 (eb + sb)
    LeqProof <- FloatPrecisionRepr (FloatingPointPrecision eb sb)
    -> LeqProof 1 (eb + sb)
    forall (eb' :: Nat) (sb' :: Nat).
    FloatPrecisionRepr (FloatingPointPrecision eb' sb')
    -> LeqProof 1 (eb' + sb')
    lemmaFloatPrecisionIsPos FloatPrecisionRepr (FloatingPointPrecision eb sb)
    fpp
      = NatRepr (eb + sb) -> BaseTypeRepr (BaseBVType (eb + sb))
    forall (eb :: Nat).
    (1 <= eb) =>
    NatRepr eb -> BaseTypeRepr (BaseBVType eb)
    BaseBVRepr (NatRepr (eb + sb) -> BaseTypeRepr (BaseBVType (eb + sb)))
    -> NatRepr (eb + sb) -> BaseTypeRepr (BaseBVType (eb + sb))
    forall a b. (a -> b) -> a -> b
    $ NatRepr eb -> NatRepr sb -> NatRepr (eb + sb)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr eb
    eb NatRepr sb
    sb

    lemmaFloatPrecisionIsPos
      :: forall eb' sb'
       . FloatPrecisionRepr (FloatingPointPrecision eb' sb')
      -> LeqProof 1 (eb' + sb')
    lemmaFloatPrecisionIsPos :: forall (eb' :: Nat) (sb' :: Nat).
    FloatPrecisionRepr (FloatingPointPrecision eb' sb')
    -> LeqProof 1 (eb' + sb')
    lemmaFloatPrecisionIsPos (FloatingPointPrecisionRepr NatRepr eb
    eb NatRepr sb
    sb)
      | LeqProof 1 eb'
    LeqProof <- LeqProof 1 2 -> LeqProof 2 eb' -> LeqProof 1 eb'
    forall (m :: Nat) (n :: Nat) (p :: Nat).
    LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans (forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
    LeqProof @1 @2) (forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
    LeqProof @2 @eb')
      , LeqProof 1 sb'
    LeqProof <- LeqProof 1 2 -> LeqProof 2 sb' -> LeqProof 1 sb'
    forall (m :: Nat) (n :: Nat) (p :: Nat).
    LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans (forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
    LeqProof @1 @2) (forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
    LeqProof @2 @sb')
      = NatRepr eb -> NatRepr sb -> LeqProof 1 (eb + sb)
    forall (m :: Nat) (n :: Nat) (p :: Nat -> Type) (q :: Nat -> Type).
    (1 <= m, 1 <= n) =>
    p m -> q n -> LeqProof 1 (m + n)
    leqAddPos NatRepr eb
    eb NatRepr sb
    sb

    instance KnownRepr BaseTypeRepr BaseBoolType where
      knownRepr :: BaseTypeRepr BaseBoolType
    knownRepr = BaseTypeRepr BaseBoolType
    BaseBoolRepr
    instance KnownRepr BaseTypeRepr BaseIntegerType where
      knownRepr :: BaseTypeRepr BaseIntegerType
    knownRepr = BaseTypeRepr BaseIntegerType
    BaseIntegerRepr
    instance KnownRepr BaseTypeRepr BaseRealType where
      knownRepr :: BaseTypeRepr BaseRealType
    knownRepr = BaseTypeRepr BaseRealType
    BaseRealRepr
    instance KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si) where
      knownRepr :: BaseTypeRepr (BaseStringType si)
    knownRepr = StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
    forall (eb :: StringInfo).
    StringInfoRepr eb -> BaseTypeRepr (BaseStringType eb)
    BaseStringRepr StringInfoRepr si
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
    instance (1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w) where
      knownRepr :: BaseTypeRepr (BaseBVType w)
    knownRepr = NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (eb :: Nat).
    (1 <= eb) =>
    NatRepr eb -> BaseTypeRepr (BaseBVType eb)
    BaseBVRepr NatRepr w
    forall (n :: Nat). KnownNat n => NatRepr n
    knownNat
    instance (KnownRepr FloatPrecisionRepr fpp) => KnownRepr BaseTypeRepr (BaseFloatType fpp) where
      knownRepr :: BaseTypeRepr (BaseFloatType fpp)
    knownRepr = FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
    forall (eb :: FloatPrecision).
    FloatPrecisionRepr eb -> BaseTypeRepr (BaseFloatType eb)
    BaseFloatRepr FloatPrecisionRepr fpp
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
    instance KnownRepr BaseTypeRepr BaseComplexType where
      knownRepr :: BaseTypeRepr BaseComplexType
    knownRepr = BaseTypeRepr BaseComplexType
    BaseComplexRepr

    instance KnownRepr (Ctx.Assignment BaseTypeRepr) ctx
          => KnownRepr BaseTypeRepr (BaseStructType ctx) where
      knownRepr :: BaseTypeRepr (BaseStructType ctx)
    knownRepr = Assignment BaseTypeRepr ctx -> BaseTypeRepr (BaseStructType ctx)
    forall (eb :: Ctx BaseType).
    Assignment BaseTypeRepr eb -> BaseTypeRepr (BaseStructType eb)
    BaseStructRepr Assignment BaseTypeRepr ctx
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

    instance ( KnownRepr (Ctx.Assignment BaseTypeRepr) idx
             , KnownRepr BaseTypeRepr tp
             , KnownRepr BaseTypeRepr t
             )
          => KnownRepr BaseTypeRepr (BaseArrayType (idx Ctx.::> tp) t) where
      knownRepr :: BaseTypeRepr (BaseArrayType (idx ::> tp) t)
    knownRepr = Assignment BaseTypeRepr (idx ::> tp)
    -> BaseTypeRepr t -> BaseTypeRepr (BaseArrayType (idx ::> tp) t)
    forall (eb :: Ctx BaseType) (sb :: BaseType) (xs :: BaseType).
    Assignment BaseTypeRepr (eb ::> sb)
    -> BaseTypeRepr xs -> BaseTypeRepr (BaseArrayType (eb ::> sb) xs)
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr BaseTypeRepr t
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

    instance (2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es) where
      knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es)
    knownRepr = NatRepr eb
    -> NatRepr es -> FloatPrecisionRepr (FloatingPointPrecision eb es)
    forall (eb :: Nat) (sb :: Nat).
    (2 <= eb, 2 <= sb) =>
    NatRepr eb
    -> NatRepr sb -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
    FloatingPointPrecisionRepr NatRepr eb
    forall (n :: Nat). KnownNat n => NatRepr n
    knownNat NatRepr es
    forall (n :: Nat). KnownNat n => NatRepr n
    knownNat

    instance KnownRepr StringInfoRepr Char8 where
      knownRepr :: StringInfoRepr Char8
    knownRepr = StringInfoRepr Char8
    Char8Repr
    instance KnownRepr StringInfoRepr Char16 where
      knownRepr :: StringInfoRepr Char16
    knownRepr = StringInfoRepr Char16
    Char16Repr
    instance KnownRepr StringInfoRepr Unicode where
      knownRepr :: StringInfoRepr Unicode
    knownRepr = StringInfoRepr Unicode
    UnicodeRepr

    -- Force BaseTypeRepr, etc. to be in context for next slice.
    $(return [])

    instance HashableF BaseTypeRepr where
      hashWithSaltF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> Int
    hashWithSaltF = Int -> BaseTypeRepr tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt
    instance Hashable (BaseTypeRepr bt) where
      hashWithSalt :: Int -> BaseTypeRepr bt -> Int
    hashWithSalt = $(structuralHashWithSalt [t|BaseTypeRepr|] [])

    instance HashableF FloatPrecisionRepr where
      hashWithSaltF :: forall (tp :: FloatPrecision). Int -> FloatPrecisionRepr tp -> Int
    hashWithSaltF = Int -> FloatPrecisionRepr tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt
    instance Hashable (FloatPrecisionRepr fpp) where
      hashWithSalt :: Int -> FloatPrecisionRepr fpp -> Int
    hashWithSalt = $(structuralHashWithSalt [t|FloatPrecisionRepr|] [])

    instance HashableF StringInfoRepr where
      hashWithSaltF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> Int
    hashWithSaltF = Int -> StringInfoRepr tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt
    instance Hashable (StringInfoRepr si) where
      hashWithSalt :: Int -> StringInfoRepr si -> Int
    hashWithSalt = $(structuralHashWithSalt [t|StringInfoRepr|] [])

    instance Pretty (BaseTypeRepr bt) where
      pretty :: forall ann. BaseTypeRepr bt -> Doc ann
    pretty = BaseTypeRepr bt -> Doc ann
    forall a ann. Show a => a -> Doc ann
    viaShow
    instance Show (BaseTypeRepr bt) where
      showsPrec :: Int -> BaseTypeRepr bt -> ShowS
    showsPrec = $(structuralShowsPrec [t|BaseTypeRepr|])
    instance ShowF BaseTypeRepr

    instance Pretty (FloatPrecisionRepr fpp) where
      pretty :: forall ann. FloatPrecisionRepr fpp -> Doc ann
    pretty = FloatPrecisionRepr fpp -> Doc ann
    forall a ann. Show a => a -> Doc ann
    viaShow
    instance Show (FloatPrecisionRepr fpp) where
      showsPrec :: Int -> FloatPrecisionRepr fpp -> ShowS
    showsPrec = $(structuralShowsPrec [t|FloatPrecisionRepr|])
    instance ShowF FloatPrecisionRepr

    instance Pretty (StringInfoRepr si) where
      pretty :: forall ann. StringInfoRepr si -> Doc ann
    pretty = StringInfoRepr si -> Doc ann
    forall a ann. Show a => a -> Doc ann
    viaShow
    instance Show (StringInfoRepr si) where
      showsPrec :: Int -> StringInfoRepr si -> ShowS
    showsPrec = $(structuralShowsPrec [t|StringInfoRepr|])
    instance ShowF StringInfoRepr

    instance TestEquality BaseTypeRepr where
      testEquality :: forall (a :: BaseType) (b :: BaseType).
    BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
    testEquality = $(structuralTypeEquality [t|BaseTypeRepr|]
                       [ (TypeApp (ConType [t|NatRepr|]) AnyType, [|testEquality|])
                       , (TypeApp (ConType [t|FloatPrecisionRepr|]) AnyType, [|testEquality|])
                       , (TypeApp (ConType [t|StringInfoRepr|]) AnyType, [|testEquality|])
                       , (TypeApp (ConType [t|BaseTypeRepr|]) AnyType, [|testEquality|])
                       , ( TypeApp (TypeApp (ConType [t|Ctx.Assignment|]) AnyType) AnyType
                         , [|testEquality|]
                         )
                       ]
                      )
    instance Eq (BaseTypeRepr bt) where
      BaseTypeRepr bt
    x == :: BaseTypeRepr bt -> BaseTypeRepr bt -> Bool
    == BaseTypeRepr bt
    y = Maybe (bt :~: bt) -> Bool
    forall a. Maybe a -> Bool
    isJust (BaseTypeRepr bt -> BaseTypeRepr bt -> Maybe (bt :~: bt)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
    testEquality BaseTypeRepr bt
    x BaseTypeRepr bt
    y)

    instance OrdF BaseTypeRepr where
      compareF :: forall (x :: BaseType) (y :: BaseType).
    BaseTypeRepr x -> BaseTypeRepr y -> OrderingF x y
    compareF = $(structuralTypeOrd [t|BaseTypeRepr|]
                       [ (TypeApp (ConType [t|NatRepr|]) AnyType, [|compareF|])
                       , (TypeApp (ConType [t|FloatPrecisionRepr|]) AnyType, [|compareF|])
                       , (TypeApp (ConType [t|StringInfoRepr|]) AnyType, [|compareF|])
                       , (TypeApp (ConType [t|BaseTypeRepr|]) AnyType, [|compareF|])
                       , (TypeApp (TypeApp (ConType [t|Ctx.Assignment|]) AnyType) AnyType
                         , [|compareF|]
                         )
                       ]
                      )

    instance TestEquality FloatPrecisionRepr where
      testEquality :: forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality = $(structuralTypeEquality [t|FloatPrecisionRepr|]
          [(TypeApp (ConType [t|NatRepr|]) AnyType, [|testEquality|])]
        )
    instance Eq (FloatPrecisionRepr fpp) where
      FloatPrecisionRepr fpp
    x == :: FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> Bool
    == FloatPrecisionRepr fpp
    y = Maybe (fpp :~: fpp) -> Bool
    forall a. Maybe a -> Bool
    isJust (FloatPrecisionRepr fpp
    -> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality FloatPrecisionRepr fpp
    x FloatPrecisionRepr fpp
    y)
    instance OrdF FloatPrecisionRepr where
      compareF :: forall (x :: FloatPrecision) (y :: FloatPrecision).
    FloatPrecisionRepr x -> FloatPrecisionRepr y -> OrderingF x y
    compareF = $(structuralTypeOrd [t|FloatPrecisionRepr|]
          [(TypeApp (ConType [t|NatRepr|]) AnyType, [|compareF|])]
        )

    instance TestEquality StringInfoRepr where
      testEquality :: forall (a :: StringInfo) (b :: StringInfo).
    StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b)
    testEquality = $(structuralTypeEquality [t|StringInfoRepr|] [])
    instance Eq (StringInfoRepr si) where
      StringInfoRepr si
    x == :: StringInfoRepr si -> StringInfoRepr si -> Bool
    == StringInfoRepr si
    y = Maybe (si :~: si) -> Bool
    forall a. Maybe a -> Bool
    isJust (StringInfoRepr si -> StringInfoRepr si -> Maybe (si :~: si)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: StringInfo) (b :: StringInfo).
    StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b)
    testEquality StringInfoRepr si
    x StringInfoRepr si
    y)
    instance OrdF StringInfoRepr where
      compareF :: forall (x :: StringInfo) (y :: StringInfo).
    StringInfoRepr x -> StringInfoRepr y -> OrderingF x y
    compareF = $(structuralTypeOrd [t|StringInfoRepr|] [])