Use LHName for type constructor in embed declarations

ucsd-progsys · Oct 24, 2024 · 178aee8 · 178aee8
1 parent 7679b1e
commit 178aee8
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 10 deletions.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -362,7 +362,7 @@ makeGhcSpec0 cfg session tcg 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 session tcg src lmap ((name, targetSpec) : dependencySpecs)
@@ -375,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

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
@@ -28,6 +28,7 @@ module Language.Haskell.Liquid.Bare.Resolve
   , lookupGhcTyCon
   , lookupGhcVar
   , lookupGhcNamedVar
+  , matchTyCon
 
   -- * Checking if names exist
   , knownGhcVar

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -851,7 +851,7 @@ data Pspec ty ctor
   | Using  (ty, ty)                                       -- ^ 'using' declaration (for local invariants on a type)
   | Alias   (Located (RTAlias Symbol BareType))           -- ^ 'type' alias declaration
   | EAlias  (Located (RTAlias Symbol Expr))               -- ^ 'predicate' alias declaration
-  | Embed   (LocSymbol, FTycon, TCArgs)                   -- ^ 'embed' declaration
+  | Embed   (Located LHName, FTycon, TCArgs)              -- ^ 'embed' declaration
   | Qualif  Qualifier                                     -- ^ 'qualif' definition
   | LVars   LocSymbol                                     -- ^ 'lazyvar' annotation, defer checks to *use* sites
   | Lazy    LocSymbol                                     -- ^ 'lazy' annotation, skip termination check on binder
@@ -1284,9 +1284,9 @@ invaliasP
 genBareTypeP :: Parser BareType
 genBareTypeP = bareTypeP
 
-embedP :: Parser (Located Symbol, FTycon, TCArgs)
+embedP :: Parser (Located LHName, FTycon, TCArgs)
 embedP = do
-  x <- locUpperIdP
+  x <- fmap (makeUnresolvedLHName LHTcName) <$> locUpperIdP
   a <- try (reserved "*" >> return WithArgs) <|> return NoArgs -- TODO: reserved "*" looks suspicious
   _ <- reserved "as"
   t <- fTyConP

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -79,6 +79,7 @@ import           Data.HashSet            (HashSet)
 import qualified Data.HashMap.Strict     as M
 import           Data.HashMap.Strict     (HashMap)
 import           Language.Haskell.Liquid.Types.DataDecl
+import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.RType
 import           Language.Haskell.Liquid.Types.Types
 import           Language.Haskell.Liquid.Types.Variance
@@ -410,7 +411,7 @@ data Spec ty bndr  = Spec
   , includes   :: ![FilePath]                                         -- ^ Included qualifier files
   , aliases    :: ![F.Located (RTAlias F.Symbol BareType)]            -- ^ RefType aliases
   , ealiases   :: ![F.Located (RTAlias F.Symbol F.Expr)]              -- ^ Expression aliases
-  , embeds     :: !(F.TCEmb F.LocSymbol)                              -- ^ GHC-Tycon-to-fixpoint Tycon map
+  , embeds     :: !(F.TCEmb (F.Located LHName))                       -- ^ GHC-Tycon-to-fixpoint Tycon map
   , qualifiers :: ![F.Qualifier]                                      -- ^ Qualifiers in source files
   , lvars      :: !(S.HashSet F.LocSymbol)                            -- ^ Variables that should be checked in the environment they are used
   , lazy       :: !(S.HashSet F.LocSymbol)                            -- ^ Ignore Termination Check in these Functions
@@ -607,7 +608,7 @@ data LiftedSpec = LiftedSpec
     -- ^ RefType aliases
   , liftedEaliases   :: HashSet (F.Located (RTAlias F.Symbol F.Expr))
     -- ^ Expression aliases
-  , liftedEmbeds     :: F.TCEmb F.LocSymbol
+  , liftedEmbeds     :: F.TCEmb (F.Located LHName)
     -- ^ GHC-Tycon-to-fixpoint Tycon map
   , liftedQualifiers :: HashSet F.Qualifier
     -- ^ Qualifiers in source/spec files