From 5b2fb1241c0c5a3d44525a67f5d7e0512db08640 Mon Sep 17 00:00:00 2001 From: Gergo ERDI Date: Mon, 14 Oct 2024 05:08:53 +0100 Subject: [PATCH 1/4] Use real `typecheckModule` and `desugarModule` API from GHC --- liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs | 13 +++-- .../src-ghc/Liquid/GHC/API/Extra.hs | 50 ------------------- .../src/Language/Haskell/Liquid/GHC/Misc.hs | 10 ---- .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 26 ++++++---- 4 files changed, 24 insertions(+), 75 deletions(-) diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs index 00a94eb952..91ede4f7b2 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs @@ -23,7 +23,7 @@ import GHC as Ghc ( Class , DataCon , DesugaredModule(DesugaredModule, dm_typechecked_module, dm_core_module) - , DynFlags(backend, debugLevel, ghcLink, ghcMode) + , DynFlags(backend, debugLevel, ghcLink, ghcMode, warningFlags) , FixityDirection(InfixN, InfixR) , FixitySig(FixitySig) , GenLocated(L) @@ -81,9 +81,11 @@ import GHC as Ghc , TypecheckedModule(tm_checked_module_info, tm_internals_, tm_parsed_module) , classMethods , classSCTheta + , coreModule , dataConTyCon , dataConFieldLabels , dataConWrapperType + , desugarModule , getLocA , getLogger , getName @@ -154,6 +156,7 @@ import GHC as Ghc , tyConDataCons , tyConKind , tyConTyVars + , typecheckModule , unLoc ) @@ -413,8 +416,7 @@ import GHC.Driver.Config.Diagnostic as Ghc , initIfaceMessageOpts ) import GHC.Driver.Main as Ghc - ( hscDesugar - , hscTcRcLookupName + ( hscTcRcLookupName ) import GHC.Driver.Plugins as Ghc ( ParsedResult(..) @@ -428,7 +430,7 @@ import GHC.Driver.Session as Ghc , updOptLevel , xopt_set ) -import GHC.Driver.Monad as Ghc (withSession) +import GHC.Driver.Monad as Ghc (withSession, reflectGhc, Session(..)) import GHC.HsToCore.Monad as Ghc ( DsM, initDsTc, initDsWithModGuts, newUnique ) import GHC.Iface.Syntax as Ghc @@ -452,6 +454,7 @@ import GHC.Driver.Backend as Ghc (interpreterBackend) import GHC.Driver.Env as Ghc ( HscEnv(hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins) , Hsc + , hscSetFlags, hscUpdateFlags ) import GHC.Driver.Errors as Ghc ( printMessages ) @@ -499,6 +502,7 @@ import GHC.Tc.Utils.Monad as Ghc ( captureConstraints , discardConstraints , getEnv + , getTopEnv , failIfErrsM , failM , failWithTc @@ -510,6 +514,7 @@ import GHC.Tc.Utils.Monad as Ghc , reportDiagnostic , reportDiagnostics , updEnv + , updTopEnv ) import GHC.Tc.Utils.TcType as Ghc (tcSplitDFunTy, tcSplitMethodTy) import GHC.Tc.Zonk.Type as Ghc diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs index 8550e700f0..8f01f46796 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs @@ -10,14 +10,12 @@ module Liquid.GHC.API.Extra ( , apiComments , apiCommentsParsedSource , dataConSig - , desugarModuleIO , fsToUnitId , isPatErrorAlt , lookupModSummary , minus_RDR , modInfoLookupNameIO , moduleInfoTc - , parseModuleIO , qualifiedNameFS , relevantModules , renderWithStyle @@ -28,7 +26,6 @@ module Liquid.GHC.API.Extra ( , strictNothing , thisPackage , tyConRealArity - , typecheckModuleIO , untick ) where @@ -49,7 +46,6 @@ import GHC.Core.Make (pAT_ERROR_ID) import GHC.Core.Type as Ghc hiding (typeKind , isPredTy, extendCvSubst, linear) import GHC.Data.Bag (bagToList) import GHC.Data.FastString as Ghc -import qualified GHC.Data.EnumSet as EnumSet import GHC.Data.Maybe import qualified GHC.Data.Strict import GHC.Driver.Env @@ -146,52 +142,6 @@ relevantModules mg modGuts = used `S.union` dependencies UsageMergedRequirement { usg_mod = modl } -> modl : acc _ -> acc --- --- Parsing, typechecking and desugaring a module --- -parseModuleIO :: HscEnv -> ModSummary -> IO ParsedModule -parseModuleIO hscEnv ms = do - let hsc_env_tmp = hscEnv { hsc_dflags = ms_hspp_opts ms } - hpm <- hscParse hsc_env_tmp ms - return (ParsedModule ms (hpm_module hpm) (hpm_src_files hpm)) - --- | Our own simplified version of 'TypecheckedModule'. -data TypecheckedModuleLH = TypecheckedModuleLH { - tmlh_parsed_module :: ParsedModule - , tmlh_renamed_source :: Maybe RenamedSource - , tmlh_mod_summary :: ModSummary - , tmlh_gbl_env :: TcGblEnv - } - -typecheckModuleIO :: HscEnv -> ParsedModule -> IO TypecheckedModuleLH -typecheckModuleIO hscEnv pmod = do - -- Suppress all the warnings, so that they won't be printed (which would result in them being - -- printed twice, one by GHC and once here). - let ms = pm_mod_summary pmod - let dynFlags' = ms_hspp_opts ms - let hsc_env_tmp = hscEnv { hsc_dflags = dynFlags' { warningFlags = EnumSet.empty } } - (tc_gbl_env, rn_info) - <- hscTypecheckRename hsc_env_tmp ms $ - HsParsedModule { hpm_module = parsedSource pmod, - hpm_src_files = pm_extra_src_files pmod } - return TypecheckedModuleLH { - tmlh_parsed_module = pmod - , tmlh_renamed_source = rn_info - , tmlh_mod_summary = ms - , tmlh_gbl_env = tc_gbl_env - } - --- | Desugar a typechecked module. -desugarModuleIO :: HscEnv -> ModSummary -> TypecheckedModuleLH -> IO ModGuts -desugarModuleIO hscEnv originalModSum typechecked = do - -- See [NOTE:ghc810] on why we override the dynFlags here before calling 'desugarModule'. - let modSum = originalModSum { ms_hspp_opts = hsc_dflags hscEnv } - let parsedMod' = (tmlh_parsed_module typechecked) { pm_mod_summary = modSum } - let typechecked' = typechecked { tmlh_parsed_module = parsedMod' } - - let hsc_env_tmp = hscEnv { hsc_dflags = ms_hspp_opts (tmlh_mod_summary typechecked') } - hscDesugar hsc_env_tmp (tmlh_mod_summary typechecked') (tmlh_gbl_env typechecked') - -- | Abstraction of 'EpaComment'. data ApiComment = ApiLineComment String diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs index d58cf68f37..9726e920f5 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -623,16 +623,6 @@ stripParens t = fromMaybe t (strip t) stripParensSym :: Symbol -> Symbol stripParensSym (symbolText -> t) = symbol (stripParens t) -desugarModule :: TypecheckedModule -> Ghc DesugaredModule -desugarModule tcm = do - let ms = pm_mod_summary $ tm_parsed_module tcm - -- let ms = modSummary tcm - let (tcg, _) = tm_internals_ tcm - hsc_env <- getSession - let hsc_env_tmp = hsc_env { hsc_dflags = ms_hspp_opts ms } - guts <- liftIO $ hscDesugar{- WithLoc -} hsc_env_tmp ms tcg - return DesugaredModule { dm_typechecked_module = tcm, dm_core_module = guts } - -------------------------------------------------------------------------------- -- | GHC Compatibility Layer --------------------------------------------------- -------------------------------------------------------------------------------- diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs index 0943dd611b..e7d5cb0d58 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -309,8 +309,6 @@ typecheckHook' cfg0 modSummary0 parsed0 tcGblEnv = do let modSummary = updateModSummaryDynFlags unoptimiseDynFlags modSummary0 thisFile = LH.modSummaryHsFile modSummary - env0 <- env_top <$> getEnv - let env = env0 { hsc_dflags = ms_hspp_opts modSummary } let specComments = map mkSpecComment $ LH.extractSpecComments parsed0 parsed = addNoInlinePragmasToLocalBinds parsed0 @@ -323,19 +321,23 @@ typecheckHook' cfg0 modSummary0 parsed0 tcGblEnv = do let modSummary2 = updateModSummaryDynFlags (maybeInsertBreakPoints cfg) modSummary parsed2 = parsed { pm_mod_summary = modSummary2 } - env2 = env { hsc_dflags = ms_hspp_opts modSummary2 } - typechecked <- liftIO $ typecheckModuleIO env2 (LH.ignoreInline parsed2) - resolvedNames <- liftIO $ LH.lookupTyThings env2 tcGblEnv - availTyCons <- liftIO $ LH.availableTyCons env2 tcGblEnv (tcg_exports tcGblEnv) - availVars <- liftIO $ LH.availableVars env2 tcGblEnv (tcg_exports tcGblEnv) + updTopEnv (hscUpdateFlags noWarnings . hscSetFlags (ms_hspp_opts modSummary2)) $ do + env2 <- getTopEnv - unoptimisedGuts <- liftIO $ desugarModuleIO env2 modSummary2 typechecked + pipelineData <- liftIO $ do + session <- Session <$> newIORef env2 + flip reflectGhc session $ do + typechecked <- typecheckModule (LH.ignoreInline parsed2) + unoptimisedGuts <- desugarModule typechecked - let tcData = mkTcData (tcg_rn_imports tcGblEnv) resolvedNames availTyCons availVars - let pipelineData = PipelineData unoptimisedGuts tcData specs + resolvedNames <- liftIO $ LH.lookupTyThings env2 tcGblEnv + availTyCons <- liftIO $ LH.availableTyCons env2 tcGblEnv (tcg_exports tcGblEnv) + availVars <- liftIO $ LH.availableVars env2 tcGblEnv (tcg_exports tcGblEnv) + + let tcData = mkTcData (tcg_rn_imports tcGblEnv) resolvedNames availTyCons availVars + return $ PipelineData (coreModule unoptimisedGuts) tcData specs - updEnv (\e -> e {env_top = env2}) $ liquidHaskellCheckWithConfig cfg pipelineData modSummary2 tcGblEnv where @@ -346,6 +348,8 @@ typecheckHook' cfg0 modSummary0 parsed0 tcGblEnv = do updateModSummaryDynFlags f ms = ms { ms_hspp_opts = f (ms_hspp_opts ms) } + noWarnings dflags = dflags { warningFlags = mempty } + serialiseSpec :: Module -> TcGblEnv -> LiquidLib -> TcM TcGblEnv serialiseSpec thisModule tcGblEnv liquidLib = do -- --- From e063938f2cde0e808a2212da6317ecc0ac6c3fe0 Mon Sep 17 00:00:00 2001 From: Gergo ERDI Date: Mon, 14 Oct 2024 08:27:07 +0100 Subject: [PATCH 2/4] Do more *with* the GHC API instead of *instead of it*. --- liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs | 5 +- .../src-ghc/Liquid/GHC/API/Extra.hs | 16 ++--- .../Language/Haskell/Liquid/GHC/Interface.hs | 63 +++++++------------ .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 7 ++- 4 files changed, 34 insertions(+), 57 deletions(-) diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs index 91ede4f7b2..1126b7cd4b 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs @@ -37,6 +37,7 @@ import GHC as Ghc , GhcException(CmdLineError, ProgramError) , GhcLink(LinkInMemory) , GhcMode(CompManager) + , GhcMonad , GhcPs , GhcRn , HsDecl(SigD) @@ -111,6 +112,7 @@ import GHC as Ghc , isRecordSelector , isTypeSynonymTyCon , isVanillaDataCon + , lookupName , mkHsApp , mkHsDictLet , mkHsForAllInvisTele @@ -415,9 +417,6 @@ import GHC.Driver.Config.Diagnostic as Ghc , initDsMessageOpts , initIfaceMessageOpts ) -import GHC.Driver.Main as Ghc - ( hscTcRcLookupName - ) import GHC.Driver.Plugins as Ghc ( ParsedResult(..) ) diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs index 8f01f46796..063cd656f5 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs @@ -14,7 +14,7 @@ module Liquid.GHC.API.Extra ( , isPatErrorAlt , lookupModSummary , minus_RDR - , modInfoLookupNameIO + , modInfoLookupName , moduleInfoTc , qualifiedNameFS , relevantModules @@ -31,7 +31,7 @@ module Liquid.GHC.API.Extra ( import Control.Monad.IO.Class import Liquid.GHC.API.StableModule as StableModule -import GHC +import GHC hiding (modInfoLookupName) import Data.Data (Data, gmapQr, gmapT) import Data.Generics (extQ, extT) import Data.Foldable (asum) @@ -59,7 +59,6 @@ import GHC.Types.SourceText (SourceText(..)) import GHC.Types.SrcLoc as Ghc import GHC.Types.TypeEnv import GHC.Types.Unique (getUnique, hasKey) -import GHC.Types.Unique.FM import GHC.Unit.Module.Deps as Ghc (Dependencies(dep_direct_mods)) import GHC.Unit.Module.Graph as Ghc @@ -225,16 +224,13 @@ lookupModSummary hscEnv mdl = do -- | Our own simplified version of 'ModuleInfo' to overcome the fact we cannot construct the \"original\" -- one as the constructor is not exported, and 'getHomeModuleInfo' and 'getPackageModuleInfo' are not -- exported either, so we had to backport them as well. -newtype ModuleInfoLH = ModuleInfoLH { minflh_type_env :: UniqFM Name TyThing } +newtype ModuleInfoLH = ModuleInfoLH { minflh_type_env :: TypeEnv } -modInfoLookupNameIO :: HscEnv - -> ModuleInfoLH - -> Name - -> IO (Maybe TyThing) -modInfoLookupNameIO hscEnv minf name = +modInfoLookupName :: (GhcMonad m) => ModuleInfoLH -> Name -> m (Maybe TyThing) +modInfoLookupName minf name = do case lookupTypeEnv (minflh_type_env minf) name of Just tyThing -> return (Just tyThing) - Nothing -> lookupType hscEnv name + Nothing -> lookupGlobalName name moduleInfoTc :: HscEnv -> TcGblEnv -> IO ModuleInfoLH moduleInfoTc hscEnv tcGblEnv = do diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs index f610e34b5c..b7ffa0d222 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs @@ -40,8 +40,7 @@ module Language.Haskell.Liquid.GHC.Interface ( , keepRawTokenStream , ignoreInline , lookupTyThings - , availableTyCons - , availableVars + , availableTyThings , updLiftedSpec ) where @@ -184,47 +183,29 @@ qImports qns = QImports -- for this module; we will use this to create our name-resolution environment -- (see `Bare.Resolve`) --------------------------------------------------------------------------------------- -lookupTyThings :: HscEnv -> TcGblEnv -> IO [(Name, Maybe TyThing)] -lookupTyThings hscEnv tcGblEnv = forM names (lookupTyThing hscEnv tcGblEnv) +lookupTyThings :: (GhcMonad m) => TcGblEnv -> m [(Name, Maybe TyThing)] +lookupTyThings tcGblEnv = mapM (lookupTyThing tcGblEnv) names where - names :: [Ghc.Name] - names = liftM2 (++) - (fmap Ghc.greName . Ghc.globalRdrEnvElts . tcg_rdr_env) - (fmap is_dfun_name . tcg_insts) tcGblEnv --- | Lookup a single 'Name' in the GHC environment, yielding back the 'Name' alongside the 'TyThing', --- if one is found. -lookupTyThing :: HscEnv -> TcGblEnv -> Name -> IO (Name, Maybe TyThing) -lookupTyThing hscEnv tcGblEnv n = do - mty <- runMaybeT $ - MaybeT (Ghc.hscTcRcLookupName hscEnv n) - `mplus` - MaybeT ( - do mi <- moduleInfoTc hscEnv tcGblEnv - modInfoLookupNameIO hscEnv mi n - ) - return (n, mty) - -availableTyThings :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [TyThing] -availableTyThings hscEnv tcGblEnv avails = + names = liftA2 (++) + (fmap Ghc.greName . Ghc.globalRdrEnvElts . tcg_rdr_env) + (fmap is_dfun_name . tcg_insts) + tcGblEnv + +lookupTyThing :: (GhcMonad m) => TcGblEnv -> Name -> m (Name, Maybe TyThing) +lookupTyThing tcGblEnv name = do + hscEnv <- getSession + mbTy <- runMaybeT . msum . map MaybeT $ + [ lookupName name + , do minf <- liftIO $ moduleInfoTc hscEnv tcGblEnv + modInfoLookupName minf name + ] + return (name, mbTy) + +availableTyThings :: (GhcMonad m) => TcGblEnv -> [AvailInfo] -> m [TyThing] +availableTyThings tcGblEnv avails = fmap catMaybes $ - mapM (fmap snd . lookupTyThing hscEnv tcGblEnv) $ - availableNames avails - --- | Returns all the available (i.e. exported) 'TyCon's (type constructors) for the input 'Module'. -availableTyCons :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [Ghc.TyCon] -availableTyCons hscEnv tcGblEnv avails = - fmap (\things -> [tyCon | (ATyCon tyCon) <- things]) (availableTyThings hscEnv tcGblEnv avails) - --- | Returns all the available (i.e. exported) 'Var's for the input 'Module'. -availableVars :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [Ghc.Var] -availableVars hscEnv tcGblEnv avails = - fmap (\things -> [var | (AnId var) <- things]) (availableTyThings hscEnv tcGblEnv avails) - -availableNames :: [AvailInfo] -> [Name] -availableNames = - concatMap $ \case - Avail n -> [n] - AvailTC n ns -> n : ns + mapM (fmap snd . lookupTyThing tcGblEnv) $ + concatMap availNames avails _dumpTypeEnv :: TypecheckedModule -> IO () _dumpTypeEnv tm = do diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs index e7d5cb0d58..0143844297 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -331,9 +331,10 @@ typecheckHook' cfg0 modSummary0 parsed0 tcGblEnv = do typechecked <- typecheckModule (LH.ignoreInline parsed2) unoptimisedGuts <- desugarModule typechecked - resolvedNames <- liftIO $ LH.lookupTyThings env2 tcGblEnv - availTyCons <- liftIO $ LH.availableTyCons env2 tcGblEnv (tcg_exports tcGblEnv) - availVars <- liftIO $ LH.availableVars env2 tcGblEnv (tcg_exports tcGblEnv) + resolvedNames <- LH.lookupTyThings tcGblEnv + avails <- LH.availableTyThings tcGblEnv (tcg_exports tcGblEnv) + let availTyCons = [ tc | ATyCon tc <- avails ] + availVars = [ var | AnId var <- avails ] let tcData = mkTcData (tcg_rn_imports tcGblEnv) resolvedNames availTyCons availVars return $ PipelineData (coreModule unoptimisedGuts) tcData specs From 6c2e11d0fa301250f7a43e59d7850ce37a3dc078 Mon Sep 17 00:00:00 2001 From: Gergo ERDI Date: Mon, 14 Oct 2024 09:35:44 +0100 Subject: [PATCH 3/4] The `ParsedModule` passed to `typecheckHook` already contains its own `ModSummary` --- .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs index 0143844297..4d9cb99cd2 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -137,7 +137,7 @@ plugin = GHC.defaultPlugin { liftIO $ printWarning logger warning pure gblEnv else do - newGblEnv <- typecheckHook cfg summary gblEnv + newGblEnv <- typecheckHook cfg gblEnv case newGblEnv of -- Exit with success if all expected errors were found Left (ErrorsOccurred []) -> pure gblEnv @@ -279,14 +279,14 @@ parsedHook _ ms parsedResult = do -- grab from parsing (again) the module by using the GHC API, so we are really -- independent from the \"normal\" compilation pipeline. -- -typecheckHook :: Config -> ModSummary -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv) -typecheckHook cfg0 modSummary0 tcGblEnv = bracket startTypechecking endTypechecking $ \case +typecheckHook :: Config -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv) +typecheckHook cfg0 tcGblEnv = bracket startTypechecking endTypechecking $ \case Just Typechecking -> -- We're being called from the `typecheckModuleIO` call in `typecheckHook`, so we avoid looping -- See 'Breadcrumb' for more information. pure $ Right tcGblEnv Just (Parsed parsed0) -> - typecheckHook' cfg0 modSummary0 parsed0 tcGblEnv + typecheckHook' cfg0 parsed0 tcGblEnv Nothing -> -- The module has been verified by an earlier call to the plugin. -- This could happen if multiple @-fplugin=LiquidHaskell@ flags are passed to GHC. @@ -303,8 +303,8 @@ typecheckHook cfg0 modSummary0 tcGblEnv = bracket startTypechecking endTypecheck Just Parsed{} -> void $ swapBreadcrumb thisModule Nothing _ -> pure () -typecheckHook' :: Config -> ModSummary -> ParsedModule -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv) -typecheckHook' cfg0 modSummary0 parsed0 tcGblEnv = do +typecheckHook' :: Config -> ParsedModule -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv) +typecheckHook' cfg0 parsed0 tcGblEnv = do debugLog $ "We are in module: " <> show (toStableModule thisModule) let modSummary = updateModSummaryDynFlags unoptimiseDynFlags modSummary0 thisFile = LH.modSummaryHsFile modSummary @@ -345,6 +345,8 @@ typecheckHook' cfg0 modSummary0 parsed0 tcGblEnv = do thisModule :: Module thisModule = tcg_mod tcGblEnv + modSummary0 = pm_mod_summary parsed0 + continue = pure $ Left (ErrorsOccurred []) updateModSummaryDynFlags f ms = ms { ms_hspp_opts = f (ms_hspp_opts ms) } From 0cc6cbc477123f1bbdc67036760316950d3d305f Mon Sep 17 00:00:00 2001 From: Gergo ERDI Date: Mon, 14 Oct 2024 09:36:49 +0100 Subject: [PATCH 4/4] Refactor all the patching that happens before the LH desugaring so that everything is done as late as possible, i.e. explicitly showing which steps require re-typechecking and which steps require re-desugaring. --- .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 108 ++++++++++-------- 1 file changed, 63 insertions(+), 45 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs index 4d9cb99cd2..98831658ad 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -306,52 +306,78 @@ typecheckHook cfg0 tcGblEnv = bracket startTypechecking endTypechecking $ \case typecheckHook' :: Config -> ParsedModule -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv) typecheckHook' cfg0 parsed0 tcGblEnv = do debugLog $ "We are in module: " <> show (toStableModule thisModule) - let modSummary = updateModSummaryDynFlags unoptimiseDynFlags modSummary0 - thisFile = LH.modSummaryHsFile modSummary - - let specComments = map mkSpecComment $ LH.extractSpecComments parsed0 - parsed = addNoInlinePragmasToLocalBinds parsed0 case parseSpecComments (coerce specComments) of Left errors -> LH.filterReportErrors thisFile GHC.failM continue (getFilters cfg0) Full errors Right specs -> + updTopEnv (hscUpdateFlags noWarnings) $ do + env <- getTopEnv + + typechecked <- liftIO $ do + session <- Session <$> newIORef env + let parsed = addNoInlinePragmasToLocalBinds parsed0 + flip reflectGhc session $ typecheckModule (LH.ignoreInline parsed) + liquidCheckModule cfg0 typechecked specs tcGblEnv - withPragmas cfg0 thisFile [s | Pragma s <- specs] $ \cfg -> do + where + ms = pm_mod_summary parsed0 - let modSummary2 = updateModSummaryDynFlags (maybeInsertBreakPoints cfg) modSummary - parsed2 = parsed { pm_mod_summary = modSummary2 } + thisModule = ms_mod ms + thisFile = LH.modSummaryHsFile ms - updTopEnv (hscUpdateFlags noWarnings . hscSetFlags (ms_hspp_opts modSummary2)) $ do - env2 <- getTopEnv + specComments = map mkSpecComment $ LH.extractSpecComments parsed0 - pipelineData <- liftIO $ do - session <- Session <$> newIORef env2 - flip reflectGhc session $ do - typechecked <- typecheckModule (LH.ignoreInline parsed2) - unoptimisedGuts <- desugarModule typechecked + continue = pure $ Left (ErrorsOccurred []) - resolvedNames <- LH.lookupTyThings tcGblEnv - avails <- LH.availableTyThings tcGblEnv (tcg_exports tcGblEnv) - let availTyCons = [ tc | ATyCon tc <- avails ] - availVars = [ var | AnId var <- avails ] + noWarnings dflags = dflags { warningFlags = mempty } - let tcData = mkTcData (tcg_rn_imports tcGblEnv) resolvedNames availTyCons availVars - return $ PipelineData (coreModule unoptimisedGuts) tcData specs +liquidCheckModule :: Config -> TypecheckedModule -> [BPspec] -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv) +liquidCheckModule cfg0 typechecked specs tcg0 = do + updTopEnv (hscUpdateFlags noWarnings) $ do + withPragmas cfg0 thisFile [s | Pragma s <- specs] $ \cfg -> do + env <- getTopEnv - liquidHaskellCheckWithConfig cfg pipelineData modSummary2 tcGblEnv + pipelineData <- liftIO $ do + session <- Session <$> newIORef env + flip reflectGhc session $ mkPipelineData cfg typechecked specs + liquidLib <- liquidHaskellCheckWithConfig cfg pipelineData ms + traverse (serialiseSpec thisModule tcg0) liquidLib where - thisModule :: Module - thisModule = tcg_mod tcGblEnv + ms = pm_mod_summary . tm_parsed_module $ typechecked - modSummary0 = pm_mod_summary parsed0 + thisModule = ms_mod ms + thisFile = LH.modSummaryHsFile ms - continue = pure $ Left (ErrorsOccurred []) + noWarnings dflags = dflags { warningFlags = mempty } - updateModSummaryDynFlags f ms = ms { ms_hspp_opts = f (ms_hspp_opts ms) } +updateModSummaryDynFlags :: (DynFlags -> DynFlags) -> ModSummary -> ModSummary +updateModSummaryDynFlags f ms = ms { ms_hspp_opts = f (ms_hspp_opts ms) } - noWarnings dflags = dflags { warningFlags = mempty } +updateTypecheckedModuleModSummary :: (ModSummary -> ModSummary) -> TypecheckedModule -> TypecheckedModule +updateTypecheckedModuleModSummary f typechecked = typechecked + { tm_parsed_module = let pm = tm_parsed_module typechecked in pm + { pm_mod_summary = let ms = pm_mod_summary pm in f ms + } + } + +mkPipelineData :: (GhcMonad m) => Config -> TypecheckedModule -> [BPspec] -> m PipelineData +mkPipelineData cfg typechecked specs = do + unoptimisedGuts <- desugarModule typechecked' + + resolvedNames <- LH.lookupTyThings tcg + avails <- LH.availableTyThings tcg (tcg_exports tcg) + let availTyCons = [ tc | ATyCon tc <- avails ] + availVars = [ var | AnId var <- avails ] + + let tcData = mkTcData (tcg_rn_imports tcg) resolvedNames availTyCons availVars + return $ PipelineData (coreModule unoptimisedGuts) tcData specs + where + typechecked' = + updateTypecheckedModuleModSummary (updateModSummaryDynFlags (maybeInsertBreakPoints cfg . unoptimiseDynFlags)) typechecked + + (tcg, _) = tm_internals_ typechecked serialiseSpec :: Module -> TcGblEnv -> LiquidLib -> TcM TcGblEnv serialiseSpec thisModule tcGblEnv liquidLib = do @@ -382,8 +408,8 @@ serialiseSpec thisModule tcGblEnv liquidLib = do pure $ tcGblEnv { tcg_anns = serialisedSpec : tcg_anns tcGblEnv } -processInputSpec :: Config -> PipelineData -> ModSummary -> TcGblEnv -> BareSpec -> TcM (Either LiquidCheckException TcGblEnv) -processInputSpec cfg pipelineData modSummary tcGblEnv inputSpec = do +processInputSpec :: Config -> PipelineData -> ModSummary -> BareSpec -> TcM (Either LiquidCheckException LiquidLib) +processInputSpec cfg pipelineData modSummary inputSpec = do hscEnv <- env_top <$> getEnv debugLog $ " Input spec: \n" ++ show inputSpec debugLog $ "Relevant ===> \n" ++ unlines (renderModule <$> S.toList (relevantModules (hsc_mod_graph hscEnv) modGuts)) @@ -405,42 +431,34 @@ processInputSpec cfg pipelineData modSummary tcGblEnv inputSpec = do -- liftIO $ putStrLn ("liquidHaskellCheck 6: " ++ show isIg) if isIgnore inputSpec then pure $ Left (ErrorsOccurred []) - else do - liquidLib' <- checkLiquidHaskellContext lhContext - traverse (serialiseSpec thisModule tcGblEnv) liquidLib' + else checkLiquidHaskellContext lhContext where - thisModule :: Module - thisModule = tcg_mod tcGblEnv - modGuts :: ModGuts modGuts = pdUnoptimisedCore pipelineData liquidHaskellCheckWithConfig - :: Config -> PipelineData -> ModSummary -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv) -liquidHaskellCheckWithConfig cfg pipelineData modSummary tcGblEnv = do + :: Config -> PipelineData -> ModSummary -> TcM (Either LiquidCheckException LiquidLib) +liquidHaskellCheckWithConfig cfg pipelineData modSummary = do -- Parse the spec comments stored in the pipeline data. let inputSpec = toBareSpec . snd $ hsSpecificationP (moduleName thisModule) (pdSpecComments pipelineData) - processInputSpec cfg pipelineData modSummary tcGblEnv inputSpec + processInputSpec cfg pipelineData modSummary inputSpec `Ex.catch` (\(e :: UserError) -> reportErrs [e]) `Ex.catch` (\(e :: Error) -> reportErrs [e]) `Ex.catch` (\(es :: [Error]) -> reportErrs es) where - thisFile :: FilePath thisFile = LH.modSummaryHsFile modSummary + thisModule = ms_mod modSummary - continue :: TcM (Either LiquidCheckException TcGblEnv) + continue :: TcM (Either LiquidCheckException a) continue = pure $ Left (ErrorsOccurred []) - reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcM (Either LiquidCheckException TcGblEnv) + reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcM (Either LiquidCheckException a) reportErrs = LH.filterReportErrors thisFile GHC.failM continue (getFilters cfg) Full - thisModule :: Module - thisModule = tcg_mod tcGblEnv - checkLiquidHaskellContext :: LiquidHaskellContext -> TcM (Either LiquidCheckException LiquidLib) checkLiquidHaskellContext lhContext = do pmr <- processModule lhContext