content: -----------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.Types
  -- Description      : This module exports the types used in Crucible
  --                    expressions.
  -- Copyright        : (c) Galois, Inc 2014
  -- License          : BSD3
  -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
  -- Stability        : provisional
  --
  -- This module exports the types used in Crucible 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
  -- of the embedded CFG language apart.
  --
  -- In addition, we provide a value-level reification of the type
  -- indices that can be examined by pattern matching, called 'TypeRepr'.
  -- The 'KnownRepr' class computes the value-level representation
  -- of a given type index, when the type is known at compile time.
  -- Similar setups exist for other components of the type system:
  -- bitvector data and type contexts.
  ------------------------------------------------------------------------
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE EmptyDataDecls #-}
  {-# LANGUAGE ExistentialQuantification #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE ViewPatterns #-}
  module Lang.Crucible.Types
    ( -- * CrucibleType data kind
      type CrucibleType
      -- ** Constructors for kind CrucibleType
    , AnyType
    , UnitType
    , BoolType
    , NatType
    , IntegerType
    , RealValType
    , SymbolicStructType
    , ComplexRealType
    , BVType
    , FloatType
    , IEEEFloatType
    , CharType
    , StringType
    , FunctionHandleType
    , MaybeType
    , RecursiveType
    , IntrinsicType
    , VectorType
    , SequenceType
    , StructType
    , VariantType
    , ReferenceType
    , WordMapType
  
    , StringMapType
    , SymbolicArrayType
  
      -- * IsRecursiveType
    , IsRecursiveType(..)
  
      -- * Base type injection
    , BaseToType
    , baseToType
  
    , AsBaseType(..)
    , asBaseType
  
      -- * Other stuff
    , CtxRepr
    , pattern KnownBV
    , ppTypeRepr
    , ppIntrinsicDefault
  
      -- * Representation of Crucible types
    , TypeRepr(..)
  
      -- * Re-exports
    , module Data.Parameterized.Ctx
    , module Data.Parameterized.NatRepr
    , module Data.Parameterized.SymbolRepr
    , module What4.BaseTypes
    , module What4.InterpretedFloatingPoint
    ) where
  
  import           Data.Functor.Identity (Identity(..))
  import           Data.Hashable
  import           Data.Type.Equality
  import           GHC.TypeNats (Nat, KnownNat)
  import           Data.Parameterized.Classes
  import qualified Data.Parameterized.Context as Ctx
  import           Data.Parameterized.Ctx
  import           Data.Parameterized.NatRepr
  import           Data.Parameterized.SymbolRepr
  import qualified Data.Parameterized.TH.GADT as U
  import           Data.Parameterized.TraversableFC
  import           Prettyprinter
  
  import           What4.BaseTypes
  import           What4.InterpretedFloatingPoint
  
  ------------------------------------------------------------------------
  -- Crucible types
  
  
  -- | This typeclass is used to register recursive Crucible types
  --   with the compiler.  This class defines, for a given symbol,
  --   both the type-level and the representative-level unrolling
  --   of a named recursive type.
  --
  --   The symbol constitutes a unique compile-time identifier for the
  --   recursive type, allowing recursive types to be unrolled at run
  --   time without requiring dynamic checks.
  --
  --   Parameter @nm@ has kind 'Symbol'.
  class IsRecursiveType (nm::Symbol) where
    type UnrollType nm (ctx :: Ctx CrucibleType) :: CrucibleType
    unrollType :: SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
  
  type CtxRepr = Ctx.Assignment TypeRepr
  
  -- | This data kind describes the types of values and expressions that
  --   can occur in Crucible CFGs.
  data CrucibleType where
     -- | An injection of solver interface types into Crucible types
     BaseToType :: BaseType -> CrucibleType
  
     -- | A dynamic type that can contain values of any type.
     AnyType :: CrucibleType
  
     -- | A type containing a single value "Unit"
     UnitType :: CrucibleType
  
     -- | A type for natural numbers.
     NatType :: CrucibleType
  
     -- | A type index for floating point numbers, whose interpretation
     --   depends on the symbolic backend.
     FloatType :: FloatInfo -> CrucibleType
     -- | A single character, as a 16-bit wide char.
     CharType :: CrucibleType
     -- | A function handle taking a context of formal arguments and a return type
     FunctionHandleType :: Ctx CrucibleType -> CrucibleType -> CrucibleType
  
     -- The Maybe type lifted into crucible expressions
     MaybeType :: CrucibleType -> CrucibleType
  
     -- A finite (one-dimensional) sequence of values.  Vectors are
     -- optimized for random-access indexing and updating.  Vectors
     -- of different lengths may not be combined at join points.
     VectorType :: CrucibleType -> CrucibleType
  
     -- Sequences of values, represented as linked lists of cons cells.  Sequences
     -- only allow access to the front. Unlike Vectors, sequences of
     -- different lengths may be combined at join points.
     SequenceType :: CrucibleType -> CrucibleType
  
     -- A structure is an aggregate type consisting of a sequence of values.
     -- The type of each value is known statically.
     StructType :: Ctx CrucibleType -> CrucibleType
  
     -- The type of mutable reference cells.
     ReferenceType :: CrucibleType -> CrucibleType
  
     -- A variant is a disjoint union of the types listed in the context.
     VariantType :: Ctx CrucibleType -> CrucibleType
  
     -- A finite map from bitvector values to the given crucible type.
     -- The nat index gives the width of the bitvector values used to index
     -- the map.
     WordMapType :: Nat -> BaseType -> CrucibleType
  
     -- Named recursive types, named by the given symbol.  To use recursive types
     -- you must provide an instance of the IsRecursiveType class that gives
     -- the unfolding of this recursive type.  The RollRecursive and UnrollRecursive
     -- operations witness the isomorphism between a recursive type and its one-step
     -- unrolling.  Similar to Haskell's newtype, recursive types do not necessarily
     -- have to mention the recursive type being defined; in which case, the type
     -- is simply a new named type which is isomorphic to its definition.
     RecursiveType :: Symbol -> Ctx CrucibleType -> CrucibleType
  
     -- Named intrinsic types.  Intrinsic types are a way to extend the
     -- crucible type system after-the-fact and add new type
     -- implementations.  Core crucible provides no operations on
     -- intrinsic types; they must be provided as built-in override
     -- functions, or via the language extension mechanism.  See the
     -- `IntrinsicClass` typeclass and the `Intrinsic` type family
     -- defined in "Lang.Crucible.Simulator.Intrinsics".
     --
     -- The context of crucible types are type arguments to the intrinsic type.
     IntrinsicType :: Symbol -> Ctx CrucibleType -> CrucibleType
  
     -- A partial map from strings to values.
     StringMapType :: CrucibleType -> CrucibleType
  
  type BaseToType      = 'BaseToType                -- ^ @:: 'BaseType' -> 'CrucibleType'@.
  type BoolType        = BaseToType BaseBoolType    -- ^ @:: 'CrucibleType'@.
  type BVType w        = BaseToType (BaseBVType w)  -- ^ @:: 'Nat' -> 'CrucibleType'@.
  type ComplexRealType = BaseToType BaseComplexType -- ^ @:: 'CrucibleType'@.
  type IntegerType     = BaseToType BaseIntegerType -- ^ @:: 'CrucibleType'@.
  type StringType si   = BaseToType (BaseStringType si) -- ^ @:: 'StringInfo' -> 'CrucibleType'@.
  type RealValType     = BaseToType BaseRealType    -- ^ @:: 'CrucibleType'@.
  type IEEEFloatType p = BaseToType (BaseFloatType p) -- ^ @:: FloatPrecision -> CrucibleType@
  
  type SymbolicArrayType idx xs = BaseToType (BaseArrayType idx xs) -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType' -> 'CrucibleType'@.
  type SymbolicStructType flds = BaseToType (BaseStructType flds) -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'CrucibleType'@.
  
  
  -- | A dynamic type that can contain values of any type.
  type AnyType  = 'AnyType  -- ^ @:: 'CrucibleType'@.
  
  -- | A single character, as a 16-bit wide char.
  type CharType = 'CharType -- ^ @:: 'CrucibleType'@.
  
  -- | A type index for floating point numbers, whose interpretation
  --   depends on the symbolic backend.
  type FloatType    = 'FloatType    -- ^ @:: 'FloatInfo' -> 'CrucibleType'@.
  
  
  -- | A function handle taking a context of formal arguments and a return type.
  type FunctionHandleType = 'FunctionHandleType -- ^ @:: 'Ctx' 'CrucibleType' -> 'CrucibleType' -> 'CrucibleType'@.
  
  -- | Named recursive types, named by the given symbol. To use
  -- recursive types you must provide an instance of the
  -- 'IsRecursiveType' class that gives the unfolding of this recursive
  -- type. The 'Lang.Crucible.CFG.Expr.RollRecursive' and
  -- 'Lang.Crucible.CFG.Expr.UnrollRecursive' operations witness the
  -- isomorphism between a recursive type and its one-step unrolling.
  -- Similar to Haskell's @newtype@, recursive types do not necessarily
  -- have to mention the recursive type being defined; in which case,
  -- the type is simply a new named type which is isomorphic to its
  -- definition.
  type RecursiveType = 'RecursiveType -- ^ @:: 'Symbol' -> 'Ctx' 'CrucibleType' -> 'CrucibleType'@.
  
  -- | Named intrinsic types. Intrinsic types are a way to extend the
  -- Crucible type system after-the-fact and add new type
  -- implementations. Core Crucible provides no operations on intrinsic
  -- types; they must be provided as built-in override functions. See
  -- the 'Lang.Crucible.Simulator.Intrinsics.IntrinsicClass' typeclass
  -- and the 'Lang.Crucible.Simulator.Intrinsics.Intrinsic' type family
  -- defined in "Lang.Crucible.Simulator.Intrinsics".
  type IntrinsicType ctx = 'IntrinsicType ctx -- ^ @:: 'Symbol' -> 'Ctx' 'CrucibleType' -> 'CrucibleType'@.
  
  -- | The type of mutable reference cells.
  type ReferenceType = 'ReferenceType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.
  
  -- | The 'Maybe' type lifted into Crucible expressions.
  type MaybeType = 'MaybeType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.
  
  -- | A partial map from strings to values.
  type StringMapType = 'StringMapType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.
  
  -- | A structure is an aggregate type consisting of a sequence of
  -- values. The type of each value is known statically.
  type StructType = 'StructType -- ^ @:: 'Ctx' 'CrucibleType' -> 'CrucibleType'@.
  
  -- | A type containing a single value "Unit".
  type UnitType      = 'UnitType      -- ^ @:: 'CrucibleType'@.
  
  -- | A type for natural numbers.
  type NatType       = 'NatType       -- ^ @:: 'CrucibleType'@.
  
  -- | A variant is a disjoint union of the types listed in the context.
  type VariantType   = 'VariantType   -- ^ @:: 'Ctx' 'CrucibleType' -> 'CrucibleType'@.
  
  -- | A finite (one-dimensional) sequence of values.  Vectors are
  -- optimized for random-access indexing and updating.  Vectors
  -- of different lengths may not be combined at join points.
  type VectorType    = 'VectorType    -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.
  
  -- | Sequences of values, represented as linked lists of cons cells.  Sequences
  -- only allow access to the front. Unlike Vectors, sequences of
  -- different lengths may be combined at join points.
  type SequenceType  = 'SequenceType  -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.
  
  -- | A finite map from bitvector values to the given Crucible type.
  -- The 'Nat' index gives the width of the bitvector values used to
  -- index the map.
  type WordMapType   = 'WordMapType   -- ^ @:: 'Nat' -> 'BaseType' -> 'CrucibleType'@.
  
  ----------------------------------------------------------------
  -- Base Type Injection
  
  baseToType :: BaseTypeRepr bt -> TypeRepr (BaseToType bt)
  baseToType bt =
    case bt of
      BaseBoolRepr -> BoolRepr
      BaseIntegerRepr -> IntegerRepr
      BaseRealRepr -> RealValRepr
      BaseStringRepr si -> StringRepr si
      BaseBVRepr w -> BVRepr w
      BaseComplexRepr -> ComplexRealRepr
      BaseArrayRepr idx xs -> SymbolicArrayRepr idx xs
      BaseStructRepr flds -> SymbolicStructRepr flds
      BaseFloatRepr ps -> IEEEFloatRepr ps
  
  data AsBaseType tp where
    AsBaseType  :: tp ~ BaseToType bt => BaseTypeRepr bt -> AsBaseType tp
    NotBaseType :: AsBaseType tp
  
  asBaseType :: TypeRepr tp -> AsBaseType tp
  asBaseType tp =
    case tp of
      BoolRepr -> AsBaseType BaseBoolRepr
      IntegerRepr -> AsBaseType BaseIntegerRepr
      RealValRepr -> AsBaseType BaseRealRepr
      StringRepr si -> AsBaseType (BaseStringRepr si)
      BVRepr w -> AsBaseType (BaseBVRepr w)
      ComplexRealRepr -> AsBaseType BaseComplexRepr
      SymbolicArrayRepr idx xs ->
        AsBaseType (BaseArrayRepr idx xs)
      IEEEFloatRepr ps ->
        AsBaseType (BaseFloatRepr ps)
      SymbolicStructRepr flds -> AsBaseType (BaseStructRepr flds)
      _ -> NotBaseType
  
  ----------------------------------------------------------------
  -- Type representatives
  
  -- | A family of representatives for Crucible types. Parameter @tp@
  -- has kind 'CrucibleType'.
  data TypeRepr (tp::CrucibleType) where
     AnyRepr :: TypeRepr AnyType
     UnitRepr :: TypeRepr UnitType
     BoolRepr :: TypeRepr BoolType
     NatRepr  :: TypeRepr NatType
     IntegerRepr :: TypeRepr IntegerType
     RealValRepr :: TypeRepr RealValType
     ComplexRealRepr :: TypeRepr ComplexRealType
     BVRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
     IntrinsicRepr :: !(SymbolRepr nm)
                   -> !(CtxRepr ctx)
                   -> TypeRepr (IntrinsicType nm ctx)
     RecursiveRepr :: IsRecursiveType nm
                   => SymbolRepr nm
                   -> CtxRepr ctx
                   -> TypeRepr (RecursiveType nm ctx)
  
     -- | This is a representation of floats that works at known fixed
     -- mantissa and exponent widths, but the symbolic backend may pick
     -- the representation.
     FloatRepr :: !(FloatInfoRepr flt) -> TypeRepr (FloatType flt)
  
     -- | This is a float with user-definable mantissa and exponent that
     -- maps directly to the what4 base type.
     IEEEFloatRepr :: !(FloatPrecisionRepr ps) -> TypeRepr (IEEEFloatType ps)
  
     CharRepr :: TypeRepr CharType
     StringRepr :: StringInfoRepr si -> TypeRepr (StringType si)
     FunctionHandleRepr :: !(CtxRepr ctx)
                        -> !(TypeRepr ret)
                        -> TypeRepr (FunctionHandleType ctx ret)
  
     MaybeRepr   :: !(TypeRepr tp) -> TypeRepr (MaybeType tp)
     SequenceRepr:: !(TypeRepr tp) -> TypeRepr (SequenceType tp)
     VectorRepr  :: !(TypeRepr tp) -> TypeRepr (VectorType tp)
     StructRepr  :: !(CtxRepr ctx) -> TypeRepr (StructType ctx)
     VariantRepr :: !(CtxRepr ctx) -> TypeRepr (VariantType ctx)
     ReferenceRepr :: !(TypeRepr a) -> TypeRepr (ReferenceType a)
  
     WordMapRepr :: (1 <= n)
                 => !(NatRepr n)
                 -> !(BaseTypeRepr tp)
                 -> TypeRepr (WordMapType n tp)
  
     StringMapRepr :: !(TypeRepr tp) -> TypeRepr (StringMapType tp)
  
     SymbolicArrayRepr :: !(Ctx.Assignment BaseTypeRepr (idx::>tp))
                       -> !(BaseTypeRepr t)
                       -> TypeRepr (SymbolicArrayType (idx::>tp) t)
  
     -- A reference to a symbolic struct.
     SymbolicStructRepr :: Ctx.Assignment BaseTypeRepr ctx
                        -> TypeRepr (SymbolicStructType ctx)
  
  ------------------------------------------------------------------------------
  -- Representable class instances
  
  instance KnownRepr TypeRepr AnyType             where knownRepr = AnyRepr
  instance KnownRepr TypeRepr UnitType            where knownRepr = UnitRepr
  instance KnownRepr TypeRepr CharType            where knownRepr = CharRepr
  instance KnownRepr TypeRepr NatType             where knownRepr = NatRepr
  
  instance KnownRepr BaseTypeRepr bt => KnownRepr TypeRepr (BaseToType bt) where
    knownRepr = baseToType knownRepr
  
  instance KnownCtx TypeRepr ctx => KnownRepr TypeRepr (StructType ctx) where
    knownRepr = StructRepr knownRepr
  
  instance KnownCtx TypeRepr ctx => KnownRepr TypeRepr (VariantType ctx) where
    knownRepr = VariantRepr knownRepr
  
  instance KnownRepr TypeRepr a => KnownRepr TypeRepr (ReferenceType a) where
    knownRepr = ReferenceRepr knownRepr
  
  instance (KnownSymbol s, KnownCtx TypeRepr ctx) => KnownRepr TypeRepr (IntrinsicType s ctx) where
    knownRepr = IntrinsicRepr knownSymbol knownRepr
  
  instance (KnownSymbol s, KnownCtx TypeRepr ctx, IsRecursiveType s) => KnownRepr TypeRepr (RecursiveType s ctx) where
    knownRepr = RecursiveRepr knownSymbol knownRepr
  
  instance (1 <= w, KnownNat w, KnownRepr BaseTypeRepr tp)
        => KnownRepr TypeRepr (WordMapType w tp) where
    knownRepr = WordMapRepr (knownNat :: NatRepr w) (knownRepr :: BaseTypeRepr tp)
  
  instance (KnownCtx TypeRepr ctx, KnownRepr TypeRepr ret)
        => KnownRepr TypeRepr (FunctionHandleType ctx ret) where
    knownRepr = FunctionHandleRepr knownRepr knownRepr
  
  instance KnownRepr FloatInfoRepr flt => KnownRepr TypeRepr (FloatType flt) where
    knownRepr = FloatRepr knownRepr
  
  instance KnownRepr FloatPrecisionRepr ps => KnownRepr TypeRepr (IEEEFloatType ps) where
    knownRepr = IEEEFloatRepr knownRepr
  
  instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (VectorType tp) where
    knownRepr = VectorRepr knownRepr
  
  instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (SequenceType tp) where
    knownRepr = SequenceRepr knownRepr
  
  instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (MaybeType tp) where
    knownRepr = MaybeRepr knownRepr
  
  instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (StringMapType tp) where
    knownRepr = StringMapRepr knownRepr
  
  -- | Pattern synonym specifying bitvector TypeReprs.  Intended to be use
  --   with type applications, e.g., @KnownBV \@32@.
  pattern KnownBV :: forall n. (1 <= n, KnownNat n) => TypeRepr (BVType n)
  pattern KnownBV <- BVRepr (testEquality (knownRepr :: NatRepr n) -> Just Refl)
    where KnownBV = knownRepr
  
  ------------------------------------------------------------------------
  -- Misc typeclass instances
  
  -- Force TypeRepr, etc. to be in context for next slice.
  $(return [])
  
  instance HashableF TypeRepr where
    hashWithSaltF = hashWithSalt
  instance Hashable (TypeRepr ty) where
    hashWithSalt = $(U.structuralHashWithSalt [t|TypeRepr|] [])
  
  -- Helper, not exported
  prettyCtx ::
    Monad f =>
    -- | How to print 'IntrinsicRepr', see 'ppIntrinsicDefault'
    (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)) ->
    Ctx.Assignment TypeRepr ctx ->
    f (Doc ann)
  -- The following specialization is used in the 'Pretty' instance and doesn't
  -- need to generate code for (>>=), so it seems worth specializing for it.
  {-# SPECIALIZE
    prettyCtx :: 
      (forall s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)) ->
      Ctx.Assignment TypeRepr tp ->
      Identity (Doc ann) #-}
  prettyCtx f = fmap hsep . foldlMFC (\l t -> (:l) <$> ppTypeRepr f t) []
  
  -- Helper, not exported
  prettyBaseCtx :: Ctx.Assignment BaseTypeRepr ctx -> Doc ann
  prettyBaseCtx = hsep . toListFC pretty
  
  -- | Pretty-print a type.
  --
  -- Attempts to be consistent with the syntax provided in the @crucible-syntax@
  -- package.
  --
  -- This is monadic mostly to allow failure, e.g., in case the caller finds an
  -- intrinsic type that it doesn\'t expect.
  ppTypeRepr ::
    Monad f =>
    -- | How to print 'IntrinsicRepr', see 'ppIntrinsicDefault'
    (forall s ctx. SymbolRepr s -> CtxRepr ctx -> f (Doc ann)) ->
    TypeRepr tp ->
    f (Doc ann)
  -- The following specialization is used in the 'Pretty' instance and doesn't
  -- need to generate code for (>>=), so it seems worth specializing for it.
  {-# SPECIALIZE
    ppTypeRepr :: 
      (forall s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)) ->
      TypeRepr tp ->
      Identity (Doc ann) #-}
  ppTypeRepr f x =
    case x of
      AnyRepr -> pure "Any"
      UnitRepr -> pure "Unit"
      BoolRepr -> pure "Bool"
      NatRepr -> pure "Nat"
      IntegerRepr -> pure "Integer"
      RealValRepr -> pure "RealVal"
      ComplexRealRepr -> pure "ComplexReal"
      BVRepr n -> pure (parens ("Bitvector" <+> viaShow n))
      IntrinsicRepr name tys -> f name tys
      RecursiveRepr name tys ->
        parens . (("Rec" <+> pretty (symbolRepr name)) <+>) <$> prettyCtx f tys
      FloatRepr fr -> pure (parens ("Float" <+> pretty fr))
      IEEEFloatRepr fr -> pure (parens ("IEEEFloat" <+> pretty fr))
      CharRepr -> pure "Char"
      StringRepr s -> pure (parens ("String" <+> pretty s))
      FunctionHandleRepr args ret ->
        (\args' ret' -> parens ("->" <+> args' <+> ret'))
        <$> prettyCtx f args
        <*> ppTypeRepr f ret
      MaybeRepr tp -> parens . ("Maybe" <+>) <$> ppTypeRepr f tp
      SequenceRepr s -> parens . ("Sequence" <+>) <$> ppTypeRepr f s
      VariantRepr variants -> parens . ("Variant" <+>) <$> prettyCtx f variants
      VectorRepr elems -> parens . ("Vector" <+>) <$> ppTypeRepr f elems
      StructRepr fields -> parens . ("Struct" <+>) <$> prettyCtx f fields
      ReferenceRepr t -> parens . ("Reference" <+>) <$> ppTypeRepr f t
      WordMapRepr n t -> pure (parens ("WorldMap" <+> viaShow n <+> pretty t))
      StringMapRepr s -> parens . ("StringMap" <+>) <$> ppTypeRepr f s
      SymbolicArrayRepr idxs a ->
        pure (parens ("SymbolicArray" <+> prettyBaseCtx idxs <+> pretty a))
      SymbolicStructRepr fields ->
        pure (parens ("SymbolicStruct" <+> prettyBaseCtx fields))
  
  -- | A default printer for 'IntrinsicRepr', suitable for use with 'ppTypeRepr'.
  ppIntrinsicDefault :: SymbolRepr s -> CtxRepr ctx -> Doc ann
  ppIntrinsicDefault name tys = runIdentity (go name tys)
    where
    go :: forall ann s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)
    go name' tys' =
      Identity $
        parens $
          pretty (symbolRepr name') <+> runIdentity (prettyCtx go tys')
  
  -- | Pretty-print a type. Based on 'ppTypeRepr', using 'ppIntrinsicDefault'.
  instance Pretty (TypeRepr tp) where
    pretty =
      runIdentity . ppTypeRepr (\name tys -> Identity (ppIntrinsicDefault name tys))
  
  instance Show (TypeRepr tp) where
    showsPrec = $(U.structuralShowsPrec [t|TypeRepr|])
  instance ShowF TypeRepr
  
  
  instance TestEquality TypeRepr where
    testEquality = $(U.structuralTypeEquality [t|TypeRepr|]
                     [ (U.TypeApp (U.ConType [t|NatRepr|]) U.AnyType, [|testEquality|])
                     , (U.TypeApp (U.ConType [t|SymbolRepr|]) U.AnyType, [|testEquality|])
                     , (U.TypeApp (U.ConType [t|FloatInfoRepr|]) U.AnyType, [|testEquality|])
                     , (U.TypeApp (U.ConType [t|FloatPrecisionRepr|]) U.AnyType, [|testEquality|])
                     , (U.TypeApp (U.ConType [t|CtxRepr|]) U.AnyType, [|testEquality|])
                     , (U.TypeApp (U.ConType [t|BaseTypeRepr|]) U.AnyType, [|testEquality|])
                     , (U.TypeApp (U.ConType [t|StringInfoRepr|])  U.AnyType, [|testEquality|])
                     , (U.TypeApp (U.ConType [t|TypeRepr|]) U.AnyType, [|testEquality|])
                     , (U.TypeApp (U.TypeApp (U.ConType [t|Ctx.Assignment|]) U.AnyType) U.AnyType
                       , [|testEquality|])
                     ]
                    )
  instance Eq (TypeRepr tp) where
    x == y = isJust (testEquality x y)
  instance EqF TypeRepr where
    eqF x y = isJust (testEquality x y)
  
  instance OrdF TypeRepr where
    compareF = $(U.structuralTypeOrd [t|TypeRepr|]
                     [ (U.TypeApp (U.ConType [t|NatRepr|]) U.AnyType, [|compareF|])
                     , (U.TypeApp (U.ConType [t|SymbolRepr|]) U.AnyType, [|compareF|])
                     , (U.TypeApp (U.ConType [t|FloatInfoRepr|]) U.AnyType, [|compareF|])
                     , (U.TypeApp (U.ConType [t|FloatPrecisionRepr|]) U.AnyType, [|compareF|])
                     , (U.TypeApp (U.ConType [t|BaseTypeRepr|])  U.AnyType, [|compareF|])
                     , (U.TypeApp (U.ConType [t|StringInfoRepr|])  U.AnyType, [|compareF|])
                     , (U.TypeApp (U.ConType [t|TypeRepr|])      U.AnyType, [|compareF|])
                     , (U.TypeApp (U.ConType [t|CtxRepr|])      U.AnyType, [|compareF|])
                     , (U.TypeApp (U.TypeApp (U.ConType [t|Ctx.Assignment|]) U.AnyType) U.AnyType
                       , [|compareF|])
                     ]
                    )
  