diff --git a/ghc-api-tests/GhcApiTests.hs b/ghc-api-tests/GhcApiTests.hs
--- a/ghc-api-tests/GhcApiTests.hs
+++ b/ghc-api-tests/GhcApiTests.hs
@@ -7,6 +7,8 @@
     , Expr(..)
     , Alt(..)
     , AltCon(..)
+    , LitNumType(..)
+    , Literal(..)
     , apiCommentsParsedSource
     , occNameString
     , pAT_ERROR_ID
@@ -17,15 +19,20 @@
 import           Test.Tasty.Runners.AntXML
 
 import qualified GHC as GHC
+import qualified GHC.Builtin.Names as GHC
+import qualified GHC.Builtin.Types as GHC
 import qualified GHC.Core as GHC
 import qualified GHC.Data.EnumSet as EnumSet
 import qualified GHC.Data.FastString as GHC
 import qualified GHC.Data.StringBuffer as GHC
 import qualified GHC.Parser as Parser
 import qualified GHC.Parser.Lexer as GHC
-import qualified GHC.Types.Name.Occurrence as GHC
+import qualified GHC.Types.Id as GHC
+import qualified GHC.Types.Name as GHC
 import qualified GHC.Types.SrcLoc as GHC
 import qualified GHC.Unit.Module.ModGuts as GHC
+import qualified GHC.Utils.Error as GHC
+import qualified GHC.Utils.Outputable as GHC
 
 import GHC.Paths (libdir)
 
@@ -39,6 +46,7 @@
     testGroup "GHC API"
       [ testCase "apiComments" testApiComments
       , testCase "caseDesugaring" testCaseDesugaring
+      , testCase "numericLiteralDesugaring" testNumLitDesugaring
       ]
 
 -- Tests that Liquid.GHC.API.Extra.apiComments can retrieve the comments in
@@ -78,13 +86,22 @@
     parseMod str filepath = do
       let location = GHC.mkRealSrcLoc (GHC.mkFastString filepath) 1 1
           buffer = GHC.stringToStringBuffer str
-          popts = GHC.mkParserOpts EnumSet.empty EnumSet.empty False True True True
+          popts = GHC.mkParserOpts EnumSet.empty diagOpts [] False True True True
           parseState = GHC.initParserState popts buffer location
       case GHC.unP Parser.parseModule parseState of
         GHC.POk _ result -> return result
         _ -> fail "Unexpected parser error"
 
+    diagOpts = GHC.DiagOpts
+      { GHC.diag_warning_flags = EnumSet.empty
+      , GHC.diag_fatal_warning_flags = EnumSet.empty
+      , GHC.diag_warn_is_error = True
+      , GHC.diag_reverse_errors = False
+      , GHC.diag_max_errors = Nothing
+      , GHC.diag_ppr_ctx = GHC.defaultSDocContext
+      }
 
+
 -- | Tests that case expressions desugar as Liquid Haskell expects.
 testCaseDesugaring :: IO ()
 testCaseDesugaring = do
@@ -121,26 +138,61 @@
             -> e3 == pAT_ERROR_ID
           _ -> False
 
-    coreProgram <- compileToCore inputSource
+    coreProgram <- compileToCore "CaseDesugaring" inputSource
     unless (isExpectedDesugaring coreProgram) $
       fail $ unlines $
         "Unexpected desugaring:" : map showPprQualified coreProgram
-  where
-    compileToCore inputSource = do
-      now <- getCurrentTime
-      GHC.runGhc (Just libdir) $ do
-        df1 <- GHC.getSessionDynFlags
-        GHC.setSessionDynFlags df1
-        let target = GHC.Target {
-                     GHC.targetId           = GHC.TargetFile "CaseDesugaring.hs" Nothing
-                   , GHC.targetAllowObjCode = False
-                   , GHC.targetContents     = Just (GHC.stringToStringBuffer inputSource, now)
-                   }
-        GHC.setTargets [target]
-        void $ GHC.load GHC.LoadAllTargets
 
-        dsMod <- GHC.getModSummary (GHC.mkModuleName "CaseDesugaring")
-               >>= GHC.parseModule
-               >>= GHC.typecheckModule
-               >>= GHC.desugarModule
-        return $ GHC.mg_binds $ GHC.dm_core_module dsMod
+-- | Tests that numeric literal expressions desugar as Liquid Haskell expects.
+testNumLitDesugaring :: IO ()
+testNumLitDesugaring = do
+    let inputSource = unlines
+          [ "module NumLitDesugaring where"
+          , "f :: Num a => a"
+          , "f = 1"
+          ]
+
+        fBind (GHC.NonRec b _e) =
+          occNameString (GHC.occName b) == "f"
+        fBind _ = False
+
+        -- Expected desugaring:
+        --
+        -- NumLitDesugaring.f
+        --      = \@a dict -> fromInteger @a dict (GHC.Num.Integer.IS 1#)
+        --
+        isExpectedDesugaring p = case find fBind p of
+          Just (GHC.NonRec _ e0)
+            | Lam _a (Lam _dict (App fromIntegerApp (App (Var vIS) lit))) <- e0
+            , App (App (Var vFromInteger) _aty) _numDict <- fromIntegerApp
+            , GHC.idName vFromInteger  == GHC.fromIntegerName
+            , GHC.nameStableString (GHC.idName vIS) == GHC.nameStableString GHC.integerISDataConName
+            , Lit (LitNumber LitNumInt 1) <- lit
+            -> True
+          _ -> False
+
+    coreProgram <- compileToCore "NumLitDesugaring" inputSource
+    unless (isExpectedDesugaring coreProgram) $
+      fail $ unlines $
+        "Unexpected desugaring:" : map showPprQualified coreProgram
+
+compileToCore :: String -> String -> IO [GHC.CoreBind]
+compileToCore modName inputSource = do
+    now <- getCurrentTime
+    GHC.runGhc (Just libdir) $ do
+      df1 <- GHC.getSessionDynFlags
+      GHC.setSessionDynFlags df1
+      let target = GHC.Target {
+                   GHC.targetId           = GHC.TargetFile (modName ++ ".hs") Nothing
+                 , GHC.targetUnitId       = GHC.homeUnitId_ df1
+                 , GHC.targetAllowObjCode = False
+                 , GHC.targetContents     = Just (GHC.stringToStringBuffer inputSource, now)
+                 }
+      GHC.setTargets [target]
+      void $ GHC.load GHC.LoadAllTargets
+
+      dsMod <- GHC.getModSummary (GHC.mkModuleName modName)
+             >>= GHC.parseModule
+             >>= GHC.typecheckModule
+             >>= GHC.desugarModule
+      return $ GHC.mg_binds $ GHC.dm_core_module dsMod
diff --git a/liquidhaskell-boot.cabal b/liquidhaskell-boot.cabal
--- a/liquidhaskell-boot.cabal
+++ b/liquidhaskell-boot.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               liquidhaskell-boot
-version:            0.9.2.8.0
+version:            0.9.4.7.0
 synopsis:           Liquid Types for Haskell
 description:        This package provides a plugin to verify Haskell programs.
                     But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell)
@@ -13,7 +13,7 @@
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
 build-type:         Simple
-tested-with:        GHC == 9.2.8
+tested-with:        GHC == 9.4.7
 
 data-files:         include/CoreToLogic.lg
                     syntax/liquid.css
@@ -126,7 +126,7 @@
                     , aeson
                     , binary
                     , bytestring           >= 0.10
-                    , Cabal                < 3.7
+                    , Cabal                < 3.9
                     , cereal
                     , cmdargs              >= 0.10
                     , containers           >= 0.5
@@ -136,14 +136,14 @@
                     , filepath             >= 1.3
                     , fingertree           >= 0.1
                     , exceptions           < 0.11
-                    , ghc                  ^>= 9.2
+                    , ghc                  ^>= 9.4
                     , ghc-boot
                     , ghc-paths            >= 0.1
                     , ghc-prim
                     , gitrev
                     , hashable             >= 1.3 && < 1.5
                     , hscolour             >= 1.22
-                    , liquid-fixpoint      == 0.9.2.5
+                    , liquid-fixpoint      == 0.9.4.7
                     , mtl                  >= 2.1
                     , optparse-applicative < 0.18
                     , githash
diff --git a/src-ghc/Liquid/GHC/API.hs b/src-ghc/Liquid/GHC/API.hs
--- a/src-ghc/Liquid/GHC/API.hs
+++ b/src-ghc/Liquid/GHC/API.hs
@@ -59,7 +59,6 @@
     , LexicalFixity(Prefix)
     , Located
     , LocatedN
-    , Logger
     , ModIface_(mi_anns, mi_exports, mi_globals, mi_module)
     , ModLocation(ml_hs_file)
     , ModSummary(ms_hspp_file, ms_hspp_opts, ms_location, ms_mod)
@@ -319,7 +318,9 @@
     , pAT_ERROR_ID
     )
 import GHC.Core.Predicate             as Ghc (getClassPredTys_maybe, getClassPredTys, isEvVarType, isEqPrimPred, isEqPred, isClassPred, isDictId, mkClassPred)
-import GHC.Core.Subst                 as Ghc (deShadowBinds, emptySubst, extendCvSubst)
+import GHC.Core.Reduction             as Ghc
+    ( Reduction(Reduction) )
+import GHC.Core.Subst                 as Ghc (emptySubst, extendCvSubst)
 import GHC.Core.TyCo.Rep              as Ghc
     ( AnonArgFlag(VisArg)
     , ArgFlag(Required)
@@ -370,7 +371,7 @@
     , isPromotedDataCon
     , isTupleTyCon
     , isVanillaAlgTyCon
-    , mkKindTyCon
+    , mkPrimTyCon
     , newTyConRhs
     , tyConBinders
     , tyConDataCons_maybe
@@ -420,12 +421,14 @@
     , fsLit
     , mkFastString
     , mkFastStringByteString
-    , sLit
+    , mkPtrString
     , uniq
     , unpackFS
     )
 import GHC.Data.Pair                  as Ghc
     ( Pair(Pair) )
+import GHC.Driver.Config.Diagnostic as Ghc
+    ( initDiagOpts )
 import GHC.Driver.Main                as Ghc
     ( hscDesugar
     , hscTcRcLookupName
@@ -433,8 +436,7 @@
 import GHC.Driver.Phases              as Ghc (Phase(StopLn))
 import GHC.Driver.Pipeline            as Ghc (compileFile)
 import GHC.Driver.Session             as Ghc
-    ( WarnReason(NoReason)
-    , getDynFlags
+    ( getDynFlags
     , gopt_set
     , updOptLevel
     , xopt_set
@@ -448,6 +450,7 @@
                                              , fromSerialized
                                              , toSerialized
                                              , defaultPlugin
+                                             , emptyPlugins
                                              , Plugin(..)
                                              , CommandLineOption
                                              , purePlugin
@@ -458,11 +461,12 @@
 import GHC.Core.Opt.OccurAnal         as Ghc
     ( occurAnalysePgm )
 import GHC.Driver.Env                 as Ghc
-    ( HscEnv(hsc_EPS, hsc_HPT, hsc_dflags, hsc_plugins, hsc_static_plugins) )
+    ( HscEnv(hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins) )
+import GHC.Driver.Errors              as Ghc
+    ( printMessages )
 import GHC.Driver.Ppr                 as Ghc
     ( showPpr
     , showSDoc
-    , showSDocDump
     )
 import GHC.HsToCore.Expr              as Ghc
     ( dsLExpr )
@@ -471,13 +475,14 @@
     , loadInterface
     )
 import GHC.Rename.Expr                as Ghc (rnLExpr)
+import GHC.Rename.Names               as Ghc (renamePkgQual)
+import GHC.Tc.Errors.Types            as Ghc
+    ( TcRnMessage(TcRnUnknownMessage) )
 import GHC.Tc.Gen.App                 as Ghc (tcInferSigma)
 import GHC.Tc.Gen.Bind                as Ghc (tcValBinds)
 import GHC.Tc.Gen.Expr                as Ghc (tcInferRho)
 import GHC.Tc.Module                  as Ghc
-    ( getModuleInterface
-    , tcRnLookupRdrName
-    )
+    ( getModuleInterface )
 import GHC.Tc.Solver                  as Ghc
     ( InferMode(NoRestrictions)
     , captureTopConstraints
@@ -503,14 +508,17 @@
     , failWithTc
     , initIfaceTcRn
     , liftIO
-    , mkLongErrAt
+    , addErrAt
+    , addErrs
     , pushTcLevelM
-    , reportError
-    , reportErrors
+    , reportDiagnostic
+    , reportDiagnostics
     )
 import GHC.Tc.Utils.TcType            as Ghc (tcSplitDFunTy, tcSplitMethodTy)
 import GHC.Tc.Utils.Zonk              as Ghc
     ( zonkTopLExpr )
+import GHC.Types.PkgQual              as Ghc
+    ( PkgQual(NoPkgQual) )
 import GHC.Types.Annotations          as Ghc
     ( AnnPayload
     , AnnTarget(ModuleTarget)
@@ -539,9 +547,12 @@
     ( CostCentre(cc_loc)
     )
 import GHC.Types.Error                as Ghc
-    ( Messages
-    , DecoratedSDoc
+    ( Messages(getMessages)
+    , MessageClass(MCDiagnostic)
+    , DiagnosticReason(WarningWithoutFlag)
     , MsgEnvelope(errMsgSpan)
+    , errorsOrFatalWarningsFound
+    , mkPlainError
     )
 import GHC.Types.Fixity               as Ghc
     ( Fixity(Fixity) )
@@ -560,7 +571,7 @@
 import GHC.Types.Id.Info              as Ghc
     ( CafInfo(NoCafRefs)
     , IdDetails(DataConWorkId, DataConWrapId, RecSelId, VanillaId)
-    , IdInfo(occInfo, unfoldingInfo)
+    , IdInfo(occInfo, realUnfoldingInfo)
     , cafInfo
     , inlinePragInfo
     , mayHaveCafRefs
@@ -660,8 +671,11 @@
     , extendVarSetList
     , unitVarSet
     )
+import GHC.Unit.Env                   as Ghc
+    ( UnitEnv(ue_eps), ue_hpt )
 import GHC.Unit.External              as Ghc
     ( ExternalPackageState (eps_ann_env)
+    , ExternalUnitCache(euc_eps)
     )
 import GHC.Unit.Finder                as Ghc
     ( FindResult(Found, NoPackage, FoundMultiple, NotFound)
@@ -693,7 +707,7 @@
       , mg_usages
       )
     )
-import GHC.Utils.Error                as Ghc (withTiming)
-import GHC.Utils.Logger               as Ghc (putLogMsg)
+import GHC.Utils.Error                as Ghc (pprLocMsgEnvelope, withTiming)
+import GHC.Utils.Logger               as Ghc (Logger(logFlags), putLogMsg)
 import GHC.Utils.Outputable           as Ghc hiding ((<>))
 import GHC.Utils.Panic                as Ghc (panic, throwGhcException, throwGhcExceptionIO)
diff --git a/src-ghc/Liquid/GHC/API/Extra.hs b/src-ghc/Liquid/GHC/API/Extra.hs
--- a/src-ghc/Liquid/GHC/API/Extra.hs
+++ b/src-ghc/Liquid/GHC/API/Extra.hs
@@ -11,18 +11,17 @@
   , dataConSig
   , desugarModuleIO
   , fsToUnitId
-  , getDependenciesModuleNames
   , isPatErrorAlt
   , lookupModSummary
   , modInfoLookupNameIO
   , moduleInfoTc
-  , moduleUnitId
   , parseModuleIO
   , qualifiedNameFS
   , relevantModules
   , renderWithStyle
   , showPprQualified
   , showSDocQualified
+  , strictNothing
   , thisPackage
   , tyConRealArity
   , typecheckModuleIO
@@ -35,6 +34,7 @@
 import Data.Generics (extQ)
 import Data.Foldable                  (asum)
 import Data.List                      (foldl', sortOn)
+import qualified Data.Map as Map
 import qualified Data.Set as S
 import GHC.Core                       as Ghc
 import GHC.Core.Coercion              as Ghc
@@ -44,6 +44,7 @@
 import GHC.Data.FastString            as Ghc
 import qualified GHC.Data.EnumSet as EnumSet
 import GHC.Data.Maybe
+import qualified GHC.Data.Strict
 import GHC.Driver.Env
 import GHC.Driver.Main
 import GHC.Driver.Session             as Ghc
@@ -54,7 +55,12 @@
 import GHC.Types.Unique               (getUnique)
 import GHC.Types.Unique.FM
 
-import GHC.Unit.Module.Deps           as Ghc (Dependencies(dep_mods))
+import GHC.Unit.Module.Deps           as Ghc (Dependencies(dep_direct_mods))
+import GHC.Unit.Module.Graph          as Ghc
+  ( NodeKey(NodeKey_Module)
+  , ModNodeKeyWithUid(ModNodeKeyWithUid)
+  , mgTransDeps
+  )
 import GHC.Unit.Module.ModDetails     (md_types)
 import GHC.Unit.Module.ModSummary     (isBootSummary)
 import GHC.Utils.Outputable           as Ghc hiding ((<>))
@@ -67,9 +73,6 @@
 fsToUnitId :: FastString -> UnitId
 fsToUnitId = toUnitId . fsToUnit
 
-moduleUnitId :: Module -> UnitId
-moduleUnitId = toUnitId . moduleUnit
-
 thisPackage :: DynFlags -> UnitId
 thisPackage = homeUnitId_
 
@@ -83,8 +86,17 @@
         Nothing -> acc
         Just ks -> go (acc + 1) ks
 
-getDependenciesModuleNames :: Dependencies -> [ModuleNameWithIsBoot]
-getDependenciesModuleNames = dep_mods
+getDependenciesModuleNames :: ModuleGraph -> UnitId -> Dependencies -> [ModuleNameWithIsBoot]
+getDependenciesModuleNames mg unitId deps =
+    mapMaybe nodeKeyToModuleName $ S.toList $ S.unions $ catMaybes
+      [ Map.lookup k tdeps
+      | (_, m) <- S.toList $ dep_direct_mods deps
+      , let k = NodeKey_Module $ ModNodeKeyWithUid m unitId
+      ]
+  where
+    tdeps = mgTransDeps mg
+    nodeKeyToModuleName (NodeKey_Module (ModNodeKeyWithUid m _)) = Just m
+    nodeKeyToModuleName _ = Nothing
 
 renderWithStyle :: DynFlags -> SDoc -> PprStyle -> String
 renderWithStyle dynflags sdoc style = Ghc.renderWithContext (Ghc.initSDocContext dynflags style) sdoc
@@ -95,13 +107,13 @@
   = (dataConUnivAndExTyCoVars dc, dataConTheta dc, map irrelevantMult $ dataConOrigArgTys dc, dataConOrigResTy dc)
 
 -- | The collection of dependencies and usages modules which are relevant for liquidHaskell
-relevantModules :: ModGuts -> S.Set Module
-relevantModules modGuts = used `S.union` dependencies
+relevantModules :: ModuleGraph -> ModGuts -> S.Set Module
+relevantModules mg modGuts = used `S.union` dependencies
   where
     dependencies :: S.Set Module
     dependencies = S.fromList $ map (toModule . gwib_mod)
                               . filter ((NotBoot ==) . gwib_isBoot)
-                              . getDependenciesModuleNames $ deps
+                              . getDependenciesModuleNames mg thisUnitId $ deps
 
     deps :: Dependencies
     deps = mg_deps modGuts
@@ -109,8 +121,10 @@
     thisModule :: Module
     thisModule = mg_module modGuts
 
+    thisUnitId = moduleUnitId thisModule
+
     toModule :: ModuleName -> Module
-    toModule = unStableModule . mkStableModule (moduleUnitId thisModule)
+    toModule = unStableModule . mkStableModule thisUnitId
 
     used :: S.Set Module
     used = S.fromList $ foldl' collectUsage mempty . mg_usages $ modGuts
@@ -192,7 +206,7 @@
 
     -- TODO: take into account anchor_op, which only matters if the source was
     -- pre-processed by an exact-print-aware tool.
-    toRealSrc (L a e) = L (RealSrcSpan (anchor a) Nothing) e
+    toRealSrc (L a e) = L (RealSrcSpan (anchor a) strictNothing) e
 
     spanToLineColumn =
       fmap (\s -> (srcSpanStartLine s, srcSpanStartCol s)) . srcSpanToRealSrcSpan
@@ -221,10 +235,9 @@
     Just tyThing -> return (Just tyThing)
     Nothing      -> lookupType hscEnv name
 
-moduleInfoTc :: HscEnv -> ModSummary -> TcGblEnv -> IO ModuleInfoLH
-moduleInfoTc hscEnv ms tcGblEnv = do
-  let hsc_env_tmp = hscEnv { hsc_dflags = ms_hspp_opts ms }
-  details <- md_types <$> liftIO (makeSimpleDetails hsc_env_tmp tcGblEnv)
+moduleInfoTc :: HscEnv -> TcGblEnv -> IO ModuleInfoLH
+moduleInfoTc hscEnv tcGblEnv = do
+  details <- md_types <$> liftIO (makeSimpleDetails (hsc_logger hscEnv) tcGblEnv)
   pure ModuleInfoLH { minflh_type_env = details }
 
 -- | Tells if a case alternative calls to patError
@@ -271,3 +284,7 @@
 myQualify :: Ghc.PrintUnqualified
 myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames }
 -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 }
+
+
+strictNothing :: GHC.Data.Strict.Maybe a
+strictNothing = GHC.Data.Strict.Nothing
diff --git a/src/Language/Haskell/Liquid/Bare/Elaborate.hs b/src/Language/Haskell/Liquid/Bare/Elaborate.hs
--- a/src/Language/Haskell/Liquid/Bare/Elaborate.hs
+++ b/src/Language/Haskell/Liquid/Bare/Elaborate.hs
@@ -568,7 +568,7 @@
 
 
 mkHsTyConApp ::  IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
-mkHsTyConApp tyconId tyargs = nlHsTyConApp Prefix tyconId (map HsValArg tyargs)
+mkHsTyConApp tyconId tyargs = nlHsTyConApp NotPromoted Prefix tyconId (map HsValArg tyargs)
 
 -- | Embed fixpoint expressions into parsed haskell expressions.
 --   It allows us to bypass the GHC parser and use arbitrary symbols
@@ -688,10 +688,11 @@
 specTypeToLHsType =
   flip (ghylo (distPara @SpecType) distAna) (fmap pure . project) $ \case
     RVarF (RTV tv) _ -> nlHsTyVar
+      NotPromoted
       -- (GM.notracePpr ("varRdr" ++ F.showpp (F.symbol tv)) $ getRdrName tv)
       (symbolToRdrNameNs tvName (F.symbol tv))
     RFunF _ _ (tin, tin') (_, tout) _
-      | isClassType tin -> noLocA $ HsQualTy Ghc.noExtField (Just (noLocA [tin'])) tout
+      | isClassType tin -> noLocA $ HsQualTy Ghc.noExtField (noLocA [tin']) tout
       | otherwise       -> nlHsFunTy tin' tout
     RAllTF (ty_var_value -> (RTV tv)) (_, t) _ -> noLocA $ HsForAllTy
       Ghc.noExtField
diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs
--- a/src/Language/Haskell/Liquid/Constraint/Generate.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -14,7 +14,7 @@
 -- | This module defines the representation of Subtyping and WF Constraints,
 --   and the code for syntax-directed constraint generation.
 
-module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints, generateConstraintsWithEnv, caseEnv, consE ) where
+module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints, caseEnv, consE ) where
 
 import           Prelude                                       hiding (error)
 import           GHC.Stack ( CallStack )
@@ -61,13 +61,6 @@
 generateConstraints info = {-# SCC "ConsGen" #-} execState act $ initCGI cfg info
   where
     act                  = do { γ <- initEnv info; consAct γ cfg info }
-    cfg                  = getConfig   info
-
-generateConstraintsWithEnv :: TargetInfo -> CGInfo -> CGEnv -> CGInfo
---------------------------------------------------------------------------------
-generateConstraintsWithEnv info cgi γ = {-# SCC "ConsGenEnv" #-} execState act cgi
-  where
-    act                  = consAct γ cfg info
     cfg                  = getConfig   info
 
 consAct :: CGEnv -> Config -> TargetInfo -> CG ()
diff --git a/src/Language/Haskell/Liquid/Constraint/Termination.hs b/src/Language/Haskell/Liquid/Constraint/Termination.hs
--- a/src/Language/Haskell/Liquid/Constraint/Termination.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Termination.hs
@@ -22,10 +22,6 @@
 import           Control.Applicative (liftA2)
 import           Control.Monad.State ( gets, forM, foldM )
 import           Text.PrettyPrint.HughesPJ ( (<+>), text )
-import           GHC.Types.Var (Var)
-import           GHC.Types.Name (NamedThing, getSrcSpan)
-import           GHC.Core.TyCon (TyCon)
-import           GHC.Core (Bind, CoreExpr, bindersOf)
 import qualified Language.Haskell.Liquid.GHC.Misc                    as GM
 import qualified Language.Fixpoint.Types            as F
 import           Language.Fixpoint.Types.PrettyPrint (PPrint)
@@ -40,9 +36,11 @@
    toRTypeRep, structuralTerm, bkArrowDeep, mkArrow, bkUniv, bkArrow, fromRTypeRep)
 import           Language.Haskell.Liquid.Types.RefType (isDecreasing, makeDecrType, makeLexRefa, makeNumEnv)
 import           Language.Haskell.Liquid.Misc (safeFromLeft, replaceN, (<->), zip4, safeFromJust, fst5)
+import qualified Liquid.GHC.API as GHC
 
 
 data TCheck = TerminationCheck | StrataCheck | NoCheck
+  deriving Show
 
 mkTCheck :: Bool -> Bool -> TCheck
 mkTCheck tc is
@@ -50,7 +48,7 @@
   | tc        = TerminationCheck
   | otherwise = NoCheck
 
-doTermCheck :: Config -> Bind Var -> CG Bool
+doTermCheck :: Config -> GHC.Bind GHC.Var -> CG Bool
 doTermCheck cfg bind = do
   lazyVs    <- gets specLazy
   termVs    <- gets specTmVars
@@ -59,9 +57,9 @@
   return     $ chk && not skip
   where
     nocheck  = if typeclass cfg then GM.isEmbeddedDictVar else GM.isInternal
-    xs       = bindersOf bind
+    xs       = GHC.bindersOf bind
 
-makeTermEnvs :: CGEnv -> [(Var, [F.Located F.Expr])] -> [(Var, CoreExpr)]
+makeTermEnvs :: CGEnv -> [(GHC.Var, [F.Located F.Expr])] -> [(GHC.Var, GHC.CoreExpr)]
              -> [SpecType] -> [SpecType]
              -> [CGEnv]
 makeTermEnvs γ xtes xes ts ts' = setTRec γ . zip xs <$> rts
@@ -78,7 +76,7 @@
     rts  = zipWith (addObligation OTerm) ts' <$> rss
     (xs, ces)    = unzip xes
     mkSub ys ys' = F.mkSubst [(x, F.EVar y) | (x, y) <- zip ys ys']
-    collectArgs' = GM.collectArguments . length . ty_binds . toRTypeRep
+    collectArgs' = collectArguments . length . ty_binds . toRTypeRep
     err x        = "Constant: makeTermEnvs: no terminating expression for " ++ GM.showPpr x
 
 addObligation :: Oblig -> SpecType -> RReft -> SpecType
@@ -92,7 +90,7 @@
 -- | TERMINATION TYPE ----------------------------------------------------------
 --------------------------------------------------------------------------------
 
-makeDecrIndex :: (Var, Template SpecType, [Var]) -> CG (Maybe Int)
+makeDecrIndex :: (GHC.Var, Template SpecType, [GHC.Var]) -> CG (Maybe Int)
 makeDecrIndex (x, Assumed t, args)
   = do dindex <- makeDecrIndexTy x t args
        case dindex of
@@ -105,14 +103,14 @@
          Right i  -> return $ Just i
 makeDecrIndex _ = return Nothing
 
-makeDecrIndexTy :: Var -> SpecType -> [Var] -> CG (Either (TError t) Int)
+makeDecrIndexTy :: GHC.Var -> SpecType -> [GHC.Var] -> CG (Either (TError t) Int)
 makeDecrIndexTy x st args
   = do autosz <- gets autoSize
        return $ case dindex autosz of
          Nothing -> Left msg
          Just i  -> Right i
     where
-       msg  = ErrTermin (getSrcSpan x) [F.pprint x] (text "No decreasing parameter")
+       msg  = ErrTermin (GHC.getSrcSpan x) [F.pprint x] (text "No decreasing parameter")
        trep = toRTypeRep $ unOCons st
        ts   = ty_args trep
        tvs  = zip ts args
@@ -122,7 +120,7 @@
        dindex     autosz = L.findIndex (p autosz) tvs
 
 recType :: F.Symbolic a
-        => S.HashSet TyCon
+        => S.HashSet GHC.TyCon
         -> (([a], Maybe Int), (t, Maybe Int, SpecType))
         -> SpecType
 recType _       ((_, Nothing), (_, Nothing, t)) = t
@@ -133,20 +131,20 @@
         xts  = zip (ty_binds trep) (ty_args trep)
         trep = toRTypeRep $ unOCons t
 
-checkIndex :: (NamedThing t, PPrint t, PPrint a)
+checkIndex :: (GHC.NamedThing t, PPrint t, PPrint a)
            => (t, [a], Template (RType c tv r), Maybe Int)
            -> CG (Maybe (RType c tv r))
 checkIndex (_,  _, _, Nothing   ) = return Nothing
 checkIndex (x, vs, t, Just index) = safeLogIndex msg1 vs index >> safeLogIndex msg2 ts index
     where
-       loc   = getSrcSpan x
+       loc   = GHC.getSrcSpan x
        ts    = ty_args $ toRTypeRep $ unOCons $ unTemplate t
        msg1  = ErrTermin loc [xd] (text "No decreasing" <+> F.pprint index <-> text "-th argument on" <+> xd <+> text "with" <+> F.pprint vs)
        msg2  = ErrTermin loc [xd] (text  "No decreasing parameter")
        xd    = F.pprint x
 
 makeRecType :: (Enum a1, Eq a1, Num a1, F.Symbolic a)
-            => S.HashSet TyCon
+            => S.HashSet GHC.TyCon
             -> SpecType
             -> Maybe a
             -> Maybe (F.Symbol, SpecType)
@@ -180,8 +178,8 @@
   | otherwise      = return $ Just $ ls !! n
 
 -- RJ: AAAAAAARGHHH!!!!!! THIS CODE IS HORRIBLE!!!!!!!!!
-consCBSizedTys :: (Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)) ->
-                  CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
+consCBSizedTys :: (Bool -> CGEnv -> (GHC.Var, GHC.CoreExpr, Template SpecType) -> CG (Template SpecType)) ->
+                  CGEnv -> [(GHC.Var, GHC.CoreExpr)] -> CG CGEnv
 consCBSizedTys consBind γ xes
   = do ts'      <- forM xes $ \(x, e) -> varTemplate γ (x, Just e)
        autoenv  <- gets autoSize
@@ -200,14 +198,14 @@
        allowTC        = typeclass (getConfig γ)
        (vars, es)     = unzip xes
        dxs            = F.pprint <$> vars
-       collectArgs'   = GM.collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate
+       collectArgs'   = collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate
        checkEqTypes :: [Maybe SpecType] -> CG [SpecType]
        checkEqTypes x = checkAllVsHead err1 toRSort (catMaybes x)
        err1           = ErrTermin loc dxs $ text "The decreasing parameters should be of same type"
        checkSameLens :: [Maybe Int] -> CG [Maybe Int]
        checkSameLens  = checkAllVsHead err2 length
        err2           = ErrTermin loc dxs $ text "All Recursive functions should have the same number of decreasing parameters"
-       loc            = getSrcSpan (head vars)
+       loc            = GHC.getSrcSpan (head vars)
 
        checkAllVsHead :: Eq b => Error -> (a -> b) -> [a] -> CG [a]
        checkAllVsHead _   _ []          = return []
@@ -215,8 +213,28 @@
          | all (== f x) (f <$> xs) = return (x:xs)
          | otherwise               = addWarning err >> return []
 
-consCBWithExprs :: (Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)) ->
-                   CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
+-- See Note [Shape of normalized terms] in
+-- Language.Haskell.Liquid.Transforms.ANF
+collectArguments :: Int -> GHC.CoreExpr -> [GHC.Var]
+collectArguments n e = take n (vs' ++ vs)
+  where
+    (vs', e')        = collectValBinders' $ snd $ GHC.collectTyBinders e
+    vs               = fst $ GHC.collectBinders $ ignoreLetBinds e'
+
+collectValBinders' :: GHC.CoreExpr -> ([GHC.Var], GHC.CoreExpr)
+collectValBinders' = go []
+  where
+    go tvs (GHC.Lam b e) | GHC.isTyVar b = go tvs     e
+    go tvs (GHC.Lam b e) | GHC.isId    b = go (b:tvs) e
+    go tvs (GHC.Tick _ e)            = go tvs e
+    go tvs e                         = (reverse tvs, e)
+
+ignoreLetBinds :: GHC.Expr b -> GHC.Expr b
+ignoreLetBinds (GHC.Let (GHC.NonRec _ _) e') = ignoreLetBinds e'
+ignoreLetBinds e = e
+
+consCBWithExprs :: (Bool -> CGEnv -> (GHC.Var, GHC.CoreExpr, Template SpecType) -> CG (Template SpecType)) ->
+                   CGEnv -> [(GHC.Var, GHC.CoreExpr)] -> CG CGEnv
 consCBWithExprs consBind γ xes
   = do ts0      <- forM xes $ \(x, e) -> varTemplate γ (x, Just e)
        texprs   <- gets termExprs
diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs
--- a/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/src/Language/Haskell/Liquid/GHC/Interface.hs
@@ -122,7 +122,7 @@
     f (Rec xes)    = any eqFd (fst <$> xes)
     eqFd x         = varName x == varName fd
     deps           = concatMap unfoldDep unfolds
-    unfolds        = unfoldingInfo . idInfo <$> concatMap bindersOf cbs'
+    unfolds        = realUnfoldingInfo . idInfo <$> concatMap bindersOf cbs'
 
 unfoldDep :: Unfolding -> [Id]
 unfoldDep (DFunUnfolding _ _ e)       = concatMap exprDep e
@@ -190,8 +190,8 @@
 --   for this module; we will use this to create our name-resolution environment
 --   (see `Bare.Resolve`)
 ---------------------------------------------------------------------------------------
-lookupTyThings :: HscEnv -> ModSummary -> TcGblEnv -> IO [(Name, Maybe TyThing)]
-lookupTyThings hscEnv modSum tcGblEnv = forM names (lookupTyThing hscEnv modSum tcGblEnv)
+lookupTyThings :: HscEnv -> TcGblEnv -> IO [(Name, Maybe TyThing)]
+lookupTyThings hscEnv tcGblEnv = forM names (lookupTyThing hscEnv tcGblEnv)
   where
     names :: [Ghc.Name]
     names  = liftM2 (++)
@@ -199,32 +199,32 @@
              (fmap is_dfun_name . tcg_insts) tcGblEnv
 -- | Lookup a single 'Name' in the GHC environment, yielding back the 'Name' alongside the 'TyThing',
 -- if one is found.
-lookupTyThing :: HscEnv -> ModSummary -> TcGblEnv -> Name -> IO (Name, Maybe TyThing)
-lookupTyThing hscEnv modSum tcGblEnv n = do
+lookupTyThing :: HscEnv -> TcGblEnv -> Name -> IO (Name, Maybe TyThing)
+lookupTyThing hscEnv tcGblEnv n = do
   mty <- runMaybeT $
          MaybeT (Ghc.hscTcRcLookupName hscEnv n)
          `mplus`
          MaybeT (
-           do mi  <- moduleInfoTc hscEnv modSum tcGblEnv
+           do mi  <- moduleInfoTc hscEnv tcGblEnv
               modInfoLookupNameIO hscEnv mi n
            )
   return (n, mty)
 
-availableTyThings :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [TyThing]
-availableTyThings hscEnv modSum tcGblEnv avails =
+availableTyThings :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [TyThing]
+availableTyThings hscEnv tcGblEnv avails =
     fmap catMaybes $
-      mapM (fmap snd . lookupTyThing hscEnv modSum tcGblEnv) $
+      mapM (fmap snd . lookupTyThing hscEnv tcGblEnv) $
       availableNames avails
 
 -- | Returns all the available (i.e. exported) 'TyCon's (type constructors) for the input 'Module'.
-availableTyCons :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [Ghc.TyCon]
-availableTyCons hscEnv modSum tcGblEnv avails =
-  fmap (\things -> [tyCon | (ATyCon tyCon) <- things]) (availableTyThings hscEnv modSum tcGblEnv avails)
+availableTyCons :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [Ghc.TyCon]
+availableTyCons hscEnv tcGblEnv avails =
+  fmap (\things -> [tyCon | (ATyCon tyCon) <- things]) (availableTyThings hscEnv tcGblEnv avails)
 
 -- | Returns all the available (i.e. exported) 'Var's for the input 'Module'.
-availableVars :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [Ghc.Var]
-availableVars hscEnv modSum tcGblEnv avails =
-  fmap (\things -> [var | (AnId var) <- things]) (availableTyThings hscEnv modSum tcGblEnv avails)
+availableVars :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [Ghc.Var]
+availableVars hscEnv tcGblEnv avails =
+  fmap (\things -> [var | (AnId var) <- things]) (availableTyThings hscEnv tcGblEnv avails)
 
 availableNames :: [AvailInfo] -> [Name]
 availableNames =
diff --git a/src/Language/Haskell/Liquid/GHC/Logging.hs b/src/Language/Haskell/Liquid/GHC/Logging.hs
--- a/src/Language/Haskell/Liquid/GHC/Logging.hs
+++ b/src/Language/Haskell/Liquid/GHC/Logging.hs
@@ -9,10 +9,11 @@
      to pay the price of a pretty-printing \"roundtrip\".
 -}
 
-module Language.Haskell.Liquid.GHC.Logging (
-    fromPJDoc
+module Language.Haskell.Liquid.GHC.Logging
+  ( addTcRnUnknownMessage
+  , addTcRnUnknownMessages
+  , fromPJDoc
   , putWarnMsg
-  , mkLongErrAt
   ) where
 
 import qualified Liquid.GHC.API as GHC
@@ -27,23 +28,20 @@
 -- | Like the original 'putLogMsg', but internally converts the input 'Doc' (from the \"pretty\" library)
 -- into GHC's internal 'SDoc'.
 putLogMsg :: GHC.Logger
-          -> GHC.DynFlags
-          -> GHC.WarnReason
           -> GHC.Severity
           -> GHC.SrcSpan
           -> Maybe GHC.PprStyle
           -> PJ.Doc
           -> IO ()
-putLogMsg logger dynFlags reason sev srcSpan _mbStyle =
-  GHC.putLogMsg logger dynFlags reason sev srcSpan . GHC.text . PJ.render
+putLogMsg logger sev srcSpan _mbStyle =
+  GHC.putLogMsg logger (GHC.logFlags logger) (GHC.MCDiagnostic sev GHC.WarningWithoutFlag) srcSpan . GHC.text . PJ.render
 
-defaultErrStyle :: GHC.DynFlags -> GHC.PprStyle
-defaultErrStyle _dynFlags = GHC.defaultErrStyle
+putWarnMsg :: GHC.Logger -> GHC.SrcSpan -> PJ.Doc -> IO ()
+putWarnMsg logger srcSpan doc =
+  putLogMsg logger GHC.SevWarning srcSpan (Just GHC.defaultErrStyle) doc
 
-putWarnMsg :: GHC.Logger -> GHC.DynFlags -> GHC.SrcSpan -> PJ.Doc -> IO ()
-putWarnMsg logger dynFlags srcSpan doc =
-  putLogMsg logger dynFlags GHC.NoReason GHC.SevWarning srcSpan (Just $ defaultErrStyle dynFlags) doc
+addTcRnUnknownMessage :: GHC.SrcSpan -> PJ.Doc -> GHC.TcRn ()
+addTcRnUnknownMessage srcSpan = GHC.addErrAt srcSpan . GHC.TcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc
 
--- | Like GHC's 'mkLongErrAt', but it builds the final 'ErrMsg' out of two \"HughesPJ\"'s 'Doc's.
-mkLongErrAt :: GHC.SrcSpan -> PJ.Doc -> PJ.Doc -> GHC.TcRn (GHC.MsgEnvelope GHC.DecoratedSDoc)
-mkLongErrAt srcSpan msg extra = GHC.mkLongErrAt srcSpan (fromPJDoc msg) (fromPJDoc extra)
+addTcRnUnknownMessages :: [(GHC.SrcSpan, PJ.Doc)] -> GHC.TcRn ()
+addTcRnUnknownMessages = GHC.addErrs . map (fmap (GHC.TcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc))
diff --git a/src/Language/Haskell/Liquid/GHC/Misc.hs b/src/Language/Haskell/Liquid/GHC/Misc.hs
--- a/src/Language/Haskell/Liquid/GHC/Misc.hs
+++ b/src/Language/Haskell/Liquid/GHC/Misc.hs
@@ -28,11 +28,10 @@
 import           Liquid.GHC.API            as Ghc hiding ( L
                                                                           , sourceName
                                                                           , showPpr
-                                                                          , showSDocDump
                                                                           , panic
                                                                           , showSDoc
                                                                           )
-import qualified Liquid.GHC.API            as Ghc (GenLocated (L), showSDoc, panic, showSDocDump)
+import qualified Liquid.GHC.API            as Ghc (GenLocated (L), showSDoc, panic)
 
 
 import           Data.Char                                  (isLower, isSpace, isUpper)
@@ -46,7 +45,7 @@
 import qualified Data.Text.Encoding                         as T
 import qualified Data.Text                                  as T
 import           Control.Arrow                              (second)
-import           Control.Monad                              ((>=>), foldM)
+import           Control.Monad                              ((>=>), foldM, when)
 import qualified Text.PrettyPrint.HughesPJ                  as PJ
 import           Language.Fixpoint.Types                    hiding (L, panic, Loc (..), SrcSpan, Constant, SESearch (..))
 import qualified Language.Fixpoint.Types                    as F
@@ -74,7 +73,7 @@
 
 tickSrcSpan :: CoreTickish -> SrcSpan
 tickSrcSpan (ProfNote cc _ _) = cc_loc cc
-tickSrcSpan (SourceNote ss _) = RealSrcSpan ss Nothing
+tickSrcSpan (SourceNote ss _) = RealSrcSpan ss strictNothing
 tickSrcSpan _                 = noSrcSpan
 
 --------------------------------------------------------------------------------
@@ -112,7 +111,7 @@
 
 -- FIXME: reusing uniques like this is really dangerous
 stringTyConWithKind :: Kind -> Char -> Int -> String -> TyCon
-stringTyConWithKind k c n s = Ghc.mkKindTyCon name [] k [] name
+stringTyConWithKind k c n s = Ghc.mkPrimTyCon name [] k []
   where
     name          = mkInternalName (mkUnique c n) occ noSrcSpan
     occ           = mkTcOcc s
@@ -201,7 +200,7 @@
 -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 }
 
 showSDocDump :: Ghc.SDoc -> String
-showSDocDump  = Ghc.showSDocDump Ghc.defaultSDocContext
+showSDocDump  = Ghc.renderWithContext Ghc.defaultSDocContext
 
 instance Outputable a => Outputable (S.HashSet a) where
   ppr = ppr . S.toList
@@ -246,7 +245,7 @@
     p'             = srcSpanSourcePosE sp
 
 sourcePos2SrcSpan :: SourcePos -> SourcePos -> SrcSpan
-sourcePos2SrcSpan p p' = RealSrcSpan (packRealSrcSpan f (unPos l) (unPos c) (unPos l') (unPos c')) Nothing
+sourcePos2SrcSpan p p' = RealSrcSpan (packRealSrcSpan f (unPos l) (unPos c) (unPos l') (unPos c')) strictNothing
   where
     (f, l,  c)         = F.sourcePosElts p
     (_, l', c')        = F.sourcePosElts p'
@@ -327,40 +326,6 @@
 namedPanic x msg = panic (Just (getSrcSpan x)) msg
 
 --------------------------------------------------------------------------------
--- | Manipulating CoreExpr -----------------------------------------------------
---------------------------------------------------------------------------------
-
-collectArguments :: Int -> CoreExpr -> [Var]
-collectArguments n e = if length xs > n then take n xs else xs
-  where
-    (vs', e')        = collectValBinders' $ snd $ collectTyBinders e
-    vs               = fst $ collectBinders $ ignoreLetBinds e'
-    xs               = vs' ++ vs
-
-{-
-collectTyBinders :: CoreExpr -> ([Var], CoreExpr)
-collectTyBinders expr
-  = go [] expr
-  where
-    go tvs (Lam b e) | isTyVar b = go (b:tvs) e
-    go tvs e                     = (reverse tvs, e)
--}
-
-collectValBinders' :: Ghc.Expr Var -> ([Var], Ghc.Expr Var)
-collectValBinders' = go []
-  where
-    go tvs (Lam b e) | isTyVar b = go tvs     e
-    go tvs (Lam b e) | isId    b = go (b:tvs) e
-    go tvs (Tick _ e)            = go tvs e
-    go tvs e                     = (reverse tvs, e)
-
-ignoreLetBinds :: Ghc.Expr t -> Ghc.Expr t
-ignoreLetBinds (Let (NonRec _ _) e')
-  = ignoreLetBinds e'
-ignoreLetBinds e
-  = e
-
---------------------------------------------------------------------------------
 -- | Predicates on CoreExpr and DataCons ---------------------------------------
 --------------------------------------------------------------------------------
 
@@ -420,7 +385,7 @@
 lookupRdrName :: HscEnv -> ModuleName -> RdrName -> IO (Maybe Name)
 lookupRdrName hsc_env mod_name rdr_name = do
     -- First find the package the module resides in by searching exposed packages and home modules
-    found_module <- findImportedModule hsc_env mod_name Nothing
+    found_module <- findImportedModule hsc_env mod_name NoPkgQual
     case found_module of
         Found _ mod' -> do
             -- Find the exports of the module
@@ -438,7 +403,7 @@
 -- XXX                        [gre] -> return (Just (gre_name gre))
                         []    -> return Nothing
                         _     -> Ghc.panic "lookupRdrNameInModule"
-                Nothing -> throwCmdLineErrorS dflags $ Ghc.hsep [Ghc.ptext (sLit "Could not determine the exports of the module"), ppr mod_name]
+                Nothing -> throwCmdLineErrorS dflags $ Ghc.hsep [Ghc.ptext (Ghc.mkPtrString "Could not determine the exports of the module"), ppr mod_name]
         err' -> throwCmdLineErrorS dflags $ cannotFindModule hsc_env mod_name err'
   where dflags = hsc_dflags hsc_env
         throwCmdLineErrorS dflags' = throwCmdLineError . Ghc.showSDoc dflags'
@@ -460,12 +425,6 @@
 -- | Symbol Conversions --------------------------------------------------------
 --------------------------------------------------------------------------------
 
-symbolTyConWithKind :: Kind -> Char -> Int -> Symbol -> TyCon
-symbolTyConWithKind k x i n = stringTyConWithKind k x i (symbolString n)
-
-symbolTyCon :: Char -> Int -> Symbol -> TyCon
-symbolTyCon x i n = stringTyCon x i (symbolString n)
-
 symbolTyVar :: Symbol -> TyVar
 symbolTyVar = stringTyVar . symbolString
 
@@ -719,9 +678,6 @@
 synTyConRhs_maybe :: TyCon -> Maybe Type
 synTyConRhs_maybe = Ghc.synTyConRhs_maybe
 
-tcRnLookupRdrName :: HscEnv -> Ghc.LocatedN RdrName -> IO (Messages DecoratedSDoc, Maybe [Name])
-tcRnLookupRdrName = Ghc.tcRnLookupRdrName
-
 showCBs :: Bool -> [CoreBind] -> String
 showCBs untidy
   | untidy    =
@@ -919,7 +875,18 @@
     -- Ignore the dictionary bindings
     evbs' <- simplifyInteractive residual
     full_expr <- zonkTopLExpr (mkHsDictLet (EvBinds evbs') (mkHsDictLet evbs tc_expr))
-    initDsTc $ dsLExpr full_expr
+    (ds_msgs, me) <- initDsTc $ dsLExpr full_expr
+
+    logger <- getLogger
+    diag_opts <- initDiagOpts <$> getDynFlags
+    liftIO $ printMessages logger diag_opts ds_msgs
+
+    case me of
+      Nothing -> failM
+      Just e -> do
+        when (errorsOrFatalWarningsFound ds_msgs)
+          failM
+        return e
 
 newtype HashableType = HashableType {getHType :: Type}
 
diff --git a/src/Language/Haskell/Liquid/GHC/Plugin.hs b/src/Language/Haskell/Liquid/GHC/Plugin.hs
--- a/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -27,7 +27,7 @@
                                                                  , filterReportErrorsWith
                                                                  , defaultFilterReporter
                                                                  , reduceFilters )
-import qualified Language.Haskell.Liquid.GHC.Logging     as LH   (fromPJDoc)
+import qualified Language.Haskell.Liquid.GHC.Logging     as LH   (addTcRnUnknownMessages)
 
 import           Language.Haskell.Liquid.GHC.Plugin.Types
 import           Language.Haskell.Liquid.GHC.Plugin.Util as Util
@@ -127,7 +127,7 @@
     liquidPluginGo summary gblEnv = do
       logger <- getLogger
       dynFlags <- getDynFlags
-      withTiming logger dynFlags (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do
+      withTiming logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do
         if gopt Opt_Haddock dynFlags
           then do
             -- Warn the user
@@ -136,7 +136,7 @@
                                   ]
             let srcLoc  = mkSrcLoc (mkFastString $ ms_hspp_file summary) 1 1
             let warning = mkWarning (mkSrcSpan srcLoc srcLoc) msg
-            liftIO $ printWarning logger dynFlags warning
+            liftIO $ printWarning logger warning
             pure gblEnv
           else do
             newGblEnv <- typecheckHook summary gblEnv
@@ -229,9 +229,9 @@
   -- would lead to a loop if we didn't remove the plugin when calling the type
   -- checker.
   typechecked     <- liftIO $ typecheckModuleIO (dropPlugins env) (LH.ignoreInline parsed)
-  resolvedNames   <- liftIO $ LH.lookupTyThings env modSummary tcGblEnv
-  availTyCons     <- liftIO $ LH.availableTyCons env modSummary tcGblEnv (tcg_exports tcGblEnv)
-  availVars       <- liftIO $ LH.availableVars env modSummary tcGblEnv (tcg_exports tcGblEnv)
+  resolvedNames   <- liftIO $ LH.lookupTyThings env tcGblEnv
+  availTyCons     <- liftIO $ LH.availableTyCons env tcGblEnv (tcg_exports tcGblEnv)
+  availVars       <- liftIO $ LH.availableVars env tcGblEnv (tcg_exports tcGblEnv)
 
   unoptimisedGuts <- liftIO $ desugarModuleIO env modSummary typechecked
 
@@ -244,7 +244,7 @@
     thisModule :: Module
     thisModule = tcg_mod tcGblEnv
 
-    dropPlugins hsc_env = hsc_env { hsc_plugins = [], hsc_static_plugins = [] }
+    dropPlugins hsc_env = hsc_env { hsc_plugins = emptyPlugins }
 
 serialiseSpec :: Module -> TcGblEnv -> LiquidLib -> TcM TcGblEnv
 serialiseSpec thisModule tcGblEnv liquidLib = do
@@ -277,8 +277,9 @@
 
 processInputSpec :: Config -> PipelineData -> ModSummary -> TcGblEnv -> BareSpec -> TcM (Either LiquidCheckException TcGblEnv)
 processInputSpec cfg pipelineData modSummary tcGblEnv inputSpec = do
+  hscEnv <- env_top <$> getEnv
   debugLog $ " Input spec: \n" ++ show inputSpec
-  debugLog $ "Relevant ===> \n" ++ unlines (renderModule <$> S.toList (relevantModules modGuts))
+  debugLog $ "Relevant ===> \n" ++ unlines (renderModule <$> S.toList (relevantModules (hsc_mod_graph hscEnv) modGuts))
 
   logicMap :: LogicMap <- liftIO LH.makeLogicMap
 
@@ -291,7 +292,7 @@
       , lhModuleSummary   = modSummary
       , lhModuleTcData    = pdTcData pipelineData
       , lhModuleGuts      = pdUnoptimisedCore pipelineData
-      , lhRelevantModules = relevantModules modGuts
+      , lhRelevantModules = relevantModules (hsc_mod_graph hscEnv) modGuts
       }
 
   -- liftIO $ putStrLn ("liquidHaskellCheck 6: " ++ show isIg)
@@ -378,11 +379,11 @@
 errorLogger :: FilePath -> [Filter] -> OutputResult -> TcM ()
 errorLogger file filters outputResult = do
   LH.filterReportErrorsWith
-    FilterReportErrorsArgs { msgReporter = GHC.reportErrors
+    FilterReportErrorsArgs { errorReporter = \errs ->
+                               LH.addTcRnUnknownMessages [(sp, e) | (sp, e) <- errs]
                            , filterReporter = LH.defaultFilterReporter file
                            , failure = GHC.failM
                            , continue = pure ()
-                           , pprinter = \(spn, e) -> mkLongErrAt spn (LH.fromPJDoc e) O.empty
                            , matchingFilters = LH.reduceFilters (\(src, doc) -> PJ.render doc ++ " at " ++ LH.showPpr src) filters
                            , filters = filters
                            }
@@ -499,7 +500,6 @@
 
     targetSrc  <- liftIO $ makeTargetSrc moduleCfg file lhModuleTcData modGuts hscEnv
     logger <- getLogger
-    dynFlags <- getDynFlags
 
     -- See https://github.com/ucsd-progsys/liquidhaskell/issues/1711
     -- Due to the fact the internals can throw exceptions from pure code at any point, we need to
@@ -516,10 +516,10 @@
     (case result of
       -- Print warnings and errors, aborting the compilation.
       Left diagnostics -> do
-        liftIO $ mapM_ (printWarning logger dynFlags)    (allWarnings diagnostics)
+        liftIO $ mapM_ (printWarning logger)    (allWarnings diagnostics)
         reportErrs $ allErrors diagnostics
       Right (warnings, targetSpec, liftedSpec) -> do
-        liftIO $ mapM_ (printWarning logger dynFlags) warnings
+        liftIO $ mapM_ (printWarning logger) warnings
         let targetInfo = TargetInfo targetSrc targetSpec
 
         debugLog $ "bareSpec ==> "   ++ show bareSpec
diff --git a/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs b/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
--- a/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
+++ b/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
@@ -64,14 +64,14 @@
                   -- ^ Any relevant module fetched during dependency-discovery.
                   -> TcM [SpecFinderResult]
 findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do
-    eps <- liftIO $ readIORef (hsc_EPS hscEnv)
+    eps <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv)
     foldM (loadRelevantSpec eps) mempty mods
   where
 
     loadRelevantSpec :: ExternalPackageState -> [SpecFinderResult] -> Module -> TcM [SpecFinderResult]
     loadRelevantSpec eps !acc currentModule = do
       res <- liftIO $ runMaybeT $
-        lookupInterfaceAnnotations eps (hsc_HPT hscEnv) currentModule
+        lookupInterfaceAnnotations eps (ue_hpt $ hsc_unit_env hscEnv) currentModule
       case res of
         Nothing         -> do
           mAssm <- loadModuleLHAssumptionsIfAny currentModule
@@ -81,18 +81,19 @@
 
     loadModuleLHAssumptionsIfAny m | isImportExcluded m = return Nothing
                                    | otherwise = do
-      let assModName = assumptionsModuleName m
+      let assumptionsModName = assumptionsModuleName m
       -- loadInterface might mutate the EPS if the module is
       -- not already loaded
-      res <- liftIO $ findImportedModule hscEnv assModName Nothing
+      res <- liftIO $ findImportedModule hscEnv assumptionsModName NoPkgQual
       case res of
-        Found _ assMod -> do
-          _ <- initIfaceTcRn $ loadInterface "liquidhaskell assumptions" assMod ImportBySystem
+        Found _ assumptionsMod -> do
+          _ <- initIfaceTcRn $ loadInterface "liquidhaskell assumptions" assumptionsMod ImportBySystem
           -- read the EPS again
-          eps2 <- liftIO $ readIORef (hsc_EPS hscEnv)
+          eps2 <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv)
           -- now look up the assumptions
-          liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assMod
-        FoundMultiple{} -> failWithTc $ cannotFindModule hscEnv assModName res
+          liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assumptionsMod
+        FoundMultiple{} -> failWithTc $ TcRnUnknownMessage $ mkPlainError [] $
+                             cannotFindModule hscEnv assumptionsModName res
         _ -> return Nothing
 
     isImportExcluded m =
@@ -162,7 +163,7 @@
 
     lookupLiquidBaseModule :: ModuleName -> IO (Maybe StableModule)
     lookupLiquidBaseModule mn = do
-      res <- findExposedPackageModule env mn (Just "liquidhaskell")
+      res <- findImportedModule env mn (renamePkgQual (hsc_unit_env env) mn (Just "liquidhaskell"))
       case res of
         Found _ mdl -> pure $ Just (toStableModule mdl)
         _           -> pure Nothing
diff --git a/src/Language/Haskell/Liquid/Termination/Structural.hs b/src/Language/Haskell/Liquid/Termination/Structural.hs
--- a/src/Language/Haskell/Liquid/Termination/Structural.hs
+++ b/src/Language/Haskell/Liquid/Termination/Structural.hs
@@ -23,7 +23,7 @@
 import Data.Foldable (fold)
 
 terminationVars :: TargetInfo -> [Var]
-terminationVars info = failingBinds info >>= allBoundVars
+terminationVars info = failingBinds info >>= allLetBoundVars
 
 failingBinds :: TargetInfo -> [CoreBind]
 failingBinds info = filter (hasErrors . checkBind) structBinds
@@ -37,13 +37,10 @@
 
 checkBind :: CoreBind -> Result ()
 checkBind bind = do
-  srcCallInfo <- getCallInfoBind emptyEnv (deShadowBind bind)
+  srcCallInfo <- getCallInfoBind emptyEnv bind
   let structCallInfo = fmap toStructCall <$> srcCallInfo
   fold $ mapWithFun structDecreasing structCallInfo
 
-deShadowBind :: CoreBind -> CoreBind
-deShadowBind bind = head $ deShadowBinds [bind]
-
 findStructBinds :: HashSet Var -> CoreProgram -> [CoreBind]
 findStructBinds structFuns program = filter isStructBind program
   where
@@ -51,9 +48,9 @@
     isStructBind (Rec []) = False
     isStructBind (Rec ((f,_):xs)) = f `HS.member` structFuns || isStructBind (Rec xs)
 
-allBoundVars :: CoreBind -> [Var]
-allBoundVars (NonRec v e) = v : (nextBinds e >>= allBoundVars)
-allBoundVars (Rec binds) = map fst binds ++ (map snd binds >>= nextBinds >>= allBoundVars)
+allLetBoundVars :: CoreBind -> [Var]
+allLetBoundVars (NonRec v e) = v : (nextBinds e >>= allLetBoundVars)
+allLetBoundVars (Rec binds) = map fst binds ++ (map snd binds >>= nextBinds >>= allLetBoundVars)
 
 nextBinds :: CoreExpr -> [CoreBind]
 nextBinds = \case
diff --git a/src/Language/Haskell/Liquid/Transforms/ANF.hs b/src/Language/Haskell/Liquid/Transforms/ANF.hs
--- a/src/Language/Haskell/Liquid/Transforms/ANF.hs
+++ b/src/Language/Haskell/Liquid/Transforms/ANF.hs
@@ -255,8 +255,9 @@
 
 -- Note [Shape of normalized terms]
 --
--- The termination checker in Termination.collectArguments expects the type
--- binders to come before lets:
+-- The termination checker in
+-- Language.Haskell.Liquid.Constraint.Termination.collectArguments expects the
+-- type binders to come before lets:
 --
 -- > \ (@a) -> let ... in \ b c d -> ...
 --
diff --git a/src/Language/Haskell/Liquid/Types/Errors.hs b/src/Language/Haskell/Liquid/Types/Errors.hs
--- a/src/Language/Haskell/Liquid/Types/Errors.hs
+++ b/src/Language/Haskell/Liquid/Types/Errors.hs
@@ -90,7 +90,7 @@
 import qualified Language.Fixpoint.Misc       as Misc
 import qualified Language.Haskell.Liquid.Misc     as Misc
 import           Language.Haskell.Liquid.Misc ((<->))
-import           Language.Haskell.Liquid.Types.Generics
+import           Language.Haskell.Liquid.Types.Generics()
 
 type ParseError = P.ParseError String Void
 
@@ -726,7 +726,7 @@
 instance FromJSON SrcSpan where
   parseJSON (Object v) = do tag <- v .: "realSpan"
                             if tag
-                              then RealSrcSpan <$> v .: "spanInfo" <*> pure Nothing
+                              then RealSrcSpan <$> v .: "spanInfo" <*> pure strictNothing
                               else return noSrcSpan
   parseJSON _          = mempty
 
@@ -1082,8 +1082,8 @@
 
 sourceErrors :: String -> SourceError -> [TError t]
 sourceErrors s =
-  concatMap errMsgErrors . bagToList . srcErrorMessages
+  concatMap errMsgErrors . bagToList . getMessages . srcErrorMessages
   where
     errMsgErrors e = [ ErrGhc (errMsgSpan e) msg ]
       where
-        msg = text s $+$ nest 4 (text (show e))
+        msg = text s $+$ nest 4 (text $ showSDocQualified (pprLocMsgEnvelope e))
diff --git a/src/Language/Haskell/Liquid/Types/Generics.hs b/src/Language/Haskell/Liquid/Types/Generics.hs
--- a/src/Language/Haskell/Liquid/Types/Generics.hs
+++ b/src/Language/Haskell/Liquid/Types/Generics.hs
@@ -1,33 +1,18 @@
-{- | Geriving instances, generically.
-   This module shares some of the underlying ideas and implementations of the
-   [generic-data](https://hackage.haskell.org/package/generic-data-0.8.1.0/docs/Generic-Data.html)
-   package, allowing us to derive a bunch of instances using the underlying 'Generic' implementation,
-   but in a more declarative way.
-
-   In particular we introduc the 'Generically' newtype wrapper to be used with '-XDerivingVia' to make
-   derivation explicit. For example:
-
-@
-  data Foo = Foo
-       deriving Generic
-       deriving Eq via Generically Foo
-@
+{- | Deriving instances of Hashable and Binary, generically.
 
 -}
 
-{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
 
-module Language.Haskell.Liquid.Types.Generics where
+module Language.Haskell.Liquid.Types.Generics() where
 
 import GHC.Generics
 import Data.Hashable
 import Data.Binary
 import Data.Hashable.Generic
 import Data.Function
-
-newtype Generically a = Generically a deriving Generic
 
 -- * 'Hashable'
 
diff --git a/src/Language/Haskell/Liquid/Types/PrettyPrint.hs b/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
--- a/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
+++ b/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
@@ -41,7 +41,6 @@
 
   ) where
 
-import           Control.Monad                           (void)
 import qualified Data.HashMap.Strict              as M
 import qualified Data.List                        as L                               -- (sort)
 import qualified Data.Set                         as Set
@@ -62,7 +61,7 @@
                                                          , srcSpanStartLine
                                                          , srcSpanStartCol
                                                          )
-import           Language.Haskell.Liquid.GHC.Logging (mkLongErrAt)
+import           Language.Haskell.Liquid.GHC.Logging
 import           Language.Haskell.Liquid.GHC.Misc
 import           Language.Haskell.Liquid.Misc
 import           Language.Haskell.Liquid.Types.Types
@@ -98,8 +97,6 @@
 --------------------------------------------------------------------------------
 -- | A whole bunch of PPrint instances follow ----------------------------------
 --------------------------------------------------------------------------------
-instance PPrint (Ghc.MsgEnvelope Ghc.DecoratedSDoc) where
-  pprintTidy _ = text . show
 
 instance PPrint SourceError where
   pprintTidy _ = text . show
@@ -458,11 +455,11 @@
 filterReportErrors :: forall e' a. (Show e', F.PPrint e') => FilePath -> Ghc.TcRn a -> Ghc.TcRn a -> [Filter] -> F.Tidy -> [TError e'] -> Ghc.TcRn a
 filterReportErrors path failure continue filters k =
   filterReportErrorsWith
-    FilterReportErrorsArgs { msgReporter = Ghc.reportErrors
+    FilterReportErrorsArgs { errorReporter = \errs ->
+                               addTcRnUnknownMessages [(pos err, ppError k empty err) | err <- errs]
                            , filterReporter = defaultFilterReporter path
                            , failure = failure
                            , continue = continue
-                           , pprinter = \err -> mkLongErrAt (pos err) (ppError k empty err) mempty
                            , matchingFilters = reduceFilters renderer filters
                            , filters = filters
                            }
@@ -494,7 +491,7 @@
   FilterReportErrorsArgs
   {
     -- | Report the @msgs@ to the monad (usually IO)
-    msgReporter :: [msg] -> m ()
+    errorReporter :: [e] -> m ()
   ,
     -- | Report unmatched @filters@ to the monad
     filterReporter :: [filter] -> m ()
@@ -505,9 +502,6 @@
     -- | Continuation for when there are no unmatched errors or filters
     continue :: m a
   ,
-    -- | Compute a representation of the given error; does not report the error
-    pprinter :: e -> m msg
-  ,
     -- | Yields the filters that map a given error. Must only yield
     -- filters in the @filters@ field.
     matchingFilters :: e -> [filter]
@@ -533,15 +527,14 @@
         filterReporter unmatchedFilters
         failure
     else do
-      msgs <- traverse (pprinter . fst) unmatchedErrors
-      void $ msgReporter msgs
+      errorReporter $ map fst unmatchedErrors
       failure
 
 -- | Report errors via GHC's API stating the given `Filter`s did not get
 -- matched. Does nothing if the list of filters is empty.
 defaultFilterReporter :: FilePath -> [Filter] -> Ghc.TcRn ()
 defaultFilterReporter _ [] = pure ()
-defaultFilterReporter path fs = Ghc.reportError =<< mkLongErrAt srcSpan (vcat $ leaderMsg : (nest 4 <$> filterMsgs)) empty
+defaultFilterReporter path fs = addTcRnUnknownMessage srcSpan (vcat $ leaderMsg : (nest 4 <$> filterMsgs))
   where
     leaderMsg :: Doc
     leaderMsg = text "Could not match the following expected errors with actual thrown errors:"
diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs
--- a/src/Language/Haskell/Liquid/Types/RefType.hs
+++ b/src/Language/Haskell/Liquid/Types/RefType.hs
@@ -1721,8 +1721,8 @@
 -- Why do we return the strictness of the data-con arguments?
 -- Answer: see Note [Record evaluated-ness in worker/wrapper]
 deepSplitProductType fam_envs ty
-  | let (co, ty1) = topNormaliseType_maybe fam_envs ty
-                    `orElse` (mkRepReflCo ty, ty)
+  | let Reduction co ty1 = topNormaliseType_maybe fam_envs ty
+                    `orElse` Reduction (mkRepReflCo ty) ty
   , Just (tc, tc_args) <- splitTyConApp_maybe ty1
   , Just con <- tyConSingleDataCon_maybe tc
   , let arg_tys = dataConInstArgTys con tc_args
diff --git a/src/Language/Haskell/Liquid/Types/Specs.hs b/src/Language/Haskell/Liquid/Types/Specs.hs
--- a/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DerivingVia                #-}
+{-# LANGUAGE StandaloneDeriving         #-}
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 
@@ -76,7 +77,6 @@
 import qualified Data.HashMap.Strict     as M
 import           Data.HashMap.Strict     (HashMap)
 import           Language.Haskell.Liquid.Types.Types
-import           Language.Haskell.Liquid.Types.Generics
 import           Language.Haskell.Liquid.Types.Variance
 import           Language.Haskell.Liquid.Types.Bounds
 import           Liquid.GHC.API hiding (text, (<+>))
@@ -198,6 +198,7 @@
   , gsImps   :: ![(F.Symbol, F.Sort)]  -- ^ Imported Environment
   , gsConfig :: !Config
   }
+  deriving Show
 
 instance HasConfig TargetSpec where
   getConfig = gsConfig
@@ -209,6 +210,7 @@
   , gsLvars      :: !(S.HashSet Var)              -- ^ Variables that should be checked "lazily" in the environment they are used
   , gsCMethods   :: ![Var]                        -- ^ Refined Class methods
   }
+  deriving Show
 
 instance Semigroup GhcSpecVars where
   sv1 <> sv2 = SpVar
@@ -225,6 +227,7 @@
   { gsQualifiers :: ![F.Qualifier]                -- ^ Qualifiers in Source/Spec files e.g tests/pos/qualTest.hs
   , gsRTAliases  :: ![F.Located SpecRTAlias]      -- ^ Refinement type aliases (only used for qualifiers)
   }
+  deriving Show
 
 data GhcSpecSig = SpSig
   { gsTySigs   :: ![(Var, LocSpecType)]           -- ^ Asserted Reftypes
@@ -238,6 +241,7 @@
   , gsRelation :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
   , gsAsmRel   :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
   }
+  deriving Show
 
 instance Semigroup GhcSpecSig where
   x <> y = SpSig
@@ -270,6 +274,8 @@
   , gsMeasures   :: ![Measure SpecType DataCon]   -- ^ Measure definitions
   , gsUnsorted   :: ![UnSortedExpr]
   }
+  deriving Show
+
 data GhcSpecNames = SpNames
   { gsFreeSyms   :: ![(F.Symbol, Var)]            -- ^ List of `Symbol` free in spec and corresponding GHC var, eg. (Cons, Cons#7uz) from tests/pos/ex1.hs
   , gsDconsP     :: ![F.Located DataCon]          -- ^ Predicated Data-Constructors, e.g. see tests/pos/Map.hs
@@ -278,7 +284,11 @@
   , gsADTs       :: ![F.DataDecl]                 -- ^ ADTs extracted from Haskell 'data' definitions
   , gsTyconEnv   :: !TyConMap
   }
+  deriving Show
 
+deriving instance Show TyConP
+deriving instance Show TyConMap
+
 data GhcSpecTerm = SpTerm
   { gsStTerm     :: !(S.HashSet Var)              -- ^ Binders to CHECK by structural termination
   , gsAutosize   :: !(S.HashSet TyCon)            -- ^ Binders to IGNORE during termination checking
@@ -286,6 +296,7 @@
   , gsFail       :: !(S.HashSet (F.Located Var))    -- ^ Binders to fail type checking
   , gsNonStTerm  :: !(S.HashSet Var)              -- ^ Binders to CHECK using REFINEMENT-TYPES/termination metrics
   }
+  deriving Show
 
 instance Semigroup GhcSpecTerm where
   t1 <> t2 = SpTerm
@@ -309,6 +320,7 @@
   , gsRewrites     :: S.HashSet (F.Located Var)
   , gsRewritesWith :: M.HashMap Var [Var]
   }
+  deriving Show
 
 instance Semigroup GhcSpecRefl where
   x <> y = SpRefl
@@ -331,6 +343,7 @@
   { gsLawDefs :: ![(Class, [(Var, LocSpecType)])]
   , gsLawInst :: ![LawInstance]
   }
+  deriving Show
 
 data LawInstance = LawInstance
   { lilName   :: Class
@@ -339,6 +352,7 @@
   , lilEqus   :: [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
   , lilPos    :: SrcSpan
   }
+  deriving Show
 
 type VarOrLocSymbol = Either Var LocSymbol
 type BareMeasure   = Measure LocBareType F.LocSymbol
diff --git a/src/Language/Haskell/Liquid/Types/Types.hs b/src/Language/Haskell/Liquid/Types/Types.hs
--- a/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/src/Language/Haskell/Liquid/Types/Types.hs
@@ -293,7 +293,6 @@
 
 import qualified Language.Fixpoint.Types as F
 
-import           Language.Haskell.Liquid.Types.Generics
 import           Language.Haskell.Liquid.GHC.Misc
 import           Language.Haskell.Liquid.GHC.Logging as GHC
 import           Language.Haskell.Liquid.Types.Variance
@@ -1996,8 +1995,8 @@
 -- | Printing Warnings ---------------------------------------------------------
 --------------------------------------------------------------------------------
 
-printWarning :: Logger -> DynFlags -> Warning -> IO ()
-printWarning logger dyn (Warning srcSpan doc) = GHC.putWarnMsg logger dyn srcSpan doc
+printWarning :: Logger -> Warning -> IO ()
+printWarning logger (Warning srcSpan doc) = GHC.putWarnMsg logger srcSpan doc
 
 --------------------------------------------------------------------------------
 -- | Error Data Type -----------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/Types/Variance.hs b/src/Language/Haskell/Liquid/Types/Variance.hs
--- a/src/Language/Haskell/Liquid/Types/Variance.hs
+++ b/src/Language/Haskell/Liquid/Types/Variance.hs
@@ -24,7 +24,6 @@
 
 import qualified Language.Fixpoint.Types as F
 
-import           Language.Haskell.Liquid.Types.Generics
 import qualified Language.Haskell.Liquid.GHC.Misc as GM
 import           Liquid.GHC.API        as Ghc hiding (text)
 
diff --git a/src/Language/Haskell/Liquid/UX/DiffCheck.hs b/src/Language/Haskell/Liquid/UX/DiffCheck.hs
--- a/src/Language/Haskell/Liquid/UX/DiffCheck.hs
+++ b/src/Language/Haskell/Liquid/UX/DiffCheck.hs
@@ -540,7 +540,7 @@
 isCheckedRealSpan cm              = not . null . (`IM.search` cm) . srcSpanStartLine
 
 adjustSpan :: LMap -> SrcSpan -> Maybe SrcSpan
-adjustSpan lm (RealSrcSpan rsp _) = RealSrcSpan <$> adjustReal lm rsp <*> pure Nothing
+adjustSpan lm (RealSrcSpan rsp _) = RealSrcSpan <$> adjustReal lm rsp <*> pure strictNothing
 adjustSpan _  sp                  = Just sp
 
 adjustReal :: LMap -> RealSrcSpan -> Maybe RealSrcSpan