diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2022-05-06
+        * Version bump (3.9). (#320)
+        * Compliance with style guide (partial). (#316)
+        * Add support for GHC 9.0. (#294)
+
 2022-03-07
         * Version bump (3.8). (#298)
         * Mark package as uncurated to avoid modification. (#288)
diff --git a/copilot.cabal b/copilot.cabal
--- a/copilot.cabal
+++ b/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             3.8
+version:             3.9
 cabal-version:       >= 1.10
 license:             BSD3
 license-file:        LICENSE
@@ -52,11 +52,11 @@
                      , directory            >= 1.3  && < 1.4
                      , filepath             >= 1.4  && < 1.5
 
-                     , copilot-core         >= 3.8  && < 3.9
-                     , copilot-theorem      >= 3.8  && < 3.9
-                     , copilot-language     >= 3.8  && < 3.9
-                     , copilot-libraries    >= 3.8  && < 3.9
-                     , copilot-c99          >= 3.8  && < 3.9
+                     , copilot-core         >= 3.9  && < 3.10
+                     , copilot-theorem      >= 3.9  && < 3.10
+                     , copilot-language     >= 3.9  && < 3.10
+                     , copilot-libraries    >= 3.9  && < 3.10
+                     , copilot-c99          >= 3.9  && < 3.10
 
 
     exposed-modules: Language.Copilot, Language.Copilot.Main
diff --git a/examples/AddMult.hs b/examples/AddMult.hs
--- a/examples/AddMult.hs
+++ b/examples/AddMult.hs
@@ -1,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Another small example that calculates a constant value using a recursive
 -- function.
diff --git a/examples/Array.hs b/examples/Array.hs
--- a/examples/Array.hs
+++ b/examples/Array.hs
@@ -1,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | This is a simple example for arrays. As a program, it does not make much
 -- sense, however it shows of the features of arrays nicely.
@@ -8,8 +6,8 @@
 -- | Enable compiler extension for type-level data, necesary for the array
 -- length.
 
-{-# LANGUAGE RebindableSyntax #-}
 {-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE RebindableSyntax #-}
 
 module Main where
 
diff --git a/examples/Cast.hs b/examples/Cast.hs
--- a/examples/Cast.hs
+++ b/examples/Cast.hs
@@ -1,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Examples of casting types.
 
diff --git a/examples/Clock.hs b/examples/Clock.hs
--- a/examples/Clock.hs
+++ b/examples/Clock.hs
@@ -1,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Example showing usage of clocks to generate periodically recurring truth
 -- values.
diff --git a/examples/Counter.hs b/examples/Counter.hs
--- a/examples/Counter.hs
+++ b/examples/Counter.hs
@@ -1,6 +1,4 @@
--------------------------------------------------------------------------------
 -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Example showing an implementation of a resettable counter.
 
@@ -22,8 +20,9 @@
 
 -- Counter that resets when it reaches 256
 bytecounter :: Stream Int32
-bytecounter = counter true reset where
-  reset = counter true false `mod` 256 == 0
+bytecounter = counter true reset
+  where
+    reset = counter true false `mod` 256 == 0
 
 spec :: Spec
 spec = trigger "counter" true [arg $ bytecounter]
diff --git a/examples/Engine.hs b/examples/Engine.hs
--- a/examples/Engine.hs
+++ b/examples/Engine.hs
@@ -1,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Example implementing an engine cooling control system.
 
@@ -11,11 +9,10 @@
 import Language.Copilot
 import qualified Prelude as P
 
-{- If the majority of the engine temperature probes exeeds 250 degrees, then
- - the cooler is engaged and remains engaged until the majority of the engine
- - temperature probes drop to 250 or below.  Otherwise, trigger an immediate
- - shutdown of the engine.
--}
+-- If the majority of the engine temperature probes exeeds 250 degrees, then
+-- the cooler is engaged and remains engaged until the majority of the engine
+-- temperature probes drop to 250 or below.  Otherwise, trigger an immediate
+-- shutdown of the engine.
 
 engineMonitor :: Spec
 engineMonitor = do
@@ -28,7 +25,7 @@
   exceed   = map (> 250) vals
   maj      = majority exceed
   checkMaj = aMajority exceed maj
-  ok       = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) 
+  ok       = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler)
 
   two51  = Just $ [251, 251] P.++ repeat (250 :: Word8)
   zero   = Just $ repeat (0 :: Word8)
diff --git a/examples/Heater.hs b/examples/Heater.hs
--- a/examples/Heater.hs
+++ b/examples/Heater.hs
@@ -1,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright 2019 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- This is a simple example with basic usage. It implements a simple home
 -- heating system: It heats when temp gets too low, and stops when it is high
diff --git a/examples/Structs.hs b/examples/Structs.hs
--- a/examples/Structs.hs
+++ b/examples/Structs.hs
@@ -11,7 +11,6 @@
 import Language.Copilot
 import Copilot.Compile.C99
 
-
 -- | Definition for `Volts`.
 data Volts = Volts
   { numVolts :: Field "numVolts" Word16
@@ -65,7 +64,6 @@
   trigger "equalityDifferentIndices"
     ((((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4))
     [arg battery]
-
 
 main :: IO ()
 main = do
diff --git a/examples/Voting.hs b/examples/Voting.hs
--- a/examples/Voting.hs
+++ b/examples/Voting.hs
@@ -1,6 +1,4 @@
---------------------------------------------------------------------------------
 -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
 
 -- | Fault-tolerant voting examples.
 
diff --git a/examples/WCV.hs b/examples/WCV.hs
--- a/examples/WCV.hs
+++ b/examples/WCV.hs
@@ -3,7 +3,7 @@
 -- Well-Clear Bounday Models for the Integration of UAS in the NAS',
 -- https://ntrs.nasa.gov/citations/20140010078.
 
-{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DataKinds        #-}
 {-# LANGUAGE RebindableSyntax #-}
 
 module Main where
@@ -14,7 +14,6 @@
 import Data.Foldable (forM_)
 import qualified Control.Monad as Monad
 
-
 -- | `dthr` is the horizontal distance threshold.
 dthr :: Stream Double
 dthr = extern "dthr" Nothing
@@ -33,10 +32,7 @@
 
 type Vect2 = (Stream Double, Stream Double)
 
-
---------------------------------
 -- External streams for relative position and velocity.
---------------------------------
 
 -- | The relative x velocity between ownship and the intruder.
 vx :: Stream Double
@@ -54,7 +50,6 @@
 v :: (Stream Double, Stream Double)
 v = (vx, vy)
 
-
 -- | The relative x position between ownship and the intruder.
 sx :: Stream Double
 sx = extern "relative_position_x" Nothing
@@ -71,10 +66,7 @@
 s :: (Stream Double, Stream Double)
 s = (sx, sy)
 
-
-------------------
 -- The following section contains basic libraries for working with vectors.
-------------------
 
 -- | Multiply two Vectors.
 (|*|) :: Vect2 -> Vect2 -> Stream Double
@@ -101,11 +93,8 @@
 neg :: Vect2 -> Vect2
 neg (x, y) = (negate x, negate y)
 
-
---------------------
 -- From here on the algorithm, as described by the paper mentioned on the top
 -- of this file, is implemented. Please refer to the paper for details.
---------------------
 
 tau :: Vect2 -> Vect2 -> Stream Double
 tau s v = if s |*| v < 0
@@ -134,7 +123,6 @@
 theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double
 theta s v d e = (-(s |*| v) + e * (sqrt $ delta s v d)) / (sq v)
 
-
 tcoa :: Stream Double -> Stream Double -> Stream Double
 tcoa sz vz = if (sz * vz) < 0
                then (-sz) / vz
@@ -143,10 +131,7 @@
 dcpa :: Vect2 -> Vect2 -> Stream Double
 dcpa s@(sx, sy) v@(vx, vy) = norm (sx + (tcpa s v) * vx, sy + (tcpa s v) * vy)
 
-
---------------------------
 -- Well clear Violation --
---------------------------
 
 -- | Determines if the well clear property is violated or not.
 wcv :: (Vect2 -> Vect2 -> Stream Double) ->
@@ -168,7 +153,6 @@
 spec = do
   Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v)))
   -- Monad.void $ prop "3d" (forall $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
-
 
 main :: IO ()
 main = do
diff --git a/examples/what4/Arithmetic.hs b/examples/what4/Arithmetic.hs
--- a/examples/what4/Arithmetic.hs
+++ b/examples/what4/Arithmetic.hs
@@ -38,7 +38,6 @@
   -- Another example with floats. This fails, because it isn't true.
   void $ prop "Example 6" (forall ((efloat + 1) /= efloat))
 
-
 main :: IO ()
 main = do
   spec' <- reify spec
diff --git a/examples/what4/Propositional.hs b/examples/what4/Propositional.hs
--- a/examples/what4/Propositional.hs
+++ b/examples/what4/Propositional.hs
@@ -46,7 +46,6 @@
   let a = extern "a" Nothing
   void $ prop "Example 7" (forall (a || not a))
 
-
 main :: IO ()
 main = do
   spec' <- reify spec
diff --git a/examples/what4/Structs.hs b/examples/what4/Structs.hs
--- a/examples/what4/Structs.hs
+++ b/examples/what4/Structs.hs
@@ -12,7 +12,6 @@
 import Language.Copilot
 import Copilot.Theorem.What4
 
-
 -- | Definition for `Volts`.
 data Volts = Volts
   { numVolts :: Field "numVolts" Word16
@@ -64,7 +63,6 @@
   -- false).
   void $ prop "Example 2" $ forall $
     (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)
-
 
 main :: IO ()
 main = do
diff --git a/src/Language/Copilot/Main.hs b/src/Language/Copilot/Main.hs
--- a/src/Language/Copilot/Main.hs
+++ b/src/Language/Copilot/Main.hs
@@ -44,7 +44,6 @@
                                     <> metavar "INT" <> showDefault
                                     <> help "Interpret specification and write result to output")
 
-
 -- | Create a main to either compile or interpret a copilot specification.
 --
 -- This function must be provided an auxiliary function capable of compiling
@@ -63,18 +62,19 @@
 --     * @--interpret/-i NUM@: interpret the specification for a given number
 --       of steps.
 copilotMain :: Interpreter -> Printer -> Compiler -> Spec -> IO ()
-copilotMain interp pretty comp spec = main =<< execParser opts where
-  opts = info (cmdargs <**> helper) fullDesc
+copilotMain interp pretty comp spec = main =<< execParser opts
+  where
+    opts = info (cmdargs <**> helper) fullDesc
 
-  main :: CmdArgs -> IO ()
-  main args = do
-    let iters = ainterpret args
-    when (apretty args)       $ pretty spec
-    when (iters Prelude.> 0)  $ interp (fromIntegral iters) spec
+    main :: CmdArgs -> IO ()
+    main args = do
+      let iters = ainterpret args
+      when (apretty args)       $ pretty spec
+      when (iters Prelude.> 0)  $ interp (fromIntegral iters) spec
 
-    when (not $ acompile args) $ do
-      spec' <- reify spec
-      comp (aoutput args) spec'
+      when (not $ acompile args) $ do
+        spec' <- reify spec
+        comp (aoutput args) spec'
 
 -- | Create a main function with a default interpreter and pretty printer.
 --