diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,10 @@
+2022-11-07
+        * Version bump (3.12). (#389)
+        * Deprecate Copilot.Core.PrettyPrinter. (#383)
+        * Replace uses of Copilot.Core.Type.Equality with definitions from
+          base:Data.Type.Equality; deprecate Copilot.Core.Type.Equality. (#379)
+        * Compliance with style guide. (#332)
+
 2022-09-07
         * Version bump (3.11). (#376)
         * Deprecate Copilot.Core.PrettyDot. (#359)
diff --git a/copilot-core.cabal b/copilot-core.cabal
--- a/copilot-core.cabal
+++ b/copilot-core.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             3.11
+version:             3.12
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs
--- a/src/Copilot/Core.hs
+++ b/src/Copilot/Core.hs
@@ -1,6 +1,14 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+{-# LANGUAGE Safe #-}
 
--- | Intermediate representation for Copilot specifications.
+-- The following warning is enabled in this module so that the import of
+-- Copilot.Core.External does not give rise to a warning. It can be removed
+-- when that module is removed from the implementation.
+{-# OPTIONS_GHC -fno-warn-deprecations #-}
+
+-- |
+-- Description: Intermediate representation for Copilot specifications.
+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
+--
 -- The following articles might also be useful:
 --
 -- * Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh,
@@ -17,29 +25,26 @@
 -- ("Copilot.Core.Interpret")
 -- and the pretty-printer
 -- ("Copilot.Core.PrettyPrint").
-
-{-# LANGUAGE Safe #-}
--- The following warning is enabled in this module so that the import of
--- Copilot.Core.External does not give rise to a warning. It can be removed
--- when that module is removed from the implementation.
-{-# OPTIONS_GHC -fno-warn-deprecations #-}
-
 module Copilot.Core
-  ( module Copilot.Core.Expr
-  , module Copilot.Core.External
-  , module Copilot.Core.Operators
-  , module Copilot.Core.Spec
-  , module Copilot.Core.Type
-  , module Copilot.Core.Type.Array
-  , module Data.Int
-  , module Data.Word
-  ) where
+    ( module Copilot.Core.Expr
+    , module Copilot.Core.External
+    , module Copilot.Core.Operators
+    , module Copilot.Core.Spec
+    , module Copilot.Core.Type
+    , module Copilot.Core.Type.Array
+    , module Data.Int
+    , module Data.Word
+    )
+  where
 
+-- External imports
+import Data.Int
+import Data.Word
+
+-- Internal imports
 import Copilot.Core.Expr
 import Copilot.Core.External -- See GHC flag enabled above
 import Copilot.Core.Operators
 import Copilot.Core.Spec
 import Copilot.Core.Type
 import Copilot.Core.Type.Array
-import Data.Int
-import Data.Word
diff --git a/src/Copilot/Core/Error.hs b/src/Copilot/Core/Error.hs
--- a/src/Copilot/Core/Error.hs
+++ b/src/Copilot/Core/Error.hs
@@ -1,11 +1,13 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
 {-# LANGUAGE Safe #-}
 
--- | Custom functions to report error messages to users.
+-- |
+-- Description: Custom functions to report error messages to users.
+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
 module Copilot.Core.Error
-  ( impossible
-  , badUsage ) where
+    ( impossible
+    , badUsage
+    )
+  where
 
 -- | Report an error due to a bug in Copilot.
 impossible :: String -- ^ Name of the function in which the error was detected.
diff --git a/src/Copilot/Core/Expr.hs b/src/Copilot/Core/Expr.hs
--- a/src/Copilot/Core/Expr.hs
+++ b/src/Copilot/Core/Expr.hs
@@ -1,24 +1,27 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE Safe                      #-}
 
--- | Internal representation of Copilot stream expressions.
+-- |
+-- Description: Internal representation of Copilot stream expressions.
+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
 module Copilot.Core.Expr
-  ( Id
-  , Name
-  , Expr (..)
-  , UExpr (..)
-  , DropIdx
-  ) where
-
-import Copilot.Core.Operators (Op1, Op2, Op3)
-import Copilot.Core.Type (Type)
-import Data.Word (Word32)
+    ( Id
+    , Name
+    , Expr (..)
+    , UExpr (..)
+    , DropIdx
+    )
+  where
 
+-- External imports
 import Data.Typeable (Typeable)
+import Data.Word     (Word32)
 
+-- Internal imports
+import Copilot.Core.Operators (Op1, Op2, Op3)
+import Copilot.Core.Type      (Type)
+
 -- | A stream identifier.
 type Id = Int
 
@@ -34,19 +37,37 @@
 -- representation contains information about the types of elements in the
 -- stream.
 data Expr a where
-  Const        :: Typeable a => Type a -> a -> Expr a
-  Drop         :: Typeable a => Type a -> DropIdx -> Id -> Expr a
-  Local        :: Typeable a => Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b
-  Var          :: Typeable a => Type a -> Name -> Expr a
-  ExternVar    :: Typeable a => Type a -> Name -> Maybe [a] -> Expr a
-  Op1          :: Typeable a => Op1 a b -> Expr a -> Expr b
-  Op2          :: (Typeable a, Typeable b) => Op2 a b c -> Expr a -> Expr b -> Expr c
-  Op3          :: (Typeable a, Typeable b, Typeable c) => Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
-  Label        :: Typeable a => Type a -> String -> Expr a -> Expr a
+  Const     :: Typeable a
+            => Type a -> a -> Expr a
 
+  Drop      :: Typeable a
+            => Type a -> DropIdx -> Id -> Expr a
+
+  Local     :: Typeable a
+            => Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b
+
+  Var       :: Typeable a
+            => Type a -> Name -> Expr a
+
+  ExternVar :: Typeable a
+            => Type a -> Name -> Maybe [a] -> Expr a
+
+  Op1       :: Typeable a
+            => Op1 a b -> Expr a -> Expr b
+
+  Op2       :: (Typeable a, Typeable b)
+            => Op2 a b c -> Expr a -> Expr b -> Expr c
+
+  Op3       :: (Typeable a, Typeable b, Typeable c)
+            => Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
+
+  Label     :: Typeable a
+            => Type a -> String -> Expr a -> Expr a
+
 -- | A untyped expression that carries the information about the type of the
 -- expression as a value, as opposed to exposing it at type level (using an
 -- existential).
-data UExpr = forall a. Typeable a => UExpr
+data UExpr = forall a . Typeable a => UExpr
   { uExprType :: Type a
-  , uExprExpr :: Expr a }
+  , uExprExpr :: Expr a
+  }
diff --git a/src/Copilot/Core/Operators.hs b/src/Copilot/Core/Operators.hs
--- a/src/Copilot/Core/Operators.hs
+++ b/src/Copilot/Core/Operators.hs
@@ -1,22 +1,25 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
 {-# LANGUAGE GADTs      #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE Safe       #-}
 
--- | Internal representation of Copilot operators.
+-- |
+-- Description: Internal representation of Copilot operators.
+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
 module Copilot.Core.Operators
-  ( Op1 (..)
-  , Op2 (..)
-  , Op3 (..)
-  ) where
+    ( Op1 (..)
+    , Op2 (..)
+    , Op3 (..)
+    )
+  where
 
-import GHC.TypeLits             (KnownSymbol)
+-- External imports
+import Data.Bits    (Bits)
+import Data.Word    (Word32)
+import GHC.TypeLits (KnownSymbol)
 
-import Copilot.Core.Type        (Type(..), Field(..))
-import Copilot.Core.Type.Array  (Array)
-import Data.Bits
-import Data.Word                (Word32)
+-- Internal imports
+import Copilot.Core.Type       (Field (..), Type (..))
+import Copilot.Core.Type.Array (Array)
 
 -- | Unary operators.
 data Op1 a b where
@@ -47,7 +50,7 @@
   Ceiling  :: RealFrac a => Type a -> Op1 a a
   Floor    :: RealFrac a => Type a -> Op1 a a
   -- Bitwise operators.
-  BwNot    :: Bits     a => Type a -> Op1 a a
+  BwNot    :: Bits a => Type a -> Op1 a a
   -- Casting operator.
   Cast     :: (Integral a, Num b) => Type a -> Type b -> Op1 a b
               -- ^ Casting operator.
@@ -87,14 +90,13 @@
   BwAnd    :: Bits a => Type a -> Op2 a a a
   BwOr     :: Bits a => Type a -> Op2 a a a
   BwXor    :: Bits a => Type a -> Op2 a a a
-  BwShiftL :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a
-  BwShiftR :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a
+  BwShiftL :: (Bits a, Integral b) => Type a -> Type b -> Op2 a b a
+  BwShiftR :: (Bits a, Integral b) => Type a -> Type b -> Op2 a b a
   -- Array operator.
-
   Index    :: Type (Array n t) -> Op2 (Array n t) Word32 t
               -- ^ Array access/projection of an array element.
 
 -- | Ternary operators.
 data Op3 a b c d where
-  -- Conditional operator:
-  Mux   :: Type a -> Op3 Bool a a a
+  -- Conditional operator.
+  Mux :: Type a -> Op3 Bool a a a
diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs
--- a/src/Copilot/Core/PrettyPrint.hs
+++ b/src/Copilot/Core/PrettyPrint.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE Safe  #-}
 
 module Copilot.Core.PrettyPrint
+  {-# DEPRECATED "This module is deprecated in Copilot 3.12. Use copilot-prettyprinter instead." #-}
   ( prettyPrint
   , ppExpr
   ) where
diff --git a/src/Copilot/Core/Spec.hs b/src/Copilot/Core/Spec.hs
--- a/src/Copilot/Core/Spec.hs
+++ b/src/Copilot/Core/Spec.hs
@@ -1,11 +1,12 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE Safe                      #-}
 
--- | Copilot specifications constitute the main declaration of Copilot modules.
+-- |
+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
 --
+-- Copilot specifications constitute the main declaration of Copilot modules.
+--
 -- A specification normally contains the association between streams to monitor
 -- and their handling functions, or streams to observe, or a theorem that must
 -- be proved.
@@ -14,52 +15,61 @@
 -- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core
 -- representations for Specs and the main types of element in a spec..
 module Copilot.Core.Spec
-  ( Stream (..)
-  , Observer (..)
-  , Trigger (..)
-  , Spec (..)
-  , Property (..)
-  ) where
+    ( Stream (..)
+    , Observer (..)
+    , Trigger (..)
+    , Spec (..)
+    , Property (..)
+    )
+  where
 
-import Copilot.Core.Expr (Name, Id, Expr, UExpr)
-import Copilot.Core.Type (Type, Typed)
+-- External imports
 import Data.Typeable (Typeable)
 
+-- Internal imports
+import Copilot.Core.Expr (Expr, Id, Name, UExpr)
+import Copilot.Core.Type (Type, Typed)
+
 -- | A stream in an infinite succession of values of the same type.
 --
 -- Stream can carry different types of data. Boolean streams play a special
 -- role: they are used by other parts (e.g., 'Trigger') to detect when the
 -- properties being monitored are violated.
-data Stream = forall a. (Typeable a, Typed a) => Stream
-  { streamId         :: Id
-  , streamBuffer     :: [a]
-  , streamExpr       :: Expr a
-  , streamExprType   :: Type a }
+data Stream = forall a . (Typeable a, Typed a) => Stream
+  { streamId       :: Id
+  , streamBuffer   :: [a]
+  , streamExpr     :: Expr a
+  , streamExprType :: Type a
+  }
 
 -- | An observer, representing a stream that we observe during interpretation
 -- at every sample.
-data Observer = forall a. Typeable a => Observer
+data Observer = forall a . Typeable a => Observer
   { observerName     :: Name
   , observerExpr     :: Expr a
-  , observerExprType :: Type a }
+  , observerExprType :: Type a
+  }
 
 -- | A trigger, representing a function we execute when a boolean stream becomes
 -- true at a sample.
 data Trigger = Trigger
-  { triggerName      :: Name
-  , triggerGuard     :: Expr Bool
-  , triggerArgs      :: [UExpr] }
+  { triggerName  :: Name
+  , triggerGuard :: Expr Bool
+  , triggerArgs  :: [UExpr]
+  }
 
 -- | A property, representing a boolean stream that is existentially or
 -- universally quantified over time.
 data Property = Property
-  { propertyName     :: Name
-  , propertyExpr     :: Expr Bool }
+  { propertyName :: Name
+  , propertyExpr :: Expr Bool
+  }
 
 -- | A Copilot specification is a list of streams, together with monitors on
 -- these streams implemented as observers, triggers or properties.
 data Spec = Spec
-  { specStreams      :: [Stream]
-  , specObservers    :: [Observer]
-  , specTriggers     :: [Trigger]
-  , specProperties   :: [Property] }
+  { specStreams    :: [Stream]
+  , specObservers  :: [Observer]
+  , specTriggers   :: [Trigger]
+  , specProperties :: [Property]
+  }
diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs
--- a/src/Copilot/Core/Type.hs
+++ b/src/Copilot/Core/Type.hs
@@ -1,13 +1,3 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
--- | Typing for Core.
---
--- All expressions and streams in Core are accompanied by a representation of
--- the types of the underlying expressions used or carried by the streams.
--- This information is needed by the compiler to generate code, since it must
--- initialize variables and equivalent representations for those types in
--- the target languages.
-
 {-# LANGUAGE DataKinds                 #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleContexts          #-}
@@ -18,36 +8,51 @@
 {-# LANGUAGE ScopedTypeVariables       #-}
 {-# LANGUAGE UndecidableInstances      #-}
 
-module Copilot.Core.Type
-  ( Type (..)
-  , Typed (..)
-  , UType (..)
-  , SimpleType (..)
-
-  , tysize
-  , tylength
+-- The following flag is disabled in this module so that the import of
+-- Copilot.Core.Type.Equality does not give rise to warnings.
+{-# OPTIONS_GHC -fno-warn-deprecations #-}
 
-  , Value (..)
-  , toValues
-  , Field (..)
-  , typename
+-- |
+-- Description: Typing for Core.
+-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
+--
+-- All expressions and streams in Core are accompanied by a representation of
+-- the types of the underlying expressions used or carried by the streams.
+-- This information is needed by the compiler to generate code, since it must
+-- initialize variables and equivalent representations for those types in
+-- the target languages.
+module Copilot.Core.Type
+    ( Type (..)
+    , Typed (..)
+    , UType (..)
+    , SimpleType (..)
 
-  , Struct
-  , fieldname
-  , accessorname
-  ) where
+    , tysize
+    , tylength
 
-import Data.Int
-import Data.Word
-import Copilot.Core.Type.Equality
-import Copilot.Core.Type.Array
+    , Value (..)
+    , toValues
+    , Field (..)
+    , typename
 
-import Data.Typeable (Typeable, typeRep)
+    , Struct
+    , fieldname
+    , accessorname
+    )
+  where
 
-import GHC.TypeLits (KnownNat, natVal, Symbol, KnownSymbol, symbolVal)
-import Data.Proxy   (Proxy (..))
+-- External imports
+import Data.Int           (Int16, Int32, Int64, Int8)
+import Data.List          (intercalate)
+import Data.Proxy         (Proxy (..))
+import Data.Type.Equality as DE
+import Data.Typeable      (Typeable, typeRep)
+import Data.Word          (Word16, Word32, Word64, Word8)
+import GHC.TypeLits       (KnownNat, KnownSymbol, Symbol, natVal, symbolVal)
 
-import Data.List (intercalate)
+-- Internal imports
+import Copilot.Core.Type.Array    (Array)
+import Copilot.Core.Type.Equality as CE
 
 -- | The value of that is a product or struct, defined as a constructor with
 -- several fields.
@@ -58,19 +63,21 @@
   toValues :: a -> [Value a]
 
 -- | The field of a struct, together with a representation of its type.
-data Value a = forall s t. (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)
+data Value a =
+  forall s t . (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)
 
 -- | A field in a struct. The name of the field is a literal at the type
 -- level.
 data Field (s :: Symbol) t = Field t
 
 -- | Extract the name of a field.
-fieldname :: forall s t. KnownSymbol s => Field s t -> String
+fieldname :: forall s t . KnownSymbol s => Field s t -> String
 fieldname _ = symbolVal (Proxy :: Proxy s)
 
 -- | Extract the name of an accessor (a function that returns a field of a
 -- struct).
-accessorname :: forall a s t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String
+accessorname :: forall a s t . (Struct a, KnownSymbol s)
+             => (a -> Field s t) -> String
 accessorname _ = symbolVal (Proxy :: Proxy s)
 
 instance (KnownSymbol s, Show t) => Show (Field s t) where
@@ -89,45 +96,59 @@
 -- former, the length of the array is part of the type. In the latter, the
 -- names of the fields are part of the type.
 data Type :: * -> * where
-  Bool    :: Type Bool
-  Int8    :: Type Int8
-  Int16   :: Type Int16
-  Int32   :: Type Int32
-  Int64   :: Type Int64
-  Word8   :: Type Word8
-  Word16  :: Type Word16
-  Word32  :: Type Word32
-  Word64  :: Type Word64
-  Float   :: Type Float
-  Double  :: Type Double
-  Array   :: forall n t. ( KnownNat n
+  Bool   :: Type Bool
+  Int8   :: Type Int8
+  Int16  :: Type Int16
+  Int32  :: Type Int32
+  Int64  :: Type Int64
+  Word8  :: Type Word8
+  Word16 :: Type Word16
+  Word32 :: Type Word32
+  Word64 :: Type Word64
+  Float  :: Type Float
+  Double :: Type Double
+  Array  :: forall n t . ( KnownNat n
                          , Typed t
                          ) => Type t -> Type (Array n t)
-  Struct  :: (Typed a, Struct a) => a -> Type a
+  Struct :: (Typed a, Struct a) => a -> Type a
 
 -- | Return the length of an array from its type
-tylength :: forall n t. KnownNat n => Type (Array n t) -> Int
+tylength :: forall n t . KnownNat n => Type (Array n t) -> Int
 tylength _ = fromIntegral $ natVal (Proxy :: Proxy n)
 
 -- | Return the total (nested) size of an array from its type
-tysize :: forall n t. KnownNat n => Type (Array n t) -> Int
+tysize :: forall n t . KnownNat n => Type (Array n t) -> Int
 tysize ty@(Array ty'@(Array _)) = tylength ty * tysize ty'
 tysize ty@(Array _            ) = tylength ty
 
 instance EqualType Type where
-  (=~=) Bool   Bool   = Just Refl
-  (=~=) Int8   Int8   = Just Refl
-  (=~=) Int16  Int16  = Just Refl
-  (=~=) Int32  Int32  = Just Refl
-  (=~=) Int64  Int64  = Just Refl
-  (=~=) Word8  Word8  = Just Refl
-  (=~=) Word16 Word16 = Just Refl
-  (=~=) Word32 Word32 = Just Refl
-  (=~=) Word64 Word64 = Just Refl
-  (=~=) Float  Float  = Just Refl
-  (=~=) Double Double = Just Refl
+  (=~=) Bool   Bool   = Just CE.Refl
+  (=~=) Int8   Int8   = Just CE.Refl
+  (=~=) Int16  Int16  = Just CE.Refl
+  (=~=) Int32  Int32  = Just CE.Refl
+  (=~=) Int64  Int64  = Just CE.Refl
+  (=~=) Word8  Word8  = Just CE.Refl
+  (=~=) Word16 Word16 = Just CE.Refl
+  (=~=) Word32 Word32 = Just CE.Refl
+  (=~=) Word64 Word64 = Just CE.Refl
+  (=~=) Float  Float  = Just CE.Refl
+  (=~=) Double Double = Just CE.Refl
   (=~=) _ _ = Nothing
 
+instance TestEquality Type where
+  testEquality Bool   Bool   = Just DE.Refl
+  testEquality Int8   Int8   = Just DE.Refl
+  testEquality Int16  Int16  = Just DE.Refl
+  testEquality Int32  Int32  = Just DE.Refl
+  testEquality Int64  Int64  = Just DE.Refl
+  testEquality Word8  Word8  = Just DE.Refl
+  testEquality Word16 Word16 = Just DE.Refl
+  testEquality Word32 Word32 = Just DE.Refl
+  testEquality Word64 Word64 = Just DE.Refl
+  testEquality Float  Float  = Just DE.Refl
+  testEquality Double Double = Just DE.Refl
+  testEquality _ _ = Nothing
+
 -- | A simple, monomorphic representation of types that facilitates putting
 -- variables in heterogeneous lists and environments in spite of their types
 -- being different.
@@ -149,22 +170,21 @@
 -- | Type equality, used to help type inference.
 
 -- This instance is necessary, otherwise the type of SArray can't be inferred.
-
 instance Eq SimpleType where
-  SBool   == SBool    = True
-  SInt8   == SInt8    = True
-  SInt16  == SInt16   = True
-  SInt32  == SInt32   = True
-  SInt64  == SInt64   = True
-  SWord8  == SWord8   = True
-  SWord16 == SWord16  = True
-  SWord32 == SWord32  = True
-  SWord64 == SWord64  = True
-  SFloat  == SFloat   = True
-  SDouble == SDouble  = True
-  (SArray t1) == (SArray t2) | Just Refl <- t1 =~= t2 = True
-                             | otherwise              = False
-  SStruct == SStruct  = True
+  SBool   == SBool   = True
+  SInt8   == SInt8   = True
+  SInt16  == SInt16  = True
+  SInt32  == SInt32  = True
+  SInt64  == SInt64  = True
+  SWord8  == SWord8  = True
+  SWord16 == SWord16 = True
+  SWord32 == SWord32 = True
+  SWord64 == SWord64 = True
+  SFloat  == SFloat  = True
+  SDouble == SDouble = True
+  (SArray t1) == (SArray t2) | Just DE.Refl <- testEquality t1 t2 = True
+                             | otherwise                          = False
+  SStruct == SStruct = True
   _ == _ = False
 
 -- | A typed expression, from which we can obtain the two type representations
@@ -174,42 +194,53 @@
   simpleType :: Type a -> SimpleType
   simpleType _ = SStruct
 
-instance Typed Bool   where
+instance Typed Bool where
   typeOf       = Bool
   simpleType _ = SBool
-instance Typed Int8   where
+
+instance Typed Int8 where
   typeOf       = Int8
   simpleType _ = SBool
-instance Typed Int16  where
+
+instance Typed Int16 where
   typeOf       = Int16
   simpleType _ = SInt16
-instance Typed Int32  where
+
+instance Typed Int32 where
   typeOf       = Int32
   simpleType _ = SInt32
-instance Typed Int64  where
+
+instance Typed Int64 where
   typeOf       = Int64
   simpleType _ = SInt64
-instance Typed Word8  where
+
+instance Typed Word8 where
   typeOf       = Word8
   simpleType _ = SWord8
+
 instance Typed Word16 where
   typeOf       = Word16
   simpleType _ = SWord16
+
 instance Typed Word32 where
   typeOf       = Word32
   simpleType _ = SWord32
+
 instance Typed Word64 where
   typeOf       = Word64
   simpleType _ = SWord64
-instance Typed Float  where
+
+instance Typed Float where
   typeOf       = Float
   simpleType _ = SFloat
+
 instance Typed Double where
   typeOf       = Double
   simpleType _ = SDouble
+
 instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
-  typeOf                = Array typeOf
-  simpleType (Array t)  = SArray t
+  typeOf               = Array typeOf
+  simpleType (Array t) = SArray t
 
 -- | A untyped type (no phantom type).
 data UType = forall a . Typeable a => UType { uTypeType :: Type a }
diff --git a/src/Copilot/Core/Type/Array.hs b/src/Copilot/Core/Type/Array.hs
--- a/src/Copilot/Core/Type/Array.hs
+++ b/src/Copilot/Core/Type/Array.hs
@@ -1,31 +1,32 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE KindSignatures        #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE TypeOperators         #-}
 
--- | Implementation of an array that uses type literals to store length. No
+-- |
+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
+--
+-- Implementation of an array that uses type literals to store length. No
 -- explicit indexing is used for the input data. Supports arbitrary nesting of
 -- arrays.
-
 module Copilot.Core.Type.Array
-  ( Array
-  , array
-  , flatten
-  , size
-  , Flatten
-  , InnerType
-  , arrayelems
-  ) where
+    ( Array
+    , array
+    , flatten
+    , size
+    , Flatten
+    , InnerType
+    , arrayelems
+    )
+  where
 
-import GHC.TypeLits     (Nat, KnownNat, natVal)
-import Data.Proxy       (Proxy (..))
+-- External imports
+import Data.Proxy   (Proxy (..))
+import GHC.TypeLits (KnownNat, Nat, natVal)
 
 -- | Implementation of an array that uses type literals to store length.
 data Array (n :: Nat) t where
diff --git a/src/Copilot/Core/Type/Equality.hs b/src/Copilot/Core/Type/Equality.hs
--- a/src/Copilot/Core/Type/Equality.hs
+++ b/src/Copilot/Core/Type/Equality.hs
@@ -6,6 +6,7 @@
 
 -- | Propositional equality and type equality.
 module Copilot.Core.Type.Equality
+  {-# DEPRECATED "This module is deprecated in Copilot 3.12. Use base:Data.Type.Equality instead." #-}
   ( Equal (..)
   , EqualType (..)
   , coerce
diff --git a/src/Copilot/Core/Type/ShowInternal.hs b/src/Copilot/Core/Type/ShowInternal.hs
--- a/src/Copilot/Core/Type/ShowInternal.hs
+++ b/src/Copilot/Core/Type/ShowInternal.hs
@@ -1,20 +1,20 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE Safe                      #-}
 
--- | Show Copilot Core types and typed values.
+-- |
+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
+--
+-- Show Copilot Core types and typed values.
 module Copilot.Core.Type.ShowInternal
-  ( showWithType
-  , ShowType(..)
-  , showType
-  ) where
-
-import Copilot.Core.Type
+    ( showWithType
+    , ShowType (..)
+    , showType
+    )
+  where
 
--- Are we proving equivalence with a C backend, in which case we want to show
--- Booleans as '0' and '1'.
+-- Internal imports
+import Copilot.Core.Type (Type (..))
 
 -- | Target language for showing a typed value. Used to adapt the
 -- representation of booleans.
@@ -24,33 +24,33 @@
 -- language. Booleans are represented differently depending on the backend.
 showWithType :: ShowType -> Type a -> a -> String
 showWithType showT t x =
-  case showT of
-    C         -> case t of
+    case showT of
+      C       -> case t of
                    Bool -> if x then "1" else "0"
                    _    -> sw
-    Haskell   -> case t of
+      Haskell -> case t of
                    Bool -> if x then "true" else "false"
                    _    -> sw
   where
-  sw = case showWit t of
-         ShowWit -> show x
+    sw = case showWit t of
+           ShowWit -> show x
 
 -- | Show Copilot Core type.
 showType :: Type a -> String
 showType t =
   case t of
-    Bool   -> "Bool"
-    Int8   -> "Int8"
-    Int16  -> "Int16"
-    Int32  -> "Int32"
-    Int64  -> "Int64"
-    Word8  -> "Word8"
-    Word16 -> "Word16"
-    Word32 -> "Word32"
-    Word64 -> "Word64"
-    Float  -> "Float"
-    Double -> "Double"
-    Array t -> "Array " ++ showType t
+    Bool     -> "Bool"
+    Int8     -> "Int8"
+    Int16    -> "Int16"
+    Int32    -> "Int32"
+    Int64    -> "Int64"
+    Word8    -> "Word8"
+    Word16   -> "Word16"
+    Word32   -> "Word32"
+    Word64   -> "Word64"
+    Float    -> "Float"
+    Double   -> "Double"
+    Array t  -> "Array " ++ showType t
     Struct t -> "Struct"
 
 -- * Auxiliary show instance
@@ -62,16 +62,16 @@
 showWit :: Type a -> ShowWit a
 showWit t =
   case t of
-    Bool   -> ShowWit
-    Int8   -> ShowWit
-    Int16  -> ShowWit
-    Int32  -> ShowWit
-    Int64  -> ShowWit
-    Word8  -> ShowWit
-    Word16 -> ShowWit
-    Word32 -> ShowWit
-    Word64 -> ShowWit
-    Float  -> ShowWit
-    Double -> ShowWit
-    Array t -> ShowWit
+    Bool     -> ShowWit
+    Int8     -> ShowWit
+    Int16    -> ShowWit
+    Int32    -> ShowWit
+    Int64    -> ShowWit
+    Word8    -> ShowWit
+    Word16   -> ShowWit
+    Word32   -> ShowWit
+    Word64   -> ShowWit
+    Float    -> ShowWit
+    Double   -> ShowWit
+    Array t  -> ShowWit
     Struct t -> ShowWit