diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,12 @@
+2022-05-06
+        * Version bump (3.9). (#320)
+        * Compliance with style guide (partial). (#316)
+        * Hide module Copilot.Core.Interpret.Render. (#303)
+        * Remove Copilot.Core.Type.Dynamic.fromDynF,toDynF. (#301)
+        * Hide module Copilot.Core.Error. (#300)
+        * Remove Copilot.Core.Type.Uninitialized. (#302)
+        * Remove Copilot.Core.Expr.Tag. (#304)
+
 2022-03-07
         * Version bump (3.8). (#298)
         * Replaces uses of the internal Dynamic with base:Data.Dynamic. (#266)
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.8
+version:             3.9
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
@@ -51,12 +51,10 @@
   exposed-modules:
 
     Copilot.Core
-    Copilot.Core.Error
     Copilot.Core.Expr
     Copilot.Core.External
     Copilot.Core.Interpret
     Copilot.Core.Interpret.Eval
-    Copilot.Core.Interpret.Render
     Copilot.Core.Operators
     Copilot.Core.Spec
     Copilot.Core.Type
@@ -64,14 +62,13 @@
     Copilot.Core.Type.Dynamic
     Copilot.Core.Type.Equality
     Copilot.Core.Type.Show
-    Copilot.Core.Type.Uninitialized
     Copilot.Core.PrettyPrint
     Copilot.Core.PrettyDot
 
   other-modules:
 
-    Copilot.Core.ErrorInternal
-    Copilot.Core.Interpret.RenderInternal
+    Copilot.Core.Error
+    Copilot.Core.Interpret.Render
 
 test-suite unit-tests
   type:
@@ -82,7 +79,6 @@
 
   other-modules:
     Test.Extra
-    Test.Copilot.Core.Error
     Test.Copilot.Core.External
     Test.Copilot.Core.Interpret.Eval
     Test.Copilot.Core.Type
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,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Intermediate representation for Copilot specifications.
 -- The following articles might also be useful:
@@ -23,25 +21,21 @@
 {-# LANGUAGE Safe #-}
 
 module Copilot.Core
-  ( module Copilot.Core.Error
-  , module Copilot.Core.Expr
+  ( 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 Copilot.Core.Type.Uninitialized
   , module Data.Int
   , module Data.Word
   ) where
 
-import Copilot.Core.Error
 import Copilot.Core.Expr
 import Copilot.Core.External
 import Copilot.Core.Operators
 import Copilot.Core.Spec
 import Copilot.Core.Type
 import Copilot.Core.Type.Array
-import Copilot.Core.Type.Uninitialized
 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,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 {-# LANGUAGE Safe #-}
 
@@ -9,17 +7,18 @@
   ( impossible
   , badUsage ) where
 
-import qualified Copilot.Core.ErrorInternal as Err
-
 -- | Report an error due to a bug in Copilot.
-{-# DEPRECATED impossible "This function is deprecated in Copilot 3.6." #-}
 impossible :: String -- ^ Name of the function in which the error was detected.
            -> String -- ^ Name of the package in which the function is located.
            -> a
-impossible = Err.impossible
+impossible function package =
+  error $ "\"Impossible\" error in function "
+    ++ function ++ ", in package " ++ package
+    ++ ". Please file an issue at "
+    ++ "https://github.com/Copilot-Language/copilot/issues"
+    ++ "or email the maintainers at <ivan.perezdominguez@nasa.gov>"
 
 -- | Report an error due to an error detected by Copilot (e.g., user error).
-{-# DEPRECATED badUsage "This function is deprecated in Copilot 3.6." #-}
 badUsage :: String -- ^ Description of the error.
          -> a
-badUsage = Err.badUsage
+badUsage msg = error $ "Copilot error: " ++ msg
diff --git a/src/Copilot/Core/ErrorInternal.hs b/src/Copilot/Core/ErrorInternal.hs
deleted file mode 100644
--- a/src/Copilot/Core/ErrorInternal.hs
+++ /dev/null
@@ -1,26 +0,0 @@
---------------------------------------------------------------------------------
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
-
-{-# LANGUAGE Safe #-}
-
--- | Custom functions to report error messages to users.
-module Copilot.Core.ErrorInternal
-  ( impossible
-  , badUsage ) where
-
--- | Report an error due to a bug in Copilot.
-impossible :: String -- ^ Name of the function in which the error was detected.
-           -> String -- ^ Name of the package in which the function is located.
-           -> a
-impossible function package =
-  error $ "\"Impossible\" error in function "
-    ++ function ++ ", in package " ++ package
-    ++ ". Please file an issue at "
-    ++ "https://github.com/Copilot-Language/copilot/issues"
-    ++ "or email the maintainers at <ivan.perezdominguez@nasa.gov>"
-
--- | Report an error due to an error detected by Copilot (e.g., user error).
-badUsage :: String -- ^ Description of the error.
-         -> a
-badUsage msg = error $ "Copilot error: " ++ msg
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,9 +1,8 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE GADTs, ExistentialQuantification #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE Safe                      #-}
 
 -- | Internal representation of Copilot stream expressions.
 module Copilot.Core.Expr
@@ -12,7 +11,6 @@
   , Expr (..)
   , UExpr (..)
   , DropIdx
-  , Tag
   ) where
 
 import Copilot.Core.Operators (Op1, Op2, Op3)
@@ -21,29 +19,15 @@
 
 import Data.Typeable (Typeable)
 
---------------------------------------------------------------------------------
-
 -- | A stream identifier.
 type Id = Int
 
---------------------------------------------------------------------------------
-
 -- | A name of a trigger, an external variable, or an external function.
 type Name = String
 
---------------------------------------------------------------------------------
-
 -- | An index for the drop operator.
 type DropIdx = Word32
 
---------------------------------------------------------------------------------
-
--- | A unique tag for external arrays/function calls.
-{-# DEPRECATED Tag "The type Tag is deprecated in Copilot 3.6." #-}
-type Tag = Int
-
---------------------------------------------------------------------------------
-
 -- | Internal representation of Copilot stream expressions.
 --
 -- The Core representation mimics the high-level Copilot stream, but the Core
@@ -59,8 +43,6 @@
   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
diff --git a/src/Copilot/Core/External.hs b/src/Copilot/Core/External.hs
--- a/src/Copilot/Core/External.hs
+++ b/src/Copilot/Core/External.hs
@@ -1,10 +1,8 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
-{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE Rank2Types                #-}
+{-# LANGUAGE Trustworthy               #-}
 
 -- | Internal Copilot Core representation of Copilot externs.
 module Copilot.Core.External
@@ -21,16 +19,12 @@
 
 import Data.Typeable    (Typeable)
 
---------------------------------------------------------------------------------
-
 -- | An extern variable declaration, together with the type of the underlying
 -- extern.
 data ExtVar = ExtVar
   { externVarName :: Name
   , externVarType :: UType }
 
---------------------------------------------------------------------------------
-
 -- | List of all externs used in a specification.
 externVars :: Spec -> [ExtVar]
 externVars = nubBy eqExt . toList . all externVarsExpr
@@ -57,8 +51,6 @@
 -- | Extract all expressions used in an untyped Copilot expression.
 externVarsUExpr :: UExpr -> DList ExtVar
 externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e
-
---------------------------------------------------------------------------------
 
 -- | Apply a function to all expressions in a specification, concatenating the
 -- results.
diff --git a/src/Copilot/Core/Interpret.hs b/src/Copilot/Core/Interpret.hs
--- a/src/Copilot/Core/Interpret.hs
+++ b/src/Copilot/Core/Interpret.hs
@@ -1,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | An interpreter for Copilot specifications.
 
@@ -13,7 +11,7 @@
 
 import Copilot.Core
 import Copilot.Core.Interpret.Eval
-import Copilot.Core.Interpret.RenderInternal
+import Copilot.Core.Interpret.Render
 import Copilot.Core.Type.Show (ShowType(..))
 
 -- | Output format for the results of a Copilot spec interpretation.
@@ -28,4 +26,5 @@
   case format of
     Table -> renderAsTable e
     CSV   -> renderAsCSV e
-  where e = eval Haskell k spec
+  where
+    e = eval Haskell k spec
diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs
--- a/src/Copilot/Core/Interpret/Eval.hs
+++ b/src/Copilot/Core/Interpret/Eval.hs
@@ -1,11 +1,11 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | A tagless interpreter for Copilot specifications.
 
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE GADTs, BangPatterns, DeriveDataTypeable #-}
+{-# LANGUAGE BangPatterns       #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE GADTs              #-}
+{-# LANGUAGE Safe               #-}
 
 module Copilot.Core.Interpret.Eval
   ( Env
@@ -14,13 +14,13 @@
   , eval
   ) where
 
-import Copilot.Core               (Expr (..), Field (..), Id, Name,
-                                   Observer (..), Op1 (..), Op2 (..), Op3 (..),
-                                   Spec, Stream (..), Trigger (..),
-                                   Type (Struct), UExpr (..), arrayelems,
-                                   specObservers, specStreams, specTriggers)
-import Copilot.Core.ErrorInternal (badUsage)
-import Copilot.Core.Type.Show     (ShowType, showWithType)
+import Copilot.Core           (Expr (..), Field (..), Id, Name, Observer (..),
+                               Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),
+                               Trigger (..), Type (Struct), UExpr (..),
+                               arrayelems, specObservers, specStreams,
+                               specTriggers)
+import Copilot.Core.Error     (badUsage)
+import Copilot.Core.Type.Show (ShowType, showWithType)
 
 import           Prelude hiding (id)
 import qualified Prelude as P
@@ -32,8 +32,6 @@
 import Data.Maybe        (fromJust)
 import Data.Typeable     (Typeable)
 
---------------------------------------------------------------------------------
-
 -- | Exceptions that may be thrown during interpretation of a Copilot
 -- specification.
 data InterpException
@@ -81,14 +79,10 @@
 -- exception mechanisms.
 instance Exception InterpException
 
---------------------------------------------------------------------------------
-
 -- | An environment that contains an association between (stream or extern)
 -- names and their values.
 type Env nm = [(nm, Dynamic)]
 
---------------------------------------------------------------------------------
-
 -- | The simulation output is defined as a string. Different backends may
 -- choose to format their results differently.
 type Output = String
@@ -108,8 +102,6 @@
   }
   deriving Show
 
---------------------------------------------------------------------------------
-
 -- We could write this in a beautiful lazy style like above, but that creates a
 -- space leak in the interpreter that is hard to fix while maintaining laziness.
 -- We take a more brute-force appraoch below.
@@ -139,8 +131,6 @@
                     zip (map observerName (specObservers spec)) obsvs
                 }
 
---------------------------------------------------------------------------------
-
 -- | An environment that contains an association between (stream or extern)
 -- names and their values.
 type LocalEnv = [(Name, Dynamic)]
@@ -178,8 +168,6 @@
     let ev1 = evalExpr_ k e1 locs strms in
     ev1
 
---------------------------------------------------------------------------------
-
 -- | Evaluate an extern stream for a number of steps, obtaining the value of
 -- the sample at that time.
 evalExternVar :: Int -> Name -> Maybe [a] -> a
@@ -191,10 +179,6 @@
         Nothing -> throw (NotEnoughValues name k)
         Just x  -> x
 
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
-
 -- | Evaluate an 'Copilot.Core.Operators.Op1' by producing an equivalent
 -- Haskell function operating on the same types as the
 -- 'Copilot.Core.Operators.Op1'.
@@ -232,8 +216,6 @@
     -- Extract value from field
     unfield (Field v) = v
 
---------------------------------------------------------------------------------
-
 -- | Evaluate an 'Copilot.Core.Operators.Op2' by producing an equivalent
 -- Haskell function operating on the same types as the
 -- 'Copilot.Core.Operators.Op2'.
@@ -272,16 +254,12 @@
 catchZero _ _ 0 = throw DivideByZero
 catchZero f x y = f x y
 
---------------------------------------------------------------------------------
-
 -- | Evaluate an 'Copilot.Core.Operators.Op3' by producing an equivalent
 -- Haskell function operating on the same types as the
 -- 'Copilot.Core.Operators.Op3'.
 evalOp3 :: Op3 a b c d -> (a -> b -> c -> d)
 evalOp3 (Mux _) = \ !v !x !y -> if v then x else y
 
---------------------------------------------------------------------------------
-
 -- | Turn a stream into a key-value pair that can be added to an 'Env' for
 -- simulation.
 initStrm :: Stream -> (Id, Dynamic)
@@ -312,8 +290,6 @@
       let ls = x `seq` (x:xs)                                  in
       (id, toDyn ls)
 
---------------------------------------------------------------------------------
-
 -- | Evaluate a trigger for a number of steps.
 evalTrigger :: ShowType          -- ^ Show booleans as @0@/@1@ (C) or
                                  --   @True@/@False@ (Haskell).
@@ -346,8 +322,6 @@
   evalUExpr (UExpr t e1) =
     map (showWithType showType t) (evalExprs_ k e1 strms)
 
---------------------------------------------------------------------------------
-
 -- | Evaluate an observer for a number of steps.
 evalObserver :: ShowType  -- ^ Show booleans as @0@/@1@ (C) or @True@/@False@
                           --   (Haskell).
@@ -362,21 +336,15 @@
     , observerExprType = t }
   = map (showWithType showType t) (evalExprs_ k e strms)
 
---------------------------------------------------------------------------------
-
 -- | Evaluate an expression for a number of steps, producing a list with the
 -- changing value of the expression until that time.
 evalExprs_ :: Typeable a => Int -> Expr a -> Env Id -> [a]
 evalExprs_ k e strms =
   map (\i -> evalExpr_ i e [] strms) [0..(k-1)]
 
---------------------------------------------------------------------------------
-
 -- | Safe indexing (!!) on possibly infininite lists.
 safeIndex :: Int -> [a] -> Maybe a
 safeIndex i ls =
   let ls' = take (i+1) ls in
   if length ls' > i then Just (ls' !! i)
     else Nothing
-
--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Interpret/Render.hs b/src/Copilot/Core/Interpret/Render.hs
--- a/src/Copilot/Core/Interpret/Render.hs
+++ b/src/Copilot/Core/Interpret/Render.hs
@@ -1,15 +1,122 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Pretty-print the results of a simulation.
 
 {-# LANGUAGE Safe #-}
 
 module Copilot.Core.Interpret.Render
-  {-# DEPRECATED "This module is deprecated in Copilot 3.6." #-}
   ( renderAsTable
   , renderAsCSV
   ) where
 
-import Copilot.Core.Interpret.RenderInternal
+import Data.List (intersperse, transpose, foldl')
+import Data.Maybe (catMaybes)
+import Copilot.Core.Interpret.Eval (Output, ExecTrace (..))
+import Text.PrettyPrint
+
+import Prelude hiding ((<>))
+
+-- | Render an execution trace as a table, formatted to faciliate readability.
+renderAsTable :: ExecTrace -> String
+renderAsTable
+  ExecTrace
+    { interpTriggers  = trigs
+    , interpObservers = obsvs } = ( render
+                                  . asColumns
+                                  . transpose
+                                  . (:) (ppTriggerNames ++ ppObserverNames)
+                                  . transpose
+                                  ) (ppTriggerOutputs ++ ppObserverOutputs)
+     where
+
+     ppTriggerNames :: [Doc]
+     ppTriggerNames  = map (text . (++ ":")) (map fst trigs)
+
+     ppObserverNames :: [Doc]
+     ppObserverNames = map (text . (++ ":")) (map fst obsvs)
+
+     ppTriggerOutputs :: [[Doc]]
+     ppTriggerOutputs = map (map ppTriggerOutput) (map snd trigs)
+
+     ppTriggerOutput :: Maybe [Output] -> Doc
+     ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"
+     ppTriggerOutput Nothing   = text "--"
+
+     ppObserverOutputs :: [[Doc]]
+     ppObserverOutputs = map (map text) (map snd obsvs)
+
+-- | Render an execution trace as using comma-separate value (CSV) format.
+renderAsCSV :: ExecTrace -> String
+renderAsCSV = render . unfold
+
+-- | Pretty print all the steps of the execution trace and concatenate the
+-- results.
+unfold :: ExecTrace -> Doc
+unfold r =
+  case step r of
+    (cs, Nothing) -> cs
+    (cs, Just r') -> cs $$ unfold r'
+
+-- | Pretty print the state of the triggers, and provide a continuation
+-- for the execution trace at the next point in time.
+step :: ExecTrace -> (Doc, Maybe ExecTrace)
+step ExecTrace
+       { interpTriggers  = trigs
+       } =
+  if null trigs then (empty, Nothing)
+    else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)
+
+  where
+
+  ppTriggerOutputs :: [Doc]
+  ppTriggerOutputs =
+      catMaybes
+    . fmap ppTriggerOutput
+    . map (fmap head)
+    $ trigs
+
+  ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc
+  ppTriggerOutput (_,  Nothing) = Nothing
+  ppTriggerOutput (cs, Just xs) = Just $
+    text cs <> text "," <>
+      (foldr (<>) empty . map text . intersperse ",") xs
+
+  tails :: Maybe ExecTrace
+  tails =
+    if any null (fmap (tail.snd) trigs)
+      then Nothing
+      else Just
+        ExecTrace
+          { interpTriggers  = map (fmap tail) trigs
+          , interpObservers = []
+          }
+
+-- Copied from pretty-ncols because of incompatibility with newer GHC versions.
+asColumns :: [[Doc]] -> Doc
+asColumns = flip asColumnsWithBuff $ 1
+
+asColumnsWithBuff :: [[Doc]] -> Int -> Doc
+asColumnsWithBuff lls q = normalize
+        where
+          normalize = vcat $ map hsep
+                    $ map (\x -> pad (length x) longColumnLen empty x)
+                    $ pad' longEntryLen q
+                    $ transpose lls -- normalize column height
+          longColumnLen = maximum (map length lls)
+          longEntryLen = maximum $ map docLen (concat lls)
+
+docLen d = length $ render d
+
+-- | Pad a string on the right to reach an expected length.
+pad :: Int -> Int -> a -> [a] -> [a]
+pad lx max b ls = ls ++ replicate (max - lx) b
+
+-- | Pad a list of strings on the right with spaces.
+pad' :: Int      -- ^ Mininum number of spaces to add
+     -> Int      -- ^ Maximum number of spaces to add
+     -> [[Doc]]  -- ^ List of documents to pad
+     -> [[Doc]]
+pad' _ _ []       = []
+pad' mx q (ls:xs) = map buf ls : pad' mx q xs
+        where
+          buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
diff --git a/src/Copilot/Core/Interpret/RenderInternal.hs b/src/Copilot/Core/Interpret/RenderInternal.hs
deleted file mode 100644
--- a/src/Copilot/Core/Interpret/RenderInternal.hs
+++ /dev/null
@@ -1,130 +0,0 @@
---------------------------------------------------------------------------------
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
-
--- | Pretty-print the results of a simulation.
-
-{-# LANGUAGE Safe #-}
-
-module Copilot.Core.Interpret.RenderInternal
-  ( renderAsTable
-  , renderAsCSV
-  ) where
-
-import Data.List (intersperse, transpose, foldl')
-import Data.Maybe (catMaybes)
-import Copilot.Core.Interpret.Eval (Output, ExecTrace (..))
-import Text.PrettyPrint
-
-import Prelude hiding ((<>))
-
---------------------------------------------------------------------------------
-
--- | Render an execution trace as a table, formatted to faciliate readability.
-renderAsTable :: ExecTrace -> String
-renderAsTable
-  ExecTrace
-    { interpTriggers  = trigs
-    , interpObservers = obsvs } = ( render
-                                  . asColumns
-                                  . transpose
-                                  . (:) (ppTriggerNames ++ ppObserverNames)
-                                  . transpose
-                                  ) (ppTriggerOutputs ++ ppObserverOutputs)
-     where
-
-     ppTriggerNames :: [Doc]
-     ppTriggerNames  = map (text . (++ ":")) (map fst trigs)
-
-     ppObserverNames :: [Doc]
-     ppObserverNames = map (text . (++ ":")) (map fst obsvs)
-
-     ppTriggerOutputs :: [[Doc]]
-     ppTriggerOutputs = map (map ppTriggerOutput) (map snd trigs)
-
-     ppTriggerOutput :: Maybe [Output] -> Doc
-     ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"
-     ppTriggerOutput Nothing   = text "--"
-
-     ppObserverOutputs :: [[Doc]]
-     ppObserverOutputs = map (map text) (map snd obsvs)
-
---------------------------------------------------------------------------------
-
--- | Render an execution trace as using comma-separate value (CSV) format.
-renderAsCSV :: ExecTrace -> String
-renderAsCSV = render . unfold
-
--- | Pretty print all the steps of the execution trace and concatenate the
--- results.
-unfold :: ExecTrace -> Doc
-unfold r =
-  case step r of
-    (cs, Nothing) -> cs
-    (cs, Just r') -> cs $$ unfold r'
-
--- | Pretty print the state of the triggers, and provide a continuation
--- for the execution trace at the next point in time.
-step :: ExecTrace -> (Doc, Maybe ExecTrace)
-step ExecTrace
-       { interpTriggers  = trigs
-       } =
-  if null trigs then (empty, Nothing)
-    else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)
-
-  where
-
-  ppTriggerOutputs :: [Doc]
-  ppTriggerOutputs =
-      catMaybes
-    . fmap ppTriggerOutput
-    . map (fmap head)
-    $ trigs
-
-  ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc
-  ppTriggerOutput (_,  Nothing) = Nothing
-  ppTriggerOutput (cs, Just xs) = Just $
-    text cs <> text "," <>
-      (foldr (<>) empty . map text . intersperse ",") xs
-
-  tails :: Maybe ExecTrace
-  tails =
-    if any null (fmap (tail.snd) trigs)
-      then Nothing
-      else Just
-        ExecTrace
-          { interpTriggers  = map (fmap tail) trigs
-          , interpObservers = []
-          }
-
---------------------------------------------------------------------------------
-
-
-
--- Copied from pretty-ncols because of incompatibility with newer GHC versions.
-asColumns :: [[Doc]] -> Doc
-asColumns = flip asColumnsWithBuff $ 1
-
-asColumnsWithBuff :: [[Doc]] -> Int -> Doc
-asColumnsWithBuff lls q = normalize
-        where normalize = vcat $ map hsep
-                        $ map (\x -> pad (length x) longColumnLen empty x)
-                        $ pad' longEntryLen q
-                        $ transpose lls -- normalize column height
-              longColumnLen = maximum (map length lls)
-              longEntryLen = maximum $ map docLen (concat lls)
-
-docLen d = length $ render d
-
--- | Pad a string on the right to reach an expected length.
-pad :: Int -> Int -> a -> [a] -> [a]
-pad lx max b ls = ls ++ replicate (max - lx) b
-
--- | Pad a list of strings on the right with spaces.
-pad' :: Int      -- ^ Mininum number of spaces to add
-     -> Int      -- ^ Maximum number of spaces to add
-     -> [[Doc]]  -- ^ List of documents to pad
-     -> [[Doc]]
-pad' _ _ []       = []
-pad' mx q (ls:xs) = map buf ls : pad' mx q xs
-        where buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
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,9 +1,8 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE GADTs, Rank2Types #-}
+{-# LANGUAGE GADTs      #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE Safe       #-}
 
 -- | Internal representation of Copilot operators.
 module Copilot.Core.Operators
@@ -18,8 +17,6 @@
 import Copilot.Core.Type.Array  (Array)
 import Data.Bits
 import Data.Word                (Word32)
-
---------------------------------------------------------------------------------
 
 -- | Unary operators.
 data Op1 a b where
diff --git a/src/Copilot/Core/PrettyDot.hs b/src/Copilot/Core/PrettyDot.hs
--- a/src/Copilot/Core/PrettyDot.hs
+++ b/src/Copilot/Core/PrettyDot.hs
@@ -1,11 +1,9 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | A pretty printer for Copilot specifications as GraphViz/dot graphs.
 
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE Safe  #-}
 
 module Copilot.Core.PrettyDot
   ( prettyPrintDot
@@ -23,8 +21,6 @@
 mkExtTmpVar :: String -> String
 mkExtTmpVar = ("ext_" ++)
 
---------------------------------------------------------------------------------
-
 -- | Pretty print a Copilot Expression as a GraphViz graph part.
 --
 -- See the
@@ -52,7 +48,7 @@
                   <> text (printf "%s [label=\"def: %s\",color=blue, style=filled]\n" ((show $ ii+1)::String) (name::String) )
                   <> text (printf "%s -> %s\n" (show ii::String) (show $ ii+1::String))
                   <> r1
-                  <> r2 ,i2)
+                  <> r2, i2)
 
   Var _ name                 -> (text (printf "%s [label=\"var: %s\",color=blue, style=filled]\n" (show ii::String) (name::String) )
                   <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)
@@ -67,7 +63,7 @@
            in (text (printf "%s [label=\"op2: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp2 op::String))
                   <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))
                   <> r1
-                  <> r2 ,i2)
+                  <> r2, i2)
   Op3 op e1 e2 e3            -> let (r1,i1) = ppExprDot (ii+1) ii bb e1
                                 in let (r2,i2) = ppExprDot i1 ii bb e2
                                 in let (r3,i3) = ppExprDot i2 ii bb e3
@@ -75,7 +71,7 @@
                   <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))
                   <> r1
                   <> r2
-                  <> r3 ,i3)
+                  <> r3, i3)
 
   Label _ s e                -> let (r1,i1) = ppExprDot (ii+1) ii bb e
            in (text (printf "%s [label=\"label: %s\",color=plum, style=filled]\n" (show ii::String) (s::String))
@@ -151,8 +147,6 @@
 ppOp3 op = case op of
   Mux _    -> "mux"
 
---------------------------------------------------------------------------------
-
 -- | Pretty print a stream as a GraphViz graph part.
 ppStream :: Int        -- ^ Index or ID of the next node in the graph.
          -> Stream     -- ^ Stream to pretty print
@@ -171,8 +165,8 @@
     <> text (printf "%s [label=\"[%s]\",color=green, style=filled]\n" ((show $ i+2)::String) ((concat $ intersperse "," $ map (showWithType Haskell t) buffer )) ::String)
     <> text (printf "%s -> %s\n" (show (i+1)::String) ((show $ i+2)::String))
     <> r1, i1)
-    where (r1, i1) = ppExprDot (i+3) (i+1) True e
---------------------------------------------------------------------------------
+    where
+      (r1, i1) = ppExprDot (i+3) (i+1) True e
 
 -- | Pretty print a trigger as a GraphViz graph part.
 ppTrigger :: Int        -- ^ Index or ID of the next node in the graph.
@@ -209,8 +203,6 @@
     (r1, i1) = ppUExpr i pere bb a
     (r2, i2) = ppUExprL i1 pere bb b
 
---------------------------------------------------------------------------------
-
 -- | Pretty print an observer as a GraphViz graph part.
 ppObserver :: Int         -- ^ Index or ID of the next node in the graph.
            -> Observer    -- ^ Observer to pretty print
@@ -222,8 +214,8 @@
   =
   (text (printf "%s [label=\"observer: \n%s\",color=mediumblue, style=filled]\n" (show i::String) name::String)
   <> r1, i1)
-  where (r1, i1) = ppExprDot (i+1) i True e
---------------------------------------------------------------------------------
+  where
+    (r1, i1) = ppExprDot (i+1) i True e
 
 -- | Pretty print a property as a GraphViz graph part.
 ppProperty :: Int         -- ^ Index or ID of the next node in the graph.
@@ -236,12 +228,8 @@
   =
   (text (printf "%s [label=\"property: \n%s\",color=mediumblue, style=filled]\n" (show i::String) name::String)
   <> r1, i1)
-  where (r1, i1) = ppExprDot (i+1) i True e
-
---------------------------------------------------------------------------------
-
-
---------------------------------------------------------------------------------
+  where
+    (r1, i1) = ppExprDot (i+1) i True e
 
 -- | Pretty print a list of streams as a GraphViz graph part.
 ppStreamL :: Int        -- ^ Index or ID of the next node in the graph.
@@ -254,8 +242,6 @@
     (s1,i1) = ppStream i a
     (s2,i2) = ppStreamL i1 b
 
---------------------------------------------------------------------------------
-
 -- | Pretty print a list of triggers as a GraphViz graph part.
 ppTriggerL :: Int        -- ^ Index or ID of the next node in the graph.
            -> [Trigger]  -- ^ List of triggers to pretty print
@@ -267,8 +253,6 @@
     (s1,i1) = ppTrigger i a
     (s2,i2) = ppTriggerL i1 b
 
---------------------------------------------------------------------------------
-
 -- | Pretty print a list of observers as a GraphViz graph part.
 ppObserverL :: Int         -- ^ Index or ID of the next node in the graph.
             -> [Observer]  -- ^ List of observers to pretty print
@@ -280,9 +264,6 @@
     (s1,i1) = ppObserver i a
     (s2,i2) = ppObserverL i1 b
 
-
---------------------------------------------------------------------------------
-
 -- | Pretty print a list of properties as a GraphViz graph part.
 ppPropertyL :: Int         -- ^ Index or ID of the next node in the graph.
             -> [Property]  -- ^ List of properties to pretty print
@@ -294,8 +275,6 @@
     (s1,i1) = ppProperty i a
     (s2,i2) = ppPropertyL i1 b
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot specification as a GraphViz/dot graph.
 ppSpecDot :: Int        -- ^ Index or ID of the next node in the graph.
           -> Spec       -- ^ Spec to pretty print.
@@ -310,8 +289,6 @@
     (fs, i4) = ppPropertyL i3 (specProperties spec)
     bb = text "\n}\n"
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot expression as a GraphViz/dot graph.
 prettyPrintExprDot :: Bool     -- ^ Mark externs with the prefix @externV:@.
                    -> Expr a   -- ^ The expression to pretty print.
@@ -324,6 +301,5 @@
 -- | Pretty-print a Copilot specification as a GraphViz/dot graph.
 prettyPrintDot :: Spec -> String
 prettyPrintDot s = render r1
-  where (r1, _) = ppSpecDot 0 s
-
---------------------------------------------------------------------------------
+  where
+    (r1, _) = ppSpecDot 0 s
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
@@ -1,33 +1,27 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | A pretty printer for Copilot specifications.
 
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE Safe  #-}
 
 module Copilot.Core.PrettyPrint
   ( prettyPrint
   , ppExpr
   ) where
 
-import Copilot.Core hiding (impossible)
-import Copilot.Core.ErrorInternal (impossible)
+import Copilot.Core
+import Copilot.Core.Error (impossible)
 import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)
 import Prelude hiding (id, (<>))
 import Text.PrettyPrint.HughesPJ
 import Data.List (intersperse)
 
---------------------------------------------------------------------------------
-
 -- | Create a unique stream name by prefixing the given ID by a lowercase
 -- letter @"s"@.
 strmName :: Int -> Doc
 strmName id = text "s" <> int id
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot expression.
 --
 -- The type is ignored, and only the expression is pretty-printed.
@@ -115,8 +109,6 @@
     text "then" <+> doc2 <+>
     text "else" <+> doc3 <> text ")"
 
---------------------------------------------------------------------------------
-
 -- | Parenthesize two 'Doc's, separated by an infix 'String'.
 ppInfix :: String -> Doc -> Doc -> Doc
 ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2
@@ -125,8 +117,6 @@
 ppPrefix :: String -> Doc -> Doc
 ppPrefix cs = (text cs <+>)
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot stream as a case of a top-level function for
 -- streams of that type, by pattern matching on the stream name.
 ppStream :: Stream -> Doc
@@ -147,8 +137,6 @@
     <+> text "++"
     <+> ppExpr e
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot trigger as a case of a top-level @trigger@
 -- function, by pattern matching on the trigger name.
 ppTrigger :: Trigger -> Doc
@@ -165,8 +153,6 @@
                           map (\a -> text "arg" <+> ppUExpr a) args))
   $$  nest 2 rbrack
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot observer as a case of a top-level @observer@
 -- function, by pattern matching on the observer name.
 ppObserver :: Observer -> Doc
@@ -178,8 +164,6 @@
   <+> text "="
   <+> ppExpr e
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot property as a case of a top-level @property@
 -- function, by pattern matching on the property name.
 ppProperty :: Property -> Doc
@@ -191,8 +175,6 @@
   <+> text "="
   <+> ppExpr e
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot specification, in the following order:
 --
 -- - Streams definitions
@@ -207,10 +189,6 @@
     es = foldr (($$) . ppObserver) empty (specObservers spec)
     fs = foldr (($$) . ppProperty) empty (specProperties spec)
 
---------------------------------------------------------------------------------
-
 -- | Pretty-print a Copilot specification.
 prettyPrint :: Spec -> String
 prettyPrint = render . ppSpec
-
---------------------------------------------------------------------------------
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,9 +1,8 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE ExistentialQuantification, GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE Safe                      #-}
 
 -- | Copilot specifications constitute the main declaration of Copilot modules.
 --
@@ -26,8 +25,6 @@
 import Copilot.Core.Type (Type, Typed)
 import Data.Typeable (Typeable)
 
---------------------------------------------------------------------------------
-
 -- | A stream in an infinite succession of values of the same type.
 --
 -- Stream can carry different types of data. Boolean streams play a special
@@ -39,8 +36,6 @@
   , 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
@@ -48,8 +43,6 @@
   , observerExpr     :: Expr a
   , observerExprType :: Type a }
 
---------------------------------------------------------------------------------
-
 -- | A trigger, representing a function we execute when a boolean stream becomes
 -- true at a sample.
 data Trigger = Trigger
@@ -57,16 +50,12 @@
   , 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 }
 
---------------------------------------------------------------------------------
-
 -- | A Copilot specification is a list of streams, together with monitors on
 -- these streams implemented as observers, triggers or properties.
 data Spec = Spec
@@ -74,5 +63,3 @@
   , 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,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Typing for Core.
 --
@@ -10,16 +8,15 @@
 -- initialize variables and equivalent representations for those types in
 -- the target languages.
 
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE  ExistentialQuantification
-            , GADTs
-            , KindSignatures
-            , ScopedTypeVariables
-            , UndecidableInstances
-            , FlexibleContexts
-            , DataKinds
-            , FlexibleInstances
-#-}
+{-# LANGUAGE DataKinds                 #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts          #-}
+{-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE KindSignatures            #-}
+{-# LANGUAGE Safe                      #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE UndecidableInstances      #-}
 
 module Copilot.Core.Type
   ( Type (..)
@@ -80,9 +77,10 @@
   show f@(Field v) = fieldname f ++ ":" ++ show v
 
 instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where
-  show t = "<" ++ fields ++ ">" where
-    fields = intercalate "," $ map showfield (toValues t)
-    showfield (Value _ field) = show field
+  show t = "<" ++ fields ++ ">"
+    where
+      fields = intercalate "," $ map showfield (toValues t)
+      showfield (Value _ field) = show field
 
 -- | A Type representing the types of expressions or values handled by
 -- Copilot Core.
@@ -132,8 +130,6 @@
   (=~=) Double Double = Just Refl
   (=~=) _ _ = Nothing
 
---------------------------------------------------------------------------------
-
 -- | A simple, monomorphic representation of types that facilitates putting
 -- variables in heterogeneous lists and environments in spite of their types
 -- being different.
@@ -154,7 +150,7 @@
 
 -- | Type equality, used to help type inference.
 
-{- This instance is necessary, otherwise the type of SArray can't be inferred -}
+-- This instance is necessary, otherwise the type of SArray can't be inferred.
 
 instance Eq SimpleType where
   SBool   == SBool    = True
@@ -173,8 +169,6 @@
   SStruct == SStruct  = True
   _ == _ = False
 
---------------------------------------------------------------------------------
-
 -- | A typed expression, from which we can obtain the two type representations
 -- used by Copilot: 'Type' and 'SimpleType'.
 class (Show a, Typeable a) => Typed a where
@@ -182,8 +176,6 @@
   simpleType :: Type a -> SimpleType
   simpleType _ = SStruct
 
---------------------------------------------------------------------------------
-
 instance Typed Bool   where
   typeOf       = Bool
   simpleType _ = SBool
@@ -221,12 +213,8 @@
   typeOf                = Array typeOf
   simpleType (Array t)  = SArray t
 
---------------------------------------------------------------------------------
-
 -- | A untyped type (no phantom type).
 data UType = forall a . Typeable a => UType { uTypeType :: Type a }
 
 instance Eq UType where
   UType ty1 == UType ty2 = typeRep ty1 == typeRep ty2
-
---------------------------------------------------------------------------------
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,22 +1,19 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
-{-# LANGUAGE Safe #-}
+{-# 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
 -- explicit indexing is used for the input data. Supports arbitrary nesting of
 -- arrays.
 
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeFamilies #-}
-
 module Copilot.Core.Type.Array
   ( Array
   , array
@@ -41,12 +38,12 @@
 -- list matches the length of the array at type level.
 array :: forall n t. KnownNat n => [t] -> Array n t
 array xs | datalen == typelen = Array xs
-         | otherwise          = error errmsg where
-  datalen = length xs
-  typelen = fromIntegral $ natVal (Proxy :: Proxy n)
-  errmsg = "Length of data (" ++ show datalen ++
-           ") does not match length of type (" ++ show typelen ++ ")."
-
+         | otherwise          = error errmsg
+  where
+    datalen = length xs
+    typelen = fromIntegral $ natVal (Proxy :: Proxy n)
+    errmsg = "Length of data (" ++ show datalen ++
+             ") does not match length of type (" ++ show typelen ++ ")."
 
 -- | Association between an array and the type of the elements it contains.
 type family InnerType x where
diff --git a/src/Copilot/Core/Type/Dynamic.hs b/src/Copilot/Core/Type/Dynamic.hs
--- a/src/Copilot/Core/Type/Dynamic.hs
+++ b/src/Copilot/Core/Type/Dynamic.hs
@@ -1,10 +1,11 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE KindSignatures            #-}
+{-# LANGUAGE Rank2Types                #-}
+{-# LANGUAGE Safe                      #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
 
 -- | An implementation of dynamic types using "Copilot.Core.Type.Equality".
 -- The theory behind this technique is described the following paper:
@@ -13,22 +14,16 @@
 -- \"/Typing dynamic typing/\",
 -- ACM SIGPLAN Notices vol. 37, p. 157-166, 2002
 
-{-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables #-}
-
 module Copilot.Core.Type.Dynamic
   {-# DEPRECATED "This module is deprecated in Copilot 3.8." #-}
   ( Dynamic  (..)
   , DynamicF (..)
   , toDyn
   , fromDyn
-  , toDynF
-  , fromDynF
   ) where
 
 import Copilot.Core.Type.Equality
 
---------------------------------------------------------------------------------
-
 -- | Representation of a value accompanied by its type.
 data Dynamic :: (* -> *) -> * where
   Dynamic :: a -> t a -> Dynamic t
@@ -47,18 +42,4 @@
 fromDyn t1 (Dynamic x t2) =
   case t1 =~= t2 of
     Just Refl -> return x
-    Nothing   -> Nothing
-
--- | Enclose a function and its type in a container.
-{-# DEPRECATED toDynF "This function is deprecated in Copilot 3.6." #-}
-toDynF :: t a -> f a -> DynamicF f t
-toDynF t fx = DynamicF fx t
-
--- | Extract a value from a dynamic function container. Return 'Nothing' if
--- the value is not of the given type.
-{-# DEPRECATED fromDynF "This function is deprecated in Copilot 3.6." #-}
-fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a)
-fromDynF t1 (DynamicF fx t2) =
-  case t1 =~= t2 of
-    Just Refl -> return fx
     Nothing   -> Nothing
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
@@ -1,9 +1,8 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE GADTs, KindSignatures #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE Safe           #-}
 
 -- | Propositional equality and type equality.
 module Copilot.Core.Type.Equality
diff --git a/src/Copilot/Core/Type/Show.hs b/src/Copilot/Core/Type/Show.hs
--- a/src/Copilot/Core/Type/Show.hs
+++ b/src/Copilot/Core/Type/Show.hs
@@ -1,9 +1,8 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE ExistentialQuantification, GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE Safe                      #-}
 
 -- | Show Copilot Core types and typed values.
 module Copilot.Core.Type.Show
@@ -15,14 +14,10 @@
 
 import Copilot.Core.Type
 
---------------------------------------------------------------------------------
-
 -- | Witness datatype for showing a value, used by 'showWithType'.
 {-# DEPRECATED ShowWit "This type is deprecated in Copilot 3.7." #-}
 data ShowWit a = Show a => ShowWit
 
---------------------------------------------------------------------------------
-
 -- | Turn a type into a show witness.
 showWit :: Type a -> ShowWit a
 showWit t =
@@ -41,8 +36,6 @@
     Array t -> ShowWit
     Struct t -> ShowWit
 
---------------------------------------------------------------------------------
-
 -- | Show Copilot Core type.
 showType :: Type a -> String
 showType t =
@@ -61,8 +54,6 @@
     Array t -> "Array " ++ showType t
     Struct t -> "Struct"
 
---------------------------------------------------------------------------------
-
 -- Are we proving equivalence with a C backend, in which case we want to show
 -- Booleans as '0' and '1'.
 
@@ -70,8 +61,6 @@
 -- representation of booleans.
 data ShowType = C | Haskell
 
---------------------------------------------------------------------------------
-
 -- | Show a value. The representation depends on the type and the target
 -- language. Booleans are represented differently depending on the backend.
 showWithType :: ShowType -> Type a -> a -> String
@@ -86,5 +75,3 @@
   where
   sw = case showWit t of
          ShowWit -> show x
-
---------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Type/Uninitialized.hs b/src/Copilot/Core/Type/Uninitialized.hs
deleted file mode 100644
--- a/src/Copilot/Core/Type/Uninitialized.hs
+++ /dev/null
@@ -1,35 +0,0 @@
---------------------------------------------------------------------------------
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
-
--- | Initial values for a given type.
-
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE GADTs #-}
-
-module Copilot.Core.Type.Uninitialized
-  ( uninitialized
-  ) where
-
-import Copilot.Core.Type
-
---------------------------------------------------------------------------------
-
--- | Initial value for a given type.
---
--- Does not support structs or arrays.
-{-# DEPRECATED uninitialized "This function is deprecated in Copilot 3.6" #-}
-uninitialized :: Type a -> a
-uninitialized t =
-  case t of
-    Bool   -> False
-    Int8   -> 0
-    Int16  -> 0
-    Int32  -> 0
-    Int64  -> 0
-    Word8  -> 0
-    Word16 -> 0
-    Word32 -> 0
-    Word64 -> 0
-    Float  -> 0
-    Double -> 0
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -6,7 +6,6 @@
 import Test.Framework (Test, defaultMainWithOpts)
 
 -- Internal library modules being tested
-import qualified Test.Copilot.Core.Error
 import qualified Test.Copilot.Core.External
 import qualified Test.Copilot.Core.Interpret.Eval
 import qualified Test.Copilot.Core.Type
@@ -21,8 +20,7 @@
 -- | All unit tests in copilot-core.
 tests :: [Test.Framework.Test]
 tests =
-  [ Test.Copilot.Core.Error.tests
-  , Test.Copilot.Core.External.tests
+  [ Test.Copilot.Core.External.tests
   , Test.Copilot.Core.Interpret.Eval.tests
   , Test.Copilot.Core.Type.tests
   , Test.Copilot.Core.Type.Array.tests
diff --git a/tests/Test/Copilot/Core/Error.hs b/tests/Test/Copilot/Core/Error.hs
deleted file mode 100644
--- a/tests/Test/Copilot/Core/Error.hs
+++ /dev/null
@@ -1,35 +0,0 @@
--- | Test copilot-core:Copilot.Core.Error.
-module Test.Copilot.Core.Error where
-
--- External imports
-import Test.Framework                 (Test, testGroup)
-import Test.Framework.Providers.HUnit (testCase)
-import Test.HUnit                     (assertBool)
-
--- Internal imports: auxiliary testing facilities
-import Test.Extra (withoutException)
-
--- Internal imports: library modules being tested
-import Copilot.Core.Error (badUsage, impossible)
-
--- | All unit tests for copilot-core:Copilot.Core.Error.
-tests :: Test.Framework.Test
-tests =
-  testGroup "Copilot.Core.Error"
-    [ testCase "impossible" testErrorImpossible
-    , testCase "badUsage"   testErrorBadUsage
-    ]
-
--- * Individual tests
-
--- | Test that 'Error.impossible' always throws an exception of some kind.
-testErrorImpossible :: IO ()
-testErrorImpossible = do
-  res <- not <$> withoutException (impossible "func1" "pkg1")
-  assertBool "The function impossible should fail with an exception" res
-
--- | Test that 'Error.badUsage' always throws an exception of some kind.
-testErrorBadUsage :: IO ()
-testErrorBadUsage = do
-  res <- not <$> withoutException (badUsage "func1")
-  assertBool "The function badUsage should fail with an exception" res
diff --git a/tests/Test/Extra.hs b/tests/Test/Extra.hs
--- a/tests/Test/Extra.hs
+++ b/tests/Test/Extra.hs
@@ -1,21 +1,8 @@
-{-# LANGUAGE ScopedTypeVariables #-}
 -- | Auxiliary testing helper functions.
 module Test.Extra where
 
 -- External imports
-import Control.Arrow     ((***))
-import Control.Exception (SomeException, catch)
-
--- * Detecting exceptions
-
--- | Test that a computation terminates without throwing an exception.
---
--- Returns 'True' if the computation can be completed without an exception,
--- and 'False' otherwise.
-withoutException :: IO a -> IO Bool
-withoutException e =
-  catch (e >> return True)
-        (\(_ :: SomeException) -> return False)
+import Control.Arrow ((***))
 
 -- * Function application