Handle assume on local names when resolving to LHName

cabal.project

@@ -36,3 +36,7 @@ package liquidhaskell
 package liquidhaskell-boot
   ghc-options: -j
   flags: +devel
+
+constraints:
+  -- vector-0.13.2.0 breaks store-0.7.18
+  vector <= 0.13.1.0

liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs

@@ -635,7 +635,7 @@ import GHC.Types.Name                 as Ghc
     , stableNameCmp
     )
 import GHC.Types.Name.Env             as Ghc
-    ( lookupNameEnv )
+    ( NameEnv, lookupNameEnv, mkNameEnv )
 import GHC.Types.Name.Set             as Ghc
     ( NameSet
     , elemNameSet

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -123,12 +123,13 @@ to disk so that we can retrieve it later without having to re-check the relevant
 -- with a list of 'Warning's, which shouldn't abort the compilation (modulo explicit request from the user,
 -- to treat warnings and errors).
 makeTargetSpec :: Config
+               -> Bare.LocalVars
                -> LogicMap
                -> TargetSrc
                -> BareSpec
                -> TargetDependencies
                -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
-makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do
+makeTargetSpec cfg localVars lmap targetSrc bareSpec dependencies = do
   let targDiagnostics     = Bare.checkTargetSrc cfg targetSrc
   let depsDiagnostics     = mapM (Bare.checkBareSpec . snd) legacyDependencies
   let bareSpecDiagnostics = Bare.checkBareSpec legacyBareSpec
@@ -167,7 +168,7 @@ makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do
       --     "let {len :: [a] -> Int; len _ = undefined}"
       --     Ghc.execOptions
 
-      diagOrSpec <- makeGhcSpec cfg (fromTargetSrc targetSrc) lmap legacyBareSpec legacyDependencies
+      diagOrSpec <- makeGhcSpec cfg localVars (fromTargetSrc targetSrc) lmap legacyBareSpec legacyDependencies
       case diagOrSpec of
         Left d -> return $ Left d
         Right (warns, ghcSpec) -> do
@@ -191,7 +192,9 @@ makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do
       tcg <- Ghc.getGblEnv
       let exportedNames = Ghc.availsToNameSet (Ghc.tcg_exports tcg)
           exportedAssumption (LHNResolved (LHRGHC n) _) =
-            Ghc.nameModule_maybe n /= Just (Ghc.tcg_mod tcg) || Ghc.elemNameSet n exportedNames
+            case Ghc.nameModule_maybe n of
+              Nothing -> Ghc.elemNameSet n exportedNames
+              Just m -> m /= Ghc.tcg_mod tcg || Ghc.elemNameSet n exportedNames
           exportedAssumption _ = True
       return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) }
 
@@ -200,17 +203,18 @@ makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do
 --   validates it using @checkGhcSpec@.
 -------------------------------------------------------------------------------------
 makeGhcSpec :: Config
+            -> Bare.LocalVars
             -> GhcSrc
             -> LogicMap
             -> Ms.BareSpec
             -> [(ModName, Ms.BareSpec)]
             -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec))
 -------------------------------------------------------------------------------------
-makeGhcSpec cfg src lmap targetSpec dependencySpecs = do
+makeGhcSpec cfg localVars src lmap targetSpec dependencySpecs = do
   hscEnv <- Ghc.getTopEnv
   session <- Ghc.Session <$> Ghc.liftIO (newIORef hscEnv)
   tcg <- Ghc.getGblEnv
-  (dg0, sp) <- makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs
+  (dg0, sp) <- makeGhcSpec0 cfg session tcg localVars src lmap targetSpec dependencySpecs
   let diagnostics = Bare.checkTargetSpec (targetSpec : map snd dependencySpecs)
                                          (toTargetSrc src)
                                          (ghcSpecEnv sp)
@@ -252,12 +256,13 @@ makeGhcSpec0
   :: Config
   -> Ghc.Session
   -> Ghc.TcGblEnv
+  -> Bare.LocalVars
   -> GhcSrc
   -> LogicMap
   -> Ms.BareSpec
   -> [(ModName, Ms.BareSpec)]
   -> Ghc.TcRn (Diagnostics, GhcSpec)
-makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs = do
+makeGhcSpec0 cfg session tcg localVars src lmap targetSpec dependencySpecs = do
   -- build up environments
   tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier
   let tyi      = Bare.tcTyConMap   tycEnv
@@ -380,7 +385,7 @@ makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs = do
     embs     = makeEmbeds          src env (mySpec0 : map snd dependencySpecs)
     dm       = Bare.tcDataConMap tycEnv0
     (dg0, datacons, tycEnv0) = makeTycEnv0   cfg name env embs mySpec2 iSpecs2
-    env      = Bare.makeEnv cfg session tcg src lmap ((name, targetSpec) : dependencySpecs)
+    env      = Bare.makeEnv cfg session tcg localVars src lmap ((name, targetSpec) : dependencySpecs)
     -- check barespecs
     name     = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod  src
     zzz      = F.showpp (fst <$> mspecs)
@@ -891,7 +896,7 @@ makeTySigs env sigEnv name spec = do
 bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
 bareTySigs env name spec = checkDuplicateSigs <$> vts
   where
-    vts = forM ( Ms.sigs spec ++ Ms.localSigs spec ) $ \ (x, t) -> do
+    vts = forM ( Ms.sigs spec ) $ \ (x, t) -> do
             v <- F.notracepp "LOOKUP-GHC-VAR" $ Bare.lookupGhcVar env name "rawTySigs" x
             return (v, t)
 
@@ -998,7 +1003,7 @@ allAsmSigs env myName specs = do
       -- constraints should account instead for what logic functions are used in
       -- the constraints, which should be easier to do when precise renaming has
       -- been implemented for expressions and reflected functions.
-    , isUsedExternalVar v || isInScope v
+    , isUsedExternalVar v || isInScope v || isLocalVar v
     ]
   where
     lookupSymbolOrLHName :: ModName -> Bool -> SymbolOrLHName -> Bare.Lookup (Maybe Ghc.Var)
@@ -1056,6 +1061,8 @@ allAsmSigs env myName specs = do
             Ghc.DataConWorkId dc -> inScope dc
             _ -> inScope v0
 
+    isLocalVar = Mb.isNothing . Ghc.nameModule_maybe . Ghc.getName
+
 resolveAsmVar :: Bare.Env -> ModName -> Bool -> LocSymbol -> Bare.Lookup (Maybe Ghc.Var)
 resolveAsmVar env name True  lx = Just  <$> Bare.lookupGhcVar env name "resolveAsmVar-True"  lx
 resolveAsmVar env name False lx = return $  Bare.maybeResolveSym     env name "resolveAsmVar-False" lx  <|> GM.maybeAuxVar (F.val lx)

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs

@@ -388,7 +388,6 @@ expandBareSpec rtEnv l sp = sp
   { measures   = expand rtEnv l (measures   sp)
   , asmSigs    = map (second (expand rtEnv l)) (asmSigs sp)
   , sigs       = expand rtEnv l (sigs       sp)
-  , localSigs  = expand rtEnv l (localSigs  sp)
   , reflSigs   = expand rtEnv l (reflSigs   sp)
   , ialiases   = [ (f x, f y) | (x, y) <- ialiases sp ]
   , dataDecls  = expand rtEnv l (dataDecls  sp)

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs

@@ -14,6 +14,7 @@
 module Language.Haskell.Liquid.Bare.Resolve
   ( -- * Creating the Environment
     makeEnv
+  , makeLocalVars
 
     -- * Resolving symbols
   , ResolveSym (..)
@@ -30,6 +31,7 @@ module Language.Haskell.Liquid.Bare.Resolve
   , lookupGhcVar
   , lookupGhcIdLHName
   , lookupGhcNamedVar
+  , lookupLocalVar
   , matchTyCon
 
   -- * Checking if names exist
@@ -102,18 +104,19 @@ type Lookup a = Either [Error] a
 -------------------------------------------------------------------------------
 -- | Creating an environment
 -------------------------------------------------------------------------------
-makeEnv :: Config -> Ghc.Session -> Ghc.TcGblEnv -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
-makeEnv cfg session tcg src lmap specs = RE
+makeEnv :: Config -> Ghc.Session -> Ghc.TcGblEnv -> LocalVars -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
+makeEnv cfg session tcg localVars src lmap specs = RE
   { reSession   = session
   , reTcGblEnv  = tcg
+  , reLocalVarsEnv = makeLocalVarsEnv localVars
   , reUsedExternals = usedExternals
   , reLMap      = lmap
   , reSyms      = syms
   , _reSubst    = makeVarSubst   src
   , _reTyThings = makeTyThingMap src
   , reQualImps  = _gsQualImps     src
   , reAllImps   = _gsAllImps      src
-  , reLocalVars = makeLocalVars  src
+  , reLocalVars = localVars
   , reSrc       = src
   , reGlobSyms  = S.fromList     globalSyms
   , reCfg       = cfg
@@ -135,8 +138,12 @@ getGlobalSyms (_, spec)
   where
     mbName = F.val . msName
 
-makeLocalVars :: GhcSrc -> LocalVars
-makeLocalVars = localVarMap . localBinds . _giCbs
+makeLocalVars :: [Ghc.CoreBind] -> LocalVars
+makeLocalVars = localVarMap . localBinds
+
+makeLocalVarsEnv :: LocalVars -> Ghc.NameEnv Ghc.Var
+makeLocalVarsEnv m =
+    Ghc.mkNameEnv [ (Ghc.getName (lvdVar d), lvdVar d) | d <- concat (M.elems m) ]
 
 -- TODO: rewrite using CoreVisitor
 localBinds :: [Ghc.CoreBind] -> [LocalVarDetails]
@@ -447,7 +454,6 @@ qualifyBareSpec env name l bs sp = sp
   { measures   = qualify env name l bs (measures   sp)
   , asmSigs    = qualify env name l bs (asmSigs    sp)
   , sigs       = qualify env name l bs (sigs       sp)
-  , localSigs  = qualify env name l bs (localSigs  sp)
   , reflSigs   = qualify env name l bs (reflSigs   sp)
   , dataDecls  = qualify env name l bs (dataDecls  sp)
   , newtyDecls = qualify env name l bs (newtyDecls sp)
@@ -495,8 +501,8 @@ lookupGhcNamedVar env name z = maybeResolveSym  env name "Var" lx
 
 lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.Var
 lookupGhcVar env name kind lx = case resolveLocSym env name kind lx of
-    Right v -> Mb.maybe (Right v) Right (lookupLocalVar env lx [v])
-    Left  e -> Mb.maybe (Left  e) Right (lookupLocalVar env lx [])
+    Right v -> Mb.maybe (Right v) (either Right Right) (lookupLocalVar (reLocalVars env) lx [v])
+    Left  e -> Mb.maybe (Left  e) (either Right Right) (lookupLocalVar (reLocalVars env) lx [])
 
   -- where
     -- err e   = Misc.errorP "error-lookupGhcVar" (F.showpp (e, F.loc lx, lx))
@@ -506,12 +512,11 @@ lookupGhcVar env name kind lx = case resolveLocSym env name kind lx of
 --   that also match the name @lx@; we then pick the "closest" definition.
 --   See tests/names/LocalSpec.hs for a motivating example.
 
-lookupLocalVar :: Env -> LocSymbol -> [Ghc.Var] -> Maybe Ghc.Var
-lookupLocalVar env lx gvs = findNearest lxn kvs
+lookupLocalVar :: F.Loc a => LocalVars -> LocSymbol -> [a] -> Maybe (Either a Ghc.Var)
+lookupLocalVar localVars lx gvs = findNearest lxn kvs
   where
-    _msg                  = "LOOKUP-LOCAL: " ++ F.showpp (F.val lx, lxn, kvs)
-    kvs                   = prioritizeRecBinds (M.lookupDefault [] x $ reLocalVars env) ++ gs
-    gs                    = [(F.sp_start $ F.srcSpan v, v) | v <- gvs]
+    kvs                   = prioritizeRecBinds (M.lookupDefault [] x localVars) ++ gs
+    gs                    = [(F.sp_start $ F.srcSpan v, Left v) | v <- gvs]
     lxn                   = F.sp_start $ F.srcSpan lx
     (_, x)                = unQualifySymbol (F.val lx)
 
@@ -521,9 +526,9 @@ lookupLocalVar env lx gvs = findNearest lxn kvs
     prioritizeRecBinds lvds =
       let (recs, nrecs) = L.partition lvdIsRec lvds
        in map lvdToPair (recs ++ nrecs)
-    lvdToPair lvd = (lvdSourcePos lvd, lvdVar lvd)
+    lvdToPair lvd = (lvdSourcePos lvd, Right (lvdVar lvd))
 
-    findNearest :: F.SourcePos -> [(F.SourcePos, Ghc.Var)] -> Maybe Ghc.Var
+    findNearest :: F.SourcePos -> [(F.SourcePos, b)] -> Maybe b
     findNearest key kvs1 = argMin [ (posDistance key k, v) | (k, v) <- kvs1 ]
 
     -- We prefer the var with the smaller distance, or equal distance
@@ -568,9 +573,13 @@ lookupGhcDataConLHName env lname = do
 
 lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.Id
 lookupGhcIdLHName env lname = do
-   case lookupTyThing env lname of
-     Ghc.AConLike (Ghc.RealDataCon d) -> Right (Ghc.dataConWorkId d)
-     Ghc.AnId x -> Right x
+   case lookupTyThingMaybe env lname of
+     Nothing
+       | LHNResolved (LHRGHC n) _ <- val lname
+       , Just x <- Ghc.lookupNameEnv (reLocalVarsEnv env) n ->
+         Right x
+     Just (Ghc.AConLike (Ghc.RealDataCon d)) -> Right (Ghc.dataConWorkId d)
+     Just (Ghc.AnId x) -> Right x
      _ -> panic
            (Just $ GM.fSrcSpan lname) $ "not a variable of data constructor: " ++ show (val lname)
 
@@ -955,19 +964,21 @@ matchTyCon env lc = do
 -- This should be benign because the result doesn't depend of when exactly this is
 -- called. Since this code is intended to be used inside a GHC plugin, there is no
 -- danger that GHC is finalized before the result is evaluated.
-lookupTyThing :: Env -> Located LHName -> Ghc.TyThing
-lookupTyThing env lc@(Loc _ _ c0) = unsafePerformIO $ do
+lookupTyThingMaybe :: Env -> Located LHName -> Maybe Ghc.TyThing
+lookupTyThingMaybe env lc@(Loc _ _ c0) = unsafePerformIO $ do
     case c0 of
       LHNUnresolved _ _ -> panic (Just $ GM.fSrcSpan lc) $ "unresolved name: " ++ show c0
       LHNResolved rn _ -> case rn of
         LHRLocal _ -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a local name: " ++ show c0
         LHRIndex i -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a LHRIndex " ++ show i
         LHRLogic (LogicName s _) -> panic (Just $ GM.fSrcSpan lc) $ "lookupTyThing: cannot resolve a LHRLogic name " ++ show s
-        LHRGHC n -> do
-          m <- Ghc.reflectGhc (Interface.lookupTyThing (reTcGblEnv env) n) (reSession env)
-          case m of
-            Just tt -> return tt
-            Nothing -> panic (Just $ GM.fSrcSpan lc) $ "not found: " ++ show c0
+        LHRGHC n ->
+          Ghc.reflectGhc (Interface.lookupTyThing (reTcGblEnv env) n) (reSession env)
+
+lookupTyThing :: Env -> Located LHName -> Ghc.TyThing
+lookupTyThing env lc =
+    Mb.fromMaybe (panic (Just $ GM.fSrcSpan lc) $ "not found: " ++ show (val lc)) $
+      lookupTyThingMaybe env lc
 
 bareTCApp :: (Expandable r)
           => r

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs

@@ -72,6 +72,7 @@ plugSrc _        = Nothing
 data Env = RE 
   { reSession   :: Ghc.Session
   , reTcGblEnv  :: Ghc.TcGblEnv
+  , reLocalVarsEnv :: Ghc.NameEnv Ghc.Var   -- ^ an environment of local variables
   , reUsedExternals :: Ghc.NameSet
   , reLMap      :: LogicMap
   , reSyms      :: [(F.Symbol, Ghc.Var)]    -- ^ see "syms" in old makeGhcSpec'

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs

@@ -315,6 +315,9 @@ locNamedThing x = F.Loc l lE x
 instance F.Loc Var where
   srcSpan v = SS (getSourcePos v) (getSourcePosE v)
 
+instance F.Loc Name where
+  srcSpan v = SS (getSourcePos v) (getSourcePosE v)
+
 namedLocSymbol :: (F.Symbolic a, NamedThing a) => a -> F.Located F.Symbol
 namedLocSymbol d = F.symbol <$> locNamedThing d
 

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs

@@ -73,6 +73,7 @@ import           Language.Haskell.Liquid.Types.Specs
 import           Language.Haskell.Liquid.Types.Types
 import           Language.Haskell.Liquid.Types.Visitors
 import           Language.Haskell.Liquid.Bare
+import           Language.Haskell.Liquid.Bare.Resolve (makeLocalVars)
 import           Language.Haskell.Liquid.UX.CmdLine
 import           Language.Haskell.Liquid.UX.Config
 
@@ -509,8 +510,10 @@ data ProcessModuleResult = ProcessModuleResult {
 
 processModule :: LiquidHaskellContext -> TcM (Either LiquidCheckException ProcessModuleResult)
 processModule LiquidHaskellContext{..} = do
+  let modGuts0   = lhModuleGuts
+      thisModule = mg_module modGuts0
+
   debugLog ("Module ==> " ++ renderModule thisModule)
-  hscEnv              <- env_top <$> getEnv
 
   let bareSpec0       = lhInputSpec
   -- /NOTE/: For the Plugin to work correctly, we shouldn't call 'canonicalizePath', because otherwise
@@ -527,11 +530,13 @@ processModule LiquidHaskellContext{..} = do
     when debugLogs $
       forM_ (HM.keys . getDependencies $ dependencies) $ debugLog . moduleStableString . unStableModule
 
-    debugLog $ "mg_exports => " ++ O.showSDocUnsafe (O.ppr $ mg_exports modGuts)
-    debugLog $ "mg_tcs => " ++ O.showSDocUnsafe (O.ppr $ mg_tcs modGuts)
+    debugLog $ "mg_exports => " ++ O.showSDocUnsafe (O.ppr $ mg_exports modGuts0)
+    debugLog $ "mg_tcs => " ++ O.showSDocUnsafe (O.ppr $ mg_tcs modGuts0)
 
-    dynFlags <- getDynFlags
-    targetSrc  <- liftIO $ makeTargetSrc moduleCfg dynFlags file lhModuleTcData modGuts hscEnv
+    hscEnv <- getTopEnv
+    let preNormalizedCore = preNormalizeCore moduleCfg modGuts0
+        modGuts = modGuts0 { mg_binds = preNormalizedCore }
+    targetSrc  <- liftIO $ makeTargetSrc moduleCfg file lhModuleTcData modGuts hscEnv
     logger <- getLogger
 
     -- See https://github.com/ucsd-progsys/liquidhaskell/issues/1711
@@ -540,13 +545,18 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let rtAliases = collectTypeAliases thisModule bareSpec0 (HM.toList $ getDependencies dependencies)
-        eBareSpec = resolveLHNames rtAliases (tcg_rdr_env tcg) bareSpec0
+        localVars = makeLocalVars preNormalizedCore
+        eBareSpec = resolveLHNames
+          localVars
+          rtAliases
+          (tcg_rdr_env tcg)
+          bareSpec0
     result <-
       case eBareSpec of
         Left errors -> pure $ Left $ mkDiagnostics [] errors
         Right bareSpec ->
           fmap (,bareSpec) <$>
-            makeTargetSpec moduleCfg lhModuleLogicMap targetSrc bareSpec dependencies
+            makeTargetSpec moduleCfg localVars lhModuleLogicMap targetSrc bareSpec dependencies
 
     let continue = pure $ Left (ErrorsOccurred [])
         reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcRn (Either LiquidCheckException ProcessModuleResult)
@@ -576,23 +586,17 @@ processModule LiquidHaskellContext{..} = do
       `Ex.catch` (\(e :: Error) -> reportErrs [e])
       `Ex.catch` (\(es :: [Error]) -> reportErrs es)
 
-  where
-    modGuts    = lhModuleGuts
-    thisModule = mg_module modGuts
-
 makeTargetSrc :: Config
-              -> DynFlags
               -> FilePath
               -> TcData
               -> ModGuts
               -> HscEnv
               -> IO TargetSrc
-makeTargetSrc cfg dynFlags file tcData modGuts hscEnv = do
-  let preNormCoreBinds = preNormalizeCore cfg modGuts
+makeTargetSrc cfg file tcData modGuts hscEnv = do
   when (dumpPreNormalizedCore cfg) $ do
     putStrLn "\n*************** Pre-normalized CoreBinds *****************\n"
-    putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr dynFlags) preNormCoreBinds
-  coreBinds <- anormalize cfg hscEnv modGuts { mg_binds = preNormCoreBinds }
+    putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr (GHC.hsc_dflags hscEnv)) (mg_binds modGuts)
+  coreBinds <- anormalize cfg hscEnv modGuts
 
   -- The type constructors for a module are the (nubbed) union of the ones defined and
   -- the ones exported. This covers the case of \"wrapper modules\" that simply re-exports