Use GHC Name to represent resolved type constructors

liquid-prelude/src/Language/Haskell/Liquid/Foreign.hs

@@ -35,7 +35,7 @@ cSizeInt :: CSize -> Int
 cSizeInt = fromIntegral
 
 
-{-@ assume mkPtr :: x:GHC.Prim.Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-}
+{-@ assume mkPtr :: x:Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-}
 mkPtr   :: Addr# -> Ptr b
 mkPtr = undefined -- Ptr x
 

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,7 +215,9 @@ import GHC.Builtin.Types              as Ghc
     , trueDataConId
     , tupleDataCon
     , tupleTyCon
+    , tupleTyConName
     , typeSymbolKind
+    , unrestrictedFunTyConName
     )
 import GHC.Builtin.Types.Prim         as Ghc
     ( isArrowTyCon
@@ -293,6 +296,7 @@ import GHC.Core.DataCon               as Ghc
     , dataConWrapId
     , dataConWrapId_maybe
     , isTupleDataCon
+    , promoteDataCon
     )
 import GHC.Core.FamInstEnv            as Ghc
     ( FamFlavor(DataFamilyInst)
@@ -403,6 +407,7 @@ import GHC.Data.FastString            as Ghc
     , bytesFS
     , concatFS
     , fsLit
+    , lexicalCompareFS
     , mkFastString
     , mkFastStringByteString
     , mkPtrString#
@@ -433,7 +438,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
@@ -450,7 +456,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
     )
@@ -467,6 +473,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
@@ -501,6 +509,8 @@ import GHC.Tc.Types.Origin            as Ghc (lexprCtOrigin)
 import GHC.Tc.Utils.Monad             as Ghc
     ( captureConstraints
     , discardConstraints
+    , getGblEnv
+    , setGblEnv
     , getEnv
     , getTopEnv
     , failIfErrsM
@@ -537,6 +547,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
@@ -597,26 +608,43 @@ import GHC.Types.Name                 as Ghc
     , getSrcSpan
     , isInternalName
     , isSystemName
+    , isTupleTyConName
     , mkInternalName
     , mkSystemName
     , mkTcOcc
     , mkTyVarOcc
     , mkVarOcc
     , mkVarOccFS
     , nameModule_maybe
+    , nameNameSpace
     , nameOccName
     , nameSrcLoc
     , nameStableString
+    , nameUnique
     , occNameFS
     , occNameString
     , stableNameCmp
     )
+import GHC.Types.Name.Cache           as Ghc (NameCache)
+import GHC.Types.Name.Occurrence      as Ghc
+    ( NameSpace
+    , isFieldNameSpace
+    , 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
@@ -692,6 +720,7 @@ import GHC.Unit.Module                as Ghc
     , IsBootInterface(NotBoot, IsBoot)
     , ModuleNameWithIsBoot
     , UnitId
+    , stableModuleCmp
     , fsToUnit
     , mkModuleNameFS
     , moduleNameFS
@@ -710,6 +739,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.hs

@@ -26,6 +26,7 @@ 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)
 import qualified Data.Maybe                                 as Mb
 import qualified Data.List                                  as L
 import qualified Data.HashMap.Strict                        as M
@@ -191,7 +192,10 @@ makeGhcSpec :: Config
             -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec))
 -------------------------------------------------------------------------------------
 makeGhcSpec cfg src lmap targetSpec dependencySpecs = do
-  (dg0, sp) <- makeGhcSpec0 cfg src lmap targetSpec dependencySpecs
+  hscEnv <- Ghc.getTopEnv
+  session <- Ghc.Session <$> Ghc.liftIO (newIORef hscEnv)
+  tcg <- Ghc.getGblEnv
+  (dg0, sp) <- makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs
   let diagnostics = Bare.checkTargetSpec (targetSpec : map snd dependencySpecs)
                                          (toTargetSrc src)
                                          (ghcSpecEnv sp)
@@ -231,12 +235,14 @@ ghcSpecEnv sp = F.notracepp "RENV" $ fromListSEnv binds
 -------------------------------------------------------------------------------------
 makeGhcSpec0
   :: Config
+  -> Ghc.Session
+  -> Ghc.TcGblEnv
   -> GhcSrc
   -> LogicMap
   -> Ms.BareSpec
   -> [(ModName, Ms.BareSpec)]
   -> Ghc.TcRn (Diagnostics, GhcSpec)
-makeGhcSpec0 cfg src lmap targetSpec dependencySpecs = do
+makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs = do
   -- build up environments
   tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier
   let tyi      = Bare.tcTyConMap   tycEnv
@@ -356,10 +362,10 @@ makeGhcSpec0 cfg src lmap targetSpec dependencySpecs = do
                               else (targetSpec, [])
     mySpec1  = mySpec0 <> lSpec0
     lSpec0   = makeLiftedSpec0 cfg src embs lmap mySpec0
-    embs     = makeEmbeds          src env ((name, mySpec0) : dependencySpecs)
+    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 src lmap ((name, targetSpec) : dependencySpecs)
+    env      = Bare.makeEnv cfg session tcg src lmap ((name, targetSpec) : dependencySpecs)
     -- check barespecs
     name     = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod  src
     zzz      = F.showpp (fst <$> mspecs)
@@ -369,17 +375,17 @@ makeImports specs = concatMap (expSigs . snd) specs'
   where specs' = filter (isSrcImport . fst) specs
 
 
-makeEmbeds :: GhcSrc -> Bare.Env -> [(ModName, Ms.BareSpec)] -> F.TCEmb Ghc.TyCon
+makeEmbeds :: GhcSrc -> Bare.Env -> [Ms.BareSpec] -> F.TCEmb Ghc.TyCon
 makeEmbeds src env
   = Bare.addClassEmbeds (_gsCls src) (_gsFiTcs src)
   . mconcat
   . map (makeTyConEmbeds env)
 
-makeTyConEmbeds :: Bare.Env -> (ModName, Ms.BareSpec) -> F.TCEmb Ghc.TyCon
-makeTyConEmbeds env (name, spec)
+makeTyConEmbeds :: Bare.Env -> Ms.BareSpec -> F.TCEmb Ghc.TyCon
+makeTyConEmbeds env spec
   = F.tceFromList [ (tc, t) | (c,t) <- F.tceToList (Ms.embeds spec), tc <- symTc c ]
     where
-      symTc = Mb.maybeToList . Bare.maybeResolveSym env name "embed-tycon"
+      symTc = Mb.maybeToList . either (const Nothing) Just . Bare.matchTyCon env
 
 --------------------------------------------------------------------------------
 -- | [NOTE]: REFLECT-IMPORTS

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

@@ -149,7 +149,7 @@ makeCLaws env sigEnv myName specs = do
   return (Mb.catMaybes zMbs)
   where
     err tc   = error ("Not a type class: " ++ F.showpp tc)
-    classTc  = Bare.maybeResolveSym env myName "makeClass" . btc_tc . rcName
+    classTc  = either (const Nothing) Just . Bare.matchTyCon env . btc_tc . rcName
     classTcs = [ (name, cls, tc) | (name, spec) <- M.toList specs
                                  , cls          <- Ms.claws spec
                                  , tc           <- Mb.maybeToList (classTc cls)
@@ -167,7 +167,7 @@ makeClasses env sigEnv myName specs = do
     classTcs = [ (name, cls, tc) | (name, spec) <- M.toList specs
                                  , cls          <- Ms.classes spec
                                  , tc           <- Mb.maybeToList (classTc cls) ]
-    classTc = Bare.maybeResolveSym env myName "makeClass" . btc_tc . rcName
+    classTc = either (const Nothing) Just . Bare.matchTyCon env . btc_tc . rcName
 
 mkClass :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> RClass LocBareType -> Ghc.TyCon
         -> Bare.Lookup (Maybe (DataConP, [(ModName, Ghc.Var, LocSpecType)]))

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

@@ -34,6 +34,7 @@ import qualified Language.Haskell.Liquid.GHC.Misc       as GM
 import qualified Liquid.GHC.API        as Ghc
 import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Errors
+import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.PredType (dataConPSpecType)
 import qualified Language.Haskell.Liquid.Types.RefType  as RT
 import           Language.Haskell.Liquid.Types.RType
@@ -44,7 +45,6 @@ import qualified Language.Fixpoint.Misc                 as Misc
 import qualified Language.Haskell.Liquid.Misc           as Misc
 import           Language.Haskell.Liquid.Types.Variance
 import           Language.Haskell.Liquid.WiredIn
-import           Language.Haskell.Liquid.Types.Names (selfSymbol)
 
 import qualified Language.Haskell.Liquid.Measure        as Ms
 
@@ -418,11 +418,11 @@ makeConTypes'' env name spec dcs vdcs = do
   return (unzip zong)
 
 
-type DSizeMap = M.HashMap F.Symbol (F.Symbol, [F.Symbol])
+type DSizeMap = M.HashMap F.Symbol (F.Symbol, [LHName])
 normalizeDSize :: [([LocBareType], F.LocSymbol)] -> DSizeMap
 normalizeDSize ds = M.fromList (concatMap go ds)
   where go (ts,x) = let xs = Mb.mapMaybe (getTc . val) ts
-                    in [(tc, (val x, xs)) | tc <- xs]
+                    in [(getLHNameSymbol tc, (val x, xs)) | tc <- xs]
         getTc (RAllT _ t _)  = getTc t
         getTc (RApp c _ _ _) = Just (val $ btc_tc c)
         getTc _ = Nothing
@@ -439,10 +439,10 @@ makeSize smap d
   | otherwise
    = d
 
-makeSizeCtor :: (F.Symbol, [F.Symbol]) -> DataCtor -> DataCtor
+makeSizeCtor :: (F.Symbol, [LHName]) -> DataCtor -> DataCtor
 makeSizeCtor (s,xs) d = d {dcFields = fmap (mapBot go) <$> dcFields d}
   where
-    go (RApp c ts rs r) | F.symbol c `elem` xs
+    go (RApp c ts rs r) | val (btc_tc c) `elem` xs
                         = RApp c ts rs (r `meet` rsz)
     go t                = t
     rsz  = MkUReft (F.Reft (F.vv_, F.PAtom F.Lt