From 21333a5117f91efde232a20f896735d1d3dd69c8 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Sat, 15 Nov 2025 21:06:37 +0300
Subject: [PATCH 01/20] warn fix warnings in core

---
 copilot-core/copilot-core.cabal               | 26 +++++++++----------
 copilot-core/src/Copilot/Core/Type.hs         |  9 +++++--
 copilot-core/src/Copilot/Core/Type/Array.hs   |  4 +--
 copilot-core/tests/Test/Copilot/Core/Type.hs  |  4 +--
 .../tests/Test/Copilot/Core/Type/Array.hs     |  8 +++---
 5 files changed, 26 insertions(+), 25 deletions(-)

diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal
index 6c18d6ca3..0df53251c 100644
--- a/copilot-core/copilot-core.cabal
+++ b/copilot-core/copilot-core.cabal
@@ -1,4 +1,4 @@
-cabal-version:       >=1.10
+cabal-version:       2.2
 name:                copilot-core
 version:             4.6
 synopsis:            An intermediate representation for Copilot.
@@ -14,7 +14,7 @@ description:
 
 author:              Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,
                      Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez
-license:             BSD3
+license:             BSD-3-Clause
 license-file:        LICENSE
 maintainer:          Ivan Perez <ivan.perezdominguez@nasa.gov>
 homepage:            https://copilot-language.github.io
@@ -31,16 +31,19 @@ source-repository head
     location:   https://github.com/Copilot-Language/copilot.git
     subdir:     copilot-core
 
-library
-
-  default-language:  Haskell2010
-
-  hs-source-dirs:    src
+common base
+  default-language:  GHC2021
+  default-extensions:
+    LambdaCase
+    NoGeneralizedNewtypeDeriving
 
   ghc-options:
     -Wall
-    -fno-warn-orphans
+    -Werror
 
+library
+  import: base
+  hs-source-dirs:    src
   build-depends:
     base >= 4.9 && < 5
 
@@ -54,6 +57,7 @@ library
     Copilot.Core.Type.Array
 
 test-suite unit-tests
+  import: base
   type:
     exitcode-stdio-1.0
 
@@ -77,9 +81,3 @@ test-suite unit-tests
 
   hs-source-dirs:
     tests
-
-  default-language:
-    Haskell2010
-
-  ghc-options:
-    -Wall
diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs
index b290810c2..05ac4c16e 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          #-}
@@ -48,6 +49,7 @@ module Copilot.Core.Type
 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
@@ -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       =  \case
+    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..1b71d6dbd 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 (_x: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..d6f3d96c6 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,7 @@ testSimpleTypesEqualityTransitive =
 -- | Test that each type is only equal to itself.
 testSimpleTypesEqualityUniqueness :: Property
 testSimpleTypesEqualityUniqueness =
-  forAllBlind (shuffle simpleTypes) $ \(t:ts) ->
-    notElem t ts
+  forAllBlind (shuffle simpleTypes) $ \case [] -> 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..7cf23c59f 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      $ \length' ->
+    forAll (xsInt64 length') $ \ls ->
       let array' :: Array n Int64
           array' = array ls
       in arrayElems array' == ls
   where
-    xsInt64 length = vectorOf length arbitrary
+    xsInt64 length' = vectorOf length' 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   $ \_v ->
       let -- Original array
           array' :: Array n Int64
           array' = array ls

From 269b649e33dc176538492c20122eff0e367fd5c4 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Sun, 16 Nov 2025 08:13:07 +0300
Subject: [PATCH 02/20] warn downgrade language to Haskell2010

---
 copilot-core/copilot-core.cabal | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal
index 0df53251c..b55923794 100644
--- a/copilot-core/copilot-core.cabal
+++ b/copilot-core/copilot-core.cabal
@@ -32,10 +32,9 @@ source-repository head
     subdir:     copilot-core
 
 common base
-  default-language:  GHC2021
+  default-language:  Haskell2010
   default-extensions:
     LambdaCase
-    NoGeneralizedNewtypeDeriving
 
   ghc-options:
     -Wall

From 268b6ebc5dee530de967638ea244759570593b5a Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Sun, 16 Nov 2025 08:24:48 +0300
Subject: [PATCH 03/20] warn fix warnings in prettyprinter

---
 copilot-prettyprinter/copilot-prettyprinter.cabal    |  9 +++++----
 .../src/Copilot/PrettyPrint/Type.hs                  | 12 +++++-------
 2 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal
index 0f413f63d..e38bfbdd0 100644
--- a/copilot-prettyprinter/copilot-prettyprinter.cabal
+++ b/copilot-prettyprinter/copilot-prettyprinter.cabal
@@ -1,4 +1,4 @@
-cabal-version:       >=1.10
+cabal-version:       2.2
 name:                copilot-prettyprinter
 version:             4.6
 synopsis:            A prettyprinter of Copilot Specifications.
@@ -14,7 +14,7 @@ description:
 
 author:              Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,
                      Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez
-license:             BSD3
+license:             BSD-3-Clause
 license-file:        LICENSE
 maintainer:          Ivan Perez <ivan.perezdominguez@nasa.gov>
 homepage:            https://copilot-language.github.io
@@ -34,12 +34,13 @@ source-repository head
 library
 
   default-language:  Haskell2010
-
+  default-extensions:
+    LambdaCase
   hs-source-dirs:    src
 
   ghc-options:
     -Wall
-    -fno-warn-orphans
+    -Werror
 
   build-depends:
     base   >= 4.9 && < 5,
diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
index 2f6f95f07..fcaa1539d 100644
--- a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
+++ b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
@@ -37,8 +37,7 @@ showWithType showT t x =
 
 -- | Show Copilot Core type.
 showType :: Type a -> String
-showType t =
-  case t of
+showType = \case
     Bool   -> "Bool"
     Int8   -> "Int8"
     Int16  -> "Int16"
@@ -51,7 +50,7 @@ showType t =
     Float  -> "Float"
     Double -> "Double"
     Array t -> "Array " ++ showType t
-    Struct t -> "Struct"
+    Struct _ -> "Struct"
 
 -- * Auxiliary show instance
 
@@ -60,8 +59,7 @@ data ShowWit a = Show a => ShowWit
 
 -- | Turn a type into a show witness.
 showWit :: Type a -> ShowWit a
-showWit t =
-  case t of
+showWit = \case
     Bool   -> ShowWit
     Int8   -> ShowWit
     Int16  -> ShowWit
@@ -73,5 +71,5 @@ showWit t =
     Word64 -> ShowWit
     Float  -> ShowWit
     Double -> ShowWit
-    Array t -> ShowWit
-    Struct t -> ShowWit
+    Array _ -> ShowWit
+    Struct _ -> ShowWit

From d952fed75a864e4594b95e5b529f1e1c3a917b25 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Sun, 16 Nov 2025 09:11:24 +0300
Subject: [PATCH 04/20] warn fix interpreter warnings

---
 copilot-interpreter/copilot-interpreter.cabal | 23 +++++++--------
 .../src/Copilot/Interpret/Eval.hs             | 28 ++++++++++---------
 .../src/Copilot/Interpret/Render.hs           | 24 ++++++++--------
 .../tests/Test/Copilot/Interpret/Eval.hs      | 13 ++++-----
 4 files changed, 42 insertions(+), 46 deletions(-)

diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal
index e8b9fad4f..3c07b8b5d 100644
--- a/copilot-interpreter/copilot-interpreter.cabal
+++ b/copilot-interpreter/copilot-interpreter.cabal
@@ -1,4 +1,4 @@
-cabal-version:       >=1.10
+cabal-version:       2.2
 name:                copilot-interpreter
 version:             4.6
 synopsis:            Interpreter for Copilot.
@@ -14,7 +14,7 @@ description:
 
 author:              Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,
                      Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez
-license:             BSD3
+license:             BSD-3-Clause
 license-file:        LICENSE
 maintainer:          Ivan Perez <ivan.perezdominguez@nasa.gov>
 homepage:            https://copilot-language.github.io
@@ -31,15 +31,17 @@ source-repository head
     location:   https://github.com/Copilot-Language/copilot.git
     subdir:     copilot-interpreter
 
-library
-
+common base
   default-language:  Haskell2010
-
-  hs-source-dirs:    src
-
+  default-extensions:
+    LambdaCase
   ghc-options:
     -Wall
+    -Werror
 
+library
+  import: base
+  hs-source-dirs:    src
   build-depends:
     base       >= 4.9 && < 5,
     pretty     >= 1.0 && < 1.2,
@@ -57,6 +59,7 @@ library
     Copilot.Interpret.Render
 
 test-suite unit-tests
+  import: base
   type:
     exitcode-stdio-1.0
 
@@ -80,9 +83,3 @@ test-suite unit-tests
 
   hs-source-dirs:
     tests
-
-  default-language:
-    Haskell2010
-
-  ghc-options:
-    -Wall
diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
index 462b5853e..68fe751e0 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 _t 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 _t1 _ 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 _t 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,14 @@ 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 _ty) = \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 } =
+                } =
   (id, toDyn (reverse buffer))
 
 -- | Evaluate several streams for a number of steps, producing the environment
@@ -293,7 +295,7 @@ evalStreams top specStrms initStrms =
     strms_ = map evalStream specStrms
     evalStream Stream { streamId       = id
                       , streamExpr     = e
-                      , streamExprType = t } =
+                      } =
       let xs = fromJust $ lookup id strms >>= fromDynamic      in
       let x  = evalExpr_ k e [] strms                          in
       let ls = x `seq` (x:xs)                                  in
@@ -402,5 +404,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..5baef97f3 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 max' b ls = ls ++ replicate (max' - lx) b
 
 -- | Pad a list of strings on the right with spaces.
 pad' :: Int      -- ^ Mininum number of spaces to add
diff --git a/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs b/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
index bcabddc21..87677c07f 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"
@@ -787,8 +787,7 @@ lookupWithDefault k def = fromMaybe def . lookup k
 
 -- | Show Copilot Core type.
 showType :: Type a -> String
-showType t =
-  case t of
+showType = \case
     Bool   -> "Bool"
     Int8   -> "Int8"
     Int16  -> "Int16"
@@ -801,4 +800,4 @@ showType t =
     Float  -> "Float"
     Double -> "Double"
     Array t -> "Array " ++ showType t
-    Struct t -> "Struct"
+    Struct _ -> "Struct"

From 303ca49a82546e2b1962c2601498941cd29db9d0 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Sun, 16 Nov 2025 12:47:32 +0300
Subject: [PATCH 05/20] warn fix theorem warnings

---
 copilot-theorem/copilot-theorem.cabal         |  7 +-
 .../src/Copilot/Theorem/IL/PrettyPrint.hs     | 18 +----
 .../src/Copilot/Theorem/IL/Spec.hs            |  2 +-
 .../src/Copilot/Theorem/IL/Transform.hs       |  6 +-
 .../src/Copilot/Theorem/IL/Translate.hs       | 39 ++++-----
 .../src/Copilot/Theorem/Kind2/Output.hs       |  4 +-
 .../src/Copilot/Theorem/Kind2/PrettyPrint.hs  |  1 +
 .../src/Copilot/Theorem/Kind2/Prover.hs       | 11 +--
 .../src/Copilot/Theorem/Kind2/Translate.hs    |  3 +-
 .../src/Copilot/Theorem/Misc/SExpr.hs         |  9 ++-
 .../src/Copilot/Theorem/Misc/Utils.hs         |  9 +--
 copilot-theorem/src/Copilot/Theorem/Prove.hs  |  4 +-
 .../src/Copilot/Theorem/Prover/SMT.hs         |  8 +-
 .../src/Copilot/Theorem/Prover/SMTLib.hs      | 11 ++-
 .../src/Copilot/Theorem/Prover/TPTP.hs        |  3 +-
 .../src/Copilot/Theorem/TransSys/Cast.hs      |  1 +
 .../src/Copilot/Theorem/TransSys/Operators.hs | 10 ++-
 .../Copilot/Theorem/TransSys/PrettyPrint.hs   |  3 +
 .../src/Copilot/Theorem/TransSys/Renaming.hs  | 10 ++-
 .../src/Copilot/Theorem/TransSys/Spec.hs      |  6 +-
 .../src/Copilot/Theorem/TransSys/Transform.hs | 28 ++++---
 .../src/Copilot/Theorem/TransSys/Translate.hs | 27 +++++--
 copilot-theorem/src/Copilot/Theorem/What4.hs  |  9 +--
 .../src/Copilot/Theorem/What4/Translate.hs    | 79 ++++++++++---------
 24 files changed, 164 insertions(+), 144 deletions(-)

diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal
index b830f91a6..1411c8f81 100644
--- a/copilot-theorem/copilot-theorem.cabal
+++ b/copilot-theorem/copilot-theorem.cabal
@@ -40,10 +40,8 @@ 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
+                            -Werror
 
   build-depends           : base                  >= 4.9 && < 5
                           , bimap                 (>= 0.3 && < 0.4) || (>= 0.5 && < 0.6)
@@ -136,3 +134,4 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
+    -Werror
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/IL/PrettyPrint.hs
index 196873060..53289bea0 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..ccb5996c4 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
@@ -4,7 +4,11 @@
 -- | Simplify IL expressions by partly evaluating operations on booleans.
 module Copilot.Theorem.IL.Transform ( bsimpl ) where
 
-import Copilot.Theorem.IL.Spec
+import safe Copilot.Theorem.IL.Spec
+    ( Expr(FunApp, Ite, Op1, ConstB, Op2),
+      Type(Bool),
+      Op1(Not),
+      Op2(Eq, Or, And) )
 
 -- | 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..71b252ca9 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
@@ -25,6 +25,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 +38,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 +79,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 t' = case t' of
   C.Int8    -> bound' C.Int8
   C.Int16   -> bound' C.Int16
   C.Int32   -> bound' C.Int32
@@ -140,14 +138,14 @@ expr (C.ExternVar t name _) = bound s t >> return s
   where
     s = SVal (trType t) (ncExternVar name) _n_
 
-expr (C.Op1 (C.Sign ta) e) = case ta of
-  C.Int8   -> trSign ta e
-  C.Int16  -> trSign ta e
-  C.Int32  -> trSign ta e
-  C.Int64  -> trSign ta e
-  C.Float  -> trSign ta e
-  C.Double -> trSign ta e
-  _        -> expr $ C.Const ta 1
+expr (C.Op1 (C.Sign ta') e') = case ta' of
+  C.Int8   -> trSign ta' e'
+  C.Int16  -> trSign ta' e'
+  C.Int32  -> trSign ta' e'
+  C.Int64  -> trSign ta' e'
+  C.Float  -> trSign ta' e'
+  C.Double -> trSign ta' e'
+  _        -> expr $ C.Const ta' 1
   where
     trSign :: (Typeable a, Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr
     trSign ta e =
@@ -187,9 +185,10 @@ 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
+trConst t' v = case t' of
   C.Bool   -> ConstB v
   C.Float  -> negifyR (float2Double v)
   C.Double -> negifyR v
@@ -201,15 +200,16 @@ trConst t v = case t of
   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 +282,7 @@ trType = \case
   C.Word64 -> BV64
   C.Float  -> Real
   C.Double -> Real
+  _o       -> 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..304b573b2 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
@@ -35,9 +35,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 +47,14 @@ kind2Prover opts = Prover
   , askProver    = askKind2
   , closeProver  = const $ return () }
 
+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 +71,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..0732eb52a 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,7 +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)
+      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..ff12a850f 100644
--- a/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
@@ -7,9 +7,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
@@ -28,17 +26,18 @@ isSublistOf = Set.isSubsetOf `on` Set.fromList
 nubEq :: Ord a => [a] -> [a] -> Bool
 nubEq = (==) `on` Set.fromList
 
+
 -- | Remove duplicates from a list.
 --
 -- This is an efficient version of 'Data.List.nub' that works for lists with a
 -- 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..1b6d8940b 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prove.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prove.hs
@@ -21,7 +21,6 @@ module Copilot.Theorem.Prove
 import qualified Copilot.Core as Core
 
 import Data.List (intercalate)
-import Control.Applicative (liftA2)
 import Control.Monad        (ap, liftM)
 import Control.Monad.Writer
 
@@ -79,12 +78,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..911b8f3c3 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs
@@ -8,8 +8,15 @@ module Copilot.Theorem.Prover.SMTLib (SmtLib, interpret) where
 
 import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))
 
-import Copilot.Theorem.IL
-import Copilot.Theorem.Misc.SExpr
+import safe Copilot.Theorem.IL.Spec
+    ( Expr(..),
+      Type(Real, Bool),
+      Op1(Acosh, Not, Neg, Abs, Exp, Sqrt, Log, Sin, Tan, Cos, Asin,
+          Atan, Acos, Sinh, Tanh, Cosh, Asinh, Atanh),
+      Op2(Pow, Eq, Le, Lt, Ge, Gt, And, Or, Add, Sub, Mul, Mod, Fdiv),
+      SeqIndex(Var, Fixed) )
+import safe Copilot.Theorem.Misc.SExpr
+    ( SExpr, blank, atom, singleton, list, node )
 
 import Text.Printf
 
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs b/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
index e179409e8..90f79b2db 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
@@ -7,7 +7,8 @@
 module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where
 
 import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))
-import Copilot.Theorem.IL
+import safe Copilot.Theorem.IL
+    ( Expr(..), Op1(..), Op2(..), SeqIndex(Var, Fixed) )
 
 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..2e2f7af87 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
@@ -135,7 +135,7 @@ handleOp1 ::
 
   -> m (expr resT)
 
-handleOp1 resT (op, e) handleExpr notHandledF mkOp = case op of
+handleOp1 resT (op', e) handleExpr notHandledF mkOp = case op' of
 
   C.Not      -> boolOp Not (handleExpr Bool e)
 
@@ -168,11 +168,12 @@ 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)
@@ -221,7 +222,7 @@ handleOp2 ::
 
   -> m (expr resT)
 
-handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of
+handleOp2 resT (op', e1, e2) handleExpr notHandledF mkOp notOp = case op' of
 
   C.And        -> boolConnector And
   C.Or         -> boolConnector Or
@@ -261,6 +262,7 @@ 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
 
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
index 3debe552c..f42981130 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
@@ -14,7 +14,9 @@ import qualified Data.Bimap as Bimap
 
 import Prelude hiding ((<>))
 
+indent :: Doc -> Doc
 indent     = nest 4
+emptyLine :: Doc
 emptyLine  = text ""
 
 -- | Pretty print a TransSys specification as a Kind2/Lustre specification.
@@ -30,6 +32,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..8e8aabbc3 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..bb65b31b1 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
@@ -32,11 +32,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 +102,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 +114,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..18cf4a9fb 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
@@ -207,9 +208,10 @@ removeCycles spec =
     buildScc nrep ns =
      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 +233,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 +248,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 +270,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..6b9c668f8 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
@@ -43,7 +43,7 @@
 -- 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
 
@@ -52,25 +52,31 @@ 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)
 
 import qualified Copilot.Core as C
 import qualified Data.Map     as Map
 import qualified Data.Bimap   as Bimap
-
+import Prelude hiding (id)
 -- Naming conventions
 -- These are important in order to avoid name conflicts
 
+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"
-ncAnonInput   = "in"
+ncLocal :: [Char] -> [Char]
 ncLocal s     = "l" ++ dropWhile (not . isNumber) s
 
+ncExternVarNode :: [Char] -> [Char]
 ncExternVarNode name = "ext-" ++ name
 
 ncImported :: NodeId -> String -> String
@@ -121,6 +127,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 +182,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
@@ -230,6 +236,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 +262,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 +279,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 +302,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 :: MonadState TransSt m => NodeId -> U Type -> m ()
 newExtVarNode id t =
   modify $ \st -> st { _extVarsNodes = (id, t) : _extVarsNodes st }
diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs
index 51ed6e8ff..7e2dc3ad1 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4.hs
@@ -79,7 +79,7 @@ import Data.Parameterized.Some
 import qualified Data.Parameterized.Vector as V
 import GHC.Float (castWord32ToFloat, castWord64ToDouble)
 import LibBF (BigFloat, bfToDouble, pattern NearEven)
-import qualified Panic as Panic
+import qualified Panic
 
 import Copilot.Theorem.What4.Translate
 
@@ -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..674c8d3cb 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
@@ -64,8 +64,8 @@ import           Data.Type.Equality             (TestEquality (..), (:~:) (..))
 import           Data.Word                      (Word32)
 import           GHC.TypeLits                   (KnownSymbol)
 import           GHC.TypeNats                   (KnownNat, type (<=), type (+))
-import qualified Panic                          as Panic
-
+import qualified Panic
+import Prelude hiding (pred, recip, id)
 import qualified What4.BaseTypes                as WT
 import qualified What4.Interface                as WI
 import qualified What4.InterpretedFloatingPoint as WFP
@@ -366,17 +366,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
@@ -462,9 +463,9 @@ translateOp1 :: forall sym a b .
              -> CE.Op1 a b
              -> XExpr sym
              -> TransM sym (XExpr sym)
-translateOp1 sym origExpr op xe = case (op, xe) of
+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.Not, _) -> panic ["Expected bool", show xe']
   (CE.Abs _, xe) -> translateAbs xe
   (CE.Sign _, xe) -> translateSign xe
 
@@ -473,7 +474,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
   -- 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
@@ -484,7 +485,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
   -- The argument should not be less than -0
   (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
   -- The argument should not be infinite
@@ -513,14 +514,14 @@ translateOp1 sym origExpr op xe = case (op, xe) of
   -- The argument should not cause the result to overflow
   (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) ->
     liftIO $
-    fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatRound @_ @fi sym WI.RTN) xe
+    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
+    _ -> 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
@@ -621,8 +622,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 +634,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 +645,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.
@@ -664,7 +665,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
                     -> m x
     unexpectedValue op =
       panic [ "Unexpected value in " ++ op ++ ": " ++ show (CP.ppExpr origExpr)
-            , show xe
+            , show xe'
             ]
 
 type BVOp2 sym w =
@@ -706,7 +707,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 +718,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,7 +731,7 @@ 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
 
@@ -746,7 +747,7 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
   -- * 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 +794,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 +1004,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 +1042,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 +1058,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 +1072,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 +1127,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 +1141,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 +1179,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

From 71fcfa802421e7d563301ea924fe2bc8ae711d17 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Sun, 16 Nov 2025 12:58:18 +0300
Subject: [PATCH 06/20] warn remove common and lambdacase from core cabal

---
 copilot-core/copilot-core.cabal              | 22 ++++++++++++--------
 copilot-core/src/Copilot/Core/Type.hs        |  4 ++--
 copilot-core/tests/Test/Copilot/Core/Type.hs |  2 +-
 3 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal
index b55923794..1ee498c7a 100644
--- a/copilot-core/copilot-core.cabal
+++ b/copilot-core/copilot-core.cabal
@@ -1,4 +1,4 @@
-cabal-version:       2.2
+cabal-version:       >=1.10
 name:                copilot-core
 version:             4.6
 synopsis:            An intermediate representation for Copilot.
@@ -14,7 +14,7 @@ description:
 
 author:              Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,
                      Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez
-license:             BSD-3-Clause
+license:             BSD3
 license-file:        LICENSE
 maintainer:          Ivan Perez <ivan.perezdominguez@nasa.gov>
 homepage:            https://copilot-language.github.io
@@ -31,18 +31,16 @@ source-repository head
     location:   https://github.com/Copilot-Language/copilot.git
     subdir:     copilot-core
 
-common base
+library
+
   default-language:  Haskell2010
-  default-extensions:
-    LambdaCase
+
+  hs-source-dirs:    src
 
   ghc-options:
     -Wall
     -Werror
 
-library
-  import: base
-  hs-source-dirs:    src
   build-depends:
     base >= 4.9 && < 5
 
@@ -56,7 +54,6 @@ library
     Copilot.Core.Type.Array
 
 test-suite unit-tests
-  import: base
   type:
     exitcode-stdio-1.0
 
@@ -80,3 +77,10 @@ test-suite unit-tests
 
   hs-source-dirs:
     tests
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall
+    -Werror
diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs
index 05ac4c16e..8633cc5fa 100644
--- a/copilot-core/src/Copilot/Core/Type.hs
+++ b/copilot-core/src/Copilot/Core/Type.hs
@@ -289,8 +289,8 @@ instance Typed Double where
 
 instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
   typeOf               = Array typeOf
-  simpleType       =  \case
-    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).
diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs
index d6f3d96c6..9c7ca9327 100644
--- a/copilot-core/tests/Test/Copilot/Core/Type.hs
+++ b/copilot-core/tests/Test/Copilot/Core/Type.hs
@@ -135,7 +135,7 @@ testSimpleTypesEqualityTransitive =
 -- | Test that each type is only equal to itself.
 testSimpleTypesEqualityUniqueness :: Property
 testSimpleTypesEqualityUniqueness =
-  forAllBlind (shuffle simpleTypes) $ \case [] -> False; (t:ts) ->  notElem  t ts
+  forAllBlind (shuffle simpleTypes) $ \x -> case x of [] -> False; (t:ts) ->  notElem t ts
 
 -- | Simple types tested.
 simpleTypes :: [SimpleType]

From d7f01792bdb4222f84f39976c0f4985c7f5565ab Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Sun, 16 Nov 2025 15:26:55 +0300
Subject: [PATCH 07/20] warn revert cabals and fix rest of warnings

---
 copilot-bluespec/copilot-bluespec.cabal       |  3 +-
 copilot-c99/copilot-c99.cabal                 |  3 +-
 .../src/Copilot/Compile/C99/CodeGen.hs        |  2 ++
 copilot-c99/src/Copilot/Compile/C99/Expr.hs   | 18 +++++-----
 .../src/Copilot/Compile/C99/Representation.hs |  2 +-
 copilot-c99/tests/Test/Copilot/Compile/C99.hs | 24 ++++++-------
 copilot-interpreter/copilot-interpreter.cabal | 23 +++++++-----
 .../tests/Test/Copilot/Interpret/Eval.hs      |  2 +-
 copilot-language/copilot-language.cabal       |  2 ++
 copilot-language/src/Copilot/Language.hs      |  1 -
 .../src/Copilot/Language/Analyze.hs           | 35 ++++++++-----------
 .../src/Copilot/Language/Reify.hs             | 20 +++--------
 .../src/Copilot/Language/Stream.hs            |  3 +-
 .../tests/Test/Copilot/Language/Reify.hs      |  2 +-
 copilot-libraries/copilot-libraries.cabal     |  2 ++
 copilot-libraries/src/Copilot/Library/MTL.hs  | 17 +++++----
 copilot-libraries/tests/Test/Extra.hs         |  5 ---
 .../copilot-prettyprinter.cabal               |  7 ++--
 .../src/Copilot/PrettyPrint/Type.hs           |  4 +--
 .../src/Copilot/Theorem/IL/Translate.hs       |  3 ++
 .../src/Copilot/Theorem/Kind2/Prover.hs       |  5 +++
 .../src/Copilot/Theorem/Misc/Utils.hs         |  5 +++
 copilot-theorem/src/Copilot/Theorem/Prove.hs  |  5 +++
 .../src/Copilot/Theorem/TransSys/Spec.hs      |  6 ++++
 .../src/Copilot/Theorem/TransSys/Translate.hs |  6 +++-
 copilot-theorem/src/Copilot/Theorem/What4.hs  |  2 +-
 .../src/Copilot/Theorem/What4/Translate.hs    |  8 ++---
 copilot-visualizer/copilot-visualizer.cabal   |  2 ++
 copilot/copilot.cabal                         |  2 +-
 copilot/src/Language/Copilot/Main.hs          |  4 +++
 30 files changed, 124 insertions(+), 99 deletions(-)

diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal
index 975868aca..394c249e2 100644
--- a/copilot-bluespec/copilot-bluespec.cabal
+++ b/copilot-bluespec/copilot-bluespec.cabal
@@ -38,7 +38,7 @@ library
   default-language        : Haskell2010
   hs-source-dirs          : src
 
-  ghc-options             : -Wall
+  ghc-options             : -Wall -Werror
   build-depends           : base              >= 4.9    && < 5
                           , directory         >= 1.3    && < 1.4
                           , filepath          >= 1.4    && < 1.6
@@ -98,3 +98,4 @@ test-suite tests
 
   ghc-options:
     -Wall
+    -Werror
diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal
index e5efd5f24..0f100ed5a 100644
--- a/copilot-c99/copilot-c99.cabal
+++ b/copilot-c99/copilot-c99.cabal
@@ -38,7 +38,7 @@ library
   default-language        : Haskell2010
   hs-source-dirs          : src
 
-  ghc-options             : -Wall
+  ghc-options             : -Wall -Werror
   build-depends           : base                >= 4.9 && < 5
                           , directory           >= 1.3 && < 1.4
                           , filepath            >= 1.4 && < 1.6
@@ -95,3 +95,4 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
+    -Werror
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..05478dea1 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 arrTy'@(Array ty) = C.LitInt (fromIntegral $ typeLength arrTy')
                          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' size'
           where
             dest = C.Index (C.Ident varName) e2'
-            size = C.LitInt
+            size' = 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-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal
index 3c07b8b5d..14ac4a2fc 100644
--- a/copilot-interpreter/copilot-interpreter.cabal
+++ b/copilot-interpreter/copilot-interpreter.cabal
@@ -1,4 +1,4 @@
-cabal-version:       2.2
+cabal-version:       >=1.10
 name:                copilot-interpreter
 version:             4.6
 synopsis:            Interpreter for Copilot.
@@ -14,7 +14,7 @@ description:
 
 author:              Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,
                      Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez
-license:             BSD-3-Clause
+license:             BSD3
 license-file:        LICENSE
 maintainer:          Ivan Perez <ivan.perezdominguez@nasa.gov>
 homepage:            https://copilot-language.github.io
@@ -31,17 +31,16 @@ source-repository head
     location:   https://github.com/Copilot-Language/copilot.git
     subdir:     copilot-interpreter
 
-common base
+library
+
   default-language:  Haskell2010
-  default-extensions:
-    LambdaCase
+
+  hs-source-dirs:    src
+
   ghc-options:
     -Wall
     -Werror
 
-library
-  import: base
-  hs-source-dirs:    src
   build-depends:
     base       >= 4.9 && < 5,
     pretty     >= 1.0 && < 1.2,
@@ -59,7 +58,6 @@ library
     Copilot.Interpret.Render
 
 test-suite unit-tests
-  import: base
   type:
     exitcode-stdio-1.0
 
@@ -83,3 +81,10 @@ test-suite unit-tests
 
   hs-source-dirs:
     tests
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall
+    -Werror
diff --git a/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs b/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
index 87677c07f..d52535832 100644
--- a/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
+++ b/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
@@ -787,7 +787,7 @@ lookupWithDefault k def = fromMaybe def . lookup k
 
 -- | Show Copilot Core type.
 showType :: Type a -> String
-showType = \case
+showType t' = case t' of
     Bool   -> "Bool"
     Int8   -> "Int8"
     Int16  -> "Int16"
diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal
index 543a11770..fefde30cf 100644
--- a/copilot-language/copilot-language.cabal
+++ b/copilot-language/copilot-language.cabal
@@ -74,6 +74,7 @@ library
                  , Copilot.Language.Error
   ghc-options:
     -Wall
+    -Werror
 
 test-suite unit-tests
   type:
@@ -107,3 +108,4 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
+    -Werror
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..82d6a17e9 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 _ [] = fail "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..547bb1844 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/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal
index 9b17524f4..d9a190324 100644
--- a/copilot-libraries/copilot-libraries.cabal
+++ b/copilot-libraries/copilot-libraries.cabal
@@ -57,6 +57,7 @@ library
 
   ghc-options:
     -Wall
+    -Werror
 
 test-suite unit-tests
   type:
@@ -88,3 +89,4 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
+    -Werror
diff --git a/copilot-libraries/src/Copilot/Library/MTL.hs b/copilot-libraries/src/Copilot/Library/MTL.hs
index 1ea570844..65efd9629 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,10 +30,10 @@ 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)
+  mins = clk + constant l
+  maxes = clk + constant u
   res _ _ 0 = false
   res c s k =
     c <= maxes && ((mins <= c && s) || nextRes c s k)
@@ -46,10 +45,10 @@ 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)
+  mins = clk - constant u
+  maxes = clk - constant l
   res _ _ 0 = false
   res c s k =
     mins <= c && ((c <= maxes && s) || nextRes c s k)
@@ -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/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal
index e38bfbdd0..4f6b1b86d 100644
--- a/copilot-prettyprinter/copilot-prettyprinter.cabal
+++ b/copilot-prettyprinter/copilot-prettyprinter.cabal
@@ -1,4 +1,4 @@
-cabal-version:       2.2
+cabal-version:       >=1.10
 name:                copilot-prettyprinter
 version:             4.6
 synopsis:            A prettyprinter of Copilot Specifications.
@@ -14,7 +14,7 @@ description:
 
 author:              Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,
                      Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez
-license:             BSD-3-Clause
+license:             BSD3
 license-file:        LICENSE
 maintainer:          Ivan Perez <ivan.perezdominguez@nasa.gov>
 homepage:            https://copilot-language.github.io
@@ -34,8 +34,7 @@ source-repository head
 library
 
   default-language:  Haskell2010
-  default-extensions:
-    LambdaCase
+
   hs-source-dirs:    src
 
   ghc-options:
diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
index fcaa1539d..22174ffe2 100644
--- a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
+++ b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
@@ -37,7 +37,7 @@ showWithType showT t x =
 
 -- | Show Copilot Core type.
 showType :: Type a -> String
-showType = \case
+showType t' = case t' of
     Bool   -> "Bool"
     Int8   -> "Int8"
     Int16  -> "Int16"
@@ -59,7 +59,7 @@ data ShowWit a = Show a => ShowWit
 
 -- | Turn a type into a show witness.
 showWit :: Type a -> ShowWit a
-showWit = \case
+showWit t = case t of
     Bool   -> ShowWit
     Int8   -> ShowWit
     Int16  -> ShowWit
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
index 71b252ca9..b5a44c9b6 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE Safe                #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE CPP #-}
 
 -- | Translate Copilot specifications into IL specifications.
 module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where
@@ -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
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
index 304b573b2..6181b573f 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
diff --git a/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs b/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
index ff12a850f..078f2dc8a 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
diff --git a/copilot-theorem/src/Copilot/Theorem/Prove.hs b/copilot-theorem/src/Copilot/Theorem/Prove.hs
index 1b6d8940b..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,7 +22,11 @@ module Copilot.Theorem.Prove
 import qualified Copilot.Core as Core
 
 import Data.List (intercalate)
+#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
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
index bb65b31b1..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
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
index 6b9c668f8..2b8dc1ca8 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      #-}
@@ -47,7 +48,10 @@ 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)
diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs
index 7e2dc3ad1..f91fdde8b 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)
diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
index 674c8d3cb..6d04870a2 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
@@ -737,14 +737,14 @@ translateOp2 sym origExpr op' xe1' xe2' = case (op', xe1', xe2') of
 
   -- 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
diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal
index 6afd9070a..d3a689726 100644
--- a/copilot-visualizer/copilot-visualizer.cabal
+++ b/copilot-visualizer/copilot-visualizer.cabal
@@ -54,6 +54,7 @@ library
 
   ghc-options:
     -Wall
+    -Werror
 
   build-depends:
     base       >= 4.9     && < 5,
@@ -117,6 +118,7 @@ executable tikz-example
 
   ghc-options:
     -Wall
+    -Werror
 
   build-depends:
     base               >= 4.9 && < 5,
diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal
index f52eecc4e..f5a18e6c9 100644
--- a/copilot/copilot.cabal
+++ b/copilot/copilot.cabal
@@ -45,7 +45,7 @@ library
     default-language:  Haskell2010
     ghc-options:
       -Wall
-      -fno-warn-orphans
+      -Werror
     build-depends:
                        base                  >= 4.9  && < 5
                      , optparse-applicative  >= 0.14 && < 0.19
diff --git a/copilot/src/Language/Copilot/Main.hs b/copilot/src/Language/Copilot/Main.hs
index cc23524b3..b03b82ada 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,19,0)
+#else
 import Data.Semigroup ((<>))
+#endif
 import Control.Monad (when)
 
 -- | An interpreter of Copilot specifications for a given

From 895828eea43cfc49c50eb0a833f88eec7edd8fc0 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Mon, 17 Nov 2025 14:12:15 +0300
Subject: [PATCH 08/20] warn remove Werror

---
 copilot-bluespec/copilot-bluespec.cabal           | 3 +--
 copilot-c99/copilot-c99.cabal                     | 3 +--
 copilot-core/copilot-core.cabal                   | 2 --
 copilot-interpreter/copilot-interpreter.cabal     | 2 --
 copilot-language/copilot-language.cabal           | 2 --
 copilot-libraries/copilot-libraries.cabal         | 2 --
 copilot-prettyprinter/copilot-prettyprinter.cabal | 1 -
 copilot-theorem/copilot-theorem.cabal             | 2 --
 copilot-visualizer/copilot-visualizer.cabal       | 2 --
 copilot/copilot.cabal                             | 1 -
 10 files changed, 2 insertions(+), 18 deletions(-)

diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal
index 394c249e2..975868aca 100644
--- a/copilot-bluespec/copilot-bluespec.cabal
+++ b/copilot-bluespec/copilot-bluespec.cabal
@@ -38,7 +38,7 @@ library
   default-language        : Haskell2010
   hs-source-dirs          : src
 
-  ghc-options             : -Wall -Werror
+  ghc-options             : -Wall
   build-depends           : base              >= 4.9    && < 5
                           , directory         >= 1.3    && < 1.4
                           , filepath          >= 1.4    && < 1.6
@@ -98,4 +98,3 @@ test-suite tests
 
   ghc-options:
     -Wall
-    -Werror
diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal
index 0f100ed5a..e5efd5f24 100644
--- a/copilot-c99/copilot-c99.cabal
+++ b/copilot-c99/copilot-c99.cabal
@@ -38,7 +38,7 @@ library
   default-language        : Haskell2010
   hs-source-dirs          : src
 
-  ghc-options             : -Wall -Werror
+  ghc-options             : -Wall
   build-depends           : base                >= 4.9 && < 5
                           , directory           >= 1.3 && < 1.4
                           , filepath            >= 1.4 && < 1.6
@@ -95,4 +95,3 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
-    -Werror
diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal
index 1ee498c7a..f2ee3e6ee 100644
--- a/copilot-core/copilot-core.cabal
+++ b/copilot-core/copilot-core.cabal
@@ -39,7 +39,6 @@ library
 
   ghc-options:
     -Wall
-    -Werror
 
   build-depends:
     base >= 4.9 && < 5
@@ -83,4 +82,3 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
-    -Werror
diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal
index 14ac4a2fc..e8b9fad4f 100644
--- a/copilot-interpreter/copilot-interpreter.cabal
+++ b/copilot-interpreter/copilot-interpreter.cabal
@@ -39,7 +39,6 @@ library
 
   ghc-options:
     -Wall
-    -Werror
 
   build-depends:
     base       >= 4.9 && < 5,
@@ -87,4 +86,3 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
-    -Werror
diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal
index fefde30cf..543a11770 100644
--- a/copilot-language/copilot-language.cabal
+++ b/copilot-language/copilot-language.cabal
@@ -74,7 +74,6 @@ library
                  , Copilot.Language.Error
   ghc-options:
     -Wall
-    -Werror
 
 test-suite unit-tests
   type:
@@ -108,4 +107,3 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
-    -Werror
diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal
index d9a190324..9b17524f4 100644
--- a/copilot-libraries/copilot-libraries.cabal
+++ b/copilot-libraries/copilot-libraries.cabal
@@ -57,7 +57,6 @@ library
 
   ghc-options:
     -Wall
-    -Werror
 
 test-suite unit-tests
   type:
@@ -89,4 +88,3 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
-    -Werror
diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal
index 4f6b1b86d..055522f8c 100644
--- a/copilot-prettyprinter/copilot-prettyprinter.cabal
+++ b/copilot-prettyprinter/copilot-prettyprinter.cabal
@@ -39,7 +39,6 @@ library
 
   ghc-options:
     -Wall
-    -Werror
 
   build-depends:
     base   >= 4.9 && < 5,
diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal
index 1411c8f81..26be51298 100644
--- a/copilot-theorem/copilot-theorem.cabal
+++ b/copilot-theorem/copilot-theorem.cabal
@@ -41,7 +41,6 @@ library
 
   ghc-options             : -Wall
                             -freduction-depth=100
-                            -Werror
 
   build-depends           : base                  >= 4.9 && < 5
                           , bimap                 (>= 0.3 && < 0.4) || (>= 0.5 && < 0.6)
@@ -134,4 +133,3 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
-    -Werror
diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal
index d3a689726..6afd9070a 100644
--- a/copilot-visualizer/copilot-visualizer.cabal
+++ b/copilot-visualizer/copilot-visualizer.cabal
@@ -54,7 +54,6 @@ library
 
   ghc-options:
     -Wall
-    -Werror
 
   build-depends:
     base       >= 4.9     && < 5,
@@ -118,7 +117,6 @@ executable tikz-example
 
   ghc-options:
     -Wall
-    -Werror
 
   build-depends:
     base               >= 4.9 && < 5,
diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal
index f5a18e6c9..c9f2e7f30 100644
--- a/copilot/copilot.cabal
+++ b/copilot/copilot.cabal
@@ -45,7 +45,6 @@ library
     default-language:  Haskell2010
     ghc-options:
       -Wall
-      -Werror
     build-depends:
                        base                  >= 4.9  && < 5
                      , optparse-applicative  >= 0.14 && < 0.19

From fc5db3725fd36cbe290f60a22f3e52b4e82496ff Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Mon, 17 Nov 2025 14:13:27 +0300
Subject: [PATCH 09/20] warn import Semigroup till 4.13

---
 copilot/src/Language/Copilot/Main.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/copilot/src/Language/Copilot/Main.hs b/copilot/src/Language/Copilot/Main.hs
index b03b82ada..5fb4686aa 100644
--- a/copilot/src/Language/Copilot/Main.hs
+++ b/copilot/src/Language/Copilot/Main.hs
@@ -10,7 +10,7 @@ import Copilot.Language (Spec)
 import qualified Copilot.PrettyPrint as PP
 
 import Options.Applicative
-#if MIN_VERSION_base(4,19,0)
+#if MIN_VERSION_base(4,13,0)
 #else
 import Data.Semigroup ((<>))
 #endif

From 8a8a0b174e5f691a36a9ad69fc088c8a1ba382c6 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 17:59:51 +0300
Subject: [PATCH 10/20] warn mitigate prime shift in core

---
 copilot-core/src/Copilot/Core/Type.hs              | 2 +-
 copilot-core/src/Copilot/Core/Type/Array.hs        | 2 +-
 copilot-core/tests/Test/Copilot/Core/Type/Array.hs | 8 ++++----
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs
index 8633cc5fa..ad7afe4f2 100644
--- a/copilot-core/src/Copilot/Core/Type.hs
+++ b/copilot-core/src/Copilot/Core/Type.hs
@@ -291,7 +291,7 @@ instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
   typeOf               = Array typeOf
   simpleType t         = case t of
     Array t' -> SArray t'
-    o -> error $ "There is a bug in the type checker " ++ show o
+    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 1b71d6dbd..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)
diff --git a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs
index 7cf23c59f..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

From 4c1e5b51afeec8f3bb286f2ae594caa55634fd1f Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 18:12:29 +0300
Subject: [PATCH 11/20] warn stylish core Type.hs

---
 copilot-core/src/Copilot/Core/Type.hs | 28 +++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs
index ad7afe4f2..b91d7e79e 100644
--- a/copilot-core/src/Copilot/Core/Type.hs
+++ b/copilot-core/src/Copilot/Core/Type.hs
@@ -46,22 +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 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       (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.

From 0308c1db5c000b3be77b9652da6391322507bd8b Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 18:19:29 +0300
Subject: [PATCH 12/20] warn wrap long line

---
 copilot-core/tests/Test/Copilot/Core/Type.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs
index 9c7ca9327..bb202e5d1 100644
--- a/copilot-core/tests/Test/Copilot/Core/Type.hs
+++ b/copilot-core/tests/Test/Copilot/Core/Type.hs
@@ -135,7 +135,10 @@ testSimpleTypesEqualityTransitive =
 -- | Test that each type is only equal to itself.
 testSimpleTypesEqualityUniqueness :: Property
 testSimpleTypesEqualityUniqueness =
-  forAllBlind (shuffle simpleTypes) $ \x -> case x of [] -> False; (t:ts) ->  notElem t ts
+  forAllBlind (shuffle simpleTypes) $
+    \x -> case x of
+      []     -> False
+      (t:ts) -> notElem t ts
 
 -- | Simple types tested.
 simpleTypes :: [SimpleType]

From 664260af8e0a66889a516296aee3ef3634d9d497 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 18:25:35 +0300
Subject: [PATCH 13/20] warn prime align c99

---
 copilot-c99/src/Copilot/Compile/C99/Expr.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/copilot-c99/src/Copilot/Compile/C99/Expr.hs b/copilot-c99/src/Copilot/Compile/C99/Expr.hs
index 05478dea1..d6d459611 100644
--- a/copilot-c99/src/Copilot/Compile/C99/Expr.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/Expr.hs
@@ -117,7 +117,7 @@ transExpr (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"
 
@@ -126,10 +126,10 @@ transExpr (Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do
 
   -- 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))
 

From a52c577a2b5f3b3b352649ceb765196c4cdbf464 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 18:50:41 +0300
Subject: [PATCH 14/20] warn review issues of interpreter

---
 .../src/Copilot/Interpret/Eval.hs              | 18 +++++++-----------
 .../src/Copilot/Interpret/Render.hs            |  4 ++--
 .../tests/Test/Copilot/Interpret/Eval.hs       |  7 ++++---
 3 files changed, 13 insertions(+), 16 deletions(-)

diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
index 68fe751e0..c03c92052 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs
+++ b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
@@ -141,15 +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                        ->
+  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 _t1 _ name e1 e2              ->
+      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
@@ -269,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
-                } =
+initStrm Stream { streamId = id, streamBuffer = buffer } =
   (id, toDyn (reverse buffer))
 
 -- | Evaluate several streams for a number of steps, producing the environment
@@ -293,9 +291,7 @@ evalStreams top specStrms initStrms =
     evalStreams_ (k+1) $! strms_
     where
     strms_ = map evalStream specStrms
-    evalStream Stream { streamId       = id
-                      , streamExpr     = e
-                      } =
+    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
diff --git a/copilot-interpreter/src/Copilot/Interpret/Render.hs b/copilot-interpreter/src/Copilot/Interpret/Render.hs
index 5baef97f3..fe0c33f7c 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Render.hs
+++ b/copilot-interpreter/src/Copilot/Interpret/Render.hs
@@ -69,7 +69,7 @@ step ExecTrace
   where
 
   ppTriggerOutputs :: [Doc]
-  ppTriggerOutputs = mapMaybe ppTriggerOutput $ trigs
+  ppTriggerOutputs = mapMaybe ppTriggerOutput trigs
 
   ppTriggerOutput :: (String, [Maybe [Output]]) -> Maybe Doc
   ppTriggerOutput (cs, Just xs : _) = Just $
@@ -107,7 +107,7 @@ 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 d52535832..1e75e212a 100644
--- a/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
+++ b/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
@@ -35,7 +35,7 @@ import Copilot.PrettyPrint      (ppExpr)
 
 -- Internal imports: auxiliary functions
 import Test.Extra (apply1, apply2, apply3)
-import Text.Read (readEither)
+import Text.Read  (readEither)
 
 -- * Constants
 
@@ -787,7 +787,8 @@ lookupWithDefault k def = fromMaybe def . lookup k
 
 -- | Show Copilot Core type.
 showType :: Type a -> String
-showType t' = case t' of
+showType t =
+  case t of
     Bool   -> "Bool"
     Int8   -> "Int8"
     Int16  -> "Int16"
@@ -799,5 +800,5 @@ showType t' = case t' of
     Word64 -> "Word64"
     Float  -> "Float"
     Double -> "Double"
-    Array t -> "Array " ++ showType t
+    Array t' -> "Array " ++ showType t'
     Struct _ -> "Struct"

From 89863b9d5e9e0b94686a5e20ca36d32f75265003 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 19:05:49 +0300
Subject: [PATCH 15/20] warn language - align and fail/error

---
 copilot-language/src/Copilot/Language/Analyze.hs | 2 +-
 copilot-language/src/Copilot/Language/Reify.hs   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/copilot-language/src/Copilot/Language/Analyze.hs b/copilot-language/src/Copilot/Language/Analyze.hs
index 82d6a17e9..a39d4b2c6 100644
--- a/copilot-language/src/Copilot/Language/Analyze.hs
+++ b/copilot-language/src/Copilot/Language/Analyze.hs
@@ -264,7 +264,7 @@ analyzeExts ExternEnv { externVarEnv  = vars
     foldM_ ( \(name, c0) (_, c1) -> check name c0 c1)
            grpHead
            grp
-  foldCheck _ [] = fail "Dead code executed"
+  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 547bb1844..1d1298f41 100644
--- a/copilot-language/src/Copilot/Language/Reify.hs
+++ b/copilot-language/src/Copilot/Language/Reify.hs
@@ -214,7 +214,7 @@ mkStream refMkId refStreams refMap e0 = do
   dstn <- makeDynStableName e0
   (buf, e) <- case e0 of
     Append buf _ e -> pure (buf, e)
-    o -> fail $ "Expected Append but got " ++ show o
+    o              -> fail $ "Expected Append but got " ++ show o
   mk <- haveVisited dstn
   case mk of
     Just id_ -> return id_

From e1d0d553acb3e420e268a70b7d5755d92ebc18a5 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 19:09:41 +0300
Subject: [PATCH 16/20] warn revert paretheses in libraries

---
 copilot-libraries/src/Copilot/Library/MTL.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/copilot-libraries/src/Copilot/Library/MTL.hs b/copilot-libraries/src/Copilot/Library/MTL.hs
index 65efd9629..70e0c2970 100644
--- a/copilot-libraries/src/Copilot/Library/MTL.hs
+++ b/copilot-libraries/src/Copilot/Library/MTL.hs
@@ -32,8 +32,8 @@ 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
   where
-  mins = clk + constant l
-  maxes = clk + constant u
+  mins = clk + (constant l)
+  maxes = clk + (constant u)
   res _ _ 0 = false
   res c s k =
     c <= maxes && ((mins <= c && s) || nextRes c s k)
@@ -47,8 +47,8 @@ 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
   where
-  mins = clk - constant u
-  maxes = clk - constant l
+  mins = clk - (constant u)
+  maxes = clk - (constant l)
   res _ _ 0 = false
   res c s k =
     mins <= c && ((c <= maxes && s) || nextRes c s k)

From 496382d1cdc4b7e63f37519f21a69377569ea76e Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 19:14:06 +0300
Subject: [PATCH 17/20] warn prettyprinter review issues

---
 copilot-prettyprinter/copilot-prettyprinter.cabal     | 1 +
 copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs | 8 +++++---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal
index 055522f8c..0f413f63d 100644
--- a/copilot-prettyprinter/copilot-prettyprinter.cabal
+++ b/copilot-prettyprinter/copilot-prettyprinter.cabal
@@ -39,6 +39,7 @@ library
 
   ghc-options:
     -Wall
+    -fno-warn-orphans
 
   build-depends:
     base   >= 4.9 && < 5,
diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
index 22174ffe2..f679ebce2 100644
--- a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
+++ b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
@@ -37,7 +37,8 @@ showWithType showT t x =
 
 -- | Show Copilot Core type.
 showType :: Type a -> String
-showType t' = case t' of
+showType t =
+  case t of
     Bool   -> "Bool"
     Int8   -> "Int8"
     Int16  -> "Int16"
@@ -49,7 +50,7 @@ showType t' = case t' of
     Word64 -> "Word64"
     Float  -> "Float"
     Double -> "Double"
-    Array t -> "Array " ++ showType t
+    Array p -> "Array " ++ showType p
     Struct _ -> "Struct"
 
 -- * Auxiliary show instance
@@ -59,7 +60,8 @@ data ShowWit a = Show a => ShowWit
 
 -- | Turn a type into a show witness.
 showWit :: Type a -> ShowWit a
-showWit t = case t of
+showWit t =
+  case t of
     Bool   -> ShowWit
     Int8   -> ShowWit
     Int16  -> ShowWit

From 898b27a7763d900c8ca62df4f301d1f4cbb52c45 Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 20:15:31 +0300
Subject: [PATCH 18/20] warn theorem review issues

---
 .../src/Copilot/Theorem/IL/PrettyPrint.hs     |  2 +-
 .../src/Copilot/Theorem/IL/Transform.hs       |  8 +-
 .../src/Copilot/Theorem/IL/Translate.hs       | 66 +++++++-------
 .../src/Copilot/Theorem/Kind2/Prover.hs       |  3 +-
 .../src/Copilot/Theorem/Kind2/Translate.hs    |  3 +-
 .../src/Copilot/Theorem/Misc/Utils.hs         |  1 -
 .../src/Copilot/Theorem/Prover/SMTLib.hs      | 12 +--
 .../src/Copilot/Theorem/Prover/TPTP.hs        |  3 +-
 .../src/Copilot/Theorem/TransSys/Operators.hs | 30 +++----
 .../Copilot/Theorem/TransSys/PrettyPrint.hs   |  3 +-
 .../src/Copilot/Theorem/TransSys/Transform.hs |  4 +-
 .../src/Copilot/Theorem/TransSys/Translate.hs | 33 ++++---
 copilot-theorem/src/Copilot/Theorem/What4.hs  |  2 +-
 .../src/Copilot/Theorem/What4/Translate.hs    | 85 ++++++++++---------
 14 files changed, 127 insertions(+), 128 deletions(-)

diff --git a/copilot-theorem/src/Copilot/Theorem/IL/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/IL/PrettyPrint.hs
index 53289bea0..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 ((<>), id)
+import Prelude hiding (id, (<>))
 
 -- | Pretty print an IL specification.
 prettyPrint :: IL -> String
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs b/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
index ccb5996c4..09ebaf572 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
@@ -4,11 +4,9 @@
 -- | Simplify IL expressions by partly evaluating operations on booleans.
 module Copilot.Theorem.IL.Transform ( bsimpl ) where
 
-import safe Copilot.Theorem.IL.Spec
-    ( Expr(FunApp, Ite, Op1, ConstB, Op2),
-      Type(Bool),
-      Op1(Not),
-      Op2(Eq, Or, And) )
+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 b5a44c9b6..c11f6db31 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
@@ -1,10 +1,10 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE NamedFieldPuns      #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE Safe                #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE CPP #-}
 
 -- | Translate Copilot specifications into IL specifications.
 module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where
@@ -82,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
@@ -141,24 +141,24 @@ expr (C.ExternVar t name _) = bound s t >> return s
   where
     s = SVal (trType t) (ncExternVar name) _n_
 
-expr (C.Op1 (C.Sign ta') e') = case ta' of
-  C.Int8   -> trSign ta' e'
-  C.Int16  -> trSign ta' e'
-  C.Int32  -> trSign ta' e'
-  C.Int64  -> trSign ta' e'
-  C.Float  -> trSign ta' e'
-  C.Double -> trSign ta' e'
-  _        -> expr $ C.Const ta' 1
+expr (C.Op1 (C.Sign ta) e) = case ta of
+  C.Int8   -> trSign ta e
+  C.Int16  -> trSign ta e
+  C.Int32  -> trSign ta e
+  C.Int64  -> trSign ta e
+  C.Float  -> trSign ta e
+  C.Double -> trSign ta e
+  _        -> 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)
@@ -191,28 +191,28 @@ expr (C.Op3 (C.Mux t) cond e1 e2) = do
 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
+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 -> error $ "There is bug in the type checker" ++ show 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'
+      | 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
@@ -285,7 +285,7 @@ trType = \case
   C.Word64 -> BV64
   C.Float  -> Real
   C.Double -> Real
-  _o       -> error "THere is a bug in the type checker"
+  _        -> error "THere is a bug in the type checker"
 
 -- | Translation state.
 data TransST = TransST
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
index 6181b573f..3553847ed 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
@@ -53,7 +53,8 @@ kind2Prover opts = Prover
   , closeProver  = const $ return () }
 
 kind2Prog :: String
-kind2Prog        = "kind2"
+kind2Prog = "kind2"
+
 kind2BaseOptions :: [String]
 kind2BaseOptions = ["--input-format", "native", "-xml"]
 
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
index 0732eb52a..7fdaf3354 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
@@ -98,8 +98,7 @@ addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) =
       in pred { K.predInit = init', K.predTrans = trans' }
 
     vars =
-      let
-          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/Utils.hs b/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
index 078f2dc8a..f61801788 100644
--- a/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
@@ -31,7 +31,6 @@ isSublistOf = Set.isSubsetOf `on` Set.fromList
 nubEq :: Ord a => [a] -> [a] -> Bool
 nubEq = (==) `on` Set.fromList
 
-
 -- | Remove duplicates from a list.
 --
 -- This is an efficient version of 'Data.List.nub' that works for lists with a
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs b/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs
index 911b8f3c3..be2c5ca64 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/SMTLib.hs
@@ -8,15 +8,9 @@ module Copilot.Theorem.Prover.SMTLib (SmtLib, interpret) where
 
 import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))
 
-import safe Copilot.Theorem.IL.Spec
-    ( Expr(..),
-      Type(Real, Bool),
-      Op1(Acosh, Not, Neg, Abs, Exp, Sqrt, Log, Sin, Tan, Cos, Asin,
-          Atan, Acos, Sinh, Tanh, Cosh, Asinh, Atanh),
-      Op2(Pow, Eq, Le, Lt, Ge, Gt, And, Or, Add, Sub, Mul, Mod, Fdiv),
-      SeqIndex(Var, Fixed) )
-import safe Copilot.Theorem.Misc.SExpr
-    ( SExpr, blank, atom, singleton, list, node )
+import Copilot.Theorem.IL.Spec hiding (args)
+import Copilot.Theorem.Misc.SExpr
+
 
 import Text.Printf
 
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs b/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
index 90f79b2db..f35f9654c 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
@@ -7,8 +7,7 @@
 module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where
 
 import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))
-import safe Copilot.Theorem.IL
-    ( Expr(..), Op1(..), Op2(..), SeqIndex(Var, Fixed) )
+import Copilot.Theorem.IL hiding (args)
 
 import Data.List
 
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
index 2e2f7af87..87509270d 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
@@ -135,7 +135,7 @@ handleOp1 ::
 
   -> m (expr resT)
 
-handleOp1 resT (op', e) handleExpr notHandledF mkOp = case op' of
+handleOp1 resT (op, e) handleExpr notHandledF mkOp = case op of
 
   C.Not      -> boolOp Not (handleExpr Bool e)
 
@@ -172,12 +172,12 @@ handleOp1 resT (op', e) handleExpr notHandledF mkOp = case op' of
 
   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)
@@ -222,7 +222,7 @@ handleOp2 ::
 
   -> m (expr resT)
 
-handleOp2 resT (op', e1, e2) handleExpr notHandledF mkOp notOp = case op' of
+handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of
 
   C.And        -> boolConnector And
   C.Or         -> boolConnector Or
@@ -267,15 +267,15 @@ handleOp2 resT (op', e1, e2) handleExpr notHandledF mkOp notOp = case op' of
   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
@@ -291,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 f42981130..487b4ac3b 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
@@ -15,7 +15,8 @@ import qualified Data.Bimap as Bimap
 import Prelude hiding ((<>))
 
 indent :: Doc -> Doc
-indent     = nest 4
+indent = nest 4
+
 emptyLine :: Doc
 emptyLine  = text ""
 
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
index 18cf4a9fb..fc4765281 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
@@ -208,8 +208,10 @@ removeCycles spec =
     buildScc nrep ns =
      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"
+    acycN Graph.CyclicSCC {}   = error "Cyclic graph is not handled"
+
     topoSort s = s { specNodes =
       map acycN $ buildScc id (specNodes s) }
 
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
index 2b8dc1ca8..70aa6ccbe 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
@@ -63,22 +63,27 @@ import Data.Bimap (Bimap)
 import qualified Copilot.Core as C
 import qualified Data.Map     as Map
 import qualified Data.Bimap   as Bimap
-import Prelude hiding (id)
+
 -- Naming conventions
 -- These are important in order to avoid name conflicts
 
 ncSep :: String
-ncSep         = "."
+ncSep = "."
+
 ncMain :: String
-ncMain        = "out"
+ncMain = "out"
+
 ncNode :: Show a => a -> [Char]
-ncNode i      = "s" ++ show i
+ncNode i = "s" ++ show i
+
 ncPropNode :: [Char] -> [Char]
-ncPropNode s  = "prop-" ++ s
+ncPropNode s = "prop-" ++ s
+
 ncTopNode :: String
-ncTopNode     = "top"
+ncTopNode = "top"
+
 ncLocal :: [Char] -> [Char]
-ncLocal s     = "l" ++ dropWhile (not . isNumber) s
+ncLocal s = "l" ++ dropWhile (not . isNumber) s
 
 ncExternVarNode :: [Char] -> [Char]
 ncExternVarNode name = "ext-" ++ name
@@ -195,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
@@ -207,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
@@ -317,5 +322,5 @@ curNode :: StateT TransSt Data.Functor.Identity.Identity NodeId
 curNode = _curNode <$> get
 
 newExtVarNode :: MonadState TransSt m => NodeId -> U Type -> m ()
-newExtVarNode id t =
-  modify $ \st -> st { _extVarsNodes = (id, t) : _extVarsNodes st }
+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 f91fdde8b..0eca06577 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4.hs
@@ -79,7 +79,7 @@ import Data.Parameterized.Some
 import qualified Data.Parameterized.Vector as V
 import GHC.Float (castWord32ToFloat, castWord64ToDouble)
 import LibBF (BigFloat, bfToDouble, pattern NearEven)
-import qualified Panic
+import qualified Panic as Panic
 
 import Copilot.Theorem.What4.Translate
 
diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
index 6d04870a2..a36d0d26d 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
@@ -64,8 +64,9 @@ import           Data.Type.Equality             (TestEquality (..), (:~:) (..))
 import           Data.Word                      (Word32)
 import           GHC.TypeLits                   (KnownSymbol)
 import           GHC.TypeNats                   (KnownNat, type (<=), type (+))
-import qualified Panic
-import Prelude hiding (pred, recip, id)
+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
@@ -463,78 +464,78 @@ translateOp1 :: forall sym a b .
              -> CE.Op1 a b
              -> XExpr sym
              -> TransM sym (XExpr sym)
-translateOp1 sym origExpr op' xe' = case (op', xe') of
+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.Not, _) -> panic ["Expected bool", show 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
@@ -557,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
@@ -580,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
@@ -609,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
@@ -623,7 +624,7 @@ translateOp1 sym origExpr op' xe' = case (op', xe') of
       _ -> unexpectedValue "numOp"
 
     bvOp' :: (forall w . BVOp1 sym w) -> XExpr sym -> IO (XExpr sym)
-    bvOp' f xe = case xe of
+    bvOp' f xe' = case xe' of
       XInt8 e -> XInt8 <$> f e
       XInt16 e -> XInt16 <$> f e
       XInt32 e -> XInt32 <$> f e
@@ -635,7 +636,7 @@ translateOp1 sym origExpr op' xe' = case (op', xe') of
       _ -> unexpectedValue "bvOp"
 
     fpOp' :: (forall fi . FPOp1 sym fi) -> XExpr sym -> IO (XExpr sym)
-    fpOp' g xe = case xe of
+    fpOp' g xe' = case xe' of
       XFloat e -> XFloat <$> g WFP.SingleFloatRepr e
       XDouble e -> XDouble <$> g WFP.DoubleFloatRepr e
       _ -> unexpectedValue "fpOp"
@@ -663,9 +664,9 @@ 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)
-            , show xe'
+    unexpectedValue op' =
+      panic [ "Unexpected value in " ++ op' ++ ": " ++ show (CP.ppExpr origExpr)
+            , show xe
             ]
 
 type BVOp2 sym w =

From ec6960a522e016098f6c704f612a99b5c3538adb Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 20:18:39 +0300
Subject: [PATCH 19/20] warn revert no orphan flag in just copilot

---
 copilot/copilot.cabal | 1 +
 1 file changed, 1 insertion(+)

diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal
index c9f2e7f30..f52eecc4e 100644
--- a/copilot/copilot.cabal
+++ b/copilot/copilot.cabal
@@ -45,6 +45,7 @@ library
     default-language:  Haskell2010
     ghc-options:
       -Wall
+      -fno-warn-orphans
     build-depends:
                        base                  >= 4.9  && < 5
                      , optparse-applicative  >= 0.14 && < 0.19

From e2e92e561408b28c8ec673ff97578c4337cffd3e Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Tue, 18 Nov 2025 20:38:19 +0300
Subject: [PATCH 20/20] warn missed theorem

---
 copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs
index 8e8aabbc3..6348008f7 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Renaming.hs
@@ -22,7 +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)
+import           GHC.Stack (HasCallStack)
 
 -- | A monad capable of keeping track of variable renames and of providing
 -- fresh names for variables.