Resolve LHNames and serialize them and deserialize them

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

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 ((<>))

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

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

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)

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

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 ----------------------------------------

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))
 
 

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