diff --git a/liquidhaskell-boot/liquidhaskell-boot.cabal b/liquidhaskell-boot/liquidhaskell-boot.cabal
index 82d77c665f..c33813ef79 100644
--- a/liquidhaskell-boot/liquidhaskell-boot.cabal
+++ b/liquidhaskell-boot/liquidhaskell-boot.cabal
@@ -74,6 +74,7 @@ library
                       Language.Haskell.Liquid.GHC.Plugin
                       Language.Haskell.Liquid.GHC.Plugin.Tutorial
                       Language.Haskell.Liquid.LawInstances
+                      Language.Haskell.Liquid.LHNameResolution
                       Language.Haskell.Liquid.Liquid
                       Language.Haskell.Liquid.Measure
                       Language.Haskell.Liquid.Misc
@@ -124,6 +125,7 @@ library
 
   build-depends:      base                 >= 4.11.1.0 && < 5
                     , Diff                 >= 0.3 && < 0.6
+                    , array
                     , aeson
                     , binary
                     , bytestring           >= 0.10
diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
index f08e2d180e..313d630c8f 100644
--- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
+++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
@@ -204,6 +204,7 @@ import GHC.Builtin.Types              as Ghc
     , intTyCon
     , intTyConName
     , liftedTypeKind
+    , liftedTypeKindTyConName
     , listTyCon
     , listTyConName
     , naturalTy
@@ -214,6 +215,7 @@ import GHC.Builtin.Types              as Ghc
     , trueDataConId
     , tupleDataCon
     , tupleTyCon
+    , tupleTyConName
     , typeSymbolKind
     )
 import GHC.Builtin.Types.Prim         as Ghc
@@ -434,7 +436,8 @@ import GHC.HsToCore.Monad             as Ghc
     ( DsM, initDsTc, initDsWithModGuts, newUnique )
 import GHC.Iface.Syntax               as Ghc
     ( IfaceAnnotation(ifAnnotatedValue) )
-import GHC.Plugins                    as Ghc ( deserializeWithData
+import GHC.Plugins                    as Ghc ( Serialized(Serialized)
+                                             , deserializeWithData
                                              , fromSerialized
                                              , toSerialized
                                              , defaultPlugin
@@ -451,7 +454,7 @@ import GHC.Core.Opt.OccurAnal         as Ghc
 import GHC.Core.TyCo.FVs              as Ghc (tyCoVarsOfCo, tyCoVarsOfType)
 import GHC.Driver.Backend             as Ghc (interpreterBackend)
 import GHC.Driver.Env                 as Ghc
-    ( HscEnv(hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins)
+    ( HscEnv(hsc_NC, hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins)
     , Hsc
     , hscSetFlags, hscUpdateFlags
     )
@@ -468,6 +471,8 @@ import GHC.Hs                         as Ghc
     )
 import GHC.HsToCore.Expr              as Ghc
     ( dsLExpr )
+import GHC.Iface.Binary               as Ghc
+    ( TraceBinIFace(QuietBinIFace), getWithUserData, putWithUserData )
 import GHC.Iface.Errors.Ppr            as Ghc
     ( missingInterfaceErrorDiagnostic )
 import GHC.Iface.Load                 as Ghc
@@ -502,6 +507,8 @@ import GHC.Tc.Types.Origin            as Ghc (lexprCtOrigin)
 import GHC.Tc.Utils.Monad             as Ghc
     ( captureConstraints
     , discardConstraints
+    , getGblEnv
+    , setGblEnv
     , getEnv
     , getTopEnv
     , failIfErrsM
@@ -538,6 +545,7 @@ import GHC.Types.Basic                as Ghc
     , PprPrec
     , PromotionFlag(NotPromoted)
     , TopLevelFlag(NotTopLevel)
+    , TupleSort(BoxedTuple)
     , funPrec
     , InlinePragma(inl_act, inl_inline, inl_rule, inl_sat, inl_src)
     , isDeadOcc
@@ -613,12 +621,20 @@ import GHC.Types.Name                 as Ghc
     , occNameString
     , stableNameCmp
     )
+import GHC.Types.Name.Cache           as Ghc (NameCache)
+import GHC.Types.Name.Occurrence      as Ghc (mkOccName, dataName, tcName)
 import GHC.Types.Name.Reader          as Ghc
-    ( ImpItemSpec(ImpAll)
+    ( GlobalRdrEnv
+    , ImpItemSpec(ImpAll)
+    , LookupGRE(LookupRdrName)
+    , WhichGREs(SameNameSpace)
     , getRdrName
     , globalRdrEnvElts
     , greName
+    , lookupGRE
     , mkQual
+    , mkRdrQual
+    , mkRdrUnqual
     , mkVarUnqual
     , mkUnqual
     , nameRdrName
@@ -713,6 +729,14 @@ import GHC.Unit.Module.ModGuts        as Ghc
       , mg_usages
       )
     )
+import GHC.Utils.Binary               as Ghc
+    ( Binary(get, put_)
+    , getByte
+    , openBinMem
+    , putByte
+    , unsafeUnpackBinBuffer
+    , withBinBuffer
+    )
 import GHC.Utils.Error                as Ghc (pprLocMsgEnvelope, withTiming)
 import GHC.Utils.Logger               as Ghc (Logger(logFlags), putLogMsg)
 import GHC.Utils.Outputable           as Ghc hiding ((<>))
diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/StableModule.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/StableModule.hs
index 72568af491..b287b9bf1d 100644
--- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/StableModule.hs
+++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/StableModule.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveDataTypeable #-}
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 
@@ -16,6 +17,7 @@ module Liquid.GHC.API.StableModule (
 import qualified GHC
 import qualified GHC.Unit.Types as GHC
 import qualified GHC.Unit.Module as GHC
+import           Data.Data (Data)
 import           Data.Hashable
 import           GHC.Generics            hiding (to, moduleName)
 import           Data.Binary
@@ -27,7 +29,7 @@ import           Data.Binary
 --
 newtype StableModule =
   StableModule { unStableModule :: GHC.Module }
-  deriving Generic
+  deriving (Data, Generic)
 
 -- | Converts a 'Module' into a 'StableModule'.
 toStableModule :: GHC.Module -> StableModule
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
index ff8955020b..69c8e7cd17 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -34,7 +34,6 @@ import qualified Control.Exception         as Ex
 import qualified Data.HashMap.Strict       as M
 import qualified Data.Char                 as Char
 import qualified Data.List                 as L
-import qualified Text.Printf               as Printf
 import qualified Text.PrettyPrint.HughesPJ as PJ
 
 import qualified Language.Fixpoint.Types               as F
@@ -43,6 +42,7 @@ import qualified Language.Fixpoint.Misc                as Misc
 import           Language.Fixpoint.Types (Expr(..)) -- , Symbol, symbol)
 import qualified Language.Haskell.Liquid.GHC.Misc      as GM
 import qualified Liquid.GHC.API       as Ghc
+import           Language.Haskell.Liquid.LHNameResolution (exprArg)
 import           Language.Haskell.Liquid.Types.Errors
 import           Language.Haskell.Liquid.Types.DataDecl
 import qualified Language.Haskell.Liquid.Types.RefType as RT
@@ -459,31 +459,6 @@ errRTAliasApp l la rta = Just . ErrAliasApp  sp name sp'
     sp'             = GM.sourcePosSrcSpan la
 
 
-
---------------------------------------------------------------------------------
--- | exprArg converts a tyVar to an exprVar because parser cannot tell
---   this function allows us to treating (parsed) "types" as "value"
---   arguments, e.g. type Matrix a Row Col = List (List a Row) Col
---   Note that during parsing, we don't necessarily know whether a
---   string is a type or a value expression. E.g. in tests/pos/T1189.hs,
---   the string `Prop (Ev (plus n n))` where `Prop` is the alias:
---     {-@ type Prop E = {v:_ | prop v = E} @-}
---   the parser will chomp in `Ev (plus n n)` as a `BareType` and so
---   `exprArg` converts that `BareType` into an `Expr`.
---------------------------------------------------------------------------------
-exprArg :: F.SourcePos -> String -> BareType -> Expr
-exprArg l msg = F.notracepp ("exprArg: " ++ msg) . go
-  where
-    go :: BareType -> Expr
-    go (RExprArg e)     = val e
-    go (RVar x _)       = EVar (F.symbol x)
-    go (RApp x [] [] _) = EVar (F.symbol x)
-    go (RApp f ts [] _) = F.mkEApp (F.symbol <$> btc_tc f) (go <$> ts)
-    go (RAppTy t1 t2 _) = F.EApp (go t1) (go t2)
-    go z                = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show z) msg
-    sp                  = Just (GM.sourcePosSrcSpan l)
-
-
 ----------------------------------------------------------------------------------------
 -- | @cookSpecType@ is the central place where a @BareType@ gets processed,
 --   in multiple steps, into a @SpecType@. See [NOTE:Cooking-SpecType] for
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs
index 8bd0f4262b..9bcab521d7 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs
@@ -15,7 +15,7 @@ module Language.Haskell.Liquid.Bare.Misc
 
 import           Prelude                               hiding (error)
 
-import           Liquid.GHC.API       as Ghc  hiding (Located, showPpr)
+import           Liquid.GHC.API       as Ghc  hiding (Located, get, showPpr)
 
 import           Control.Monad                         (zipWithM_)
 import           Control.Monad.Except                  (MonadError, throwError)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs
index e65d37ad3b..7872a3c2eb 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs
@@ -68,7 +68,7 @@ import           Language.Fixpoint.SortCheck (pruneUnsortedReft)
 
 
 
-import           Liquid.GHC.API hiding (panic)
+import           Liquid.GHC.API hiding (get, panic)
 import           Language.Haskell.Liquid.Types.RefType
 import qualified Language.Haskell.Liquid.GHC.SpanStack as Sp
 import           Language.Haskell.Liquid.Types.Errors
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Fresh.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Fresh.hs
index cd37e18974..d4abb3eaa5 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Fresh.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Fresh.hs
@@ -40,7 +40,7 @@ import           Language.Haskell.Liquid.Types.Types
 import           Language.Haskell.Liquid.Constraint.Types
 import qualified Language.Haskell.Liquid.GHC.Misc as GM
 import           Language.Haskell.Liquid.UX.Config
-import           Liquid.GHC.API as Ghc
+import           Liquid.GHC.API as Ghc hiding (get)
 
 --------------------------------------------------------------------------------
 -- | This is all hardwiring stuff to CG ----------------------------------------
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs
index f5332685c1..cc11f28c66 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs
@@ -29,7 +29,7 @@ import           Debug.Trace
 
 import           Prelude                                    hiding (error)
 import           Liquid.GHC.API            as Ghc hiding
-  (L, line, sourceName, showPpr, panic, showSDoc)
+  (L, get, line, sourceName, showPpr, panic, showSDoc)
 import qualified Liquid.GHC.API            as Ghc (GenLocated (L))
 
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 301e577371..5a9c9123e6 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -7,6 +7,8 @@
 {-# LANGUAGE OverloadedStrings          #-}
 {-# LANGUAGE RecordWildCards            #-}
 {-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE TypeApplications           #-}
 
 module Language.Haskell.Liquid.GHC.Plugin (
 
@@ -21,6 +23,7 @@ import qualified Language.Fixpoint.Types                 as F
 import qualified  Language.Haskell.Liquid.GHC.Misc        as LH
 import qualified Language.Haskell.Liquid.UX.CmdLine      as LH
 import qualified Language.Haskell.Liquid.GHC.Interface   as LH
+import           Language.Haskell.Liquid.LHNameResolution (collectTypeAliases, resolveLHNames)
 import qualified Language.Haskell.Liquid.Liquid          as LH
 import qualified Language.Haskell.Liquid.Types.PrettyPrint as LH ( filterReportErrors
                                                                  , filterReportErrorsWith
@@ -301,7 +304,7 @@ liquidCheckModule cfg0 ms tcg specs = do
       env <- getTopEnv
       session <- Session <$> liftIO (newIORef env)
       liftIO $ flip reflectGhc session $ mkPipelineData ms tcg specs
-    liquidLib <- liquidHaskellCheckWithConfig cfg pipelineData ms
+    liquidLib <- setGblEnv tcg $ liquidHaskellCheckWithConfig cfg pipelineData ms
     traverse (serialiseSpec tcg) liquidLib
   where
     thisFile = LH.modSummaryHsFile ms
@@ -347,7 +350,7 @@ serialiseSpec tcGblEnv liquidLib = do
   -- liftIO $ putStrLn "liquidHaskellCheck 9"
   -- ---
 
-  let serialisedSpec = Serialisation.serialiseLiquidLib liquidLib thisModule
+  serialisedSpec <- liftIO $ Serialisation.serialiseLiquidLib liquidLib thisModule
   debugLog $ "Serialised annotation ==> " ++ (O.showSDocUnsafe . O.ppr $ serialisedSpec)
 
   -- liftIO $ putStrLn "liquidHaskellCheck 10"
@@ -356,9 +359,14 @@ serialiseSpec tcGblEnv liquidLib = do
   where
     thisModule = tcg_mod tcGblEnv
 
-processInputSpec :: Config -> PipelineData -> ModSummary -> BareSpec -> TcM (Either LiquidCheckException LiquidLib)
+processInputSpec
+  :: Config
+  -> PipelineData
+  -> ModSummary
+  -> BareSpec
+  -> TcM (Either LiquidCheckException LiquidLib)
 processInputSpec cfg pipelineData modSummary inputSpec = do
-  hscEnv <- env_top <$> getEnv
+  hscEnv <- getTopEnv
   debugLog $ " Input spec: \n" ++ show inputSpec
   debugLog $ "Relevant ===> \n" ++ unlines (renderModule <$> S.toList (relevantModules (hsc_mod_graph hscEnv) modGuts))
 
@@ -502,15 +510,15 @@ processModule LiquidHaskellContext{..} = do
   debugLog ("Module ==> " ++ renderModule thisModule)
   hscEnv              <- env_top <$> getEnv
 
-  let bareSpec        = lhInputSpec
+  let bareSpec0       = lhInputSpec
   -- /NOTE/: For the Plugin to work correctly, we shouldn't call 'canonicalizePath', because otherwise
   -- this won't trigger the \"external name resolution\" as part of 'Language.Haskell.Liquid.Bare.Resolve'
   -- (cfr. 'allowExtResolution').
   let file            = LH.modSummaryHsFile lhModuleSummary
 
-  _                   <- liftIO $ LH.checkFilePragmas $ Ms.pragmas (fromBareSpec bareSpec)
+  _                   <- liftIO $ LH.checkFilePragmas $ Ms.pragmas (fromBareSpec bareSpec0)
 
-  withPragmas lhGlobalCfg file (Ms.pragmas $ fromBareSpec bareSpec) $ \moduleCfg -> do
+  withPragmas lhGlobalCfg file (Ms.pragmas $ fromBareSpec bareSpec0) $ \moduleCfg -> do
     dependencies <- loadDependencies moduleCfg (S.toList lhRelevantModules)
 
     debugLog $ "Found " <> show (HM.size $ getDependencies dependencies) <> " dependencies:"
@@ -528,9 +536,15 @@ processModule LiquidHaskellContext{..} = do
     -- Due to the fact the internals can throw exceptions from pure code at any point, we need to
     -- call 'evaluate' to force any exception and catch it, if we can.
 
-
+    tcg <- getGblEnv
+    let rtAliases = collectTypeAliases thisModule bareSpec0 (HM.toList $ getDependencies dependencies)
+        eBareSpec = resolveLHNames rtAliases (tcg_rdr_env tcg) bareSpec0
     result <-
-      makeTargetSpec moduleCfg lhModuleLogicMap targetSrc bareSpec dependencies
+      case eBareSpec of
+        Left errors -> pure $ Left $ mkDiagnostics [] errors
+        Right bareSpec ->
+          fmap (,bareSpec) <$>
+            makeTargetSpec moduleCfg lhModuleLogicMap targetSrc bareSpec dependencies
 
     let continue = pure $ Left (ErrorsOccurred [])
         reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcRn (Either LiquidCheckException ProcessModuleResult)
@@ -541,7 +555,7 @@ processModule LiquidHaskellContext{..} = do
       Left diagnostics -> do
         liftIO $ mapM_ (printWarning logger)    (allWarnings diagnostics)
         reportErrs $ allErrors diagnostics
-      Right (warnings, targetSpec, liftedSpec) -> do
+      Right ((warnings, targetSpec, liftedSpec), bareSpec) -> do
         liftIO $ mapM_ (printWarning logger) warnings
         let targetInfo = TargetInfo targetSrc targetSpec
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs
index 8c42eecf5b..eada6dee7e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs
@@ -8,64 +8,134 @@ module Language.Haskell.Liquid.GHC.Plugin.Serialisation (
 
       ) where
 
+import qualified Data.Array                               as Array
 import           Data.Foldable                            ( asum )
 
 import           Control.Monad
 
 import qualified Data.Binary                             as B
-import           Data.Binary                              ( Binary )
+import qualified Data.Binary.Builder                     as Builder
+import qualified Data.Binary.Put                         as B
 import qualified Data.ByteString.Lazy                    as B
-import           Data.Typeable
+import           Data.Data (Data)
+import           Data.Generics (ext0, gmapAccumT)
+import           Data.HashMap.Strict                     as M
 import           Data.Maybe                               ( listToMaybe )
+import           Data.Word                               (Word8)
 
-import           Liquid.GHC.API
+import qualified Liquid.GHC.API as GHC
 import           Language.Haskell.Liquid.GHC.Plugin.Types (LiquidLib)
+import           Language.Haskell.Liquid.Types.Names
 
 
 --
 -- Serialising and deserialising Specs
 --
 
-deserialiseBinaryObjectFromEPS
-  :: forall a. (Typeable a, Binary a)
-  => Module
-  -> ExternalPackageState
-  -> Maybe a
-deserialiseBinaryObjectFromEPS thisModule eps = extractFromEps
+getLiquidLibBytesFromEPS
+  :: GHC.Module
+  -> GHC.ExternalPackageState
+  -> Maybe LiquidLibBytes
+getLiquidLibBytesFromEPS thisModule eps = extractFromEps
   where
-    extractFromEps :: Maybe a
-    extractFromEps = listToMaybe $ findAnns (B.decode . B.pack) (eps_ann_env eps) (ModuleTarget thisModule)
-
-deserialiseBinaryObject :: forall a. (Typeable a, Binary a)
-                        => Module
-                        -> ExternalPackageState
-                        -> HomePackageTable
-                        -> Maybe a
-deserialiseBinaryObject thisModule eps hpt =
-    asum [extractFromHpt, deserialiseBinaryObjectFromEPS thisModule eps]
+    extractFromEps :: Maybe LiquidLibBytes
+    extractFromEps = listToMaybe $ GHC.findAnns LiquidLibBytes (GHC.eps_ann_env eps) (GHC.ModuleTarget thisModule)
+
+getLiquidLibBytes :: GHC.Module
+                        -> GHC.ExternalPackageState
+                        -> GHC.HomePackageTable
+                        -> Maybe LiquidLibBytes
+getLiquidLibBytes thisModule eps hpt =
+    asum [extractFromHpt, getLiquidLibBytesFromEPS thisModule eps]
   where
-    extractFromHpt :: Maybe a
+    extractFromHpt :: Maybe LiquidLibBytes
     extractFromHpt = do
-      modInfo <- lookupHpt hpt (moduleName thisModule)
-      guard (thisModule == (mi_module . hm_iface $ modInfo))
-      xs <- mapM (fromSerialized deserialise . ifAnnotatedValue) (mi_anns . hm_iface $ modInfo)
+      modInfo <- GHC.lookupHpt hpt (GHC.moduleName thisModule)
+      guard (thisModule == (GHC.mi_module . GHC.hm_iface $ modInfo))
+      xs <- mapM (GHC.fromSerialized LiquidLibBytes . GHC.ifAnnotatedValue) (GHC.mi_anns . GHC.hm_iface $ modInfo)
       listToMaybe xs
 
-    deserialise :: [B.Word8] -> a
-    deserialise payload = B.decode (B.pack payload)
+newtype LiquidLibBytes = LiquidLibBytes { unLiquidLibBytes :: [Word8] }
+
+-- | Serialise a 'LiquidLib', removing the termination checks from the target.
+serialiseLiquidLib :: LiquidLib -> GHC.Module -> IO GHC.Annotation
+serialiseLiquidLib lib thisModule = do
+    bs <- encodeLiquidLib lib
+    return $ GHC.Annotation
+      (GHC.ModuleTarget thisModule)
+      (GHC.toSerialized unLiquidLibBytes (LiquidLibBytes $ B.unpack bs))
+
+deserialiseLiquidLib
+  :: GHC.Module
+  -> GHC.ExternalPackageState
+  -> GHC.HomePackageTable
+  -> GHC.NameCache
+  -> IO (Maybe LiquidLib)
+deserialiseLiquidLib thisModule eps hpt nameCache = do
+    let mlibbs = getLiquidLibBytes thisModule eps hpt
+    case mlibbs of
+      Just (LiquidLibBytes ws) -> do
+        let bs = B.pack ws
+        Just <$> decodeLiquidLib nameCache bs
+      _ -> return Nothing
 
-serialiseBinaryObject :: forall a. (Binary a, Typeable a) => a -> Module -> Annotation
-serialiseBinaryObject obj thisModule = serialised
+deserialiseLiquidLibFromEPS
+  :: GHC.Module
+  -> GHC.ExternalPackageState
+  -> GHC.NameCache
+  -> IO (Maybe LiquidLib)
+deserialiseLiquidLibFromEPS thisModule eps nameCache = do
+    let mlibbs = getLiquidLibBytesFromEPS thisModule eps
+    case mlibbs of
+      Just (LiquidLibBytes ws) -> do
+        let bs = B.pack ws
+        Just <$> decodeLiquidLib nameCache bs
+      _ -> return Nothing
+
+encodeLiquidLib :: LiquidLib -> IO B.ByteString
+encodeLiquidLib lib0 = do
+    let (lib1, ns) = collectLHNames lib0
+    bh <- GHC.openBinMem (1024*1024)
+    GHC.putWithUserData GHC.QuietBinIFace bh ns
+    GHC.withBinBuffer bh $ \bs ->
+      return $ Builder.toLazyByteString $ B.execPut (B.put lib1) <> Builder.fromByteString bs
+
+decodeLiquidLib :: GHC.NameCache -> B.ByteString -> IO LiquidLib
+decodeLiquidLib nameCache bs0 = do
+    case B.decodeOrFail bs0 of
+      Left (_, _, err) -> error $ "decodeLiquidLib: decodeOrFail: " ++ err
+      Right (bs1, _, lib) -> do
+        bh <- GHC.unsafeUnpackBinBuffer $ B.toStrict bs1
+        ns <- GHC.getWithUserData nameCache bh
+        let n = fromIntegral $ length ns
+            arr = Array.listArray (0, n - 1) ns
+        return $ mapLHNames (resolveLHNameIndex arr) lib
   where
-    serialised :: Annotation
-    serialised = Annotation (ModuleTarget thisModule) (toSerialized (B.unpack . B.encode) obj)
+    resolveLHNameIndex :: Array.Array Word LHResolvedName -> LHName -> LHName
+    resolveLHNameIndex arr lhname =
+      case getLHNameResolved lhname of
+        LHRIndex i ->
+          if i <= snd (Array.bounds arr) then
+            makeResolvedLHName (arr Array.! i) (getLHNameSymbol lhname)
+          else
+            error $ "decodeLiquidLib: index out of bounds: " ++ show (i, Array.bounds arr)
+        _ ->
+          lhname
 
--- | Serialise a 'LiquidLib', removing the termination checks from the target.
-serialiseLiquidLib :: LiquidLib -> Module -> Annotation
-serialiseLiquidLib lib = serialiseBinaryObject @LiquidLib lib
+newtype AccF a b = AccF { unAccF :: a -> b -> (a, b) }
 
-deserialiseLiquidLib :: Module -> ExternalPackageState -> HomePackageTable -> Maybe LiquidLib
-deserialiseLiquidLib thisModule = deserialiseBinaryObject @LiquidLib thisModule
+collectLHNames :: Data a => a -> (a, [LHResolvedName])
+collectLHNames t =
+    let ((_, _, xs), t') = go (0, M.empty, []) t
+     in (t', reverse xs)
+  where
+    go
+      :: Data a
+      => (Word, M.HashMap LHResolvedName Word, [LHResolvedName])
+      -> a
+      -> ((Word, M.HashMap LHResolvedName Word, [LHResolvedName]), a)
+    go = gmapAccumT $ unAccF $ AccF go `ext0` AccF collectName
 
-deserialiseLiquidLibFromEPS :: Module -> ExternalPackageState -> Maybe LiquidLib
-deserialiseLiquidLibFromEPS = deserialiseBinaryObjectFromEPS @LiquidLib
+    collectName acc@(sz, m, xs) n = case M.lookup n m of
+      Just i -> (acc, LHRIndex i)
+      Nothing -> ((sz + 1, M.insert n sz m, n : xs), LHRIndex sz)
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 72f1aa9092..ea6c7b5bca 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
@@ -51,7 +51,7 @@ findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do
     loadRelevantSpec :: ExternalPackageState -> Module -> TcM SpecFinderResult
     loadRelevantSpec eps currentModule = do
       res <- liftIO $ runMaybeT $
-        lookupInterfaceAnnotations eps (ue_hpt $ hsc_unit_env hscEnv) currentModule
+        lookupInterfaceAnnotations eps (ue_hpt $ hsc_unit_env hscEnv) (hsc_NC hscEnv) currentModule
       case res of
         Nothing         -> do
           mAssm <- loadModuleLHAssumptionsIfAny currentModule
@@ -71,7 +71,7 @@ findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do
           -- read the EPS again
           eps2 <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv)
           -- now look up the assumptions
-          liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assumptionsMod
+          liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 (hsc_NC hscEnv) assumptionsMod
         FoundMultiple{} -> failWithTc $ mkTcRnUnknownMessage $ mkPlainError [] $
                              missingInterfaceErrorDiagnostic (initIfaceMessageOpts $ hsc_dflags hscEnv) $
                              cannotFindModule hscEnv assumptionsModName res
@@ -85,14 +85,14 @@ findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do
       mkModuleNameFS $ moduleNameFS (moduleName m) <> "_LHAssumptions"
 
 -- | Load specs from an interface file.
-lookupInterfaceAnnotations :: ExternalPackageState -> HomePackageTable -> SpecFinder m
-lookupInterfaceAnnotations eps hpt thisModule = do
-  lib <- MaybeT $ pure $ Serialisation.deserialiseLiquidLib thisModule eps hpt
+lookupInterfaceAnnotations :: ExternalPackageState -> HomePackageTable -> NameCache -> SpecFinder m
+lookupInterfaceAnnotations eps hpt nameCache thisModule = do
+  lib <- MaybeT $ Serialisation.deserialiseLiquidLib thisModule eps hpt nameCache
   pure $ LibFound thisModule lib
 
-lookupInterfaceAnnotationsEPS :: ExternalPackageState -> SpecFinder m
-lookupInterfaceAnnotationsEPS eps thisModule = do
-  lib <- MaybeT $ pure $ Serialisation.deserialiseLiquidLibFromEPS thisModule eps
+lookupInterfaceAnnotationsEPS :: ExternalPackageState -> NameCache -> SpecFinder m
+lookupInterfaceAnnotationsEPS eps nameCache thisModule = do
+  lib <- MaybeT $ Serialisation.deserialiseLiquidLibFromEPS thisModule eps nameCache
   pure $ LibFound thisModule lib
 
 -- | Returns a list of 'StableModule's which can be filtered out of the dependency list, because they are
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Types.hs
index 38809b979b..434ba922df 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Types.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
 
 module Language.Haskell.Liquid.GHC.Plugin.Types
@@ -29,6 +30,7 @@ module Language.Haskell.Liquid.GHC.Plugin.Types
     ) where
 
 import           Data.Binary                             as B
+import           Data.Data                               ( Data )
 import           GHC.Generics                      hiding ( moduleName )
 
 import qualified Data.HashSet        as HS
@@ -47,7 +49,7 @@ data LiquidLib = LiquidLib
   -- ^ The target /LiftedSpec/.
   ,  llDeps   :: TargetDependencies
   -- ^ The specs which were necessary to produce the target 'BareSpec'.
-  } deriving (Show, Generic)
+  } deriving (Show, Data, Generic)
 
 instance B.Binary LiquidLib
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
new file mode 100644
index 0000000000..35b923c698
--- /dev/null
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -0,0 +1,228 @@
+-- | This module provides a GHC 'Plugin' that allows LiquidHaskell to be hooked directly into GHC's
+-- compilation pipeline, facilitating its usage and adoption.
+
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE RecordWildCards            #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE TypeApplications           #-}
+
+module Language.Haskell.Liquid.LHNameResolution
+  ( collectTypeAliases
+  , resolveLHNames
+  , exprArg
+  ) where
+
+import           Liquid.GHC.API         as GHC hiding (Expr, panic)
+import qualified  Language.Haskell.Liquid.GHC.Misc        as LH
+import           Language.Haskell.Liquid.Types.Names
+import           Language.Haskell.Liquid.Types.RType
+
+import           Control.Monad.Writer
+import           Data.Data (Data, gmapT)
+import           Data.Generics (extT)
+
+
+import qualified Data.HashSet                            as HS
+import qualified Data.HashMap.Strict                     as HM
+
+import           Language.Fixpoint.Types hiding (Error, panic)
+import           Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic)
+import           Language.Haskell.Liquid.Types.Specs
+import           Language.Haskell.Liquid.Types.Types
+
+import qualified Text.PrettyPrint.HughesPJ as PJ
+import qualified Text.Printf               as Printf
+
+-- | Collects type aliases from the current module and its dependencies.
+collectTypeAliases
+  :: Module
+  -> BareSpec
+  -> [(StableModule, LiftedSpec)]
+  -> HM.HashMap Symbol (GHC.Module, RTAlias Symbol BareType)
+collectTypeAliases m bs deps =
+    let spec = getBareSpec bs
+        bsAliases = [ (rtName a, (m, a)) | a <- map val (aliases spec) ]
+        depAliases =
+          [ (rtName a, (unStableModule sm, a))
+          | (sm, lspec) <- deps
+          , a <- map val (HS.toList $ liftedAliases lspec)
+          ]
+     in
+        HM.fromList $ bsAliases ++ depAliases
+
+-- | Converts occurrences of LHNUnresolved to LHNResolved using the provided
+-- type aliases and GlobalRdrEnv.
+resolveLHNames
+  :: HM.HashMap Symbol (Module, RTAlias Symbol BareType)
+  -> GlobalRdrEnv
+  -> BareSpec
+  -> Either [Error] BareSpec
+resolveLHNames taliases globalRdrEnv =
+    (\(bs, es) -> if null es then Right bs else Left es) .
+    runWriter .
+    mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) .
+    fixExpressionArgsOfTypeAliases taliases
+  where
+    resolveLHName lname = case val lname of
+      LHNUnresolved LHTcName s
+        | isTuple s ->
+          pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s
+        | isList s ->
+          pure $ LHNResolved (LHRGHC GHC.listTyConName) s
+        | s == "*" ->
+          pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s
+        | otherwise ->
+          case HM.lookup s taliases of
+            Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m) s
+            Nothing -> case GHC.lookupGRE globalRdrEnv (mkLookupGRE LHTcName s) of
+              [e] -> pure $ LHNResolved (LHRGHC $ GHC.greName e) s
+              es@(_:_) -> do
+                tell [ErrDupNames
+                        (LH.fSrcSpan lname)
+                        (pprint s)
+                        (map (PJ.text . showPprUnsafe) es)
+                     ]
+                pure $ val lname
+              [] -> do
+                tell [errResolve "type constructor" "Cannot resolve name" (s <$ lname)]
+                pure $ val lname
+      LHNUnresolved LHDataConName s ->
+          case GHC.lookupGRE globalRdrEnv (mkLookupGRE LHDataConName s) of
+            [e] ->
+              pure $ LHNResolved (LHRGHC $ GHC.greName e) s
+            es@(_:_) -> do
+              tell [ErrDupNames
+                      (LH.fSrcSpan lname)
+                      (pprint s)
+                      (map (PJ.text . showPprUnsafe) es)
+                   ]
+              pure $ val lname
+            [] -> do
+              tell [errResolve "data constructor" "Cannot resolve name" (s <$ lname)]
+              pure $ val lname
+      n@(LHNResolved (LHRLocal _) _) -> pure n
+      n ->
+        let sp = Just $ LH.sourcePosSrcSpan $ loc lname
+         in panic sp $ "resolveLHNames: Unexpected resolved name: " ++ show n
+
+    errResolve :: PJ.Doc -> String -> LocSymbol -> Error
+    errResolve k msg lx = ErrResolve (LH.fSrcSpan lx) k (pprint (val lx)) (PJ.text msg)
+
+    mkLookupGRE ns s =
+      let m = LH.takeModuleNames s
+          n = LH.dropModuleNames s
+          oname = GHC.mkOccName (mkGHCNameSpace ns) $ symbolString n
+          rdrn =
+            if m == "" then
+              GHC.mkRdrUnqual oname
+            else
+              GHC.mkRdrQual (GHC.mkModuleName $ symbolString m) oname
+       in GHC.LookupRdrName rdrn GHC.SameNameSpace
+
+    mkGHCNameSpace = \case
+      LHTcName -> GHC.tcName
+      LHDataConName -> GHC.dataName
+
+    tupleArity s =
+      let a = read $ drop 5 $ symbolString s
+       in if a > 64 then
+            error $ "tupleArity: Too large (more than 64): " ++ show a
+          else
+            a
+
+-- | Changes unresolved names to local resolved names in the body of type
+-- aliases.
+resolveBoundVarsInTypeAliases :: BareSpec -> BareSpec
+resolveBoundVarsInTypeAliases = updateAliases resolveBoundVars
+  where
+    resolveBoundVars boundVars = \case
+      LHNUnresolved LHTcName s ->
+        if elem s boundVars then
+          LHNResolved (LHRLocal s) s
+        else
+          LHNUnresolved LHTcName s
+      n ->
+        error $ "resolveLHNames: Unexpected resolved name: " ++ show n
+
+    -- Applies a function to the body of type aliases, passes to every call the
+    -- arguments of the alias.
+    updateAliases f bs =
+      let spec = getBareSpec bs
+       in MkBareSpec spec
+            { aliases = [ Loc sp0 sp1 (a { rtBody = mapLHNames (f args) (rtBody a) })
+                        | Loc sp0 sp1 a <- aliases spec
+                        , let args = rtTArgs a ++ rtVArgs a
+                        ]
+            }
+
+-- | The expression arguments of type aliases are initially parsed as
+-- types. This function converts them to expressions.
+--
+-- For instance, in @Prop (Ev (plus n n))@ where `Prop` is the alias
+--
+-- > {-@ type Prop E = {v:_ | prop v = E} @-}
+--
+-- the parser builds a type for @Ev (plus n n)@.
+--
+fixExpressionArgsOfTypeAliases
+  :: HM.HashMap Symbol (Module, RTAlias Symbol BareType)
+  -> BareSpec
+  -> BareSpec
+fixExpressionArgsOfTypeAliases taliases =
+    mapBareTypes go . resolveBoundVarsInTypeAliases
+  where
+    go :: BareType -> BareType
+    go (RApp c@(BTyCon { btc_tc = Loc _ _ (LHNUnresolved LHTcName s) }) ts rs r)
+      | Just (_, rta) <- HM.lookup s taliases =
+        RApp c (fixExprArgs (btc_tc c) rta (map go ts)) (map goRef rs) r
+    go (RApp c ts rs r) =
+        RApp c (map go ts) (map goRef rs) r
+    go (RAppTy t1 t2 r)  = RAppTy (go t1) (go t2) r
+    go (RFun  x i t1 t2 r) = RFun  x i (go t1) (go t2) r
+    go (RAllT a t r)     = RAllT a (go t) r
+    go (RAllP a t)       = RAllP a (go t)
+    go (RAllE x t1 t2)   = RAllE x (go t1) (go t2)
+    go (REx x t1 t2)     = REx   x (go t1) (go t2)
+    go (RRTy e r o t)    = RRTy  e r o     (go t)
+    go t@RHole{}         = t
+    go t@RVar{}          = t
+    go t@RExprArg{}      = t
+    goRef (RProp ss t)   = RProp ss (go t)
+
+    fixExprArgs lname rta ts =
+      let n = length (rtTArgs rta)
+          (targs, eargs) = splitAt n ts
+          msg = "FIX-EXPRESSION-ARG: " ++ showpp (rtName rta)
+          toExprArg = exprArg (LH.fSourcePos lname) msg
+       in targs ++ [ RExprArg $ toExprArg e <$ lname | e <- eargs ]
+
+mapBareTypes :: (BareType -> BareType) -> BareSpec -> BareSpec
+mapBareTypes f  = go
+  where
+    go :: Data a => a -> a
+    go = gmapT (go `extT` f)
+
+-- | exprArg converts a tyVar to an exprVar because parser cannot tell
+--   this function allows us to treating (parsed) "types" as "value"
+--   arguments, e.g. type Matrix a Row Col = List (List a Row) Col
+--   Note that during parsing, we don't necessarily know whether a
+--   string is a type or a value expression. E.g. in tests/pos/T1189.hs,
+--   the string `Prop (Ev (plus n n))` where `Prop` is the alias:
+--     {-@ type Prop E = {v:_ | prop v = E} @-}
+--   the parser will chomp in `Ev (plus n n)` as a `BareType` and so
+--   `exprArg` converts that `BareType` into an `Expr`.
+exprArg :: SourcePos -> String -> BareType -> Expr
+exprArg l msg = notracepp ("exprArg: " ++ msg) . go
+  where
+    go :: BareType -> Expr
+    go (RExprArg e)     = val e
+    go (RVar x _)       = EVar (symbol x)
+    go (RApp x [] [] _) = EVar (symbol x)
+    go (RApp f ts [] _) = mkEApp (symbol <$> btc_tc f) (go <$> ts)
+    go (RAppTy t1 t2 _) = EApp (go t1) (go t2)
+    go z                = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show z) msg
+    sp                  = Just (LH.sourcePosSrcSpan l)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs
index e3e3e0447a..3e6444e34b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs
@@ -14,7 +14,7 @@ module Language.Haskell.Liquid.Transforms.ANF (anormalize) where
 import           Debug.Trace (trace)
 import           Prelude                          hiding (error)
 import           Language.Haskell.Liquid.GHC.TypeRep
-import           Liquid.GHC.API  as Ghc hiding ( mkTyArg
+import           Liquid.GHC.API  as Ghc hiding ( get, mkTyArg
                                                                 , showPpr
                                                                 , DsM
                                                                 , panic)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
index 367b0d11d5..5c3e4f47b0 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
@@ -25,7 +25,7 @@ import           Data.Bifunctor (first)
 import           Data.ByteString                       (ByteString)
 import           Prelude                               hiding (error)
 import           Language.Haskell.Liquid.GHC.TypeRep   () -- needed for Eq 'Type'
-import           Liquid.GHC.API       hiding (Expr, Located, panic)
+import           Liquid.GHC.API       hiding (Expr, Located, get, panic)
 import qualified Liquid.GHC.API       as Ghc
 import qualified Liquid.GHC.API       as C
 import qualified Data.List                             as L
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs
index d2d699d5a3..e0a85e344c 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs
@@ -24,7 +24,7 @@ module Language.Haskell.Liquid.Transforms.Rewrite
 
   ) where
 
-import           Liquid.GHC.API as Ghc hiding (showPpr, substExpr)
+import           Liquid.GHC.API as Ghc hiding (get, showPpr, substExpr)
 import           Language.Haskell.Liquid.GHC.TypeRep ()
 import           Data.Maybe     (fromMaybe, isJust, mapMaybe)
 import           Control.Monad.State hiding (lift)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index e17eef7579..d7d6279f96 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -10,7 +10,7 @@ module Language.Haskell.Liquid.Types.Names
   , selfSymbol
   , LogicName (..)
   , LHResolvedName (..)
-  , LHName
+  , LHName (..)
   , LHNameSpace (..)
   , makeResolvedLHName
   , getLHNameResolved
@@ -25,6 +25,7 @@ import qualified Data.Binary as B
 import Data.Data (Data, gmapM, gmapT)
 import Data.Generics (extM, extT)
 import Data.Hashable
+import Data.String (fromString)
 import GHC.Generics
 import GHC.Stack
 import Language.Fixpoint.Types
@@ -128,6 +129,23 @@ instance B.Binary LHResolvedName where
   put (LHRLocal s) = B.putWord8 0 >> B.put (symbolString s)
   put (LHRIndex n) = B.putWord8 1 >> B.put n
 
+instance GHC.Binary LHResolvedName where
+  get bh = do
+    tag <- GHC.getByte bh
+    case tag of
+      0 -> LHRLogic <$> GHC.get bh
+      1 -> LHRGHC <$> GHC.get bh
+      2 -> LHRLocal . fromString <$> GHC.get bh
+      _ -> error "GHC.Binary: invalid tag for LHResolvedName"
+  put_ bh (LHRLogic n) = GHC.putByte bh 0 >> GHC.put_ bh n
+  put_ bh (LHRGHC n) = GHC.putByte bh 1 >> GHC.put_ bh n
+  put_ bh (LHRLocal n) = GHC.putByte bh 2 >> GHC.put_ bh (symbolString n)
+  put_ _bh (LHRIndex _n) = error "GHC.Binary: cannot serialize LHRIndex"
+
+instance GHC.Binary LogicName where
+  get bh = LogicName . fromString <$> GHC.get bh <*> GHC.get bh
+  put_ bh (LogicName s m) = GHC.put_ bh (symbolString s) >> GHC.put_ bh m
+
 instance PPrint LHName where
   pprintTidy _ = text . show
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs
index 5b43e129aa..da757e55dc 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs
@@ -119,7 +119,7 @@ import           Language.Haskell.Liquid.Misc
 import           Language.Haskell.Liquid.Types.Names
 import qualified Language.Haskell.Liquid.GHC.Misc as GM
 import           Language.Haskell.Liquid.GHC.Play (mapType, stringClassArg, isRecursivenewTyCon)
-import           Liquid.GHC.API        as Ghc hiding ( Expr
+import           Liquid.GHC.API        as Ghc hiding ( Expr, get
                                                                       , Located
                                                                       , tyConName
                                                                       , punctuate
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index 69016cb09c..64dfb9364f 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -4,6 +4,7 @@
 
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE DeriveDataTypeable         #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DerivingVia                #-}
 {-# LANGUAGE StandaloneDeriving         #-}
@@ -71,6 +72,7 @@ import           GHC.Generics            hiding (to, moduleName)
 import           Data.Binary
 import qualified Language.Fixpoint.Types as F
 import           Language.Fixpoint.Misc (sortNub)
+import           Data.Data (Data)
 import           Data.Hashable
 import qualified Data.HashSet            as S
 import           Data.HashSet            (HashSet)
@@ -82,7 +84,7 @@ import           Language.Haskell.Liquid.Types.Types
 import           Language.Haskell.Liquid.Types.Variance
 import           Language.Haskell.Liquid.Types.Bounds
 import           Language.Haskell.Liquid.UX.Config
-import           Liquid.GHC.API hiding (text, (<+>))
+import           Liquid.GHC.API hiding (Binary, text, (<+>))
 import           Language.Haskell.Liquid.GHC.Types
 import           Text.PrettyPrint.HughesPJ              (text, (<+>))
 import           Text.PrettyPrint.HughesPJ as HughesPJ (($$))
@@ -379,7 +381,7 @@ type SpecMeasure   = Measure LocSpecType DataCon
 -- to undefined or out-of-scope entities.
 newtype BareSpec =
   MkBareSpec { getBareSpec :: Spec LocBareType F.LocSymbol }
-  deriving (Generic, Show, Binary)
+  deriving (Data, Generic, Show, Binary)
 
 instance Semigroup BareSpec where
   x <> y = MkBareSpec { getBareSpec = getBareSpec x <> getBareSpec y }
@@ -440,7 +442,7 @@ data Spec ty bndr  = Spec
   , dsize      :: ![([ty], F.LocSymbol)]                              -- ^ Size measure to enforce fancy termination
   , bounds     :: !(RRBEnv ty)
   , axeqs      :: ![F.Equation]                                       -- ^ Equalities used for Proof-By-Evaluation
-  } deriving (Generic, Show)
+  } deriving (Data, Generic, Show)
 
 instance Binary (Spec LocBareType F.LocSymbol)
 
@@ -633,7 +635,7 @@ data LiftedSpec = LiftedSpec
   , liftedBounds     :: RRBEnv LocBareType
   , liftedAxeqs      :: HashSet F.Equation
     -- ^ Equalities used for Proof-By-Evaluation
-  } deriving (Eq, Generic, Show)
+  } deriving (Eq, Data, Generic, Show)
     deriving Hashable via Generically LiftedSpec
     deriving Binary   via Generically LiftedSpec
 
@@ -677,7 +679,7 @@ emptyLiftedSpec = LiftedSpec
 -- | The /target/ dependencies that concur to the creation of a 'TargetSpec' and a 'LiftedSpec'.
 newtype TargetDependencies =
   TargetDependencies { getDependencies :: HashMap StableModule LiftedSpec }
-  deriving (Eq, Show, Generic)
+  deriving (Data, Eq, Show, Generic)
   deriving Binary via Generically TargetDependencies
 
 -- instance S.Store TargetDependencies
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Variance.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Variance.hs
index f0cf833e30..c955e14870 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Variance.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Variance.hs
@@ -25,7 +25,7 @@ import qualified Data.HashSet            as S
 import qualified Language.Fixpoint.Types as F
 
 import qualified Language.Haskell.Liquid.GHC.Misc as GM
-import           Liquid.GHC.API        as Ghc hiding (text)
+import           Liquid.GHC.API        as Ghc hiding (Binary, text)
 
 type VarianceInfo = [Variance]