Merge pull request #2421 from ucsd-progsys/fd/sigs-names

Use GHC Name after resolving asserted specs

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

@@ -634,8 +634,6 @@ import GHC.Types.Name                 as Ghc
     , occNameString
     , stableNameCmp
     )
-import GHC.Types.Name.Env             as Ghc
-    ( NameEnv, lookupNameEnv, mkNameEnv )
 import GHC.Types.Name.Set             as Ghc
     ( NameSet
     , elemNameSet
@@ -701,6 +699,12 @@ import GHC.Types.SrcLoc               as Ghc
     , srcSpanToRealSrcSpan
     )
 import GHC.Types.Tickish              as Ghc (CoreTickish, GenTickish(..))
+import GHC.Types.TypeEnv              as Ghc
+    ( TypeEnv
+    , lookupTypeEnv
+    , mkTypeEnv
+    , plusTypeEnv
+    )
 import GHC.Types.Unique               as Ghc
     ( getKey, mkUnique )
 import GHC.Types.Unique.Set           as Ghc (mkUniqSet)

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

@@ -24,7 +24,6 @@ module Language.Haskell.Liquid.Bare (
 
 import           Prelude                                    hiding (error)
 import           Control.Monad                              (forM, mplus, when)
-import           Control.Applicative                        ((<|>))
 import qualified Control.Exception                          as Ex
 import qualified Data.Binary                                as B
 import           Data.IORef (newIORef)
@@ -885,19 +884,19 @@ makeFromSet msg f env specs = concat [ mk n xs | (n, s) <- specs, let xs = S.toL
 makeTySigs :: Bare.Env -> Bare.SigEnv -> ModName -> Ms.BareSpec
            -> Bare.Lookup [(Ghc.Var, LocSpecType, Maybe [Located F.Expr])]
 makeTySigs env sigEnv name spec = do
-  bareSigs   <- bareTySigs env name                spec
+  bareSigs   <- bareTySigs env                     spec
   expSigs    <- makeTExpr  env name bareSigs rtEnv spec
   let rawSigs = Bare.resolveLocalBinds env expSigs
   return [ (x, cook x bt, z) | (x, bt, z) <- rawSigs ]
   where
     rtEnv     = Bare.sigRTEnv sigEnv
     cook x bt = Bare.cookSpecType env sigEnv name (Bare.HsTV x) bt
 
-bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
-bareTySigs env name spec = checkDuplicateSigs <$> vts
+bareTySigs :: Bare.Env -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
+bareTySigs env spec = checkDuplicateSigs <$> vts
   where
     vts = forM ( Ms.sigs spec ) $ \ (x, t) -> do
-            v <- F.notracepp "LOOKUP-GHC-VAR" $ Bare.lookupGhcVar env name "rawTySigs" x
+            v <- F.notracepp "LOOKUP-GHC-VAR" $ Bare.lookupGhcIdLHName env x
             return (v, t)
 
 -- checkDuplicateSigs :: [(Ghc.Var, LocSpecType)] -> [(Ghc.Var, LocSpecType)]
@@ -936,7 +935,7 @@ myAsmSig v sigs = Mb.fromMaybe errImp (mbHome `mplus` mbImp)
 makeTExpr :: Bare.Env -> ModName -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec
           -> Bare.Lookup [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
 makeTExpr env name tySigs rtEnv spec = do
-  vExprs       <- M.fromList <$> makeVarTExprs env name spec
+  vExprs       <- M.fromList <$> makeVarTExprs env spec
   let vSigExprs = Misc.hashMapMapWithKey (\v t -> (t, M.lookup v vExprs)) vSigs
   return [ (v, t, qual t <$> es) | (v, (t, es)) <- M.toList vSigExprs ]
   where
@@ -952,10 +951,10 @@ qualifyTermExpr env name rtEnv t le
     e   = F.val le
     bs  = ty_binds . toRTypeRep . val $ t
 
-makeVarTExprs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
-makeVarTExprs env name spec =
+makeVarTExprs :: Bare.Env -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
+makeVarTExprs env spec =
   forM (Ms.termexprs spec) $ \(x, es) -> do
-    vx <- Bare.lookupGhcVar env name "Var" x
+    vx <- Bare.lookupGhcIdLHName env x
     return (vx, es)
 
 ----------------------------------------------------------------------------------------
@@ -994,10 +993,10 @@ allAsmSigs env myName specs = do
   let aSigs = [ (name, locallyDefined, x, t) | (name, spec) <- M.toList specs
                                    , (locallyDefined, x, t) <- getAsmSigs myName name spec ]
   vSigs    <- forM aSigs $ \(name, locallyDefined, x, t) -> do
-                vMb <- lookupSymbolOrLHName name locallyDefined x
-                return (vMb, (locallyDefined, name, t))
+                v <- Bare.lookupGhcIdLHName env x
+                return (v, (locallyDefined, name, t))
   return $ Misc.groupList
-    [ (v, z) | (Just v, z) <- vSigs
+    [ (v, z) | (v, z) <- vSigs
       -- TODO: we require signatures to be in scope because LH includes them in
       -- the environment of contraints sometimes. The criteria to add bindings to
       -- constraints should account instead for what logic functions are used in
@@ -1006,39 +1005,6 @@ allAsmSigs env myName specs = do
     , isUsedExternalVar v || isInScope v || isLocalVar v
     ]
   where
-    lookupSymbolOrLHName :: ModName -> Bool -> SymbolOrLHName -> Bare.Lookup (Maybe Ghc.Var)
-    lookupSymbolOrLHName _name _locallyDefined (SOLLHName x) =
-      Just <$> Bare.lookupGhcIdLHName env x
-    lookupSymbolOrLHName name locallyDefined (SOLSymbol x) = do
-                -- Qualified assumes that refer to module aliases import declarations
-                -- are resolved looking at import declarations
-                let (mm, s) = Bare.unQualifySymbol (val x)
-                if not (isAbsoluteQualifiedSym mm) then resolveAsmVar env name locallyDefined x
-                       else if locallyDefined then
-                         -- Fully qualified assumes that are locally defined produce an error if they aren't found
-                         lookupImportedSym x (mm, s)
-                       else
-                         -- Imported fully qualified assumes do not produce an error if they
-                         -- aren't found, and we looked them anyway without considering
-                         -- import declarations.
-                         -- LH seems to send here assumes for data constructors that
-                         -- yield Nothing, like for GHC.Types.W#
-                         return $ lookupImportedSymMaybe (mm, s)
-
-    lookupImportedSym x qp =
-      let errRes = Left [Bare.errResolve "variable" "Var" x]
-       in maybe errRes (Right . Just) $
-            lookupImportedSymMaybe qp
-    lookupImportedSymMaybe (mm, s) = do
-      mts <- M.lookup s (Bare._reTyThings env)
-      m <- mm
-      Mb.listToMaybe [ v | (k, Ghc.AnId v) <- mts, k == m ]
-
-    isAbsoluteQualifiedSym (Just m) =
-       not $ M.member m $ qiNames (Bare.reQualImps env)
-    isAbsoluteQualifiedSym Nothing =
-       False
-
     isUsedExternalVar :: Ghc.Var -> Bool
     isUsedExternalVar v = case Ghc.idDetails v of
       Ghc.DataConWrapId dc ->
@@ -1063,24 +1029,16 @@ allAsmSigs env myName specs = do
 
     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)
-
--- | Temporary data type to represent a symbol or an LHName while not all of the
--- code has been migrated to use LHName.
-data SymbolOrLHName = SOLSymbol LocSymbol | SOLLHName (Located LHName)
-
-getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, SymbolOrLHName, LocBareType)]
+getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, Located LHName, LocBareType)]
 getAsmSigs myName name spec
-  | myName == name = [ (True, SOLLHName x,  t) | (x, t) <- Ms.asmSigs spec ] -- MUST    resolve, or error
+  | myName == name = [ (True, x,  t) | (x, t) <- Ms.asmSigs spec ] -- MUST    resolve, or error
   | otherwise      =
       [ (False, x, t)
-      | (x, t) <- map (first SOLLHName) (Ms.asmSigs spec)
-                  ++ map (first (SOLSymbol . qSym)) (Ms.sigs spec)
+      | (x, t) <- Ms.asmSigs spec
+                  ++ map (first (fmap (updateLHNameSymbol qSym))) (Ms.sigs spec)
       ]
   where
-    qSym           = fmap (GM.qualifySymbol ns)
+    qSym           = GM.qualifySymbol ns
     ns             = F.symbol name
 
 -- TODO-REBARE: grepClassAssumes
@@ -1410,7 +1368,7 @@ makeLiftedSpec name src env refl sData sig qual myRTE lSpec0 = lSpec0
   { Ms.asmSigs    = F.notracepp   ("makeLiftedSpec : ASSUMED-SIGS " ++ F.showpp name ) (xbs ++ myDCs)
   , Ms.reflSigs   = F.notracepp "REFL-SIGS" $ map (first (fmap getLHNameSymbol)) xbs
   , Ms.sigs       = F.notracepp   ("makeLiftedSpec : LIFTED-SIGS " ++ F.showpp name ) $
-                      map (first (fmap getLHNameSymbol)) $ mkSigs (gsTySigs sig)
+                      mkSigs (gsTySigs sig)
   , Ms.invariants = [ (Bare.varLocSym <$> x, Bare.specToBare <$> t)
                        | (x, t) <- gsInvariants sData
                        , isLocInFile srcF t

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

@@ -387,7 +387,7 @@ expandBareSpec :: BareRTEnv -> F.SourcePos -> Ms.BareSpec -> Ms.BareSpec
 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)
+  , sigs       = map (second (expand rtEnv l)) (sigs 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

@@ -108,7 +108,12 @@ makeEnv :: Config -> Ghc.Session -> Ghc.TcGblEnv -> LocalVars -> GhcSrc -> Logic
 makeEnv cfg session tcg localVars src lmap specs = RE
   { reSession   = session
   , reTcGblEnv  = tcg
-  , reLocalVarsEnv = makeLocalVarsEnv localVars
+  , reTypeEnv   =
+      -- Types differ in tcg_type_env vs the core bindings though they seem to
+      -- be alpha-equivalent. We prefer the type in the core bindings and we
+      -- also include the types of local variables.
+      let varsEnv = Ghc.mkTypeEnv $ map Ghc.AnId $ letVars $ _giCbs src
+       in Ghc.tcg_type_env tcg `Ghc.plusTypeEnv` varsEnv
   , reUsedExternals = usedExternals
   , reLMap      = lmap
   , reSyms      = syms
@@ -141,10 +146,6 @@ getGlobalSyms (_, spec)
 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]
 localBinds                    = concatMap bgoT
@@ -572,16 +573,12 @@ lookupGhcDataConLHName env lname = do
            (Just $ GM.fSrcSpan lname) $ "not a data constructor: " ++ show (val lname)
 
 lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.Id
-lookupGhcIdLHName env lname = do
-   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
+lookupGhcIdLHName env lname =
+   case lookupTyThing env lname of
+     Ghc.AConLike (Ghc.RealDataCon d) -> Right (Ghc.dataConWorkId d)
+     Ghc.AnId x -> Right x
      _ -> panic
-           (Just $ GM.fSrcSpan lname) $ "not a variable of data constructor: " ++ show (val lname)
+           (Just $ GM.fSrcSpan lname) $ "not a variable or data constructor: " ++ show (val lname)
 
 -------------------------------------------------------------------------------
 -- | Checking existence of names
@@ -973,7 +970,7 @@ lookupTyThingMaybe env lc@(Loc _ _ c0) = unsafePerformIO $ do
         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 ->
-          Ghc.reflectGhc (Interface.lookupTyThing (reTcGblEnv env) n) (reSession env)
+          Ghc.reflectGhc (Interface.lookupTyThing (reTypeEnv env) n) (reSession env)
 
 lookupTyThing :: Env -> Located LHName -> Ghc.TyThing
 lookupTyThing env lc =

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

@@ -73,15 +73,15 @@ compileClasses src env (name, spec) rest =
       -- class methods
   (refinedMethods, sigsNew) = foldr grabClassSig (mempty, mempty) (sigs spec)
   grabClassSig
-    :: (F.LocSymbol, ty)
-    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.LocSymbol, ty)])
-    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.LocSymbol, ty)])
+    :: (F.Located LHName, ty)
+    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.Located LHName, ty)])
+    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.Located LHName, ty)])
   grabClassSig sigPair@(lsym, ref) (refs, sigs') = case clsOp of
     Nothing         -> (refs, sigPair : sigs')
     Just (cls, sig) -> (M.alter (merge sig) cls refs, sigs')
    where
     clsOp = do
-      var <- Bare.maybeResolveSym env name "grabClassSig" lsym
+      var <- either (const Nothing) Just $ Bare.lookupGhcIdLHName env lsym
       cls <- Ghc.isClassOpId_maybe var
       pure (cls, (var, ref))
     merge sig v = case v of

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

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

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

@@ -170,24 +170,24 @@ qImports qns  = QImports
 --   (see `Bare.Resolve`)
 ---------------------------------------------------------------------------------------
 lookupTyThings :: (GhcMonad m) => TcGblEnv -> m [(Name, Maybe TyThing)]
-lookupTyThings tcGblEnv = zip names <$> mapM (lookupTyThing tcGblEnv) names
+lookupTyThings tcGblEnv = zip names <$> mapM (lookupTyThing (Ghc.tcg_type_env tcGblEnv)) names
   where
     names = liftA2 (++)
         (fmap Ghc.greName . Ghc.globalRdrEnvElts . tcg_rdr_env)
         (fmap is_dfun_name . tcg_insts)
         tcGblEnv
 
-lookupTyThing :: (GhcMonad m) => TcGblEnv -> Name -> m (Maybe TyThing)
-lookupTyThing tcGblEnv name = do
+lookupTyThing :: (GhcMonad m) => Ghc.TypeEnv -> Name -> m (Maybe TyThing)
+lookupTyThing tyEnv name = do
     runMaybeT . msum . map MaybeT $
-        [ pure (lookupNameEnv (tcg_type_env tcGblEnv) name)
+        [ pure (lookupTypeEnv tyEnv name)
         , lookupName name
         ]
 
 availableTyThings :: (GhcMonad m) => TcGblEnv -> [AvailInfo] -> m [TyThing]
 availableTyThings tcGblEnv avails =
     fmap catMaybes $
-      mapM (lookupTyThing tcGblEnv) $
+      mapM (lookupTyThing (Ghc.tcg_type_env tcGblEnv)) $
       concatMap availNames avails
 
 _dumpTypeEnv :: TypecheckedModule -> IO ()

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

@@ -838,9 +838,9 @@ data Pspec ty ctor
   = Meas    (Measure ty ctor)                             -- ^ 'measure' definition
   | Assm    (Located LHName, ty)                          -- ^ 'assume' signature (unchecked)
   | AssmReflect (LocSymbol, LocSymbol)                    -- ^ 'assume reflects' signature (unchecked)
-  | Asrt    (LocSymbol, ty)                               -- ^ 'assert' signature (checked)
+  | Asrt    (Located LHName, ty)                          -- ^ 'assert' signature (checked)
   | LAsrt   (LocSymbol, ty)                               -- ^ 'local' assertion -- TODO RJ: what is this
-  | Asrts   ([LocSymbol], (ty, Maybe [Located Expr]))     -- ^ sym0, ..., symn :: ty / [m0,..., mn]
+  | Asrts   ([Located LHName], (ty, Maybe [Located Expr]))     -- ^ sym0, ..., symn :: ty / [m0,..., mn]
   | Impt    Symbol                                        -- ^ 'import' a specification module
   | DDecl   DataDecl                                      -- ^ refined 'data'    declaration
   | NTDecl  DataDecl                                      -- ^ refined 'newtype' declaration
@@ -886,9 +886,9 @@ instance (PPrint ty, PPrint ctor) => PPrint (Pspec ty ctor) where
 splice :: PJ.Doc -> [PJ.Doc] -> PJ.Doc
 splice sep = PJ.hcat . PJ.punctuate sep
 
-ppAsserts :: (PPrint t) => Tidy -> [LocSymbol] -> t -> Maybe [Located Expr] -> PJ.Doc
+ppAsserts :: (PPrint t) => Tidy -> [Located LHName] -> t -> Maybe [Located Expr] -> PJ.Doc
 ppAsserts k lxs t mles
-  = PJ.hcat [ splice ", " (pprintTidy k <$> (val <$> lxs))
+  = PJ.hcat [ splice ", " (map (pprintTidy k . val) lxs)
             , " :: "
             , pprintTidy k t
             , ppLes mles
@@ -1044,8 +1044,8 @@ qualifySpec name sp = sp { sigs      = [ (tx x, t)  | (x, t)  <- sigs sp]
                          -- , asmSigs   = [ (tx x, t)  | (x, t)  <- asmSigs sp]
                          }
   where
-    tx :: Located Symbol -> Located Symbol
-    tx = fmap (qualifySymbol name)
+    tx :: Located LHName -> Located LHName
+    tx = fmap (updateLHNameSymbol (qualifySymbol name))
 
 -- | Turns a list of parsed specifications into a "bare spec".
 --
@@ -1118,7 +1118,7 @@ specP
   = fallbackSpecP "assume" ((reserved "reflect" >> fmap AssmReflect assmReflectBindP)
         <|> (reserved "relational" >>  fmap AssmRel relationalP)
         <|>                            fmap Assm   tyBindLHNameP  )
-    <|> fallbackSpecP "assert"      (fmap Asrt    tyBindP  )
+    <|> fallbackSpecP "assert"      (fmap Asrt    tyBindLHNameP)
     <|> fallbackSpecP "autosize"    (fmap ASize   asizeP   )
     <|> (reserved "local"         >> fmap LAsrt   tyBindP  )
 
@@ -1184,10 +1184,10 @@ specP
 fallbackSpecP :: String -> Parser BPspec -> Parser BPspec
 fallbackSpecP kw p = do
   (Loc l1 l2 _) <- locReserved kw
-  p <|> fmap Asrts (tyBindsRemP (Loc l1 l2 (symbol kw)) )
+  p <|> fmap Asrts (tyBindsRemP (Loc l1 l2 (makeUnresolvedLHName LHVarName (symbol kw))) )
 
 -- | Same as tyBindsP, except the single initial symbol has already been matched
-tyBindsRemP :: LocSymbol -> Parser ([LocSymbol], (Located BareType, Maybe [Located Expr]))
+tyBindsRemP :: Located LHName -> Parser ([Located LHName], (Located BareType, Maybe [Located Expr]))
 tyBindsRemP sy = do
   reservedOp "::"
   tb <- termBareTypeP
@@ -1249,9 +1249,9 @@ varianceP = (reserved "bivariant"     >> return Bivariant)
         <|> (reserved "contravariant" >> return Contravariant)
         <?> "Invalid variance annotation\t Use one of bivariant, invariant, covariant, contravariant"
 
-tyBindsP :: Parser ([LocSymbol], (Located BareType, Maybe [Located Expr]))
+tyBindsP :: Parser ([Located LHName], (Located BareType, Maybe [Located Expr]))
 tyBindsP =
-  xyP (sepBy1 locBinderP comma) (reservedOp "::") termBareTypeP
+  xyP (sepBy1 locBinderLHNameP comma) (reservedOp "::") termBareTypeP
 
 tyBindNoLocP :: Parser (LocSymbol, BareType)
 tyBindNoLocP = second val <$> tyBindP
@@ -1459,6 +1459,10 @@ locBinderP :: Parser (Located Symbol)
 locBinderP =
   located binderP -- TODO
 
+locBinderLHNameP :: Parser (Located LHName)
+locBinderLHNameP =
+  located $ makeUnresolvedLHName LHVarName <$> binderP
+
 -- | LHS of the thing being defined
 --
 -- TODO, Andres: this is still very broken