diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,14 @@
+## 1.0 (August 29, 2019)
+
+* Update to new fortran-src version 0.4.0.
+* New command: basic-checks, which runs a series of other checks in Simple.hs.
+* Add max-lines threshold for snippets output, currently 5.
+* Rename units-compile to units-summarise/summarize.
+* Bring over same command-line flexibility to units-compile as 'fortran-src -c', can specify multiple files-or-directories.
+* Use ModGraph functionality to allow units-summarise to build dependency graphs and summarise in build-order.
+* Search includedir recursively for mod-files, like fortran-src.
+* Numerous changes to increase strictness and reduce memory usage: use Pipes, avoid constructing needlessly large graphs.
+
 ## 0.906 (June 13, 2019)
 
 * Update to new fortran-src version 0.3.0.
diff --git a/camfort.cabal b/camfort.cabal
--- a/camfort.cabal
+++ b/camfort.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.31.1.
+-- This file has been generated from package.yaml by hpack version 0.31.2.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: d90f27e0fcefd6d71f89123fef96fef2ec2cb33a5f7c7c99da877dd1734efa95
+-- hash: 2a8d91415419eaf0c7d1532effdda9c5b02165f03a0eac6a02562949c3765671
 
 name:           camfort
-version:        0.906
+version:        1.0
 synopsis:       CamFort - Cambridge Fortran infrastructure
 description:    CamFort is a tool for the analysis, transformation, verification of Fortran code.
 category:       Language
@@ -50,6 +50,7 @@
     tests/fixtures/Specification/Stencils/example8.f
     tests/fixtures/Specification/Stencils/example9.expected.f
     tests/fixtures/Specification/Stencils/example9.f
+    tests/fixtures/Specification/Units/complexity0.f90
     tests/fixtures/Specification/Units/do-loop1.f90
     tests/fixtures/Specification/Units/do-loop2.f90
     tests/fixtures/Specification/Units/eapVarApp.f90
@@ -78,6 +79,7 @@
     tests/fixtures/Specification/Units/literal-nonzero-inconsist5.f90
     tests/fixtures/Specification/Units/literal-nonzero.f90
     tests/fixtures/Specification/Units/literal-nonzero2.f90
+    tests/fixtures/Specification/Units/literal-prop.f90
     tests/fixtures/Specification/Units/literal-zero.f90
     tests/fixtures/Specification/Units/param.f90
     tests/fixtures/Specification/Units/recursive1.f90
@@ -180,9 +182,6 @@
       src
   extra-libraries:
       flint
-  build-tools:
-      alex ==3.2.*
-    , happy ==1.19.*
   build-depends:
       GenericPretty >=1.2.2 && <1.3
     , array >=0.4 && <0.6
@@ -190,20 +189,22 @@
     , binary >=0.8.3.0 && <0.9
     , bytestring >=0.10 && <0.11
     , containers >=0.5.0.0 && <0.7
+    , deepseq
     , directory >=1.2 && <1.4
     , fgl >=5.6 && <5.8
     , filepath >=1.4 && <1.5
-    , fortran-src >=0.3 && <0.4
+    , fortran-src >=0.4 && <0.5
     , ghc-prim >=0.3.1.0 && <0.6
-    , hmatrix >=0.15 && <0.20
-    , lattices >=1.7.1 && <1.8
+    , hmatrix >=0.20 && <0.21
+    , lattices >=2.0.0 && <2.1
     , lens >=4.15.1 && <5
     , matrix >=0.2.2 && <0.4
     , mmorph >=1.0.9 && <2
     , mtl >=2.1 && <2.3
     , parallel
+    , pipes
     , pretty >=1.1 && <2
-    , sbv >=7.0 && <8
+    , sbv >=8.0 && <9
     , singletons >=2.2 && <3
     , strict >=0.3.2 && <1
     , syb >=0.4 && <0.8
@@ -213,11 +214,11 @@
     , transformers >=0.5.5.0 && <0.6
     , uniplate >=1.6.10 && <1.7
     , vector >=0.1 && <0.13
-    , verifiable-expressions >=0.4
+    , verifiable-expressions >=0.6.0 && <0.7.0
     , vinyl >=0.6 && <1.0
-    , writer-cps-morph >=0.1.0.2
-    , writer-cps-mtl >=0.1.1.5
-    , writer-cps-transformers >=0.1.1.2
+  build-tools:
+      alex ==3.2.*
+    , happy ==1.19.*
   default-language: Haskell2010
 
 executable camfort
@@ -227,8 +228,8 @@
       base >=4.6 && <5
     , camfort
     , directory >=1.2 && <2
-    , fortran-src >=0.3 && <0.4
-    , optparse-applicative >=0.14 && <0.15
+    , fortran-src >=0.4 && <0.5
+    , optparse-applicative >=0.14 && <0.16
   default-language: Haskell2010
 
 test-suite spec
@@ -261,8 +262,6 @@
       Paths_camfort
   hs-source-dirs:
       tests
-  build-tool-depends:
-      hspec-discover:hspec-discover
   build-depends:
       QuickCheck >=2.8 && <3
     , array >=0.4 && <0.6
@@ -274,17 +273,19 @@
     , directory >=1.2 && <2
     , fgl >=5.6 && <5.8
     , filepath >=1.4 && <1.5
-    , fortran-src >=0.3 && <0.4
-    , hmatrix >=0.15 && <0.20
+    , fortran-src >=0.4 && <0.5
+    , hmatrix >=0.20 && <0.21
     , hspec >=2.2 && <3
-    , lattices >=1.7.1 && <1.8
+    , lattices >=2.0.0 && <2.1
     , lens >=4.15.1 && <5
     , mtl >=2.1 && <2.3
-    , sbv >=7.0 && <8
+    , sbv >=8.0 && <9
     , silently ==1.2.*
     , temporary >=1.2.0.4 && <1.4
     , text >=0.11.2.3 && <1.3
     , time
     , uniplate >=1.6.10 && <1.7
-    , verifiable-expressions >=0.4
+    , verifiable-expressions >=0.6.0 && <0.7.0
+  build-tool-depends:
+      hspec-discover:hspec-discover
   default-language: Haskell2010
diff --git a/src/Camfort/Analysis.hs b/src/Camfort/Analysis.hs
--- a/src/Camfort/Analysis.hs
+++ b/src/Camfort/Analysis.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DefaultSignatures          #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE FlexibleContexts           #-}
@@ -90,13 +91,13 @@
 import           Control.Monad.Except
 import           Control.Monad.Morph
 import           Control.Monad.Reader
-import qualified Control.Monad.RWS              as Lazy
-import           Control.Monad.RWS.CPS
+import           Control.Monad.RWS
 import qualified Control.Monad.State            as Lazy
 import           Control.Monad.State.Strict
-import qualified Control.Monad.Writer           as Lazy
-import           Control.Monad.Writer.CPS
+import           Control.Monad.Writer
 import           Control.Monad.Fail
+import           Control.DeepSeq
+import           GHC.Generics                   (Generic)
 
 import           Control.Lens
 
@@ -191,9 +192,7 @@
 instance MonadAnalysis e w m => MonadAnalysis e w (StateT s m)
 instance (MonadAnalysis e w m, Monoid w') => MonadAnalysis e w (WriterT w' m)
 instance MonadAnalysis e w m => MonadAnalysis e w (Lazy.StateT s m)
-instance (MonadAnalysis e w m, Monoid w') => MonadAnalysis e w (Lazy.WriterT w' m)
 instance (MonadAnalysis e w m, Monoid w') => MonadAnalysis e w (RWST r w' s m)
-instance (MonadAnalysis e w m, Monoid w') => MonadAnalysis e w (Lazy.RWST r w' s m)
 
 --------------------------------------------------------------------------------
 --  Combinators
@@ -258,10 +257,12 @@
 data AnalysisResult e r
   = ARFailure Origin e
   | ARSuccess r
-  deriving (Show, Eq, Functor)
+  deriving (Show, Eq, Functor, Generic)
 
 makePrisms ''AnalysisResult
 
+instance (NFData e, NFData r) => NFData (AnalysisResult e r)
+
 -- | When an analysis is run, it produces a report consisting of the logs it
 -- collect as it ran. In addition, it either fails at a certain location or
 -- succeeds with a result value.
@@ -271,10 +272,12 @@
   , _arMessages   :: ![SomeMessage e w]
   , _arResult     :: !(AnalysisResult e r)
   }
-  deriving (Show, Eq, Functor)
+  deriving (Show, Eq, Functor, Generic)
 
 makeLenses ''AnalysisReport
 
+instance (NFData e, NFData w, NFData r) => NFData (AnalysisReport e w r)
+
 -- | Produce a human-readable version of an 'AnalysisReport', at the given
 -- verbosity level. Giving 'Nothing' for the log level hides all logs.
 describeReport
@@ -341,6 +344,7 @@
 -- Insert snippets of code where source spans are referenced.
 insertSnippets :: MonadIO m => Lazy.Text -> m Lazy.Text
 insertSnippets output = do
+  let maxLines = 5
   let findLines n cnt str
         | n > 0, ls <- Lazy.lines str, ls'@(_:_) <- drop (n-1) ls = Just (take cnt ls')
         | otherwise                                               = Nothing
@@ -348,7 +352,10 @@
         | Just (ParsedOrigin fn (l1, _) (l2, _)) <- parseOrigin (Lazy.unpack l) = do
             f <- liftIO $ Lazy.readFile fn
             case findLines l1 (l2 - l1 + 1) f of
-              Just fLines -> return $ [l, Lazy.empty] ++ fLines ++ [Lazy.empty]
+              Just fLines -> do
+                let fLines' | null (drop maxLines fLines) = fLines
+                            | otherwise = take maxLines fLines ++ ["[...]"]
+                return $ [l, Lazy.empty] ++ fLines' ++ [Lazy.empty]
               Nothing     -> return [l]
         | otherwise = return [l]
   Lazy.unlines <$> concat <$> mapM doLine (Lazy.lines output)
diff --git a/src/Camfort/Analysis/Logger.hs b/src/Camfort/Analysis/Logger.hs
--- a/src/Camfort/Analysis/Logger.hs
+++ b/src/Camfort/Analysis/Logger.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DefaultSignatures          #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveTraversable          #-}
+{-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE FunctionalDependencies     #-}
@@ -80,20 +81,16 @@
 import qualified Data.Semigroup                 as SG
 import           Data.Void                      (Void)
 
+import           Control.DeepSeq
 import           Control.Lens
 
 import           Control.Monad.Except
 import           Control.Monad.Morph
 import           Control.Monad.Reader
-import qualified Control.Monad.RWS              as Lazy
-import           Control.Monad.RWS.CPS
-import           Control.Monad.Trans.RWS.CPS.Morph ()
-import           Control.Monad.Trans.RWS.CPS.Internal (RWST(..))
+import           Control.Monad.RWS
 import qualified Control.Monad.State            as Lazy
 import           Control.Monad.State.Strict
-import qualified Control.Monad.Writer           as Lazy
-import           Control.Monad.Writer.CPS
-import           Control.Monad.Trans.Writer.CPS.Morph ()
+import           Control.Monad.Writer
 import           Control.Monad.Fail
 
 import           Data.Text                      (Text)
@@ -102,6 +99,8 @@
 import           Data.Text.Lazy.Builder         (Builder)
 import qualified Data.Text.Lazy.Builder         as Builder
 
+import           GHC.Generics
+
 import           Text.Read                      (readMaybe)
 import qualified Language.Fortran.Util.Position as F
 
@@ -163,10 +162,12 @@
   { _oFile :: FilePath
   , _oSpan :: F.SrcSpan
   }
-  deriving (Show, Eq, Ord)
+  deriving (Show, Eq, Ord, Generic)
 
 makeLenses ''Origin
 
+instance NFData Origin
+
 instance Describe Origin where
   describeBuilder origin =
     "at [" <> Builder.fromString (origin ^. oFile) <>
@@ -221,10 +222,12 @@
   { _lmOrigin :: Maybe Origin
   , _lmMsg    :: a
   }
-  deriving (Show, Eq, Functor, Foldable, Traversable)
+  deriving (Show, Eq, Functor, Foldable, Traversable, Generic)
 
 makeLenses ''LogMessage
 
+instance NFData a => NFData (LogMessage a)
+
 instance Describe a => Describe (LogMessage a) where
   describeBuilder msg =
     maybe "" describeBuilder (msg ^. lmOrigin) <>
@@ -236,10 +239,12 @@
   | MsgWarn (LogMessage w)
   | MsgInfo (LogMessage Text)
   | MsgDebug (LogMessage Text)
-  deriving (Show, Eq)
+  deriving (Show, Eq, Generic)
 
 makePrisms ''SomeMessage
 
+instance (NFData e, NFData w) => NFData (SomeMessage e w)
+
 someMessageOrigin :: Lens' (SomeMessage e w) (Maybe Origin)
 someMessageOrigin =
   lens
@@ -366,9 +371,9 @@
 instance MonadLogger e w m => MonadLogger e w (StateT s m)
 instance (MonadLogger e w m, Monoid w') => MonadLogger e w (WriterT w' m)
 instance MonadLogger e w m => MonadLogger e w (Lazy.StateT s m)
-instance (MonadLogger e w m, Monoid w') => MonadLogger e w (Lazy.WriterT w' m)
+-- instance (MonadLogger e w m, Monoid w') => MonadLogger e w (Lazy.WriterT w' m)
 instance (MonadLogger e w m, Monoid w') => MonadLogger e w (RWST r w' s m)
-instance (MonadLogger e w m, Monoid w') => MonadLogger e w (Lazy.RWST r w' s m)
+-- instance (MonadLogger e w m, Monoid w') => MonadLogger e w (Lazy.RWST r w' s m)
 
 --------------------------------------------------------------------------------
 --  'LoggerT' monad
@@ -426,15 +431,16 @@
 
 instance (MonadReader r m) => MonadReader r (LoggerT e w m) where
   ask = lift ask
-  local f (LoggerT m) | k <- runRWST m = LoggerT $ rwsT $ \e -> local f . k e
+  local f (LoggerT (RWST k)) = LoggerT $ RWST $ \e -> local f . k e
 
 instance (MonadWriter w' m) => MonadWriter w' (LoggerT e w m) where
   tell = lift . tell
-  listen (LoggerT m) | k <- runRWST m = LoggerT $ rwsT $ \e s -> do
+
+  listen (LoggerT (RWST k)) = LoggerT $ RWST $ \e s -> do
     ((x, w, s'), w') <- listen (k e s)
     return ((x, w'), w, s')
 
-  pass (LoggerT m) | k <- runRWST m = LoggerT $ rwsT $ \e s ->
+  pass (LoggerT (RWST k)) = LoggerT $ RWST $ \e s ->
     pass $ (\((x, f), w, s') -> ((x, w, s'), f)) <$> k e s
 
 instance (Monad m, Describe e, Describe w) =>
@@ -451,10 +457,11 @@
 -- the resulting 'LoggerT' cannot output as it goes. It still collects logs to
 -- be inspected when it finishes.
 instance MFunctor (LoggerT e w) where
-  hoist f (LoggerT (RWST k)) = LoggerT ( RWST ( \e s w ->
+  hoist f (LoggerT (RWST k)) = LoggerT $ RWST $ \e s ->
     let e' = hoistEnv (const (return ())) e
-    in f (k e' s w) ) )
+    in f (k e' s)
 
+
 -- | A function to output logs in a particular monad @m@.
 data LogOutput m = LogOutput
   { _loConciseOutput :: Bool
@@ -520,7 +527,7 @@
 -- | Change the error and warning types in a logger computation. To change the
 -- underlying monad use 'hoist'.
 mapLoggerT
-  :: (Monad m)
+  :: (Functor m)
   => (e -> e') -> (w -> w')
   -> LoggerT e w m a -> LoggerT e' w' m a
 mapLoggerT mapErr mapWarn (LoggerT x) = LoggerT (mapRWST mapInner x)
diff --git a/src/Camfort/Analysis/ModFile.hs b/src/Camfort/Analysis/ModFile.hs
--- a/src/Camfort/Analysis/ModFile.hs
+++ b/src/Camfort/Analysis/ModFile.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
 {- |
 Module      :  Camfort.Analysis.ModFile
 Description :  CamFort-specific ModFiles helpers.
@@ -13,8 +14,12 @@
     -- * Getting mod files
     MFCompiler
   , genModFiles
+  , genModFilesP
+--  , genModFilesIO
   , getModFiles
   , readParseSrcDir
+  , readParseSrcDirP
+  , readParseSrcFile
   , simpleCompiler
     -- * Using mod files
   , withCombinedModuleMap
@@ -50,6 +55,11 @@
 import           Camfort.Analysis.Annotations       (A, unitAnnotation)
 import           Camfort.Helpers
 
+import           Pipes
+-- import           Pipes.Core
+import qualified Pipes.Prelude                      as P
+import           Prelude                            hiding (mod)
+
 --------------------------------------------------------------------------------
 --  Getting mod files
 --------------------------------------------------------------------------------
@@ -66,31 +76,86 @@
 genCModFile :: MFCompiler r m -> r -> FM.ModFiles -> F.ProgramFile A -> m FM.ModFile
 genCModFile = id
 
--- | Generate a mode file based on the given mod file compiler
+-- | Generate mod files based on the given mod file compiler
 genModFiles
   :: (MonadIO m)
   => Maybe FortranVersion -> FM.ModFiles -> MFCompiler r m -> r -> FilePath -> [Filename] -> m FM.ModFiles
-genModFiles mv mfs mfc env fp excludes = do
+genModFiles mv mfs mfc opts fp excludes = do
   fortranFiles <- liftIO $ fmap fst <$> readParseSrcDir mv mfs fp excludes
-  traverse (genCModFile mfc env mfs) fortranFiles
+  traverse (genCModFile mfc opts mfs) fortranFiles
 
+-- | Generate mod files based on the given mod file compiler (Pipes version)
+genModFilesP
+  :: forall m r. (MonadIO m)
+  => Maybe FortranVersion -> FM.ModFiles -> MFCompiler r m -> r -> [FilePath] -> Producer' FM.ModFile m ()
+genModFilesP mv mfs mfc opts files = parse >-> compile
+  where
+    compile = P.mapM (genCModFile mfc opts mfs)
+    parse = for (each files) $ \ file -> do
+      mProgSrc <- liftIO $ readParseSrcFile mv mfs file
+      case mProgSrc of
+        Just (pf, _) -> yield pf
+        Nothing -> pure ()
+
+
+-- | Generate mod files based on the given mod file compiler (Pipes version)
+-- (testing 'bi-directional' pipes)
+-- genModFilesP'
+--   :: forall x' x m r. (MonadIO m)
+--   => Maybe FortranVersion -> FM.ModFiles -> MFCompiler r m -> r -> [FilePath] -> [FilePath] -> Proxy x' x () FM.ModFile m ()
+-- genModFilesP' mv mfs mfc opts files incDirs = parse //> compile
+--   where
+--     compile :: F.ProgramFile A -> Proxy x' x () FM.ModFile m FM.ModFile
+--     compile pf = do
+--       mod <- liftIO undefined -- (genCModFile mfc opts mfs pf)
+--       yield mod
+--       -- request mod
+--       pure mod
+
+--     parse :: Proxy x' x (FM.ModFile) (F.ProgramFile A) m ()
+--     parse = loop files
+--       where loop [] = pure ()
+--             loop (f:fs) = do
+--               mProgSrc <- liftIO $ readParseSrcFile mv mfs f
+--               case mProgSrc of
+--                 Just (pf, _) -> do
+--                   _ <- respond pf
+--                   loop fs
+--                 Nothing -> loop fs
+
+-- | Generate mod files based on the given mod file compiler (PipesIO version)
+-- Accumulates mods as it goes.
+-- (testing)
+-- genModFilesIO
+--   :: Maybe FortranVersion -> FM.ModFiles -> MFCompiler r IO -> r -> [FilePath] -> IO FM.ModFiles
+-- genModFilesIO mv mfs mfc opts files = fst <$> P.foldM' f (pure mfs) pure (each files)
+--   where
+--     f :: FM.ModFiles -> Filename -> IO [FM.ModFile]
+--     f mods file = do
+--       mProgSrc <- readParseSrcFile mv mods file
+--       case mProgSrc of
+--         Just (pf, _) -> do
+--           mod <- genCModFile mfc opts mods pf
+--           -- yield mod
+--           pure $ mod:mods
+--         Nothing -> pure mods
+
 -- | Retrieve the ModFiles under a given path.
 getModFiles :: FilePath -> IO FM.ModFiles
 getModFiles dir = do
   -- Figure out the camfort mod files and parse them.
-  modFileNames <- (filter isModFile . map (dir </>)) <$> listDirectory dir
-  mods <- forM modFileNames $ \modFileName -> do
+  modFileNames <- (filter isModFile . map (dir </>)) <$> listDirectoryRecursively dir
+  mods <- fmap concat . forM modFileNames $ \modFileName -> do
     modData <- LB.readFile modFileName
     let eResult = FM.decodeModFile modData
     case eResult of
       Left msg -> do
         putStrLn $ modFileName ++ ": Error: " ++ show msg
-        pure Nothing
-      Right modFile -> do
-        pure . pure $ modFile
-  let mods' = catMaybes mods
-  putStrLn $ "Successfully parsed " ++ show (length mods) ++ " precompiled file(s)."
-  pure mods'
+        pure []
+      Right modFiles -> do
+        pure modFiles
+  putStrLn $ "Successfully parsed " ++ show (length mods) ++ " summary file(s)."
+  pure mods
 
   where
     isModFile :: String -> Bool
@@ -130,6 +195,30 @@
     mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
     mapMaybeM f = fmap catMaybes . mapM f
 
+readParseSrcDirP :: MonadIO m
+                => Maybe FortranVersion
+                -> FM.ModFiles
+                -> FileOrDir
+                -> [Filename]
+                -> Producer' (F.ProgramFile A, SourceText) m ()
+readParseSrcDirP mv mods inp excludes = do
+  isdir <- liftIO $ isDirectory inp
+  files <-
+    if isdir
+    then do
+      files <- liftIO $ getFortranFiles inp
+      -- Compute alternate list of excludes with the
+      -- the directory appended
+      let excludes' = excludes ++ map (\x -> inp </> x) excludes
+      pure $ files \\ excludes'
+    else pure [inp]
+  for (each files) $ \ file -> do
+    mProgSrc <- liftIO $ readParseSrcFile mv mods file
+    case mProgSrc of
+      Just progSrc -> yield progSrc
+      Nothing -> pure ()
+  pure ()
+
 readParseSrcFile :: Maybe FortranVersion -> FM.ModFiles -> Filename -> IO (Maybe (F.ProgramFile A, SourceText))
 readParseSrcFile mv mods f = do
   inp <- flexReadFile f
@@ -169,7 +258,6 @@
   let
     -- Use the module map derived from all of the included Camfort Mod files.
     mmap = FM.combinedModuleMap mfs
-    tenv = FM.combinedTypeEnv mfs
     pfRenamed = FAR.analyseRenamesWithModuleMap mmap $ pf
   in (pfRenamed, mmap `Map.union` FM.extractModuleMap pfRenamed)
 
diff --git a/src/Camfort/Analysis/Simple.hs b/src/Camfort/Analysis/Simple.hs
--- a/src/Camfort/Analysis/Simple.hs
+++ b/src/Camfort/Analysis/Simple.hs
@@ -18,6 +18,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TupleSections #-}
+{-# LANGUAGE DeriveGeneric #-}
 
 {- Simple syntactic analysis on Fortran programs -}
 
@@ -33,10 +34,10 @@
 
 import Prelude hiding (unlines)
 import Control.Monad
-import Control.Arrow (first)
+import Control.DeepSeq
 import Data.Data
 import Data.Function (on)
-import Data.Maybe (catMaybes, fromMaybe, maybeToList, listToMaybe, mapMaybe)
+import Data.Maybe (catMaybes, fromMaybe, listToMaybe, mapMaybe)
 import qualified Data.Set as S
 import qualified Data.IntSet as IS
 import qualified Data.Map.Strict as M
@@ -45,27 +46,28 @@
 import Data.Monoid ((<>))
 import Data.Generics.Uniplate.Operations
 import qualified Data.Text.Lazy.Builder as Builder
-import Data.Text (Text, unlines, intercalate, pack)
-import Data.List ((\\), sort, nub, nubBy, tails)
+import Data.Text (unlines, intercalate, pack)
+import Data.List (sort, nub, nubBy, tails)
+import GHC.Generics
 
 import Data.Graph.Inductive
 
 import qualified Language.Fortran.AST as F
 import qualified Language.Fortran.Util.Position as F
 import qualified Language.Fortran.Analysis as F
-import qualified Language.Fortran.Analysis.Types as F
 import qualified Language.Fortran.Analysis.DataFlow as F
 import qualified Language.Fortran.Analysis.BBlocks as F
 import Language.Fortran.Util.ModFile
 
-import Camfort.Analysis (describeShow, analysisModFiles,  ExitCodeOfReport(..), atSpanned, atSpannedInFile, Origin
+import Camfort.Analysis (analysisModFiles,  ExitCodeOfReport(..), atSpanned, atSpannedInFile, Origin
                         , logError, describe, describeBuilder
                         , PureAnalysis, Describe )
 import Camfort.Analysis.ModFile (withCombinedEnvironment)
 
 {-| Counts the number of declarations (of variables) in a whole program -}
 
-newtype VarCountReport = VarCountReport Int
+newtype VarCountReport = VarCountReport Int deriving Generic
+instance NFData VarCountReport
 instance ExitCodeOfReport VarCountReport where
   exitCodeOf _ = 0
 instance Describe VarCountReport where
@@ -77,7 +79,8 @@
 type PULoc = (F.ProgramUnitName, Origin)
 data ImplicitNoneReport
   = ImplicitNoneReport [PULoc] -- ^ list of program units identified as needing implicit none
-
+  deriving Generic
+instance NFData ImplicitNoneReport
 instance SG.Semigroup ImplicitNoneReport where
   ImplicitNoneReport r1 <> ImplicitNoneReport r2 = ImplicitNoneReport $ r1 ++ r2
 
@@ -104,7 +107,7 @@
      ImplicitNoneReport [(F.Named name, orig)] -> logError orig name
      _ -> return ()
 
-  return $ mconcat checkedPUs
+  return $!! mconcat checkedPUs
 
   where
     isUseStmt (F.BlStatement _ _ _ (F.StUse {})) = True
@@ -148,7 +151,8 @@
 data CheckAllocReport
   = CheckAllocReport { unbalancedAllocs :: [(F.Name, PULoc)]
                      , outOfOrder       :: [(F.Name, PULoc)]}
-
+  deriving Generic
+instance NFData CheckAllocReport
 instance SG.Semigroup CheckAllocReport where
   CheckAllocReport a1 b1 <> CheckAllocReport a2 b2 = CheckAllocReport (a1 ++ a2) (b1 ++ b2)
 
@@ -181,7 +185,7 @@
 
   let reports = map checkPU (universeBi pf)
 
-  return $ mconcat reports
+  return $!! mconcat reports
 
 
 instance Describe CheckAllocReport where
@@ -202,7 +206,8 @@
 
 data CheckFPReport
   = CheckFPReport { badEquality :: [PULoc] }
-
+  deriving Generic
+instance NFData CheckFPReport
 instance SG.Semigroup CheckFPReport where
   CheckFPReport a1 <> CheckFPReport a2 = CheckFPReport (a1 ++ a2)
 
@@ -230,7 +235,7 @@
 
   let reports = map checkPU (universeBi pf'')
 
-  return $ mconcat reports
+  return $!! mconcat reports
 
 floatingPointTypes :: [F.BaseType]
 floatingPointTypes = [F.TypeReal, F.TypeDoubleComplex, F.TypeComplex, F.TypeDoublePrecision]
@@ -254,7 +259,8 @@
                    , duppedOnly  :: [(String, PULoc)]
                    , unusedNames :: [(String, PULoc)]
                    }
-
+  deriving Generic
+instance NFData CheckUseReport
 instance SG.Semigroup CheckUseReport where
   CheckUseReport a1 b1 c1 <> CheckUseReport a2 b2 c2 = CheckUseReport (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
 
@@ -283,14 +289,15 @@
                         , n == n' ]
           extractUseName (F.UseID _ ss (F.ExpValue _ _ (F.ValVariable n)))       = (n, ss)
           extractUseName (F.UseRename _ ss (F.ExpValue _ _ (F.ValVariable n)) _) = (n, ss)
+          extractUseName u = error $ "checkModuleUse: extractUseName: invalid AST: " ++ show (fmap (const ()) u)
           unusedNames = [ (n, (F.getName pu, atSpannedInFile file ss))
                         | F.StUse _ _ _ _ _ (Just (F.AList _ _ uses)) <- statements
                         , (n, ss) <- map extractUseName uses
-                        , length [ () | F.ExpValue _ _ (F.ValVariable n') <- expressions, n == n' ] < 2 ]
+                        , null (drop 1 [ () | F.ExpValue _ _ (F.ValVariable n') <- expressions, n == n' ]) ]
 
   let reports = map checkPU (universeBi pf')
 
-  return $ mconcat reports
+  return $!! mconcat reports
 
 instance Describe CheckUseReport where
   describeBuilder (CheckUseReport {..})
@@ -312,7 +319,8 @@
 
 data CheckArrayReport
   = CheckArrayReport { nestedIdx, missingIdx :: [([String], PULoc)] }
-
+  deriving Generic
+instance NFData CheckArrayReport
 instance SG.Semigroup CheckArrayReport where
   CheckArrayReport a1 b1 <> CheckArrayReport a2 b2 = CheckArrayReport (a1 ++ a2) (b1 ++ b2)
 
@@ -332,7 +340,6 @@
   let pf''        = F.analyseConstExps . F.analyseParameterVars pvm . F.analyseBBlocks $ pf'
   let bm          = F.genBlockMap pf''
   let dm          = F.genDefMap bm
-  let cm          = F.genCallMap pf''
 
   let checkPU :: F.ProgramUnit (F.Analysis a) -> CheckArrayReport
       checkPU pu | F.Analysis { F.bBlocks = Just _ } <- F.getAnnotation pu = CheckArrayReport {..}
@@ -340,9 +347,9 @@
           F.Analysis { F.bBlocks = Just gr } = F.getAnnotation pu
           bedges = F.genBackEdgeMap (F.dominators gr) $ F.bbgrGr gr
           ivmap  = F.genInductionVarMapByASTBlock bedges gr
-          divmap = F.genDerivedInductionMap bedges gr
           rdmap  = F.reachingDefinitions dm gr
-          flFrom = tc . grev $ F.genFlowsToGraph bm dm gr rdmap
+          flTo   = F.genFlowsToGraph bm dm gr rdmap
+          flFrom = grev flTo
 
           blocks :: [F.Block (F.Analysis a)]
           blocks = F.programUnitBody pu
@@ -360,7 +367,7 @@
           getNestedIdx vs (b:bs) = bad ++ getNestedIdx vs bs
             where
               vset = S.fromList vs
-              vmap = zip vs [0..]
+              vmap = zip vs ([0..] :: [Int])
               subs = [ (ivars, ss)
                      | F.ExpSubscript _ ss _ (F.AList _ _ is) <- universeBi b :: [F.Expression (F.Analysis a)]
                      , let ivars = [ (F.varName e, F.srcName e)
@@ -379,7 +386,7 @@
           -- blocks. We can exclude variables for which If/Case
           -- control-flow depends on it instead of needing it to be
           -- directly used by a subscript expression.
-          getMissingUse :: forall a. Data a => [String] -> F.Block (F.Analysis a) -> [([String], F.SrcSpan)]
+          getMissingUse :: forall a'. Data a' => [String] -> F.Block (F.Analysis a') -> [([String], F.SrcSpan)]
           getMissingUse excls (F.BlDo _ _ _ _ _ _ bs _)      = concatMap (getMissingUse excls) bs
           getMissingUse excls (F.BlDoWhile _ _ _ _ _ _ bs _) = concatMap (getMissingUse excls) bs
           getMissingUse excls (F.BlForall _ _ _ _ _ bs _)    = concatMap (getMissingUse excls) bs
@@ -390,7 +397,7 @@
             where
               es = catMaybes mes
               -- find any induction variables that are referenced by If-Elseif expressions
-              excl' = concatMap getExcludes (universeBi es :: [F.Expression (F.Analysis a)])
+              excl' = getExcludes b
               rest = concatMap (getMissingUse (excls ++ excl')) $ concat bss
               bads = getMissingUse' excls b
           getMissingUse excls b@(F.BlCase F.Analysis{F.insLabel = Just i} _ _ _ e _ bss _)
@@ -398,21 +405,22 @@
             | eligible i (length excls) e = bads ++ rest
             | otherwise                   = rest
             where
-              rest = concatMap (getMissingUse (excls ++ getExcludes e)) $ concat bss
+              rest = concatMap (getMissingUse (excls ++ getExcludes b)) $ concat bss
               bads = map (fmap (const (F.getSpan e))) $ getMissingUse' excls b
           getMissingUse excls b@(F.BlStatement F.Analysis{F.insLabel = Just i} _ _ st)
             | eligible i (length excls) st = getMissingUse' excls b
             | otherwise                    = []
           getMissingUse _ F.BlInterface{}  = []
           getMissingUse _ F.BlComment{}    = []
+          getMissingUse _ b = error $ "checkArrayUse: getMissingUse: missing insLabel: " ++ show (fmap F.insLabel b)
 
-          getMissingUse' :: forall a. Data a => [F.Name] -> F.Block (F.Analysis a) -> [([F.Name], F.SrcSpan)]
+          getMissingUse' :: forall a'. Data a' => [F.Name] -> F.Block (F.Analysis a') -> [([F.Name], F.SrcSpan)]
           getMissingUse' excls b
             | Just i            <- F.insLabel (F.getAnnotation b)
             -- obtain the live induction variables at this program point
             , Just ivarSet      <- IM.lookup i ivmap
             -- find the definitions that flowed into this program point
-            , flFroms           <- suc flFrom i
+            , flFroms           <- drop 1 $ bfs i flFrom
             -- get their AST Blocks
             , Just flFromBlocks <- sequence $ map (flip IM.lookup bm) flFroms
             -- find out what variables they define
@@ -430,10 +438,10 @@
           -- eligible bits of AST are those that contain subscripting
           -- expressions with a length equivalent to the number of
           -- currently live induction variables.
-          eligible :: forall a b. (Data a, Data (b (F.Analysis a))) => Int -> Int -> b (F.Analysis a) -> Bool
+          eligible :: forall a' b'. (Data a', Data (b' (F.Analysis a'))) => Int -> Int -> b' (F.Analysis a') -> Bool
           eligible i numExcls x
             | Just ivars <- IM.lookup i ivmap =
-                not $ null [ () | F.ExpSubscript _ _ _ (F.AList _ _ idxs) <- universeBi x :: [F.Expression (F.Analysis a)]
+                not $ null [ () | F.ExpSubscript _ _ _ (F.AList _ _ idxs) <- universeBi x :: [F.Expression (F.Analysis a')]
                                 , length idxs == S.size ivars - numExcls ]
             | otherwise = False
 
@@ -441,10 +449,18 @@
           -- expression depends on any induction variable and
           -- therefore can be used to exclude that induction variable
           -- from the 'missing' list.
-          getExcludes e
-            | Just ei <- F.insLabel (F.getAnnotation e)
-            , Just (F.IELinear n _ _) <- IM.lookup ei divmap = [n]
-          getExcludes _ = []
+          getExcludes b
+            | Just i            <- F.insLabel (F.getAnnotation b)
+            -- obtain the live induction variables at this program point
+            , Just ivarSet      <- IM.lookup i ivmap
+            -- find the definitions that flowed into this program point
+            , flFroms           <- drop 1 $ bfs i flFrom
+            -- get their AST Blocks
+            , Just flFromBlocks <- sequence $ map (flip IM.lookup bm) flFroms
+            -- find out what variables they define
+            , flFromBlockDefSet <- S.fromList $ concatMap F.blockVarDefs flFromBlocks
+            = S.toList (ivarSet `S.intersection` flFromBlockDefSet)
+            | otherwise = []
 
           -- look through the DefMap and BlockMap for instances of
           -- variable v in order to retrieve its 'source name'.
@@ -456,7 +472,7 @@
       checkPU _ = mempty
   let reports = map checkPU (universeBi pf'')
 
-  return $ mconcat reports
+  return $!! mconcat reports
 
 -- Look through a piece of AST for the source name of a given var name.
 findSrcName :: forall a. Data a => F.Name -> F.Block (F.Analysis a) -> Maybe F.Name
diff --git a/src/Camfort/Functionality.hs b/src/Camfort/Functionality.hs
--- a/src/Camfort/Functionality.hs
+++ b/src/Camfort/Functionality.hs
@@ -63,64 +63,49 @@
   , camfortInitialize
   ) where
 
-import           Control.Arrow                                   (first, second)
-import           Data.List                                       (intersperse)
-import           Data.Maybe                                      (fromMaybe)
-import           Data.Void                                       (Void)
-import qualified Data.ByteString                                 as B
-import qualified Data.ByteString.Lazy                            as LB
-import           System.Directory                                (doesDirectoryExist, createDirectoryIfMissing,
-                                                                  getCurrentDirectory)
-import           System.FilePath                                 (takeDirectory,
-                                                                  (</>), replaceExtension)
-
-import           Text.PrettyPrint.GenericPretty                  (pp, pretty, Out)
-
-import           Control.Lens
-import           Control.Monad.Reader.Class
-import           Control.Monad
-import           Control.Monad.IO.Class
-
-import qualified Language.Fortran.AST                            as F
-import qualified Language.Fortran.Analysis.Renaming              as FA
-import qualified Language.Fortran.Analysis                       as FA
-import qualified Language.Fortran.Util.ModFile                   as FM
-import           Language.Fortran.ParserMonad                    (FortranVersion(..))
-import           Language.Fortran.PrettyPrint
-
 import           Camfort.Analysis
-import           Camfort.Analysis.Annotations                    (Annotation)
 import           Camfort.Analysis.Logger
-import           Camfort.Analysis.ModFile                        (MFCompiler,
-                                                                  getModFiles,
-                                                                  genModFiles,
-                                                                  readParseSrcDir,
-                                                                  simpleCompiler)
+import           Camfort.Analysis.ModFile (readParseSrcFile,  MFCompiler, getModFiles, genModFiles
+                                          , readParseSrcDir, readParseSrcDirP, simpleCompiler)
 import           Camfort.Analysis.Simple
+import           Camfort.Helpers (FileOrDir, Filename)
 import           Camfort.Input
-import qualified Camfort.Specification.DerivedDataType           as DDT
-import qualified Camfort.Specification.Stencils                  as Stencils
-import           Camfort.Specification.Stencils.Analysis         (compileStencils)
-import qualified Camfort.Specification.Units                     as LU
-import           Camfort.Specification.Units.Analysis            (compileUnits)
-import           Camfort.Specification.Units.Annotation          (unitInfo)
-import           Camfort.Specification.Units.Analysis.Consistent (checkUnits)
-import           Camfort.Specification.Units.Analysis.Criticals  (inferCriticalVariables)
-import           Camfort.Specification.Units.Analysis.Infer      (InferenceResult(..), InferenceReport(..), inferUnits)
-import           Camfort.Specification.Units.Monad               (runUnitAnalysis,
-                                                                  unitOpts0)
-import           Camfort.Specification.Units.ModFile             (dumpModFileCompiledUnits)
-import           Camfort.Specification.Units.MonadTypes          (LiteralsOpt,
-                                                                  UnitAnalysis,
-                                                                  UnitEnv (..),
-                                                                  UnitOpts (..))
+import qualified Camfort.Specification.DerivedDataType as DDT
 import qualified Camfort.Specification.Hoare as Hoare
+import qualified Camfort.Specification.Stencils as Stencils
+import           Camfort.Specification.Stencils.Analysis (compileStencils)
+import qualified Camfort.Specification.Units as LU
+import           Camfort.Specification.Units.Analysis (compileUnits)
+import           Camfort.Specification.Units.Analysis.Consistent (checkUnits)
+import           Camfort.Specification.Units.Analysis.Criticals (inferCriticalVariables)
+import           Camfort.Specification.Units.Analysis.Infer (InferenceResult(..), InferenceReport(..), inferUnits)
+import           Camfort.Specification.Units.Annotation (unitInfo)
+import           Camfort.Specification.Units.ModFile (dumpModFileCompiledUnits)
+import           Camfort.Specification.Units.Monad (runUnitAnalysis, unitOpts0)
+import           Camfort.Specification.Units.MonadTypes (LiteralsOpt, UnitAnalysis, UnitEnv (..), UnitOpts (..))
 import           Camfort.Transformation.CommonBlockElim
 import           Camfort.Transformation.DeadCode
 import           Camfort.Transformation.EquivalenceElim
-
-import           Camfort.Helpers                                 (FileOrDir,
-                                                                  Filename)
+import           Control.DeepSeq
+import           Control.Monad
+import           Control.Monad.IO.Class
+import qualified Data.ByteString.Lazy as LB
+import           Data.Char (toLower)
+import           Data.List (intersperse)
+import           Data.Maybe (fromMaybe)
+import qualified Language.Fortran.Analysis as FA
+import qualified Language.Fortran.Analysis.ModGraph as FM
+import qualified Language.Fortran.Analysis.Renaming as FA
+import           Language.Fortran.ParserMonad (FortranVersion(..))
+import qualified Language.Fortran.Util.ModFile as FM
+import           Pipes
+import qualified Pipes.Prelude as P
+import           Prelude hiding (mod)
+import           System.Directory
+import           System.Directory (doesDirectoryExist, createDirectoryIfMissing, getCurrentDirectory)
+import           System.FilePath (takeDirectory, (</>), takeExtension, replaceExtension)
+import           System.IO
+import           Text.PrettyPrint.GenericPretty (pp)
 
 data AnnotationType = ATDefault | Doxygen | Ford
 
@@ -179,7 +164,7 @@
   -- ^ Mod file input
   -> CamfortEnv
   -> IO r
-runFunctionality description program runner mfCompiler mfInput env = do
+runFunctionality description program runner _ _ env = do
   putStrLn $ description ++ " '" ++ ceInputSources env ++ "'"
   incDir' <- maybe getCurrentDirectory pure (ceIncludeDir env)
   isDir <- doesDirectoryExist incDir'
@@ -193,8 +178,37 @@
   pfsTexts <- readParseSrcDir (ceFortranVersion env) modFiles (ceInputSources env) (ceExcludeFiles env)
   runner program (logOutputStd True) (ceLogLevel env) (ceSourceSnippets env) modFiles pfsTexts
 
+runFunctionalityP
+  :: (Describe e, Describe w, ExitCodeOfReport b)
+  => String
+  -- ^ Functionality desription
+  -> AnalysisProgram e w IO a b
+  -- ^ Analysis program
+  -> AnalysisRunnerP e w IO a b (AnalysisReport e w b)
+  -- ^ Analysis runner
+  -> MFCompiler i IO
+  -- ^ Mod file compiler
+  -> i
+  -- ^ Mod file input
+  -> CamfortEnv
+  -> IO Int
+runFunctionalityP description program runner _ _ env = do
+  putStrLn $ description ++ " '" ++ ceInputSources env ++ "'"
+  incDir' <- maybe getCurrentDirectory pure (ceIncludeDir env)
+  isDir <- doesDirectoryExist incDir'
+  let incDir | isDir     = incDir'
+             | otherwise = takeDirectory incDir'
+  -- Previously...
+--modFiles <- genModFiles mfCompiler mfInput incDir (ceExcludeFiles env)
+  -- ...instead for now, just get the mod files
 
+  modFiles <- getModFiles incDir
 
+  reports <- P.toListM $
+    readParseSrcDirP (ceFortranVersion env) modFiles (ceInputSources env) (ceExcludeFiles env) >->
+    runner program (logOutputStd True) (ceLogLevel env) (ceSourceSnippets env) modFiles
+  return . exitCodeOfSet $ reports
+
 --------------------------------------------------------------------------------
 -- * Wrappers on all of the features
 
@@ -208,10 +222,10 @@
 
 countVarDecls :: CamfortEnv -> IO Int
 countVarDecls =
-  runFunctionality
+  runFunctionalityP
   "Counting variable declarations in"
   (generalizePureAnalysis . countVariableDeclarations)
-  (describePerFileAnalysis "count variable declarations")
+  (describePerFileAnalysisP "count variable declarations")
   simpleCompiler ()
 
 dead :: FileOrDir -> CamfortEnv -> IO Int
@@ -243,42 +257,42 @@
 
 implicitNone :: Bool -> CamfortEnv -> IO Int
 implicitNone allPU =
-  runFunctionality
+  runFunctionalityP
   "Checking 'implicit none' completeness"
   (generalizePureAnalysis . (checkImplicitNone allPU))
-  (describePerFileAnalysis "check 'implicit none'")
+  (describePerFileAnalysisP "check 'implicit none'")
   simpleCompiler ()
 
 allocCheck :: CamfortEnv -> IO Int
 allocCheck =
-  runFunctionality
+  runFunctionalityP
   "Checking allocate / deallocate usage"
   (generalizePureAnalysis . checkAllocateStatements)
-  (describePerFileAnalysis "check allocate / deallocate")
+  (describePerFileAnalysisP "check allocate / deallocate")
   simpleCompiler ()
 
 fpCheck :: CamfortEnv -> IO Int
 fpCheck =
-  runFunctionality
+  runFunctionalityP
   "Checking usage of floating point"
   (generalizePureAnalysis . checkFloatingPointUse)
-  (describePerFileAnalysis "check floating point")
+  (describePerFileAnalysisP "check floating point")
   simpleCompiler ()
 
 useCheck :: CamfortEnv -> IO Int
 useCheck =
-  runFunctionality
+  runFunctionalityP
   "Checking usage of USE statements"
   (generalizePureAnalysis . checkModuleUse)
-  (describePerFileAnalysis "check module USE")
+  (describePerFileAnalysisP "check module USE")
   simpleCompiler ()
 
 arrayCheck :: CamfortEnv -> IO Int
 arrayCheck =
-  runFunctionality
+  runFunctionalityP
   "Checking array usage"
   (generalizePureAnalysis . checkArrayUse)
-  (describePerFileAnalysis "check array usage")
+  (describePerFileAnalysisP "check array usage")
   simpleCompiler ()
 
 ddtRefactor :: FileOrDir -> CamfortEnv -> IO Int
@@ -299,18 +313,18 @@
 
 ddtCheck :: CamfortEnv -> IO Int
 ddtCheck =
-  runFunctionality
+  runFunctionalityP
   "Checking derived datatype annotations"
   (generalizePureAnalysis . DDT.check)
-  (describePerFileAnalysis "check derived datatypes")
+  (describePerFileAnalysisP "check derived datatypes")
   simpleCompiler ()
 
 ddtInfer :: CamfortEnv -> IO Int
 ddtInfer =
-  runFunctionality
+  runFunctionalityP
   "Inferring derived datatypes"
   (generalizePureAnalysis . DDT.infer)
-  (describePerFileAnalysis "infer derived datatypes")
+  (describePerFileAnalysisP "infer derived datatypes")
   simpleCompiler ()
 
 ddtCompile :: CamfortEnv -> IO Int
@@ -321,29 +335,29 @@
   isDir <- doesDirectoryExist incDir'
   let incDir | isDir     = incDir'
              | otherwise = takeDirectory incDir'
-  modFiles <- getModFiles incDir
+  modFileNames <- getModFiles incDir
 
   -- Run the gen mod file routine directly on the input source
-  modFiles <- genModFiles (ceFortranVersion env) modFiles DDT.compile () (ceInputSources env) (ceExcludeFiles env)
+  modFiles <- genModFiles (ceFortranVersion env) modFileNames DDT.compile () (ceInputSources env) (ceExcludeFiles env)
   -- Write the mod files out
   forM_ modFiles $ \ modFile -> do
      let mfname = replaceExtension (FM.moduleFilename modFile) FM.modFileSuffix
-     LB.writeFile mfname (FM.encodeModFile modFile)
+     LB.writeFile mfname (FM.encodeModFile [modFile])
   return 0
 
 {- Units feature -}
 
-runUnitsFunctionality
-  :: (Describe e, Describe w)
+runUnitsFunctionalityP
+  :: (Describe e, Describe w, ExitCodeOfReport b)
   => String
   -> (UnitOpts -> AnalysisProgram e w IO a b)
-  -> AnalysisRunner e w IO a b r
+  -> AnalysisRunnerP e w IO a b (AnalysisReport e w b)
   -> LiteralsOpt
   -> CamfortEnv
-  -> IO r
-runUnitsFunctionality description unitsProgram runner opts =
+  -> IO Int
+runUnitsFunctionalityP description unitsProgram runner opts =
   let uo = optsToUnitOpts opts
-  in runFunctionality description (unitsProgram uo) runner compileUnits uo
+  in runFunctionalityP description (unitsProgram uo) runner compileUnits uo
 
 optsToUnitOpts :: LiteralsOpt -> UnitOpts
 optsToUnitOpts m = o1
@@ -362,15 +376,16 @@
 
 
 -- slight hack to make doRefactorAndCreate happy
-singlePfUnits'
-  :: UnitAnalysis a -> UnitOpts
-  -> AnalysisProgram () () IO [ProgramFile] a
-singlePfUnits' unitAnalysis opts (pf:_) =
-  let ue = UnitEnv
-        { unitOpts = opts
-        , unitProgramFile = pf
-        }
-  in runUnitAnalysis ue unitAnalysis
+-- singlePfUnits'
+--   :: UnitAnalysis a -> UnitOpts
+--   -> AnalysisProgram () () IO [ProgramFile] a
+-- singlePfUnits' unitAnalysis opts (pf:_) =
+--   let ue = UnitEnv
+--         { unitOpts = opts
+--         , unitProgramFile = pf
+--         }
+--   in runUnitAnalysis ue unitAnalysis
+-- singlePfUnits' _ _ [] = error "singlePfUnits': no program file provided"
 
 multiPfUnits
   :: (Describe a)
@@ -399,57 +414,88 @@
     Left msg -> do
       putStrLn $ modFileName ++ ": Error: " ++ show msg
       pure 1
-    Right modFile -> do
-      putStrLn $ modFileName ++ ": successfully parsed precompiled file."
-      putStrLn . fromMaybe "unable to find units info" $ dumpModFileCompiledUnits modFile
+    Right modFiles -> do
+      forM_ modFiles $ \ modFile -> do
+        putStrLn $ modFileName ++ ": successfully parsed summary file."
+        putStrLn . fromMaybe "unable to find units info" $ dumpModFileCompiledUnits modFile
       pure 0
 
 unitsCheck :: LiteralsOpt -> CamfortEnv -> IO Int
 unitsCheck =
-  runUnitsFunctionality
+  runUnitsFunctionalityP
   "Checking units for"
   (singlePfUnits checkUnits)
-  (describePerFileAnalysis "unit checking")
+  (describePerFileAnalysisP "unit checking")
 
 
 unitsInfer :: Bool -> LiteralsOpt -> CamfortEnv -> IO Int
 unitsInfer showAST =
-  runUnitsFunctionality
+  runUnitsFunctionalityP
   "Inferring units for"
   (singlePfUnits inferUnits)
   (if showAST
-      then describePerFileAnalysisShowASTUnitInfo
-      else describePerFileAnalysis "unit inference")
+      then describePerFileAnalysisShowASTUnitInfoP
+      else describePerFileAnalysisP "unit inference")
 
 -- | Given an analysis program for a single file, run it over every input file
 -- and collect the reports, then print those reports to standard output.
-describePerFileAnalysisShowASTUnitInfo
-  :: (MonadIO m, Describe w, Describe e)
-  => AnalysisRunner e w m ProgramFile InferenceResult Int
-describePerFileAnalysisShowASTUnitInfo program logOutput logLevel snippets modFiles pfsTexts = do
-  reports <- runPerFileAnalysis program logOutput logLevel snippets modFiles pfsTexts
-  flip mapM_ reports $ \ r -> do
-    case r of
-      AnalysisReport _ _ (ARSuccess (Inferred (InferenceReport pfUA eVars))) ->
-        liftIO . pp . fmap (unitInfo . FA.prevAnnotation) . FA.rename $ pfUA
-      _ -> pure ()
-    putDescribeReport "unit inference" (Just logLevel) snippets r
-  return $ exitCodeOfSet reports
+describePerFileAnalysisShowASTUnitInfoP
+  :: (MonadIO m, Describe w, Describe e, NFData w, NFData e)
+  => AnalysisRunnerP e w m ProgramFile InferenceResult (AnalysisReport e w InferenceResult)
+describePerFileAnalysisShowASTUnitInfoP program logOutput logLevel snippets modFiles =
+  runPerFileAnalysisP program logOutput logLevel snippets modFiles >->
+    (P.mapM $ \ r -> do
+        case r of
+          AnalysisReport _ _ (ARSuccess (Inferred (InferenceReport pfUA _))) ->
+            liftIO . pp . fmap (unitInfo . FA.prevAnnotation) . FA.rename $ pfUA
+          _ -> pure ()
+        putDescribeReport "unit inference" (Just logLevel) snippets r
+        pure r)
 
-{-  TODO: remove if not needed
-unitsCompile :: FileOrDir -> LiteralsOpt -> CamfortEnv -> IO ()
-unitsCompile outSrc opts env =
-  runUnitsFunctionality
-  "Compiling units for"
-  (singlePfUnits inferAndCompileUnits)
-  (compilePerFile "unit compilation" (ceInputSources env) outSrc)
-  opts
-  env
--}
-  -- Previously...
---modFiles <- genModFiles mfCompiler mfInput incDir (ceExcludeFiles env)
-  -- ...instead for now, just get the mod files
+-- | Expand all paths that are directories into a list of Fortran
+-- files from a recursive directory listing.
+expandDirs :: [FilePath] -> IO [FilePath]
+expandDirs = fmap concat . mapM doEach
+  where
+    doEach path = do
+      isDir <- doesDirectoryExist path
+      if isDir
+        then listFortranFiles path
+        else pure [path]
 
+-- | Get a list of Fortran files under the given directory.
+listFortranFiles :: FilePath -> IO [FilePath]
+listFortranFiles dir = filter isFortran <$> listDirectoryRecursively dir
+  where
+    -- | True if the file has a valid fortran extension.
+    isFortran :: FilePath -> Bool
+    isFortran x = map toLower (takeExtension x) `elem` exts
+      where exts = [".f", ".f90", ".f77", ".f03"]
+
+listDirectoryRecursively :: FilePath -> IO [FilePath]
+listDirectoryRecursively dir = listDirectoryRec dir ""
+  where
+    listDirectoryRec :: FilePath -> FilePath -> IO [FilePath]
+    listDirectoryRec d f = do
+      let fullPath = d </> f
+      isDir <- doesDirectoryExist fullPath
+      if isDir
+      then do
+        conts <- listDirectory fullPath
+        concat <$> mapM (listDirectoryRec fullPath) conts
+      else pure [fullPath]
+
+decodeOneModFile :: FilePath -> IO FM.ModFiles
+decodeOneModFile path = do
+  contents <- LB.readFile path
+  case FM.decodeModFile contents of
+    Left msg -> do
+      hPutStrLn stderr $ path ++ ": Error: " ++ msg
+      return []
+    Right modFiles -> do
+      hPutStrLn stderr $ path ++ ": successfully parsed summary file."
+      return modFiles
+
 unitsCompile :: LiteralsOpt -> CamfortEnv -> IO Int
 unitsCompile opts env = do
   let uo = optsToUnitOpts opts
@@ -459,32 +505,68 @@
   isDir <- doesDirectoryExist incDir'
   let incDir | isDir     = incDir'
              | otherwise = takeDirectory incDir'
-  modFiles <- getModFiles incDir
+  -- modFileNames <- getModFiles incDir
 
-  -- Run the gen mod file routine directly on the input source
-  modFiles <- genModFiles (ceFortranVersion env) modFiles compileUnits uo (ceInputSources env) (ceExcludeFiles env)
-  -- Write the mod files out
-  forM_ modFiles $ \modFile -> do
-     let mfname = replaceExtension (FM.moduleFilename modFile) FM.modFileSuffix
-     LB.writeFile mfname (FM.encodeModFile modFile)
+  paths' <- expandDirs $ [ceInputSources env]
+  -- Build the graph of module dependencies
+  mg0 <- FM.genModGraph (ceFortranVersion env) [incDir] paths'
+
+  let compileFileToMod mods pf = do
+        mod <- compileUnits uo mods pf
+        let mfname = replaceExtension (FM.moduleFilename mod) FM.modFileSuffix
+        LB.writeFile mfname (FM.encodeModFile [mod])
+        pure mod
+
+  -- Loop through the dependency graph until it is empty
+  let loop mg mods
+        | nxt <- FM.takeNextMods mg
+        , not (null nxt) = do
+            let fnPaths = [ fn | (_, Just (FM.MOFile fn)) <- nxt ]
+            newMods <- fmap concat . forM fnPaths $ \ fnPath -> do
+              tsStatus <- FM.checkTimestamps fnPath
+              case tsStatus of
+                FM.NoSuchFile -> do
+                  putStr $ "Does not exist: " ++ fnPath
+                  pure [FM.emptyModFile]
+                FM.ModFileExists modPath -> do
+                  putStrLn $ "Loading mod file " ++ modPath ++ "."
+                  decodeOneModFile modPath
+                FM.CompileFile -> do
+                  putStr $ "Summarising " ++ fnPath ++ "..."
+                  m_pf <- readParseSrcFile (ceFortranVersion env) mods fnPath
+                  case m_pf of
+                    Just (pf, _) -> do
+                      mod <- compileFileToMod mods pf
+                      putStrLn "done"
+                      pure [mod]
+                    Nothing -> do
+                      putStrLn "failed"
+                      pure []
+
+            let ns  = map fst nxt
+            let mg' = FM.delModNodes ns mg
+            loop mg' $ newMods ++ mods
+      loop _ mods = pure mods
+
+  _allMods <- loop mg0 []
   return 0
 
 unitsSynth :: AnnotationType -> FileOrDir -> LiteralsOpt -> CamfortEnv -> IO Int
 unitsSynth annType outSrc opts env =
-  runUnitsFunctionality
-  "Synthesising units for"
-  (multiPfUnits $ LU.synthesiseUnits (markerChar annType))
-  (doRefactor "unit synthesis" (ceInputSources env) outSrc)
-  opts
-  env
-
+  runFunctionality "Synthesising units for"
+                   (multiPfUnits (LU.synthesiseUnits (markerChar annType)) uo)
+                   (doRefactor "unit synthesis" (ceInputSources env) outSrc)
+                   compileUnits
+                   uo
+                   env
+  where uo = optsToUnitOpts opts
 
 unitsCriticals :: LiteralsOpt -> CamfortEnv -> IO Int
 unitsCriticals =
-  runUnitsFunctionality
+  runUnitsFunctionalityP
   "Suggesting variables to annotate with unit specifications in"
   (singlePfUnits inferCriticalVariables)
-  (describePerFileAnalysis "unit critical variable analysis")
+  (describePerFileAnalysisP "unit critical variable analysis")
 
 
 {- Stencils feature -}
@@ -492,19 +574,19 @@
 
 stencilsCheck :: CamfortEnv -> IO Int
 stencilsCheck =
-  runFunctionality
+  runFunctionalityP
   "Checking stencil specs for"
   (generalizePureAnalysis . Stencils.check)
-  (describePerFileAnalysis "stencil checking")
+  (describePerFileAnalysisP "stencil checking")
   compileStencils ()
 
 
 stencilsInfer :: Bool -> CamfortEnv -> IO Int
 stencilsInfer useEval =
-  runFunctionality
+  runFunctionalityP
   "Inferring stencil specs for"
   (generalizePureAnalysis . Stencils.infer useEval '=')
-  (describePerFileAnalysis "stencil inference")
+  (describePerFileAnalysisP "stencil inference")
   compileStencils ()
 
 
@@ -526,10 +608,10 @@
 
 invariantsCheck :: Hoare.PrimReprOption -> CamfortEnv -> IO Int
 invariantsCheck pro =
-  runFunctionality
+  runFunctionalityP
   "Checking invariants in"
   (Hoare.check pro)
-  (describePerFileAnalysis "invariant checking")
+  (describePerFileAnalysisP "invariant checking")
   simpleCompiler ()
 
 
diff --git a/src/Camfort/Helpers.hs b/src/Camfort/Helpers.hs
--- a/src/Camfort/Helpers.hs
+++ b/src/Camfort/Helpers.hs
@@ -43,7 +43,7 @@
 import qualified Data.ByteString.Char8 as B
 import System.Directory
 import qualified Data.Map.Lazy as Map hiding (map, (\\))
-import Control.Monad.Writer.CPS
+import Control.Monad.Writer
 
 -- collect: from an association list to a map with list-based bins for matching keys
 collect :: (Eq a, Ord k) => [(k, a)] -> Map.Map k [a]
@@ -57,13 +57,14 @@
 -- Filename and directory related helpers
 
 -- gets the directory part of a filename
-getDir :: String -> String
+getDir :: Filename -> Directory
 getDir file = let ixs = elemIndices '/' file
               in if null ixs then file
                  else take (last $ ixs) file
 
 
 {-| Creates a directory (from a filename string) if it doesn't exist -}
+checkDir :: Directory -> IO ()
 checkDir f = case (elemIndices '/' f) of
                [] -> return ()
                ix -> let d = take (last ix) f
@@ -92,7 +93,7 @@
 instance Traversable (Reverse Str.Str) where
     traverse _ (Reverse Str.Zero) = pure $ Reverse Str.Zero
     traverse f (Reverse (Str.One x)) = (Reverse . Str.One) <$> f x
-    traverse f (Reverse (Str.Two x y)) = (\y x -> Reverse $ Str.Two x y)
+    traverse f (Reverse (Str.Two x y)) = (\y' x' -> Reverse $ Str.Two x' y')
                              <$> (fmap unwrapReverse . traverse f . Reverse $ y)
                              <*> (fmap unwrapReverse . traverse f . Reverse $ x)
 
diff --git a/src/Camfort/Helpers/Syntax.hs b/src/Camfort/Helpers/Syntax.hs
--- a/src/Camfort/Helpers/Syntax.hs
+++ b/src/Camfort/Helpers/Syntax.hs
@@ -62,10 +62,13 @@
 data AnnotationFree t = AnnotationFree { annotationBound :: t } deriving Show
 
 {-| short-hand constructor for 'AnnotationFree' -}
+af :: t -> AnnotationFree t
 af = AnnotationFree
 
 -- variable renaming helpers
+caml :: [Char] -> [Char]
 caml (x:xs) = toUpper x : xs
+caml []     = []
 
 -- Here begins varioous 'Eq' instances for instantiations of 'AnnotationFree'
 
@@ -118,8 +121,8 @@
 -- SrcSpan helpers
 
 dropLine :: FU.SrcSpan -> FU.SrcSpan
-dropLine (FU.SrcSpan s1 (FU.Position o _ l f Nothing)) =
-    FU.SrcSpan s1 (FU.Position o 1 (l+1) f Nothing)
+dropLine (FU.SrcSpan s1 (FU.Position o _ l f po)) =
+    FU.SrcSpan s1 (FU.Position o 1 (l+1) f po)
 
 deleteLine :: FU.SrcSpan -> FU.SrcSpan
 deleteLine (FU.SrcSpan (FU.Position ol cl ll fl pl) (FU.Position ou _ lu fu pu)) =
@@ -128,6 +131,7 @@
 linesCovered :: FU.Position -> FU.Position -> Int
 linesCovered (FU.Position _ _ l1 _ _) (FU.Position _ _ l2 _ _) = l2 - l1 + 1
 
+toCol0 :: FU.Position -> FU.Position
 toCol0 (FU.Position o _ l f p) = FU.Position o 1 l f p
 
 afterAligned :: FU.SrcSpan -> FU.Position
diff --git a/src/Camfort/Helpers/Vec.hs b/src/Camfort/Helpers/Vec.hs
--- a/src/Camfort/Helpers/Vec.hs
+++ b/src/Camfort/Helpers/Vec.hs
@@ -60,8 +60,8 @@
 
 -- Indexed natural number type
 data Natural (n :: Nat) where
-     Zero :: Natural Z
-     Succ :: Natural n -> Natural (S n)
+     Zero :: Natural 'Z
+     Succ :: Natural n -> Natural ('S n)
 
 deriving instance Show (Natural n)
 
@@ -71,15 +71,15 @@
 class IsNatural (n :: Nat) where
    fromNat :: Proxy n -> Int
 
-instance IsNatural Z where
+instance IsNatural 'Z where
    fromNat Proxy = 0
-instance IsNatural n => IsNatural (S n) where
+instance IsNatural n => IsNatural ('S n) where
    fromNat Proxy = 1 + fromNat (Proxy :: Proxy n)
 
 -- Indexed vector type
 data Vec (n :: Nat) a where
-     Nil :: Vec Z a
-     Cons :: a -> Vec n a -> Vec (S n) a
+     Nil :: Vec 'Z a
+     Cons :: a -> Vec n a -> Vec ('S n) a
 
 length :: Vec n a -> Int
 length Nil = 0
@@ -102,10 +102,10 @@
 instance Show a => Show (Vec n a) where
   show xs = "<" ++ showV xs ++ ">"
     where
-      showV :: forall n a . Show a => Vec n a -> String
+      showV :: forall n' a' . Show a' => Vec n' a' -> String
       showV Nil          = ""
-      showV (Cons x Nil) = show x
-      showV (Cons x xs)  = show x ++ "," ++ showV xs
+      showV (Cons x Nil)  = show x
+      showV (Cons x xs')  = show x ++ "," ++ showV xs'
 
 instance Foldable (Vec n) where
   foldr _ acc Nil = acc
@@ -130,6 +130,7 @@
 (!!) :: Vec n a -> Int -> a
 Cons x _  !! 0 = x
 Cons _ v' !! n = v' !! (n - 1)
+_ !! _         = error "Vec: (!!)"
 
 replace :: Int -> a -> Vec n a -> Vec n a
 replace 0 a (Cons _ xs) = Cons a xs
@@ -161,7 +162,7 @@
   return ReflEq
 proveEqSize _ _ = Nothing
 
-proveNonEmpty :: Vec n a -> Maybe (ExistsEqT S n)
+proveNonEmpty :: Vec n a -> Maybe (ExistsEqT 'S n)
 proveNonEmpty v =
   case v of
     Nil -> Nothing
@@ -173,15 +174,15 @@
 -- pre-condition: the input is a 'rectangular' list of lists (i.e. all internal
 -- lists have the same size)
 fromLists :: forall a . [[a]] -> VecList a
-fromLists [] = VL ([] :: [Vec Z a])
+fromLists [] = VL ([] :: [Vec 'Z a])
 fromLists (xs:xss) = consList (fromList xs) (fromLists xss)
   where
     consList :: VecBox a -> VecList a -> VecList a
     consList (VecBox vec) (VL [])     = VL [vec]
-    consList (VecBox vec) (VL xs) = -- Force the pre-condition equality
-      case preCondition vec xs of
-          ReflEq -> VL (vec : xs)
+    consList (VecBox vec) (VL xs') = -- Force the pre-condition equality
+      case preCondition vec xs' of
+          ReflEq -> VL (vec : xs')
           where -- At the moment the pre-condition is 'assumed', and therefore
             -- force used unsafeCoerce: TODO, rewrite
-            preCondition :: forall n n1 a . Vec n a -> [Vec n1 a] -> EqT n n1
+            preCondition :: forall n n1 a' . Vec n a' -> [Vec n1 a'] -> EqT n n1
             preCondition _ _ = unsafeCoerce ReflEq
diff --git a/src/Camfort/Input.hs b/src/Camfort/Input.hs
--- a/src/Camfort/Input.hs
+++ b/src/Camfort/Input.hs
@@ -15,10 +15,12 @@
   , ProgramFile
   , AnalysisProgram
   , AnalysisRunner
+  , AnalysisRunnerP
+  , AnalysisRunnerConsumer
     -- * Builders for analysers and refactorings
-  , runPerFileAnalysis
+  , runPerFileAnalysisP
   , runMultiFileAnalysis
-  , describePerFileAnalysis
+  , describePerFileAnalysisP
   , doRefactor
   , doRefactorAndCreate
   , perFileRefactoring
@@ -35,6 +37,7 @@
 import           Data.List                     (intercalate)
 
 import           Control.Lens
+import           Control.DeepSeq
 
 import qualified Language.Fortran.AST          as F
 import           Language.Fortran.Util.ModFile (ModFiles, emptyModFiles)
@@ -47,6 +50,9 @@
 import           Camfort.Helpers
 import           Camfort.Output
 
+import           Pipes
+import qualified Pipes.Prelude                 as P
+
 -- | An analysis program which accepts inputs of type @a@ and produces results
 -- of type @b@.
 --
@@ -59,30 +65,36 @@
 type AnalysisRunner e w m a b r =
   AnalysisProgram e w m a b -> LogOutput m -> LogLevel -> Bool -> ModFiles -> [(ProgramFile, SourceText)] -> m r
 
+type AnalysisRunnerP e w m a b r =
+  AnalysisProgram e w m a b -> LogOutput m -> LogLevel -> Bool -> ModFiles -> Pipe (ProgramFile, SourceText) r m ()
+
+type AnalysisRunnerConsumer e w m a b r =
+  AnalysisProgram e w m a b -> LogOutput m -> LogLevel -> Bool -> ModFiles -> Consumer (ProgramFile, SourceText) m ()
+
 --------------------------------------------------------------------------------
 --  Simple runners
 --------------------------------------------------------------------------------
 
 -- | Given an analysis program for a single file, run it over every input file
 -- and collect the reports. Doesn't produce any output.
-runPerFileAnalysis
-  :: (Monad m, Describe e, Describe w)
-  => AnalysisRunner e w m ProgramFile b [AnalysisReport e w b]
-runPerFileAnalysis program logOutput logLevel snippets modFiles =
-  traverse (\pf ->
-    runAnalysisT
-      (F.pfGetFilename pf)
-      logOutput
-      logLevel
-      modFiles
-      (program pf)) . map fst
+runPerFileAnalysisP
+  :: (MonadIO m, Describe e, Describe w, NFData e, NFData w, NFData b)
+  => AnalysisRunnerP e w m ProgramFile b (AnalysisReport e w b)
+runPerFileAnalysisP program logOutput logLevel _ modFiles =
+  P.mapM $ \ (pf, _) -> do
+    -- liftIO . putStrLn $ "Running analysis on " ++ (F.pfGetFilename pf)
+    runAnalysisT (F.pfGetFilename pf)
+                 logOutput
+                 logLevel
+                 modFiles
+                 (program pf)
 
 -- | Run an analysis program over every input file and get the report. Doesn't
 -- produce any output.
 runMultiFileAnalysis
   :: (Monad m, Describe e, Describe w)
   => AnalysisRunner e w m [ProgramFile] b (AnalysisReport e w b)
-runMultiFileAnalysis program logOutput logLevel snippets modFiles
+runMultiFileAnalysis program logOutput logLevel _ modFiles
   = runAnalysisT "<unknown>" logOutput logLevel modFiles . program . map fst
 
 --------------------------------------------------------------------------------
@@ -117,13 +129,12 @@
 
 -- | Given an analysis program for a single file, run it over every input file
 -- and collect the reports, then print those reports to standard output.
-describePerFileAnalysis
-  :: (MonadIO m, Describe r, ExitCodeOfReport r, Describe w, Describe e)
-  => Text -> AnalysisRunner e w m ProgramFile r Int
-describePerFileAnalysis analysisName program logOutput logLevel snippets modFiles pfsTexts = do
-  reports <- runPerFileAnalysis program logOutput logLevel snippets modFiles pfsTexts
-  mapM_ (putDescribeReport analysisName (Just logLevel) snippets) reports
-  return $ exitCodeOfSet reports
+describePerFileAnalysisP
+  :: (MonadIO m, Describe r, ExitCodeOfReport r, Describe w, Describe e, NFData e, NFData w, NFData r)
+  => Text -> AnalysisRunnerP e w m ProgramFile r (AnalysisReport e w r)
+describePerFileAnalysisP analysisName program logOutput logLevel snippets modFiles = do
+  runPerFileAnalysisP program logOutput logLevel snippets modFiles >->
+    (P.mapM $ \ r -> liftIO (putDescribeReport analysisName (Just logLevel) snippets r) >> pure r)
 
 -- | Accepts an analysis program for multiple input files which produces a
 -- result value along with refactored files. Performs the refactoring, and
diff --git a/src/Camfort/Output.hs b/src/Camfort/Output.hs
--- a/src/Camfort/Output.hs
+++ b/src/Camfort/Output.hs
@@ -29,6 +29,8 @@
   , refactoring
   ) where
 
+import Prelude hiding (span)
+
 import qualified Language.Fortran.AST as F
 import qualified Language.Fortran.PrettyPrint as PP
 import qualified Language.Fortran.Util.Position as FU
@@ -91,6 +93,7 @@
 
 {-| changeDir is used to change the directory of a filename string.
     If the filename string has no directory then this is an identity  -}
+changeDir :: Eq a => [a] -> [a] -> [a] -> [a]
 changeDir newDir oldDir oldFilename =
     newDir ++ listDiffL oldDir oldFilename
   where
@@ -250,20 +253,22 @@
 might actually be less than 'n'- but in principle this should not
 happen with the usaage in 'refactorDecl' -}
 
+removeNewLines :: B.ByteString -> Int -> (B.ByteString, Int)
 removeNewLines xs 0 = (xs, 0)
 -- Deal with CR LF in the same way as just LF
-removeNewLines xs n =
-    case unpackFst (B.splitAt 4 xs) of
+removeNewLines topXS n =
+    case unpackFst (B.splitAt 4 topXS) of
       ("\r\n\r\n", xs) -> (xs', n' + 1)
           where (xs', n') = removeNewLines (B.pack "\r\n" `B.append` xs) (n - 1)
       _ ->
-        case unpackFst (B.splitAt 2 xs) of
+        case unpackFst (B.splitAt 2 topXS) of
           ("\n\n", xs)     -> (xs', n' + 1)
               where (xs', n') = removeNewLines (B.pack "\n" `B.append` xs) (n - 1)
           _ ->
-           case B.uncons xs of
-               Nothing -> (xs, 0)
+           case B.uncons topXS of
+               Nothing -> (topXS, 0)
                Just (x, xs) -> (B.cons x xs', n)
                    where (xs', _) = removeNewLines xs n
 
+unpackFst :: (B.ByteString, b) -> (String, b)
 unpackFst (x, y) = (B.unpack x, y)
diff --git a/src/Camfort/Specification/DerivedDataType.hs b/src/Camfort/Specification/DerivedDataType.hs
--- a/src/Camfort/Specification/DerivedDataType.hs
+++ b/src/Camfort/Specification/DerivedDataType.hs
@@ -33,42 +33,38 @@
 import           Camfort.Analysis.Annotations (onPrev, buildCommentText, A, Annotation(..))
 import           Camfort.Analysis.CommentAnnotator (annotateComments, ASTEmbeddable(..), Linkable(..))
 import           Camfort.Analysis.ModFile
-import           Camfort.Helpers (Filename)
 import           Camfort.Helpers.Syntax (afterAligned, toCol0, deleteLine)
 import           Camfort.Specification.DerivedDataType.Parser (ddtParser, DDTStatement(..))
 import           Control.Applicative
-import           Control.Arrow ((***), (|||), first, second, (&&&))
-import           Control.Lens
+import           Control.Arrow (first, second, (&&&))
+import           Control.DeepSeq
 import           Control.Monad
-import           Control.Monad.RWS.CPS
-import           Control.Monad.Writer.CPS
+import           Control.Monad.RWS.Strict
+import           Control.Monad.Writer.Strict
 import           Data.Binary (Binary, decodeOrFail, encode)
-import qualified Data.ByteString.Lazy.Char8 as LB
 import           Data.Data
 import           Data.Function (on)
-import           Data.Generics.Uniplate.Operations
+import           Data.Generics.Uniplate.Operations hiding (rewrite)
 import qualified Data.IntMap.Strict as IM
 import           Data.List (sort, foldl', groupBy)
 import qualified Data.List as List
 import qualified Data.Map.Strict as M
-import           Data.Maybe (mapMaybe, fromMaybe, fromJust, maybeToList, isJust)
+import           Data.Maybe (mapMaybe, fromMaybe, fromJust, isJust)
 import           Data.Monoid ((<>))
 import qualified Data.Semigroup as SG
 import qualified Data.Set as S
 import qualified Data.Strict.Either as SE
 import           Data.Text (Text, unlines, intercalate, pack)
-import           Data.Text.Lazy.Builder (Builder)
 import qualified Data.Text.Lazy.Builder as Builder
 import           GHC.Generics (Generic)
 import qualified Language.Fortran.AST as F
 import qualified Language.Fortran.Analysis as FA
 import qualified Language.Fortran.Analysis.BBlocks as FAB
 import qualified Language.Fortran.Analysis.DataFlow as FAD
-import qualified Language.Fortran.Analysis.Renaming as FAR
 import qualified Language.Fortran.Analysis.Types as FAT
 import           Language.Fortran.Util.ModFile
 import qualified Language.Fortran.Util.Position as FU
-import           Prelude hiding (unlines)
+import           Prelude hiding (unlines, minBound, maxBound)
 
 ddtShort :: String
 ddtShort = "ddt"
@@ -126,6 +122,7 @@
 -- | Info about a variable: source name, source filename, source span.
 data VInfo = VInfo { vSrcName :: F.Name, vFileName :: String, vSrcSpan :: FU.SrcSpan }
   deriving (Generic, Show, Eq)
+instance NFData VInfo
 instance Binary VInfo
 
 -- special ord instance compares by filename, source span and then name.
@@ -139,6 +136,7 @@
                        , essStarred  :: Bool              -- ^ is this essence 'starred'?
                        }
   deriving (Show, Generic)
+instance NFData Essence
 instance Binary Essence
 
 -- special eq instance: only compare type-name and labels
@@ -153,6 +151,7 @@
 data IndexError = IndexDupError String VInfo [Int]
                 | IndexOOBError String VInfo [Int]
   deriving (Show, Eq, Ord, Generic)
+instance NFData IndexError
 instance Binary IndexError
 
 -- | Variable(dim)s and any conflicting spec essences.
@@ -177,6 +176,7 @@
                           , ddtrBDE   :: BadDimErrors
                           , ddtrCheck :: Bool }
   deriving Generic
+instance NFData DerivedDataTypeReport
 instance Binary DerivedDataTypeReport
 
 -- | These reports can be combined, e.g. from multiple files, and the
@@ -246,7 +246,7 @@
       num = length ddtrSpecs
       specReport = linesByFile specLines
       specLines = [ (vinfo, [pack $ genCommentText r (var, vSrcName)])
-                  | ((var, dim), essenceSet) <- M.toList ddtrSMap
+                  | ((var, _), essenceSet)   <- M.toList ddtrSMap
                   , Essence{..}              <- S.toList essenceSet
                   , vinfo@VInfo{..}          <- S.toList essVInfoSet ]
 
@@ -260,7 +260,7 @@
                             describe dim <> ")\nconflicts with\n" <>
                             unlines [ pack fn <> ": " <> describe ss <> " " <> pack ty <> "(" <> describeLabels labs <> ")"
                                     | Essence ty labs vinfoSet _ <- essences
-                                    , VInfo src fn ss <- S.toList vinfoSet ]])
+                                    , VInfo _ fn ss <- S.toList vinfoSet ]])
                  | ((_, dim), essenceSet) <- M.toList ddtrCE
                  , not (S.null essenceSet)
                  , let Essence ty0 l0 vinfoSet0 _:essences = S.toList essenceSet
@@ -384,14 +384,14 @@
       where
         vinfos = S.toList essVInfoSet
         -- Labels that appear more than once in the label map:
-        labs = M.keys . M.filter (>1) . M.fromListWith (+) . map (,1) $ IM.elems essLabelMap
+        labs = M.keys . M.filter (>1) . M.fromListWith (+) . map (,1::Int) $ IM.elems essLabelMap
 
     -- Dupped labels:
     badLabels = M.filter (not . null) $ M.map (setConcatMap findDupLabels) essences
 
     -- Badly specified 'dim' attributes (e.g. out of bounds):
     badDims = [ ((declVarName, dim), S.singleton (maxDim, vinfo))
-              | (spec@DDTSt{..} , b) <- specs
+              | (DDTSt{..}, b)       <- specs
               , (srcName, dim)       <- ddtStVarDims
               , (declVarName, vinfo) <- declaredVars srcFile b
               , vSrcName vinfo == srcName
@@ -406,10 +406,10 @@
 
     -- Index out-of-bounds of statically-known array dimensions:
     oobIndices = [ IndexOOBError tyname vinfo indices
-                 | (spec@DDTSt{..} , b) <- specs
+                 | (DDTSt{..}, b)       <- specs
                  , (srcName, dim)       <- ddtStVarDims
                  , (declVarName, vinfo) <- declaredVars srcFile b
-                 , let indices = [], let tyname = ""
+                 , let tyname = ""
                  , vSrcName vinfo == srcName
                  , Just indices <- [ do FA.IDType { FA.idCType = Just (FA.CTArray dims) } <- M.lookup declVarName tenv
                                         let maxDim = length dims
@@ -496,7 +496,7 @@
     -- FIXME: possibly use the 'essences' writer slot to instead
     -- gather derived-type declarations and put them somewhere
     -- central.
-    (pf', _, essences) = runRWS (descendBiM refactorBlocks pf) r False
+    (pf', _, _) = runRWS (descendBiM refactorBlocks pf) r False
 
 refactorBlocks :: [F.Block DA] -> RefactorM [F.Block DA]
 refactorBlocks = fmap concat . mapM refactorBlock
@@ -550,24 +550,25 @@
 
             -- Process each dimension and return the AST-blocks that define the derived type.
             eachDim :: [F.DimensionDeclarator DA] -> Int -> [(Int, F.TypeSpec DA)] -> [F.Block DA]
-            eachDim dimList maxDim ((dim, F.TypeSpec _ _ (F.TypeCustom tyName) _):(_, nextTy):rest)
+            eachDim dimList' maxDim' ((dim, F.TypeSpec _ _ (F.TypeCustom tyName) _):(_, nextTy):rest)
               | Just (Essence{..}:_) <- fmap S.toList $ M.lookup (var, dim) ddtrSMap = let
                   mInit | null rest = declInitialiser decl
                         | otherwise = Nothing
-                  dimDeclAList = F.AList a ss $ drop dim dimList
-                  eachLabel (n, lab)
-                    | maxDim == dim &&
-                      dim < length dimList = F.DeclArray a ss (FA.genVar a ss lab) dimDeclAList Nothing mInit
-                    | otherwise            = F.DeclVariable a ss (FA.genVar a ss lab) Nothing mInit
+                  dimDeclAList = F.AList a ss $ drop dim dimList'
+                  eachLabel (_, lab')
+                    | maxDim' == dim &&
+                      dim < length dimList' = F.DeclArray a ss (FA.genVar a ss lab') dimDeclAList Nothing mInit
+                    | otherwise             = F.DeclVariable a ss (FA.genVar a ss lab') Nothing mInit
                   labelDecls = map eachLabel . sort $ IM.toList essLabelMap
                   in [ F.BlStatement a'' ss' Nothing (F.StType stA stSS Nothing tyName)
                      , F.BlStatement a'' ss' Nothing (F.StDeclaration stA stSS nextTy attrs'' (F.AList alA alSS labelDecls))
                      , F.BlStatement a'' ss' Nothing (F.StEndType stA stSS Nothing) ]
             eachDim _ _ _ = []
-
             in (concat . reverse $ map (eachDim dimList maxDim) (List.tails $ dimTypes ++ [(0, ty)])) ++
                -- The declaration of the variable under the new derived type:
                [F.BlStatement a'' ss' lab (F.StDeclaration stA stSS ty' attrs'' (F.AList alA alSS [decl' dimDeclAList']))]
+          | otherwise = []
+
     let aRem = onOrigAnnotation (\ orig -> orig { deleteNode = null declsRem }) a'
     return $ -- Reinsert any other variables, with the refactored ones removed from the list.
              [F.BlStatement aRem ss lab (F.StDeclaration stA stSS ty attrs (F.AList alA alSS (map snd declsRem)))] ++
@@ -611,15 +612,15 @@
       , list' <- groupBy ((==) `on` SE.isLeft) list
       , e'    <- foldl' rewrite e1 list'             -> put True >> return e'
         where
-          ixLookup dim ix@(F.IxSingle ixA ixS Nothing e)
-            | Just (FAD.ConstInt i) <- FA.constExp (F.getAnnotation e)
+          ixLookup dim (F.IxSingle ixA ixS Nothing eIdx)
+            | Just (FAD.ConstInt i) <- FA.constExp (F.getAnnotation eIdx)
             , Just (Essence{..}:_)  <- fmap S.toList $ M.lookup (FA.varName e1, dim) smap
             , Just label            <- IM.lookup (fromIntegral i) essLabelMap = SE.Right (ixA, ixS, label)
           ixLookup _ ix = SE.Left ix
 
-          rewrite e l@(SE.Left _:_)                = F.ExpSubscript a s e (F.AList a s $ map SE.fromLeft l)
-          rewrite e (SE.Right (ixA, ixS, label):l) = rewrite (F.ExpDataRef a s e (F.ExpValue a s (F.ValVariable label))) l
-          rewrite e []                             = e
+          rewrite e' l@(SE.Left _:_)              = F.ExpSubscript a s e' (F.AList a s $ map SE.fromLeft l)
+          rewrite e' (SE.Right (_, _, label):l)   = rewrite (F.ExpDataRef a s e' (F.ExpValue a s (F.ValVariable label))) l
+          rewrite e' []                           = e'
     -- FIXME: either convert array slices, or regard that as a disqualifying effect
     _ -> return e
 
@@ -636,9 +637,9 @@
   -- check if this declaration has variables of interest
   F.BlStatement a ss _ F.StDeclaration{} | vars <- ofInterest b -> genComment vars ++ [b]
     where
-      ofInterest b = filter (flip M.member amap . fst) $
-        [ (FA.varName e, FA.srcName e) | F.DeclVariable _ _ e _ _ <- universeBi b :: [F.Declarator DA] ] ++
-        [ (FA.varName e, FA.srcName e) | F.DeclArray _ _ e _ _ _ <- universeBi b :: [F.Declarator DA] ]
+      ofInterest b' = filter (flip M.member amap . fst) $
+        [ (FA.varName e, FA.srcName e) | F.DeclVariable _ _ e _ _ <- universeBi b' :: [F.Declarator DA] ] ++
+        [ (FA.varName e, FA.srcName e) | F.DeclArray _ _ e _ _ _ <- universeBi b' :: [F.Declarator DA] ]
 
       genComment = map $ \ var ->
         F.BlComment newA newSS . F.Comment . buildCommentText mi space $ marker:genCommentText r var
@@ -650,7 +651,7 @@
       FU.SrcSpan lp _ = ss
       space = FU.posColumn lp - 1
   -- strip existing comment annotations
-  F.BlComment a ss c | isJust . ddtSpec . FA.prevAnnotation $ a -> [F.BlComment a' ss' $ F.Comment ""]
+  F.BlComment a ss _ | isJust . ddtSpec . FA.prevAnnotation $ a -> [F.BlComment a' ss' $ F.Comment ""]
     where
       FU.SrcSpan lp _ = ss
       ss' = deleteLine ss
@@ -677,6 +678,7 @@
         , starStr       <- if essStarred then "* " else " " ->
             " " ++ ddtShort ++ starStr ++ essTypeName ++ "(" ++ labs ++ ") :: " ++ srcName ++ "(dim=" ++ show dim ++ ")"
       _ -> error $ "genCommentText: unable to generate text for " ++ srcName
+  | otherwise = error $ "genCommentText: empty pmap entry and/or unable to lookup varName = " ++ varName
 
 --------------------------------------------------
 -- Check helpers
@@ -717,9 +719,9 @@
   -- if there's a problem
   | otherwise   = SE.Left $ IndexDupError tyname vinfo (nums List.\\ List.nub nums)
   where
-    labels'     = map (first read) labels
-    nums        = map fst labels'
-    noDups nums = length (List.nub nums) == length nums
+    labels'   = map (first read) labels
+    nums      = map fst labels'
+    noDups ns = length (List.nub ns) == length ns
 
 -- | Create an essence from array access information derived in a
 -- file, assuming some default names and labels.
diff --git a/src/Camfort/Specification/DerivedDataType/Parser.y b/src/Camfort/Specification/DerivedDataType/Parser.y
--- a/src/Camfort/Specification/DerivedDataType/Parser.y
+++ b/src/Camfort/Specification/DerivedDataType/Parser.y
@@ -9,6 +9,7 @@
   ) where
 
 import Camfort.Specification.Parser (mkParser, SpecParser)
+import Control.DeepSeq
 import Control.Monad.Except (throwError)
 import Data.Binary (Binary)
 import Data.Char (isLetter, isNumber, isAlphaNum, toLower)
@@ -65,6 +66,7 @@
           , ddtStLabels   :: [(String, String)]
           , ddtStVarDims  :: [(String, Int)] }
   deriving (Data, Eq, Show, Generic)
+instance NFData DDTStatement
 instance Binary DDTStatement
 
 data DDTParseError
diff --git a/src/Camfort/Specification/Hoare.hs b/src/Camfort/Specification/Hoare.hs
--- a/src/Camfort/Specification/Hoare.hs
+++ b/src/Camfort/Specification/Hoare.hs
@@ -124,32 +124,29 @@
 -}
 module Camfort.Specification.Hoare (check, HoareCheckResults(..), PrimReprOption(..)) where
 
-import           Control.Monad.Except
-import           Data.List                                 (intersperse)
-
-import qualified Language.Fortran.Analysis                 as FA
-import qualified Language.Fortran.Analysis.BBlocks         as FAB
-import qualified Language.Fortran.Analysis.Renaming        as FAR
-import qualified Language.Fortran.AST                      as F
-import qualified Language.Fortran.Util.Position            as F
-
 import           Camfort.Analysis
 import           Camfort.Analysis.Annotations
-import           Camfort.Analysis.ModFile
-import           Camfort.Helpers
-import           Camfort.Input
 import           Camfort.Specification.Hoare.Annotation
 import           Camfort.Specification.Hoare.CheckBackend
 import           Camfort.Specification.Hoare.CheckFrontend
-import           Camfort.Specification.Hoare.Parser
+import           Control.DeepSeq
+import           Data.List                                 (intersperse)
+import qualified Language.Fortran.AST                      as F
+import qualified Language.Fortran.Analysis                 as FA
+import qualified Language.Fortran.Analysis.BBlocks         as FAB
+import qualified Language.Fortran.Analysis.Renaming        as FAR
 import           Language.Fortran.Model.Repr.Prim
 
+
 --------------------------------------------------------------------------------
 --  Types
 --------------------------------------------------------------------------------
 
 newtype HoareCheckResults = HoareCheckResults [HoareCheckResult]
 
+instance NFData HoareCheckResults where
+  rnf _ = ()
+
 instance ExitCodeOfReport HoareCheckResults where
   exitCodeOf (HoareCheckResults rs) = exitCodeOfSet rs
 
@@ -186,8 +183,8 @@
   FAB.analyseBBlocks . FAR.analyseRenames .
   FA.initAnalysis . fmap hoareAnn0
 
-defaultSymSpec :: PrimReprSpec
-defaultSymSpec = prsIdealized
+-- defaultSymSpec :: PrimReprSpec
+-- defaultSymSpec = prsIdealized
 
 fromPrimReprOption :: PrimReprOption -> PrimReprSpec
 fromPrimReprOption PROIdealized = prsIdealized
@@ -197,19 +194,19 @@
 --  Testsing
 --------------------------------------------------------------------------------
 
-testOn :: FilePath -> IO ()
-testOn fp = do
-  (mfs, pfsSources) <- loadModAndProgramFiles Nothing simpleCompiler () fp fp []
-  describePerFileAnalysis
-    "invariant checking"
-    (check PROIdealized)
-    (logOutputStd True)
-    LogDebug
-    False
-    mfs
-    pfsSources
-  return ()
+-- testOn :: FilePath -> IO ()
+-- testOn fp = do
+--   (mfs, pfsSources) <- loadModAndProgramFiles Nothing simpleCompiler () fp fp []
+--   describePerFileAnalysis
+--     "invariant checking"
+--     (check PROIdealized)
+--     (logOutputStd True)
+--     LogDebug
+--     False
+--     mfs
+--     pfsSources
+--   return ()
 
-testHoare = do
-  testOn "camfort/samples/invariants/arrays.f90"
-  testOn "camfort/samples/invariants/invariants.f90"
+-- testHoare = do
+--   testOn "camfort/samples/invariants/arrays.f90"
+--   testOn "camfort/samples/invariants/invariants.f90"
diff --git a/src/Camfort/Specification/Hoare/CheckBackend.hs b/src/Camfort/Specification/Hoare/CheckBackend.hs
--- a/src/Camfort/Specification/Hoare/CheckBackend.hs
+++ b/src/Camfort/Specification/Hoare/CheckBackend.hs
@@ -27,7 +27,7 @@
 import           Control.Monad.Reader
 import           Control.Monad.Fail
 import           Control.Monad.State.Strict
-import           Control.Monad.Writer.CPS
+import           Control.Monad.Writer.Lazy
 import           Control.Monad.Trans.Maybe
 import           Data.Data                              (Data)
 import           Data.Foldable                          (foldlM)
diff --git a/src/Camfort/Specification/Hoare/CheckFrontend.hs b/src/Camfort/Specification/Hoare/CheckFrontend.hs
--- a/src/Camfort/Specification/Hoare/CheckFrontend.hs
+++ b/src/Camfort/Specification/Hoare/CheckFrontend.hs
@@ -27,7 +27,7 @@
 import           Control.Applicative                      (liftA2)
 import           Control.Exception
 import           Control.Lens
-import           Control.Monad.Writer.CPS                 hiding (Product)
+import           Control.Monad.Writer.Lazy                hiding (Product)
 import           Data.Generics.Uniplate.Operations
 import           Data.Map                                 (Map)
 import qualified Data.Map                                 as Map
@@ -51,6 +51,8 @@
 import           Camfort.Specification.Hoare.Parser.Types (HoareParseError)
 import           Camfort.Specification.Hoare.Syntax
 
+import           Control.DeepSeq
+
 --------------------------------------------------------------------------------
 --  Invariant Checking
 --------------------------------------------------------------------------------
@@ -92,8 +94,14 @@
   | InvalidPUConditions F.ProgramUnitName [SpecOrDecl InnerHA]
   | BackendError HoareBackendError
 
+instance NFData HoareFrontendError where
+  rnf _ = ()
+
 data HoareFrontendWarning
   = OrphanDecls F.ProgramUnitName
+
+instance NFData HoareFrontendWarning where
+  rnf _ = ()
 
 instance Describe HoareFrontendError where
   describeBuilder = \case
diff --git a/src/Camfort/Specification/Stencils.hs b/src/Camfort/Specification/Stencils.hs
--- a/src/Camfort/Specification/Stencils.hs
+++ b/src/Camfort/Specification/Stencils.hs
@@ -18,29 +18,22 @@
 module Camfort.Specification.Stencils
  (infer, check, synth) where
 
-import Control.Arrow ((***), first, second)
-import Data.Maybe (catMaybes)
-
 import           Camfort.Analysis
 import           Camfort.Analysis.Annotations
-import           Camfort.Helpers
 import           Camfort.Specification.Stencils.Analysis (StencilsAnalysis)
 import qualified Camfort.Specification.Stencils.Annotation as SA
-import           Camfort.Specification.Stencils.CheckFrontend hiding (LogLine)
+import           Camfort.Specification.Stencils.CheckFrontend
 import           Camfort.Specification.Stencils.InferenceFrontend
-import           Camfort.Specification.Stencils.Synthesis
-
+import           Control.DeepSeq
+import           Data.Maybe (catMaybes)
 import qualified Language.Fortran.AST as F
 import qualified Language.Fortran.Analysis as FA
-import qualified Language.Fortran.Util.ModFile as MF
-import qualified Language.Fortran.Analysis.Renaming as FAR
 import qualified Language.Fortran.Analysis.BBlocks as FAB
 import qualified Language.Fortran.Analysis.DataFlow as FAD
-
-import Data.List
-
+import qualified Language.Fortran.Analysis.Renaming as FAR
 
 -- | Helper for retrieving analysed blocks.
+getBlocks :: F.ProgramFile A -> F.ProgramFile SA.SA
 getBlocks = FAD.analyseConstExps . FAB.analyseBBlocks . FAR.analyseRenames . FA.initAnalysis . fmap SA.mkStencilAnnotation
 
 --------------------------------------------------
@@ -52,7 +45,7 @@
       -> F.ProgramFile Annotation
       -> StencilsAnalysis StencilsReport
 infer useEval marker pf =
-  (StencilsReport . map (F.pfGetFilename pf,)) <$> stencilInference useEval marker (getBlocks pf)
+  (force . StencilsReport . map (F.pfGetFilename pf,)) <$> stencilInference useEval marker (getBlocks pf)
 
 --------------------------------------------------
 --         Stencil specification synthesis      --
@@ -65,7 +58,7 @@
 synth marker pfs = do
   syntheses <- unzip <$> traverse buildOutput pfs
   logInfo' pfs $ describe . normaliseMsg . fst $ syntheses
-  pure (catMaybes $ snd syntheses)
+  pure . catMaybes $ snd syntheses
   where
     buildOutput :: F.ProgramFile A -> StencilsAnalysis ((String, String), Maybe (F.ProgramFile Annotation))
     buildOutput pf = do
@@ -102,7 +95,7 @@
 --------------------------------------------------
 
 check :: F.ProgramFile Annotation -> StencilsAnalysis CheckResult
-check = stencilChecking . getBlocks
+check = fmap force . stencilChecking . getBlocks
 
 -- Local variables:
 -- mode: haskell
diff --git a/src/Camfort/Specification/Stencils/Analysis.hs b/src/Camfort/Specification/Stencils/Analysis.hs
--- a/src/Camfort/Specification/Stencils/Analysis.hs
+++ b/src/Camfort/Specification/Stencils/Analysis.hs
@@ -13,8 +13,6 @@
   , compileStencils
   ) where
 
-import qualified Language.Fortran.Util.ModFile as MF
-
 import           Camfort.Analysis
 import           Camfort.Analysis.ModFile      (MFCompiler, simpleCompiler)
 
diff --git a/src/Camfort/Specification/Stencils/CheckFrontend.hs b/src/Camfort/Specification/Stencils/CheckFrontend.hs
--- a/src/Camfort/Specification/Stencils/CheckFrontend.hs
+++ b/src/Camfort/Specification/Stencils/CheckFrontend.hs
@@ -29,15 +29,17 @@
   , existingStencils
   ) where
 
-import Control.Monad.IO.Class (MonadIO(..))
-import Control.Monad.Reader (MonadReader, ReaderT, asks, runReaderT)
-import Control.Monad.State.Strict
-import Control.Monad.Writer.CPS hiding (Product)
-import Data.Function (on)
-import Data.Generics.Uniplate.Operations
-import Data.List (intercalate, sort, union)
-import Data.Maybe
+import           Prelude hiding (span)
 
+import           Control.DeepSeq
+import           Control.Monad.Reader (ReaderT, asks, runReaderT)
+import           Control.Monad.State.Strict hiding (state)
+import           Control.Monad.Writer.Lazy hiding (Product)
+import           Data.Function (on)
+import           Data.Generics.Uniplate.Operations
+import           Data.List (intercalate, sort, union)
+import           Data.Maybe
+
 import           Camfort.Analysis
 import           Camfort.Analysis.Annotations
 import           Camfort.Analysis.CommentAnnotator
@@ -52,15 +54,16 @@
 import           Camfort.Specification.Stencils.Parser.Types (reqRegions)
 import           Camfort.Specification.Stencils.Syntax
 
-import qualified Language.Fortran.AST               as F
-import qualified Language.Fortran.Analysis          as FA
-import qualified Language.Fortran.Analysis.BBlocks  as FAB
+import qualified Language.Fortran.AST as F
+import qualified Language.Fortran.Analysis as FA
+import qualified Language.Fortran.Analysis.BBlocks as FAB
 import qualified Language.Fortran.Analysis.DataFlow as FAD
-import qualified Language.Fortran.Util.ModFile      as MF
-import qualified Language.Fortran.Util.Position     as FU
+import qualified Language.Fortran.Util.Position as FU
 
 -- TODO: Replace instances of this with logging of errors and warnings
 newtype CheckResult = CheckResult [StencilResult]
+instance NFData CheckResult where
+  rnf _ = ()
 instance ExitCodeOfReport CheckResult where
   exitCodeOf (CheckResult rs) = exitCodeOfSet rs
 
@@ -184,7 +187,7 @@
 unusedRegion srcSpan var = SCWarn $ UnusedRegion srcSpan var
 
 specOkay :: FU.SrcSpan -> Specification -> Variable -> FU.SrcSpan -> StencilResult
-specOkay spanSpec@(FU.SrcSpan (FU.Position o1 _ _ _ _) (FU.Position o2 _ _ _ _)) spec var spanBody@(FU.SrcSpan (FU.Position o1' _ _ _ _) (FU.Position o2' _ _ _ _)) =
+specOkay spanSpec spec var spanBody =
   SCOkay { scSpan      = spanSpec
          , scSpec      = spec
          , scBodySpan  = spanBody
@@ -283,12 +286,12 @@
 
 -- | Remove the given regions variables from the tracked unused regions.
 informRegionsUsed :: [Variable] -> Checker ()
-informRegionsUsed regions = modify
-  (\s -> s { usedRegions = usedRegions s `union` regions })
+informRegionsUsed rs = modify
+  (\s -> s { usedRegions = usedRegions s `union` rs })
 
 -- | Start tracking a region.
 addRegionToTracked :: FU.SrcSpan -> Variable -> Checker ()
-addRegionToTracked srcSpan@(FU.SrcSpan (FU.Position o1 _ _ _ _) (FU.Position o2 _ _ _ _)) r =
+addRegionToTracked srcSpan r =
   modify (\s -> s { regions = (srcSpan, r) : regions s })
 
 -- | True if the region name is already tracked.
@@ -407,7 +410,7 @@
   -- Work out whether this is a stencil (non empty LHS indices) or not
   let (subs, isStencil) = case maybeSubs of
                              Nothing -> ([], False)
-                             Just subs -> (subs, True)
+                             Just subs' -> (subs', True)
 
   -- Get the induction variables relative to the current block
   ivmap <- fmap ivMap get
diff --git a/src/Camfort/Specification/Stencils/Consistency.hs b/src/Camfort/Specification/Stencils/Consistency.hs
--- a/src/Camfort/Specification/Stencils/Consistency.hs
+++ b/src/Camfort/Specification/Stencils/Consistency.hs
@@ -35,7 +35,7 @@
       (Mult _, Once _) -> Inconsistent
         "Specification lacks readOnce, but the indices are unique."
   where
-    specModel :: Multiplicity (Approximation (UnionNF n (Interval Standard)))
+    specModel :: Multiplicity (Approximation (UnionNF n (Interval 'Standard)))
     specModel =
       case sequence $ (sequence . fmap (regionsToIntervals nOfDims)) <$> mult of
         Right model -> model
@@ -46,7 +46,7 @@
 
 -- | This is the actual consistency check using set comparison supplied in
 -- the model.
-consistent' :: Approximation (UnionNF n (Interval Standard))
+consistent' :: Approximation (UnionNF n (Interval 'Standard))
             -> UnionNF n Offsets
             -> ConsistencyResult
 consistent' (Exact unf) ixs =
diff --git a/src/Camfort/Specification/Stencils/DenotationalSemantics.hs b/src/Camfort/Specification/Stencils/DenotationalSemantics.hs
--- a/src/Camfort/Specification/Stencils/DenotationalSemantics.hs
+++ b/src/Camfort/Specification/Stencils/DenotationalSemantics.hs
@@ -18,7 +18,7 @@
 -- 1. If finite interval, all have "lower bound <= 0 <= upper bound";
 -- 2. No dimensionality of 0; (insured by dep. type);
 -- 3. All unioned interval lists are of equal length (insured by dep.  type).
-intervalsToRegions :: UnionNF (V.S n) (Interval Standard)
+intervalsToRegions :: UnionNF ('V.S n) (Interval 'Standard)
                    -> Either String Spatial
 intervalsToRegions as = do
     sums <- mapM toProd
@@ -36,23 +36,24 @@
           IntervHoled m n p ->
             asymmetryElim (V.replace ix (IntervHoled m 0 p) ints) SG.<>
             asymmetryElim (V.replace ix (IntervHoled 0 n p) ints)
+          _ -> error "intervalsToRegions: asymmetryElim: case ints V.!! ix of ..."
       | otherwise = return ints
     findAsymmetry =
       V.findIndex $ \case
         (IntervHoled m n _) -> m /= 0 && n /= 0 && m /= -n
         _ -> False
 
-    toProd :: V.Vec n (Interval Standard) -> Either String RegionProd
+    toProd :: V.Vec n (Interval 'Standard) -> Either String RegionProd
     toProd ints =
       fmap Product $ mapM convert
                    . filter (isNonInf . fst)
                    $ zip (V.toList ints) [0..]
 
-    isNonInf :: Interval Standard -> Bool
+    isNonInf :: Interval 'Standard -> Bool
     isNonInf IntervInfinite = False
     isNonInf _ = True
 
-    convert :: (Interval Standard, Int) -> Either String Region
+    convert :: (Interval 'Standard, Int) -> Either String Region
     convert (IntervHoled 0 0 False, _) =
       Left "Empty set cannot be realised as a region."
     convert (IntervHoled 0 0 True, ix) = return $ Centered 0 (ix + 1) True
@@ -68,13 +69,13 @@
 regionsToIntervals :: forall n .
                       V.Natural n
                    -> Spatial
-                   -> Either String (UnionNF n (Interval Standard))
+                   -> Either String (UnionNF n (Interval 'Standard))
 regionsToIntervals nOfDims (Spatial (Sum prods))
     | null prods = Left "Empty region sum"
     | otherwise =
       fmap SG.sconcat . sequence . fmap convert . NE.fromList $ prods
   where
-    convert :: RegionProd -> Either String (UnionNF n (Interval Standard))
+    convert :: RegionProd -> Either String (UnionNF n (Interval 'Standard))
     convert (Product rs)
       | null rs = Left "Empty region product"
       | otherwise = Right $ meets1 . NE.fromList . map convert' $ rs
@@ -85,10 +86,10 @@
         Backward dep dim p -> (dim-1, IntervHoled (- fromIntegral dep) 0 p)
         Centered dep dim p -> (dim-1, IntervHoled (- fromIntegral dep) (fromIntegral dep) p)
 
-    proto :: forall n .
-             V.Natural n
-          -> (Int, Interval Standard)
-          -> V.Vec n (Interval Standard)
+    proto :: forall n' .
+             V.Natural n'
+          -> (Int, Interval 'Standard)
+          -> V.Vec n' (Interval 'Standard)
     proto V.Zero _ = V.Nil
     proto (V.Succ n) (i, interv) = V.Cons
       (if i == 0 then interv else IntervInfinite)
diff --git a/src/Camfort/Specification/Stencils/Generate.hs b/src/Camfort/Specification/Stencils/Generate.hs
--- a/src/Camfort/Specification/Stencils/Generate.hs
+++ b/src/Camfort/Specification/Stencils/Generate.hs
@@ -35,7 +35,7 @@
 
 import           Control.Monad (void, when, zipWithM)
 import           Control.Monad.State.Strict (State, get, put, runState)
-import           Control.Monad.Writer.CPS (WriterT, runWriterT, tell)
+import           Control.Monad.Writer.Lazy (WriterT, runWriterT, tell)
 import           Control.Monad.Reader (ReaderT, runReaderT, asks)
 import           Data.Data (Data)
 import           Data.Foldable (foldrM)
@@ -50,10 +50,8 @@
 import qualified Language.Fortran.AST               as F
 import qualified Language.Fortran.Analysis          as FA
 import qualified Language.Fortran.Analysis.DataFlow as FAD
-import           Language.Fortran.Util.ModFile (ModFiles)
 import qualified Language.Fortran.Util.Position     as FU
 
-import           Camfort.Analysis
 import           Camfort.Helpers (collect)
 import qualified Camfort.Helpers.Vec as V
 import           Camfort.Specification.Stencils.Annotation ()
diff --git a/src/Camfort/Specification/Stencils/InferenceBackend.hs b/src/Camfort/Specification/Stencils/InferenceBackend.hs
--- a/src/Camfort/Specification/Stencils/InferenceBackend.hs
+++ b/src/Camfort/Specification/Stencils/InferenceBackend.hs
@@ -42,7 +42,7 @@
 
 type Span a = (a, a)
 
-spansToApproxSpatial :: [ Span (V.Vec (V.S n) Int) ]
+spansToApproxSpatial :: [ Span (V.Vec ('V.S n) Int) ]
                        -> Either String (Approximation Spatial)
 spansToApproxSpatial spans = sequence . fmap intervalsToRegions $ approxUnion
   where
@@ -50,8 +50,8 @@
       toApprox . map (fmap absRepToInf . transposeVecInterval) $ spans
     approxUnion = fmap (optimise . joins1 . NE.fromList . map return) approxVecs
 
-    toApprox :: [ V.Vec n (Interval Arbitrary) ]
-             -> Approximation [ V.Vec n (Interval Standard) ]
+    toApprox :: [ V.Vec n (Interval 'Arbitrary) ]
+             -> Approximation [ V.Vec n (Interval 'Standard) ]
     toApprox vs
       | parts <- (elongatedPartitions . map approxVec) vs =
           case parts of
@@ -64,14 +64,14 @@
       partition $ \case { Exact{} -> True; Bound{} -> False }
 
     -- TODO: DELETE AS SOON AS POSSIBLE
-    absRepToInf :: Interval Arbitrary -> Interval Arbitrary
+    absRepToInf :: Interval 'Arbitrary -> Interval 'Arbitrary
     absRepToInf interv@(IntervArbitrary a b)
       | fromIntegral a == absoluteRep = IntervInfiniteArbitrary
       | fromIntegral b == absoluteRep = IntervInfiniteArbitrary
       | otherwise = interv
     absRepToInf interv = interv
 
-    transposeVecInterval :: Span (V.Vec n Int) -> V.Vec n (Interval Arbitrary)
+    transposeVecInterval :: Span (V.Vec n Int) -> V.Vec n (Interval 'Arbitrary)
     transposeVecInterval (us, vs) = V.zipWith IntervArbitrary us vs
 
 mkTrivialSpan :: V.Vec n Int -> Span (V.Vec n Int)
@@ -167,8 +167,6 @@
   = True
 containedWithin (V.Cons l1 ls1, V.Cons u1 us1) (V.Cons l2 ls2, V.Cons u2 us2)
   = (l2 <= l1 && u1 <= u2) && containedWithin (ls1, us1) (ls2, us2)
-containedWithin _ _
-  = False
 
 -- Local variables:
 -- mode: haskell
diff --git a/src/Camfort/Specification/Stencils/InferenceFrontend.hs b/src/Camfort/Specification/Stencils/InferenceFrontend.hs
--- a/src/Camfort/Specification/Stencils/InferenceFrontend.hs
+++ b/src/Camfort/Specification/Stencils/InferenceFrontend.hs
@@ -29,46 +29,35 @@
   , StencilsReport(..)
   ) where
 
-import Control.Monad.RWS.CPS
-import Control.Monad.Writer.CPS
-
 import           Camfort.Analysis
 import           Camfort.Analysis.Annotations
 import           Camfort.Analysis.CommentAnnotator
-import           Camfort.Helpers (collect, descendReverseM, descendBiReverseM)
-import qualified Camfort.Helpers.Vec as V
-import           Camfort.Input
+import           Camfort.Helpers (descendReverseM, descendBiReverseM)
 import           Camfort.Specification.Stencils.Analysis (StencilsAnalysis)
 import           Camfort.Specification.Stencils.Annotation (SA)
 import qualified Camfort.Specification.Stencils.Annotation as SA
-import           Camfort.Specification.Stencils.CheckBackend (synToAst)
 import           Camfort.Specification.Stencils.CheckFrontend
   (CheckResult, existingStencils, stencilChecking)
 import           Camfort.Specification.Stencils.Generate
-import           Camfort.Specification.Stencils.InferenceBackend
-import           Camfort.Specification.Stencils.Model
 import qualified Camfort.Specification.Stencils.Parser as Parser
-import           Camfort.Specification.Stencils.Parser.Types (SpecInner)
 import           Camfort.Specification.Stencils.Syntax
 import qualified Camfort.Specification.Stencils.Synthesis as Synth
-
-import qualified Language.Fortran.AST               as F
-import qualified Language.Fortran.Analysis          as FA
-import qualified Language.Fortran.Analysis.BBlocks  as FAB
-import qualified Language.Fortran.Analysis.DataFlow as FAD
-import qualified Language.Fortran.Util.Position     as FU
-
-import Data.Data
-import Data.Foldable
-import Data.Generics.Uniplate.Operations
-import Data.Graph.Inductive.Graph hiding (isEmpty)
+import           Control.DeepSeq
+import           Control.Monad.RWS.Lazy hiding (state)
+import           Control.Monad.Writer.Lazy
+import           Data.Foldable
+import           Data.Generics.Uniplate.Operations
 import qualified Data.Map as M
-import qualified Data.Set as S
-import Data.Maybe
-import Data.Monoid ((<>))
+import           Data.Maybe
+import qualified Language.Fortran.AST as F
+import qualified Language.Fortran.Analysis as FA
+import qualified Language.Fortran.Analysis.BBlocks as FAB
+import qualified Language.Fortran.Analysis.DataFlow as FAD
+import qualified Language.Fortran.Util.Position as FU
+import           Prelude hiding (span, log)
 
 data InferState = IS {
-     ivMap        :: FAD.InductionVarMapByASTBlock
+     _ivMap       :: FAD.InductionVarMapByASTBlock
    , visitedNodes :: [Int]}
 
 data InferEnv = IE
@@ -89,6 +78,10 @@
 type LogLine = (FU.SrcSpan, Either [([Variable], Specification)] (String,Variable))
 
 data StencilsReport = StencilsReport [(String, LogLine)] -- ^ (filename, logged stencil)
+
+instance NFData StencilsReport where
+  rnf _ = ()
+
 instance ExitCodeOfReport StencilsReport where
   exitCodeOf _ = 0
 
@@ -153,11 +146,11 @@
 -- | Attempt to convert a 'Parser.Specification' into a 'Specification'.
 --
 -- Only performs conversions for spatial specifications.
-specToSynSpec :: SpecInner -> Maybe Specification
-specToSynSpec spec = let ?renv = [] in
-                       case synToAst spec of
-                         Left err -> Nothing
-                         Right x  -> Just x
+-- specToSynSpec :: SpecInner -> Maybe Specification
+-- specToSynSpec spec = let ?renv = [] in
+--                        case synToAst spec of
+--                          Left _   -> Nothing
+--                          Right x  -> Just x
 
 -- | Main stencil inference code
 stencilInference :: Bool
@@ -212,9 +205,9 @@
             beMap = FAD.genBackEdgeMap (FAD.dominators gr) $ FA.bbgrGr gr
 
             -- identify every loop by its back-edge
-            ivMap = FAD.genInductionVarMapByASTBlock beMap gr
+            ivmap = FAD.genInductionVarMapByASTBlock beMap gr
 
-        (pu', log) <- lift $ runInferer checkRes useEval doSynth marker mi ivMap flTo pum
+        (pu', log) <- lift $ runInferer checkRes useEval doSynth marker mi ivmap flTo pum
         tell log
         pure pu'
     perPU pu = pure pu
@@ -262,6 +255,7 @@
 -- the following code is inside a do-loop since we only target
 -- array computations inside loops.
 
+perBlockInfer' :: Bool -> F.Block SA -> Inferer (F.Block SA)
 perBlockInfer' _ b@F.BlComment{} = pure b
 
 perBlockInfer' inDo b@(F.BlStatement ann span@(FU.SrcSpan lp _) _ stmnt) = do
@@ -308,8 +302,8 @@
         Just subs ->
           -- Left-hand side is a subscript-by relative index or by a range
           case neighbourIndex ivmap subs of
-            Just lhs -> genSpecsAndReport span lhs b
-            Nothing  -> do
+            Just lhs' -> genSpecsAndReport span lhs' b
+            Nothing   -> do
               whenEval $
                 tell [(span , Right ("EVALMODE: LHS is an array\
                                      \ subscript we can't handle \
@@ -318,7 +312,7 @@
         -- Not an assign we are interested in
         _ -> pure []
 
-perBlockInfer' _ b@(F.BlDo ann span lab cname lab' mDoSpec body tlab) = do
+perBlockInfer' _ (F.BlDo ann span lab cname lab' mDoSpec body tlab) = do
   -- descend into the body of the do-statement (in reverse order)
   body' <- mapM (descendBiReverseM (perBlockInfer' True)) (reverse body)
   return $ F.BlDo ann span lab cname lab' mDoSpec (reverse body') tlab
diff --git a/src/Camfort/Specification/Stencils/Model.hs b/src/Camfort/Specification/Stencils/Model.hs
--- a/src/Camfort/Specification/Stencils/Model.hs
+++ b/src/Camfort/Specification/Stencils/Model.hs
@@ -50,10 +50,11 @@
                                             , Peelable(..)
                                             ) where
 
+import           Prelude hiding (pred)
+
 import qualified Control.Monad as CM
 
 import           Algebra.Lattice
-import           Data.Semigroup
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Set as S
 import           Data.Foldable
@@ -97,27 +98,21 @@
   member _ _ = True
 
   compile (Offsets s) i = i `sElem` map fromIntegral (S.toList s)
-  compile SetOfIntegers _ = true
+  compile SetOfIntegers _ = sTrue
 
-instance JoinSemiLattice Offsets where
+instance Lattice Offsets where
   (Offsets s) \/ (Offsets s') = Offsets $ s `S.union` s'
   _ \/ _ = SetOfIntegers
-
-instance MeetSemiLattice Offsets where
   (Offsets s) /\ (Offsets s') = Offsets $ s `S.intersection` s'
   off@Offsets{} /\ _ = off
   _ /\ o = o
 
-instance Lattice Offsets
-
 instance BoundedJoinSemiLattice Offsets where
   bottom = Offsets S.empty
 
 instance BoundedMeetSemiLattice Offsets where
   top = SetOfIntegers
 
-instance BoundedLattice Offsets
-
 --------------------------------------------------------------------------------
 -- Interval as defined in the paper
 --------------------------------------------------------------------------------
@@ -128,19 +123,19 @@
 -- 1. The first num. param. is less than the second;
 -- 2. For holed intervals, first num. param. <= 0 <= second num. param.;
 data Interval a where
-  IntervArbitrary :: Int -> Int -> Interval Arbitrary
-  IntervInfiniteArbitrary :: Interval Arbitrary
-  IntervHoled     :: Int64 -> Int64 -> Bool -> Interval Standard
-  IntervInfinite  :: Interval Standard
+  IntervArbitrary :: Int -> Int -> Interval 'Arbitrary
+  IntervInfiniteArbitrary :: Interval 'Arbitrary
+  IntervHoled     :: Int64 -> Int64 -> Bool -> Interval 'Standard
+  IntervInfinite  :: Interval 'Standard
 
 deriving instance Eq (Interval a)
 
-instance Show (Interval Standard) where
+instance Show (Interval 'Standard) where
   show IntervInfinite = "IntervInfinite"
   show (IntervHoled lb up p) =
     "Interv [" ++ show lb ++ "," ++ show up ++ "]^" ++ show p
 
-approxInterv :: Interval Arbitrary -> Approximation (Interval Standard)
+approxInterv :: Interval 'Arbitrary -> Approximation (Interval 'Standard)
 approxInterv (IntervArbitrary a b)
   | a > b = error
     "Interval condition violated: lower bound is bigger than the upper bound."
@@ -156,22 +151,22 @@
 approxInterv IntervInfiniteArbitrary = Exact IntervInfinite
 
 approxVec :: forall n .
-             V.Vec n (Interval Arbitrary)
-          -> Approximation (V.Vec n (Interval Standard))
+             V.Vec n (Interval 'Arbitrary)
+          -> Approximation (V.Vec n (Interval 'Standard))
 approxVec v =
   case findApproxIntervs stdVec of
     ([],_) -> Exact . fmap fromExact $ stdVec
     _      -> Bound Nothing (Just $ upperBound <$> stdVec)
   where
-    stdVec :: V.Vec n (Approximation (Interval Standard))
+    stdVec :: V.Vec n (Approximation (Interval 'Standard))
     stdVec = fmap approxInterv v
 
-    findApproxIntervs :: forall n . V.Vec n (Approximation (Interval Standard))
+    findApproxIntervs :: forall n' . V.Vec n' (Approximation (Interval 'Standard))
                       -> ([ Int ], [ Int ])
-    findApproxIntervs v = findApproxIntervs' 0 v ([],[])
+    findApproxIntervs v' = findApproxIntervs' 0 v' ([],[])
 
-    findApproxIntervs' :: forall n . Int
-                       -> V.Vec n (Approximation (Interval Standard))
+    findApproxIntervs' :: forall n' . Int
+                       -> V.Vec n' (Approximation (Interval 'Standard))
                        -> ([ Int ], [ Int ])
                        -> ([ Int ], [ Int ])
     findApproxIntervs' _ V.Nil acc = acc
@@ -181,9 +176,9 @@
           Bound{} -> (i:bixs, eixs)
           Exact{} -> (bixs, i:eixs)
 
-instance Container (Interval Standard) where
-  type MemberTyp (Interval Standard) = Int64
-  type CompTyp (Interval Standard) = SInt64
+instance Container (Interval 'Standard) where
+  type MemberTyp (Interval 'Standard) = Int64
+  type CompTyp (Interval 'Standard) = SInt64
 
   member 0 (IntervHoled _ _ b) = b
   member i (IntervHoled a b _) = i >= a && i <= b
@@ -191,31 +186,27 @@
 
   compile (IntervHoled i1 i2 b) i
     | b = inRange i range
-    | otherwise = inRange i range &&& i ./= 0
+    | otherwise = inRange i range .&& i ./= 0
     where
       range = (fromIntegral i1, fromIntegral i2)
-  compile IntervInfinite _ = true
+  compile IntervInfinite _ = sTrue
 
-instance JoinSemiLattice (Interval Standard) where
+instance Lattice (Interval 'Standard) where
   (IntervHoled lb ub noHole) \/ (IntervHoled lb' ub' noHole') =
     IntervHoled (min lb lb') (max ub ub') (noHole || noHole')
   _ \/ _ = top
-
-instance MeetSemiLattice (Interval Standard) where
   (IntervHoled lb ub noHole) /\ (IntervHoled lb' ub' noHole') =
     IntervHoled (max lb lb') (min ub ub') (noHole && noHole')
   int@IntervHoled{} /\ _ = int
   _ /\ int = int
 
-instance Lattice (Interval Standard)
-
-instance BoundedJoinSemiLattice (Interval Standard) where
+instance BoundedJoinSemiLattice (Interval 'Standard) where
   bottom = IntervHoled 0 0 False
 
-instance BoundedMeetSemiLattice (Interval Standard) where
+instance BoundedMeetSemiLattice (Interval 'Standard) where
   top = IntervInfinite
 
-instance BoundedLattice (Interval Standard)
+-- instance BoundedLattice (Interval 'Standard)
 
 --------------------------------------------------------------------------------
 -- Union of cartesian products normal form
@@ -231,21 +222,17 @@
   type CompTyp (UnionNF n a) = V.Vec n (CompTyp a)
   member is = any (member' is)
     where
-      member' is space = and $ V.zipWith member is space
+      member' is' space = and $ V.zipWith member is' space
 
-  compile spaces is = foldr1 (|||) $ NE.map (`compile'` is) spaces
+  compile spaces is = foldr1 (.||) $ NE.map (`compile'` is) spaces
     where
-      compile' space is =
-        foldr' (\(set, i) -> (&&&) $ compile set i) true $ V.zip space is
+      compile' space is' =
+        foldr' (\(set, i) -> (.&&) $ compile set i) sTrue $ V.zip space is'
 
-instance JoinSemiLattice (UnionNF n a) where
+instance BoundedMeetSemiLattice a => Lattice (UnionNF n a) where
   oi \/ oi' = oi <> oi'
-
-instance BoundedLattice a => MeetSemiLattice (UnionNF n a) where
   (/\) = CM.liftM2 (V.zipWith (/\))
 
-instance BoundedLattice a => Lattice (UnionNF n a)
-
 unfCompare :: forall a b n . ( Container a,          Container b
                              , MemberTyp a ~ Int64,  MemberTyp b ~ Int64
                              , CompTyp a ~ SInt64,   CompTyp b ~ SInt64
@@ -257,7 +244,7 @@
       -- Tell the user if there was a hard proof error (e.g., if
       -- z3 is not installed/accessible).
       -- TODO: give more information
-      ThmResult (ProofError _ msgs) -> fail $ unlines msgs
+      ThmResult (ProofError _ msgs _) -> fail $ unlines msgs
       _ ->
         if modelExists thmRes
         then do
@@ -309,7 +296,7 @@
   SetOfIntegers <= Offsets{} = False
   _ <= SetOfIntegers = True
 
-instance PO.PartialOrd (Interval Standard) where
+instance PO.PartialOrd (Interval 'Standard) where
   (IntervHoled lb ub p) <= (IntervHoled lb' ub' p') =
     (p' || not p) && lb >= lb' && ub <= ub'
   IntervInfinite <= IntervHoled{} = False
@@ -318,7 +305,7 @@
 instance PO.PartialOrd a => PO.PartialOrd (V.Vec n a) where
   v <= v' = and $ V.zipWith (PO.<=) v v'
 
-optimise :: UnionNF n (Interval Standard) -> UnionNF n (Interval Standard)
+optimise :: UnionNF n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
 optimise = NE.fromList . maximas . fixedPointUnion . NE.toList
   where
     fixedPointUnion unf =
@@ -332,7 +319,7 @@
                 -> [ [ a ] ]
 sensibleGroupBy ord p l = nub . map (\el -> sortBy ord . filter (p el) $ l) $ l
 
-maximas :: [ V.Vec n (Interval Standard) ] -> [ V.Vec n (Interval Standard) ]
+maximas :: [ V.Vec n (Interval 'Standard) ] -> [ V.Vec n (Interval 'Standard) ]
 maximas = nub
         . fmap (head . PO.maxima)
         . sensibleGroupBy ord (PO.<=)
@@ -344,7 +331,7 @@
 -- The union is again a product of intervals that agrees with the original
 -- dimensions in all dimensions except the original differing one. At that
 -- point it is the union of intervals, which is itself still an interval.
-unionLemma :: [ V.Vec n (Interval Standard) ] -> [ V.Vec n (Interval Standard) ]
+unionLemma :: [ V.Vec n (Interval 'Standard) ] -> [ V.Vec n (Interval 'Standard) ]
 unionLemma = map (foldr1 (V.zipWith (\/)))
            . sensibleGroupBy (\a b -> if a == b then EQ else LT) agreeButOne
   where
diff --git a/src/Camfort/Specification/Stencils/PartialOrd.hs b/src/Camfort/Specification/Stencils/PartialOrd.hs
--- a/src/Camfort/Specification/Stencils/PartialOrd.hs
+++ b/src/Camfort/Specification/Stencils/PartialOrd.hs
@@ -29,9 +29,8 @@
 
 import Data.Bool
 import Data.Maybe
-import Prelude (Int, Integer, Float, Double, ($), Integral)
+import Prelude (Int, Integer, Float, Double, ($))
 import qualified Data.Ord as Ord
-import qualified Data.Eq as Eq
 import qualified Data.List as List
 import qualified Data.Set as Set
 import qualified Data.Foldable as Foldable
diff --git a/src/Camfort/Specification/Stencils/Syntax.hs b/src/Camfort/Specification/Stencils/Syntax.hs
--- a/src/Camfort/Specification/Stencils/Syntax.hs
+++ b/src/Camfort/Specification/Stencils/Syntax.hs
@@ -69,7 +69,8 @@
 -- but can be made smaller for debugging purposes,
 -- e.g., 100, but it needs to be high enough to clash with reasonable
 -- relative indices.
-absoluteRep = maxBound :: Int
+absoluteRep :: Int
+absoluteRep = maxBound
 
 {- *** 1 . Specification syntax -}
 
@@ -127,6 +128,7 @@
 setLinearity l (Specification mult isStencil)
   | l == Linear    = Specification (Once $ peel mult) isStencil
   | l == NonLinear = Specification (Mult $ peel mult) isStencil
+  | otherwise      = error "setLinearity: impossible"
 
 data Linearity = Linear | NonLinear deriving (Eq, Data, Typeable)
 
@@ -305,6 +307,7 @@
      | otherwise = showRegion "centered" dep dim reflx
 
 -- Helper for showing regions
+showRegion :: (Show dep, Show dim) => String -> dep -> dim -> Bool -> [Char]
 showRegion typ depS dimS reflx = typ ++ "(depth=" ++ show depS
                                ++ ", dim=" ++ show dimS
                                ++ (if reflx then "" else ", nonpointed")
diff --git a/src/Camfort/Specification/Stencils/Synthesis.hs b/src/Camfort/Specification/Stencils/Synthesis.hs
--- a/src/Camfort/Specification/Stencils/Synthesis.hs
+++ b/src/Camfort/Specification/Stencils/Synthesis.hs
@@ -23,30 +23,27 @@
   , offsetToIx
   ) where
 
-import Data.List
-
-import Camfort.Specification.Stencils.Syntax
-
-import Camfort.Analysis.Annotations
-
+import           Camfort.Analysis.Annotations
+import           Camfort.Specification.Stencils.Syntax
+import           Data.List hiding (span)
 import qualified Language.Fortran.AST as F
 import qualified Language.Fortran.Analysis as FA
+import           Language.Fortran.Util.Position
 import qualified Language.Fortran.Util.Position as FU
-
-import Language.Fortran.Util.Position
+import           Prelude hiding (span)
 
 -- Format inferred specifications
 formatSpec :: F.MetaInfo -> Int -> Char
  -> (FU.SrcSpan, Either [([Variable], Specification)] (String,Variable))
  -> String
-formatSpec mi indent marker (span, Right (evalInfo, name)) =
+formatSpec mi indent marker (_, Right (evalInfo, name)) =
   buildCommentText mi indent $
        marker : " "
     ++ evalInfo
     ++ (if name /= "" then " :: " ++ name else "") ++ "\n"
 
 formatSpec _ _ _ (_, Left []) = ""
-formatSpec mi indent marker (span, Left specs) =
+formatSpec mi indent marker (_, Left specs) =
   intercalate "\n" $ map commentText specs
     where
       commentText s = buildCommentText mi indent (marker : " " ++ doSpec s)
@@ -73,9 +70,6 @@
 
 
 ------------------------
-a = (head $ FA.initAnalysis [unitAnnotation]) { FA.insLabel = Just 0 }
-s = SrcSpan (Position 0 0 0 "" Nothing) (Position 0 0 0 "" Nothing)
-
 -- Make indexing expression for variable 'v' from an offset.
 -- essentially inverse to `ixToOffset` in StencilSpecification
 offsetToIx :: F.Name -> Int -> F.Index (FA.Analysis A)
@@ -89,3 +83,7 @@
   | otherwise = F.IxSingle a s Nothing (F.ExpBinary a s F.Subtraction
                                  (F.ExpValue a s (F.ValVariable v))
                                  (F.ExpValue a s (F.ValInteger $ show (abs o))))
+  where
+    a = (head $ FA.initAnalysis [unitAnnotation]) { FA.insLabel = Just 0 }
+    s = SrcSpan (Position 0 0 0 "" Nothing) (Position 0 0 0 "" Nothing)
+
diff --git a/src/Camfort/Specification/Units.hs b/src/Camfort/Specification/Units.hs
--- a/src/Camfort/Specification/Units.hs
+++ b/src/Camfort/Specification/Units.hs
@@ -22,11 +22,6 @@
 
 module Camfort.Specification.Units (synthesiseUnits) where
 
-import Control.Monad.Reader (asks)
-
-import qualified Language.Fortran.AST      as F
-import qualified Language.Fortran.Analysis as FA
-
 import           Camfort.Analysis.Annotations
 import           Camfort.Specification.Units.Analysis
   (UnitAnalysis, runInference)
@@ -37,15 +32,15 @@
 import qualified Camfort.Specification.Units.Annotation as UA
 import           Camfort.Specification.Units.InferenceBackend (chooseImplicitNames)
 import           Camfort.Specification.Units.Monad
-import           Camfort.Specification.Units.MonadTypes (UnitEnv(..))
 import           Camfort.Specification.Units.Synthesis (runSynthesis)
+import qualified Language.Fortran.AST as F
+import qualified Language.Fortran.Analysis as FA
 
 {-| Synthesis unspecified units for a program (after checking) -}
 synthesiseUnits
   :: Char -> UnitAnalysis (Either ConsistencyError (InferenceReport, F.ProgramFile Annotation))
 synthesiseUnits marker = do
   infRes <- inferUnits
-  pfOriginal <- asks unitProgramFile
   case infRes of
     InfInconsistent err       -> pure $ Left err
     Inferred report -> do
diff --git a/src/Camfort/Specification/Units/Analysis.hs b/src/Camfort/Specification/Units/Analysis.hs
--- a/src/Camfort/Specification/Units/Analysis.hs
+++ b/src/Camfort/Specification/Units/Analysis.hs
@@ -21,47 +21,45 @@
   , puSrcName
   ) where
 
-import           Control.Monad
-import           Control.Monad.State.Strict
-import           Control.Monad.Writer.CPS
-import           Control.Monad.Reader
-import           Data.Data (Data)
-import qualified Data.IntMap.Strict as IM
-import           Data.Generics.Uniplate.Operations
-import           Data.List (nub, intercalate)
-import qualified Data.Array as A
-import qualified Data.Map.Strict as M
-import           Data.Maybe (isJust, fromMaybe, mapMaybe)
-import qualified Data.Set as S
-import qualified Numeric.LinearAlgebra as H -- for debugging
-import           Data.Text (Text)
-import           Control.Lens ((^?), _1)
-
-import qualified Language.Fortran.AST      as F
-import qualified Language.Fortran.Analysis as FA
-import qualified Language.Fortran.Analysis.DataFlow as FAD
-import qualified Language.Fortran.Analysis.BBlocks as FAB
-import           Language.Fortran.Analysis (constExp, varName, srcName)
-import           Language.Fortran.Parser.Utils (readReal, readInteger)
-import           Language.Fortran.Util.ModFile
-import           Language.Fortran.Util.Position (getSpan)
-
 import           Camfort.Analysis
-import           Camfort.Analysis.Logger (LogLevel(..))
 import           Camfort.Analysis.Annotations (Annotation)
 import           Camfort.Analysis.CommentAnnotator (annotateComments)
+import           Camfort.Analysis.Logger (LogLevel(..))
 import           Camfort.Analysis.ModFile (withCombinedEnvironment)
-import qualified Camfort.Specification.Units.Annotation   as UA
+import qualified Camfort.Specification.Units.Annotation as UA
 import           Camfort.Specification.Units.Environment
 import           Camfort.Specification.Units.InferenceBackend
 import qualified Camfort.Specification.Units.InferenceBackendFlint as Flint
+import qualified Camfort.Specification.Units.InferenceBackendSBV as BackendSBV
 import           Camfort.Specification.Units.ModFile
   (genUnitsModFile, initializeModFiles, runCompileUnits)
 import           Camfort.Specification.Units.Monad
 import           Camfort.Specification.Units.MonadTypes
 import           Camfort.Specification.Units.Parser (unitParser)
 import qualified Camfort.Specification.Units.Parser.Types as P
-import qualified Camfort.Specification.Units.InferenceBackendSBV as BackendSBV
+import           Control.Lens ((^?), _1)
+import           Control.Monad
+import           Control.Monad.Reader
+import           Control.Monad.State.Strict
+import           Control.Monad.Writer.Lazy
+import qualified Data.Array as A
+import           Data.Data (Data)
+import           Data.Generics.Uniplate.Operations
+import qualified Data.IntMap.Strict as IM
+import           Data.List (nub, intercalate)
+import qualified Data.Map.Strict as M
+import           Data.Maybe (isJust, fromMaybe, mapMaybe)
+import qualified Data.Set as S
+import           Data.Text (Text)
+import qualified Language.Fortran.AST as F
+import           Language.Fortran.Analysis (constExp, varName, srcName)
+import qualified Language.Fortran.Analysis as FA
+import qualified Language.Fortran.Analysis.BBlocks as FAB
+import qualified Language.Fortran.Analysis.DataFlow as FAD
+import           Language.Fortran.Parser.Utils (readReal, readInteger)
+import           Language.Fortran.Util.ModFile
+import qualified Numeric.LinearAlgebra as H -- for debugging
+import           Prelude hiding (mod)
 
 -- | Prepare to run an inference function.
 initInference :: UnitSolver ()
@@ -129,7 +127,6 @@
 -- | Run a 'UnitSolver' analysis within a 'UnitsAnalysis'.
 runInference :: UnitSolver a -> UnitAnalysis (a, UnitState)
 runInference solver = do
-  uOpts <- asks unitOpts
   pf <- asks unitProgramFile
   mfs <- lift analysisModFiles
 
@@ -332,14 +329,14 @@
       F.ExpBinary a s op e1 e2
         | op `elem` [F.Multiplication, F.Division] -> case () of
             -- leave it alone if they're both constants
-            _ | Just c1 <- constExp (F.getAnnotation e1)
-              , Just c2 <- constExp (F.getAnnotation e2)        -> pure e
+            _ | Just _ <- constExp (F.getAnnotation e1)
+              , Just _ <- constExp (F.getAnnotation e2)        -> pure e
             -- a constant multiplier is unitless
-            _ | Just c1 <- constExp (F.getAnnotation e1)
+            _ | Just _ <- constExp (F.getAnnotation e1)
               , Just UnitLiteral{} <- UA.getUnitInfo e1         ->
                 pure $ F.ExpBinary a s op (UA.setUnitInfo UnitlessLit e1) e2
             -- a constant multiplier is unitless
-              | Just c2 <- constExp (F.getAnnotation e2)
+              | Just _ <- constExp (F.getAnnotation e2)
               , Just UnitLiteral{} <- UA.getUnitInfo e2         ->
                 pure $ F.ExpBinary a s op e1 (UA.setUnitInfo UnitlessLit e2)
             _                                                   -> pure e
@@ -362,7 +359,7 @@
       | isLiteral e = flip UA.setUnitInfo e <$> m
       | otherwise   = pure e
 
-    isPolyCtxt = case pu of F.PUFunction {} -> True; F.PUSubroutine {} -> True; _ -> False
+    -- isPolyCtxt = case pu of F.PUFunction {} -> True; F.PUSubroutine {} -> True; _ -> False
 
     genLit e
       | isLiteralZero e = withLiterals genParamLit e
@@ -386,6 +383,7 @@
   Just (FA.ConstUninterpReal s) -> readReal s /= Just 0
   _                             -> False
 
+isLiteralZero :: F.Expression UA -> Bool
 isLiteralZero x = isLiteral x && not (isLiteralNonZero x)
 
 --------------------------------------------------
@@ -631,6 +629,7 @@
              u3 <- (UA.getUnitInfo =<< m_e3) `mplus` if isMonomorphic u2 then mzero else pure UnitlessVar
              pure [ConEq u2 u3]
         ]
+propagateDoSpec _ = error "propagateDoSpec: called on invalid DoSpec"
 
 propagateStatement :: F.Statement UA -> UnitSolver (F.Statement UA)
 propagateStatement stmt = case stmt of
@@ -835,6 +834,7 @@
 binOpKind F.NE               = RelOp
 binOpKind F.Or               = LogicOp
 binOpKind F.And              = LogicOp
+binOpKind F.XOr              = LogicOp
 binOpKind F.Equivalent       = RelOp
 binOpKind F.NotEquivalent    = RelOp
 binOpKind (F.BinCustom _)    = RelOp
@@ -846,7 +846,7 @@
   nmap <- getNameParamMap
   -- Translate a Use AST node into a pair mapping unique name to 'local' source name in this program file.
   let useToPair (F.UseID _ _ e) = (varName e, srcName e)
-      useToPair (F.UseRename _ _ e1 e2) = (varName e1, srcName e1) -- (unique name, 'local' source name)
+      useToPair (F.UseRename _ _ e1 _) = (varName e1, srcName e1) -- (unique name, 'local' source name)
   -- A map of modules -> (maps of variables -> their unit info).
   let modnmaps = [ M.fromList (mapMaybe f (M.toList npkmap))
                  -- find all StUse statements and identify variables that need to be imported from nmap
@@ -918,7 +918,7 @@
     logDebugNoOrigin $ "newColIndices = " <> describeShow newColIndices
     logDebugNoOrigin "--------------------------------------------------\nLHS Cols with newColIndices:"
     let lhsCols = A.elems lhsColA ++ map (lhsColA A.!) newColIndices
-    logDebugNoOrigin $ describe . unlines . map show $ zip [0..] lhsCols
+    logDebugNoOrigin $ describe . unlines . map show $ zip [(0::Int)..] lhsCols
     -- logDebugNoOrigin "--------------------------------------------------\nSolved (SVD) M:"
     -- logDebugNoOrigin $ show (H.linearSolveSVD lhsM rhsM)
     -- logDebugNoOrigin "--------------------------------------------------\nSingular Values:"
@@ -932,8 +932,8 @@
     let unitAssignments = genUnitAssignments cons
     logDebugNoOrigin . describe . unlines $ map (\ (u1s, u2) -> "  ***UnitAssignment: " ++ show u1s ++ " === " ++ show (flattenUnits u2) ++ "\n") unitAssignments
     logDebugNoOrigin "--------------------------------------------------"
-    let unitAssignments = BackendSBV.genUnitAssignments cons
-    logDebugNoOrigin . describe . unlines $ map (\ (u1s, u2) -> "  ***UnitAssignmentSBV: " ++ show u1s ++ " === " ++ show (flattenUnits u2)) unitAssignments
+    let unitAssignmentsSBV = BackendSBV.genUnitAssignments cons
+    logDebugNoOrigin . describe . unlines $ map (\ (u1s, u2) -> "  ***UnitAssignmentSBV: " ++ show u1s ++ " === " ++ show (flattenUnits u2)) unitAssignmentsSBV
     logDebugNoOrigin "--------------------------------------------------\nProvenance:"
     let (augM', p) = provenance augM
     logDebugNoOrigin . describeShow $ augM'
diff --git a/src/Camfort/Specification/Units/Analysis/Consistent.hs b/src/Camfort/Specification/Units/Analysis/Consistent.hs
--- a/src/Camfort/Specification/Units/Analysis/Consistent.hs
+++ b/src/Camfort/Specification/Units/Analysis/Consistent.hs
@@ -16,27 +16,21 @@
   , checkUnits
   ) where
 
-import           Control.Monad.State (get)
-import           Control.Monad.Reader (asks)
-import           Data.Data
-import           Data.Generics.Uniplate.Operations
-import           Data.List (partition, find, group, sort)
-import qualified Data.Map.Strict as M
-import           Data.Maybe (maybeToList, maybe)
-import           Data.Function (on)
-
 import           Camfort.Analysis (ExitCodeOfReport(..), Describe(..))
-import           Camfort.Analysis.Annotations
 import           Camfort.Specification.Units.Analysis (UnitAnalysis, runInference)
 import qualified Camfort.Specification.Units.Annotation as UA
+import qualified Camfort.Specification.Units.BackendTypes as B
 import           Camfort.Specification.Units.Environment
 import           Camfort.Specification.Units.InferenceBackend (inconsistentConstraints)
-import qualified Camfort.Specification.Units.InferenceBackend as MatrixBackend
 import           Camfort.Specification.Units.Monad
-import           Camfort.Specification.Units.MonadTypes
-import qualified Camfort.Specification.Units.BackendTypes as B
-
-import qualified Language.Fortran.AST           as F
+import           Control.DeepSeq
+import           Control.Monad.Reader (asks)
+import           Control.Monad.State (get)
+import           Data.Generics.Uniplate.Operations
+import           Data.List (partition, find, group, sort)
+import qualified Data.Map.Strict as M
+import           Data.Maybe (maybeToList, maybe)
+import qualified Language.Fortran.AST as F
 import qualified Language.Fortran.Util.Position as FU
 
 -- | A report that summarises unit consistency.
@@ -45,7 +39,8 @@
   = forall a. Consistent (F.ProgramFile a) Int
     -- | An inconsistency was found in units of the program.
   | Inconsistent ConsistencyError
-
+instance NFData ConsistencyReport where
+  rnf _ = ()
 instance Show ConsistencyReport where
   show (Consistent pf nVars) = concat ["\n", fname, ": Consistent ", show nVars, " variables checked."]
     where fname = F.pfGetFilename pf
@@ -91,8 +86,8 @@
               rhs = flattenUnits v
           orient c = c
 
-          partitionUnits f u = (foldUnits a, foldUnits b)
-            where (a, b) = partition f (flattenUnits u)
+          -- partitionUnits f u = (foldUnits a, foldUnits b)
+          --   where (a, b) = partition f (flattenUnits u)
           unitPower (UnitPow u k) = unitPower u * k
           unitPower UnitlessLit = 0
           unitPower UnitlessVar = 0
@@ -159,9 +154,9 @@
     pfUA :: F.ProgramFile UA
     pfUA = usProgramFile state -- the program file after units analysis is done
 
-  pure $ case eCons of
-           Nothing     -> Consistent pf nVars
-           (Just cons) -> Inconsistent $ Inconsistency pfUA cons
+  pure $!! case eCons of
+             Nothing     -> Consistent pf nVars
+             (Just cons) -> Inconsistent $ Inconsistency pfUA cons
   where
     isParametricUnit u = case u of UnitParamPosAbs {} -> True; UnitParamPosUse {} -> True
                                    UnitParamVarAbs {} -> True; UnitParamVarUse {} -> True
@@ -199,12 +194,14 @@
 shiftConEq f (ConConj cs) = ConConj $ map (shiftConEq f) cs
 
 -- | Balance equations by shifting terms that satisfy predicate f
+balanceConEq :: (UnitInfo -> Bool) -> Constraint -> Constraint
 balanceConEq f (ConEq l r) = ConEq (foldUnits (lhsOk ++ negateCons rhsShift)) (foldUnits (rhsOk ++ negateCons lhsShift))
   where
     (lhsShift, lhsOk) = partition f (flattenUnits l)
     (rhsShift, rhsOk) = partition f (flattenUnits r)
 balanceConEq f (ConConj cs) = ConConj $ map (balanceConEq f) cs
 
+negateCons :: [UnitInfo] -> [UnitInfo]
 negateCons = map (\ x -> case x of
                      UnitPow u k -> UnitPow u (-k)
                      u -> UnitPow u (-1))
diff --git a/src/Camfort/Specification/Units/Analysis/Criticals.hs b/src/Camfort/Specification/Units/Analysis/Criticals.hs
--- a/src/Camfort/Specification/Units/Analysis/Criticals.hs
+++ b/src/Camfort/Specification/Units/Analysis/Criticals.hs
@@ -16,29 +16,24 @@
   ( inferCriticalVariables
   ) where
 
-import           Control.Monad.State (get)
-import           Control.Monad.Reader (asks, lift)
-import           Data.Generics.Uniplate.Operations
-import qualified Data.Map.Strict       as M
-import           Data.Maybe (fromMaybe)
-
-import Camfort.Analysis
-import Camfort.Analysis.Annotations
-import Camfort.Analysis.ModFile (withCombinedModuleMap)
-import Camfort.Specification.Units.InferenceBackendSBV (criticalVariables)
-
--- Provides the types and data accessors used in this module
+import           Camfort.Analysis
+import           Camfort.Analysis.Annotations
+import           Camfort.Analysis.ModFile (withCombinedModuleMap)
 import           Camfort.Specification.Units.Analysis (UnitAnalysis, runInference)
 import qualified Camfort.Specification.Units.Annotation as UA
 import           Camfort.Specification.Units.Environment
+import           Camfort.Specification.Units.InferenceBackendSBV (criticalVariables)
 import           Camfort.Specification.Units.Monad
-import           Camfort.Specification.Units.MonadTypes
-
-import qualified Language.Fortran.AST               as F
-import qualified Language.Fortran.Analysis          as FA
-import qualified Language.Fortran.Analysis.Renaming as FAR
+import           Control.DeepSeq
+import           Control.Monad.Reader (asks, lift)
+import           Control.Monad.State (get)
+import           Data.Generics.Uniplate.Operations
+import qualified Data.Map.Strict as M
+import           Data.Maybe (fromMaybe)
+import qualified Language.Fortran.AST as F
+import qualified Language.Fortran.Analysis as FA
 import           Language.Fortran.Util.ModFile
-import qualified Language.Fortran.Util.Position     as FU
+import qualified Language.Fortran.Util.Position as FU
 
 -- | An inference of variables that must be provided with
 -- unit annotations before units for all variables can be
@@ -57,6 +52,9 @@
   , criticalsFromWhere    :: M.Map F.Name FilePath
   }
 
+instance NFData Criticals where
+  rnf _ = ()
+
 instance ExitCodeOfReport Criticals where
   exitCodeOf _ = 0
 
@@ -111,9 +109,9 @@
                 -- going to ignore intrinsics here
               ] `M.union` (M.unions . map (M.fromList . map (\ (a, (b, _)) -> (b, a)) . M.toList) $ M.elems mmap)
     fromWhereMap = genUniqNameToFilenameMap mfs
-  pure Criticals { criticalsPf           = pf
-                 , criticalsVariables    = eVars
-                 , criticalsDeclarations = dmap
-                 , criticalsUniqMap      = uniqnameMap
-                 , criticalsFromWhere    = fromWhereMap
-                 }
+  pure $!! Criticals { criticalsPf           = pf
+                     , criticalsVariables    = eVars
+                     , criticalsDeclarations = dmap
+                     , criticalsUniqMap      = uniqnameMap
+                     , criticalsFromWhere    = fromWhereMap
+                     }
diff --git a/src/Camfort/Specification/Units/Analysis/Infer.hs b/src/Camfort/Specification/Units/Analysis/Infer.hs
--- a/src/Camfort/Specification/Units/Analysis/Infer.hs
+++ b/src/Camfort/Specification/Units/Analysis/Infer.hs
@@ -18,33 +18,25 @@
   , inferUnits
   ) where
 
+import           Camfort.Analysis (ExitCodeOfReport(..), Describe(..))
+import           Camfort.Specification.Units.Analysis
+  (UnitAnalysis, puName, puSrcName, runInference)
+import           Camfort.Specification.Units.Analysis.Consistent
+  (ConsistencyError, ConsistencyReport(..), checkUnits)
+import           Camfort.Specification.Units.Environment
+import           Camfort.Specification.Units.InferenceBackend (inferVariables, chooseImplicitNames)
+import           Camfort.Specification.Units.Monad
+import           Control.DeepSeq
 import           Data.Data (Data)
-import           Data.Generics.Uniplate.Operations
-  (universeBi)
+import           Data.Generics.Uniplate.Operations (universeBi)
 import           Data.List (sort)
 import qualified Data.Map.Strict as M
 import           Data.Maybe (mapMaybe, maybeToList)
 import           GHC.Generics (Generic)
-import qualified Data.ByteString as B
-
-import qualified Language.Fortran.AST           as F
-import qualified Language.Fortran.Analysis      as FA
+import qualified Language.Fortran.AST as F
+import qualified Language.Fortran.Analysis as FA
 import qualified Language.Fortran.Util.Position as FU
 
-import Camfort.Analysis (ExitCodeOfReport(..), Describe(..))
-import Camfort.Analysis.Annotations (Annotation)
-import Camfort.Specification.Units.Analysis
-  (UnitAnalysis, puName, puSrcName, runInference)
-import Camfort.Specification.Units.Analysis.Consistent
-  (ConsistencyError, ConsistencyReport(..), checkUnits)
-import Camfort.Specification.Units.Environment
--- import Camfort.Specification.Units.InferenceBackendSBV (inferVariables)
-import Camfort.Specification.Units.InferenceBackend (inferVariables,
-                                                     chooseImplicitNames)
-import Camfort.Specification.Units.Monad
-
-import Camfort.Helpers (FileOrDir, Filename)
-
 data ExpInfo = ExpInfo
   { eiSrcSpan :: FU.SrcSpan
   , eiVName   :: F.Name
@@ -55,10 +47,16 @@
 data InferenceReport
   = InferenceReport (F.ProgramFile UA) [(VV, UnitInfo)]
 
+instance NFData InferenceReport where
+  rnf _ = ()
+
 data InferenceResult
   = Inferred InferenceReport
   | InfInconsistent ConsistencyError
 
+instance NFData InferenceResult where
+  rnf _ = ()
+
 instance ExitCodeOfReport InferenceResult where
   exitCodeOf (Inferred _) = 0
   exitCodeOf (InfInconsistent _) = 1
@@ -110,10 +108,10 @@
   case eVars of
     [] -> do
       consistency <- checkUnits
-      pure $ case consistency of
+      pure $!! case consistency of
         Consistent{}     -> Inferred (InferenceReport pfUA eVars)
         Inconsistent err -> InfInconsistent err
-    _ -> pure . Inferred $ InferenceReport pfUA eVars
+    _ -> pure . Inferred $!! InferenceReport pfUA eVars
 
 -- | Return a list of variable names mapped to their corresponding
 -- unit that was inferred.
diff --git a/src/Camfort/Specification/Units/BackendTypes.hs b/src/Camfort/Specification/Units/BackendTypes.hs
--- a/src/Camfort/Specification/Units/BackendTypes.hs
+++ b/src/Camfort/Specification/Units/BackendTypes.hs
@@ -108,7 +108,7 @@
 
 -- | Raise the dimension to the given power
 dimRaisePow :: Integer -> Dim -> Dim
-dimRaisePow 0 d = identDim
+dimRaisePow 0 _ = identDim
 dimRaisePow k d = M.map (* k) d
 
 -- | Compare two Dims, not minding the difference between
@@ -125,11 +125,11 @@
 dimParamEq' ((u1, p1):d1') d2 = case partition (unitParamEq u1 . fst) d2 of
   ((u2, p2):d2', d2'') -> dimParamEq' (rem1 ++ d1') (rem2 ++ d2' ++ d2'')
     where
-      (rem1, rem2) | p1 == p2 = ([], [])
-                   | p1 < p2  = ([], [(u2, p2 - p1)])
-                   | p1 > p2  = ([(u1, p1 - p2)], [])
-
-  _                    -> False
+      (rem1, rem2) | p1 == p2  = ([], [])
+                   | p1 < p2   = ([], [(u2, p2 - p1)])
+                   | p1 > p2   = ([(u1, p1 - p2)], [])
+                   | otherwise = error "dimParamEq'"
+  _ -> False
 
 -- | Similar to dimParamEq but assume that dimRaisePow can be
 -- arbitrarily applied to each of the parameters, because they now
@@ -212,23 +212,23 @@
   | (u, x):_ <- valids
   , sub1     <- M.singleton u (dimFromList ((u, 1):[(v, -div y x) | (v, y) <- M.toList dim, v /= u]))
   , sub2     <- dimSimplify excludes (applySub sub1 dim) = composeSubs sub2 sub1
-
+  | otherwise = error "dimSimplify"
   where
     valids   = sortBy (comparing (abs . snd)) . filter ((`S.notMember` excludes) . fst) $ M.toList dim
     validSet = S.fromList (map fst valids)
     invals   = filter ((`S.notMember` validSet) . fst) $ M.toList dim
 
-testVar x = UnitVar (x, x)
+-- testVar x = UnitVar (x, x)
 
-u0 = testVar "u0"
-u1 = testVar "u1"
-u2 = testVar "u2"
-u3 = testVar "u3"
-u4 = testVar "u4"
+-- u0 = testVar "u0"
+-- u1 = testVar "u1"
+-- u2 = testVar "u2"
+-- u3 = testVar "u3"
+-- u4 = testVar "u4"
 
-dim1 = dimFromList [(u1, 6), (u2, 15), (u3, -7), (u4, 12)]
-dim2 = dimFromList [(u1, 2), (u2, 15), (u3, -9)]
+-- dim1 = dimFromList [(u1, 6), (u2, 15), (u3, -7), (u4, 12)]
+-- dim2 = dimFromList [(u1, 2), (u2, 15), (u3, -9)]
 
-test1 = applySub (dimSimplify (S.fromList [u3,u4]) dim1) dim1 == dimFromList [(u2, 3), (u3, 2)]
+-- test1 = applySub (dimSimplify (S.fromList [u3,u4]) dim1) dim1 == dimFromList [(u2, 3), (u3, 2)]
 
-test2 =  (dimSimplify (S.fromList [u0]) (dimFromList [(u0, 1), (u1, -2)]))
+-- test2 =  (dimSimplify (S.fromList [u0]) (dimFromList [(u0, 1), (u1, -2)]))
diff --git a/src/Camfort/Specification/Units/Environment.hs b/src/Camfort/Specification/Units/Environment.hs
--- a/src/Camfort/Specification/Units/Environment.hs
+++ b/src/Camfort/Specification/Units/Environment.hs
@@ -41,21 +41,20 @@
   , module Data.Data
   ) where
 
+import qualified Camfort.Specification.Units.Parser.Types as P
+import           Control.Arrow (first, second)
 import           Data.Binary
 import           Data.Char
 import           Data.Data
+import           Data.Generics.Uniplate.Operations (rewrite)
 import           Data.List
+import qualified Data.Map.Strict as M
 import           Data.Ratio
 import           GHC.Generics (Generic)
-import           Text.Printf
-import           Control.Arrow (first, second)
-import           Text.PrettyPrint.GenericPretty (pp, pretty, Out, doc, docPrec)
-import           Text.PrettyPrint (text)
-
 import qualified Language.Fortran.AST as F
-import qualified Camfort.Specification.Units.Parser.Types as P
-import Data.Generics.Uniplate.Operations (rewrite)
-import qualified Data.Map.Strict as M
+import           Text.PrettyPrint (text)
+import           Text.PrettyPrint.GenericPretty (Out, doc, docPrec)
+import           Text.Printf
 
 -- | A (unique name, source name) variable
 type VV = (F.Name, F.Name)
@@ -88,7 +87,8 @@
   deriving (Eq, Ord, Data, Typeable, Generic)
 
 -- | True iff u is monomorphic (has no parametric polymorphic pieces)
-isMonomorphic u = case u of
+isMonomorphic :: UnitInfo -> Bool
+isMonomorphic unitinfo = case unitinfo of
   UnitName _      -> True
   UnitAlias _     -> True
   UnitVar _       -> True
@@ -101,6 +101,7 @@
   _               -> False
 
 -- | True iff argument matches one of the unitless constructors
+isUnitless :: UnitInfo -> Bool
 isUnitless UnitlessVar = True
 isUnitless UnitlessLit = True
 isUnitless _           = False
@@ -143,18 +144,22 @@
     flatten (UnitPow u p)   = map (second (p*)) $ flatten u
     flatten u               = [(u, 1)]
 
+foldUnits :: Foldable t => t UnitInfo -> UnitInfo
 foldUnits units
   | null units = UnitlessVar
   | otherwise  = foldl1 UnitMul units
 
+-- FIXME: we know better...
+approxEq :: Double -> Double -> Bool
 approxEq a b = abs (b - a) < epsilon
+epsilon :: Double
 epsilon = 0.001 -- arbitrary
 
 
 instance Binary UnitInfo
 
 instance Show UnitInfo where
-  show u = case u of
+  show unitinfo = case unitinfo of
     UnitParamPosAbs ((f, _), i)         -> printf "#<ParamPosAbs %s[%d]>" f i
     UnitParamPosUse ((f, _), i, j)      -> printf "#<ParamPosUse %s[%d] callId=%d>" f i j
     UnitParamVarAbs ((f, _), (v, _))    -> printf "#<ParamVarAbs %s.%s>" f v
@@ -163,7 +168,7 @@
     UnitParamLitUse (i, j)              -> printf "#<ParamLitUse litId=%d callId=%d]>" i j
     UnitParamEAPAbs (v, _)              -> v
     UnitParamEAPUse ((v, _), i)         -> printf "#<ParamEAPUse %s callId=%d]>" v i
-    UnitParamImpAbs id                  -> printf "#<ParamImpAbs %s>" id
+    UnitParamImpAbs iden                -> printf "#<ParamImpAbs %s>" iden
     UnitLiteral i                       -> printf "#<Literal id=%d>" i
     UnitlessLit                         -> "1"
     UnitlessVar                         -> "1"
@@ -208,7 +213,7 @@
 -- otherwise Noting
 doubleToRationalSubset :: Double -> Maybe Rational
 doubleToRationalSubset x | x < 0 =
-    doubleToRationalSubset (abs x) >>= (\x -> return (-x))
+    negate <$> doubleToRationalSubset (abs x)
 doubleToRationalSubset x =
     doubleToRational' 0 1 (ceiling x) 1
   where
@@ -241,6 +246,7 @@
   show (ConEq u1 u2) = show u1 ++ " === " ++ show u2
   show (ConConj cs) = intercalate " && " (map show cs)
 
+isUnresolvedUnit :: UnitInfo -> Bool
 isUnresolvedUnit (UnitVar _)         = True
 isUnresolvedUnit (UnitLiteral _)     = True
 isUnresolvedUnit (UnitParamVarUse _) = True
@@ -256,6 +262,7 @@
 isUnresolvedUnit (UnitMul u1 u2)     = isUnresolvedUnit u1 || isUnresolvedUnit u2
 isUnresolvedUnit _                   = False
 
+isResolvedUnit :: UnitInfo -> Bool
 isResolvedUnit = not . isUnresolvedUnit
 
 isConcreteUnit :: UnitInfo -> Bool
@@ -306,11 +313,11 @@
       | all isAlphaNum s = s
       | otherwise        = "(" ++ s ++ ")"
       where s = pprintUnitInfo x
-    maybeParenS x
-      | all isUnitMulOk s = s
-      | otherwise         = "(" ++ s ++ ")"
-      where s = pprintUnitInfo x
-    isUnitMulOk c = isSpace c || isAlphaNum c || c `elem` "*."
+    -- maybeParenS x
+    --   | all isUnitMulOk s = s
+    --   | otherwise         = "(" ++ s ++ ")"
+    --   where s = pprintUnitInfo x
+    -- isUnitMulOk c = isSpace c || isAlphaNum c || c `elem` "*."
 
 pprintUnitInfo ui                                   = show ui
 
diff --git a/src/Camfort/Specification/Units/InferenceBackend.hs b/src/Camfort/Specification/Units/InferenceBackend.hs
--- a/src/Camfort/Specification/Units/InferenceBackend.hs
+++ b/src/Camfort/Specification/Units/InferenceBackend.hs
@@ -38,25 +38,27 @@
   , provenance
   , splitNormHNF
   ) where
-import           Prelude hiding ((<>))
+
+import           Camfort.Specification.Units.Environment
+import qualified Camfort.Specification.Units.InferenceBackendFlint as Flint
 import           Control.Arrow (first, second, (***))
 import           Control.Monad
 import           Control.Monad.ST
-import           Control.Parallel
 import           Control.Parallel.Strategies
 import qualified Data.Array as A
 import           Data.Generics.Uniplate.Operations
   (transformBi, universeBi)
+import           Data.Graph.Inductive hiding ((><))
+import qualified Data.IntMap as IM
+import qualified Data.IntSet as IS
 import           Data.List
   ((\\), findIndex, inits, nub, partition, sort, sortBy, group, tails, foldl')
-import           Data.Ord
 import qualified Data.Map.Strict as M
-import qualified Data.IntMap as IM
-import qualified Data.IntSet as IS
 import           Data.Maybe (fromMaybe, mapMaybe)
+import           Data.Ord
 import           Data.Tuple (swap)
 import           Numeric.LinearAlgebra
-  ( atIndex, (<>), (><)
+  ( atIndex, (<>)
   , rank, (?), (¿)
   , rows, cols
   , subMatrix, diag
@@ -68,10 +70,8 @@
   , writeMatrix, runSTMatrix
   , freezeMatrix, STMatrix
   )
-import Data.Graph.Inductive hiding ((><))
+import           Prelude hiding ((<>))
 
-import Camfort.Specification.Units.Environment
-import qualified Camfort.Specification.Units.InferenceBackendFlint as Flint
 
 -- | Returns list of formerly-undetermined variables and their units.
 inferVariables :: Constraints -> [(VV, UnitInfo)]
@@ -102,9 +102,9 @@
 mustBeUnitless unitAssignments = mbu
   where
     mbu = [ ConEq UnitlessLit (UnitPow (UnitLiteral l) k)
-          | a@(UnitPow (UnitLiteral l) k:_, rhs) <- ua''
+          | (UnitPow (UnitLiteral l) k:_, rhs) <- ua''
           , any isParametric (universeBi rhs :: [UnitInfo]) ]
-    ua' = map (shiftTerms . fmap flattenUnits) unitAssignments
+    -- ua' = map (shiftTerms . fmap flattenUnits) unitAssignments
     ua'' = map (shiftTermsBy isLiteral . fmap flattenUnits) unitAssignments
 
     isLiteral UnitLiteral{} = True
@@ -170,8 +170,8 @@
     (solvedM, newColIndices)      = splitNormHNF unsolvedM
     -- solvedM can have additional columns and rows from normHNF;
     -- cosolvedM corresponds to the original lhsM.
-    cosolvedM                     = subMatrix (0, 0) (rows solvedM, cols lhsM) solvedM
-    cosolvedMrhs                  = subMatrix (0, cols lhsM) (rows solvedM, cols solvedM - cols lhsM) solvedM
+    -- cosolvedM                     = subMatrix (0, 0) (rows solvedM, cols lhsM) solvedM
+    -- cosolvedMrhs                  = subMatrix (0, cols lhsM) (rows solvedM, cols solvedM - cols lhsM) solvedM
 
     -- generate a colList with both the original columns and new ones generated
     -- if a new column generated was derived from the right-hand side then negate it
@@ -186,30 +186,34 @@
     unitPows                      = map (concatMap flattenUnits . zipWith unitPow colList) (H.toLists solvedM)
 
     -- Variables to the left, unit names to the right side of the equation.
-    unitAssignments               = map (fmap (foldUnits . map negatePosAbs) . checkSanity . partition (not . isUnitRHS)) unitPows
-    isUnitRHS (UnitPow (UnitName _) _)        = True
-    isUnitRHS (UnitPow (UnitParamEAPAbs _) _) = True
+    unitAssignments               = map (fmap (foldUnits . map negatePosAbs) . checkSanity . partition (not . isUnitRHS')) unitPows
+    isUnitRHS' (UnitPow (UnitName _) _)        = True
+    isUnitRHS' (UnitPow (UnitParamEAPAbs _) _) = True
     -- Because this version of isUnitRHS different from
     -- constraintsToMatrix interpretation, we need to ensure that any
     -- moved ParamPosAbs units are negated, because they are
     -- effectively being shifted across the equal-sign:
-    isUnitRHS (UnitPow (UnitParamImpAbs _) _) = True
-    isUnitRHS (UnitPow (UnitParamPosAbs (_, 0)) _) = False
-    isUnitRHS (UnitPow (UnitParamPosAbs _) _) = True
-    isUnitRHS _                               = False
+    isUnitRHS' (UnitPow (UnitParamImpAbs _) _) = True
+    isUnitRHS' (UnitPow (UnitParamPosAbs (_, 0)) _) = False
+    isUnitRHS' (UnitPow (UnitParamPosAbs _) _) = True
+    isUnitRHS' _                               = False
 
 checkSanity :: ([UnitInfo], [UnitInfo]) -> ([UnitInfo], [UnitInfo])
 checkSanity (u1@[UnitPow (UnitVar _) _], u2)
-  | or $ [ True | UnitParamPosAbs (_, i) <- universeBi u2 ]
+  | or $ [ True | UnitParamPosAbs (_, _) <- universeBi u2 ]
       ++ [ True | UnitParamImpAbs _      <- universeBi u2 ] = (u1++u2,[])
 checkSanity (u1@[UnitPow (UnitParamVarAbs (f, _)) _], u2)
-  | or [ True | UnitParamPosAbs (f', i) <- universeBi u2, f' /= f ] = (u1++u2,[])
+  | or [ True | UnitParamPosAbs (f', _) <- universeBi u2, f' /= f ] = (u1++u2,[])
 checkSanity c = c
 
 --------------------------------------------------
 
+-- FIXME: you know better...
+approxEq :: Double -> Double -> Bool
 approxEq a b = abs (b - a) < epsilon
+notApproxEq :: Double -> Double -> Bool
 notApproxEq a b = not (approxEq a b)
+epsilon :: Double
 epsilon = 0.001 -- arbitrary
 
 --------------------------------------------------
@@ -273,7 +277,7 @@
 -- inconsistent row numbers found (in terms of the rows of the
 -- original lhsM).
 splitFindInconsistentRows :: H.Matrix Double -> H.Matrix Double -> [RowNum]
-splitFindInconsistentRows lhsM rhsM = concatMap eachComponent $ splitMatWithRHS lhsM rhsM
+splitFindInconsistentRows lhsMat rhsMat = concatMap eachComponent $ splitMatWithRHS lhsMat rhsMat
   where
     eachComponent (rs, (lhsM, rhsM), _) = map (rs !!) $ findInconsistentRows lhsM augM
       where
@@ -347,7 +351,6 @@
     rhs             = map snd shiftedCons
     (lhsM, lhsCols) = flattenedToMatrix sortfn lhs
     (rhsM, rhsCols) = flattenedToMatrix sortfn rhs
-    augM            = if rows rhsM == 0 || cols rhsM == 0 then lhsM else if rows lhsM == 0 || cols lhsM == 0 then rhsM else fromBlocks [[lhsM, rhsM]]
     inconsists      = splitFindInconsistentRows lhsM rhsM
 
 -- [[UnitInfo]] is a list of flattened constraints
@@ -355,15 +358,15 @@
 flattenedToMatrix sortfn cons = (m, A.array (0, numCols - 1) (map swap uniqUnits))
   where
     m = runSTMatrix $ do
-          m <- newMatrix 0 numRows numCols
+          newM <- newMatrix 0 numRows numCols
           -- loop through all constraints
           forM_ (zip cons [0..]) $ \ (unitPows, row) -> do
             -- write co-efficients for the lhs of the constraint
             forM_ unitPows $ \ (UnitPow u k) -> do
               case M.lookup u colMap of
-                Just col -> readMatrix m row col >>= (writeMatrix m row col . (+k))
+                Just col -> readMatrix newM row col >>= (writeMatrix newM row col . (+k))
                 _        -> return ()
-          return m
+          return newM
     -- identify and enumerate every unit uniquely
     uniqUnits = flip zip [0..] . map head . group . sortBy sortfn $ [ u | UnitPow u _ <- concat cons ]
     -- map units to their unique column number
@@ -371,8 +374,10 @@
     numRows   = length cons
     numCols   = M.size colMap
 
+negateCons :: [UnitInfo] -> [UnitInfo]
 negateCons = map (\ (UnitPow u k) -> UnitPow u (-k))
 
+negatePosAbs :: UnitInfo -> UnitInfo
 negatePosAbs (UnitPow (UnitParamPosAbs x) k) = UnitPow (UnitParamPosAbs x) (-k)
 negatePosAbs (UnitPow (UnitParamImpAbs v) k) = UnitPow (UnitParamImpAbs v) (-k)
 negatePosAbs u                               = u
@@ -380,6 +385,7 @@
 --------------------------------------------------
 
 -- Units that should appear on the right-hand-side of the matrix during solving
+isUnitRHS :: UnitInfo -> Bool
 isUnitRHS (UnitPow (UnitName _) _)        = True
 isUnitRHS (UnitPow (UnitParamEAPAbs _) _) = True
 isUnitRHS _                               = False
@@ -458,24 +464,25 @@
     -- separate elemRowAdd matrix for each cancellation that are then
     -- multiplied together, simply build a single matrix that cancels
     -- all of them out at the same time, using the ST Monad.
-    findAdds _ m ms
-      | isWritten = (new <> m, (new, ElemRowAdds ops):ms)
-      | otherwise = (m, ms)
+    findAdds _ curM ms
+      | isWritten = (newMat <> curM, (newMat, ElemRowAdds matOps):ms)
+      | otherwise = (curM, ms)
       where
-        (isWritten, ops, new) = runST $ do
-          new <- newMatrix 0 n n :: ST s (STMatrix s Double)
-          sequence [ writeMatrix new i' i' 1 | i' <- [0 .. (n - 1)] ]
+        (isWritten, matOps, newMat) = runST $ do
+          newM <- newMatrix 0 n n :: ST s (STMatrix s Double)
+          sequence_ [ writeMatrix newM i' i' 1 | i' <- [0 .. (n - 1)] ]
           let f w o i | i >= n                  = return (w, o)
                       | i == j - k              = f w o (i + 1)
                       | a `atIndex` (i, j) == 0 = f w o (i + 1)
-                      | otherwise               = writeMatrix new i (j - k) (- (a `atIndex` (i, j)))
+                      | otherwise               = writeMatrix newM i (j - k) (- (a `atIndex` (i, j)))
                                                   >> f True ((i, j - k):o) (i + 1)
-          (isWritten, ops) <- f False [] 0
-          (isWritten, ops,) `fmap` freezeMatrix new
+          (isW, ops) <- f False [] 0
+          (isW, ops,) `fmap` freezeMatrix newM
 
-    (a2, mats2) = findAdds 0 a1 mats1
+    (a2, mats2) = findAdds (0::Int) a1 mats1
 
 -- Get a list of values that occur below (i, j) in the matrix a.
+getColumnBelow :: H.Matrix Double -> (Int, Int) -> [Double]
 getColumnBelow a (i, j) = concat . H.toLists $ subMatrix (i, j) (n - i, 1) a
   where n = rows a
 
@@ -504,6 +511,7 @@
   where
     trans = concatMap (\ i -> [i] `fromMaybe` (IS.toList <$> IM.lookup i g1))
 
+invertGraphCol :: GraphCol -> GraphCol
 invertGraphCol g = IM.fromListWith IS.union [ (i, IS.singleton j) | (j, jset) <- IM.toList g, i <- IS.toList jset ]
 
 provenance :: H.Matrix Double -> (H.Matrix Double, Provenance)
@@ -546,8 +554,8 @@
   where
     absUnits = nub [ u | u@(UnitParamPosAbs _)             <- universeBi x ] ++
                nub [ u | u@(UnitParamImpAbs _)             <- universeBi x ]
-    eapNames = nub $ [ n | u@(UnitParamEAPAbs (_, n))      <- universeBi x ] ++
-                     [ n | u@(UnitParamEAPUse ((_, n), _)) <- universeBi x ]
+    eapNames = nub $ [ n | (UnitParamEAPAbs (_, n))      <- universeBi x ] ++
+                     [ n | (UnitParamEAPUse ((_, n), _)) <- universeBi x ]
     newNames = filter (`notElem` eapNames) . map ('\'':) $ nameGen
     nameGen  = concatMap sequence . tail . inits $ repeat ['a'..'z']
 
@@ -562,13 +570,13 @@
 -- inference or checking to work.
 criticalVariables :: Constraints -> [UnitInfo]
 criticalVariables [] = []
-criticalVariables cons = filter (not . isUnitRHS) $ map (colA A.!) criticalIndices
+criticalVariables cons = filter (not . isUnitRHS') $ map (colA A.!) criticalIndices
   where
     (unsolvedM, _, colA)          = constraintsToMatrix cons
     solvedM                       = rref unsolvedM
     uncriticalIndices             = mapMaybe (findIndex (/= 0)) $ H.toLists solvedM
     criticalIndices               = A.indices colA \\ uncriticalIndices
-    isUnitRHS (UnitName _)        = True; isUnitRHS _ = False
+    isUnitRHS' (UnitName _)       = True; isUnitRHS' _ = False
 
 -- | Returns just the list of constraints that were identified as
 -- being possible candidates for inconsistency, if there is a problem.
diff --git a/src/Camfort/Specification/Units/InferenceBackendFlint.hs b/src/Camfort/Specification/Units/InferenceBackendFlint.hs
--- a/src/Camfort/Specification/Units/InferenceBackendFlint.hs
+++ b/src/Camfort/Specification/Units/InferenceBackendFlint.hs
@@ -24,24 +24,14 @@
 
 module Camfort.Specification.Units.InferenceBackendFlint where
 
-import System.IO.Unsafe (unsafePerformIO)
-import Numeric.LinearAlgebra
-  ( atIndex, (<>), (><)
-  , rank, (?)
-  , rows, cols
-  , subMatrix, diag
-  , fromBlocks, ident
-  )
+import           Control.Monad
+import           Data.List (partition)
+-- import           Debug.Trace (trace, traceM, traceShowM)
+import           Foreign
+import           Foreign.C.Types
+import           Numeric.LinearAlgebra (atIndex, rows, cols)
 import qualified Numeric.LinearAlgebra as H
-
-import Control.Monad
-
-import Data.List (findIndex, partition, foldl')
-
-import Foreign
-import Foreign.Ptr
-import Foreign.C.Types
-import Debug.Trace (trace, traceM, traceShowM)
+import           System.IO.Unsafe (unsafePerformIO)
 
 foreign import ccall unsafe "flint/fmpz_mat.h fmpz_mat_init" fmpz_mat_init :: Ptr FMPZMat -> CLong -> CLong -> IO ()
 foreign import ccall unsafe "flint/fmpz_mat.h fmpz_mat_set" fmpz_mat_set :: Ptr FMPZMat -> Ptr FMPZMat -> IO ()
@@ -88,30 +78,30 @@
   peek _ = undefined
   poke _ = undefined
 
-testFlint = do
-  traceM "***********************8 testFlint 8***********************"
-  alloca $ \ a -> do
-    alloca $ \ b -> do
-      alloca $ \ den -> do
-        let n = 10
-        fmpz_mat_init a n n
-        fmpz_mat_init b n n
-        forM_ [0..n-1] $ \ i -> do
-          forM_ [0..n-1] $ \ j -> do
-            e <- fmpz_mat_entry a i j
-            fmpz_set_si e (2 * i + j)
-
-        -- fmpz_mat_mul b a a
-        r <- fmpz_mat_rref b den a
-        fmpz_mat_print_pretty a
-        fmpz_mat_print_pretty b
-        d <- peek den
-        traceM $ "r = " ++ show r ++ " den = " ++ show d
-        fmpz_mat_hnf b a
-        fmpz_mat_print_pretty b
-        fmpz_mat_clear a
-        fmpz_mat_clear b
+-- testFlint :: IO ()
+-- testFlint = do
+--   traceM "***********************8 testFlint 8***********************"
+--   alloca $ \ a -> do
+--     alloca $ \ b -> do
+--       alloca $ \ den -> do
+--         let n = 10
+--         fmpz_mat_init a n n
+--         fmpz_mat_init b n n
+--         forM_ [0..n-1] $ \ i -> do
+--           forM_ [0..n-1] $ \ j -> do
+--             e <- fmpz_mat_entry a i j
+--             fmpz_set_si e (2 * i + j)
 
+--         -- fmpz_mat_mul b a a
+--         r <- fmpz_mat_rref b den a
+--         fmpz_mat_print_pretty a
+--         fmpz_mat_print_pretty b
+--         d <- peek den
+--         traceM $ "r = " ++ show r ++ " den = " ++ show d
+--         fmpz_mat_hnf b a
+--         fmpz_mat_print_pretty b
+--         fmpz_mat_clear a
+--         fmpz_mat_clear b
 
 rref :: H.Matrix Double -> (H.Matrix Double, Int, Int)
 rref m = unsafePerformIO $ do
@@ -170,7 +160,6 @@
       let m' = H.fromLists lists
       fmpz_mat_clear inputM
       fmpz_mat_clear outputM
-      let Just (m'', _) = inv m'
       return m'
 
 inv :: H.Matrix Double -> Maybe (H.Matrix Double, Int)
@@ -191,7 +180,7 @@
 
         -- DEBUG:
         fmpz_mat_print_pretty outputM
-        traceM $ "r = " ++ show r ++ " den = " ++ show d
+        -- traceM $ "r = " ++ show r ++ " den = " ++ show d
         --
 
         lists <- forM [0..numRows-1] $ \ i -> do
@@ -231,11 +220,12 @@
 withWindow :: Ptr FMPZMat -> CLong -> CLong -> CLong -> CLong -> (Ptr FMPZMat -> IO b) -> IO b
 withWindow underM r1 c1 r2 c2 f = do
   alloca $ \ window -> do
-    fmpz_mat_window_init window underM r1 c2 r2 c2
+    fmpz_mat_window_init window underM r1 c1 r2 c2
     x <- f window
     fmpz_mat_window_clear window
     return x
 
+flintToHMatrix :: CLong -> CLong -> Ptr FMPZMat -> IO (H.Matrix Double)
 flintToHMatrix numRows numCols flintM = do
   lists <- forM [0..numRows-1] $ \ i -> do
     forM [0..numCols-1] $ \ j -> do
@@ -243,21 +233,23 @@
       fromIntegral `fmap` fmpz_get_si e
   return $ H.fromLists lists
 
+pokeM :: Ptr FMPZMat -> CLong -> CLong -> CLong -> IO ()
 pokeM flintM i j v = do
   e <- fmpz_mat_entry flintM i j
   fmpz_set_si e v
 
+peekM :: Ptr FMPZMat -> CLong -> CLong -> IO CLong
 peekM flintM i j = do
   e <- fmpz_mat_entry flintM i j
   fmpz_get_si e
 
+copyMatrix :: Ptr FMPZMat -> Ptr FMPZMat -> CLong -> CLong -> CLong -> CLong -> IO ()
 copyMatrix m1 m2 r1 c1 r2 c2 =
   forM_ [r1 .. r2-1] $ \ i ->
     forM_ [c1 .. c2-1] $ \ j ->
       peekM m2 i j >>= pokeM m1 i j
 
 
--- 'windows' don't seem to work?
 -- copyMatrix' m1 m2 r1 c1 r2 c2 =
 --   withWindow m2 r1 c1 r2 c2 $ \ w2 ->
 --     withWindow m1 r1 c1 r2 c2 $ \ w1 -> do
@@ -317,12 +309,13 @@
     indexLookup j | j < numCols = j
                   | otherwise = indices !! (j `mod` numCols)
     indices = map indexLookup $ concatMap snd rs1
-    (rs1, (m',[]):rs2) = break (null . snd) results
+    (rs1, (m',[]):_) = break (null . snd) results
     results = tail $ iterate (normHNF' . fst) (m, [])
 
 normHNF' :: H.Matrix Double -> (H.Matrix Double, [Int])
 normHNF' m = fmap (map fromIntegral) . unsafePerformIO $ withMatrix m normhnf
 
+normhnf :: (CLong, CLong, Ptr FMPZMat) -> IO (H.Matrix Double, [CLong])
 normhnf (numRows, numCols, inputM) = do
   withBlankMatrix numRows numCols $ \ outputM -> do
     fmpz_mat_hnf outputM inputM
@@ -358,6 +351,7 @@
           where
             restABS   = map abs rest
             minNLcoef = minimum (filter (/= 0) restABS)
+        genColCons _ = error "normhnf: genColCons: impossible: missing leading co-efficient"
 
     let consCols = map genColCons consCands
 
@@ -379,7 +373,7 @@
       -- apply the operations on the extra space to write the
       -- additional rows and columns providing the additional
       -- constraints
-      forM (zip [rank..] ops) $ \ (i, op) -> op outputM' i
+      forM_ (zip [rank..] ops) $ \ (i, op) -> op outputM' i
 
       -- re-run HNF
       withBlankMatrix numRows' numCols' $ \ outputM'' -> do
@@ -387,10 +381,10 @@
         rank' <- fmpz_mat_rank outputM''
         -- scale the rows so that it is a RREF, returning the indices
         -- where leading-coefficients had to be scaled to 1.
-        indices <- elemrowscale outputM'' rank' numCols'
+        indices' <- elemrowscale outputM'' rank' numCols'
         -- HNF allows non-zeroes above the leading-coefficients that
         -- were greater than 1, so also fix that to bring into RREF.
-        elemrowadds outputM'' rank' numCols' indices
+        elemrowadds outputM'' rank' numCols' indices'
         -- convert back to HMatrix form
         h <- flintToHMatrix rank' numCols' outputM''
         return (h, map fst consCols)
@@ -399,6 +393,7 @@
 -- rows accordingly to reach RREF
 --
 -- precondition: matrix outputM is in HNF
+elemrowscale :: Ptr FMPZMat -> CLong -> CLong -> IO [(CLong, CLong)]
 elemrowscale outputM rank numCols = do
   -- column indices of leading co-efficients > 1
   lcoefs <- filter ((> 1) . head . snd) <$> forM [0 .. rank-1] (\ i -> do
@@ -422,7 +417,8 @@
 -- just scaled the leading-coefficient to 1 and now we must look to
 -- see if there are any non-zeroes in the column above the
 -- leading-coefficient, because that is allowed by HNF.
-elemrowadds outputM rank numCols indices = do
+elemrowadds :: Ptr FMPZMat -> CLong -> CLong -> [(CLong, CLong)] -> IO ()
+elemrowadds outputM _ numCols indices = do
   -- look for non-zero members of the columns above the
   -- leading-coefficient and wipe them out.
   forM_ indices $ \ (lcI, lcJ) -> do
@@ -446,22 +442,24 @@
 
 --------------------------------------------------
 
-m1 = (8><6)
- [ 1.0, 0.0, 0.0, -1.0,  0.0,  0.0
- , 0.0, 1.0, 0.0,  0.0, -1.0,  0.0
- , 0.0, 0.0, 1.0,  0.0,  0.0, -1.0
- , 1.0, 0.0, 0.0, -1.0,  0.0,  0.0
- , 0.0, 1.0, 0.0,  0.0, -1.0,  0.0
- , 0.0, 0.0, 1.0,  0.0,  0.0, -1.0
- , 0.0, 0.0, 0.0,  1.0, -4.0,  0.0
- , 0.0, 0.0, 0.0,  0.0,  4.0, -3.0 ] :: H.Matrix Double
+-- m1 :: H.Matrix Double
+-- m1 = (8><6)
+--  [ 1.0, 0.0, 0.0, -1.0,  0.0,  0.0
+--  , 0.0, 1.0, 0.0,  0.0, -1.0,  0.0
+--  , 0.0, 0.0, 1.0,  0.0,  0.0, -1.0
+--  , 1.0, 0.0, 0.0, -1.0,  0.0,  0.0
+--  , 0.0, 1.0, 0.0,  0.0, -1.0,  0.0
+--  , 0.0, 0.0, 1.0,  0.0,  0.0, -1.0
+--  , 0.0, 0.0, 0.0,  1.0, -4.0,  0.0
+--  , 0.0, 0.0, 0.0,  0.0,  4.0, -3.0 ]
 
-m2 = (8><6)
- [ 1.0, 0.0, 0.0, -1.0,  0.0,  0.0
- , 0.0, 1.0, 0.0,  0.0, -1.0,  0.0
- , 0.0, 0.0, 1.0,  0.0,  0.0, -1.0
- , 1.0, 0.0, 0.0, -1.0,  0.0,  0.0
- , 0.0, 1.0, 0.0,  0.0, -1.0,  0.0
- , 0.0, 0.0, 1.0,  0.0,  0.0, -1.0
- , 0.0, 0.0, 0.0,  1.0, -6.0,  0.0
- , 0.0, 0.0, 0.0,  0.0,  6.0, -4.0 ] :: H.Matrix Double
+-- m2 :: H.Matrix Double
+-- m2 = (8><6)
+--  [ 1.0, 0.0, 0.0, -1.0,  0.0,  0.0
+--  , 0.0, 1.0, 0.0,  0.0, -1.0,  0.0
+--  , 0.0, 0.0, 1.0,  0.0,  0.0, -1.0
+--  , 1.0, 0.0, 0.0, -1.0,  0.0,  0.0
+--  , 0.0, 1.0, 0.0,  0.0, -1.0,  0.0
+--  , 0.0, 0.0, 1.0,  0.0,  0.0, -1.0
+--  , 0.0, 0.0, 0.0,  1.0, -6.0,  0.0
+--  , 0.0, 0.0, 0.0,  0.0,  6.0, -4.0 ]
diff --git a/src/Camfort/Specification/Units/InferenceBackendSBV.hs b/src/Camfort/Specification/Units/InferenceBackendSBV.hs
--- a/src/Camfort/Specification/Units/InferenceBackendSBV.hs
+++ b/src/Camfort/Specification/Units/InferenceBackendSBV.hs
@@ -21,41 +21,19 @@
   ( inconsistentConstraints, criticalVariables, inferVariables, genUnitAssignments )
 where
 
-import Data.Char
-import Data.Tuple (swap)
-import Data.Maybe (maybeToList, catMaybes, fromMaybe)
-import Data.List ((\\), isPrefixOf, findIndex, partition, sortBy, group, groupBy, tails, transpose, nub, intercalate, foldl')
-import Data.Generics.Uniplate.Operations (rewrite, transformBi)
-import Debug.Trace (trace, traceShowM, traceM)
-import Control.Monad
-import Control.Monad.ST
-import Control.Arrow (first, second)
-import qualified Data.Map.Strict as M
-import qualified Data.Set as S
-import qualified Data.Array as A
-import System.IO.Unsafe (unsafePerformIO)
-import Data.SBV -- ( transcript, SatResult(..), SMTResult(Unknown), Symbolic, SBool, SInteger, SBV
-                -- , satWith, z3, getModelDictionary, fromCW, true, namedConstraint, (.==)
-                -- , sInteger, literal, bAnd, Predicate, getModelValue, setOption )
-  hiding (engine)
-import Data.SBV.Control
-import Data.Ord (comparing)
-import Data.Function (on)
-
-import Camfort.Specification.Units.Environment
+import           Camfort.Specification.Units.BackendTypes
+import           Camfort.Specification.Units.Environment
 import qualified Camfort.Specification.Units.InferenceBackend as MatrixBackend
-import Camfort.Specification.Units.BackendTypes
-
-import Numeric.LinearAlgebra (
-    atIndex, (<>), rank, (?), rows, cols,
-    takeColumns, dropRows, subMatrix, diag, fromBlocks,
-    ident,
-  )
-import qualified Numeric.LinearAlgebra as H
-import Numeric.LinearAlgebra.Devel (
-    newMatrix, readMatrix, writeMatrix, runSTMatrix, freezeMatrix, STMatrix
-  )
-
+import           Control.Monad
+import           Data.Function (on)
+import           Data.List (partition, sortBy, groupBy, nub)
+import qualified Data.Map.Strict as M
+import           Data.Maybe (catMaybes, fromMaybe)
+import           Data.Ord (comparing)
+import           Data.SBV hiding (engine, name)
+import           Data.SBV.Control
+import           Prelude hiding (pred)
+import           System.IO.Unsafe (unsafePerformIO)
 
 --------------------------------------------------
 
@@ -63,7 +41,7 @@
 -- inference or checking to work.
 criticalVariables :: Constraints -> [UnitInfo]
 criticalVariables cons = case engine cons of
-  Left (core, labeledCons) -> []
+  Left _ -> []
   Right (_, suggests) -> suggests
 
 -- | Returns just the list of constraints that were identified as
@@ -82,21 +60,26 @@
 inferVariables cons = solvedVars
   where
     -- We are only interested in reporting the solutions to variables.
-    solvedVars = [ (vv, unit) | v@(UnitVar vv, unit) <- unitAssignments ] ++
-                 [ (vv, unit) | v@(UnitParamVarAbs (_, vv), unit) <- unitAssignments ]
+    solvedVars = [ (vv, unit) | (UnitVar vv, unit) <- unitAssignments ] ++
+                 [ (vv, unit) | (UnitParamVarAbs (_, vv), unit) <- unitAssignments ]
     unitAssignments = genUnitAssignments cons
 
 --------------------------------------------------
 
+-- FIXME
+approxEq :: Double -> Double -> Bool
 approxEq a b = abs (b - a) < epsilon
+epsilon :: Double
 epsilon = 0.001 -- arbitrary
 
 --------------------------------------------------
 
+negateCons :: [UnitInfo] -> [UnitInfo]
 negateCons = map (\ (UnitPow u k) -> UnitPow u (-k))
 
-negatePosAbs (UnitPow (UnitParamPosAbs x) k) = UnitPow (UnitParamPosAbs x) (-k)
-negatePosAbs u                               = u
+-- negatePosAbs :: UnitInfo -> UnitInfo
+-- negatePosAbs (UnitPow (UnitParamPosAbs x) k) = UnitPow (UnitParamPosAbs x) (-k)
+-- negatePosAbs u                               = u
 
 --------------------------------------------------
 
@@ -111,10 +94,10 @@
 
 -- | Shift UnitNames/EAPAbs poly units to the RHS, and all else to the LHS.
 shiftTerms :: (UnitInfo -> Bool) -> ([UnitInfo], [UnitInfo]) -> ShiftedConstraint
-shiftTerms isUnitRHS (lhs, rhs) = (lhsOk ++ negateCons rhsShift, rhsOk ++ negateCons lhsShift)
+shiftTerms isUnitRHS' (lhs, rhs) = (lhsOk ++ negateCons rhsShift, rhsOk ++ negateCons lhsShift)
   where
-    (lhsOk, lhsShift)           = partition (not . isUnitRHS) lhs
-    (rhsOk, rhsShift)           = partition isUnitRHS rhs
+    (lhsOk, lhsShift)           = partition (not . isUnitRHS') lhs
+    (rhsOk, rhsShift)           = partition isUnitRHS' rhs
 
 -- | Translate all constraints into a LHS, RHS side of units.
 flattenConstraints :: Constraints         -> [([UnitInfo], [UnitInfo])]
@@ -122,10 +105,10 @@
 
 --------------------------------------------------
 
-type Z3 a   = Symbolic a
+-- type Z3 a   = Symbolic a
 type Symbol = SInteger
 
-type UnitZ3Map = M.Map (UnitInfo, UnitInfo) Symbol
+-- type UnitZ3Map = M.Map (UnitInfo, UnitInfo) Symbol
 
 type LhsUnit         = UnitInfo
 type RhsUnit         = UnitInfo
@@ -177,7 +160,7 @@
 
 genUnitAssignments :: Constraints -> [(UnitInfo, UnitInfo)]
 genUnitAssignments cons = case engine cons of
-  Left (core, labeledCons) -> []
+  Left _ -> []
   Right (sub, _) -> subToList sub
 
 basicOptimisations :: Constraints -> Constraints
@@ -211,7 +194,7 @@
 
         -- temporary arrangement for now to identify constraints
         let encCons = encodeConstraints basisMap nameUIMap nameSIntMap shiftedCons
-        labeledCons <- forM (zip [1..] encCons) $ \ (i, (sbool, augCon)) -> do
+        labeledCons <- forM (zip [(1::Int)..] encCons) $ \ (i, (sbool, augCon)) -> do
           namedConstraint ("c"++show i) sbool
           return ("c"++show i, augCon)
 
@@ -266,7 +249,7 @@
 type AugConstraint = (Constraint, String)
 
 encodeConstraints :: BasisMap -> NameUnitInfoMap -> NameSIntegerMap -> ShiftedConstraints -> [(SBool, AugConstraint)]
-encodeConstraints basisMap nameUIMap nameSIntMap shiftedCons = do
+encodeConstraints basisMap _ nameSIntMap shiftedCons = do
   let getLhsSymbol :: String -> UnitInfo -> (Symbol, Integer)
       getLhsSymbol rhsName (UnitPow u p) = (uSym, floor p * p')
         where (uSym, p') = getLhsSymbol rhsName u
@@ -285,37 +268,37 @@
           lhsTerms :: [SInteger]
           lhsTerms = [ lhsSym * literal lhsPow | lhs_i <- lhs
                                                , let (lhsSym, lhsPow) = getLhsSymbol rhsName lhs_i ]
-          msg = intercalate " + " [ lhsName ++ "(" ++ rhsName ++ ") * " ++ show lhsPow
-                                  | lhs_i <- lhs
-                                  , let (lhsName, lhsPow) = getUnitNamePow lhs_i ] ++
-                " == " ++ rhsName ++ " * " ++ show rhsPow
+          -- msg = intercalate " + " [ lhsName ++ "(" ++ rhsName ++ ") * " ++ show lhsPow
+          --                         | lhs_i <- lhs
+          --                         , let (lhsName, lhsPow) = getUnitNamePow lhs_i ] ++
+          --       " == " ++ rhsName ++ " * " ++ show rhsPow
 
   -- for each constraint having a set of LHS terms and a set of RHS terms:
   let eachConstraint :: ([UnitInfo], [UnitInfo]) -> [(SBool, AugConstraint)]
       eachConstraint (lhs, rhs) = res
         where
           con       = ConEq (foldUnits lhs) (foldUnits rhs)
-          msg       = "eachConstraint " ++ show (lhs, rhs) ++ " = " ++ show res
+          -- msg       = "eachConstraint " ++ show (lhs, rhs) ++ " = " ++ show res
           res       = catMaybes . map (eachRhs con lhs) $ rhsPowers
           -- map every RHS to its corresponding power (including 0 for those not mentioned)
           rhsPowers = M.toList . M.unionWith (+) basisMap . M.fromListWith (+) . map getUnitNamePow $ rhs
 
   concatMap eachConstraint shiftedCons
 
-showConstraints :: BasisMap -> ShiftedConstraints -> [String]
-showConstraints basisMap = map mkMsg
-  where
---    mkMsg ([], rhs) = ""
-    mkMsg (lhs, rhs) = intercalate "\n" . filter (not . null) $ map (perRhs lhs) rhsPowers
-      where
-        rhsPowers = M.toList . M.unionWith (+) basisMap . M.fromListWith (+) . map getUnitNamePow $ rhs
+-- showConstraints :: BasisMap -> ShiftedConstraints -> [String]
+-- showConstraints basisMap = map mkMsg
+--   where
+-- --    mkMsg ([], rhs) = ""
+--     mkMsg (lhs, rhs) = intercalate "\n" . filter (not . null) $ map (perRhs lhs) rhsPowers
+--       where
+--         rhsPowers = M.toList . M.unionWith (+) basisMap . M.fromListWith (+) . map getUnitNamePow $ rhs
 
-    perRhs lhs (rhsName, rhsPow) = msg
-      where
-        msg = intercalate " + " [ lhsName ++ "(" ++ rhsName ++ ") * " ++ show lhsPow
-                                | lhs_i <- lhs
-                                , let (lhsName, lhsPow) = getUnitNamePow lhs_i ] ++
-              " == " ++ rhsName ++ " * " ++ show rhsPow
+--     perRhs lhs (rhsName, rhsPow) = msg
+--       where
+--         msg = intercalate " + " [ lhsName ++ "(" ++ rhsName ++ ") * " ++ show lhsPow
+--                                 | lhs_i <- lhs
+--                                 , let (lhsName, lhsPow) = getUnitNamePow lhs_i ] ++
+--               " == " ++ rhsName ++ " * " ++ show rhsPow
 
 
 data ValueInfo
@@ -335,8 +318,8 @@
       nvMap <- extractSIntValues nameSIntMap
       push 1
       disallowValues nameSIntMap nvMap
-      cs <- checkSat
-      case cs of
+      cs' <- checkSat
+      case cs' of
         Sat -> do
           nvMap' <- extractSIntValues nameSIntMap
           let nvMap'' = M.unionWith nvUnion nvMap nvMap'
@@ -347,12 +330,14 @@
           return $ Right nvMap
     _ -> error "unknown"
 
-identifyMultipleVISet :: NameUnitInfoMap -> NameValueInfoMap -> [UnitInfo]
-identifyMultipleVISet nameUIMap = nub . map fst . catMaybes . map (`M.lookup` nameUIMap) . M.keys . M.filter isMultipleVISet
+-- identifyMultipleVISet :: NameUnitInfoMap -> NameValueInfoMap -> [UnitInfo]
+-- identifyMultipleVISet nameUIMap = nub . map fst . catMaybes . map (`M.lookup` nameUIMap) . M.keys . M.filter isMultipleVISet
 
-isMultipleVISet (VISet (_:_:_)) = True
-isMultipleVISet _               = False
+-- isMultipleVISet :: ValueInfo -> Bool
+-- isMultipleVISet (VISet (_:_:_)) = True
+-- isMultipleVISet _               = False
 
+nvUnion :: ValueInfo -> ValueInfo -> ValueInfo
 nvUnion (VISet xs) (VISet ys) = VISet . nub $ xs ++ ys
 nvUnion x y = error $ "nvUnion on (" ++ show x ++ ", " ++ show y ++ ")"
 
@@ -361,14 +346,14 @@
   where convert (name, sInt) = ((name,) . VISet . (:[])) <$> getValue sInt
 
 disallowValues :: NameSIntegerMap -> NameValueInfoMap -> Query ()
-disallowValues nameSIntMap nvMap = constrain . bOr . catMaybes $ map mkNotEq (M.toList nvMap)
+disallowValues nameSIntMap nvMap = constrain . sOr . catMaybes $ map mkNotEq (M.toList nvMap)
   where
     mkNotEq (name, VISet vs@(_:_))
-      | Just sInt <- M.lookup name nameSIntMap = Just . bAnd $ map ((sInt ./=) . literal) vs
+      | Just sInt <- M.lookup name nameSIntMap = Just . sAnd $ map ((sInt ./=) . literal) vs
     mkNotEq _                                = Nothing
 
-disallowCurrentValues :: NameSIntegerMap -> Query ()
-disallowCurrentValues nameSIntMap = extractSIntValues nameSIntMap >>= disallowValues nameSIntMap
+-- disallowCurrentValues :: NameSIntegerMap -> Query ()
+-- disallowCurrentValues nameSIntMap = extractSIntValues nameSIntMap >>= disallowValues nameSIntMap
 
 -- Interpret results.
 
@@ -381,8 +366,8 @@
 
 interpret :: NameUnitInfoMap -> NameValueInfoMap -> Query Sub
 interpret nameUIMap nvMap = do
-  let lhsU = fst . snd
-  let unitGroups = groupBy ((==) `on` lhsU) . sortBy (comparing lhsU) $ M.toList nameUIMap
+  let getLhsU = fst . snd
+  let unitGroups = groupBy ((==) `on` getLhsU) . sortBy (comparing getLhsU) $ M.toList nameUIMap
 
   -- unitGroups =
   --   [ [(name1_1, (lhs1, rhs1)), (name1_2, (lhs1, rhs2)), ...]
@@ -390,7 +375,7 @@
   --   , ...]
 
   let eachName :: (String, (LhsUnit, RhsUnit)) -> Query (Maybe UnitInfo)
-      eachName (lhsName, (lhsU, rhsU)) = do
+      eachName (lhsName, (_, rhsU)) = do
         case M.lookup lhsName nvMap of
           Just (VISet [0]) -> return . Just $ UnitlessVar
           Just (VISet [x]) -> return . Just $ UnitPow rhsU (fromInteger x)
diff --git a/src/Camfort/Specification/Units/ModFile.hs b/src/Camfort/Specification/Units/ModFile.hs
--- a/src/Camfort/Specification/Units/ModFile.hs
+++ b/src/Camfort/Specification/Units/ModFile.hs
@@ -20,27 +20,25 @@
   , dumpModFileCompiledUnits
   ) where
 
+import           Camfort.Analysis (analysisModFiles)
+import           Camfort.Specification.Units.Annotation (UA)
+import           Camfort.Specification.Units.Environment (Constraint(..), foldUnits, UnitInfo(..), colSort, Constraints)
+import           Camfort.Specification.Units.InferenceBackend (flattenConstraints, flattenUnits, genUnitAssignments')
+import           Camfort.Specification.Units.Monad
 import           Control.Monad.State (get, gets, lift)
 import           Data.Binary (Binary, decodeOrFail, encode)
-import qualified Data.ByteString.Lazy.Char8 as LB
 import           Data.Data (Data)
 import           Data.Generics.Uniplate.Operations (universeBi)
 import           Data.List (partition)
+import qualified Data.Map as M
 import           Data.Maybe (mapMaybe, catMaybes)
-import qualified Data.Map                   as M
-import qualified Data.Set                   as S
+import qualified Data.Set as S
 import           Data.Typeable (Typeable)
 import           GHC.Generics (Generic)
-
 import qualified Language.Fortran.AST as F
 import qualified Language.Fortran.Analysis as FA
 import           Language.Fortran.Util.ModFile
-
-import Camfort.Analysis (analysisModFiles)
-import Camfort.Specification.Units.Annotation (UA)
-import Camfort.Specification.Units.Environment (Constraint(..), foldUnits, UnitInfo(..), colSort, Constraints)
-import Camfort.Specification.Units.InferenceBackend (flattenConstraints, flattenUnits, genUnitAssignments, genUnitAssignments')
-import Camfort.Specification.Units.Monad
+import           Prelude hiding (mod)
 
 -- | The data-structure stored in 'fortran-src mod files'
 data CompiledUnits = CompiledUnits
diff --git a/src/Camfort/Specification/Units/Monad.hs b/src/Camfort/Specification/Units/Monad.hs
--- a/src/Camfort/Specification/Units/Monad.hs
+++ b/src/Camfort/Specification/Units/Monad.hs
@@ -56,24 +56,13 @@
   , runUnitAnalysis
   ) where
 
-import Control.Monad.State.Strict
-import Control.Monad.Reader
-import Data.Binary (Binary)
-import Data.Typeable (Typeable)
-import Data.Char (toLower)
-import Data.Data (Data)
-import Data.List (find, isPrefixOf)
-import GHC.Generics (Generic)
+import           Camfort.Analysis
+import           Camfort.Specification.Units.Annotation (UA)
+import           Camfort.Specification.Units.Environment (Constraints, VV)
+import           Camfort.Specification.Units.MonadTypes
+import           Control.Monad.Reader
+import           Control.Monad.State.Strict
 import qualified Language.Fortran.AST as F
-import Language.Fortran.Util.ModFile (ModFiles)
-
-import Camfort.Analysis
-import Camfort.Input
-import Camfort.Analysis.Annotations (Annotation)
-import Camfort.Specification.Units.Annotation (UA)
-import Camfort.Specification.Units.Environment (UnitInfo, Constraints, VV, PP)
-
-import Camfort.Specification.Units.MonadTypes
 
 unitOpts0 :: UnitOpts
 unitOpts0 = UnitOpts LitMixed
diff --git a/src/Camfort/Specification/Units/MonadTypes.hs b/src/Camfort/Specification/Units/MonadTypes.hs
--- a/src/Camfort/Specification/Units/MonadTypes.hs
+++ b/src/Camfort/Specification/Units/MonadTypes.hs
@@ -3,26 +3,22 @@
 
 module Camfort.Specification.Units.MonadTypes where
 
+import           Camfort.Analysis
+import           Camfort.Analysis.Annotations (Annotation)
+import           Camfort.Specification.Units.Annotation (UA)
+import           Camfort.Specification.Units.Environment (Constraints, PP, UnitInfo, VV)
 import           Control.Monad.Reader
 import           Control.Monad.State.Strict
-import           Data.Binary                             (Binary)
-import           Data.Char                               (toLower)
-import           Data.Data                               (Data)
-import qualified Data.IntMap.Strict                      as IM
-import           Data.List                               (find, isPrefixOf)
-import qualified Data.Map.Strict                         as M
-import qualified Data.Set                                as S
-import           Data.Typeable                           (Typeable)
-import           GHC.Generics                            (Generic)
-import qualified Language.Fortran.AST                    as F
-import           Language.Fortran.Util.ModFile           (ModFiles)
-
-import           Camfort.Analysis
-import           Camfort.Analysis.Annotations            (Annotation)
-import           Camfort.Input
-import           Camfort.Specification.Units.Annotation  (UA)
-import           Camfort.Specification.Units.Environment (Constraints, PP,
-                                                          UnitInfo, VV)
+import           Data.Binary (Binary)
+import           Data.Char (toLower)
+import           Data.Data (Data)
+import qualified Data.IntMap.Strict as IM
+import           Data.List (find, isPrefixOf)
+import qualified Data.Map.Strict as M
+import qualified Data.Set as S
+import           Data.Typeable (Typeable)
+import           GHC.Generics (Generic)
+import qualified Language.Fortran.AST as F
 
 --------------------------------------------------------------------------------
 --  Environment
diff --git a/src/Camfort/Specification/Units/Synthesis.hs b/src/Camfort/Specification/Units/Synthesis.hs
--- a/src/Camfort/Specification/Units/Synthesis.hs
+++ b/src/Camfort/Specification/Units/Synthesis.hs
@@ -20,21 +20,19 @@
   (runSynthesis)
 where
 
-import Data.Maybe
-import qualified Data.Set as S
-import Data.Generics.Uniplate.Operations
-import Control.Monad.State.Strict hiding (gets)
-
-import qualified Language.Fortran.AST as F
-import qualified Language.Fortran.Analysis as FA
-import qualified Language.Fortran.Util.Position as FU
-
-import           Camfort.Analysis.Annotations hiding (Unitless)
+import           Camfort.Analysis.Annotations
 import           Camfort.Specification.Units.Analysis (puName, puSrcName)
 import           Camfort.Specification.Units.Annotation (UA)
 import qualified Camfort.Specification.Units.Annotation as UA
 import           Camfort.Specification.Units.Environment
 import           Camfort.Specification.Units.Monad
+import           Control.Monad.State.Strict hiding (gets)
+import           Data.Generics.Uniplate.Operations
+import           Data.Maybe
+import qualified Data.Set as S
+import qualified Language.Fortran.AST as F
+import qualified Language.Fortran.Analysis as FA
+import qualified Language.Fortran.Util.Position as FU
 
 -- | Insert unit declarations into the ProgramFile as comments.
 runSynthesis :: Char -> [(VV, UnitInfo)] -> UnitSolver [(VV, UnitInfo)]
@@ -57,7 +55,7 @@
   pf    <- usProgramFile `fmap` get
   gvSet <- usGivenVarSet `fmap` get
   newBs <- fmap catMaybes . forM (universeBi decls) $ \ e -> case e of
-    e@(F.ExpValue _ _ (F.ValVariable _))
+    (F.ExpValue _ _ (F.ValVariable _))
       | vname `S.notMember` gvSet                     -- not a member of the already-given variables
       , Just u <- lookup (vname, sname) vars -> do    -- and a unit has been inferred
         -- Create new annotation which labels this as a refactored node.
@@ -117,4 +115,5 @@
 synthProgramUnit marker vars pus pu = fmap (:pus) $ descendBiM (synthProgramUnits marker vars) pu
 
 -- Pretty print a unit declaration.
+showUnitDecl :: ([Char], UnitInfo) -> [Char]
 showUnitDecl (sname, u) = "unit(" ++ show u ++ ") :: " ++ sname
diff --git a/src/Camfort/Transformation/CommonBlockElim.hs b/src/Camfort/Transformation/CommonBlockElim.hs
--- a/src/Camfort/Transformation/CommonBlockElim.hs
+++ b/src/Camfort/Transformation/CommonBlockElim.hs
@@ -23,29 +23,28 @@
   ( commonElimToModules
   ) where
 
-import Control.Monad
-import Control.Monad.State.Lazy
-import Control.Monad.Writer.CPS (execWriter, tell)
-
-import Data.Data
-import Data.Void
-import Data.Function (on)
-import Data.List
+import           Camfort.Analysis
+import           Camfort.Analysis.Annotations
+import           Camfort.Helpers
+import           Camfort.Helpers.Syntax
+import           Control.Monad hiding (ap)
+import           Control.Monad.State.Lazy hiding (ap)
+import           Control.Monad.Writer.Lazy (execWriter, tell)
+import           Data.Data
+import           Data.Function (on)
+import           Data.Generics.Uniplate.Operations
+import           Data.List hiding (init)
 import qualified Data.Map as M
-import Data.Generics.Uniplate.Operations
-
+import           Data.Maybe (fromMaybe)
+import           Data.Void
 import qualified Language.Fortran.AST as F
 import qualified Language.Fortran.Analysis as FA
-import qualified Language.Fortran.Analysis.Types as FAT
 import qualified Language.Fortran.Analysis.Renaming as FAR
-import qualified Language.Fortran.Util.Position as FU
+import qualified Language.Fortran.Analysis.Types as FAT
 import qualified Language.Fortran.ParserMonad as PM
 import qualified Language.Fortran.PrettyPrint as PP
-
-import Camfort.Analysis
-import Camfort.Helpers
-import Camfort.Helpers.Syntax
-import Camfort.Analysis.Annotations
+import qualified Language.Fortran.Util.Position as FU
+import           Prelude hiding (mod, init)
 
 -- Typed common-block representation
 -- Tuple of:
@@ -167,9 +166,10 @@
 -- particular Common) (need to do gorouping, but sortBy is used
 -- already so... (IS THIS STABLE- does this matter?))
 
-commonName Nothing  = "Common"
-commonName (Just x) = x
+commonName :: Maybe String -> String
+commonName = fromMaybe "Common"
 
+commonNameFromAST :: Maybe (F.Expression a) -> Maybe F.Name
 commonNameFromAST (Just (F.ExpValue _ _ (F.ValVariable v))) = Just v
 commonNameFromAST _ = Nothing
 
@@ -180,8 +180,8 @@
         let mkRenamerAndCommon (r, tc) (v, t) =
                            let v' = caml (commonName cname) ++ "_" ++ v
                            in (M.insert v (Just v', Nothing) r, (v', t) : tc)
-            (r, fields') = foldl' mkRenamerAndCommon (M.empty, []) fields
-        in ((fname, (pname, (cname, fields'))), Just r)
+            (rmap, fields') = foldl' mkRenamerAndCommon (M.empty, []) fields
+        in ((fname, (pname, (cname, fields'))), Just rmap)
 
 -- From a list of typed and located common blocks group by the common
 -- block name, and then group/sort within such that the "mode" block
@@ -250,7 +250,7 @@
     -- Data-type generic reduce traversal
     reduceCollect :: (Data s, Data t, Uniplate t, Biplate t s) => (s -> Maybe a) -> t -> [a]
     reduceCollect k x = execWriter (transformBiM (\y -> do case k y of
-                                                            Just x -> tell [x]
+                                                            Just x' -> tell [x']
                                                             Nothing -> return ()
                                                            return y) x)
 
@@ -265,9 +265,9 @@
         removeDecls v (map snd tcrs') p'
       where
         pname = case F.getName p of
-                  F.Named pname -> pname
+                  F.Named n -> n
                    -- If no subname is available, use the filename
-                  _             -> fname
+                  _         -> fname
         tcrs' = lookups pname (lookups fname tcrs)
         pos = getUnitStartPosition p
         uses = mkUseStatementBlocks pos tcrs'
@@ -309,19 +309,19 @@
         matchVar :: ([F.Statement A], [F.Declarator A]) -> F.Declarator A
                  -> ([F.Statement A], [F.Declarator A])
         -- match on variable or array declaration
-        matchVar (assgns, decls) dec = case dec of
+        matchVar (assgnsNew, declsNew) dec = case dec of
           F.DeclVariable _ _ lvar@(F.ExpValue _ _ (F.ValVariable v)) _ init -> doMatchVar lvar v init
           F.DeclArray _ _ lvar@(F.ExpValue _ _ (F.ValVariable v)) _ _ init  -> doMatchVar lvar v init
-          _                                                                 -> (assgns, decls)
+          _                                                                 -> (assgnsNew, declsNew)
           where
             doMatchVar lvar v init
               | hasRenaming v rcs = case init of
                   -- Renaming exists and no default, then remove
-                  Nothing -> (assgns, decls)
+                  Nothing -> (assgnsNew, declsNew)
                     -- Renaming exists but has default, so create an
                     -- assignment for this
-                  Just initExpr -> ((F.StExpressionAssign a' (FU.getSpan dec) lvar initExpr) : assgns, decls)
-              | otherwise = (assgns, dec : decls)  -- no renaming, preserve declaration
+                  Just initExpr -> ((F.StExpressionAssign a' (FU.getSpan dec) lvar initExpr) : assgnsNew, declsNew)
+              | otherwise = (assgnsNew, dec : declsNew)  -- no renaming, preserve declaration
 
     removeDecl _ d = return d
 
@@ -358,6 +358,7 @@
 getUnitStartPosition (F.PUBlockData _ s _ []) = s
 getUnitStartPosition (F.PUBlockData _ _ _ bs) = FU.getSpan (head bs)
 getUnitStartPosition (F.PUComment _ s _) = s
+getUnitStartPosition (F.PUModule _ s _ _ _) = s
 
 renamerToUse :: RenamerCoercer -> [(F.Name, F.Name)]
 renamerToUse Nothing = []
@@ -397,8 +398,8 @@
         error "Can't generate renamer between different common blocks\n"
       where
         generate [] [] theta = theta
-        generate ((var1, ty1):vtys1) ((var2, ty2):vtys2) theta =
-            generate vtys1 vtys2 (M.insert var1 (varR, typR) theta)
+        generate ((var1, ty1):vtys1') ((var2, ty2):vtys2') theta =
+            generate vtys1' vtys2' (M.insert var1 (varR, typR) theta)
           where
              varR = if var1 == var2 then Nothing else Just var2
              typR = if ty1  ==  ty2 then Nothing else Just (ty1, ty2)
@@ -473,6 +474,7 @@
        [F.DeclArray a sp
           (F.ExpValue a sp (F.ValVariable (caml name ++ "_" ++ v))) dimDecls Nothing Nothing]
        where
-         dimDecls = F.AList a sp . flip map dims $ \ (lb, ub) -> F.DimensionDeclarator a sp (fmap exp lb) (fmap exp ub)
-         exp = F.ExpValue a sp . F.ValInteger . show
+         dimDecls = F.AList a sp . flip map dims $ \ (lb, ub) -> F.DimensionDeclarator a sp (fmap expr lb) (fmap expr ub)
+         expr = F.ExpValue a sp . F.ValInteger . show
+    toDeclarator (_, ct) = error $ "mkModule: toDeclarator: bad construct type: " ++ show ct
     decls = map toDeclBlock vtys
diff --git a/src/Camfort/Transformation/DeadCode.hs b/src/Camfort/Transformation/DeadCode.hs
--- a/src/Camfort/Transformation/DeadCode.hs
+++ b/src/Camfort/Transformation/DeadCode.hs
@@ -34,7 +34,6 @@
 import qualified Data.IntMap as IM
 import qualified Data.Set as S
 import Data.Generics.Uniplate.Operations
-import Data.Maybe
 import Control.Monad (guard)
 import Control.Monad.Trans.Writer (WriterT, runWriterT, tell)
 import Data.Monoid (Any(..), (<>))
@@ -62,7 +61,7 @@
     -- live variables
     lva   = FAD.liveVariableAnalysis gr
 
-  deadCode' flag lva pf'
+  _ <- deadCode' flag lva pf'
   pure $ fmap FA.prevAnnotation pf'
 
 deadCode' :: Bool -> FAD.InOutMap (S.Set F.Name)
diff --git a/src/Camfort/Transformation/EquivalenceElim.hs b/src/Camfort/Transformation/EquivalenceElim.hs
--- a/src/Camfort/Transformation/EquivalenceElim.hs
+++ b/src/Camfort/Transformation/EquivalenceElim.hs
@@ -21,23 +21,21 @@
   ( refactorEquivalences
   ) where
 
-import Data.List
-import Data.Void (Void)
+import           Camfort.Analysis
+import           Camfort.Analysis.Annotations
+import           Camfort.Helpers.Syntax
+import           Camfort.Transformation.DeadCode
+import           Control.Monad.State.Lazy hiding (ap)
+import           Data.Generics.Uniplate.Operations
+import           Data.List
 import qualified Data.Map as M
-import Data.Generics.Uniplate.Operations
-import Control.Monad.State.Lazy
-
+import           Data.Void (Void)
 import qualified Language.Fortran.AST as F
+import qualified Language.Fortran.Analysis as FA
+import qualified Language.Fortran.Analysis.Renaming as FAR
 import qualified Language.Fortran.Analysis.Types as FAT (analyseTypes, TypeEnv)
 import qualified Language.Fortran.Util.Position as FU
-import qualified Language.Fortran.Analysis.Renaming as FAR
-import qualified Language.Fortran.Analysis as FA
 
-import Camfort.Analysis
-import Camfort.Helpers.Syntax
-import Camfort.Analysis.Annotations
-import Camfort.Transformation.DeadCode
-
 type EquivalenceRefactoring = PureAnalysis Void Void
 
 type A1 = FA.Analysis Annotation
@@ -60,12 +58,12 @@
     refactoring
       :: FAT.TypeEnv -> F.ProgramFile A1
       -> EquivalenceRefactoring (F.ProgramFile A1)
-    refactoring tenv pf = do
-      (pf', _) <- runStateT equiv ([], 0)
-      return pf'
+    refactoring tenv pf' = do
+      (pf'', _) <- runStateT equiv ([], 0)
+      return pf''
       where
-         equiv = do pf' <- transformBiM perBlockRmEquiv pf
-                    descendBiM (addCopysPerBlockGroup tenv) pf'
+         equiv = do pf'' <- transformBiM perBlockRmEquiv pf'
+                    descendBiM (addCopysPerBlockGroup tenv) pf''
 
 addCopysPerBlockGroup
   :: FAT.TypeEnv -> [F.Block A1]
@@ -77,7 +75,7 @@
 addCopysPerBlock
   :: FAT.TypeEnv -> F.Block A1
   -> StateT RmEqState EquivalenceRefactoring [F.Block A1]
-addCopysPerBlock tenv x@(F.BlStatement _ _ _
+addCopysPerBlock tenv b@(F.BlStatement _ _ _
                  (F.StExpressionAssign a sp@(FU.SrcSpan s1 _) dstE _))
   | not (pRefactored $ FA.prevAnnotation a) = do
     -- Find all variables/cells that are equivalent to the target
@@ -85,13 +83,13 @@
     eqs <- equivalentsToExpr dstE
     -- If there is only one, then it must refer to itself, so do nothing
     if length eqs <= 1
-      then return [x]
+      then return [b]
     -- If there are more than one, copy statements must be generated
       else do
         (equivs, n) <- get
 
         -- Remove the destination from the equivalents
-        let eqs' = deleteBy (\x y -> af x == af y) dstE eqs
+        let eqs' = deleteBy (\ x y -> af x == af y) dstE eqs
 
         -- Make copy statements
         let pos = afterAligned sp
@@ -99,8 +97,8 @@
 
         let (FU.Position ao c l f p) = s1
             reportSpan i =
-              let pos = FU.Position (ao + i) c (l + i) f p
-              in (FU.SrcSpan pos pos)
+              let pos' = FU.Position (ao + i) c (l + i) f p
+              in (FU.SrcSpan pos' pos')
 
         forM_ [n..(n + length copies - 1)] $ \i -> do
           origin <- atSpanned (reportSpan i)
@@ -109,13 +107,14 @@
         -- Update refactoring state
         put (equivs, n + length eqs')
         -- Sequence original assignment with new assignments
-        return $ x : copies
+        return $ b : copies
 
 addCopysPerBlock tenv x = do
    x' <- descendBiM (addCopysPerBlockGroup tenv) x
    return [x']
 
 -- see if two expressions have the same type
+equalTypes :: FAT.TypeEnv -> F.Expression A1 -> F.Expression A1 -> Maybe FA.IDType
 equalTypes tenv e e' = do
     v1 <- extractVariable e
     v2 <- extractVariable e'
@@ -159,7 +158,7 @@
 perStatementRmEquiv
   :: F.Statement A1
   -> StateT RmEqState EquivalenceRefactoring (F.Statement A1)
-perStatementRmEquiv x@(F.StEquivalence a sp@(FU.SrcSpan spL _) equivs) = do
+perStatementRmEquiv (F.StEquivalence a sp@(FU.SrcSpan spL _) equivs) = do
     (ess, n) <- get
 
     let spL' = FU.SrcSpan spL spL
@@ -175,9 +174,9 @@
 equivalentsToExpr
   :: F.Expression A1
   -> StateT RmEqState EquivalenceRefactoring [F.Expression A1]
-equivalentsToExpr x = do
+equivalentsToExpr y = do
     (equivs, _) <- get
-    return (inGroup x equivs)
+    return (inGroup y equivs)
   where
     inGroup _ [] = []
     inGroup x (xs:xss) =
diff --git a/src/Language/Fortran/Model/Op/Eval.hs b/src/Language/Fortran/Model/Op/Eval.hs
--- a/src/Language/Fortran/Model/Op/Eval.hs
+++ b/src/Language/Fortran/Model/Op/Eval.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE MonoLocalBinds         #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MultiParamTypeClasses  #-}
diff --git a/src/Language/Fortran/Model/Repr.hs b/src/Language/Fortran/Model/Repr.hs
--- a/src/Language/Fortran/Model/Repr.hs
+++ b/src/Language/Fortran/Model/Repr.hs
@@ -105,11 +105,11 @@
 instance HFoldableAt HighRepr LogicOp where
   hfoldMap = implHfoldMap $ \case
     LogLit x     -> HRHigh (fromBool x)
-    LogNot x     -> HRHigh . bnot . getHrBool $ x
-    LogAnd x y   -> appBinop (&&&) x y
-    LogOr x y    -> appBinop (|||) x y
-    LogImpl x y  -> appBinop (==>) x y
-    LogEquiv x y -> appBinop (<=>) x y
+    LogNot x     -> HRHigh . sNot . getHrBool $ x
+    LogAnd x y   -> appBinop (.&&) x y
+    LogOr x y    -> appBinop (.||) x y
+    LogImpl x y  -> appBinop (.=>) x y
+    LogEquiv x y -> appBinop (.<=>) x y
 
     where
       appBinop (g :: SBool -> SBool -> SBool) x y =
@@ -126,7 +126,7 @@
 
 -- | Provides conversions between symbolic representations of core Fortran
 -- values and their corresponding high-level types.
-class (SymWord a) => LiftD b a | b -> a where
+class (SymVal a) => LiftD b a | b -> a where
   -- | Go from a core value to the corresponding high-level value.
   liftD :: b -> a
   -- | Go from a symbolic core value to the corresponding symbolic high-level
diff --git a/src/Language/Fortran/Model/Repr/Prim.hs b/src/Language/Fortran/Model/Repr/Prim.hs
--- a/src/Language/Fortran/Model/Repr/Prim.hs
+++ b/src/Language/Fortran/Model/Repr/Prim.hs
@@ -166,27 +166,27 @@
   PChar   -> bySymWord (0 :: Word8) getChar8
   where
     intRepr
-      :: (Integral a, SBV.SymWord a)
+      :: (Integral a, SBV.SymVal a)
       => Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
     intRepr l = case spec ^. l of
       MachineInt   -> bySymWord 0 id
       ArbitraryInt -> bySymWord (0 :: Integer) fromIntegral
 
     realRepr
-      :: (RealFloat a, SBV.SymWord a)
+      :: (RealFloat a, SBV.SymVal a)
       => Lens' PrimReprSpec (RealRepr a) -> PrimReprHandler a
     realRepr l = case spec ^. l of
       MachineFloat  -> bySymWord 0 id
       ArbitraryReal -> bySymWord (0 :: SBV.AlgReal) realToFrac
 
     boolRepr
-      :: (Integral b, SBV.SymWord b)
+      :: (Integral b, SBV.SymVal b)
       => (a -> b) -> Lens' PrimReprSpec (BoolRepr a) -> PrimReprHandler a
     boolRepr unwrap l = case spec ^. l of
       IntBool -> bySymWord 0 unwrap
       BitBool -> bySymWord (False :: Bool) (toBool . unwrap)
 
-    bySymWord :: (SBV.SymWord b) => b -> (a -> b) -> PrimReprHandler a
+    bySymWord :: (SBV.SymVal b) => b -> (a -> b) -> PrimReprHandler a
     bySymWord (repValue :: b) fromPrim =
       PrimReprHandler
       { _prhKind = SBV.kindOf repValue
diff --git a/src/Language/Fortran/Model/Singletons.hs b/src/Language/Fortran/Model/Singletons.hs
--- a/src/Language/Fortran/Model/Singletons.hs
+++ b/src/Language/Fortran/Model/Singletons.hs
@@ -49,9 +49,8 @@
 -}
 module Language.Fortran.Model.Singletons where
 
-import           Data.Singletons.Prelude
-import           Data.Singletons.Prelude.Maybe
-import           Data.Singletons.TH
+import Data.Singletons.Prelude
+import Data.Singletons.TH
 
 $(singletons
   [d|
diff --git a/src/Language/Fortran/Model/Translate.hs b/src/Language/Fortran/Model/Translate.hs
--- a/src/Language/Fortran/Model/Translate.hs
+++ b/src/Language/Fortran/Model/Translate.hs
@@ -561,6 +561,7 @@
     F.ValAssignment   -> unsupported "interface assignment"
     F.ValType s       -> unsupported "type value"
     F.ValStar         -> unsupported "star value"
+    F.ValColon        -> unsupported "colon value"
   _ -> fail "impossible: translateValue called on a non-value"
 
 
diff --git a/src/Language/Fortran/Model/Vars.hs b/src/Language/Fortran/Model/Vars.hs
--- a/src/Language/Fortran/Model/Vars.hs
+++ b/src/Language/Fortran/Model/Vars.hs
@@ -136,7 +136,7 @@
       return $ ARData valReprs
 
 arraySymbolicPrim :: (HasPrimReprHandlers r) => Prim p1 k1 i -> Prim p2 k2 a -> String -> r -> Symbolic SArr
-arraySymbolicPrim ixPrim valPrim nm = error "arraySymbolicPrim: bit-rotted in new SBV 8.0 version" -- do
+arraySymbolicPrim _ _ _ = error "arraySymbolicPrim: bit-rotted in new SBV 8.0 version" -- do
   -- k1 <- primSBVKind ixPrim
   -- k2 <- primSBVKind valPrim
   -- return $ newSArr (k1, k2) (\i -> nm ++ "_" ++ show i)
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -13,26 +13,35 @@
    limitations under the License.
 -}
 
-{-# LANGUAGE DoAndIfThenElse #-}
+{-# LANGUAGE DoAndIfThenElse, ScopedTypeVariables #-}
 
 module Main (main) where
 
 import Camfort.Analysis.Logger (LogLevel(..))
-import Camfort.Input (defaultValue)
 import Camfort.Functionality
-import Camfort.Specification.Units.Monad (LiteralsOpt(LitMixed))
 import Camfort.Specification.Hoare (PrimReprOption(..))
-
-import Language.Fortran.ParserMonad (FortranVersion(..), selectFortranVersion)
-
+import Camfort.Specification.Units.Monad (LiteralsOpt(LitMixed))
+import Control.Exception
 import Data.Maybe (fromMaybe)
 import Data.Monoid ((<>))
+import GHC.Stack
+import Language.Fortran.ParserMonad (FortranVersion(..), selectFortranVersion)
+import Options.Applicative
 import System.Directory (getCurrentDirectory)
 import System.Exit
-import Options.Applicative
 
 main :: IO ()
-main = do
+main = catch realMain stacktrace
+  where
+    stacktrace (e::AsyncException) = do
+      putStrLn "Call stack:"
+      stack <- currentCallStack
+      mapM_ putStrLn stack
+      putStrLn "Exception:"
+      print e
+
+realMain :: IO ()
+realMain = do
   currentDir <- getCurrentDirectory
   cmd <- execParser (info (commandParser currentDir) idm)
   code <- runCommand cmd
@@ -59,7 +68,6 @@
       let ro      = sioReadOptions sio
           lo      = sioLogOptions sio
           useEval = sioUseEval sio
-          inFile  = inputSource ro
       in runRO ro lo (f useEval)
     runSSO sso f =
       let ao     = ssoAnnotationOptions sso
@@ -129,9 +137,12 @@
     runCommand (CmdFPCheck ro lo)         = runRO ro lo fpCheck
     runCommand (CmdUseCheck ro lo)        = runRO ro lo useCheck
     runCommand (CmdArrayCheck ro lo)      = runRO ro lo arrayCheck
+    runCommand (CmdBasicChecks ro lo)     = maximum <$> mapM (runRO ro lo) basicChecks
     runCommand (CmdInit dir)              = camfortInitialize dir >> return 0
     runCommand CmdTopVersion              = displayVersion >> return 0
 
+basicChecks :: [CamfortEnv -> IO Int]
+basicChecks = [allocCheck, arrayCheck, fpCheck, implicitNone False, useCheck]
 
 -- | Commands supported by CamFort.
 data Command = CmdCount ReadOptions LogOptions
@@ -159,6 +170,7 @@
              | CmdFPCheck ReadOptions LogOptions
              | CmdUseCheck ReadOptions LogOptions
              | CmdArrayCheck ReadOptions LogOptions
+             | CmdBasicChecks ReadOptions LogOptions
              | CmdInit FilePath
              | CmdTopVersion
 
@@ -416,6 +428,7 @@
 
 
 cmdImplicitNone, cmdImplicitNoneAll, cmdInvariantsCheck, cmdAllocCheck, cmdFPCheck :: Parser Command
+cmdArrayCheck, cmdUseCheck, cmdBasicChecks :: Parser Command
 cmdInvariantsCheck = fmap CmdInvariantsCheck invariantsOptions
 cmdImplicitNone    = fmap CmdImplicitNone readOptions <*> logOptions
 cmdImplicitNoneAll = fmap CmdImplicitNoneAll readOptions <*> logOptions
@@ -423,6 +436,7 @@
 cmdFPCheck         = fmap CmdFPCheck readOptions <*> logOptions
 cmdUseCheck        = fmap CmdUseCheck readOptions <*> logOptions
 cmdArrayCheck      = fmap CmdArrayCheck readOptions <*> logOptions
+cmdBasicChecks     = fmap CmdBasicChecks readOptions <*> logOptions
 
 cmdRefactCommon, cmdRefactDead, cmdRefactEquivalence :: Parser Command
 cmdRefactCommon      = fmap CmdRefactCommon refactOptions
@@ -492,9 +506,9 @@
       , ("units-infer",
           ["unit-infer", "infer-units", "infer-unit"],
           cmdUnitsInfer,    "unit-of-measure inference")
-      , ("units-compile",
-          ["unit-compile", "compile-units", "compile-unit"],
-          cmdUnitsCompile,    "unit-of-measure compilation")
+      , ("units-summarise",
+          ["unit-compile", "units-summarize", "units-compile", "compile-units", "compile-unit"],
+          cmdUnitsCompile,    "unit-of-measure summarisation")
       , ("units-synth",
           ["unit-synth", "synth-units", "synth-unit"],
           cmdUnitsSynth,    "unit-of-measure synthesise specs")
@@ -513,6 +527,9 @@
       , ("array-check",
           [],
           cmdArrayCheck, "check usage of arrays")
+      , ("basic-checks",
+          [],
+          cmdBasicChecks, "run a series of basic checks: alloc, array, fp, implicit-none, use")
       ]
 
 
@@ -563,10 +580,12 @@
 
 
 -- | Current CamFort version.
-version = "0.906"
+version :: String
+version = "1.0"
 
 
 -- | Full CamFort version string.
+versionMessage :: String
 versionMessage = "CamFort " ++ version ++ " - Cambridge Fortran Infrastructure."
 
 
diff --git a/tests/Camfort/Analysis/CommentAnnotatorSpec.hs b/tests/Camfort/Analysis/CommentAnnotatorSpec.hs
--- a/tests/Camfort/Analysis/CommentAnnotatorSpec.hs
+++ b/tests/Camfort/Analysis/CommentAnnotatorSpec.hs
@@ -5,19 +5,17 @@
 
 module Camfort.Analysis.CommentAnnotatorSpec (spec) where
 
-import Test.Hspec
-
-import Data.Data
+import Camfort.Analysis.CommentAnnotator
+import Camfort.Specification.Parser (mkParser, parseError, SpecParser)
 import Control.Monad.Identity (runIdentity)
 import Control.Monad.Writer.Strict
-
+import Data.Data
 import Language.Fortran.AST
 import Language.Fortran.ParserMonad
 import Language.Fortran.Util.Position
-
-import Camfort.Analysis.CommentAnnotator
-import Camfort.Specification.Parser (mkParser, parseError, SpecParser)
+import Test.Hspec
 
+p :: SrcSpan
 p = SrcSpan (Position 0 1 1 "" Nothing) (Position 0 1 1 "" Nothing)
 
 annotateWith :: (String -> String) -> ProgramFile A -> ProgramFile A
@@ -25,6 +23,7 @@
   where trivialParser = mkParser (Right . s) []
         ignore        = const . const . pure $ ()
 
+spec :: SpecWith ()
 spec =
   describe "Comment annotator" $ do
     it "annotates with no comment blocks" $
@@ -56,35 +55,48 @@
 
 instance Linkable A where
   link a block = a { annLink = Just block }
+  linkPU = undefined
 
 -- Some helper functions
+varGen :: Name -> Expression A
 varGen x = ExpValue ea p (ValVariable x)
+intGen :: Integer -> Expression A
 intGen i = ExpValue ea p (ValInteger (show i))
-wrapBlocks bs = ProgramFile (MetaInfo { miVersion = Fortran90, miFilename = "<unknown>" }) [ pu ]
+wrapBlocks :: [Block A] -> ProgramFile A
+wrapBlocks bs' = ProgramFile (MetaInfo { miVersion = Fortran90, miFilename = "<unknown>" }) [ pu ]
   where
-    pu = PUModule ea p "my_module" bs Nothing
+    pu = PUModule ea p "my_module" bs' Nothing
 
 -- Test cases
 
 mkComment :: String -> Comment a
 mkComment = Comment . ("= "++)
 
+ea :: A
 ea = A Nothing Nothing
 
+pf :: ProgramFile A
 pf = wrapBlocks bs
+bs :: [Block A]
 bs = [ BlStatement ea p Nothing (StPause ea p Nothing) ]
 
+pf2 :: ProgramFile A
 pf2 = wrapBlocks bs2
+bs2 :: [Block A]
 bs2 =
   [ BlComment ea p (mkComment "something")
   , BlStatement ea p Nothing (StPause ea p Nothing) ]
 
+pf2e :: ProgramFile A
 pf2e = wrapBlocks bs2e
+bs2e :: [Block A]
 bs2e =
   [ BlComment (A (Just (bs2e !! 1)) (Just "hello")) p (mkComment "something")
   , BlStatement ea p Nothing (StPause ea p Nothing) ]
 
+pf3 :: ProgramFile A
 pf3 = wrapBlocks bs3
+bs3 :: [Block A]
 bs3 =
   [ BlComment ea p (mkComment "mistral")
   , BlComment ea p (mkComment "orhan")
@@ -92,7 +104,9 @@
   , BlComment ea p (mkComment "contrastin")
   , BlStatement ea p Nothing (StPause ea p Nothing) ]
 
+pf3e :: ProgramFile A
 pf3e = wrapBlocks bs3e
+bs3e :: [Block A]
 bs3e =
   [ BlComment (A (Just (last bs3e)) (Just "!!!mistral")) p (mkComment "mistral")
   , BlComment (A (Just (last bs3e)) (Just "!!!orhan")) p (mkComment "orhan")
@@ -100,7 +114,9 @@
   , BlComment (A (Just (last bs3e)) (Just "!!!contrastin")) p (mkComment "contrastin")
   , BlStatement ea p Nothing (StPause ea p Nothing) ]
 
+pf4 :: ProgramFile A
 pf4 = wrapBlocks bs4
+bs4 :: [Block A]
 bs4 =
   [ BlComment ea p (mkComment "mistral")
   , BlComment ea p (mkComment "contrastin")
@@ -109,7 +125,9 @@
   , BlComment ea p (mkComment "orchard")
   , BlStatement ea p Nothing (StExpressionAssign ea p (varGen "x") (intGen 42)) ]
 
+pf4e :: ProgramFile A
 pf4e = wrapBlocks bs4e
+bs4e :: [Block A]
 bs4e =
   [ BlComment (A (Just (bs4e !! 2)) (Just "!!!mistral")) p (mkComment "mistral")
   , BlComment (A (Just (bs4e !! 2)) (Just "!!!contrastin")) p (mkComment "contrastin")
@@ -118,13 +136,17 @@
   , BlComment (A (Just (last bs4e)) (Just "!!!orchard")) p (mkComment "orchard")
   , BlStatement ea p Nothing (StExpressionAssign ea p (varGen "x") (intGen 42)) ]
 
+pf5 :: ProgramFile A
 pf5 = wrapBlocks bs5
+bs5 :: [Block A]
 bs5 =
   [ BlComment ea p (mkComment "comment 1")
   , BlComment ea p (mkComment "comment 2")
   , BlStatement ea p Nothing (StPause ea p Nothing) ]
 
+pf5e :: ProgramFile A
 pf5e = wrapBlocks bs5e
+bs5e :: [Block A]
 bs5e =
   [ BlComment (A (Just (last bs5e)) Nothing) p (mkComment "comment 1")
   , BlComment (A (Just (last bs5e)) Nothing) p (mkComment "comment 2")
diff --git a/tests/Camfort/Analysis/ImplicitNoneSpec.hs b/tests/Camfort/Analysis/ImplicitNoneSpec.hs
--- a/tests/Camfort/Analysis/ImplicitNoneSpec.hs
+++ b/tests/Camfort/Analysis/ImplicitNoneSpec.hs
@@ -2,22 +2,13 @@
 
 module Camfort.Analysis.ImplicitNoneSpec (spec) where
 
-import Data.Binary (encodeFile)
-import Data.List (sort)
-import System.Directory (createDirectory)
-import System.FilePath ((</>), (<.>))
-import System.IO.Temp (withSystemTempDirectory)
-import Control.Lens
-
-import Language.Fortran.Util.ModFile
-import Language.Fortran.AST (ProgramUnitName(..))
-
-import Camfort.Analysis.ModFile (getModFiles)
-import Camfort.Analysis.Simple
-import Camfort.Analysis.TestUtils
-import Camfort.Analysis hiding (describe)
-
-import Test.Hspec hiding (Spec)
+import           Camfort.Analysis hiding (describe)
+import           Camfort.Analysis.Simple
+import           Camfort.Analysis.TestUtils
+import           Control.Lens
+import           Language.Fortran.AST (ProgramUnitName(..))
+import           System.FilePath ((</>))
+import           Test.Hspec hiding (Spec)
 import qualified Test.Hspec as Test
 
 spec :: Test.Spec
diff --git a/tests/Camfort/Analysis/ModFileSpec.hs b/tests/Camfort/Analysis/ModFileSpec.hs
--- a/tests/Camfort/Analysis/ModFileSpec.hs
+++ b/tests/Camfort/Analysis/ModFileSpec.hs
@@ -2,18 +2,14 @@
 
 module Camfort.Analysis.ModFileSpec (spec) where
 
-import Data.Binary (encodeFile)
-import Data.List (sort)
-import System.Directory (createDirectory)
-import System.FilePath ((</>), (<.>))
-import System.IO.Temp (withSystemTempDirectory)
-
-import Language.Fortran.Util.ModFile
-
-import Camfort.Analysis.ModFile (getModFiles)
-
-import Test.Hspec hiding (Spec)
+import           Camfort.Analysis.ModFile (getModFiles)
+import           Data.Binary (encodeFile)
+import           Data.List (sort)
+import           Language.Fortran.Util.ModFile
+import           System.FilePath ((</>), (<.>))
+import           System.IO.Temp (withSystemTempDirectory)
 import qualified Test.Hspec as Test
+import           Test.Hspec hiding (Spec)
 
 spec :: Test.Spec
 spec =
@@ -24,7 +20,7 @@
           let mkMod name = alterModFileData (const $ Just name) "mfs-name" emptyModFile
               mod1       = mkMod "file-a"
               mod2       = mkMod "file-b"
-          encodeFile (dir </> "moda" <.> modFileSuffix) mod1
-          encodeFile (dir </> "modb" <.> modFileSuffix) mod2
+          encodeFile (dir </> "moda" <.> modFileSuffix) [mod1]
+          encodeFile (dir </> "modb" <.> modFileSuffix) [mod2]
           fmap (sort . fmap (lookupModFileData "mfs-name")) . getModFiles $ dir)
         `shouldReturn` [Just "file-a", Just "file-b"]
diff --git a/tests/Camfort/Analysis/TestUtils.hs b/tests/Camfort/Analysis/TestUtils.hs
--- a/tests/Camfort/Analysis/TestUtils.hs
+++ b/tests/Camfort/Analysis/TestUtils.hs
@@ -14,20 +14,17 @@
   , testMultiFileAnalysisWithSrc
   ) where
 
-import           Control.Monad                 (forM_)
-import           Control.Monad.IO.Class
-import           System.Directory              (getCurrentDirectory)
-import           System.FilePath
-
-import           Control.Lens
-
-import qualified Language.Fortran.AST          as F
-import           Language.Fortran.Util.ModFile (ModFiles, emptyModFiles)
-
 import           Camfort.Analysis
 import           Camfort.Analysis.ModFile
 import           Camfort.Helpers
 import           Camfort.Input
+import           Control.Lens
+import           Control.Monad (forM_)
+import           Control.Monad.IO.Class
+import qualified Language.Fortran.AST as F
+import           Language.Fortran.Util.ModFile (ModFiles)
+import           System.Directory (getCurrentDirectory)
+import           System.FilePath
 
 
 data TestInput =
diff --git a/tests/Camfort/FunctionalitySpec.hs b/tests/Camfort/FunctionalitySpec.hs
--- a/tests/Camfort/FunctionalitySpec.hs
+++ b/tests/Camfort/FunctionalitySpec.hs
@@ -1,45 +1,37 @@
+{-# OPTIONS -Wno-unused-top-binds #-}
 -- TODO: Fix this
 module Camfort.FunctionalitySpec (spec) where
 
-import System.Directory (copyFile, doesDirectoryExist)
-import System.FilePath  ((</>))
-import System.IO.Silently (capture_)
-import System.IO.Temp   (withSystemTempDirectory)
-
-import           Test.Hspec hiding (Spec)
+import           Camfort.Specification.Units.Monad (LiteralsOpt(LitMixed))
+import           System.Directory (copyFile)
+import           System.FilePath ((</>))
+import           System.IO.Silently (capture_)
+import           System.IO.Temp (withSystemTempDirectory)
 import qualified Test.Hspec as Test
-
-import Camfort.Functionality
-  ( AnnotationType(ATDefault)
-  , camfortInitialize
-  , stencilsInfer
-  , unitsCheck, unitsInfer, unitsSynth )
-import Camfort.Specification.Units.Monad (LiteralsOpt(LitMixed))
+import           Test.Hspec hiding (Spec)
 
 spec :: Test.Spec
 spec = do
-  describe "camfortInitialize" $ return ()
-    -- xit "creates a .camfort directory" $
-    --   return ()
-      -- withSystemTempDirectory "camfort-test-tmp"
-      --   (\d -> camfortInitialize d >> doesDirectoryExist (d </> ".camfort"))
-      -- `shouldReturn` True
-  xdescribe "units-check" $ return ()
+  xdescribe "camfortInitialize" $ return ()
+  -- xit "creates a .camfort directory" $
+  --   withSystemTempDirectory "camfort-test-tmp"
+  --     (\d -> camfortInitialize d >> doesDirectoryExist (d </> ".camfort"))
+  --   `shouldReturn` True
+  -- xdescribe "units-check" $ return ()
   --   it "correctly detects basic cross-module inconsistent"
   --     return ()
   --     -- unitsCheckTestCrossModuleInconsistBasic
-  xdescribe "units-infer" $ return ()
+  -- xdescribe "units-infer" $ return ()
   --   it "shows consistency error with inconsistent program"
   --     return ()
   --     -- unitsInferTestCrossModuleInconsistBasic
-  xdescribe "units-synth" $ return ()
+  -- xdescribe "units-synth" $ return ()
   --   it "correct synth output with basic, consistent file"
-  --     return ()
-  --     -- unitsSynthTestBasic
-  xdescribe "stencils-infer" $ return ()
+  --     unitsSynthTestBasic
+  -- xdescribe "stencils-infer" $ return ()
   --   it "correctly infers with basic cross-module"
   --     return ()
-      -- stencilsInferTestCrossModuleBasic
+  --     stencilsInferTestCrossModuleBasic
 
 analysisWithTmpFilesTest
   :: FilePath -> [FilePath] -> FilePath
diff --git a/tests/Camfort/ReprintSpec.hs b/tests/Camfort/ReprintSpec.hs
--- a/tests/Camfort/ReprintSpec.hs
+++ b/tests/Camfort/ReprintSpec.hs
@@ -1,18 +1,13 @@
+{-# OPTIONS -Wno-orphans #-}
 {-# LANGUAGE FlexibleInstances #-}
 
 module Camfort.ReprintSpec (spec) where
 
-import Camfort.Functionality
-import Camfort.Reprint
-import Camfort.Specification.Units.Monad (LiteralsOpt(LitMixed))
+import           Camfort.Reprint
 import qualified Data.ByteString.Char8 as B
 import qualified Language.Fortran.Util.Position as FU
-
-import System.FilePath
-
-import Test.Hspec
-import Test.QuickCheck
-
+import           Test.Hspec
+import           Test.QuickCheck
 
 spec :: Spec
 spec =
@@ -99,6 +94,7 @@
       col    <- choose (1, orOne $ length (text !! (line - 1)))
       return $ FU.Position offset col line "<generated>" Nothing
 
+orOne :: (Eq p, Num p) => p -> p
 orOne x | x == 0    = 1
         | otherwise = x
 
@@ -108,13 +104,17 @@
       numLines <- choose (0, 3)
       return . B.pack . concat $ take numLines text
 
+btext :: B.ByteString
 btext = B.pack . unlines $ text
+text :: [[Char]]
 text = ["A B C D"
        ,""
        ,"  E F"
        ," G H I J K L"]
 
+btext2 :: B.ByteString
 btext2 = B.pack . unlines $ text2
+text2 :: [[Char]]
 text2 = ["A B C D"
        ,"E F"
        ,"G H"
diff --git a/tests/Camfort/Specification/DerivedDataTypeSpec.hs b/tests/Camfort/Specification/DerivedDataTypeSpec.hs
--- a/tests/Camfort/Specification/DerivedDataTypeSpec.hs
+++ b/tests/Camfort/Specification/DerivedDataTypeSpec.hs
@@ -1,22 +1,16 @@
 module Camfort.Specification.DerivedDataTypeSpec (spec) where
 
-import System.FilePath ((</>))
-
-import Control.Lens
-
-import Test.Hspec hiding (Spec)
-import qualified Test.Hspec as Test
-
-import qualified Language.Fortran.AST as F
-import Language.Fortran.Util.ModFile (ModFile, emptyModFiles)
-
-import Camfort.Analysis hiding (describe)
-import Camfort.Analysis.ModFile (genModFiles)
-import Camfort.Input (readParseSrcDir)
-import Camfort.Specification.DerivedDataType
-
+import           Camfort.Analysis hiding (describe)
+import           Camfort.Analysis.ModFile (genModFiles)
+import           Camfort.Input (readParseSrcDir)
+import           Camfort.Specification.DerivedDataType
+import           Control.Lens
 import qualified Data.Map.Strict as M
 import qualified Data.Set as S
+import           Language.Fortran.Util.ModFile (ModFile, emptyModFiles)
+import           System.FilePath ((</>))
+import qualified Test.Hspec as Test
+import           Test.Hspec hiding (Spec)
 
 fixturesDir :: String
 fixturesDir = "tests" </> "fixtures" </> "Specification" </> "DerivedDataType"
diff --git a/tests/Camfort/Specification/Hoare/ParserSpec.hs b/tests/Camfort/Specification/Hoare/ParserSpec.hs
--- a/tests/Camfort/Specification/Hoare/ParserSpec.hs
+++ b/tests/Camfort/Specification/Hoare/ParserSpec.hs
@@ -6,7 +6,7 @@
 import           Data.Either                              (isLeft)
 import           Data.Foldable                            (traverse_)
 
-import           Data.Generics.Uniplate.Operations        (Biplate, transformBi)
+import           Data.Generics.Uniplate.Operations        (transformBi)
 
 import           Camfort.Specification.Hoare.Lexer
 import           Camfort.Specification.Hoare.Parser
@@ -59,7 +59,7 @@
         add = bin F.Addition
         sub = bin F.Subtraction
 
-        xA3 = x `add` num 3
+        xA3 = x `add` num (3 :: Int)
         ySz = y `sub` z
         yAz = y `add` z
 
@@ -68,9 +68,9 @@
         (.>) = bin F.GT
         (.>=) = bin F.GTE
 
-        x *&& y = PFLogical (PLAnd x y)
-        x *|| y = PFLogical (PLOr x y)
-        x *-> y = PFLogical (PLImpl x y)
+        x' *&& y' = PFLogical (PLAnd x' y')
+        x' *|| y' = PFLogical (PLOr x' y')
+        x' *-> y' = PFLogical (PLImpl x' y')
 
         tests =
           [ "! static_assert pre(\"x == y\")"
@@ -90,14 +90,14 @@
             .->
             SodSpec (Specification SpecPost
                      (((PFExpr $ xA3 .< ySz) *&& (PFExpr $ xA3 .> yAz)) *||
-                      (PFExpr $ x .>= (num 7))
+                      (PFExpr $ x .>= (num (7::Int)))
                      ))
 
           , "! static_assert seq(\"x + 3 < y - z\" -> \"x + 3 > y + z\" -> \"x >= 7\")"
             .->
             SodSpec (Specification SpecSeq
                      ((PFExpr $ xA3 .< ySz) *->
-                      (((PFExpr $ xA3 .> yAz)) *-> (PFExpr $ x .>= (num 7)))
+                      (((PFExpr $ xA3 .> yAz)) *-> (PFExpr $ x .>= (num (7::Int))))
                      ))
 
           ]
@@ -114,6 +114,7 @@
 matches a b =
   stripSpans a == stripSpans b
 
+defSpan :: F.SrcSpan
 defSpan = F.SrcSpan (F.Position 0 0 0 "" Nothing) (F.Position 0 0 0 "" Nothing)
 
 parse :: String -> Either (Parser.SpecParseError HoareParseError) (SpecOrDecl ())
diff --git a/tests/Camfort/Specification/Stencils/CheckSpec.hs b/tests/Camfort/Specification/Stencils/CheckSpec.hs
--- a/tests/Camfort/Specification/Stencils/CheckSpec.hs
+++ b/tests/Camfort/Specification/Stencils/CheckSpec.hs
@@ -2,10 +2,6 @@
 
 module Camfort.Specification.Stencils.CheckSpec (spec) where
 
-import qualified Data.ByteString.Internal as BS
-
-import Control.Lens
-
 import           Camfort.Analysis hiding (describe)
 import           Camfort.Analysis.Annotations (unitAnnotation)
 import           Camfort.Specification.Parser (runParser)
@@ -13,18 +9,17 @@
 import           Camfort.Specification.Stencils.CheckBackend
 import           Camfort.Specification.Stencils.CheckFrontend
   (CheckResult, stencilChecking)
-import           Camfort.Specification.Stencils.Parser (specParser)
 import           Camfort.Specification.Stencils.Model
+import           Camfort.Specification.Stencils.Parser (specParser)
 import           Camfort.Specification.Stencils.Syntax
-
-import qualified Language.Fortran.Analysis          as FA
-import qualified Language.Fortran.Analysis.BBlocks  as FAB
+import           Control.Lens
+import qualified Data.ByteString.Internal as BS
+import qualified Language.Fortran.Analysis as FA
+import qualified Language.Fortran.Analysis.BBlocks as FAB
 import qualified Language.Fortran.Analysis.Renaming as FAR
 import           Language.Fortran.Parser.Any (fortranParser)
 import           Language.Fortran.Util.ModFile (emptyModFiles)
-import qualified Language.Fortran.Util.Position     as FU
-
-import Test.Hspec
+import           Test.Hspec
 
 parseAndConvert :: String -> Either SynToAstError (Either RegionDecl SpecDecl)
 parseAndConvert x =
diff --git a/tests/Camfort/Specification/Stencils/DenotationalSemanticsSpec.hs b/tests/Camfort/Specification/Stencils/DenotationalSemanticsSpec.hs
--- a/tests/Camfort/Specification/Stencils/DenotationalSemanticsSpec.hs
+++ b/tests/Camfort/Specification/Stencils/DenotationalSemanticsSpec.hs
@@ -1,14 +1,11 @@
 module Camfort.Specification.Stencils.DenotationalSemanticsSpec (spec) where
 
+import           Algebra.Lattice
 import qualified Camfort.Helpers.Vec as V
-
-import Camfort.Specification.Stencils.Model
-import Camfort.Specification.Stencils.Syntax
-import Camfort.Specification.Stencils.DenotationalSemantics
-
-import Algebra.Lattice
-
-import Test.Hspec
+import           Camfort.Specification.Stencils.DenotationalSemantics
+import           Camfort.Specification.Stencils.Model
+import           Camfort.Specification.Stencils.Syntax
+import           Test.Hspec
 
 spec :: Spec
 spec =
@@ -33,7 +30,7 @@
             \/
             return (V.Cons (IntervHoled 0 2 False)
                            (V.Cons (IntervHoled 0 2 False) V.Nil))
-      let spec = Right $ Spatial $
+      let sspec = Right $ Spatial $
             Sum [ Product [ Centered 0 1 True, Forward 1 2 False ]
                 , Product [ Forward 2 1 False, Forward 2 2 False ] ]
-      intervalsToRegions reg `shouldBe` spec
+      intervalsToRegions reg `shouldBe` sspec
diff --git a/tests/Camfort/Specification/StencilsSpec.hs b/tests/Camfort/Specification/StencilsSpec.hs
--- a/tests/Camfort/Specification/StencilsSpec.hs
+++ b/tests/Camfort/Specification/StencilsSpec.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS -Wno-orphans #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -11,49 +12,38 @@
 
 module Camfort.Specification.StencilsSpec (spec) where
 
-
-import           Control.Monad.Writer.Strict hiding (Sum, Product)
+import           Camfort.Analysis hiding (describe)
+import qualified Camfort.Analysis.Logger as L
+import           Camfort.Analysis.ModFile (genModFiles)
+import           Camfort.Analysis.TestUtils
+import           Camfort.Helpers.Vec hiding (zipWith)
+import           Camfort.Input
+import           Camfort.Output
+import           Camfort.Reprint
+import           Camfort.Specification.Stencils
+import           Camfort.Specification.Stencils.Analysis (compileStencils)
+import           Camfort.Specification.Stencils.Generate ( Neighbour(..), indicesToSpec
+                                                         , convIxToNeighbour, runStencilInferer)
+import           Camfort.Specification.Stencils.InferenceBackend
+import           Camfort.Specification.Stencils.Model
+import           Camfort.Specification.Stencils.Syntax
+import           Camfort.Specification.Stencils.Synthesis
+import           Control.Lens
+import qualified Data.ByteString.Char8 as B
+import           Data.Data (Data)
 import qualified Data.Graph.Inductive.Graph as Gr
 import           Data.List
-
-import Control.Lens
-
 import qualified Data.Text as Text
-
-import Language.Fortran.Util.ModFile (emptyModFiles, ModFile)
-
-import Camfort.Analysis.TestUtils
-import Camfort.Analysis hiding (describe)
-import qualified Camfort.Analysis.Logger as L
-import Camfort.Analysis.ModFile (genModFiles)
-import Camfort.Helpers.Vec hiding (zipWith)
-import Camfort.Input
-import Camfort.Specification.Stencils
-import Camfort.Specification.Stencils.Analysis
-  (StencilsAnalysis, compileStencils)
-import Camfort.Specification.Stencils.Generate
-  (Neighbour(..), indicesToSpec, convIxToNeighbour, runStencilInferer)
-import Camfort.Specification.Stencils.Synthesis
-import Camfort.Specification.Stencils.Model
-import Camfort.Specification.Stencils.InferenceFrontend
-import Camfort.Specification.Stencils.InferenceBackend
-import Camfort.Specification.Stencils.Syntax
 import qualified Language.Fortran.AST as F
-import Language.Fortran.Parser.Any (deduceVersion)
-import Language.Fortran.ParserMonad
-import Language.Fortran.Util.ModFile (emptyModFiles)
-import Camfort.Reprint
-import Camfort.Output
-
-import qualified Data.Set as S
-import Data.Functor.Identity
-import qualified Data.ByteString.Char8 as B
-
-import System.Directory (listDirectory)
-import System.FilePath
+import qualified Language.Fortran.Analysis as F
+import           Language.Fortran.Parser.Any (deduceVersion)
+import           Language.Fortran.Util.ModFile (emptyModFiles, ModFile)
+import           System.Directory (listDirectory)
+import           System.FilePath
+import           Test.Hspec
+import           Test.QuickCheck
 
-import Test.Hspec
-import Test.QuickCheck
+type Indices a = [[F.Index (F.Analysis a)]]
 
 spec :: Spec
 spec =
@@ -91,7 +81,7 @@
                 , Cons 1 (Cons 0 (Cons 2 Nil))
                 , Cons 2 (Cons 2 (Cons 3 Nil))
                 , Cons 1 (Cons 3 (Cons 3 Nil))
-                ] :: [Vec (S (S (S Z))) Int])
+                ] :: [Vec ('S ('S ('S 'Z))) Int])
 
     it "composeRegions (1,0)-(1,0) span and (2,0)-(2,0) span" $
       shouldBe (coalesce
@@ -396,9 +386,10 @@
         sampleFiles
 
   where -- Helpers go here for loading files and running analyses
+        assertStencilCheck :: String -> String -> String -> Spec
         assertStencilCheck fileName testComment expected = do
           let input = testInputSources (fixturesDir </> fileName)
-          it "testComment" $
+          it testComment $
             testSingleFileAnalysis input (generalizePureAnalysis . check) $ \report -> do
               let res = report ^?! arResult . _ARSuccess
               show res `shouldBe` expected
@@ -431,14 +422,12 @@
         assertStencilSynthSample = assertStencilSynthDir
           (\d f -> d </> "expected" </> f) samplesDir
 
-        assertStencilSynthResponse fileName testComment expectedResponse =
+        assertStencilSynthResponse fileName testComment expectedResponse = do
           let input = testInputSources (fixturesDir </> fileName)
-              modFiles = emptyModFiles
-          in do
-            it testComment $
-              testMultiFileAnalysis input (generalizePureAnalysis . synth '=') $ \report -> do
-                let logs = report ^.. arMessages . traverse . L._MsgInfo . L.lmMsg
-                logs `shouldBe` expectedResponse
+          it testComment $
+            testMultiFileAnalysis input (generalizePureAnalysis . synth '=') $ \report -> do
+              let logs = report ^.. arMessages . traverse . L._MsgInfo . L.lmMsg
+              logs `shouldBe` expectedResponse
 
         assertStencilSynthResponseOut fileName testComment expectedResponse =
           describe testComment $ do
@@ -446,7 +435,6 @@
             assertStencilSynthResponse fileName "correct output" expectedResponse
 
         assertStencilSynthNoWarn fileName testComment = assertStencilSynthResponseOut fileName testComment [""]
-        fixturesDir = "tests" </> "fixtures" </> "Specification" </> "Stencils"
         samplesDir  = "samples" </> "stencils"
         getExpectedSrcFileName file =
           let oldExtension = takeExtension file
@@ -478,36 +466,41 @@
   ]
 
 -- Indices for the 2D five point stencil (deliberately in an odd order)
+fivepoint :: [Vec ('S ('S 'Z)) Int]
 fivepoint = [ Cons (-1) (Cons 0 Nil), Cons 0 (Cons (-1) Nil)
             , Cons 1 (Cons 0 Nil) , Cons 0 (Cons 1 Nil), Cons 0 (Cons 0 Nil)
             ]
 -- Indices for the 3D seven point stencil
+sevenpoint :: [Vec ('S ('S ('S 'Z))) Int]
 sevenpoint = [ Cons (-1) (Cons 0 (Cons 0 Nil)), Cons 0 (Cons (-1) (Cons 0 Nil))
              , Cons 0 (Cons 0 (Cons 1 Nil)), Cons 0 (Cons 1 (Cons 0 Nil))
              , Cons 1 (Cons 0 (Cons 0 Nil)), Cons 0 (Cons 0 (Cons (-1) Nil))
              , Cons 0 (Cons 0 (Cons 0 Nil))
              ]
+centeredFwd :: [Vec ('S ('S 'Z)) Int]
 centeredFwd = [ Cons 1 (Cons 0 Nil), Cons 0 (Cons 1 Nil), Cons 0 (Cons (-1) Nil)
               , Cons 1 (Cons 1 Nil), Cons 0 (Cons 0 Nil), Cons 1 (Cons (-1) Nil)
-              ] :: [ Vec (S (S Z)) Int ]
+              ] :: [ Vec ('S ('S 'Z)) Int ]
 
 -- Examples of unusal patterns
+fivepointErr :: [Vec ('S ('S 'Z)) Int]
 fivepointErr = [ Cons (-1) (Cons 0 Nil)
                , Cons 0 (Cons (-1) Nil)
                , Cons 1 (Cons 0 Nil)
                , Cons 0 (Cons 1 Nil)
                , Cons 0 (Cons 0 Nil)
-               , Cons 1 (Cons 1 Nil) ] :: [ Vec (S (S Z)) Int ]
+               , Cons 1 (Cons 1 Nil) ] :: [ Vec ('S ('S 'Z)) Int ]
 
 {- Construct arbtirary vectors and test up to certain sizes -}
-instance {-# OVERLAPPING #-} Arbitrary a => Arbitrary (Vec Z a) where
+instance {-# OVERLAPPING #-} Arbitrary a => Arbitrary (Vec 'Z a) where
     arbitrary = return Nil
 
-instance (Arbitrary (Vec n a), Arbitrary a) => Arbitrary (Vec (S n) a) where
+instance (Arbitrary (Vec n a), Arbitrary a) => Arbitrary (Vec ('S n) a) where
     arbitrary = do x  <- arbitrary
                    xs <- arbitrary
                    return $ Cons x xs
 
+test2DSpecVariation :: Neighbour -> Neighbour -> ([[Int]], Multiplicity (Approximation Spatial)) -> SpecWith ()
 test2DSpecVariation a b (input, expectation) =
     it ("format=" ++ show input) $ do
       -- Test inference
@@ -516,13 +509,16 @@
   where
     expectedSpec = Specification expectation True
     fromFormatToIx [ri,rj] = [ offsetToIx "i" ri, offsetToIx "j" rj ]
+    fromFormatToIx _       = error "test2DSpecVariation: fromFormatToIx"
 
+indicesToSpec' :: Data ann => [Variable] -> [Neighbour] -> Indices ann -> Maybe Specification
 indicesToSpec' ivs lhs ixs =
   let inferer = indicesToSpec "a" lhs ixs
       analysis = runStencilInferer inferer ivs Gr.empty
       report = runIdentity $ runAnalysisT "example" (logOutputNone True) LogError emptyModFiles analysis
   in report ^?! arResult . _ARSuccess . _1
 
+variations :: [([[Int]], Multiplicity (Approximation Spatial))]
 variations =
   [ ( [ [0,0] ]
     , Once $ Exact $ Spatial (Sum [Product [ Centered 0 1 True, Centered 0 2 True]])
@@ -559,6 +555,7 @@
     )
   ]
 
+variationsRel :: [(Neighbour, Neighbour, [[Int]], Multiplicity (Approximation Spatial))]
 variationsRel =
   [   -- Stencil which has non-relative indices in one dimension
     (Neighbour "i" 0, Constant (F.ValInteger "0"), [ [0, absoluteRep], [1, absoluteRep] ]
@@ -590,6 +587,7 @@
     )
   ]
 
+test3DSpecVariation :: ([[Int]], Multiplicity (Approximation Spatial)) -> SpecWith ()
 test3DSpecVariation (input, expectation) =
     it ("format=" ++ show input) $
       -- Test inference
@@ -600,10 +598,11 @@
 
   where
     expectedSpec = Specification expectation True
-    fromFormatToIx [ri,rj,rk] =
-      [offsetToIx "i" ri, offsetToIx "j" rj, offsetToIx "k" rk]
+    fromFormatToIx [ri,rj,rk] = [offsetToIx "i" ri, offsetToIx "j" rj, offsetToIx "k" rk]
+    fromFormatToIx _          = error "test3DSpecVariation: fromFormatToIx"
 
 
+variations3D :: [([[Int]], Multiplicity (Approximation Spatial))]
 variations3D =
   [ ( [ [-1,0,-1], [0,0,-1], [-1,0,0], [0,0,0] ]
     ,  Once $ Exact $ Spatial (Sum [Product [Backward 1 1 True, Centered 0 2 True, Backward 1 3 True]])
@@ -620,6 +619,7 @@
 prop_extract_synth_inverse v o =
      convIxToNeighbour [v] (offsetToIx v o) == Neighbour v o
 
+unlines' :: [L.Text] -> L.Text
 unlines' = Text.init . Text.unlines
 
 -- Local variables:
diff --git a/tests/Camfort/Specification/Units/Analysis/ConsistentSpec.hs b/tests/Camfort/Specification/Units/Analysis/ConsistentSpec.hs
--- a/tests/Camfort/Specification/Units/Analysis/ConsistentSpec.hs
+++ b/tests/Camfort/Specification/Units/Analysis/ConsistentSpec.hs
@@ -1,22 +1,17 @@
 -- TODO: Fix this
 module Camfort.Specification.Units.Analysis.ConsistentSpec (spec) where
 
-import System.FilePath ((</>))
-
-import Control.Lens
-
-import Test.Hspec hiding (Spec)
+import           Camfort.Analysis hiding (describe)
+import           Camfort.Analysis.ModFile (genModFiles)
+import           Camfort.Input (readParseSrcDir)
+import           Camfort.Specification.Units.Analysis (compileUnits)
+import           Camfort.Specification.Units.Analysis.Consistent (checkUnits)
+import           Camfort.Specification.Units.Monad (LiteralsOpt(..), unitOpts0, uoLiterals, runUnitAnalysis, UnitEnv(..))
+import           Control.Lens
+import           Language.Fortran.Util.ModFile (ModFile, emptyModFiles)
+import           System.FilePath ((</>))
 import qualified Test.Hspec as Test
-
-import Language.Fortran.Util.ModFile (ModFile, emptyModFiles)
-
-import Camfort.Analysis hiding (describe)
-import Camfort.Analysis.ModFile (genModFiles)
-import Camfort.Input (readParseSrcDir)
-import Camfort.Specification.Units.Analysis (compileUnits)
-import Camfort.Specification.Units.Analysis.Consistent (checkUnits)
-import Camfort.Specification.Units.Monad
-  (LiteralsOpt(..), unitOpts0, uoLiterals, runUnitAnalysis, UnitEnv(..))
+import           Test.Hspec hiding (Spec)
 
 spec :: Test.Spec
 spec =
@@ -139,12 +134,12 @@
   \ - at 7:3: 'result of sqr' should have unit 's'\n\
   \ - at 7:11: 'parameter 1 to sqr' should have unit 's'\n"
 
-literalNonZeroInconsist4Report :: String -- fixme
-literalNonZeroInconsist4Report =
-  "\ntests/fixtures/Specification/Units/literal-nonzero-inconsist5.f90: Inconsistent:\n\
-  \- at 7:11: 'parameter 1 to sqr' should have unit 's'\n\
-  \- at 15:9: 'i' should have the same units as 'parameter 1 to sqr'\n\
-  \- at 17:12: 'i' should have unit '1'\n"
+-- literalNonZeroInconsist4Report :: String -- fixme
+-- literalNonZeroInconsist4Report =
+--   "\ntests/fixtures/Specification/Units/literal-nonzero-inconsist5.f90: Inconsistent:\n\
+--   \- at 7:11: 'parameter 1 to sqr' should have unit 's'\n\
+--   \- at 15:9: 'i' should have the same units as 'parameter 1 to sqr'\n\
+--   \- at 17:12: 'i' should have unit '1'\n"
 
 literalNonZeroInconsist5Report :: String
 literalNonZeroInconsist5Report =
diff --git a/tests/Camfort/Specification/Units/Analysis/CriticalsSpec.hs b/tests/Camfort/Specification/Units/Analysis/CriticalsSpec.hs
--- a/tests/Camfort/Specification/Units/Analysis/CriticalsSpec.hs
+++ b/tests/Camfort/Specification/Units/Analysis/CriticalsSpec.hs
@@ -1,20 +1,14 @@
 module Camfort.Specification.Units.Analysis.CriticalsSpec (spec) where
 
-import System.Directory (getCurrentDirectory)
-import System.FilePath ((</>))
-
-import Control.Lens
-
-import Test.Hspec hiding (Spec)
+import           Camfort.Analysis hiding (describe)
+import           Camfort.Analysis.ModFile (readParseSrcDir)
+import           Camfort.Specification.Units.Analysis.Criticals (inferCriticalVariables)
+import           Camfort.Specification.Units.Monad (LiteralsOpt(..), unitOpts0, uoLiterals, UnitEnv(..), runUnitAnalysis)
+import           Control.Lens
+import           Language.Fortran.Util.ModFile (emptyModFiles)
+import           System.FilePath ((</>))
 import qualified Test.Hspec as Test
-
-import Language.Fortran.Util.ModFile (emptyModFiles)
-
-import Camfort.Analysis hiding (describe)
-import Camfort.Analysis.ModFile (readParseSrcDir)
-import Camfort.Specification.Units.Analysis.Criticals (inferCriticalVariables)
-import Camfort.Specification.Units.Monad
-  (LiteralsOpt(..), unitOpts0, uoLiterals, UnitEnv(..), runUnitAnalysis)
+import           Test.Hspec hiding (Spec)
 
 spec :: Test.Spec
 spec = do
diff --git a/tests/Camfort/Specification/Units/InferenceBackendSpec.hs b/tests/Camfort/Specification/Units/InferenceBackendSpec.hs
--- a/tests/Camfort/Specification/Units/InferenceBackendSpec.hs
+++ b/tests/Camfort/Specification/Units/InferenceBackendSpec.hs
@@ -1,16 +1,15 @@
 module Camfort.Specification.Units.InferenceBackendSpec (spec) where
 
-import GHC.Real ((%))
-
-import           Test.Hspec hiding (Spec)
+import           Camfort.Specification.Units.BackendTypes (constraintToDim, dimParamEq, dimFromList, prop_composition)
+import           Camfort.Specification.Units.Environment
+import           Camfort.Specification.Units.InferenceBackend ( flattenConstraints, shiftTerms )
+import           Camfort.Specification.Units.InferenceBackendSBV ( criticalVariables
+                                                                 , inconsistentConstraints, inferVariables )
+import           Data.Maybe (fromJust)
+import           GHC.Real ((%))
 import qualified Test.Hspec as Test
-
-import Camfort.Specification.Units.Environment
-import Camfort.Specification.Units.InferenceBackendSBV ( criticalVariables, inconsistentConstraints, inferVariables )
-import Camfort.Specification.Units.InferenceBackend ( flattenConstraints, shiftTerms )
-import Camfort.Specification.Units.BackendTypes (constraintToDim, dimParamEq, Dim, dimFromList, prop_composition)
-import Data.Maybe (fromJust)
-import Test.QuickCheck
+import           Test.Hspec hiding (Spec)
+import           Test.QuickCheck
 
 spec :: Test.Spec
 spec = do
@@ -56,20 +55,24 @@
     name <- arbitrary
     return $ UnitVar (name, name)
 
+testCons1 :: [Constraint]
 testCons1 = [ ConEq (UnitName "kg") (UnitName "m")
             , ConEq (UnitVar ("x", "x")) (UnitName "m")
             , ConEq (UnitVar ("y", "y")) (UnitName "kg")]
 
+testCons1_flattened :: [([UnitInfo], [UnitInfo])]
 testCons1_flattened = [([UnitPow (UnitName "kg") 1.0],[UnitPow (UnitName "m") 1.0])
                       ,([UnitPow (UnitVar ("x", "x")) 1.0],[UnitPow (UnitName "m") 1.0])
                       ,([UnitPow (UnitVar ("y", "y")) 1.0],[UnitPow (UnitName "kg") 1.0])]
 
+testCons1_shifted :: [([UnitInfo], [UnitInfo])]
 testCons1_shifted = [([],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "kg") (-1.0)])
                     ,([UnitPow (UnitVar ("x", "x")) 1.0],[UnitPow (UnitName "m") 1.0])
                     ,([UnitPow (UnitVar ("y", "y")) 1.0],[UnitPow (UnitName "kg") 1.0])]
 
 --------------------------------------------------
 
+testCons2 :: [Constraint]
 testCons2 = [ConEq (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-1.0))) (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-1.0)))
             ,ConEq (UnitName "m") (UnitMul (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-1.0))) (UnitName "s"))
             ,ConEq (UnitAlias "accel") (UnitMul (UnitName "m") (UnitPow (UnitParamPosUse (("simple1_sqr6", "sqr"),0,0)) (-1.0)))
@@ -85,6 +88,7 @@
             ,ConEq (UnitParamPosUse (("simple1_mul7","mul"),0,1)) (UnitMul (UnitParamPosUse (("simple1_mul7","mul"),1,1)) (UnitParamPosUse (("simple1_mul7","mul"),2,1)))
             ,ConEq (UnitAlias "accel") (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-2.0)))]
 
+testCons2_shifted :: [([UnitInfo], [UnitInfo])]
 testCons2_shifted = [([],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "s") (-1.0),UnitPow (UnitName "m") (-1.0),UnitPow (UnitName "s") 1.0])
                     ,([],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "m") (-1.0)])
                     ,([UnitPow (UnitAlias "accel") 1.0,UnitPow (UnitParamPosUse (("simple1_sqr6","sqr"),0,0)) 1.0],[UnitPow (UnitName "m") 1.0])
@@ -100,20 +104,24 @@
                     ,([UnitPow (UnitParamPosUse (("simple1_mul7","mul"),0,1)) 1.0,UnitPow (UnitParamPosUse (("simple1_mul7","mul"),1,1)) (-1.0),UnitPow (UnitParamPosUse (("simple1_mul7","mul"),2,1)) (-1.0)],[])
                     ,([UnitPow (UnitAlias "accel") 1.0],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "s") (-2.0)])]
 
+testCons3 :: [Constraint]
 testCons3 = [ ConEq (UnitVar ("a", "a")) (UnitVar ("e", "e"))
             , ConEq (UnitVar ("a", "a")) (UnitMul (UnitVar ("b", "b")) (UnitMul (UnitVar ("c", "c")) (UnitVar ("d", "d"))))
             , ConEq (UnitVar ("d", "d")) (UnitName "m") ]
 
+testCons3_shifted :: [([UnitInfo], [UnitInfo])]
 testCons3_shifted = [([UnitPow (UnitVar ("a", "a")) 1.0,UnitPow (UnitVar ("e", "e")) (-1.0)],[])
                     ,([UnitPow (UnitVar ("a", "a")) 1.0,UnitPow (UnitVar ("b", "b")) (-1.0),UnitPow (UnitVar ("c", "c")) (-1.0),UnitPow (UnitVar ("d", "d")) (-1.0)],[])
                     ,([UnitPow (UnitVar ("d", "d")) 1.0],[UnitPow (UnitName "m") 1.0])]
 
+testCons4 :: [Constraint]
 testCons4 = [ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitParamPosUse (("simple2_sqr3","sqr"),0,0))
             ,ConEq (UnitVar ("simple2_a22", "simple2_a22")) (UnitParamPosUse (("simple2_sqr3","sqr"),1,0))
             -- ,ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitVar ("simple2_a11", "simple2_a11"))
             -- ,ConEq (UnitVar ("simple2_a22", "simple2_a22")) (UnitVar ("simple2_a22", "simple2_a22"))
             ,ConEq (UnitParamPosUse (("simple2_sqr3","sqr"),0,0)) (UnitMul (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)) (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)))]
 
+testCons5 :: [Constraint]
 testCons5 = [ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitParamPosUse (("simple2_sqr3","sqr"),0,0))
             ,ConEq (UnitAlias "accel") (UnitParamPosUse (("simple2_sqr3","sqr"),1,0))
             ,ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitVar ("simple2_a11", "simple2_a11"))
@@ -121,6 +129,7 @@
             ,ConEq (UnitParamPosUse (("simple2_sqr3","sqr"),0,0)) (UnitMul (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)) (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)))
             ,ConEq (UnitAlias "accel") (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-2.0)))]
 
+testCons5_infer :: [(([Char], [Char]), UnitInfo)]
 testCons5_infer = [(("simple2_a11", "simple2_a11"),UnitMul (UnitPow (UnitName "m") 2.0) (UnitPow (UnitName "s") (-4.0)))
                   ,(("simple2_a22", "simple2_a22"),UnitMul (UnitPow (UnitName "m") 1.0) (UnitPow (UnitName "s") (-2.0)))]
 
diff --git a/tests/Camfort/Transformation/CommonSpec.hs b/tests/Camfort/Transformation/CommonSpec.hs
--- a/tests/Camfort/Transformation/CommonSpec.hs
+++ b/tests/Camfort/Transformation/CommonSpec.hs
@@ -2,22 +2,19 @@
 
 import           System.Directory
 import           System.FilePath
-
 import           Test.Hspec
-
 import           Camfort.Analysis.Logger (LogLevel (..))
 import           Camfort.Functionality
 
 samplesBase :: FilePath
 samplesBase = "tests" </> "fixtures" </> "Transformation"
 
-data Example = Example FilePath FilePath
-
 readSample :: FilePath -> IO String
 readSample filename = do
   let path = samplesBase </> filename
   readFile path
 
+removeSample :: [Char] -> IO ()
 removeSample filename = do
   let path = samplesBase </> filename
   removeFile path
@@ -41,7 +38,7 @@
             , ceFortranVersion = Nothing
             }
 
-      runIO $ common outFile env
+      _ <- runIO $ common outFile env
 
       actual    <- runIO $ readSample "common.f90.out"
       actualMod <- runIO $ readSample "cmn.f90"
diff --git a/tests/Camfort/Transformation/EquivalenceElimSpec.hs b/tests/Camfort/Transformation/EquivalenceElimSpec.hs
--- a/tests/Camfort/Transformation/EquivalenceElimSpec.hs
+++ b/tests/Camfort/Transformation/EquivalenceElimSpec.hs
@@ -19,27 +19,17 @@
 
 module Camfort.Transformation.EquivalenceElimSpec (spec) where
 
-import           Control.Arrow                          (second)
-import           Control.Monad                          (forM_)
-import           System.Directory
-import           System.FilePath
-import           System.IO.Silently                     (capture_)
-
-import           Control.Lens
-
-import           Test.Hspec
-
-import qualified Language.Fortran.Util.Position         as FU
-
-import           Camfort.Analysis                       hiding (describe)
-import           Camfort.Analysis.Logger                hiding (describe)
-import           Camfort.Analysis.ModFile               (MFCompiler,
-                                                         genModFiles,
-                                                         simpleCompiler)
+import           Camfort.Analysis hiding (describe)
+import           Camfort.Analysis.Logger hiding (describe)
 import           Camfort.Analysis.TestUtils
 import           Camfort.Functionality
-import           Camfort.Input
 import           Camfort.Transformation.EquivalenceElim
+import           Control.Lens
+import           Control.Monad (forM_)
+import qualified Language.Fortran.Util.Position as FU
+import           System.Directory
+import           System.FilePath
+import           Test.Hspec
 
 samplesBase :: FilePath
 samplesBase = "tests" </> "fixtures" </> "Transformation"
@@ -63,7 +53,7 @@
         , ceFortranVersion = Nothing
         }
 
-  equivalences outFile env
+  _ <- equivalences outFile env
   actual <- readFile outFile
   removeFile outFile
   return actual
diff --git a/tests/fixtures/Specification/Units/complexity0.f90 b/tests/fixtures/Specification/Units/complexity0.f90
new file mode 100644
--- /dev/null
+++ b/tests/fixtures/Specification/Units/complexity0.f90
@@ -0,0 +1,7 @@
+module complexity
+contains
+  real function g(x, y)
+    real :: x, y, z
+    g = (x*x*x*x*x*x + y*y*y*y)
+  end function g
+end module complexity
diff --git a/tests/fixtures/Specification/Units/literal-prop.f90 b/tests/fixtures/Specification/Units/literal-prop.f90
new file mode 100644
--- /dev/null
+++ b/tests/fixtures/Specification/Units/literal-prop.f90
@@ -0,0 +1,20 @@
+module foo
+real, parameter :: one = 1.0
+contains
+  function f(x)
+    real :: x
+    f = x + one
+  end function f
+
+  subroutine s()
+    !- = unit C/K :: k2c
+    !- = unit C :: zeroc
+    real, parameter :: zeroc = 273.0, k2c
+    !- = unit c :: tc_1_in
+    !- = unit k :: t
+    real :: tc_1_in, t
+
+    tc_1_in = (k2c*t - zeroc)
+  end subroutine s
+  
+end module foo