diff --git a/.circleci/config.yml b/.circleci/config.yml
index d9f39f6e6c..745ee6ca26 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -60,7 +60,7 @@ commands:
             chmod +x ./x86_64-linux-ghcup
             ./x86_64-linux-ghcup install ghc << parameters.ghc_version >>
             ./x86_64-linux-ghcup set ghc << parameters.ghc_version >>
-            ./x86_64-linux-ghcup install cabal 3.6.2.0
+            ./x86_64-linux-ghcup install cabal 3.10.1.0
             export PATH=~/.ghcup/bin:$PATH
             echo 'export PATH=~/.ghcup/bin:$PATH' >> $BASH_ENV
             << parameters.cabal_update_command >>
@@ -127,15 +127,18 @@ commands:
           command: |
             stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> clean
             mkdir -p /tmp/junit/stack
-            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> run test-driver
-            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> test tests:tasty
+            # the -package-db and -package arguments help work around https://github.com/commercialhaskell/stack/issues/6251
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> build liquidhaskell-boot
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> build liquidhaskell --ghc-options="\"-package-db $(stack path --snapshot-pkg-db)\"" --ghc-options="\"-package-db $(stack path --local-pkg-db)\"" --ghc-options="\"-package liquidhaskell-boot\""
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> run test-driver -- -- --ghc-options="\"-package-db $(stack path --snapshot-pkg-db)\"" --ghc-options="\"-package-db $(stack path --local-pkg-db)\"" --ghc-options="\"-package liquidhaskell\""
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> test tests:tasty --ghc-options="\"-package-db $(stack path --snapshot-pkg-db)\"" --ghc-options="\"-package-db $(stack path --local-pkg-db)\"" --ghc-options="\"-package liquidhaskell\""
             stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> test -j1 liquidhaskell-boot << parameters.extra_build_flags >>
           no_output_timeout: 30m
       - run:
           name: Generate haddock
           command: |
             # stack haddock liquidhaskell --flag liquidhaskell:-devel --no-haddock-deps --haddock-arguments="--no-print-missing-docs --odir=$CIRCLE_ARTIFACTS"
-            # skip if extra_build_flags are set
+            # skip if extra_build_flags are set--ghc-options
             [ ! -z "<< parameters.extra_build_flags >>" ] || stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> haddock << parameters.extra_build_flags >> liquidhaskell  --no-haddock-deps --haddock-arguments="--no-print-missing-docs"
       - run:
           name: Dist
@@ -158,7 +161,7 @@ jobs:
       image: ubuntu-2004:202107-02
     steps:
       - cabal_build_and_test:
-          ghc_version: "9.4.7"
+          ghc_version: "9.6.3"
 
 workflows:
   version: 2
diff --git a/README.md b/README.md
index fe7cd5c5cd..acad592b00 100644
--- a/README.md
+++ b/README.md
@@ -349,7 +349,7 @@ that can be tested with `./scripts/test/test_plugin.sh`.
 [typechecking phase]:  liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L211-L226
 [ghcide]:              https://github.com/haskell/ghcide
 [findRelevantSpecs]:   liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs#L65
-[core binds]:          https://hackage.haskell.org/package/ghc-9.4.7/docs/GHC-Core.html#t:CoreBind
+[core binds]:          https://hackage.haskell.org/package/ghc-9.6.3/docs/GHC-Core.html#t:CoreBind
 [configureGhcTargets]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L254
 [processTargetModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L483
 [processModule]:       liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L509
diff --git a/benchmark-timings/benchmark-timings.cabal b/benchmark-timings/benchmark-timings.cabal
index c0507eea01..63fcce4d48 100644
--- a/benchmark-timings/benchmark-timings.cabal
+++ b/benchmark-timings/benchmark-timings.cabal
@@ -37,7 +37,7 @@ executable benchmark-timings
                     , aeson >= 1.5.6 && < 3
                     , cassava ^>=0.5.2
                     , bytestring >=0.10.12 && <0.12
-                    , optparse-applicative >=0.16.1 && <0.18
+                    , optparse-applicative >=0.16.1 && <0.19
     ghc-options:    -Wall
     hs-source-dirs:   app
     default-language: Haskell2010
diff --git a/cabal.project b/cabal.project
index f78cf27112..29ecdcacc5 100644
--- a/cabal.project
+++ b/cabal.project
@@ -1,4 +1,4 @@
-with-compiler: ghc-9.4.7
+with-compiler: ghc-9.6.3
 
 packages: .
           ./liquid-fixpoint
diff --git a/docs/mkDocs/docs/install.md b/docs/mkDocs/docs/install.md
index 4ea62eeb72..88708246f2 100644
--- a/docs/mkDocs/docs/install.md
+++ b/docs/mkDocs/docs/install.md
@@ -19,7 +19,8 @@ LiquidHaskell itself is installed&enabled by adding it as a dependency in your p
 
 Depending on your version of GHC, you might want to use a build of LiquidHaskell from github or from Hackage.
 
-* `ghc-9.4.7`: use LiquidHaskell from github
+* `ghc-9.6.3`: use LiquidHaskell from github
+* `ghc-9.4.7`: use liquidhaskell-0.9.4.7.0 from Hackage
 * `ghc-9.2.8`: use liquidhaskell-0.9.2.8.0 from Hackage
 * `ghc-9.2.5`: use liquidhaskell-0.9.2.5.0 from Hackage
 * `ghc-9.0.2`: use liquidhaskell-0.9.0.2.1 and liquid-base-0.4.15.1.0 from Hackage
diff --git a/liquid-fixpoint b/liquid-fixpoint
index c253dc1932..b6c3e11ce1 160000
--- a/liquid-fixpoint
+++ b/liquid-fixpoint
@@ -1 +1 @@
-Subproject commit c253dc1932f06ed64fcc62d356f30256abaf83cd
+Subproject commit b6c3e11ce19629cced047eb2df748ec336148451
diff --git a/liquidhaskell-boot/liquidhaskell-boot.cabal b/liquidhaskell-boot/liquidhaskell-boot.cabal
index 6ddc514528..529dac392d 100644
--- a/liquidhaskell-boot/liquidhaskell-boot.cabal
+++ b/liquidhaskell-boot/liquidhaskell-boot.cabal
@@ -126,7 +126,7 @@ library
                     , aeson
                     , binary
                     , bytestring           >= 0.10
-                    , Cabal                < 3.9
+                    , Cabal                < 3.11
                     , cereal
                     , cmdargs              >= 0.10
                     , containers           >= 0.5
@@ -136,16 +136,16 @@ library
                     , filepath             >= 1.3
                     , fingertree           >= 0.1
                     , exceptions           < 0.11
-                    , ghc                  ^>= 9.4
+                    , ghc                  ^>= 9.6
                     , 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
+                    , optparse-applicative < 0.19
                     , githash
                     , megaparsec           >= 8
                     , pretty               >= 1.1
diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
index 1c49fae008..3a21015811 100644
--- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
+++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
@@ -10,6 +10,7 @@ it easy to discover breaking changes in the GHC API.
 
 -}
 
+{-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PatternSynonyms #-}
 
 module Liquid.GHC.API (
@@ -19,8 +20,7 @@ module Liquid.GHC.API (
 import Liquid.GHC.API.Extra as Ghc
 
 import           GHC                  as Ghc
-    ( Backend(Interpreter)
-    , Class
+    ( Class
     , DataCon
     , DesugaredModule(DesugaredModule, dm_typechecked_module, dm_core_module)
     , DynFlags(backend, debugLevel, ghcLink, ghcMode)
@@ -102,7 +102,6 @@ import           GHC                  as Ghc
     , isDictonaryId
     , isExternalName
     , isFamilyTyCon
-    , isFunTyCon
     , isGoodSrcSpan
     , isLocalId
     , isNewTyCon
@@ -216,7 +215,8 @@ import GHC.Builtin.Types              as Ghc
     , typeSymbolKind
     )
 import GHC.Builtin.Types.Prim         as Ghc
-    ( eqPrimTyCon
+    ( isArrowTyCon
+    , eqPrimTyCon
     , eqReprPrimTyCon
     , primTyCons
     )
@@ -322,8 +322,8 @@ 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)
+    ( FunTyFlag(FTF_T_T)
+    , ForAllTyFlag(Required)
     , Coercion
         ( AppCo
         , AxiomRuleCo
@@ -331,10 +331,13 @@ import GHC.Core.TyCo.Rep              as Ghc
         , CoVarCo
         , ForAllCo
         , FunCo
+        , HoleCo
         , InstCo
         , KindCo
         , LRCo
-        , NthCo
+        , Refl
+        , GRefl
+        , SelCo
         , SubCo
         , SymCo
         , TransCo
@@ -355,12 +358,12 @@ import GHC.Core.TyCo.Rep              as Ghc
         , ft_res
         )
     , UnivCoProvenance(PhantomProv, ProofIrrelProv)
-    , binderVar
     , mkForAllTys
     , mkFunTy
     , mkTyVarTy
     , mkTyVarTys
     )
+import GHC.Core.TyCo.Compare          as Ghc (eqType, nonDetCmpType)
 import GHC.Core.TyCon                 as Ghc
     ( TyConBinder
     , TyConBndrVis(AnonTCB)
@@ -382,20 +385,18 @@ import GHC.Core.TyCon                 as Ghc
 import GHC.Core.Type                  as Ghc
     ( Specificity(SpecifiedSpec)
     , TyVarBinder
-    , pattern Many
-    , classifiesTypeWithValues
+    , isTYPEorCONSTRAINT
     , dropForAlls
     , emptyTvSubstEnv
-    , eqType
     , expandTypeSynonyms
     , irrelevantMult
     , isFunTy
     , isTyVar
     , isTyVarTy
+    , pattern ManyTy
     , mkTvSubstPrs
     , mkTyConApp
     , newTyConInstRhs
-    , nonDetCmpType
     , piResultTys
     , splitAppTys
     , splitFunTy_maybe
@@ -421,14 +422,16 @@ import GHC.Data.FastString            as Ghc
     , fsLit
     , mkFastString
     , mkFastStringByteString
-    , mkPtrString
+    , mkPtrString#
     , uniq
     , unpackFS
     )
 import GHC.Data.Pair                  as Ghc
     ( Pair(Pair) )
 import GHC.Driver.Config.Diagnostic as Ghc
-    ( initDiagOpts )
+    ( initDiagOpts
+    , initDsMessageOpts
+    )
 import GHC.Driver.Main                as Ghc
     ( hscDesugar
     , hscTcRcLookupName
@@ -460,6 +463,7 @@ import GHC.Plugins                    as Ghc ( deserializeWithData
 import GHC.Core.FVs                   as Ghc (exprFreeVarsList)
 import GHC.Core.Opt.OccurAnal         as Ghc
     ( occurAnalysePgm )
+import GHC.Driver.Backend             as Ghc (interpreterBackend)
 import GHC.Driver.Env                 as Ghc
     ( HscEnv(hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins) )
 import GHC.Driver.Errors              as Ghc
@@ -477,7 +481,7 @@ import GHC.Iface.Load                 as Ghc
 import GHC.Rename.Expr                as Ghc (rnLExpr)
 import GHC.Rename.Names               as Ghc (renamePkgQual)
 import GHC.Tc.Errors.Types            as Ghc
-    ( TcRnMessage(TcRnUnknownMessage) )
+    ( mkTcRnUnknownMessage )
 import GHC.Tc.Gen.App                 as Ghc (tcInferSigma)
 import GHC.Tc.Gen.Bind                as Ghc (tcValBinds)
 import GHC.Tc.Gen.Expr                as Ghc (tcInferRho)
@@ -549,6 +553,7 @@ import GHC.Types.CostCentre           as Ghc
 import GHC.Types.Error                as Ghc
     ( Messages(getMessages)
     , MessageClass(MCDiagnostic)
+    , Diagnostic(defaultDiagnosticOpts)
     , DiagnosticReason(WarningWithoutFlag)
     , MsgEnvelope(errMsgSpan)
     , errorsOrFatalWarningsFound
@@ -653,6 +658,7 @@ import GHC.Types.Unique.Supply        as Ghc
     ( MonadUnique, getUniqueM )
 import GHC.Types.Var                  as Ghc
     ( VarBndr(Bndr)
+    , binderVar
     , mkLocalVar
     , mkTyVar
     , setVarName
diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs
index 9946701917..245c4b5936 100644
--- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs
+++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs
@@ -82,7 +82,7 @@ tyConRealArity tc = go 0 (tyConKind tc)
   where
     go :: Int -> Kind -> Int
     go !acc k =
-      case asum [fmap (\(_, _, c) -> c) (splitFunTy_maybe k), fmap snd (splitForAllTyCoVar_maybe k)] of
+      case asum [fmap (\(_, _, _, c) -> c) (splitFunTy_maybe k), fmap snd (splitForAllTyCoVar_maybe k)] of
         Nothing -> acc
         Just ks -> go (acc + 1) ks
 
@@ -192,7 +192,7 @@ data ApiComment
 apiComments :: ParsedModule -> [Ghc.Located ApiComment]
 apiComments pm = apiCommentsParsedSource (pm_parsed_source pm)
 
-apiCommentsParsedSource :: Located HsModule -> [Ghc.Located ApiComment]
+apiCommentsParsedSource :: Located (HsModule GhcPs) -> [Ghc.Located ApiComment]
 apiCommentsParsedSource ps =
     let hs = unLoc ps
         go :: forall a. Data a => a -> [LEpaComment]
@@ -281,7 +281,7 @@ showSDocQualified = Ghc.renderWithContext ctx
     style = Ghc.mkUserStyle myQualify Ghc.AllTheWay
     ctx = Ghc.defaultSDocContext { sdocStyle = style }
 
-myQualify :: Ghc.PrintUnqualified
+myQualify :: Ghc.NamePprCtx
 myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames }
 -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 }
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
index 862ec5b1e7..3f62e8222e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
@@ -21,6 +21,7 @@ module Language.Haskell.Liquid.Bare.DataType
   ) where
 
 import qualified Control.Exception                      as Ex
+import           Control.Monad (forM, unless)
 import           Control.Monad.Reader
 import qualified Data.List                              as L
 import qualified Data.HashMap.Strict                    as M
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs
index 3c90c6eeae..cc3ef1f74f 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs
@@ -17,6 +17,7 @@ import           Prelude                               hiding (error)
 
 import           Liquid.GHC.API       as Ghc  hiding (Located, showPpr)
 
+import           Control.Monad                         (zipWithM_)
 import           Control.Monad.Except                  (MonadError, throwError)
 import           Control.Monad.State
 import qualified Data.Maybe                            as Mb --(fromMaybe, isNothing)
@@ -152,7 +153,7 @@ mapTyVars _ hsT lqT
        throwError (err (F.pprint hsT) (F.pprint lqT))
 
 isKind :: Kind -> Bool
-isKind = classifiesTypeWithValues -- TODO:GHC-863 isStarKind k --  typeKind k
+isKind = isTYPEorCONSTRAINT -- TODO:GHC-863 isStarKind k --  typeKind k
 
 
 mapTyRVar :: MonadError Error m
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
index 4dc9f0bcc0..78bb237c46 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
@@ -140,7 +140,7 @@ plugMany allowTC embs tyi ldcp (hsAs, hsArgs, hsRes) (lqAs, lqArgs, lqRes)
   where
     ((xs,_,ts,_), t) = bkArrow (val pT)
     pT               = plugHoles allowTC (Bare.LqTV dcName) embs tyi (const killHoles) hsT (F.atLoc ldcp lqT)
-    hsT              = foldr (Ghc.mkFunTy Ghc.VisArg Ghc.Many) hsRes hsArgs'
+    hsT              = foldr (Ghc.mkFunTy Ghc.FTF_T_T Ghc.ManyTy) hsRes hsArgs'
     lqT              = foldr (uncurry (rFun' (classRFInfo allowTC))) lqRes lqArgs'
     hsArgs'          = [ Ghc.mkTyVarTy a               | a <- hsAs] ++ hsArgs
     lqArgs'          = [(F.dummySymbol, RVar a mempty) | a <- lqAs] ++ lqArgs
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
index f020d15c4a..5addf63909 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
@@ -183,11 +183,35 @@ makeSymMap src = Misc.group [ (sym, (m, x))
 
 makeTyThingMap :: GhcSrc -> TyThingMap
 makeTyThingMap src =
+  addListTyConName $
   Misc.group [ (x, (m, t))  | t         <- srcThings src
                             , tSym      <- Mb.maybeToList (tyThingSymbol t)
                             , let (m, x) = qualifiedSymbol tSym
                             , not (isLocal m)
              ]
+  where
+    -- We add the TyThing for the List constructor here. Otherwise, we
+    -- lookups in the TyThingMap will fail for "List" and not for "[]".
+    addListTyConName m =
+      case M.lookup "[]" m of
+        Nothing -> m
+        Just ps -> M.insertWith (++) "List" (filterListTyCon ps) m
+
+    -- The TyCon name in the TyThing for @"[]"@ must be @"[]"@ apparently.
+    --
+    -- listTyCon uses "List", and that made later checks fail for some tests,
+    -- so we cannot just return @[("GHC.Types", ATyCon listTyCon)]@
+    --
+    -- Returning the TyCon that GHC yields for @"[]"@ has later tests fail,
+    -- because that TyCon has no associated data constructors.
+    --
+    -- The solution we adopted for now is to return listTyCon, and use
+    -- the name from the TyThing that GHC returned.
+    filterListTyCon ps =
+      [ (mn, Ghc.ATyCon tc') | (mn, Ghc.ATyCon tc) <- ps
+          , "GHC.Types" == mn
+          , let tc' = Ghc.listTyCon { Ghc.tyConName = Ghc.tyConName tc }
+      ]
 
 tyThingSymbol :: Ghc.TyThing -> Maybe F.Symbol
 tyThingSymbol (Ghc.AnId     x) = Just (F.symbol x)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs
index f051e85b59..828b6f1bc7 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs
@@ -49,6 +49,7 @@ module Language.Haskell.Liquid.Constraint.Env (
 import Prelude hiding (error)
 -- import Outputable
 -- import FastString (fsLit)
+import Control.Monad (foldM, msum)
 import Control.Monad.State
 
 -- import           GHC.Err.Located hiding (error)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
index 2309977870..d1d6f63228 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -27,6 +27,7 @@ import qualified Language.Haskell.Liquid.GHC.Resugar           as Rs
 import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
 import qualified Language.Haskell.Liquid.GHC.Misc              as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr )
 import Text.PrettyPrint.HughesPJ ( text )
+import           Control.Monad ( foldM, forM, forM_, when, void )
 import           Control.Monad.State
 import           Data.Maybe                                    (fromMaybe, isJust, mapMaybe)
 import           Data.Either.Extra                             (eitherToMaybe)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs
index 228082d027..1b4527d6f0 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs
@@ -15,6 +15,7 @@ module Language.Haskell.Liquid.Constraint.Init (
     ) where
 
 import           Prelude                                       hiding (error, undefined)
+import           Control.Monad (foldM, forM)
 import           Control.Monad.State
 import           Data.Maybe                                    (isNothing, fromMaybe, catMaybes, mapMaybe)
 import qualified Data.HashMap.Strict                           as M
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Relational.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Relational.hs
index 668e21fbd0..7a09a7b237 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Relational.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Relational.hs
@@ -13,7 +13,7 @@
 
 module Language.Haskell.Liquid.Constraint.Relational (consAssmRel, consRelTop) where
 
-import           Control.Monad.State
+import           Control.Monad (foldM, forM_)
 import           Data.Bifunctor                                 ( Bifunctor(bimap) )
 import qualified Data.HashMap.Strict                            as M
 import qualified Data.List                                      as L
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs
index bc53081de8..6e2091a396 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs
@@ -19,8 +19,8 @@ import qualified Data.List                          as L
 import qualified Data.HashSet                       as S
 import qualified Data.Traversable                   as T
 import qualified Data.HashMap.Strict                as M
-import           Control.Applicative (liftA2)
-import           Control.Monad.State ( gets, forM, foldM )
+import           Control.Monad ( foldM, forM )
+import           Control.Monad.State ( gets )
 import           Text.PrettyPrint.HughesPJ ( (<+>), text )
 import qualified Language.Haskell.Liquid.GHC.Misc                    as GM
 import qualified Language.Fixpoint.Types            as F
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Logging.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Logging.hs
index ef97354e02..e18bfb09d0 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Logging.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Logging.hs
@@ -34,14 +34,14 @@ putLogMsg :: GHC.Logger
           -> PJ.Doc
           -> IO ()
 putLogMsg logger sev srcSpan _mbStyle =
-  GHC.putLogMsg logger (GHC.logFlags logger) (GHC.MCDiagnostic sev GHC.WarningWithoutFlag) srcSpan . GHC.text . PJ.render
+  GHC.putLogMsg logger (GHC.logFlags logger) (GHC.MCDiagnostic sev GHC.WarningWithoutFlag Nothing) srcSpan . GHC.text . PJ.render
 
 putWarnMsg :: GHC.Logger -> GHC.SrcSpan -> PJ.Doc -> IO ()
 putWarnMsg logger srcSpan doc =
   putLogMsg logger GHC.SevWarning srcSpan (Just GHC.defaultErrStyle) doc
 
 addTcRnUnknownMessage :: GHC.SrcSpan -> PJ.Doc -> GHC.TcRn ()
-addTcRnUnknownMessage srcSpan = GHC.addErrAt srcSpan . GHC.TcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc
+addTcRnUnknownMessage srcSpan = GHC.addErrAt srcSpan . GHC.mkTcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc
 
 addTcRnUnknownMessages :: [(GHC.SrcSpan, PJ.Doc)] -> GHC.TcRn ()
-addTcRnUnknownMessages = GHC.addErrs . map (fmap (GHC.TcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc))
+addTcRnUnknownMessages = GHC.addErrs . map (fmap (GHC.mkTcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc))
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs
index ec0deb77cb..189da0d25e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE FlexibleContexts          #-}
 {-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE MagicHash                 #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE RankNTypes                #-}
 {-# LANGUAGE TupleSections             #-}
@@ -25,12 +26,8 @@ import qualified Data.List as L
 import           Debug.Trace
 
 import           Prelude                                    hiding (error)
-import           Liquid.GHC.API            as Ghc hiding ( L
-                                                                          , sourceName
-                                                                          , showPpr
-                                                                          , panic
-                                                                          , showSDoc
-                                                                          )
+import           Liquid.GHC.API            as Ghc hiding
+  (L, line, sourceName, showPpr, panic, showSDoc)
 import qualified Liquid.GHC.API            as Ghc (GenLocated (L), showSDoc, panic)
 
 
@@ -89,7 +86,7 @@ stringTyVar s = mkTyVar name liftedTypeKind
 
 -- FIXME: reusing uniques like this is really dangerous
 stringVar :: String -> Type -> Var
-stringVar s t = mkLocalVar VanillaId name Many t vanillaIdInfo
+stringVar s t = mkLocalVar VanillaId name ManyTy t vanillaIdInfo
    where
       name = mkInternalName (mkUnique 'x' 25) occ noSrcSpan
       occ  = mkVarOcc s
@@ -195,7 +192,7 @@ showPpr = Ghc.showPprQualified
 showSDoc :: Ghc.SDoc -> String
 showSDoc = Ghc.showSDocQualified
 
-myQualify :: Ghc.PrintUnqualified
+myQualify :: Ghc.NamePprCtx
 myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames }
 -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 }
 
@@ -403,7 +400,7 @@ lookupRdrName hsc_env mod_name rdr_name = do
 -- XXX                        [gre] -> return (Just (gre_name gre))
                         []    -> return Nothing
                         _     -> Ghc.panic "lookupRdrNameInModule"
-                Nothing -> throwCmdLineErrorS dflags $ Ghc.hsep [Ghc.ptext (Ghc.mkPtrString "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'
@@ -458,7 +455,7 @@ tyConTyVarsDef c
   --  none         = tracepp ("tyConTyVarsDef: " ++ show c) (noTyVars c)
 
 noTyVars :: TyCon -> Bool
-noTyVars c =  Ghc.isPrimTyCon c || isFunTyCon c || Ghc.isPromotedDataCon c
+noTyVars c =  Ghc.isPrimTyCon c || Ghc.isPromotedDataCon c
 
 --------------------------------------------------------------------------------
 -- | Symbol Instances
@@ -879,7 +876,8 @@ elabRnExpr rdr_expr = do
 
     logger <- getLogger
     diag_opts <- initDiagOpts <$> getDynFlags
-    liftIO $ printMessages logger diag_opts ds_msgs
+    print_config <- initDsMessageOpts <$> getDynFlags
+    liftIO $ printMessages logger print_config diag_opts ds_msgs
 
     case me of
       Nothing -> failM
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index d1806028a1..13ce00f584 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -190,7 +190,7 @@ instance Unoptimise DynFlags where
   unoptimise df = updOptLevel 0 df
     { debugLevel   = 1
     , ghcLink      = LinkInMemory
-    , backend      = Interpreter
+    , backend      = interpreterBackend
     , ghcMode      = CompManager
     }
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
index 66aa9d4adf..a6f2cffc34 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
@@ -92,7 +92,7 @@ findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do
           eps2 <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv)
           -- now look up the assumptions
           liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assumptionsMod
-        FoundMultiple{} -> failWithTc $ TcRnUnknownMessage $ mkPlainError [] $
+        FoundMultiple{} -> failWithTc $ mkTcRnUnknownMessage $ mkPlainError [] $
                              cannotFindModule hscEnv assumptionsModName res
         _ -> return Nothing
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/TypeRep.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/TypeRep.hs
index 4012ea6e6a..9c8bd5303e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/TypeRep.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/TypeRep.hs
@@ -115,8 +115,8 @@ substCoercion x tx (TyConAppCo r c cs)
   = TyConAppCo (subst x tx r) c (subst x tx <$> cs)
 substCoercion x tx (AppCo c1 c2)
   = AppCo (subst x tx c1) (subst x tx c2)
-substCoercion x tx (FunCo r cN c1 c2)
-  = FunCo r cN (subst x tx c1) (subst x tx c2) -- TODO(adinapoli) Is this the correct substitution?
+substCoercion x tx (FunCo r afl afr cN c1 c2)
+  = FunCo r afl afr cN (subst x tx c1) (subst x tx c2) -- TODO(adinapoli) Is this the correct substitution?
 substCoercion x tx (ForAllCo y c1 c2)
   | symbol x == symbol y 
   = ForAllCo y c1 c2
@@ -134,8 +134,8 @@ substCoercion x tx (TransCo c1 c2)
   = TransCo (subst x tx c1) (subst x tx c2)
 substCoercion x tx (AxiomRuleCo ca cs)
   = AxiomRuleCo (subst x tx ca)  (subst x tx <$> cs)  
-substCoercion x tx (NthCo r i c)
-  = NthCo r i (subst x tx c)
+substCoercion x tx (SelCo i c)
+  = SelCo i (subst x tx c)
 substCoercion x tx (LRCo i c)
   = LRCo i (subst x tx c)
 substCoercion x tx (InstCo c1 c2)
@@ -144,6 +144,12 @@ substCoercion x tx (KindCo c)
   = KindCo (subst x tx c)
 substCoercion x tx (SubCo c)
   = SubCo (subst x tx c)
+substCoercion _x _tx (Refl t)
+  = Refl t
+substCoercion _x _tx (GRefl r t c)
+  = GRefl r t c
+substCoercion _x _tx (HoleCo c)
+  = HoleCo c
 
 instance SubstTy Role where
 instance SubstTy (CoAxiom Branched) where
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs
index 6d53350c0a..5285784978 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs
@@ -19,6 +19,7 @@ import           Liquid.GHC.API  as Ghc hiding ( mkTyArg
                                                                 , DsM
                                                                 , panic)
 import qualified Liquid.GHC.API  as Ghc
+import           Control.Monad (forM)
 import           Control.Monad.State.Lazy
 import           System.Console.CmdArgs.Verbosity (whenLoud)
 import qualified Language.Fixpoint.Types    as F
@@ -366,7 +367,7 @@ freshNormalVar γ t = do
   u     <- getUniqueM
   let i  = getKey u
   let sp = Sp.srcSpan (aeSrcSpan γ)
-  return (mkUserLocal (anfOcc i) u Ghc.Many t sp)
+  return (mkUserLocal (anfOcc i) u Ghc.ManyTy t sp)
 
 anfOcc :: Int -> OccName
 anfOcc = mkVarOccFS . GM.symbolFastString . F.intSymbol F.anfPrefix
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rec.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rec.hs
index ea3478a1c2..b4327957ee 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rec.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rec.hs
@@ -208,7 +208,7 @@ mkFreshIds tvs origIds var
        let x' = setVarType var t
        return (ids'', x')
   where
-    mkType ids ty = foldl (\t x -> FunTy VisArg Many (varType x) t) ty ids -- FIXME(adinapoli): Is 'VisArg' OK here?
+    mkType ids ty = foldl (\t x -> FunTy FTF_T_T ManyTy (varType x) t) ty ids -- FIXME(adinapoli): Is 'VisArg' OK here?
 
 -- NOTE [Don't choose transform-rec binders as decreasing params]
 -- --------------------------------------------------------------
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs
index 8d1f0b1ab3..d977f39f3e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs
@@ -27,6 +27,7 @@ module Language.Haskell.Liquid.Transforms.Rewrite
 import           Liquid.GHC.API as Ghc hiding (showPpr, substExpr)
 import           Language.Haskell.Liquid.GHC.TypeRep ()
 import           Data.Maybe     (fromMaybe)
+import           Control.Monad (msum)
 import           Control.Monad.State hiding (lift)
 import           Language.Fixpoint.Misc       ({- mapFst, -}  mapSnd)
 import qualified          Language.Fixpoint.Types as F
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Bounds.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Bounds.hs
index c8b26d9aa9..fee6253bd6 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Bounds.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Bounds.hs
@@ -70,9 +70,12 @@ instance (PPrint e, PPrint t) => (PPrint (Bound t e)) where
       ppBsyms _ [] = ""
       ppBsyms k' xs = "\\" <+> pprintTidy k' xs <+> "->"
 
+instance Functor (Bound a) where
+  fmap f (Bound s vs ps xs e) = Bound s vs ps xs (f e)
+
 instance Bifunctor Bound where
   first  f (Bound s vs ps xs e) = Bound s (f <$> vs) (Misc.mapSnd f <$> ps) (Misc.mapSnd f <$> xs) e
-  second f (Bound s vs ps xs e) = Bound s vs ps xs (f e)
+  second = fmap
 
 makeBound :: (PPrint r, UReftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r)
           => RRBound RSort -> [RRType r] -> [F.Symbol] -> RRType r -> RRType r
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Equality.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Equality.hs
index 031bec9623..55de8d39d5 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Equality.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Equality.hs
@@ -8,6 +8,7 @@ import qualified Language.Fixpoint.Types as F
 import           Language.Haskell.Liquid.Types
 import qualified Liquid.GHC.API as Ghc
 
+import Control.Monad (liftM2, zipWithM)
 import Control.Monad.Writer.Lazy
 -- import Control.Monad
 import qualified Data.List as L
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs
index 8bc31eb1df..8e948f3edf 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs
@@ -5,6 +5,8 @@
 {-# LANGUAGE DeriveDataTypeable  #-}
 {-# LANGUAGE DeriveFunctor       #-}
 {-# LANGUAGE DerivingVia         #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.
 {-# OPTIONS_GHC -Wno-orphans #-} -- PPrint and aeson instances.
@@ -1084,6 +1086,7 @@ sourceErrors :: String -> SourceError -> [TError t]
 sourceErrors s =
   concatMap errMsgErrors . bagToList . getMessages . srcErrorMessages
   where
+    errMsgErrors :: forall e t. Diagnostic e => MsgEnvelope e -> [TError t]
     errMsgErrors e = [ ErrGhc (errMsgSpan e) msg ]
       where
-        msg = text s $+$ nest 4 (text $ showSDocQualified (pprLocMsgEnvelope e))
+        msg = text s $+$ nest 4 (text $ showSDocQualified (pprLocMsgEnvelope (defaultDiagnosticOpts @e) e))
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs
index 7c19c74689..12c91cf24b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs
@@ -1479,10 +1479,10 @@ toType  :: (ToTypeable r) => Bool -> RRType r -> Type
 toType useRFInfo (RFun _ RFInfo{permitTC = permitTC} t@(RApp c _ _ _) t' _)
   | useRFInfo && isErasable c = toType useRFInfo t'
   | otherwise
-  = FunTy VisArg Many (toType useRFInfo t) (toType useRFInfo t')
+  = FunTy FTF_T_T ManyTy (toType useRFInfo t) (toType useRFInfo t')
   where isErasable = if permitTC == Just True then isEmbeddedDict else isClass
 toType useRFInfo (RFun _ _ t t' _)
-  = FunTy VisArg Many (toType useRFInfo t) (toType useRFInfo t')
+  = FunTy FTF_T_T ManyTy (toType useRFInfo t) (toType useRFInfo t')
 toType useRFInfo (RAllT a t _) | RTV α <- ty_var_value a
   = ForAllTy (Bndr α Required) (toType useRFInfo t)
 toType useRFInfo (RAllP _ t)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index 8227b943af..6de4e157dc 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -890,8 +890,8 @@ instance (B.Binary s)              => B.Binary (RTVInfo s)
 --   directly to any type and has semantics _independent of_ the data-type.
 
 data Ref τ t = RProp
-  { rf_args :: [(Symbol, τ)]
-  , rf_body :: t -- ^ Abstract refinement associated with `RTyCon`
+  { rf_args :: [(Symbol, τ)] -- ^ arguments. e.g. @h@ in the above example
+  , rf_body :: t -- ^ Abstract refinement associated with `RTyCon`. e.g. @v > h@ in the above example
   } deriving (Eq, Generic, Data, Typeable, Functor)
     deriving Hashable via Generically (Ref τ t)
 
@@ -996,7 +996,7 @@ type OkRT c tv r = ( TyConable c
 -------------------------------------------------------------------------------
 
 instance TyConable RTyCon where
-  isFun      = isFunTyCon . rtc_tc
+  isFun      = isArrowTyCon . rtc_tc
   isList     = (listTyCon ==) . rtc_tc
   isTuple    = Ghc.isTupleTyCon   . rtc_tc
   isClass    = isClass . rtc_tc -- isClassRTyCon
@@ -1012,7 +1012,7 @@ instance TyConable RTyCon where
 
 
 instance TyConable TyCon where
-  isFun      = isFunTyCon
+  isFun      = isArrowTyCon
   isList     = (listTyCon ==)
   isTuple    = Ghc.isTupleTyCon
   isClass c  = isClassTyCon c   || isEqual c -- c == eqPrimTyCon
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/DiffCheck.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/DiffCheck.hs
index 50598d1fc8..7da4dacd36 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/DiffCheck.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/DiffCheck.hs
@@ -54,12 +54,8 @@ import           Language.Fixpoint.Utils.Files
 import           Language.Fixpoint.Solver.Stats ()
 import           Language.Haskell.Liquid.Misc           (mkGraph)
 import           Language.Haskell.Liquid.GHC.Misc
-import           Liquid.GHC.API        as Ghc hiding ( Located
-                                                                      , sourceName
-                                                                      , text
-                                                                      , panic
-                                                                      , showPpr
-                                                                      )
+import           Liquid.GHC.API        as Ghc hiding
+  (Located, line, sourceName, text, panic, showPpr)
 import           Text.PrettyPrint.HughesPJ              (text, render, Doc)
 import qualified Data.ByteString                        as B
 import qualified Data.ByteString.Lazy                   as LB
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
index d592de671b..91549eec4b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
@@ -30,7 +30,7 @@ import Prelude                                hiding (error)
 -- import Language.Fixpoint.Misc           (mapSnd)
 import Language.Haskell.Liquid.GHC.Misc
 import qualified Liquid.GHC.API as Ghc
-import Liquid.GHC.API (Var, Arity, TyVar, Bind(..), Boxity(..), Expr(..), ArgFlag(..))
+import Liquid.GHC.API (Var, Arity, TyVar, Bind(..), Boxity(..), Expr(..), ForAllTyFlag(Required))
 import Language.Haskell.Liquid.Types.Types
 import Language.Haskell.Liquid.Types.RefType
 import Language.Haskell.Liquid.Types.Variance
diff --git a/scripts/plot-performance/plot-performance.cabal b/scripts/plot-performance/plot-performance.cabal
index 35cc315006..08dcc8b8a3 100644
--- a/scripts/plot-performance/plot-performance.cabal
+++ b/scripts/plot-performance/plot-performance.cabal
@@ -44,7 +44,7 @@ executable plot-performance
                     , data-default-class
                     , directory
                     , lens
-                    , optparse-applicative >=0.16.1 && <0.18
+                    , optparse-applicative >=0.16.1 && <0.19
                     , vector
     ghc-options:    -Wall
     hs-source-dirs:   app
diff --git a/scripts/profiling-driver/profiling-driver.cabal b/scripts/profiling-driver/profiling-driver.cabal
index fe71436c71..3efa50c422 100644
--- a/scripts/profiling-driver/profiling-driver.cabal
+++ b/scripts/profiling-driver/profiling-driver.cabal
@@ -14,7 +14,7 @@ maintainer:         Facundo Domínguez <jhala@tweag.io>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
 build-type:         Simple
-tested-with:        GHC == 9.4.7
+tested-with:        GHC == 9.6.3
 
 source-repository head
   type:     git
@@ -29,7 +29,7 @@ flag devel
 executable profiling-driver
   main-is:          ProfilingDriver.hs
   build-depends:    base            >= 4.8.1.0 && < 5
-                  , ghc             ^>= 9.4
+                  , ghc             ^>= 9.6
                   , ghc-paths
   default-language: Haskell2010
   ghc-options:      -W
diff --git a/stack.yaml b/stack.yaml
index 61ef3b461c..880a8963e3 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -22,14 +22,13 @@ packages:
 - benchmark-timings
 - .
 extra-deps:
-- rest-rewrite-0.4.1
-- smtlib-backends-0.3
-- smtlib-backends-process-0.3
+- smtlib-backends-0.3@rev:1
+- smtlib-backends-process-0.3@rev:1
 - git: https://github.com/qnikst/ghc-timings-report
   commit: 45ef3498e35897712bde8e002ce18df6d55f8b15
 
-resolver: lts-21.20
+resolver: nightly-2023-11-27
 
 nix:
-  packages: [cacert, git, hostname, z3]
+  packages: [cacert, git, hostname, nix, stack, z3]
   path: [nixpkgs=./nixpkgs.nix]
diff --git a/stack.yaml.lock b/stack.yaml.lock
index f4854060a5..5089af3dce 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -5,26 +5,19 @@
 
 packages:
 - completed:
-    hackage: rest-rewrite-0.4.1@sha256:1254960c0a595cf4c9d5a3b986f42644407c63c74578d75b3568a6a12e5143f0,3886
+    hackage: smtlib-backends-0.3@sha256:69977f97a8db2c11e97bde92fff7e86e793c1fb23827b284bf89938ee463fbf0,1211
     pantry-tree:
-      sha256: 17b4e99420cc1929e2b7d29558a0f909d6fcabd263fbc590dbf2585f893f5a6e
-      size: 4018
-  original:
-    hackage: rest-rewrite-0.4.1
-- completed:
-    hackage: smtlib-backends-0.3@sha256:917d88540a9ede7beedbe2ed13b492acddbce394d30ccf5d0ef4f4fba9aa2c12,1157
-    pantry-tree:
-      sha256: 59b578ae7df155a6c73a513358370747e3cc6229ebb44adaba9e0935f811539c
+      sha256: d7c614eab0f3f256b22724ca2d7ac41651f22209242af1d24f052f41d7a7541f
       size: 275
   original:
-    hackage: smtlib-backends-0.3
+    hackage: smtlib-backends-0.3@rev:1
 - completed:
-    hackage: smtlib-backends-process-0.3@sha256:d4d7d02859383e0a43db2d8ce7ef01deffe1bcd356b2ff8626925c3a1c8db922,1600
+    hackage: smtlib-backends-process-0.3@sha256:3eee93e91f41c8a2fb2699e95b502a24d8053485ccf7749e2766683d1ebfe11d,1676
     pantry-tree:
-      sha256: d7d8ec52d07f4a59614000fd93d77b109d085d58f2d96e2c4b972f541c4e8287
+      sha256: 579580c8067b4c6640261187fc5d2ac0a02923db4633e0027067de72f947083c
       size: 461
   original:
-    hackage: smtlib-backends-process-0.3
+    hackage: smtlib-backends-process-0.3@rev:1
 - completed:
     commit: 45ef3498e35897712bde8e002ce18df6d55f8b15
     git: https://github.com/qnikst/ghc-timings-report
@@ -36,16 +29,9 @@ packages:
   original:
     commit: 45ef3498e35897712bde8e002ce18df6d55f8b15
     git: https://github.com/qnikst/ghc-timings-report
-- completed:
-    hackage: strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628
-    pantry-tree:
-      sha256: cf7712453587e8ea69b96f33e2e8015c22d3b448259d4cace663cc15657309d7
-      size: 671
-  original:
-    hackage: strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628
 snapshots:
 - completed:
-    sha256: 5921ddc75f5dd3f197fbc32e1e5676895a8e7b971d4f82ef6b556657801dd18a
-    size: 640054
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/21/20.yaml
-  original: lts-21.20
+    sha256: c067098ea221c83ce03ccae4cfd5b104fb8a689b17ebb15dbe9d0793e9db4329
+    size: 699418
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2023/11/27.yaml
+  original: nightly-2023-11-27
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Check.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Check.hs
index 6b261b02ec..7b560cfab6 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Check.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Check.hs
@@ -30,7 +30,9 @@ import Language.Stitch.LH.Type
 import Language.Stitch.LH.Op
 import Language.Stitch.LH.Pretty
 import Language.Stitch.LH.Unchecked
-import Text.PrettyPrint.ANSI.Leijen
+import Language.Stitch.LH.Util
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
 
 {-@
@@ -68,8 +70,8 @@ data Exp
 {-@ data ScopedExp = ScopedExp (n :: NumVarsInScope) {e : Exp | numFreeVarsExp e <= n } @-}
 data ScopedExp = ScopedExp NumVarsInScope Exp
 
-instance Pretty ScopedExp where
-  pretty (ScopedExp n e) = pretty (ScopedUExp n (uncheckExp e))
+prettyScopedExp :: ScopedExp -> Doc AnsiStyle
+prettyScopedExp (ScopedExp n e) = prettyScopedUExp (ScopedUExp n (uncheckExp e))
 
 {-@ uncheckExp :: e:Exp -> { uexp:UExp | numFreeVarsExp e = numFreeVars uexp } @-}
 uncheckExp :: Exp -> UExp
@@ -100,7 +102,7 @@ exprType (BoolE _) = TBool
 {-@
 reflect checkBindings
 checkBindings
-  :: ctx : List Ty
+  :: ctx : Language.Stitch.LH.Data.List.List Ty
   -> { e : Exp | numFreeVarsExp e <= List.length ctx }
   -> Bool
 @-}
@@ -118,8 +120,8 @@ checkBindings _ (BoolE _) = True
 {-@
 rewriteWith aClosedExpIsValidInAnyContext [List.appendLengh]
 aClosedExpIsValidInAnyContext
-  :: ctx0 : List Ty
-  -> ctx1 : List Ty
+  :: ctx0 :Language.Stitch.LH.Data.List.List Ty
+  -> ctx1 :Language.Stitch.LH.Data.List.List Ty
   -> e : Exp
   -> { WellTyped e ctx0 <=>
        WellTyped e (List.append ctx0 ctx1) && numFreeVarsExp e <= List.length ctx0
@@ -178,8 +180,8 @@ check :: Globals -> UExp -> (Exp -> Ty -> Either TyError b) -> Either TyError b
 check globals = go Nil
   where
     {-@
-      go :: ts : List Ty
-         -> VarsSmallerThan (List.length ts)
+      go :: ts :Language.Stitch.LH.Data.List.List Ty
+         -> VarsSmallerThan (Language.Stitch.LH.Data.List.length ts)
          -> (e1 : WellTypedExp ts -> { t: Ty | exprType e1 = t } -> Either TyError b)
          -> Either TyError b
       @-}
@@ -275,23 +277,23 @@ data TyError
   | TypeMismatch ScopedUExp Ty Ty ScopedUExp -- expression expected_type actual_type context
   deriving Show
 
-instance Pretty TyError where
-  pretty = \case
+prettyTyError :: TyError -> Doc AnsiStyle
+prettyTyError = \case
     OutOfScopeGlobal name ->
-      text "Global variable not in scope:" <+> squotes (text name)
+      pretty "Global variable not in scope:" <+> squotes (pretty name)
     NotAFunction e ty ->
-      text "Expected a function instead of" <+>
+      pretty "Expected a function instead of" <+>
       squotes (prettyTypedExp e ty)
     TypeMismatch e expected actual ctx ->
-      text "Found" <+> squotes (prettyTypedExp e expected) <$$>
-      text "but expected type" <+> squotes (pretty actual) <$$>
+      pretty "Found" <+> squotes (prettyTypedExp e expected) $$
+      pretty "but expected type" <+> squotes (pretty actual) $$
       inTheExpression ctx
 
-prettyTypedExp :: ScopedUExp -> Ty -> Doc
-prettyTypedExp e ty = pretty e <+> text ":" <+> pretty ty
+prettyTypedExp :: ScopedUExp -> Ty -> Doc AnsiStyle
+prettyTypedExp e ty = prettyScopedUExp e <+> pretty ":" <+> pretty ty
 
-inTheExpression :: ScopedUExp -> Doc
-inTheExpression e = text "in the expression" <+> squotes (pretty e)
+inTheExpression :: ScopedUExp -> Doc AnsiStyle
+inTheExpression e = pretty "in the expression" <+> squotes (prettyScopedUExp e)
 
 
 {-@
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Data/List.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Data/List.hs
index 0c4f4787b6..c76ac5b2c2 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Data/List.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Data/List.hs
@@ -27,21 +27,21 @@ data List a = Cons { head :: a, tail :: List a } | Nil
 
 {-@
 inline empty
-empty :: { xs : List a | length xs = 0 }
+empty :: { xs : Language.Stitch.LH.Data.List.List a | length xs = 0 }
 @-}
 empty :: List a
 empty = Nil
 
 {-@
 inline cons
-cons :: a -> xs : List a -> { ys : List a | length ys = 1 + length xs }
+cons :: a -> xs : Language.Stitch.LH.Data.List.List a -> { ys : Language.Stitch.LH.Data.List.List a | length ys = 1 + length xs }
 @-}
 cons :: a -> List a -> List a
 cons a b = Cons a b
 
 {-@
 reflect elemAt
-elemAt :: n : Nat -> { xs : List a | length xs > n } -> a
+elemAt :: n : Nat -> { xs : Language.Stitch.LH.Data.List.List a | length xs > n } -> a
 @-}
 elemAt :: Nat -> List a -> a
 elemAt 0 (Cons x _) = x
@@ -51,8 +51,8 @@ elemAt i (Cons _ xs) = elemAt (i-1) xs
 reflect take
 take
   :: n : Nat
-  -> { xs : List a | length xs >= n }
-  -> { ys : List a | length ys = n}
+  -> { xs : Language.Stitch.LH.Data.List.List a | length xs >= n }
+  -> { ys : Language.Stitch.LH.Data.List.List a | length ys = n}
 @-}
 take :: Nat -> List a -> List a
 take 0 _ = Nil
@@ -60,7 +60,7 @@ take i (Cons x xs) = Cons x (take (i-1) xs)
 
 {-@
 measure length
-length :: xs : List a -> Nat
+length :: xs : Language.Stitch.LH.Data.List.List a -> Nat
 @-}
 length :: List a -> Nat
 length Nil = 0
@@ -69,9 +69,9 @@ length (Cons _ xs) = 1 + length xs
 {-@
 reflect append
 append ::
-  xs : List a ->
-  ys : List a ->
-  { zs : List a | length zs == length xs + length ys }
+  xs : Language.Stitch.LH.Data.List.List a ->
+  ys : Language.Stitch.LH.Data.List.List a ->
+  { zs : Language.Stitch.LH.Data.List.List a | length zs == length xs + length ys }
  @-}
 append :: List a -> List a -> List a
 append Nil ys = ys
@@ -79,8 +79,8 @@ append (Cons x xs) ys = Cons x (append xs ys)
 
 {-@
 appendLengh
-  :: xs : List a
-  -> ys : List a
+  :: xs : Language.Stitch.LH.Data.List.List a
+  -> ys : Language.Stitch.LH.Data.List.List a
   -> { length (append xs ys) == length xs + length ys}
 @-}
 appendLengh :: List a -> List a -> Proof
@@ -89,8 +89,8 @@ appendLengh xs ys = trivial ? append xs ys
 {-@
 elemAtThroughAppend
   :: i : Nat
-  -> xs : { xs : List a | i < length xs }
-  -> ys : List a
+  -> xs : { xs :Language.Stitch.LH.Data.List.List a | i < length xs }
+  -> ys : Language.Stitch.LH.Data.List.List a
   -> { elemAt i (append xs ys) = elemAt i xs }
 @-}
 elemAtThroughAppend :: Nat -> List a -> List a -> Proof
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Eval.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Eval.hs
index ceff0cc3a5..36021c8be1 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Eval.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Eval.hs
@@ -31,7 +31,8 @@ import Language.Stitch.LH.Check
 import Language.Stitch.LH.Op
 import Language.Stitch.LH.Type
 
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
 ------------------------------------------------
 -- Evaluation
@@ -58,20 +59,20 @@ data Value
 @-}
 data Value = VInt Int | VBool Bool | VFun Exp (Value -> Value)
 
-instance Pretty Value where
-  pretty = \case
-    VInt i -> int i
-    VBool True -> text "true"
-    VBool False -> text "false"
-    VFun e _ -> pretty (ScopedExp (numFreeVarsExp e) e)
+prettyValue :: Value -> Doc AnsiStyle
+prettyValue = \case
+    VInt i -> pretty i
+    VBool True -> pretty "true"
+    VBool False -> pretty "false"
+    VFun e _ -> prettyScopedExp (ScopedExp (numFreeVarsExp e) e)
 
 {-@
 // XXX: Why can't we reflect map?
 // XXX: If using measure, LH fails with: elaborate makeKnowledge failed on
 reflect mapValueType
 mapValueType
-  :: vs:List Value
-  -> { ts:List Ty
+  :: vs: Language.Stitch.LH.Data.List.List Value
+  -> { ts: Language.Stitch.LH.Data.List.List Ty
      | List.length ts = List.length vs
      }
 @-}
@@ -95,7 +96,7 @@ eval :: Exp -> Value
 eval = evalWithCtx Nil
 
 {-@
-evalWithCtx :: ctx:List Value -> e:WellTypedExp (mapValueType ctx) -> ValueT (exprType e)
+evalWithCtx :: ctx:Language.Stitch.LH.Data.List.List Value -> e:WellTypedExp (mapValueType ctx) -> ValueT (exprType e)
 @-}
 evalWithCtx :: List Value -> Exp -> Value
 evalWithCtx ctx e0 = case e0 of
@@ -167,7 +168,7 @@ unsafeMod = mod
 {-@
 elemAtThroughMapValueType_prop
   :: i:Nat
-  -> ctx : { List Value | i < List.length ctx }
+  -> ctx : { Language.Stitch.LH.Data.List.List Value | i < List.length ctx }
   -> { List.elemAt i (mapValueType ctx) = valueType (List.elemAt i ctx) }
 @-}
 elemAtThroughMapValueType_prop :: Nat -> List Value -> Proof
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Monad.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Monad.hs
index 1e677eb3c5..a043149816 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Monad.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Monad.hs
@@ -29,12 +29,13 @@ module Language.Stitch.LH.Monad (
   ) where
 
 import Language.Stitch.LH.Check
-import Language.Stitch.LH.Util
 
 import System.Console.Haskeline
 
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
+import Control.Monad
 import Control.Monad.Trans.Maybe
 import Control.Monad.Except
 import Control.Monad.Reader
@@ -47,8 +48,8 @@ newtype Stitch a = Stitch { unStitch :: MaybeT (StateT Globals (InputT IO)) a }
   deriving (Monad, Functor, Applicative, MonadState Globals, MonadIO)
 
 -- | Like the 'Stitch' monad, but also supporting error messages via 'Doc's
-newtype StitchE a = StitchE { unStitchE :: ExceptT Doc Stitch a }
-  deriving (Monad, Functor, Applicative, MonadError Doc)
+newtype StitchE a = StitchE { unStitchE :: ExceptT (Doc AnsiStyle) Stitch a }
+  deriving (Monad, Functor, Applicative, MonadError (Doc AnsiStyle))
 
 instance MonadReader Globals StitchE where
   ask = StitchE get
@@ -62,14 +63,14 @@ instance MonadReader Globals StitchE where
 -- | Class for the two stitchorous monads
 class StitchM m where
   -- | Print a 'Doc' without a newline at the end
-  printDoc :: Doc -> m ()
+  printDoc :: Doc AnsiStyle -> m ()
 
   -- | Print a 'Doc' with a newline
-  printLine :: Doc -> m ()
+  printLine :: Doc AnsiStyle -> m ()
 
 instance StitchM Stitch where
-  printDoc = Stitch . liftIO . displayIO stdout . toSimpleDoc
-  printLine = Stitch . liftIO . displayIO stdout . toSimpleDoc . (<> hardline)
+  printDoc = Stitch . liftIO . hPutDoc stdout
+  printLine = Stitch . liftIO . hPutDoc stdout . (<> hardline)
 
 instance StitchM StitchE where
   printDoc = StitchE . lift . printDoc
@@ -83,16 +84,16 @@ prompt = Stitch . lift . lift . getInputLine
 -- | Abort the 'Stitch' monad
 quit :: Stitch a
 quit = do
-  printLine (text "Good-bye.")
+  printLine (pretty "Good-bye.")
   Stitch mzero
 
 -- | Abort the computation with an error
-issueError :: Doc -> StitchE a
+issueError :: Doc AnsiStyle -> StitchE a
 issueError = StitchE . throwError
 
 -- | Hoist an 'Either' into 'StitchE'
 eitherToStitchE :: Either String a -> StitchE a
-eitherToStitchE (Left err) = issueError (text err)
+eitherToStitchE (Left err) = issueError (pretty err)
 eitherToStitchE (Right x)  = return x
 
 -- | Run a 'Stitch' computation
@@ -101,6 +102,6 @@ runStitch thing_inside
   = void $ flip evalStateT emptyGlobals $ runMaybeT $ unStitch thing_inside
 
 -- | Run a 'StitchE' computation
-runStitchE :: StitchE a -> Stitch (Either Doc a)
+runStitchE :: StitchE a -> Stitch (Either (Doc AnsiStyle) a)
 runStitchE thing_inside
   = runExceptT $ unStitchE thing_inside
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Op.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Op.hs
index 4a18be41a0..b9f3f73e52 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Op.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Op.hs
@@ -24,7 +24,7 @@ import Data.Hashable
 import Language.Stitch.LH.Type
 import Language.Stitch.LH.Util (render)
 
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
 
 {-@
  data ArithOp
@@ -75,16 +75,16 @@ arithType Equals   = TBool
 -- Pretty-printing
 
 instance Pretty ArithOp where
-  pretty Plus     = char '+'
-  pretty Minus    = char '-'
-  pretty Times    = char '*'
-  pretty Divide   = char '/'
-  pretty Mod      = char '%'
-  pretty Less     = char '<'
-  pretty LessE    = text "<="
-  pretty Greater  = char '>'
-  pretty GreaterE = text ">="
-  pretty Equals   = text "=="
+  pretty Plus     = pretty '+'
+  pretty Minus    = pretty '-'
+  pretty Times    = pretty '*'
+  pretty Divide   = pretty '/'
+  pretty Mod      = pretty '%'
+  pretty Less     = pretty '<'
+  pretty LessE    = pretty "<="
+  pretty Greater  = pretty '>'
+  pretty GreaterE = pretty ">="
+  pretty Equals   = pretty "=="
 
 instance Show ArithOp where
   show = render . pretty
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Pretty.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Pretty.hs
index c0aebb9704..26fa0df8b6 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Pretty.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Pretty.hs
@@ -18,7 +18,8 @@ import Language.Stitch.LH.Op
 import Language.Stitch.LH.Util
 import Language.Stitch.LH.Data.Nat
 
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
 lamPrec, appPrec, appLeftPrec, appRightPrec, ifPrec :: Prec
 lamPrec = 1
@@ -46,12 +47,12 @@ precInfo GreaterE = (4, 4, 4)
 precInfo Equals   = (4, 4, 4)
 
 -- | A function that changes a 'Doc's color
-type ApplyColor = Doc -> Doc
+type ApplyColor = Doc AnsiStyle -> Doc AnsiStyle
 
 -- | The colors used for all rendered expressions
 {-@ coloring :: { v : [ApplyColor] | len v > 0 } @-}
 coloring :: [ApplyColor]
-coloring = [red, green, yellow, blue, magenta, cyan]
+coloring = map (annotate . color) [Red, Green, Yellow, Blue, Magenta, Cyan]
 
 {-@ ignore applyColor @-}
 -- LH would need a proof that
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Statement.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Statement.hs
index 91b3b948de..a38302a6ed 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Statement.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Statement.hs
@@ -13,13 +13,14 @@
 ----------------------------------------------------------------------------
 
 {-# OPTIONS_GHC -Wno-unused-imports #-}
-module Language.Stitch.LH.Statement ( Statement(..) ) where
+module Language.Stitch.LH.Statement ( Statement(..), prettyStatement ) where
 
 -- XXX: Import Op so LH doesn't fail with: Unknown type constructor `ArithOp`
 import Language.Stitch.LH.Op
 import Language.Stitch.LH.Unchecked
 
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
 -- | A statement can either be a bare expression, which will be evaluated,
 -- or an assignment to a global variable.
@@ -31,6 +32,6 @@ data Statement = BareExp UExp
                | NewGlobal String UExp
   deriving Show
 
-instance Pretty Statement where
-  pretty (BareExp e)     = pretty (ScopedUExp 0 e)
-  pretty (NewGlobal v e) = text v <+> char '=' <+> pretty (ScopedUExp 0 e)
+prettyStatement :: Statement -> Doc AnsiStyle
+prettyStatement (BareExp e)     = prettyScopedUExp (ScopedUExp 0 e)
+prettyStatement (NewGlobal v e) = pretty v <+> pretty '=' <+> prettyScopedUExp (ScopedUExp 0 e)
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Step.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Step.hs
index c208d67e00..362bedd21f 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Step.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Step.hs
@@ -50,7 +50,7 @@ subst es e0 =
 -- of checkBindings, it is not needed at runtime.
 {-@
 substIndex
-  :: ctx:List Ty
+  :: ctx:Language.Stitch.LH.Data.List.List Ty
   -> i: { Nat | i = List.length ctx - 1 }
   -> es:{ WellTypedExp Nil | exprType es = List.elemAt i ctx }
   -> e0:WellTypedExp ctx
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Token.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Token.hs
index da743dc500..44f6c2f93e 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Token.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Token.hs
@@ -20,7 +20,7 @@ module Language.Stitch.LH.Token (
 import Language.Stitch.LH.Util
 import Language.Stitch.LH.Op
 
-import Text.PrettyPrint.ANSI.Leijen  as Pretty
+import Prettyprinter
 import Text.Parsec.Pos ( SourcePos, newPos )
 
 import Data.List                      as List
@@ -83,7 +83,7 @@ instance Pretty Token where
   prettyList = printTogether . List.map printingInfo
 
 instance Show Token where
-  show = render . pretty
+  show = show . pretty
 
 instance Pretty LToken where
   pretty     = pretty . unLoc
@@ -92,38 +92,38 @@ instance Pretty LToken where
 instance Show LToken where
   show = render . pretty
 
-type PrintingInfo = (Doc, Bool, Bool)
+type PrintingInfo ann = (Doc ann, Bool, Bool)
    -- the bools say whether or not to include a space before or a space after
 
-alone :: Doc -> PrintingInfo
+alone :: Doc ann -> PrintingInfo ann
 alone = (, True, True)
 
-getDoc :: PrintingInfo -> Doc
+getDoc :: PrintingInfo ann -> Doc ann
 getDoc (doc, _, _) = doc
 
-printingInfo :: Token -> PrintingInfo
-printingInfo LParen          = (char '(', True, False)
-printingInfo RParen          = (char ')', False, True)
-printingInfo Lambda          = (char '\\', True, False)
-printingInfo Dot             = (char '.', False, True)
-printingInfo ArrowTok        = alone $ text "->"
-printingInfo Colon           = (char ':', False, False)
+printingInfo :: Token -> PrintingInfo ann
+printingInfo LParen          = (pretty '(', True, False)
+printingInfo RParen          = (pretty ')', False, True)
+printingInfo Lambda          = (pretty '\\', True, False)
+printingInfo Dot             = (pretty '.', False, True)
+printingInfo ArrowTok        = alone $ pretty "->"
+printingInfo Colon           = (pretty ':', False, False)
 printingInfo (ArithOp a)     = alone $ pretty a
-printingInfo (IntTok i)      = alone $ int i
-printingInfo (BoolTok True)  = alone $ text "true"
-printingInfo (BoolTok False) = alone $ text "false"
-printingInfo If              = alone $ text "if"
-printingInfo Then            = alone $ text "then"
-printingInfo Else            = alone $ text "else"
-printingInfo FixTok          = alone $ text "fix"
-printingInfo LetTok          = alone $ text "let"
-printingInfo InTok           = alone $ text "in"
-printingInfo Assign          = alone $ text "="
-printingInfo Semi            = (char ';', False, True)
-printingInfo (Name t)        = alone $ text t
-
-printTogether :: [PrintingInfo] -> Doc
-printTogether []  = Pretty.empty
+printingInfo (IntTok i)      = alone $ pretty i
+printingInfo (BoolTok True)  = alone $ pretty "true"
+printingInfo (BoolTok False) = alone $ pretty "false"
+printingInfo If              = alone $ pretty "if"
+printingInfo Then            = alone $ pretty "then"
+printingInfo Else            = alone $ pretty "else"
+printingInfo FixTok          = alone $ pretty "fix"
+printingInfo LetTok          = alone $ pretty "let"
+printingInfo InTok           = alone $ pretty "in"
+printingInfo Assign          = alone $ pretty "="
+printingInfo Semi            = (pretty ';', False, True)
+printingInfo (Name t)        = alone $ pretty t
+
+printTogether :: [PrintingInfo ann] -> Doc ann
+printTogether []  = mempty
 printTogether pis = getDoc $ List.foldl1 combine pis
   where
     combine (doc1, before_space, inner_space1) (doc2, inner_space2, after_space)
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Type.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Type.hs
index ec8db8ac36..1805a098d4 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Type.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Type.hs
@@ -17,7 +17,7 @@ module Language.Stitch.LH.Type where
 
 import Language.Stitch.LH.Util (Prec, topPrec, maybeParens)
 
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
 import Data.Hashable
 import GHC.Generics
 
@@ -46,10 +46,10 @@ arrowLeftPrec  = 5
 arrowRightPrec = 4.9
 arrowPrec      = 5
 
-pretty_ty :: Prec -> Ty -> Doc
+pretty_ty :: Prec -> Ty -> Doc ann
 pretty_ty p (TFun arg res) = maybeParens (p >= arrowPrec) $
                                hsep [ pretty_ty arrowLeftPrec arg
-                                    , text "->"
+                                    , pretty "->"
                                     , pretty_ty arrowRightPrec res ]
-pretty_ty _    TInt        = text "Int"
-pretty_ty _    TBool       = text "Bool"
+pretty_ty _    TInt        = pretty "Int"
+pretty_ty _    TBool       = pretty "Bool"
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Unchecked.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Unchecked.hs
index dc76498650..2d2919010b 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Unchecked.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Unchecked.hs
@@ -21,7 +21,8 @@ import Language.Stitch.LH.Op
 import Language.Stitch.LH.Util
 import Language.Stitch.LH.Data.Nat as Nat
 
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
 {-@
 data UExp
@@ -80,21 +81,21 @@ type ClosedUExp = { e : UExp | numFreeVars e == 0 }
 data ScopedUExp = ScopedUExp NumVarsInScope UExp
   deriving (Eq, Show)
 
-instance Pretty ScopedUExp where
-  pretty (ScopedUExp n e) = prettyExp n topPrec e
+prettyScopedUExp :: ScopedUExp -> Doc AnsiStyle
+prettyScopedUExp (ScopedUExp n e) = prettyExp n topPrec e
 
-{-@ prettyExp :: n : NumVarsInScope -> Prec -> VarsSmallerThan n -> Doc @-}
-prettyExp :: NumVarsInScope -> Prec -> UExp -> Doc
+{-@ prettyExp :: n : NumVarsInScope -> Prec -> VarsSmallerThan n -> Doc AnsiStyle @-}
+prettyExp :: NumVarsInScope -> Prec -> UExp -> Doc AnsiStyle
 prettyExp n prec = \case
-  UVar v       -> applyColor (ScopedVar n v) (char '#' <> int v)
+  UVar v       -> applyColor (ScopedVar n v) (pretty '#' <> pretty v)
 
-  UGlobal name -> text name
+  UGlobal name -> pretty name
 
   -- XXX: Putting the alternatives below in auxiliary functions would cause
   -- a mysterious failure in LH.
   ULam ty body -> maybeParens (prec >= lamPrec) $
-    fillSep [ char 'λ' <> applyColor (ScopedVar (n + 1) 0) (char '#') <>
-              text ":" <> pretty ty <> char '.'
+    fillSep [ pretty 'λ' <> applyColor (ScopedVar (n + 1) 0) (pretty '#') <>
+              pretty ":" <> pretty ty <> pretty '.'
             , prettyExp (n + 1) topPrec body ]
 
   UApp e1 e2 -> maybeParens (prec >= appPrec) $
@@ -102,8 +103,8 @@ prettyExp n prec = \case
             , prettyExp n appRightPrec e2 ]
 
   ULet e1 e2 -> maybeParens (prec >= lamPrec) $
-    fillSep [ text "let" <+> applyColor (ScopedVar (n + 1) 0) (char '#') <+>
-              char '=' <+> prettyExp n topPrec e1 <+> text "in"
+    fillSep [ pretty "let" <+> applyColor (ScopedVar (n + 1) 0) (pretty '#') <+>
+              pretty '=' <+> prettyExp n topPrec e1 <+> pretty "in"
             , prettyExp (n + 1) topPrec e2 ]
 
   UArith e1 op e2 -> maybeParens (prec >= opPrec op) $
@@ -111,15 +112,15 @@ prettyExp n prec = \case
             , prettyExp n (opRightPrec op) e2 ]
 
   UCond e1 e2 e3 -> maybeParens (prec >= ifPrec) $
-    fillSep [ text "if" <+> prettyExp n topPrec e1
-            , text "then" <+> prettyExp n topPrec e2
-            , text "else" <+> prettyExp n topPrec e3 ]
+    fillSep [ pretty "if" <+> prettyExp n topPrec e1
+            , pretty "then" <+> prettyExp n topPrec e2
+            , pretty "else" <+> prettyExp n topPrec e3 ]
 
   UFix body -> maybeParens (prec >= appPrec) $
-                 text "fix" <+> prettyExp n topPrec body
+                 pretty "fix" <+> prettyExp n topPrec body
 
-  UIntE i -> int i
+  UIntE i -> pretty i
 
-  UBoolE True -> text "true"
+  UBoolE True -> pretty "true"
 
-  UBoolE False -> text "false"
+  UBoolE False -> pretty "false"
diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Util.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Util.hs
index d4b2ca299f..640df36576 100644
--- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Util.hs
+++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Util.hs
@@ -16,14 +16,15 @@
 ----------------------------------------------------------------------------
 
 module Language.Stitch.LH.Util (
-  render, toSimpleDoc, maybeParens, ($$),
+  render, maybeParens, ($$),
   Prec, topPrec,
   stripWhitespace, foldl1M,
   allPairs
   ) where
 
 import Text.Parsec
-import Text.PrettyPrint.ANSI.Leijen as Pretty
+import Prettyprinter as Pretty
+import Prettyprinter.Render.String as Pretty
 
 import Data.Char
 import Data.List
@@ -31,7 +32,7 @@ import Data.List
 import Control.Monad
 
 instance Pretty ParseError where
-  pretty = text . show
+  pretty = pretty
 
 -- | More conspicuous synonym for operator precedence
 type Prec = Rational
@@ -41,21 +42,16 @@ topPrec :: Prec
 topPrec = 0
 
 -- | Convert a 'Doc' to a 'String'
-render :: Doc -> String
-render = flip displayS "" . toSimpleDoc
-
--- | Convert a 'Doc' to a 'SimpleDoc' for further rendering
-toSimpleDoc :: Doc -> SimpleDoc
-toSimpleDoc = renderPretty 1.0 78
+render :: Doc ann -> String
+render = Pretty.renderString . layoutPretty defaultLayoutOptions
 
 -- | Enclose a 'Doc' in parens if the flag is 'True'
-maybeParens :: Bool -> Doc -> Doc
+maybeParens :: Bool -> Doc ann -> Doc ann
 maybeParens True  = parens
 maybeParens False = id
 
--- | Synonym for 'Pretty.<$>'
-($$) :: Doc -> Doc -> Doc
-($$) = (Pretty.<$>)
+($$) :: Doc ann -> Doc ann -> Doc ann
+a $$ b = Pretty.vcat [a, b]
 
 -- | (Inefficiently) strips whitespace from a string
 stripWhitespace :: String -> String
diff --git a/tests/harness/Driver_cabal.hs b/tests/harness/Driver_cabal.hs
index 2683183f67..eade2af3ae 100644
--- a/tests/harness/Driver_cabal.hs
+++ b/tests/harness/Driver_cabal.hs
@@ -2,7 +2,6 @@
 
 import Test.Build
 import Test.Options
-import Options.Applicative
 
 main :: IO ()
-main = program cabalTestEnv cabalRun =<< execParser opts
+main = program cabalTestEnv cabalRun =<< parseOptions
diff --git a/tests/harness/Driver_stack.hs b/tests/harness/Driver_stack.hs
index fb496d383c..d3d321de22 100644
--- a/tests/harness/Driver_stack.hs
+++ b/tests/harness/Driver_stack.hs
@@ -1,6 +1,5 @@
 import Test.Build
 import Test.Options
-import Options.Applicative
 
 main :: IO ()
-main = program stackTestEnv stackRun =<< execParser opts
+main = program stackTestEnv stackRun =<< parseOptions
diff --git a/tests/harness/Test/Build.hs b/tests/harness/Test/Build.hs
index e9d58c09cf..417adcc778 100644
--- a/tests/harness/Test/Build.hs
+++ b/tests/harness/Test/Build.hs
@@ -30,6 +30,7 @@ cabalRun opts names = do
     [ "build" ]
     <> (case projectFile of Nothing -> []; Just projectFile' -> [ "--project-file", T.pack projectFile' ])
     <> (if measureTimings opts then ["--flags=measure-timings", "-j1"] else ["--keep-going"])
+    <> extraOpts opts
     <> names
 
 -- | Runs stack on the given test groups
@@ -38,12 +39,13 @@ stackRun opts names =
   runCommand "stack" $
     [ "build", "--flag", "tests:stack" ]
     <> concat [ ["--flag=tests:measure-timings", "-j1"] | measureTimings opts ]
-    -- Enables that particular executable in the cabal file
     <> testFlags
+    <> extraOpts opts
     <> [ "--" ]
     <> testNames
   where
     testNames = fmap ("tests:" <>) names
+    -- Enables that particular executable in the cabal file
     testFlags = concatMap (("--flag" :) . pure) testNames
 
 -- | Ensure prog is on the PATH
diff --git a/tests/harness/Test/Options.hs b/tests/harness/Test/Options.hs
index a59e0eb591..951951ba4d 100644
--- a/tests/harness/Test/Options.hs
+++ b/tests/harness/Test/Options.hs
@@ -4,16 +4,18 @@ import qualified Data.Text as T
 import Test.Groups
 import Options.Applicative
 import Data.List (intersperse)
+import System.Environment (getArgs)
 
 data Options = Options
-  { testGroups :: [T.Text]
+  { extraOpts :: [T.Text]
+  , testGroups :: [T.Text]
   , showAll :: Bool
   , measureTimings :: Bool
   }
   deriving (Eq, Ord, Show)
 
 options :: Parser Options
-options = Options <$>
+options = Options [] <$>
   many (argument
          (T.pack <$> str)
           (metavar "TESTGROUPNAMES..."
@@ -29,3 +31,10 @@ opts :: ParserInfo Options
 opts = info (options <**> helper)
   (fullDesc
    <> progDesc "Execute groups of tests.")
+
+parseOptions :: IO Options
+parseOptions = do
+    args <- getArgs
+    let (before, after) = break ("--"==) args
+    o <- handleParseResult (execParserPure defaultPrefs opts before)
+    return o {extraOpts = map T.pack $ drop 1 after}
diff --git a/tests/neg/AutoSize.hs b/tests/neg/AutoSize.hs
index 78da0d900b..5cef081fa9 100644
--- a/tests/neg/AutoSize.hs
+++ b/tests/neg/AutoSize.hs
@@ -1,7 +1,7 @@
 {-@ LIQUID "--expect-any-error" @-}
 module AutoSize where
 
-import GHC.Base
+import GHC.Base hiding (List)
 
 data List a = N | Cons a (List a) 
 
diff --git a/tests/tests.cabal b/tests/tests.cabal
index 53b1bba8aa..f6c1acd8a2 100644
--- a/tests/tests.cabal
+++ b/tests/tests.cabal
@@ -54,7 +54,8 @@ executable benchmark-stitch-lh
     main-is:          Main.hs
     if !flag(benchmark-stitch-lh) && flag(stack)
       buildable:      False
-    build-depends:    ansi-wl-pprint >= 0.6.7.1 && < 1.0.0
+    build-depends:    prettyprinter >= 1.0
+                    , prettyprinter-ansi-terminal >= 1.1
                     , mtl >= 2.2.1
                     , transformers >= 0.4.0.0
                     , parsec >= 3.1