diff --git a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
index ce822e558..593417b36 100644
--- a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
@@ -75,12 +75,14 @@ mkStructDecln (Struct x) = C.TypeDecln struct
 
     mkField :: Value a -> C.FieldDecln
     mkField (Value ty field) = C.FieldDecln (transType ty) (fieldName field)
+mkStructDecln _ = error "Unhandled case"
 
 -- | Write a forward struct declaration.
 mkStructForwDecln :: Struct a => Type a -> C.Decln
 mkStructForwDecln (Struct x) = C.TypeDecln struct
   where
     struct = C.TypeSpec $ C.Struct (typeName x)
+mkStructForwDecln _ = error "Unhandled case"
 
 -- * Ring buffers
 
diff --git a/copilot-c99/src/Copilot/Compile/C99/Expr.hs b/copilot-c99/src/Copilot/Compile/C99/Expr.hs
index 14e129be9..d6d459611 100644
--- a/copilot-c99/src/Copilot/Compile/C99/Expr.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/Expr.hs
@@ -61,8 +61,8 @@ transExpr (Op2 (UpdateField ty1@(Struct _) ty2 f) e1 e2) = do
   e2' <- transExpr e2
 
   -- Variable to hold the updated struct
-  (i, _, _) <- get
-  let varName = "_v" ++ show i
+  (i', _, _) <- get
+  let varName = "_v" ++ show i'
   modify (\(i, x, y) -> (i + 1, x, y))
 
   -- Add new var decl
@@ -101,14 +101,14 @@ transExpr (Op2 op e1 e2) = do
   e2' <- transExpr e2
   return $ transOp2 op e1' e2'
 
-transExpr e@(Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do
+transExpr (Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do
   e1' <- transExpr e1
   e2' <- transExpr e2
   e3' <- transExpr e3
 
   -- Variable to hold the updated array
-  (i, _, _) <- get
-  let varName = "_v" ++ show i
+  (i', _, _) <- get
+  let varName = "_v" ++ show i'
   modify (\(i, x, y) -> (i + 1, x, y))
 
   -- Add new var decl
@@ -117,18 +117,19 @@ transExpr e@(Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do
   modify (\(i, x, y) -> (i, x ++ [initDecl], y))
 
   let size :: Type (Array n t) -> C.Expr
-      size arrTy@(Array ty) = C.LitInt (fromIntegral $ typeLength arrTy)
+      size arrT'@(Array ty) = C.LitInt (fromIntegral $ typeLength arrT')
                          C..* C.SizeOfType (C.TypeName $ transType ty)
+      size _ = error "Unhandled case"
 
   -- Initialize the var to the same value as the original array
   let initStmt = C.Expr $ memcpy (C.Ident varName) e1' (size arrTy)
 
   -- Update element of array
   let updateStmt = case ty2 of
-        Array _ -> C.Expr $ memcpy dest e3' size
+        Array _ -> C.Expr $ memcpy dest e3' siz'
           where
             dest = C.Index (C.Ident varName) e2'
-            size = C.LitInt
+            siz' = C.LitInt
                        (fromIntegral $ typeSize ty2)
                        C..* C.SizeOfType (C.TypeName (tyElemName ty2))
 
@@ -183,6 +184,7 @@ transOp1 op e =
     BwNot    _    -> (C..~) e
     Cast     _ ty -> C.Cast (transTypeName ty) e
     GetField (Struct _)  _ f -> C.Dot e (accessorName f)
+    _             -> error "Unhandled case"
 
 -- | Translates a Copilot binary operator and its arguments into a C99
 -- expression.
diff --git a/copilot-c99/src/Copilot/Compile/C99/Representation.hs b/copilot-c99/src/Copilot/Compile/C99/Representation.hs
index 886808a8a..e0ffaa2fa 100644
--- a/copilot-c99/src/Copilot/Compile/C99/Representation.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/Representation.hs
@@ -16,6 +16,6 @@ data UniqueTrigger = UniqueTrigger UniqueTriggerId Trigger
 
 -- | Given a list of triggers, make their names unique.
 mkUniqueTriggers :: [Trigger] -> [UniqueTrigger]
-mkUniqueTriggers ts = zipWith mkUnique ts [0..]
+mkUniqueTriggers ts = zipWith mkUnique ts [0 :: Integer ..]
   where
     mkUnique t@(Trigger name _ _) n = UniqueTrigger (name ++ "_" ++ show n) t
diff --git a/copilot-c99/tests/Test/Copilot/Compile/C99.hs b/copilot-c99/tests/Test/Copilot/Compile/C99.hs
index 60276e870..00344417f 100644
--- a/copilot-c99/tests/Test/Copilot/Compile/C99.hs
+++ b/copilot-c99/tests/Test/Copilot/Compile/C99.hs
@@ -34,8 +34,6 @@ import Test.QuickCheck.Gen                  (chooseAny, chooseBoundedIntegral)
 
 -- External imports: Copilot
 import Copilot.Core            hiding (Property)
-import Copilot.Core.Type.Array (array)
-
 -- External imports: Modules being tested
 import Copilot.Compile.C99 (cSettingsOutputDirectory, compile, compileWith,
                             mkDefaultCSettings)
@@ -434,15 +432,15 @@ funCompose2 (f1, g1) (f2, g2) (f3, g3) =
 
 -- | Test case specification for specs with one input variable and one output.
 data TestCase1 a b = TestCase1
-  { wrapTC1Expr :: Spec
+  Spec
     -- ^ Specification containing a trigger an extern of type 'a' and a trigger
     -- with an argument of type 'b'.
 
-  , wrapTC1Fun :: [a] -> [b]
+  ([a] -> [b])
     -- ^ Function expected to function in the same way as the Spec being
     -- tested.
 
-  , wrapTC1CopInp :: (String -> String, String, String, Gen a)
+  (String -> String, String, String, Gen a)
     -- ^ Input specification.
     --
     -- - The first element is a function that prints the variable declaration
@@ -456,26 +454,26 @@ data TestCase1 a b = TestCase1
     -- - The latter contains a randomized generator for values of the given
     -- type.
 
-  , wrapTC1CopOut :: (String, String)
+  (String, String)
     -- ^ Output specification.
     --
     -- The first element of the tuple contains the type of the output in C.
     --
     -- The second element of the tuple is the formatting string when printing
     -- values of the given kind.
-  }
+
 
 -- | Test case specification for specs with two input variables and one output.
 data TestCase2 a b c = TestCase2
-  { wrapTC2Expr :: Spec
+  Spec
     -- ^ Specification containing a trigger an extern of type 'a' and a trigger
     -- with an argument of type 'b'.
 
-  , wrapTC2Fun :: [a] -> [b] -> [c]
+  ([a] -> [b] -> [c])
     -- ^ Function expected to function in the same way as the Spec being
     -- tested.
 
-  , wrapTC2CopInp1 :: (String -> String, String, String, Gen a)
+  (String -> String, String, String, Gen a)
     -- ^ Input specification for the first input.
     --
     -- - The first element is a function that prints the variable declaration
@@ -489,7 +487,7 @@ data TestCase2 a b c = TestCase2
     -- - The latter contains a randomized generator for values of the given
     -- type.
 
-  , wrapTC2CopInp2 :: (String -> String, String, String, Gen b)
+  (String -> String, String, String, Gen b)
     -- ^ Input specification for the second input.
     --
     -- - The first element is a function that prints the variable declaration
@@ -503,14 +501,14 @@ data TestCase2 a b c = TestCase2
     -- - The latter contains a randomized generator for values of the given
     -- type.
 
-  , wrapTC2CopOut :: (String, String)
+  (String, String)
     -- ^ Output specification.
     --
     -- The first element of the tuple contains the type of the output in C.
     --
     -- The second element of the tuple is the formatting string when printing
     -- values of the given kind.
-  }
+
 
 -- | Generate test cases for expressions that behave like unary functions.
 mkTestCase1 :: (Typed a, Typed b)
diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal
index 6c18d6ca3..f2ee3e6ee 100644
--- a/copilot-core/copilot-core.cabal
+++ b/copilot-core/copilot-core.cabal
@@ -39,7 +39,6 @@ library
 
   ghc-options:
     -Wall
-    -fno-warn-orphans
 
   build-depends:
     base >= 4.9 && < 5
diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs
index b290810c2..b91d7e79e 100644
--- a/copilot-core/src/Copilot/Core/Type.hs
+++ b/copilot-core/src/Copilot/Core/Type.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE DataKinds                 #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleContexts          #-}
@@ -45,21 +46,22 @@ module Copilot.Core.Type
   where
 
 -- External imports
-import Data.Char          (isLower, isUpper, toLower)
-import Data.Coerce        (coerce)
-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, eqT, typeRep)
-import Data.Word          (Word16, Word32, Word64, Word8)
-import GHC.Generics       (Datatype (..), D1, Generic (..), K1 (..), M1 (..),
-                           U1 (..), (:*:) (..))
-import GHC.TypeLits       (KnownNat, KnownSymbol, Symbol, natVal, sameNat,
-                           sameSymbol, symbolVal)
+import           Data.Char               (isLower, isUpper, toLower)
+import           Data.Coerce             (coerce)
+import           Data.Int                (Int16, Int32, Int64, Int8)
+import qualified Data.Kind               as DK
+import           Data.List               (intercalate)
+import           Data.Proxy              (Proxy (..))
+import           Data.Type.Equality      as DE
+import           Data.Typeable           (Typeable, eqT, typeRep)
+import           Data.Word               (Word16, Word32, Word64, Word8)
+import           GHC.Generics            (D1, Datatype (..), Generic (..),
+                                          K1 (..), M1 (..), U1 (..), (:*:) (..))
+import           GHC.TypeLits            (KnownNat, KnownSymbol, Symbol, natVal,
+                                          sameNat, sameSymbol, symbolVal)
 
 -- Internal imports
-import Copilot.Core.Type.Array (Array)
+import           Copilot.Core.Type.Array (Array)
 
 -- | The value of that is a product or struct, defined as a constructor with
 -- several fields.
@@ -139,7 +141,7 @@ instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where
 -- Note that both arrays and structs use dependently typed features. In the
 -- 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
+data Type :: DK.Type -> DK.Type where
   Bool   :: Type Bool
   Int8   :: Type Int8
   Int16  :: Type Int16
@@ -165,6 +167,7 @@ typeLength _ = fromIntegral $ natVal (Proxy :: Proxy n)
 typeSize :: forall n t . KnownNat n => Type (Array n t) -> Int
 typeSize ty@(Array ty'@(Array _)) = typeLength ty * typeSize ty'
 typeSize ty@(Array _            ) = typeLength ty
+typeSize ty = error $ "There is a bug in the type checker " ++ show ty
 
 instance TestEquality Type where
   testEquality Bool   Bool   = Just DE.Refl
@@ -286,7 +289,9 @@ instance Typed Double where
 
 instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
   typeOf               = Array typeOf
-  simpleType (Array t) = SArray t
+  simpleType t         = case t of
+    Array t' -> SArray t'
+    o        -> error $ "There is a bug in the type checker " ++ show o
 
 -- | A untyped type (no phantom type).
 data UType = forall a . Typeable a => UType (Type a)
diff --git a/copilot-core/src/Copilot/Core/Type/Array.hs b/copilot-core/src/Copilot/Core/Type/Array.hs
index b11e8949b..63e25fb5b 100644
--- a/copilot-core/src/Copilot/Core/Type/Array.hs
+++ b/copilot-core/src/Copilot/Core/Type/Array.hs
@@ -53,7 +53,7 @@ arrayUpdate (Array []) _ _ = error errMsg
   where
     errMsg = "copilot-core: arrayUpdate: Attempt to update empty array"
 
-arrayUpdate (Array (x:xs)) 0 y = Array (y:xs)
+arrayUpdate (Array (_:xs)) 0 y = Array (y:xs)
 
 arrayUpdate (Array (x:xs)) n y =
     arrayAppend x (arrayUpdate (Array xs) (n - 1) y)
@@ -61,4 +61,4 @@ arrayUpdate (Array (x:xs)) n y =
     -- | Append to an array while preserving length information at the type
     -- level.
     arrayAppend :: a -> Array (n - 1) a -> Array n a
-    arrayAppend x (Array xs) = Array (x:xs)
+    arrayAppend x' (Array xs') = Array (x':xs')
diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs
index 9f9cb6d5e..bb202e5d1 100644
--- a/copilot-core/tests/Test/Copilot/Core/Type.hs
+++ b/copilot-core/tests/Test/Copilot/Core/Type.hs
@@ -7,7 +7,6 @@ module Test.Copilot.Core.Type where
 
 -- External imports
 import Data.Int                             (Int16, Int32, Int64, Int8)
-import Data.Maybe                           (isJust)
 import Data.Proxy                           (Proxy (..))
 import Data.Type.Equality                   (TestEquality (..), testEquality,
                                              (:~:) (..))
@@ -136,8 +135,10 @@ testSimpleTypesEqualityTransitive =
 -- | Test that each type is only equal to itself.
 testSimpleTypesEqualityUniqueness :: Property
 testSimpleTypesEqualityUniqueness =
-  forAllBlind (shuffle simpleTypes) $ \(t:ts) ->
-    notElem t ts
+  forAllBlind (shuffle simpleTypes) $
+    \x -> case x of
+      []     -> False
+      (t:ts) -> notElem t ts
 
 -- | Simple types tested.
 simpleTypes :: [SimpleType]
diff --git a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs
index e070f138b..a8119f5ea 100644
--- a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs
+++ b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs
@@ -141,13 +141,13 @@ testArrayUpdateWrong len =
 testArrayMakeWrongLength :: forall n . KnownNat n => Proxy n -> Property
 testArrayMakeWrongLength len =
     expectFailure           $
-    forAll wrongLength      $ \length ->
-    forAll (xsInt64 length) $ \ls ->
+    forAll wrongLength      $ \lengt' ->
+    forAll (xsInt64 lengt') $ \ls ->
       let array' :: Array n Int64
           array' = array ls
       in arrayElems array' == ls
   where
-    xsInt64 length = vectorOf length arbitrary
+    xsInt64 lengt' = vectorOf lengt' arbitrary
     expectedLength = fromIntegral (natVal len)
     wrongLength    = (expectedLength +) . getNonNegative <$> arbitrary
 
@@ -157,7 +157,7 @@ testArrayUpdateElems :: forall n . KnownNat n => Proxy n -> Property
 testArrayUpdateElems len =
     forAll xsInt64  $ \ls ->
     forAll position $ \p ->
-    forAll xInt64   $ \v ->
+    forAll xInt64   $ \_ ->
       let -- Original array
           array' :: Array n Int64
           array' = array ls
diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
index 462b5853e..c03c92052 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs
+++ b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
@@ -19,7 +19,7 @@ module Copilot.Interpret.Eval
 import Copilot.Core            (Expr (..), Field (..), Id, Name, Observer (..),
                                 Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),
                                 Trigger (..), Type (..), UExpr (..), Value (..),
-				arrayElems, arrayUpdate, specObservers,
+                                arrayElems, arrayUpdate, specObservers,
                                 specStreams, specTriggers, updateField)
 import Copilot.Interpret.Error (badUsage)
 
@@ -32,7 +32,6 @@ import Data.Dynamic      (Dynamic, fromDynamic, toDyn)
 import Data.List         (transpose)
 import Data.Maybe        (fromJust)
 import Data.Typeable     (Typeable)
-import GHC.TypeLits      (KnownNat, Nat, natVal)
 
 -- | Exceptions that may be thrown during interpretation of a Copilot
 -- specification.
@@ -142,14 +141,15 @@ type LocalEnv = [(Name, Dynamic)]
 evalExpr_ :: Typeable a => Int -> Expr a -> LocalEnv -> Env Id -> a
 evalExpr_ k e0 locs strms = case e0 of
   Const _ x                          -> x
-  Drop t i id                        ->
-    let Just buff = lookup id strms >>= fromDynamic in
-    reverse buff !! (fromIntegral i + k)
-  Local t1 _ name e1 e2              ->
+  Drop _ i id                        ->
+    case lookup id strms >>= fromDynamic of
+      Just buff -> reverse buff !! (fromIntegral i + k)
+      Nothing   -> error $ "No id " ++ show id ++ " in " ++ show strms
+  Local _ _ name e1 e2               ->
     let x     = evalExpr_ k e1 locs strms in
     let locs' = (name, toDyn x) : locs  in
     x `seq` locs' `seq` evalExpr_ k e2  locs' strms
-  Var t name                         -> fromJust $ lookup name locs >>= fromDynamic
+  Var _ name                         -> fromJust $ lookup name locs >>= fromDynamic
   ExternVar _ name xs                -> evalExternVar k name xs
   Op1 op e1                          ->
     let ev1 = evalExpr_ k e1 locs strms in
@@ -210,6 +210,7 @@ evalOp1 op = case op of
     BwNot _    -> complement
     Cast _ _   -> P.fromIntegral
     GetField (Struct _) _ f -> unfield . f
+    GetField {} -> error "There is a bug in the type checker"
   where
     -- Used to help GHC pick a return type for ceiling/floor
     idI :: Integer -> Integer
@@ -247,11 +248,12 @@ evalOp2 op = case op of
   BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
   Index    _   -> \xs n -> (arrayElems xs) !! (fromIntegral n)
 
-  UpdateField (Struct _) ty (fieldAccessor :: a -> Field s b) ->
+  UpdateField (Struct _) ty (_fieldAccessor :: a -> Field s b) ->
     \stream fieldValue ->
       let newField :: Field s b
           newField = Field fieldValue
       in updateField stream (Value ty newField)
+  UpdateField {} -> error "There is a bug in the type checker"
 
 -- | Apply a function to two numbers, so long as the second one is
 -- not zero.
@@ -267,14 +269,12 @@ catchZero f x y = f x y
 -- '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
-evalOp3 (UpdateArray ty) = \xs n x -> arrayUpdate xs (fromIntegral n) x
+evalOp3 (UpdateArray _)  = \xs n x -> arrayUpdate xs (fromIntegral n) x
 
 -- | Turn a stream into a key-value pair that can be added to an 'Env' for
 -- simulation.
 initStrm :: Stream -> (Id, Dynamic)
-initStrm Stream { streamId       = id
-                , streamBuffer   = buffer
-                , streamExprType = t } =
+initStrm Stream { streamId = id, streamBuffer = buffer } =
   (id, toDyn (reverse buffer))
 
 -- | Evaluate several streams for a number of steps, producing the environment
@@ -291,9 +291,7 @@ evalStreams top specStrms initStrms =
     evalStreams_ (k+1) $! strms_
     where
     strms_ = map evalStream specStrms
-    evalStream Stream { streamId       = id
-                      , streamExpr     = e
-                      , streamExprType = t } =
+    evalStream Stream { streamId = id, streamExpr = e } =
       let xs = fromJust $ lookup id strms >>= fromDynamic      in
       let x  = evalExpr_ k e [] strms                          in
       let ls = x `seq` (x:xs)                                  in
@@ -402,5 +400,5 @@ showWit t =
     Word64 -> ShowWit
     Float  -> ShowWit
     Double -> ShowWit
-    Array t -> ShowWit
-    Struct t -> ShowWit
+    Array _ -> ShowWit
+    Struct _ -> ShowWit
diff --git a/copilot-interpreter/src/Copilot/Interpret/Render.hs b/copilot-interpreter/src/Copilot/Interpret/Render.hs
index 3b6241a8c..fe0c33f7c 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Render.hs
+++ b/copilot-interpreter/src/Copilot/Interpret/Render.hs
@@ -10,7 +10,7 @@ module Copilot.Interpret.Render
   ) where
 
 import Data.List (intersperse, transpose, foldl')
-import Data.Maybe (catMaybes)
+import Data.Maybe (mapMaybe)
 import Copilot.Interpret.Eval (Output, ExecTrace (..))
 import Text.PrettyPrint
 
@@ -69,25 +69,22 @@ step ExecTrace
   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 $
+  ppTriggerOutputs = mapMaybe ppTriggerOutput trigs
+
+  ppTriggerOutput :: (String, [Maybe [Output]]) -> Maybe Doc
+  ppTriggerOutput (cs, Just xs : _) = Just $
     text cs <> text "," <>
       (foldr (<>) empty . map text . intersperse ",") xs
+  ppTriggerOutput (_,  Nothing : _) = Nothing
+  ppTriggerOutput (_,  []) = Nothing
 
   tails :: Maybe ExecTrace
   tails =
-    if any null (fmap (tail.snd) trigs)
+    if any null (fmap (drop 1.snd) trigs)
       then Nothing
       else Just
         ExecTrace
-          { interpTriggers  = map (fmap tail) trigs
+          { interpTriggers  = map (fmap (drop 1)) trigs
           , interpObservers = []
           }
 
@@ -105,11 +102,12 @@ asColumnsWithBuff lls q = normalize
           longColumnLen = maximum (map length lls)
           longEntryLen = maximum $ map docLen (concat lls)
 
+docLen :: Doc -> Int
 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 lx mx b ls = ls ++ replicate (mx - lx) b
 
 -- | Pad a list of strings on the right with spaces.
 pad' :: Int      -- ^ Mininum number of spaces to add
diff --git a/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs b/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
index bcabddc21..1e75e212a 100644
--- a/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
+++ b/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
@@ -11,7 +11,6 @@ module Test.Copilot.Interpret.Eval where
 import Data.Bits                            (Bits, complement, shiftL, shiftR,
                                              xor, (.&.), (.|.))
 import Data.Int                             (Int16, Int32, Int64, Int8)
-import Data.List                            (lookup)
 import Data.Maybe                           (fromMaybe)
 import Data.Typeable                        (Typeable)
 import Data.Word                            (Word16, Word32, Word64, Word8)
@@ -36,6 +35,7 @@ import Copilot.PrettyPrint      (ppExpr)
 
 -- Internal imports: auxiliary functions
 import Test.Extra (apply1, apply2, apply3)
+import Text.Read  (readEither)
 
 -- * Constants
 
@@ -747,7 +747,7 @@ checkSemanticsP steps streams (SemanticsP (expr, exprList)) =
     any isNaN' expectation || resultValues == expectation
   where
     -- Limit expectation to the number of evaluation steps.
-    expectation = take steps exprList
+    expectation = pure <$> take steps exprList
 
     -- Obtain the results by looking up the observer in the spec
     -- and parsing the results into Haskell values.
@@ -772,8 +772,8 @@ checkSemanticsP steps streams (SemanticsP (expr, exprList)) =
 -- * Auxiliary
 
 -- | Read a Haskell value from the output of the evaluator.
-readResult :: Read a => String -> a
-readResult = read . readResult'
+readResult :: Read a => String -> Either String a
+readResult = readEither . readResult'
   where
     readResult' :: String -> String
     readResult' "false" = "False"
@@ -800,5 +800,5 @@ showType t =
     Word64 -> "Word64"
     Float  -> "Float"
     Double -> "Double"
-    Array t -> "Array " ++ showType t
-    Struct t -> "Struct"
+    Array t' -> "Array " ++ showType t'
+    Struct _ -> "Struct"
diff --git a/copilot-language/src/Copilot/Language.hs b/copilot-language/src/Copilot/Language.hs
index 674d601f7..1174d821b 100644
--- a/copilot-language/src/Copilot/Language.hs
+++ b/copilot-language/src/Copilot/Language.hs
@@ -62,7 +62,6 @@ import Copilot.Language.Operators.Temporal
 import Copilot.Language.Operators.BitWise
 import Copilot.Language.Operators.Array
 import Copilot.Language.Operators.Struct
-import Copilot.Language.Reify
 import Copilot.Language.Prelude
 import Copilot.Language.Spec
 import Copilot.Language.Stream (Stream)
diff --git a/copilot-language/src/Copilot/Language/Analyze.hs b/copilot-language/src/Copilot/Language/Analyze.hs
index e7065f7b4..a39d4b2c6 100644
--- a/copilot-language/src/Copilot/Language/Analyze.hs
+++ b/copilot-language/src/Copilot/Language/Analyze.hs
@@ -116,11 +116,6 @@ analyzeProperty refStreams (Property _ p) =
   -- quantifier is.
   analyzeExpr refStreams (extractProp p)
 
-data SeenExtern = NoExtern
-                | SeenFun
-                | SeenArr
-                | SeenStruct
-
 -- | Analyze a Copilot stream and report any errors detected.
 --
 -- This function can fail with one of the exceptions in 'AnalyzeException'.
@@ -128,11 +123,11 @@ analyzeExpr :: IORef Env -> Stream a -> IO ()
 analyzeExpr refStreams s = do
   b <- mapCheck refStreams
   when b (throw TooMuchRecursion)
-  go NoExtern M.empty s
+  go M.empty s
 
   where
-  go :: SeenExtern -> Env -> Stream b -> IO ()
-  go seenExt nodes e0 = do
+  go :: Env -> Stream b -> IO ()
+  go nodes e0 = do
     dstn <- makeDynStableName e0
     assertNotVisited e0 dstn nodes
     let nodes' = M.insert dstn () nodes
@@ -141,16 +136,16 @@ analyzeExpr refStreams s = do
       Const _             -> return ()
       Drop k e1           -> analyzeDrop (fromIntegral k) e1
       Extern _ _          -> return ()
-      Local e f           -> go seenExt nodes' e >>
-                             go seenExt nodes' (f (Var "dummy"))
+      Local e f           -> go nodes' e >>
+                             go nodes' (f (Var "dummy"))
       Var _               -> return ()
-      Op1 _ e             -> go seenExt nodes' e
-      Op2 _ e1 e2         -> go seenExt nodes' e1 >>
-                             go seenExt nodes' e2
-      Op3 _ e1 e2 e3      -> go seenExt nodes' e1 >>
-                             go seenExt nodes' e2 >>
-                             go seenExt nodes' e3
-      Label _ e           -> go seenExt nodes' e
+      Op1 _ e             -> go nodes' e
+      Op2 _ e1 e2         -> go nodes' e1 >>
+                             go nodes' e2
+      Op3 _ e1 e2 e3      -> go nodes' e1 >>
+                             go nodes' e2 >>
+                             go nodes' e3
+      Label _ e           -> go nodes' e
 
 -- | Detect whether the given stream name has already been visited.
 --
@@ -265,11 +260,11 @@ analyzeExts ExternEnv { externVarEnv  = vars
   groupByPred = groupBy (\(n0,_) (n1,_) -> n0 == n1)
 
   foldCheck :: (String -> a -> a -> IO (String, a)) -> [(String, a)] -> IO ()
-  foldCheck check grp =
+  foldCheck check grp@(grpHead:_) =
     foldM_ ( \(name, c0) (_, c1) -> check name c0 c1)
-           (head grp) -- should be typesafe, since this is from groupBy
+           grpHead
            grp
-
+  foldCheck _ [] = error "Dead code executed"
 -- | Obtain all the externs in a specification.
 specExts :: IORef Env -> Spec' a -> IO ExternEnv
 specExts refStreams spec = do
diff --git a/copilot-language/src/Copilot/Language/Reify.hs b/copilot-language/src/Copilot/Language/Reify.hs
index 60bae450b..1d1298f41 100644
--- a/copilot-language/src/Copilot/Language/Reify.hs
+++ b/copilot-language/src/Copilot/Language/Reify.hs
@@ -17,7 +17,7 @@ import Copilot.Core (Typed, Id, typeOf)
 
 import Copilot.Language.Analyze (analyze)
 import Copilot.Language.Error   (impossible)
-import Copilot.Language.Spec
+import Copilot.Language.Spec hiding (prop)
 import Copilot.Language.Stream (Stream (..))
 
 import Copilot.Theorem.Prove
@@ -27,7 +27,7 @@ import Data.IORef
 import System.Mem.StableName.Dynamic
 import System.Mem.StableName.Map (Map)
 import qualified System.Mem.StableName.Map as M
-import Control.Monad (liftM, unless)
+import Control.Monad (unless)
 
 -- | Transform a Copilot Language specification into a Copilot Core
 -- specification.
@@ -200,18 +200,6 @@ mkExpr refMkId refStreams refMap = go
       w3 <- go e3
       return $ Core.Op3 op w1 w2 w3
 
-    ------------------------------------------------------
-
-  mkFunArg :: Arg -> IO Core.UExpr
-  mkFunArg (Arg e) = do
-    w <- mkExpr refMkId refStreams refMap e
-    return $ Core.UExpr typeOf w
-
-  mkStrArg :: (Core.Name, Arg) -> IO (Core.Name, Core.UExpr)
-  mkStrArg (name, Arg e) = do
-    w <- mkExpr refMkId refStreams refMap e
-    return $ (name, Core.UExpr typeOf w)
-
 -- | Transform a Copilot stream expression into a Copilot Core stream
 -- expression.
 {-# INLINE mkStream #-}
@@ -224,7 +212,9 @@ mkStream
   -> IO Id
 mkStream refMkId refStreams refMap e0 = do
   dstn <- makeDynStableName e0
-  let Append buf _ e = e0 -- avoids warning
+  (buf, e) <- case e0 of
+    Append buf _ e -> pure (buf, e)
+    o              -> fail $ "Expected Append but got " ++ show o
   mk <- haveVisited dstn
   case mk of
     Just id_ -> return id_
diff --git a/copilot-language/src/Copilot/Language/Stream.hs b/copilot-language/src/Copilot/Language/Stream.hs
index 3c2a2f838..fde822668 100644
--- a/copilot-language/src/Copilot/Language/Stream.hs
+++ b/copilot-language/src/Copilot/Language/Stream.hs
@@ -18,6 +18,7 @@ import Copilot.Core (Typed, typeOf)
 import qualified Copilot.Core as Core
 import Copilot.Language.Error
 import Copilot.Language.Prelude
+import qualified Data.Kind as DK
 import qualified Prelude as P
 
 -- | A stream in Copilot is an infinite succession of values of the same type.
@@ -27,7 +28,7 @@ import qualified Prelude as P
 -- to streams, or by combining existing streams to form new streams (e.g.,
 -- 'Op2', 'Op3').
 
-data Stream :: * -> * where
+data Stream :: DK.Type -> DK.Type where
   Append      :: Typed a
               => [a] -> Maybe (Stream Bool) -> Stream a -> Stream a
   Const       :: Typed a => a -> Stream a
diff --git a/copilot-language/tests/Test/Copilot/Language/Reify.hs b/copilot-language/tests/Test/Copilot/Language/Reify.hs
index b9d5085ba..984cb9252 100644
--- a/copilot-language/tests/Test/Copilot/Language/Reify.hs
+++ b/copilot-language/tests/Test/Copilot/Language/Reify.hs
@@ -719,7 +719,7 @@ data SemanticsP = forall t
 -- | Show function for test triplets that limits the accompanying list
 -- to a certain length.
 semanticsShowK :: Int -> SemanticsP -> String
-semanticsShowK steps (SemanticsP (expr, exprList)) =
+semanticsShowK steps (SemanticsP (_expr, exprList)) =
   show ("Cannot show stream", take steps exprList)
 
 -- | Check that the expression in the semantics pair is evaluated to the given
diff --git a/copilot-libraries/src/Copilot/Library/MTL.hs b/copilot-libraries/src/Copilot/Library/MTL.hs
index 1ea570844..70e0c2970 100644
--- a/copilot-libraries/src/Copilot/Library/MTL.hs
+++ b/copilot-libraries/src/Copilot/Library/MTL.hs
@@ -19,7 +19,6 @@ module Copilot.Library.MTL
 
 import Copilot.Language
 import qualified Prelude as P
-import Copilot.Library.Utils
 
 -- It is necessary to provide a positive number of time units
 -- dist to each function, where the distance between the times
@@ -31,7 +30,7 @@ import Copilot.Library.Utils
 -- at some time @t'@, where @(t + l) <= t' <= (t + u)@.
 eventually :: ( Typed a, Integral a ) =>
   a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
-eventually l u clk dist s = res clk s $ (u `P.div` dist) + 1
+eventually l u clk dist s' = res clk s' $ (u `P.div` dist) + 1
   where
   mins = clk + (constant l)
   maxes = clk + (constant u)
@@ -46,7 +45,7 @@ eventually l u clk dist s = res clk s $ (u `P.div` dist) + 1
 -- true at some time @t'@, where @(t - u) <= t' <= (t - l)@.
 eventuallyPrev :: ( Typed a, Integral a ) =>
   a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
-eventuallyPrev l u clk dist s = res clk s $ (u `P.div` dist) + 1
+eventuallyPrev l u clk dist s' = res clk s' $ (u `P.div` dist) + 1
   where
   mins = clk - (constant u)
   maxes = clk - (constant l)
@@ -61,7 +60,7 @@ eventuallyPrev l u clk dist s = res clk s $ (u `P.div` dist) + 1
 -- @t'@ where @(t + l) <= t' <= (t + u)@.
 always :: ( Typed a, Integral a ) =>
   a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
-always l u clk dist s = res clk s $ (u `P.div` dist) + 1
+always l u clk dist s' = res clk s' $ (u `P.div` dist) + 1
   where
   mins = clk + (constant l)
   maxes = clk + (constant u)
@@ -76,7 +75,7 @@ always l u clk dist s = res clk s $ (u `P.div` dist) + 1
 -- @t'@ where @(t - u) <= t' <= (t - l)@.
 alwaysBeen :: ( Typed a, Integral a ) =>
   a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
-alwaysBeen l u clk dist s = res clk s $ (u `P.div` dist) + 1
+alwaysBeen l u clk dist s' = res clk s' $ (u `P.div` dist) + 1
   where
   mins = clk - (constant u)
   maxes = clk - (constant l)
diff --git a/copilot-libraries/tests/Test/Extra.hs b/copilot-libraries/tests/Test/Extra.hs
index da462cb05..708b8a22c 100644
--- a/copilot-libraries/tests/Test/Extra.hs
+++ b/copilot-libraries/tests/Test/Extra.hs
@@ -45,11 +45,6 @@ import           Copilot.Interpret.Eval              (ExecTrace (interpObservers
 import           Copilot.Language                    (Spec, Stream, Typed,
                                                       observer, prop)
 import qualified Copilot.Language                    as Copilot
-import qualified Copilot.Language.Operators.Boolean  as Copilot
-import qualified Copilot.Language.Operators.Constant as Copilot
-import qualified Copilot.Language.Operators.Eq       as Copilot
-import qualified Copilot.Language.Operators.Mux      as Copilot
-import qualified Copilot.Language.Operators.Ord      as Copilot
 import           Copilot.Language.Reify              (reify)
 import           Copilot.Theorem.What4               (SatResult (..),
                                                       Solver (..), prove)
diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
index 2f6f95f07..f679ebce2 100644
--- a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
+++ b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
@@ -50,8 +50,8 @@ showType t =
     Word64 -> "Word64"
     Float  -> "Float"
     Double -> "Double"
-    Array t -> "Array " ++ showType t
-    Struct t -> "Struct"
+    Array p -> "Array " ++ showType p
+    Struct _ -> "Struct"
 
 -- * Auxiliary show instance
 
@@ -73,5 +73,5 @@ showWit t =
     Word64 -> ShowWit
     Float  -> ShowWit
     Double -> ShowWit
-    Array t -> ShowWit
-    Struct t -> ShowWit
+    Array _ -> ShowWit
+    Struct _ -> ShowWit
diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal
index b830f91a6..26be51298 100644
--- a/copilot-theorem/copilot-theorem.cabal
+++ b/copilot-theorem/copilot-theorem.cabal
@@ -40,10 +40,7 @@ library
   hs-source-dirs          : src
 
   ghc-options             : -Wall
-                            -fno-warn-name-shadowing
-                            -fno-warn-unused-binds
-                            -fno-warn-missing-signatures
-                            -fcontext-stack=100
+                            -freduction-depth=100
 
   build-depends           : base                  >= 4.9 && < 5
                           , bimap                 (>= 0.3 && < 0.4) || (>= 0.5 && < 0.6)
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/IL/PrettyPrint.hs
index 196873060..f2ea70337 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/PrettyPrint.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/PrettyPrint.hs
@@ -10,7 +10,7 @@ import Copilot.Theorem.IL.Spec
 import Text.PrettyPrint.HughesPJ
 import qualified Data.Map as Map
 
-import Prelude hiding ((<>))
+import Prelude hiding (id, (<>))
 
 -- | Pretty print an IL specification.
 prettyPrint :: IL -> String
@@ -20,7 +20,9 @@ prettyPrint = render . ppSpec
 printConstraint :: Expr -> String
 printConstraint = render . ppExpr
 
+indent :: Doc -> Doc
 indent = nest 4
+emptyLine :: Doc
 emptyLine = text ""
 
 ppSpec :: IL -> Doc
@@ -37,20 +39,6 @@ ppProp :: PropId -> ([Expr], Expr) -> Doc
 ppProp id (as, c) = (foldr (($$) . ppExpr) empty as)
   $$ quotes (text id) <+> colon <+> ppExpr c
 
-ppSeqDescr :: SeqDescr -> Doc
-ppSeqDescr (SeqDescr id ty) = text id <+> colon <+> ppType ty
-
-ppVarDescr :: VarDescr -> Doc
-ppVarDescr (VarDescr id ret args) =
-  text id
-  <+> colon
-  <+> (hsep . punctuate (space <> text "->" <> space) $ map ppType args)
-  <+> text "->"
-  <+> ppType ret
-
-ppType :: Type -> Doc
-ppType = text . show
-
 ppExpr :: Expr -> Doc
 ppExpr (ConstB v) = text . show $ v
 ppExpr (ConstR v) = text . show $ v
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Spec.hs b/copilot-theorem/src/Copilot/Theorem/IL/Spec.hs
index 62ed692bd..84abf0999 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Spec.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Spec.hs
@@ -185,7 +185,7 @@ evalAt _ e@(ConstI _ _) = e
 evalAt i (Op1 t op e) = Op1 t op (evalAt i e)
 evalAt i (Op2 t op e1 e2) = Op2 t op (evalAt i e1) (evalAt i e2)
 evalAt i (Ite t c e1 e2) = Ite t (evalAt i c) (evalAt i e1) (evalAt i e2)
-evalAt i (FunApp t name args) = FunApp t name $ map (\e -> evalAt i e) args
+evalAt i (FunApp t name args') = FunApp t name $ map (\e -> evalAt i e) args'
 
 evalAt _ e@(SVal _ _ (Fixed _)) = e
 evalAt (Fixed n) (SVal t s (Var d)) = SVal t s (Fixed $ n + d)
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs b/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
index 4bdaa47f3..09ebaf572 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
@@ -4,7 +4,9 @@
 -- | Simplify IL expressions by partly evaluating operations on booleans.
 module Copilot.Theorem.IL.Transform ( bsimpl ) where
 
-import Copilot.Theorem.IL.Spec
+import           Copilot.Theorem.IL.Spec (Expr (ConstB, FunApp, Ite, Op1, Op2),
+                                          Op1 (Not), Op2 (And, Eq, Or),
+                                          Type (Bool))
 
 -- | Simplify IL expressions by partly evaluating operations on booleans,
 -- eliminating some boolean literals.
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
index c1a6606ba..c11f6db31 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE NamedFieldPuns      #-}
@@ -14,7 +15,9 @@ import qualified Copilot.Core as C
 
 import qualified Data.Map.Strict as Map
 
+#if MIN_VERSION_base(4,19,0)
 import Control.Monad       (forM, liftM2, when)
+#endif
 import Control.Monad.State
 
 import Data.Char
@@ -25,6 +28,7 @@ import Text.Printf
 import GHC.Float (float2Double)
 
 import Data.Typeable (Typeable)
+import Prelude hiding (id)
 
 -- 'nc' stands for naming convention.
 ncSeq :: C.Id -> SeqId
@@ -37,9 +41,6 @@ ncLocal s = "l" ++ dropWhile (not . isNumber) s
 ncExternVar :: C.Name -> SeqId
 ncExternVar n = "ext_" ++ n
 
-ncUnhandledOp :: String -> String
-ncUnhandledOp = id
-
 ncMux :: Integer -> SeqId
 ncMux n = "mux" ++ show n
 
@@ -81,7 +82,7 @@ translate' b (C.Spec {C.specStreams, C.specProperties}) = runTrans b $ do
     }
 
 bound :: Expr -> C.Type a -> Trans ()
-bound s t = case t of
+bound s sType = case sType of
   C.Int8    -> bound' C.Int8
   C.Int16   -> bound' C.Int16
   C.Int32   -> bound' C.Int32
@@ -150,14 +151,14 @@ expr (C.Op1 (C.Sign ta) e) = case ta of
   _        -> expr $ C.Const ta 1
   where
     trSign :: (Typeable a, Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr
-    trSign ta e =
-      expr (C.Op3 (C.Mux ta)
-        (C.Op2 (C.Lt ta) e (C.Const ta 0))
-        (C.Const ta (-1))
-        (C.Op3 (C.Mux ta)
-          (C.Op2 (C.Gt ta) e (C.Const ta 0))
-          (C.Const ta 1)
-          (C.Const ta 0)))
+    trSign tb e' =
+      expr (C.Op3 (C.Mux tb)
+        (C.Op2 (C.Lt tb) e' (C.Const tb 0))
+        (C.Const tb (-1))
+        (C.Op3 (C.Mux tb)
+          (C.Op2 (C.Gt tb) e' (C.Const tb 0))
+          (C.Const tb 1)
+          (C.Const tb 0)))
 expr (C.Op1 (C.Sqrt _) e) = do
   e' <- expr e
   return $ Op2 Real Pow e' (ConstR 0.5)
@@ -187,29 +188,31 @@ expr (C.Op3 (C.Mux t) cond e1 e2) = do
   e1'   <- expr e1
   e2'   <- expr e2
   newMux cond' (trType t) e1' e2'
+expr (C.Op3 (C.UpdateArray _) _ _ _) = error "There is bug in the type checker"
 
 trConst :: C.Type a -> a -> Expr
 trConst t v = case t of
   C.Bool   -> ConstB v
   C.Float  -> negifyR (float2Double v)
   C.Double -> negifyR v
-  t@C.Int8   -> negifyI v (trType t)
-  t@C.Int16  -> negifyI v (trType t)
-  t@C.Int32  -> negifyI v (trType t)
-  t@C.Int64  -> negifyI v (trType t)
-  t@C.Word8  -> negifyI v (trType t)
-  t@C.Word16 -> negifyI v (trType t)
-  t@C.Word32 -> negifyI v (trType t)
-  t@C.Word64 -> negifyI v (trType t)
+  t'@C.Int8   -> negifyI v (trType t')
+  t'@C.Int16  -> negifyI v (trType t')
+  t'@C.Int32  -> negifyI v (trType t')
+  t'@C.Int64  -> negifyI v (trType t')
+  t'@C.Word8  -> negifyI v (trType t')
+  t'@C.Word16 -> negifyI v (trType t')
+  t'@C.Word32 -> negifyI v (trType t')
+  t'@C.Word64 -> negifyI v (trType t')
+  t'          -> error $ "There is bug in the type checker" ++ show t'
   where
     negifyR :: Double -> Expr
-    negifyR v
-      | v >= 0    = ConstR v
-      | otherwise = Op1 Real Neg $ ConstR $ negate $ v
+    negifyR v'
+      | v' >= 0   = ConstR v'
+      | otherwise = Op1 Real Neg $ ConstR $ negate v'
     negifyI :: Integral a => a -> Type -> Expr
-    negifyI v t
-      | v >= 0    = ConstI t $ toInteger v
-      | otherwise = Op1 t Neg $ ConstI t $ negate $ toInteger v
+    negifyI v' t'
+      | v' >= 0   = ConstI t' $ toInteger v'
+      | otherwise = Op1 t' Neg $ ConstI t' $ negate $ toInteger v'
 
 trOp1 :: C.Op1 a b -> (Op1, Type)
 trOp1 = \case
@@ -282,6 +285,7 @@ trType = \case
   C.Word64 -> BV64
   C.Float  -> Real
   C.Double -> Real
+  _        -> error "THere is a bug in the type checker"
 
 -- | Translation state.
 data TransST = TransST
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs
index f80b8170b..ab647ab8b 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs
@@ -12,6 +12,7 @@ import qualified Copilot.Core as C
 
 import qualified Copilot.Theorem.Misc.Error as Err
 
+simpleName :: String -> QName
 simpleName s = QName s Nothing Nothing
 
 -- | Parse output of Kind2.
@@ -43,9 +44,6 @@ parseOutput propId propQuantifier xml = fromJust $ do
     s             -> err $ "Unrecognized status : " ++ s
 
   where
-
-    searchForRuntimeError = undefined
-
     findPropTag root =
       let rightElement elt =
             qName (elName elt) == "Property"
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
index 6851d46fa..e57637475 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
@@ -13,6 +13,7 @@ import Data.List (intercalate)
 type SSExpr = SExpr String
 
 -- | Reserved keyword prime.
+kwPrime :: String
 kwPrime = "prime"
 
 -- | Pretty print a Kind2 file.
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
index 4bb52322e..3553847ed 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
@@ -1,4 +1,9 @@
+{-# LANGUAGE CPP  #-}
+#if MIN_VERSION_base(4,19,0)
 {-# LANGUAGE Trustworthy #-}
+#else
+{-# LANGUAGE Safe #-}
+#endif
 
 -- | A prover backend based on Kind2.
 module Copilot.Theorem.Kind2.Prover
@@ -35,9 +40,7 @@ data Options = Options
 instance Default Options where
   def = Options { bmcMax = 0 }
 
-data ProverST = ProverST
-  { options  :: Options
-  , transSys :: TS.TransSys }
+data ProverST = ProverST Options TS.TransSys
 
 -- | A prover backend based on Kind2.
 --
@@ -49,11 +52,15 @@ kind2Prover opts = Prover
   , askProver    = askKind2
   , closeProver  = const $ return () }
 
-kind2Prog        = "kind2"
+kind2Prog :: String
+kind2Prog = "kind2"
+
+kind2BaseOptions :: [String]
 kind2BaseOptions = ["--input-format", "native", "-xml"]
 
 askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output
-askKind2 (ProverST opts spec) assumptions toCheck = do
+askKind2 _p _assumptions [] = fail "toCheck is empty"
+askKind2 (ProverST opts spec) assumptions toCheck@(toCheckHead:_) = do
 
   let kind2Input = prettyPrint . toKind2 Inlined assumptions toCheck $ spec
 
@@ -70,7 +77,7 @@ askKind2 (ProverST opts spec) assumptions toCheck = do
 
   removeFile tempName
 
-  let propId         = head toCheck
+  let propId         = toCheckHead
       propQuantifier = case Map.lookup propId (TS.specProps spec) of
                          Just (_, quantifier) ->
                            quantifier
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
index 123f6ed64..7fdaf3354 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
@@ -24,6 +24,7 @@ import Data.Map (Map, (!))
 
 import qualified Data.Map as Map
 import qualified Data.Bimap as Bimap
+import Prelude hiding (pred)
 
 -- The following properties MUST hold for the given transition system :
 -- * Nodes are sorted by topological order
@@ -97,8 +98,7 @@ addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) =
       in pred { K.predInit = init', K.predTrans = trans' }
 
     vars =
-      let bindings   = nodeImportedVars (specTopNode spec)
-          toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec
+      let toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec
           toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v
       in map (varName . toTopVar . toExtVar) assumptions
 
diff --git a/copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs b/copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs
index cb7d35ff3..561e5335b 100644
--- a/copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs
@@ -7,30 +7,34 @@ module Copilot.Theorem.Misc.SExpr where
 
 import Text.PrettyPrint.HughesPJ as PP hiding (char, Str)
 
-import Control.Monad
-
 -- | A structured expression is either an atom, or a sequence of expressions,
 -- where the first in the sequence denotes the tag or label of the tree.
 data SExpr a = Atom a
              | List [SExpr a]
 
 -- | Empty string expression.
+blank :: SExpr String
 blank = Atom ""
 
 -- | Atomic expression constructor.
+atom :: a -> SExpr a
 atom = Atom                 -- s
 
 -- | Empty expression (empty list).
+unit :: SExpr a
 unit = List []              -- ()
 
 -- | Single expression.
+singleton :: a -> SExpr a
 singleton a  = List [Atom a]        -- (s)
 
 -- | Sequence of expressions.
+list :: [SExpr a] -> SExpr a
 list = List                 -- (ss)
 
 -- | Sequence of expressions with a root or main note, and a series of
 -- additional expressions or arguments.
+node :: a -> [SExpr a] -> SExpr a
 node a l = List (Atom a : l)    -- (s ss)
 
 -- A straightforward string representation for 'SExpr's of Strings that
@@ -44,6 +48,7 @@ instance Show (SExpr String) where
 -- More advanced printing with some basic indentation
 
 -- | Indent by a given number.
+indent :: Doc -> Doc
 indent = nest 1
 
 -- | Pretty print a structured expression as a String.
diff --git a/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs b/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
index 10b4666a4..f61801788 100644
--- a/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
@@ -1,4 +1,9 @@
+{-# LANGUAGE CPP #-}
+#if MIN_VERSION_base(4,19,0)
 {-# LANGUAGE Trustworthy #-}
+#else
+{-# LANGUAGE Safe #-}
+#endif
 
 -- | Utility / auxiliary functions.
 module Copilot.Theorem.Misc.Utils
@@ -7,9 +12,7 @@ module Copilot.Theorem.Misc.Utils
  ) where
 
 import Data.Function (on)
-import Data.List (groupBy, sortBy, group, sort)
-
-import Control.Applicative ((<$>))
+import qualified Data.List.NonEmpty as NE
 import Control.Monad
 
 import qualified Data.Set as Set
@@ -34,11 +37,11 @@ nubEq = (==) `on` Set.fromList
 -- stronger constraint on the type (i.e., 'Ord', as opposed of
 -- 'Data.List.nub''s 'Eq' constraint).
 nub' :: Ord a => [a] -> [a]
-nub' = map head . group . sort
+nub' = maybe [] (fmap NE.head . NE.group . NE.sort) . NE.nonEmpty
 
 -- | Variant of 'nub'' parameterized by the comparison function.
 nubBy' :: (a -> a -> Ordering) -> [a] -> [a]
-nubBy' f = map head . groupBy (\x y -> f x y == EQ) . sortBy f
+nubBy' f = maybe [] (fmap NE.head . NE.groupBy (\x y -> f x y == EQ) . NE.sortBy f) . NE.nonEmpty
 
 -- | Create a temporary file and open it for writing.
 openTempFile :: String  -- ^ Directory where the file should be created.
diff --git a/copilot-theorem/src/Copilot/Theorem/Prove.hs b/copilot-theorem/src/Copilot/Theorem/Prove.hs
index ed9a7d78d..60a1f908c 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prove.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prove.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                       #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE NamedFieldPuns            #-}
@@ -21,8 +22,11 @@ module Copilot.Theorem.Prove
 import qualified Copilot.Core as Core
 
 import Data.List (intercalate)
-import Control.Applicative (liftA2)
+#if MIN_VERSION_base(4,19,0)
 import Control.Monad        (ap, liftM)
+#else
+import Control.Applicative  (liftA2)
+#endif
 import Control.Monad.Writer
 
 -- | Output produced by a prover, containing the 'Status' of the proof and
@@ -79,12 +83,11 @@ instance Functor (ProofScheme a) where
   fmap = liftM
 
 instance Applicative (ProofScheme a) where
-  pure = return
+  pure a = Proof (pure a)
   (<*>) = ap
 
 instance Monad (ProofScheme a) where
   (Proof p) >>= f = Proof $ p >>= (\a -> case f a of Proof p' -> p')
-  return a = Proof (return a)
 
 -- | Prover actions.
 data Action where
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs b/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs
index e5661a748..80edb607a 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE NamedFieldPuns    #-}
 {-# LANGUAGE RankNTypes        #-}
-{-# LANGUAGE Trustworthy       #-}
+{-# LANGUAGE Safe              #-}
 
 -- | Connections to various SMT solvers and theorem provers.
 module Copilot.Theorem.Prover.SMT
@@ -49,7 +49,7 @@ import Data.Default (Default(..))
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Copilot.Theorem.Misc.Utils
-
+import Prelude hiding (seq, id)
 import System.IO (hClose)
 
 -- * Tactics
@@ -358,9 +358,9 @@ valid msg = return $ Output P.Valid [msg]
 
 kInduction' :: SmtFormat b => Word32 -> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
 kInduction' startK maxK s as ps = (fromMaybe (Output P.Unknown ["proof by k-induction failed"]) . fst)
-  <$> runPS (msum (map induction [(toInteger startK) .. (toInteger maxK)]) <* stopSolvers) s
+  <$> runPS (msum (map induction' [(toInteger startK) .. (toInteger maxK)]) <* stopSolvers) s
   where
-    induction k = do
+    induction' k = do
       (modelInit, modelRec, toCheck, inductive) <- getModels as ps
 
       let base    = [evalAt (Fixed i) m | m <- modelRec, i <- [0 .. k]]
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs b/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs
index 0f2b1e0c6..be2c5ca64 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs
@@ -8,9 +8,10 @@ module Copilot.Theorem.Prover.SMTLib (SmtLib, interpret) where
 
 import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))
 
-import Copilot.Theorem.IL
+import Copilot.Theorem.IL.Spec hiding (args)
 import Copilot.Theorem.Misc.SExpr
 
+
 import Text.Printf
 
 -- | Type used to represent SMT-lib commands.
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs b/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
index e179409e8..f35f9654c 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
@@ -7,7 +7,7 @@
 module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where
 
 import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))
-import Copilot.Theorem.IL
+import Copilot.Theorem.IL hiding (args)
 
 import Data.List
 
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Cast.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Cast.hs
index 8d7cc7c52..880357edb 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Cast.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Cast.hs
@@ -39,6 +39,7 @@ castedType t = case t of
   Word64  -> K.U K.Integer
   Float   -> K.U K.Real
   Double  -> K.U K.Real
+  o       -> error $ "There is a bug in type checker " ++ show o
 
 -- | Cast a dynamic value to a given type.
 cast :: K.Type t -> Dyn -> t
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
index dd95d45db..87509270d 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
@@ -168,15 +168,16 @@ handleOp1 resT (op, e) handleExpr notHandledF mkOp = case op of
 
   -- Casting operator.
   C.Cast _ tb -> castTo tb
+  _o          -> error "Not handled"
 
   where
     boolOp :: Op1 Bool -> m (expr Bool) -> m (expr resT)
-    boolOp op e = case resT of
-      Bool -> (mkOp resT op) <$> e
+    boolOp op' e' = case resT of
+      Bool -> (mkOp resT op') <$> e'
       _    -> Err.impossible typeErrMsg
 
     numOp :: Op1 resT -> m (expr resT)
-    numOp op = (mkOp resT op) <$> (handleExpr resT e)
+    numOp op' = (mkOp resT op') <$> (handleExpr resT e)
 
     -- Casting from Integer (Only possible solution)
     castTo :: C.Type ctb -> m (expr resT)
@@ -261,19 +262,20 @@ handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of
   -- be casted to 'Integer', like 'ta'
   C.BwShiftL ta _tb   -> notHandled ta "bwshiftl"
   C.BwShiftR ta _tb   -> notHandled ta "bwshiftr"
+  _o                  -> error "Not handled"
 
   where
 
     boolOp :: Op2 a Bool -> expr a -> expr a -> expr resT
-    boolOp op e1' e2' = case resT of
-      Bool -> mkOp resT op e1' e2'
+    boolOp op' e1' e2' = case resT of
+      Bool -> mkOp resT op' e1' e2'
       _    -> Err.impossible typeErrMsg
 
     boolConnector :: Op2 Bool Bool -> m (expr resT)
-    boolConnector op = do
+    boolConnector op' = do
      e1' <- handleExpr Bool e1
      e2' <- handleExpr Bool e2
-     return $ boolOp op e1' e2'
+     return $ boolOp op' e1' e2'
 
     eqOp :: C.Type cta -> m (expr resT)
     eqOp ta = casting ta $ \ta' -> do
@@ -289,31 +291,31 @@ handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of
       _ -> Err.impossible typeErrMsg
 
     numOp :: (forall num . (Num num) => Op2 num num) -> m (expr resT)
-    numOp op = case resT of
+    numOp op' = case resT of
       Integer -> do
         e1' <- handleExpr Integer e1
         e2' <- handleExpr Integer e2
-        return $ mkOp resT op e1' e2'
+        return $ mkOp resT op' e1' e2'
 
       Real -> do
         e1' <- handleExpr Real e1
         e2' <- handleExpr Real e2
-        return $ mkOp resT op e1' e2'
+        return $ mkOp resT op' e1' e2'
 
       _ -> Err.impossible typeErrMsg
 
     numComp ::
       C.Type cta ->
       (forall num . (Num num) => Op2 num Bool) -> m (expr resT)
-    numComp ta op = casting ta $ \case
+    numComp ta op' = casting ta $ \case
       Integer -> do
         e1' <- handleExpr Integer e1
         e2' <- handleExpr Integer e2
-        return $ boolOp op e1' e2'
+        return $ boolOp op' e1' e2'
       Real -> do
         e1' <- handleExpr Real e1
         e2' <- handleExpr Real e2
-        return $ boolOp op e1' e2'
+        return $ boolOp op' e1' e2'
       _       -> Err.impossible typeErrMsg
 
     notHandled :: forall a . C.Type a -> String -> m (expr resT)
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
index 3debe552c..487b4ac3b 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
@@ -14,7 +14,10 @@ import qualified Data.Bimap as Bimap
 
 import Prelude hiding ((<>))
 
-indent     = nest 4
+indent :: Doc -> Doc
+indent = nest 4
+
+emptyLine :: Doc
 emptyLine  = text ""
 
 -- | Pretty print a TransSys specification as a Kind2/Lustre specification.
@@ -30,6 +33,7 @@ pSpec spec = items $$ props
         empty
         (Map.map fst (specProps spec))
 
+pProp :: String -> ExtVar -> Doc
 pProp pId extvar = quotes (text pId) <+> text "is" <+> pExtVar extvar
 
 pType :: Type t -> Doc
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs
index 76c7ba099..6348008f7 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs
@@ -22,6 +22,7 @@ import Data.Set (Set, member)
 import qualified Data.Map  as Map
 import qualified Data.Set  as Set
 import qualified Data.List as List
+import           GHC.Stack (HasCallStack)
 
 -- | A monad capable of keeping track of variable renames and of providing
 -- fresh names for variables.
@@ -43,13 +44,14 @@ addReservedName v = modify $ \st ->
 -- use one of the names in the list as a basis for new names.
 --
 -- PRE: the given list cannot be empty.
-getFreshName :: [Var] -> Renaming Var
-getFreshName vs = do
+getFreshName :: HasCallStack => [Var] -> Renaming Var
+getFreshName [] = error "Empty list given"
+getFreshName vs@(vsHead:_) = do
   usedNames <- _reservedNames <$> get
   let varAppend (Var s) = Var $ s ++ "_"
-      applicants = vs ++ List.iterate varAppend (head vs)
+      applicants = vs ++ List.iterate varAppend vsHead
       v = case dropWhile (`member` usedNames) applicants of
-            v:_ -> v
+            v':_ -> v'
             [] -> error "No more names available"
   addReservedName v
   return v
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
index b68181ae0..7bcc90dff 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                       #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE RankNTypes                #-}
@@ -24,6 +25,11 @@ module Copilot.Theorem.TransSys.Spec
   , specDependenciesGraph
   , specTopNode ) where
 
+#if MIN_VERSION_base(4,19,0)
+#else
+import Control.Applicative  (liftA2)
+#endif
+
 import qualified Copilot.Core as C
 
 import Copilot.Theorem.TransSys.Type
@@ -32,11 +38,9 @@ import Copilot.Theorem.TransSys.Invariants
 
 import Copilot.Theorem.Misc.Utils
 
-import Control.Applicative (liftA2)
 import Control.Monad (foldM, guard)
 
 import Data.Maybe
-import Data.Monoid ((<>))
 import Data.Map (Map)
 import Data.Set (Set, isSubsetOf, member)
 import Data.Bimap (Bimap)
@@ -104,6 +108,7 @@ data Expr t where
   VarE  :: Type t -> Var -> Expr t
 
 -- | Constructor for variables identifiers in the global namespace.
+mkExtVar :: NodeId -> String -> ExtVar
 mkExtVar node name = ExtVar node (Var name)
 
 foldExpr :: (Monoid m) => (forall t . Expr t -> m) -> Expr a -> m
@@ -115,9 +120,6 @@ foldExpr f expr = f expr <> fargs
       (Op2 _ _ e1 e2)  -> foldExpr f e1 <> foldExpr f e2
       _                -> mempty
 
-foldUExpr :: (Monoid m) => (forall t . Expr t -> m) -> U Expr -> m
-foldUExpr f (U e) = foldExpr f e
-
 -- | Apply an arbitrary transformation to the leafs of an expression.
 transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t
 transformExpr f = tre
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
index e59058496..fc4765281 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
@@ -9,7 +9,7 @@ module Copilot.Theorem.TransSys.Transform
   , complete
   ) where
 
-import Copilot.Theorem.TransSys.Spec
+import Copilot.Theorem.TransSys.Spec hiding (prop)
 import Copilot.Theorem.TransSys.Renaming
 
 import Copilot.Theorem.Misc.Utils
@@ -32,7 +32,8 @@ import qualified Data.Bimap as Bimap
 prefix :: String -> Var -> Var
 prefix s1 (Var s2) = Var $ s1 ++ "." ++ s2
 
-ncNodeIdSep = "-"
+ncNodeIdSep :: Char
+ncNodeIdSep = '-'
 
 -- | Merge all the given nodes, replacing all references to the given node Ids
 -- with a reference to a fresh node id (unless the nodes given as argument
@@ -53,7 +54,7 @@ mergeNodes toMergeIds spec =
     -- its name is kept
     newNodeId
       | specTopNodeId spec `elem` toMergeIds = specTopNodeId spec
-      | otherwise = intercalate ncNodeIdSep (sort toMergeIds)
+      | otherwise = intercalate [ncNodeIdSep] (sort toMergeIds)
 
     newNode = Node
       { nodeId = newNodeId
@@ -64,10 +65,10 @@ mergeNodes toMergeIds spec =
 
     -- Computing the dependencies of the new node
     dependencies = nub'
-      [ id |
+      [ id' |
         n <- toMerge
-      , id <- nodeDependencies n
-      , id `notElem` toMergeIds ]
+      , id' <- nodeDependencies n
+      , id' `notElem` toMergeIds ]
 
     -- All the work of renaming is done in the 'Misc.Renaming' monad. Some code
     -- complexity has been added so the variable names remains as clear as
@@ -208,8 +209,11 @@ removeCycles spec =
      let depGraph = map (\n -> (nrep n, nodeId n, nodeDependencies n)) ns
      in Graph.stronglyConnComp depGraph
 
+    acycN (Graph.AcyclicSCC n) = n
+    acycN Graph.CyclicSCC {}   = error "Cyclic graph is not handled"
+
     topoSort s = s { specNodes =
-      map (\(Graph.AcyclicSCC n) -> n) $ buildScc id (specNodes s) }
+      map acycN $ buildScc id (specNodes s) }
 
 -- | Completes each node of a specification with imported variables such that
 -- each node contains a copy of all its dependencies.
@@ -231,11 +235,11 @@ complete spec =
       . completeTopNodeDeps
       $ spec
 
-    completeTopNodeDeps spec = spec { specNodes = map aux nodes }
+    completeTopNodeDeps spec' = spec' { specNodes = map aux nodes }
       where
-        nodes = specNodes spec
+        nodes = specNodes spec'
         aux n
-          | nodeId n == specTopNodeId spec =
+          | nodeId n == specTopNodeId spec' =
               n { nodeDependencies = map nodeId nodes \\ [nodeId n] }
           | otherwise = n
 
@@ -246,7 +250,7 @@ complete spec =
                            , nodeImportedVars = importedVars' }) : ns
 
       where
-        nsMap = Map.fromList [(nodeId n, n) | n <- ns]
+        nsMap = Map.fromList [(nodeId n', n') | n' <- ns]
         dependencies' =
           let newDeps = do
                 dId <- nodeDependencies n
@@ -268,7 +272,7 @@ complete spec =
                 -- which come from merged nodes as they are already
                 -- decorated
                 let preferedName
-                     | head ncNodeIdSep `elem` n' = v
+                     | ncNodeIdSep `elem` n' = v
                      | otherwise = n' `prefix` v
                 alias <- getFreshName [preferedName, n' `prefix` v]
                 return $ Bimap.tryInsert alias ev acc
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
index 2659fa6cb..70aa6ccbe 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                 #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE NamedFieldPuns      #-}
@@ -43,16 +44,19 @@
 -- process.
 module Copilot.Theorem.TransSys.Translate ( translate ) where
 
-import Copilot.Theorem.TransSys.Spec
+import Copilot.Theorem.TransSys.Spec hiding (prop)
 import Copilot.Theorem.TransSys.Cast
 import Copilot.Theorem.Misc.Utils
 
-import Control.Monad            (liftM, liftM2, unless)
+#if MIN_VERSION_base(4,19,0)
+import Control.Monad (liftM, liftM2, unless)
+#endif
+
 import Control.Monad.State.Lazy
 
 import Data.Char (isNumber)
 import Data.Function (on)
-
+import Data.Functor.Identity (Identity)
 import Data.Map (Map)
 import Data.Bimap (Bimap)
 
@@ -63,14 +67,25 @@ import qualified Data.Bimap   as Bimap
 -- Naming conventions
 -- These are important in order to avoid name conflicts
 
-ncSep         = "."
-ncMain        = "out"
-ncNode i      = "s" ++ show i
-ncPropNode s  = "prop-" ++ s
-ncTopNode     = "top"
-ncAnonInput   = "in"
-ncLocal s     = "l" ++ dropWhile (not . isNumber) s
+ncSep :: String
+ncSep = "."
+
+ncMain :: String
+ncMain = "out"
+
+ncNode :: Show a => a -> [Char]
+ncNode i = "s" ++ show i
 
+ncPropNode :: [Char] -> [Char]
+ncPropNode s = "prop-" ++ s
+
+ncTopNode :: String
+ncTopNode = "top"
+
+ncLocal :: [Char] -> [Char]
+ncLocal s = "l" ++ dropWhile (not . isNumber) s
+
+ncExternVarNode :: [Char] -> [Char]
 ncExternVarNode name = "ext-" ++ name
 
 ncImported :: NodeId -> String -> String
@@ -121,6 +136,7 @@ mkTopNode topNodeId dependencies cprops =
       [ (Var cp, mkExtVar (ncPropNode cp) ncMain)
       | cp <- C.propertyName <$> cprops ]
 
+mkExtVarNode :: (NodeId, U Type) -> Node
 mkExtVarNode (name, U t) =
   Node { nodeId = name
        , nodeDependencies = []
@@ -175,7 +191,6 @@ stream (C.Stream { C.streamId
                  $ from (i + 1) bs
           in from 0 buf
         nodeLocalVars = Map.union nodeAuxVars outputLocals
-        nodeOutputs = map outvar [0 .. length buf - 1]
 
     return Node
       { nodeId, nodeDependencies, nodeLocalVars
@@ -185,8 +200,8 @@ expr :: Type t -> C.Expr t' -> Trans (Expr t)
 
 expr t (C.Const _ v) = return $ Const t (cast t $ toDyn v)
 
-expr t (C.Drop _ (fromIntegral -> k :: Int) id) = do
-  let node = ncNode id
+expr t (C.Drop _ (fromIntegral -> k :: Int) idNode) = do
+  let node = ncNode idNode
   selfRef <- (== node) <$> curNode
   let varName = ncMain `ncTimeAnnot` k
   let var = Var $ if selfRef then varName else ncImported node varName
@@ -197,12 +212,12 @@ expr t (C.Drop _ (fromIntegral -> k :: Int) id) = do
 
 expr t (C.Label _ _ e) = expr t e
 
-expr t (C.Local tl _tr id l e) = casting tl $ \tl' -> do
+expr t (C.Local tl _tr idNode l e) = casting tl $ \tl' -> do
   l' <- expr tl' l
-  newLocal (Var $ ncLocal id) $ VarDescr tl' $ Expr l'
+  newLocal (Var $ ncLocal idNode) $ VarDescr tl' $ Expr l'
   expr t e
 
-expr t (C.Var _t' id) = return $ VarE t (Var $ ncLocal id)
+expr t (C.Var _t' idNode) = return $ VarE t (Var $ ncLocal idNode)
 
 expr t (C.Op3 (C.Mux _) cond e1 e2) = do
   cond' <- expr Bool cond
@@ -230,6 +245,8 @@ expr t (C.Op2 op e1 e2) = handleOp2
     notHandled (UnhandledOp2 _opName _ta _tb _tc) =
       newUnconstrainedVar t
 
+expr t C.Op3 {} = error $ "Not handled " ++ show t
+
 newUnconstrainedVar :: Type t -> Trans (Expr t)
 newUnconstrainedVar t = do
   newNode <- getFreshNodeName
@@ -254,8 +271,8 @@ runExprTrans ::
   Type t -> NodeId -> C.Expr a ->
   Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [NodeId])
 
-runExprTrans t curNode e = do
-  modify $ \st -> st { _curNode = curNode }
+runExprTrans t curNode' e = do
+  modify $ \st -> st { _curNode = curNode' }
   modify $ \st -> st { _nextUid = 0 }
   e' <- expr t e
   (lvs, ivs, dps) <- popLocalInfos
@@ -271,6 +288,7 @@ data TransSt = TransSt
 
 type Trans a = State TransSt a
 
+newDep :: MonadState TransSt m => NodeId -> m ()
 newDep d =  modify $ \s -> s { _dependencies = d : _dependencies s }
 
 popLocalInfos :: State TransSt (Map Var VarDescr, Bimap Var ExtVar, [NodeId])
@@ -293,12 +311,16 @@ getUid = do
 getFreshNodeName :: Trans NodeId
 getFreshNodeName = liftM (("_" ++) . show) getUid
 
+newImportedVar :: MonadState TransSt m => Var -> ExtVar -> m ()
 newImportedVar l g = modify $
   \s -> s { _importedVars = Bimap.insert l g (_importedVars s) }
 
+newLocal :: MonadState TransSt m => Var -> VarDescr -> m ()
 newLocal l d  =  modify $ \s -> s { _lvars = Map.insert l d $ _lvars s }
 
+curNode :: StateT TransSt Data.Functor.Identity.Identity NodeId
 curNode = _curNode <$> get
 
-newExtVarNode id t =
-  modify $ \st -> st { _extVarsNodes = (id, t) : _extVarsNodes st }
+newExtVarNode :: MonadState TransSt m => NodeId -> U Type -> m ()
+newExtVarNode idNode t =
+  modify $ \st -> st { _extVarsNodes = (idNode, t) : _extVarsNodes st }
diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs
index 51ed6e8ff..0eca06577 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4.hs
@@ -67,7 +67,7 @@ import qualified What4.Solver.DReal             as WS
 
 import Control.Exception (Exception, throw)
 import Control.Monad (forM)
-import Control.Monad.State
+import Control.Monad.State (MonadIO (liftIO), gets, get)
 import qualified Data.BitVector.Sized as BV
 import Data.Foldable (foldrM)
 import Data.List (genericLength)
@@ -307,10 +307,10 @@ proveWithCounterExample :: Solver
                         -- ^ Spec
                         -> IO [(CE.Name, SatResultCex)]
 proveWithCounterExample solver spec =
-  proveInternal solver spec $ \baseCases indStep st satRes ->
+  proveInternal solver spec $ \baseCases' indStep st satRes ->
     case satRes of
       WS.Sat ge -> do
-        gBaseCases <- traverse (WG.groundEval ge) baseCases
+        gBaseCases <- traverse (WG.groundEval ge) baseCases'
         gIndStep <- WG.groundEval ge indStep
         gExternValues <- traverse (valFromExpr ge) (externVars st)
         gStreamValues <- traverse (valFromExpr ge) (streamValues st)
@@ -634,9 +634,6 @@ computeAssumptions sym properties spec =
       [ CS.extractProp (CS.propertyProp p)
       | p <- CS.specProperties spec
       , elem (CS.propertyName p) properties
-      , let prop = case CS.propertyProp p of
-                     CS.Forall pr -> pr
-                     CS.Exists {} -> throw UnexpectedExistentialProposition
       ]
 
     -- Compute all of the what4 predicates corresponding to each user-provided
diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
index cef4829ee..a36d0d26d 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
@@ -66,6 +66,7 @@ import           GHC.TypeLits                   (KnownSymbol)
 import           GHC.TypeNats                   (KnownNat, type (<=), type (+))
 import qualified Panic                          as Panic
 
+import           Prelude                        hiding (id, pred, recip)
 import qualified What4.BaseTypes                as WT
 import qualified What4.Interface                as WI
 import qualified What4.InterpretedFloatingPoint as WFP
@@ -366,17 +367,18 @@ translateConstExpr sym tp a = case tp of
   CT.Word64 -> XWord64 <$> WI.bvLit sym knownNat (BV.word64 a)
   CT.Float -> XFloat <$> WFP.iFloatLitSingle sym a
   CT.Double -> XDouble <$> WFP.iFloatLitDouble sym a
-  CT.Array tp -> do
-    elts <- traverse (translateConstExpr sym tp) (CT.arrayElems a)
+  CT.Array tp' -> do
+    elts <- traverse (translateConstExpr sym tp') (CT.arrayElems a)
     Some n <- return $ mkNatRepr (genericLength elts)
     case isZeroOrGT1 n of
       Left Refl -> return $ XEmptyArray tp
-      Right LeqProof -> do
-        let Just v = V.fromList n elts
-        return $ withKnownNat n $ XArray v
+      Right LeqProof ->
+        case V.fromList n elts of
+           Just v -> return $ withKnownNat n $ XArray v
+           Nothing -> fail $ "Nothing on " ++ show n ++ " " ++ show elts
   CT.Struct _ -> do
-    elts <- forM (CT.toValues a) $ \(CT.Value tp (CT.Field a)) ->
-      translateConstExpr sym tp a
+    elts <- forM (CT.toValues a) $ \(CT.Value tp' (CT.Field a')) ->
+      translateConstExpr sym tp' a'
     return $ XStruct elts
 
 arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n
@@ -465,75 +467,75 @@ translateOp1 :: forall sym a b .
 translateOp1 sym origExpr op xe = case (op, xe) of
   (CE.Not, XBool e) -> liftIO $ fmap XBool $ WI.notPred sym e
   (CE.Not, _) -> panic ["Expected bool", show xe]
-  (CE.Abs _, xe) -> translateAbs xe
-  (CE.Sign _, xe) -> translateSign xe
+  (CE.Abs _, xe') -> translateAbs xe'
+  (CE.Sign _, xe') -> translateSign xe'
 
   -- We do not track any side conditions for floating-point operations
   -- (see Note [Side conditions for floating-point operations]), but we will
   -- make a note of which operations have partial inputs.
 
   -- The argument should not be zero
-  (CE.Recip _, xe) -> liftIO $ fpOp recip xe
+  (CE.Recip _, xe') -> liftIO $ fpOp' recip xe'
     where
       recip :: forall fi . FPOp1 sym fi
       recip fiRepr e = do
         one <- fpLit fiRepr 1.0
         WFP.iFloatDiv @_ @fi sym fpRM one e
   -- The argument should not cause the result to overflow or underlow
-  (CE.Exp _, xe) -> liftIO $ fpSpecialOp WSF.Exp xe
+  (CE.Exp _, xe') -> liftIO $ fpSpecialOp WSF.Exp xe'
   -- The argument should not be less than -0
-  (CE.Sqrt _, xe) ->
+  (CE.Sqrt _, xe') ->
     liftIO $
-    fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatSqrt @_ @fi sym fpRM) xe
+    fpOp' (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatSqrt @_ @fi sym fpRM) xe'
   -- The argument should not be negative or zero
-  (CE.Log _, xe) -> liftIO $ fpSpecialOp WSF.Log xe
+  (CE.Log _, xe') -> liftIO $ fpSpecialOp WSF.Log xe'
   -- The argument should not be infinite
-  (CE.Sin _, xe) -> liftIO $ fpSpecialOp WSF.Sin xe
+  (CE.Sin _, xe') -> liftIO $ fpSpecialOp WSF.Sin xe'
   -- The argument should not be infinite
-  (CE.Cos _, xe) -> liftIO $ fpSpecialOp WSF.Cos xe
+  (CE.Cos _, xe') -> liftIO $ fpSpecialOp WSF.Cos xe'
   -- The argument should not be infinite, nor should it cause the result to
   -- overflow
-  (CE.Tan _, xe) -> liftIO $ fpSpecialOp WSF.Tan xe
+  (CE.Tan _, xe') -> liftIO $ fpSpecialOp WSF.Tan xe'
   -- The argument should not cause the result to overflow
-  (CE.Sinh _, xe) -> liftIO $ fpSpecialOp WSF.Sinh xe
+  (CE.Sinh _, xe') -> liftIO $ fpSpecialOp WSF.Sinh xe'
   -- The argument should not cause the result to overflow
-  (CE.Cosh _, xe) -> liftIO $ fpSpecialOp WSF.Cosh xe
-  (CE.Tanh _, xe) -> liftIO $ fpSpecialOp WSF.Tanh xe
+  (CE.Cosh _, xe') -> liftIO $ fpSpecialOp WSF.Cosh xe'
+  (CE.Tanh _, xe') -> liftIO $ fpSpecialOp WSF.Tanh xe'
   -- The argument should not be outside the range [-1, 1]
-  (CE.Asin _, xe) -> liftIO $ fpSpecialOp WSF.Arcsin xe
+  (CE.Asin _, xe') -> liftIO $ fpSpecialOp WSF.Arcsin xe'
   -- The argument should not be outside the range [-1, 1]
-  (CE.Acos _, xe) -> liftIO $ fpSpecialOp WSF.Arccos xe
-  (CE.Atan _, xe) -> liftIO $ fpSpecialOp WSF.Arctan xe
-  (CE.Asinh _, xe) -> liftIO $ fpSpecialOp WSF.Arcsinh xe
+  (CE.Acos _, xe') -> liftIO $ fpSpecialOp WSF.Arccos xe'
+  (CE.Atan _, xe') -> liftIO $ fpSpecialOp WSF.Arctan xe'
+  (CE.Asinh _, xe') -> liftIO $ fpSpecialOp WSF.Arcsinh xe'
   -- The argument should not be less than 1
-  (CE.Acosh _, xe) -> liftIO $ fpSpecialOp WSF.Arccosh xe
+  (CE.Acosh _, xe') -> liftIO $ fpSpecialOp WSF.Arccosh xe'
   -- The argument should not be less than or equal to -1,
   -- nor should it be greater than or equal to +1
-  (CE.Atanh _, xe) -> liftIO $ fpSpecialOp WSF.Arctanh xe
+  (CE.Atanh _, xe') -> liftIO $ fpSpecialOp WSF.Arctanh xe'
   -- The argument should not cause the result to overflow
-  (CE.Ceiling _, xe) ->
+  (CE.Ceiling _, xe') ->
     liftIO $
-    fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatRound @_ @fi sym WI.RTP) xe
+    fpOp' (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatRound @_ @fi sym WI.RTP) xe'
   -- The argument should not cause the result to overflow
-  (CE.Floor _, xe) ->
+  (CE.Floor _, xe') ->
     liftIO $
-    fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatRound @_ @fi sym WI.RTN) xe
-  (CE.BwNot _, xe) -> liftIO $ case xe of
+    fpOp' (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatRound @_ @fi sym WI.RTN) xe'
+  (CE.BwNot _, xe') -> liftIO $ case xe' of
     XBool e -> XBool <$> WI.notPred sym e
-    _ -> bvOp (WI.bvNotBits sym) xe
-  (CE.Cast _ tp, xe) -> liftIO $ castOp sym origExpr tp xe
-  (CE.GetField atp _ftp extractor, xe) -> translateGetField atp extractor xe
+    _ -> bvOp' (WI.bvNotBits sym) xe'
+  (CE.Cast _ tp, xe') -> liftIO $ castOp sym origExpr tp xe'
+  (CE.GetField atp _ftp extractor, xe') -> translateGetField atp extractor xe'
   where
     -- Translate an 'CE.Abs' operation and its argument into a what4
     -- representation of the appropriate type.
     translateAbs :: XExpr sym -> TransM sym (XExpr sym)
-    translateAbs xe = do
-      addBVSidePred1 xe $ \e w _ -> do
+    translateAbs xe' = do
+      addBVSidePred1 xe' $ \e w _ -> do
         -- The argument should not be INT_MIN
         bvIntMin <- liftIO $ WI.bvLit sym w (BV.minSigned w)
         eqIntMin <- liftIO $ WI.bvEq sym e bvIntMin
         WI.notPred sym eqIntMin
-      liftIO $ numOp bvAbs fpAbs xe
+      liftIO $ numOp bvAbs fpAbs xe'
       where
         bvAbs :: BVOp1 sym w
         bvAbs e = do
@@ -556,7 +558,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
                       -> XExpr sym
                       -- ^ The argument value (should be a struct)
                       -> TransM sym (XExpr sym)
-    translateGetField tp extractor xe = case (tp, xe) of
+    translateGetField tp extractor xe' = case (tp, xe') of
       (CT.Struct s, XStruct xes) ->
         case mIx s of
           Just ix -> return $ xes !! ix
@@ -579,7 +581,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
     -- @x > 0 ? 1 : (x < 0 ? -1 : x)@. This matches how copilot-c99 translates
     -- 'CE.Sign' to C code.
     translateSign :: XExpr sym -> TransM sym (XExpr sym)
-    translateSign xe = liftIO $ numOp bvSign fpSign xe
+    translateSign xe' = liftIO $ numOp bvSign fpSign xe'
       where
         bvSign :: BVOp1 sym w
         bvSign e = do
@@ -608,7 +610,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
           -> (forall fpp . FPOp1 sym fpp)
           -> XExpr sym
           -> IO (XExpr sym)
-    numOp bvOp fpOp xe = case xe of
+    numOp bvOp fpOp xe' = case xe' of
       XInt8 e -> XInt8 <$> bvOp e
       XInt16 e -> XInt16 <$> bvOp e
       XInt32 e -> XInt32 <$> bvOp e
@@ -621,8 +623,8 @@ translateOp1 sym origExpr op xe = case (op, xe) of
       XDouble e -> XDouble <$> fpOp WFP.DoubleFloatRepr e
       _ -> unexpectedValue "numOp"
 
-    bvOp :: (forall w . BVOp1 sym w) -> XExpr sym -> IO (XExpr sym)
-    bvOp f xe = case xe of
+    bvOp' :: (forall w . BVOp1 sym w) -> XExpr sym -> IO (XExpr sym)
+    bvOp' f xe' = case xe' of
       XInt8 e -> XInt8 <$> f e
       XInt16 e -> XInt16 <$> f e
       XInt32 e -> XInt32 <$> f e
@@ -633,8 +635,8 @@ translateOp1 sym origExpr op xe = case (op, xe) of
       XWord64 e -> XWord64 <$> f e
       _ -> unexpectedValue "bvOp"
 
-    fpOp :: (forall fi . FPOp1 sym fi) -> XExpr sym -> IO (XExpr sym)
-    fpOp g xe = case xe of
+    fpOp' :: (forall fi . FPOp1 sym fi) -> XExpr sym -> IO (XExpr sym)
+    fpOp' g xe' = case xe' of
       XFloat e -> XFloat <$> g WFP.SingleFloatRepr e
       XDouble e -> XDouble <$> g WFP.DoubleFloatRepr e
       _ -> unexpectedValue "fpOp"
@@ -644,7 +646,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
     -- the solver.
     fpSpecialOp :: WSF.SpecialFunction (EmptyCtx ::> WSF.R)
                 -> XExpr sym -> IO (XExpr sym)
-    fpSpecialOp fn = fpOp (\fiRepr -> WFP.iFloatSpecialFunction1 sym fiRepr fn)
+    fpSpecialOp fn = fpOp' (\fiRepr -> WFP.iFloatSpecialFunction1 sym fiRepr fn)
 
     -- Construct a floating-point literal value of the appropriate type.
     fpLit :: forall fi.
@@ -662,8 +664,8 @@ translateOp1 sym origExpr op xe = case (op, xe) of
                        (Panic.HasCallStack, MonadIO m)
                     => String
                     -> m x
-    unexpectedValue op =
-      panic [ "Unexpected value in " ++ op ++ ": " ++ show (CP.ppExpr origExpr)
+    unexpectedValue op' =
+      panic [ "Unexpected value in " ++ op' ++ ": " ++ show (CP.ppExpr origExpr)
             , show xe
             ]
 
@@ -706,7 +708,7 @@ translateOp2 :: forall sym a b c .
              -> XExpr sym
              -> XExpr sym
              -> TransM sym (XExpr sym)
-translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
+translateOp2 sym origExpr op' xe1' xe2' = case (op', xe1', xe2') of
   (CE.And, XBool e1, XBool e2) -> liftIO $ fmap XBool $ WI.andPred sym e1 e2
   (CE.And, _, _) -> unexpectedValues "and operation"
   (CE.Or, XBool e1, XBool e2) -> liftIO $ fmap XBool $ WI.orPred sym e1 e2
@@ -717,11 +719,11 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
   (CE.Mod _, xe1, xe2) -> do
     -- The second argument should not be zero
     addBVSidePred1 xe2 $ \e2 _ _ -> WI.bvIsNonzero sym e2
-    liftIO $ bvOp (WI.bvSrem sym) (WI.bvUrem sym) xe1 xe2
+    liftIO $ bvOp' (WI.bvSrem sym) (WI.bvUrem sym) xe1 xe2
   (CE.Div _, xe1, xe2) -> do
     -- The second argument should not be zero
     addBVSidePred1 xe2 $ \e2 _ _ -> WI.bvIsNonzero sym e2
-    liftIO $ bvOp (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 xe2
+    liftIO $ bvOp' (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 xe2
 
   -- We do not track any side conditions for floating-point operations
   -- (see Note [Side conditions for floating-point operations]), but we will
@@ -730,23 +732,23 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
   -- The second argument should not be zero
   (CE.Fdiv _, xe1, xe2) ->
     liftIO $
-    fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatDiv @_ @fi sym fpRM)
+    fpOp' (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatDiv @_ @fi sym fpRM)
          xe1
          xe2
 
   -- None of the following should happen:
   --
-  -- * The first argument is negative, and the second argument is a finite
+  --   The first argument is negative, and the second argument is a finite
   --   noninteger
   --
-  -- * The first argument is zero, and the second argument is negative
+  --   The first argument is zero, and the second argument is negative
   --
-  -- * The arguments cause the result to overflow
+  --   The arguments cause the result to overflow
   --
-  -- * The arguments cause the result to underflow
+  --   The arguments cause the result to underflow
   (CE.Pow _, xe1, xe2) -> liftIO $ fpSpecialOp WSF.Pow xe1 xe2
   -- The second argument should not be negative or zero
-  (CE.Logb _, xe1, xe2) -> liftIO $ fpOp logbFn xe1 xe2
+  (CE.Logb _, xe1, xe2) -> liftIO $ fpOp' logbFn xe1 xe2
     where
       logbFn :: forall fi . FPOp2 sym fi
       -- Implement logb(e1,e2) as log(e2)/log(e1). This matches how copilot-c99
@@ -793,11 +795,11 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
            xe1
            xe2
   (CE.BwAnd _, xe1, xe2) ->
-    liftIO $ bvOp (WI.bvAndBits sym) (WI.bvAndBits sym) xe1 xe2
+    liftIO $ bvOp' (WI.bvAndBits sym) (WI.bvAndBits sym) xe1 xe2
   (CE.BwOr _, xe1, xe2) ->
-    liftIO $ bvOp (WI.bvOrBits sym) (WI.bvOrBits sym) xe1 xe2
+    liftIO $ bvOp' (WI.bvOrBits sym) (WI.bvOrBits sym) xe1 xe2
   (CE.BwXor _, xe1, xe2) ->
-    liftIO $ bvOp (WI.bvXorBits sym) (WI.bvXorBits sym) xe1 xe2
+    liftIO $ bvOp' (WI.bvXorBits sym) (WI.bvXorBits sym) xe1 xe2
   (CE.BwShiftL _ _, xe1, xe2) -> translateBwShiftL xe1 xe2
   (CE.BwShiftR _ _, xe1, xe2) -> translateBwShiftR xe1 xe2
   (CE.Index _, xe1, xe2) -> translateIndex xe1 xe2
@@ -1003,7 +1005,7 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
         -- Update an element of a list at a particular index. This assumes the
         -- preconditions that the index is a non-negative number that is less
         -- than the length of the list.
-        updateAt :: forall a. Int -> a -> [a] -> [a]
+        updateAt :: forall a'. Int -> a' -> [a'] -> [a']
         updateAt _ _ [] = []
         updateAt 0 new (_:xs) = new : xs
         updateAt n new (x:xs) = x : updateAt (n-1) new xs
@@ -1041,12 +1043,12 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
     -- Check the types of the arguments. If the arguments are signed bitvector
     -- values, apply the first 'BVOp2'. If the arguments are unsigned bitvector
     -- values, apply the second 'BVOp2'. Otherwise, 'panic'.
-    bvOp :: (forall w . BVOp2 sym w)
+    bvOp' :: (forall w . BVOp2 sym w)
          -> (forall w . BVOp2 sym w)
          -> XExpr sym
          -> XExpr sym
          -> IO (XExpr sym)
-    bvOp opS opU xe1 xe2 = case (xe1, xe2) of
+    bvOp' opS opU xe1 xe2 = case (xe1, xe2) of
       (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2
       (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2
       (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2
@@ -1057,11 +1059,11 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
       (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2
       _ -> unexpectedValues "bvOp"
 
-    fpOp :: (forall fi . FPOp2 sym fi)
+    fpOp' :: (forall fi . FPOp2 sym fi)
          -> XExpr sym
          -> XExpr sym
          -> IO (XExpr sym)
-    fpOp op xe1 xe2 = case (xe1, xe2) of
+    fpOp' op xe1 xe2 = case (xe1, xe2) of
       (XFloat e1, XFloat e2) -> XFloat <$> op WFP.SingleFloatRepr e1 e2
       (XDouble e1, XDouble e2) -> XDouble <$> op WFP.DoubleFloatRepr e1 e2
       _ -> unexpectedValues "fpOp"
@@ -1071,7 +1073,7 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
     -- the solver.
     fpSpecialOp :: WSF.SpecialFunction (EmptyCtx ::> WSF.R ::> WSF.R)
                 -> XExpr sym -> XExpr sym -> IO (XExpr sym)
-    fpSpecialOp fn = fpOp (\fiRepr -> WFP.iFloatSpecialFunction2 sym fiRepr fn)
+    fpSpecialOp fn = fpOp' (\fiRepr -> WFP.iFloatSpecialFunction2 sym fiRepr fn)
 
     -- Check the types of the arguments. If the arguments are bitvector values,
     -- apply the 'BVCmp2'. If the arguments are floating-point values, apply the
@@ -1126,7 +1128,7 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
                      -> m x
     unexpectedValues op =
       panic [ "Unexpected values in " ++ op ++ ": " ++ show (CP.ppExpr origExpr)
-            , show xe1, show xe2
+            , show xe1', show xe2'
             ]
 
 translateOp3 :: forall sym a b c d .
@@ -1140,7 +1142,7 @@ translateOp3 :: forall sym a b c d .
              -> XExpr sym
              -> XExpr sym
              -> TransM sym (XExpr sym)
-translateOp3 sym origExpr op xe1 xe2 xe3 = case (op, xe1, xe2, xe3) of
+translateOp3 sym origExpr op' xe1' xe2' xe3' = case (op', xe1', xe2', xe3') of
     (CE.Mux _, XBool te, xe1, xe2) -> liftIO $ mkIte sym te xe1 xe2
     (CE.Mux _, _, _, _) -> unexpectedValues "mux operation"
     (CE.UpdateArray _, xe1, xe2, xe3) -> translateUpdateArray xe1 xe2 xe3
@@ -1178,7 +1180,7 @@ translateOp3 sym origExpr op xe1 xe2 xe3 = case (op, xe1, xe2, xe3) of
                      => String -> m x
     unexpectedValues op =
       panic [ "Unexpected values in " ++ op ++ ":"
-            , show (CP.ppExpr origExpr), show xe1, show xe2, show xe3
+            , show (CP.ppExpr origExpr), show xe1', show xe2', show xe3'
             ]
 
 -- | Construct an expression that indexes into an array by building a chain of
diff --git a/copilot/src/Language/Copilot/Main.hs b/copilot/src/Language/Copilot/Main.hs
index cc23524b3..5fb4686aa 100644
--- a/copilot/src/Language/Copilot/Main.hs
+++ b/copilot/src/Language/Copilot/Main.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 -- | Create Copilot executables that generate code or interpret streams and
 -- print the results to stdout.
 module Language.Copilot.Main ( copilotMain, defaultMain ) where
@@ -9,7 +10,10 @@ import Copilot.Language (Spec)
 import qualified Copilot.PrettyPrint as PP
 
 import Options.Applicative
+#if MIN_VERSION_base(4,13,0)
+#else
 import Data.Semigroup ((<>))
+#endif
 import Control.Monad (when)
 
 -- | An interpreter of Copilot specifications for a given