From 43e83adefec8ac0b4274a9cfeb9d60fb75b20bf9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Tue, 10 Dec 2024 19:44:33 +0000
Subject: [PATCH 01/16] Persist name resolution of field names

---
 .../src/Language/Haskell/Liquid/Bare/Check.hs |  8 +--
 .../src/Language/Haskell/Liquid/Bare/Class.hs |  6 +-
 .../Language/Haskell/Liquid/Bare/DataType.hs  | 38 +++---------
 .../Language/Haskell/Liquid/Bare/Measure.hs   | 15 +++--
 .../Language/Haskell/Liquid/Bare/Plugged.hs   | 12 ++--
 .../Language/Haskell/Liquid/Bare/Typeclass.hs | 10 ++--
 .../Haskell/Liquid/LHNameResolution.hs        | 58 ++++++++++++-------
 .../src/Language/Haskell/Liquid/Parse.hs      | 15 +++--
 .../Language/Haskell/Liquid/Types/DataDecl.hs |  4 +-
 .../Language/Haskell/Liquid/Types/Names.hs    | 11 +++-
 .../Language/Haskell/Liquid/Types/PredType.hs |  9 ++-
 .../Language/Haskell/Liquid/Types/RTypeOp.hs  |  5 +-
 .../src/Language/Haskell/Liquid/WiredIn.hs    |  9 +--
 13 files changed, 108 insertions(+), 92 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
index 6dcd44b8dd..93e80a3a0d 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
@@ -95,16 +95,16 @@ checkBareSpec sp
     hmeasures = S.map (fmap getLHNameSymbol) (Ms.hmeas sp)
     reflects  = S.map (fmap getLHNameSymbol) (Ms.reflects sp)
     measures  = fmap getLHNameSymbol . msName <$> Ms.measures sp
-    fields    = concatMap dataDeclFields (Ms.dataDecls sp)
+    fields    = map (fmap getLHNameSymbol) $ concatMap dataDeclFields (Ms.dataDecls sp)
 
-dataDeclFields :: DataDecl -> [F.LocSymbol]
-dataDeclFields = filter (not . GM.isTmpSymbol . F.val)
+dataDeclFields :: DataDecl -> [F.Located LHName]
+dataDeclFields = filter (not . GM.isTmpSymbol . getLHNameSymbol . F.val)
                . Misc.hashNubWith val
                . concatMap dataCtorFields
                . fromMaybe []
                . tycDCons
 
-dataCtorFields :: DataCtor -> [F.LocSymbol]
+dataCtorFields :: DataCtor -> [F.Located LHName]
 dataCtorFields c
   | isGadt c  = []
   | otherwise = F.atLoc c <$> [ f | (f,_) <- dcFields c ]
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs
index 6e367abce6..ec3f2598d9 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs
@@ -61,7 +61,9 @@ makeMethodTypes allowTC (DEnv hm) cls cbs
       classType Nothing _ = Nothing
       classType (Just (d, ts, _)) x =
         case filter ((==d) . Ghc.dataConWorkId . dcpCon) cls of
-          (di:_) -> (dcpLoc di `F.atLoc`) . subst (zip (dcpFreeTyVars di) ts) <$> L.lookup (mkSymbol x) (dcpTyArgs di)
+          (di:_) ->
+            (dcpLoc di `F.atLoc`) . subst (zip (dcpFreeTyVars di) ts) <$>
+            L.lookup (mkSymbol x) (map (first logicNameToSymbol) $ dcpTyArgs di)
           _      -> Nothing
 
       methodType d x m = ihastype (M.lookup d m) x
@@ -160,7 +162,7 @@ mkClassE env sigEnv _myName name (RClass cc ss as ms) tc = do
     meths  <- mapM (makeMethod env sigEnv name) ms'
     let vts = [ (m, v, t) | (m, kv, t) <- meths, v <- Mb.maybeToList (plugSrc kv) ]
     let sts = [(val s, unClass $ val t) | (s, _) <- ms | (_, _, t) <- meths]
-    let dcp = DataConP l dc αs [] (val <$> ss') (map (first getLHNameSymbol) (reverse sts)) rt False (F.symbol name) l'
+    let dcp = DataConP l dc αs [] (val <$> ss') (reverse sts) rt False (F.symbol name) l'
     return  $ F.notracepp msg (dcp, vts)
   where
     c      = btc_tc cc
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
index 3aed2052d6..16d23c8362 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
@@ -346,7 +346,7 @@ makeDataCtor tce c (d, dp) = F.DCtor
   }
   where
     as          = dcpFreeTyVars dp
-    xts         = [ (fld x, t) | (x, t) <- reverse (dcpTyArgs dp) ]
+    xts         = [ (fld $ logicNameToSymbol x, t) | (x, t) <- reverse (dcpTyArgs dp) ]
     fld         = F.atLoc dp . fieldName d dp
 
 fieldName :: Ghc.DataCon -> DataConP -> F.Symbol -> F.Symbol
@@ -656,7 +656,7 @@ ofBDataCtorTc env name l l' tc αs ps πs _ctor@(DataCtor _c as _ xts res) c' =
     res'          = Bare.ofBareType env name l (Just ps) <$> res
     t0'           = dataConResultTy c' αs t0 res'
     _cfg          = getConfig env
-    (yts, ot)     = qualifyDataCtor (not isGadt) name dLoc (zip xs ts', t0')
+    (yts, ot)     = (zip xs ts', t0')
     zts           = zipWith (normalizeField c') [1..] (reverse yts)
     usedTvs       = S.fromList (ty_var_value <$> concatMap RT.freeTyVars (t0':ts'))
     cs            = [ p | p <- RT.ofType <$> Ghc.dataConTheta c', keepPredType usedTvs p ]
@@ -665,7 +665,6 @@ ofBDataCtorTc env name l l' tc αs ps πs _ctor@(DataCtor _c as _ xts res) c' =
                       Nothing -> RT.gApp tc αs πs
                       Just ty -> RT.ofType ty
     isGadt        = Mb.isJust res
-    dLoc          = F.Loc l l' ()
 
 errDataConMismatch :: LocSymbol -> S.HashSet F.Symbol -> S.HashSet F.Symbol -> Error
 errDataConMismatch d dcs rdcs = ErrDataConMismatch sp v (ppTicks <$> S.toList dcs) (ppTicks <$> S.toList rdcs)
@@ -731,36 +730,13 @@ eqSubst (RApp c [_, _, RVar a _, t] _ _)
   | rtc_tc c == Ghc.eqPrimTyCon = Just (a, t)
 eqSubst _                       = Nothing
 
-normalizeField :: Ghc.DataCon -> Int -> (F.Symbol, a) -> (F.Symbol, a)
+normalizeField :: Ghc.DataCon -> Int -> (LHName, a) -> (LHName, a)
 normalizeField c i (x, t)
   | isTmp x   = (xi, t)
   | otherwise = (x , t)
   where
-    isTmp     = F.isPrefixOfSym F.tempPrefix
-    xi        = makeDataConSelector Nothing c i
-
--- | `qualifyDataCtor` qualfies the field names for each `DataCtor` to
---   ensure things work properly when exported.
-type CtorType = ([(F.Symbol, SpecType)], SpecType)
-
-qualifyDataCtor :: Bool -> ModName -> F.Located a -> CtorType -> CtorType
-qualifyDataCtor qualFlag name l ct@(xts, st)
- | qualFlag  = (xts', t')
- | otherwise = ct
- where
-   t'        = F.subst su <$> st
-   xts'      = [ (qx, F.subst su t)       | (qx, t, _) <- fields ]
-   su        = F.mkSubst [ (x, F.eVar qx) | (qx, _, Just x) <- fields ]
-   fields    = [ (qx, t, mbX) | (x, t) <- xts, let (mbX, qx) = qualifyField name (F.atLoc l x) ]
-
-qualifyField :: ModName -> LocSymbol -> (Maybe F.Symbol, F.Symbol)
-qualifyField name lx
- | needsQual = (Just x, F.notracepp msg $ qualifyModName name x)
- | otherwise = (Nothing, x)
- where
-   msg       = "QUALIFY-NAME: " ++ show x ++ " in module " ++ show (F.symbol name)
-   x         = val lx
-   needsQual = not (isWiredIn lx)
+    isTmp     = F.isPrefixOfSym F.tempPrefix . lhNameToUnqualifiedSymbol
+    xi        = makeGeneratedLogicLHName (makeDataConSelector Nothing c i)
 
 checkRecordSelectorSigs :: [(Ghc.Var, LocSpecType)] -> [(Ghc.Var, LocSpecType)]
 checkRecordSelectorSigs vts = [ (v, take1 v lspecTys) | (v, lspecTys) <- Misc.groupList vts ]
@@ -824,10 +800,10 @@ makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne
              | (x, t) <- reverse args -- NOTE: the reverse here is correct
              , let vv = rTypeValueVar t
                -- the measure singleton refinement, eg `v = getBar foo`
-             , let mt = RT.uReft (vv, F.PAtom F.Eq (F.EVar vv) (F.EApp (F.EVar x) (F.EVar z)))
+             , let mt = RT.uReft (vv, F.PAtom F.Eq (F.EVar vv) (F.EApp (F.EVar $ logicNameToSymbol x) (F.EVar z)))
              ]
 
-      su   = F.mkSubst [ (x, F.EApp (F.EVar x) (F.EVar z)) | x <- fst <$> args ]
+      su   = F.mkSubst [ (lhNameToUnqualifiedSymbol x, F.EApp (F.EVar (logicNameToSymbol x)) (F.EVar z)) | x <- fst <$> args ]
       args = dcpTyArgs dcp
       z    = "lq$recSel"
       res  = dropPreds (dcpTyRes dcp)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index fe72ef6f87..88d44d7d80 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
@@ -241,7 +241,7 @@ dataConDecl d     = {- F.notracepp msg $ -} DataCtor dx (F.symbol <$> as) [] xts
   where
     isGadt        = not (Ghc.isVanillaDataCon d)
     -- msg           = printf "dataConDecl (gadt = %s)" (show isGadt)
-    xts           = [(Bare.makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]
+    xts           = [(makeGeneratedLogicLHName $ Bare.makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]
     dx            = makeGHCLHNameLocated d
     its           = zip [1..] ts
     (as,_ps,ts,ty)  = Ghc.dataConSig d
@@ -275,7 +275,7 @@ makeMeasureSelectors cfg dm (Loc l l' c)
       = Nothing
       | otherwise
         -- TODO: Use as origin module the module where the measure is created
-      = Just $ makeMeasureSelector (Loc l l' (makeGeneratedLogicLHName x)) (projT i) dc n i
+      = Just $ makeMeasureSelector (Loc l l' x) (projT i) dc n i
 
     go' ((_,t), i)
       -- do not make selectors for functional fields
@@ -393,19 +393,18 @@ getDefinedSymbolsInLogic env measEnv specs =
   S.unions (uncurry getFromAxioms <$> specsList) -- reflections that ended up in equations
     `S.union` getLocReflects (Just env) specs -- reflected symbols
     `S.union` measVars -- Get the data constructors, ex. for Lit00.0
-    `S.union` S.unions (uncurry getDataDecls <$> specsList) -- get the Predicated type defs, ex. for T1669.CSemigroup
+    `S.union` S.unions (getDataDecls . snd <$> specsList) -- get the Predicated type defs, ex. for T1669.CSemigroup
     `S.union` S.unions (getAliases . snd <$> specsList) -- aliases, ex. for T1738Lib.incr
   where
     specsList = M.toList specs
     getFromAxioms modName spec = S.fromList $
       Bare.qualifyLocSymbolTop env modName . localize . F.eqName <$> Ms.axeqs spec
     measVars     = S.fromList $ localize . fst <$> getMeasVars env measEnv
-    getDataDecls modName spec = S.unions $
-      getFromDataCtor modName <$>
+    getDataDecls spec = S.unions $
+      getFromDataCtor <$>
         concat (tycDCons `Mb.mapMaybe` (dataDecls spec ++ newtyDecls spec))
-    getFromDataCtor modName decl = S.fromList $
-      Bare.qualifyLocSymbolTop env modName <$>
-        (fmap getLHNameSymbol (dcName decl) : (localize . fst <$> dcFields decl))
+    getFromDataCtor decl = S.fromList $
+      map (dummyLoc . logicNameToSymbol) $ val (dcName decl) : (fst <$> dcFields decl)
     getAliases spec = S.fromList $ fmap rtName <$> Ms.ealiases spec
     localize :: F.Symbol -> F.LocSymbol
     localize sym = maybe (dummyLoc sym) varLocSym $ L.lookup sym (Bare.reSyms env)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
index 1c22284479..2326728f6d 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
@@ -10,6 +10,7 @@ module Language.Haskell.Liquid.Bare.Plugged
   ) where
 
 import Prelude hiding (error)
+import qualified Data.Bifunctor as Bifunctor
 import Data.Generics.Aliases (mkT)
 import Data.Generics.Schemes (everywhere)
 
@@ -26,6 +27,7 @@ import qualified Liquid.GHC.API   as Ghc
 import           Language.Haskell.Liquid.GHC.Types (StableName, mkStableName)
 import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Errors
+import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.RefType
 import           Language.Haskell.Liquid.Types.RType
 import           Language.Haskell.Liquid.Types.RTypeOp
@@ -137,17 +139,19 @@ makePluggedDataCon allowTC embs tyi ldcp
 plugMany :: Bool -> F.TCEmb Ghc.TyCon -> Bare.TyConMap
          -> Located DataConP
          -> ([Ghc.Var], [Ghc.Type],             Ghc.Type)   -- ^ hs type
-         -> ([RTyVar] , [(F.Symbol, SpecType)], SpecType)   -- ^ lq type
-         -> ([(F.Symbol, SpecType)], SpecType)              -- ^ plugged lq type
+         -> ([RTyVar] , [(LHName, SpecType)], SpecType)   -- ^ lq type
+         -> ([(LHName, SpecType)], SpecType)              -- ^ plugged lq type
 plugMany allowTC embs tyi ldcp (hsAs, hsArgs, hsRes) (lqAs, lqArgs, lqRes)
-                     = F.notracepp msg (drop nTyVars (zip xs ts), t)
+                     = F.notracepp msg (drop nTyVars (zip (map lookupLHName xs) ts), t)
   where
+    lookupLHName s = Mb.fromMaybe (panic (Just (GM.fSrcSpan ldcp)) $ "unexpected symbol: " ++ show s) $ lookup s lhNameMap
+    lhNameMap = [ (lhNameToUnqualifiedSymbol n, n) | n <- map fst lqArgs ]
     ((xs,_,ts,_), t) = bkArrow (val pT)
     pT               = plugHoles allowTC (Bare.LqTV dcName) embs tyi (const killHoles) hsT (F.atLoc ldcp lqT)
     hsT              = foldr (Ghc.mkFunTy Ghc.FTF_T_T Ghc.ManyTy) hsRes hsArgs'
     lqT              = foldr (uncurry (rFun' (classRFInfo allowTC))) lqRes lqArgs'
     hsArgs'          = [ Ghc.mkTyVarTy a               | a <- hsAs] ++ hsArgs
-    lqArgs'          = [(F.dummySymbol, RVar a mempty) | a <- lqAs] ++ lqArgs
+    lqArgs'          = [(F.dummySymbol, RVar a mempty) | a <- lqAs] ++ map (Bifunctor.first lhNameToUnqualifiedSymbol) lqArgs
     nTyVars          = length hsAs -- == length lqAs
     dcName           = Ghc.dataConName . dcpCon . val $ ldcp
     msg              = "plugMany: " ++ F.showpp (dcName, hsT, lqT)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs
index 28f892acd1..01e5c53e30 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs
@@ -162,9 +162,9 @@ classDeclToDataDecl cls refinedIds = DataDecl
   fields = fmap attachRef classIds
   attachRef sid
     | Just ref <- L.lookup sid refinedIds
-    = (F.symbol sid, RT.subts tyVarSubst (F.val ref))
+    = (makeGHCLHNameFromId sid, RT.subts tyVarSubst (F.val ref))
     | otherwise
-    = (F.symbol sid, RT.bareOfType . dropTheta . Ghc.varType $ sid)
+    = (makeGHCLHNameFromId sid, RT.bareOfType . dropTheta . Ghc.varType $ sid)
 
   tyVarSubst = [ (GM.dropModuleUnique v, v) | v <- tyVars ]
 
@@ -189,10 +189,10 @@ elaborateClassDcp
 elaborateClassDcp coreToLg simplifier dcp = do
   t' <- flip (zipWith addCoherenceOblig) prefts
     <$> forM fts (elaborateSpecType coreToLg simplifier)
-  let ts' = elaborateMethod (F.symbol dc) (S.fromList xs) <$> t'
+  let ts' = elaborateMethod (F.symbol dc) (S.fromList $ map logicNameToSymbol xs) <$> t'
   pure
     ( dcp { dcpTyArgs = zip xs (stripPred <$> ts') }
-    , dcp { dcpTyArgs = fmap (\(x, t) -> (x, strengthenTy x t)) (zip xs t') }
+    , dcp { dcpTyArgs = fmap (\(x, t) -> (x, strengthenTy (logicNameToSymbol x) t)) (zip xs t') }
     )
  where
   addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType
@@ -393,7 +393,7 @@ makeClassAuxTypesOne elab (ldcp, inst, methods) =
     -- Monoid.mappend, ...
     clsMethods = filter (\x -> GM.dropModuleNames (F.symbol x) `elem` fmap mkSymbol methods) $
       Ghc.classAllSelIds (Ghc.is_cls inst)
-    yts = [(GM.dropModuleNames y, t) | (y, t) <- dcpTyArgs dcp]
+    yts = [(logicNameToSymbol y, t) | (y, t) <- dcpTyArgs dcp]
     mkSymbol x
       | -- F.notracepp ("isDictonaryId:" ++ GM.showPpr x) $
         Ghc.isDictonaryId x = F.mappendSym "$" (F.dropSym 2 $ GM.simplesymbol x)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index cd550dc618..676f1e1ef5 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -131,12 +131,18 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
             -- A generic traversal that resolves names of Haskell entities
             sp1 <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) $
                      fixExpressionArgsOfTypeAliases taliases bareSpec0
+            -- Data decls contain fieldnames that introduce measures with the
+            -- same names. We resolved them before constructing the logic
+            -- environment.
+            dataDecls <- mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
+            let sp2 = sp1 {dataDecls}
+
             (es0,_) <- get
             if null es0 then do
               -- Now we do a second traversal to resolve logic names
               let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
-                    makeLogicEnvs impMods thisModule sp1 dependencies
-              sp2 <- fromBareSpecLHName <$>
+                    makeLogicEnvs impMods thisModule sp2 dependencies
+              sp3 <- fromBareSpecLHName <$>
                        resolveLogicNames
                          cfg
                          inScopeEnv
@@ -146,8 +152,8 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
                          localVars
                          logicNameEnv0
                          privateReflectNames
-                         sp1
-              return (sp2, logicNameEnv0)
+                         sp2
+              return (sp3, logicNameEnv0)
             else
               return (error "resolveLHNames: invalid spec", error "resolveLHNames: invalid logic environment")
         logicNameEnv' = extendLogicNameEnv logicNameEnv ns
@@ -158,6 +164,11 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
   where
     taliases = collectTypeAliases thisModule bareSpec0 dependencies
 
+    resolveFieldLogicName n =
+      case n of
+        LHNUnresolved LHLogicNameBinder s -> pure $ makeLogicLHName s thisModule Nothing
+        _ -> panic Nothing $ "unexpected name: " ++ show n
+
     resolveLHName lname = case val lname of
       LHNUnresolved LHTcName s
         | isTuple s ->
@@ -433,13 +444,9 @@ makeLogicEnvs impAvails thisModule spec dependencies =
         -- by renaming.
         unhandledNames = HS.fromList $
           map unqualify unhandledNamesList ++ map (LH.qualifySymbol (symbol $ GHC.moduleName thisModule)) unhandledNamesList
-        unhandledNamesList = concat $
-          [ map (rtName . val) $ ealiases spec
-          , map fst $
-             concatMap DataDecl.dcFields $ concat $
-             mapMaybe DataDecl.tycDCons $
-             dataDecls spec
-          ] ++ map (map getLHNameSymbol . snd) unhandledLogicNames
+        unhandledNamesList =
+          map (rtName . val) (ealiases spec)
+          ++ concatMap (map getLHNameSymbol . snd) unhandledLogicNames
         unhandledLogicNames =
           map (fmap collectUnhandledLiftedSpecLogicNames) dependencyPairs
         logicNames =
@@ -458,6 +465,10 @@ makeLogicEnvs impAvails thisModule spec dependencies =
             ]
           , [ val (msName m) | m <- measures spec ]
           , [ val (msName m) | m <- cmeasures spec ]
+          , map fst $
+             concatMap DataDecl.dcFields $ concat $
+             mapMaybe DataDecl.tycDCons $
+             dataDecls spec
           ]
         privateReflectNames =
           mconcat $
@@ -527,19 +538,16 @@ makeLogicEnvs impAvails thisModule spec dependencies =
 {- HLINT ignore collectUnhandledLiftedSpecLogicNames "Use ++" -}
 collectUnhandledLiftedSpecLogicNames :: LiftedSpec -> [LHName]
 collectUnhandledLiftedSpecLogicNames sp =
-    concat
-      [ map (makeLocalLHName . LH.dropModuleNames . rtName . val) $ HS.toList $ liftedEaliases sp
-      , map (makeLocalLHName . LH.dropModuleNames . fst) $
-        concatMap DataDecl.dcFields $ concat $
-        mapMaybe DataDecl.tycDCons $
-        HS.toList $ liftedDataDecls sp
-      ]
+    map (makeLocalLHName . LH.dropModuleNames . rtName . val) $ HS.toList $ liftedEaliases sp
 
 collectLiftedSpecLogicNames :: LiftedSpec -> [LHName]
 collectLiftedSpecLogicNames sp = concat
     [ map fst (HS.toList $ liftedExpSigs sp)
     , map (val . msName) (HM.elems $ liftedMeasures sp)
     , map (val . msName) (HM.elems $ liftedCmeasures sp)
+    , map fst $ concatMap DataDecl.dcFields $ concat $
+        mapMaybe DataDecl.tycDCons $
+        HS.toList $ liftedDataDecls sp
     ]
 
 -- | Resolves names in the logic namespace
@@ -567,7 +575,7 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
       (map localVarToSymbol . maybe [] lvdLclEnv . (GHC.lookupNameEnv (lvNames localVars) <=< getLHGHCName))
       resolveLogicName
       (emapBareTypeVM (bscope cfg) resolveLogicName)
-      sp { imeasures }
+      sp {imeasures}
   where
     resolveIMeasLogicName lx =
       case val lx of
@@ -611,7 +619,7 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
         s = val ls
         wiredInNames =
            map fst wiredSortedSyms ++
-           map fst (concatMap (DataDecl.dcpTyArgs . val) wiredDataCons)
+           map (logicNameToSymbol . fst) (concatMap (DataDecl.dcpTyArgs . val) wiredDataCons)
 
     errResolveLogicName s alts =
       ErrResolve
@@ -710,6 +718,16 @@ mapMeasureNamesM f m = do
       measure <- f (measure d)
       return d {measure}
 
+mapDataDeclFieldNamesM :: Monad m => (LHName -> m LHName) -> DataDecl.DataDeclP v ty -> m (DataDecl.DataDeclP v ty)
+mapDataDeclFieldNamesM f d = do
+    tycDCons <- traverse (mapM (mapDataCtorFieldsM f)) (DataDecl.tycDCons d)
+    return d{DataDecl.tycDCons}
+  where
+    mapDataCtorFieldsM :: Monad m => (LHName -> m LHName) -> DataDecl.DataCtorP ty -> m (DataDecl.DataCtorP ty)
+    mapDataCtorFieldsM f1 c = do
+      dcFields <- mapM (\(n, t) -> (, t) <$> f1 n) (DataDecl.dcFields c)
+      return c{DataDecl.dcFields}
+
 toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName
 toBareSpecLHName cfg env sp0 = runIdentity $ go sp0
   where
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index d6516b7a6b..991e453bad 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -21,6 +21,7 @@ module Language.Haskell.Liquid.Parse
 import           Control.Arrow                          (second)
 import           Control.Monad
 import           Control.Monad.Identity
+import           Data.Bifunctor                         (first)
 import qualified Data.Char                              as Char
 import qualified Data.Foldable                          as F
 import           Data.String
@@ -1509,11 +1510,13 @@ mkConsPat x lc y = (makeGHCLHName (GHC.getName GHC.consDataCon) (symbol GHC.cons
 --------------------------------- Predicates ----------------------------------
 -------------------------------------------------------------------------------
 
-dataConFieldsP :: Parser [(Symbol, BareTypeParsed)]
+dataConFieldsP :: Parser [(LHName, BareTypeParsed)]
 dataConFieldsP
-   =  explicitCommaBlock predTypeDDP -- braces (sepBy predTypeDDP comma)
-  <|> many dataConFieldP
-  <?> "dataConFieldP"
+   = map (first (makeUnresolvedLHName LHLogicNameBinder)) <$>
+     (explicitCommaBlock predTypeDDP -- braces (sepBy predTypeDDP comma)
+       <|> many dataConFieldP
+       <?> "dataConFieldP"
+     )
 
 dataConFieldP :: Parser (Symbol, BareTypeParsed)
 dataConFieldP
@@ -1551,8 +1554,8 @@ tRepVars as tr = case fst <$> ty_vars tr of
   [] -> as
   vs -> symbol . ty_var_value <$> vs
 
-tRepFields :: RTypeRepV v c tv r -> [(Symbol, RTypeV v c tv r)]
-tRepFields tr = zip (ty_binds tr) (ty_args tr)
+tRepFields :: RTypeRepV v c tv r -> [(LHName, RTypeV v c tv r)]
+tRepFields tr = zip (map (makeUnresolvedLHName LHLogicNameBinder) $ ty_binds tr) (ty_args tr)
 
 -- TODO: fix Located
 dataConNameP :: Parser (Located Symbol)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/DataDecl.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/DataDecl.hs
index 8ba310090c..f4f1298fb9 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/DataDecl.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/DataDecl.hs
@@ -84,7 +84,7 @@ data DataCtorP ty = DataCtor
   { dcName   :: F.Located LHName       -- ^ DataCon name
   , dcTyVars :: [F.Symbol]             -- ^ Type parameters
   , dcTheta  :: [ty]                   -- ^ The GHC ThetaType corresponding to DataCon.dataConSig
-  , dcFields :: [(F.Symbol, ty)]       -- ^ field-name and field-Type pairs
+  , dcFields :: [(LHName, ty)]       -- ^ field-name and field-Type pairs
   , dcResult :: Maybe ty               -- ^ Possible output (if in GADT form)
   } deriving (Data, Typeable, Generic, Eq, Functor, Foldable, Traversable)
 
@@ -168,7 +168,7 @@ data DataConP = DataConP
   , dcpFreeTyVars :: ![RTyVar]               -- ^ Type parameters
   , dcpFreePred   :: ![PVar RSort]           -- ^ Abstract Refinement parameters
   , dcpTyConstrs  :: ![SpecType]             -- ^ ? Class constraints (via `dataConStupidTheta`)
-  , dcpTyArgs     :: ![(F.Symbol, SpecType)] -- ^ Value parameters
+  , dcpTyArgs     :: ![(LHName, SpecType)] -- ^ Value parameters
   , dcpTyRes      :: !SpecType               -- ^ Result type
   , dcpIsGadt     :: !Bool                   -- ^ Was this specified in GADT style (if so, DONT use function names as fields)
   , dcpModule     :: !F.Symbol               -- ^ Which module was this defined in
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index 417a15acf5..f6645cf116 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -16,6 +16,7 @@ module Language.Haskell.Liquid.Types.Names
   , getLHNameResolved
   , getLHNameSymbol
   , logicNameToSymbol
+  , lhNameToUnqualifiedSymbol
   , makeGHCLHName
   , makeGHCLHNameFromId
   , makeGHCLHNameLocated
@@ -250,7 +251,7 @@ getLHNameSymbol :: LHName -> Symbol
 getLHNameSymbol (LHNResolved _ s) = s
 getLHNameSymbol (LHNUnresolved _ s) = s
 
--- | Get the unresolved Symbol from an LHName.
+-- | Get the resolved Symbol from an LHName.
 getLHNameResolved :: HasCallStack => LHName -> LHResolvedName
 getLHNameResolved (LHNResolved n _) = n
 getLHNameResolved n@LHNUnresolved{} = error $ "getLHNameResolved: unresolved name: " ++ showLHNameDebug n
@@ -316,8 +317,16 @@ logicNameToSymbol (LHNResolved (LHRLogic (LogicName s om mReflectionOf)) _) =
           -}
 logicNameToSymbol (LHNResolved (LHRLogic (GeneratedLogicName s)) _) = s
 logicNameToSymbol (LHNResolved (LHRLocal s) _) = s
+logicNameToSymbol (LHNResolved (LHRGHC n) _) = symbol $ GHC.getOccString n
 logicNameToSymbol n = error $ "logicNameToSymbol: unexpected name: " ++ show n
 
+lhNameToUnqualifiedSymbol :: HasCallStack => LHName -> Symbol
+lhNameToUnqualifiedSymbol (LHNResolved (LHRLogic (LogicName s _ _)) _) = s
+lhNameToUnqualifiedSymbol (LHNResolved (LHRLogic (GeneratedLogicName s)) _) = s
+lhNameToUnqualifiedSymbol (LHNResolved (LHRLocal s) _) = s
+lhNameToUnqualifiedSymbol (LHNResolved (LHRGHC n) _) = symbol $ GHC.getOccString n
+lhNameToUnqualifiedSymbol n = error $ "lhNameToUnqualifiedSymbol: unexpected name: " ++ show n
+
 -- | Creates a name in the logic namespace for the given Haskell name.
 reflectLHName :: HasCallStack => GHC.Module -> LHName -> LHName
 reflectLHName thisModule (LHNResolved (LHRGHC n) _) = reflectGHCName thisModule n
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs
index f69a1f9740..9b22aeeb33 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs
@@ -56,6 +56,7 @@ import           Language.Haskell.Liquid.GHC.Misc
 import           Language.Haskell.Liquid.Misc
 import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Errors
+import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.RefType hiding (generalize)
 import           Language.Haskell.Liquid.Types.RType
 import           Language.Haskell.Liquid.Types.RTypeOp
@@ -183,16 +184,18 @@ dcWrapSpecType allowTC dc (DataConP _ _ vs ps cs yts rt _ _ _)
     mkArrow makeVars' ps ts' rt'
   where
     isCls    = Ghc.isClassTyCon $ Ghc.dataConTyCon dc
-    (as, sts) = unzip (reverse yts)
+    (as0, sts) = unzip (reverse yts)
+    as = map logicNameToSymbol as0
+    as1 = map lhNameToUnqualifiedSymbol as0
     mkDSym z = F.symbol z `F.suffixSymbol` F.symbol dc
     bs       = mkDSym <$> as
     tx _  []     []     []     = []
     tx su (x:xs) (y:ys) (t:ts) = (y, classRFInfo allowTC , if allowTC && isCls then t else F.subst (F.mkSubst su) t, mempty)
                                : tx ((x, F.EVar y):su) xs ys ts
     tx _ _ _ _ = panic Nothing "PredType.dataConPSpecType.tx called on invalid inputs"
-    yts'     = tx [] as bs sts
+    yts'     = tx [] as1 bs sts
     ts'      = map ("" , classRFInfo allowTC , , mempty) cs ++ yts'
-    subst    = F.mkSubst [(x, F.EVar y) | (x, y) <- zip as bs]
+    subst    = F.mkSubst [(x, F.EVar y) | (x, y) <- zip as1 bs]
     rt'      = F.subst subst rt
     makeVars = filter (`elem` fvs) $ zipWith (\v a -> RTVar v (rTVarInfo a :: RTVInfo RSort)) vs (fst $ splitForAllTyCoVars $ dataConRepType dc)
     makeVars' = map (, mempty) makeVars 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RTypeOp.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RTypeOp.hs
index 69e1c5fb83..ebe1ac272f 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RTypeOp.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RTypeOp.hs
@@ -74,6 +74,7 @@ import           Language.Fixpoint.Types (Expr, Symbol)
 
 import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Errors
+import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.RType
 import           Language.Haskell.Liquid.Misc
 
@@ -415,8 +416,8 @@ emapDataCtorTyM
   -> m (DataCtorP ty')
 emapDataCtorTyM f d = do
     dcTheta <- mapM (f []) (dcTheta d)
-    dcResult <- traverse (f (map fst (dcFields d))) $ dcResult d
-    dcFields <- snd <$> mapAccumM (\γ  (s, t) -> (s:γ,) . (s,) <$> f γ t) [] (dcFields d)
+    dcResult <- traverse (f (map (lhNameToUnqualifiedSymbol . fst) (dcFields d))) $ dcResult d
+    dcFields <- snd <$> mapAccumM (\γ  (s, t) -> (lhNameToUnqualifiedSymbol s:γ,) . (s,) <$> f γ t) [] (dcFields d)
     return d{dcTheta, dcFields, dcResult}
 
 emapExprArg :: ([Symbol] -> Expr -> Expr) -> [Symbol] -> RType c tv r -> RType c tv r
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
index b8856d9f7e..9c3834ee84 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
@@ -33,16 +33,17 @@ import Language.Haskell.Liquid.GHC.Misc
 import qualified Liquid.GHC.API as Ghc
 import Liquid.GHC.API (Var, Arity, TyVar, Bind(..), Boxity(..), Expr(..), ForAllTyFlag(Required))
 import Language.Haskell.Liquid.Types.Errors
+import Language.Haskell.Liquid.Types.Names
 import Language.Haskell.Liquid.Types.RType
 import Language.Haskell.Liquid.Types.Types
 import Language.Haskell.Liquid.Types.RefType
 import Language.Haskell.Liquid.Types.Variance
 import Language.Haskell.Liquid.Types.PredType
-import Language.Haskell.Liquid.Types.Names (selfSymbol)
 
 -- import Language.Fixpoint.Types hiding (panic)
 import qualified Language.Fixpoint.Smt.Theories as F
 import qualified Language.Fixpoint.Types as F
+import           Data.Bifunctor (first)
 import qualified Data.HashSet as S
 import           Data.Maybe
 
@@ -165,7 +166,7 @@ wiredTyDataCons = (concat tcs, dummyLoc <$> concat dcs)
     (tcs, dcs)  = unzip $ listTyDataCons : map tupleTyDataCons [2..maxArity]
 
 charDataCon :: Located DataConP
-charDataCon = dummyLoc (DataConP l0 Ghc.charDataCon  [] [] [] [("charX",lt)] lt False wiredInName l0)
+charDataCon = dummyLoc (DataConP l0 Ghc.charDataCon  [] [] [] [(makeGeneratedLogicLHName "charX",lt)] lt False wiredInName l0)
   where
     l0 = F.dummyPos "LH.Bare.charTyDataCons"
     c  = Ghc.charTyCon
@@ -188,7 +189,7 @@ listTyDataCons   = ( [TyConP l0 c [RTV tyv] [p] [Covariant] [Covariant] (Just fs
       lt         = rApp c [xt] [rPropP [] $ pdVarReft p] mempty
       xt         = rVar tyv
       xst        = rApp c [RVar (RTV tyv) px] [rPropP [] $ pdVarReft p] mempty
-      cargs      = [(xTail, xst), (xHead, xt)]
+      cargs      = map (first makeGeneratedLogicLHName) $ [(xTail, xst), (xHead, xt)]
       fsize      = SymSizeFun (dummyLoc "GHC.Types_LHAssumptions.len")
 
 wiredInName :: F.Symbol
@@ -213,7 +214,7 @@ tupleTyDataCons n = ( [TyConP   l0 c  (RTV <$> tyvs) ps tyvarinfo pdvarinfo Noth
     pxs           = mkps pnames (ta:ts) ((fld, F.EVar x1) : zip flds (F.EVar <$> xs))
     lt            = rApp c (rVar <$> tyvs) (rPropP [] . pdVarReft <$> ups) mempty
     xts           = zipWith (\v p -> RVar (RTV v) (pdVarReft p)) tvs pxs
-    cargs         = reverse $ (x1, rVar tv) : zip xs xts
+    cargs         = map (first makeGeneratedLogicLHName) $ reverse $ (x1, rVar tv) : zip xs xts
     pnames        = mks_ "p"
     mks  x        = (\i -> F.symbol (x++ show i)) <$> [1..n]
     mks_ x        = (\i -> F.symbol (x++ show i)) <$> [2..n]

From ebddb61daad45def6db9a4312bbdcd01b4363343 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Wed, 11 Dec 2024 18:48:48 +0000
Subject: [PATCH 02/16] Update tests

---
 tests/errors/MissingField2.hs | 16 ----------------
 tests/names/pos/DataFields.hs | 16 ++++++++++++++++
 tests/tests.cabal             |  2 +-
 3 files changed, 17 insertions(+), 17 deletions(-)
 delete mode 100644 tests/errors/MissingField2.hs
 create mode 100644 tests/names/pos/DataFields.hs

diff --git a/tests/errors/MissingField2.hs b/tests/errors/MissingField2.hs
deleted file mode 100644
index 49131d66b0..0000000000
--- a/tests/errors/MissingField2.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-{-@ LIQUID "--expect-error-containing=Unbound symbol fxx"@-}
-module MissingField2 where
-
-data F a = F {fx :: a, fy :: a, fzz :: a} | G {fx :: a}
-
-{-@ data F a = F { fxx :: a, fy :: a, fz :: a}
-             | G { fxx :: a } 
-  @-}
-
-{-@ fooG :: x:a -> {v : F a | (fxx v) > x} @-}
-fooG :: a -> F a
-fooG x = G x 
-
-{-@ foo :: x:a -> {v : F a | (fxx v) > x} @-}
-foo :: a -> F a
-foo x = F x x x
diff --git a/tests/names/pos/DataFields.hs b/tests/names/pos/DataFields.hs
new file mode 100644
index 0000000000..1f595ef7bf
--- /dev/null
+++ b/tests/names/pos/DataFields.hs
@@ -0,0 +1,16 @@
+-- | Test that data field names are resolved
+module DataFields where
+
+data F a = F {fx :: a, fy :: a, fzz :: a} | G {fx :: a}
+
+{-@ data F a = F { fxx :: a, fy :: a, fz :: a}
+             | G { fxx :: a }
+  @-}
+
+{-@ fooG :: x:a -> {v : F a | (fxx v) >= x} @-}
+fooG :: a -> F a
+fooG x = G x
+
+{-@ foo :: x:a -> {v : F a | (fxx v) >= x} @-}
+foo :: a -> F a
+foo x = F x x x
diff --git a/tests/tests.cabal b/tests/tests.cabal
index d4afe8964e..13335bc7a4 100644
--- a/tests/tests.cabal
+++ b/tests/tests.cabal
@@ -679,7 +679,6 @@ executable errors
                     , LocalHole
                     , MissingAssume
                     -- , MissingField1
-                    , MissingField2
                     , MissingReflect
                     , MissingSizeFun
                     , MultiInstMeasures
@@ -785,6 +784,7 @@ executable names-pos
                     , Capture01
                     , Capture02
                     , ClojurVector
+                    , DataFields
                     , ExpandsDependentPairs
                     , HideName00
                     , HidePrelude

From 9ddc514027b714c75a161439047e06288aaeb628 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 13:32:10 +0000
Subject: [PATCH 03/16] Fix logic names constructed for data constructors and
 logic map names

---
 .../Haskell/Liquid/LHNameResolution.hs        | 36 +++++++++++--------
 1 file changed, 21 insertions(+), 15 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index 676f1e1ef5..4ed57786c0 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -634,26 +634,33 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
         )
 
     resolveDataConName ls
-      | LH.dropModuleNames s == ":" = Just $
-        return $ makeLocalLHName s
-      | LH.dropModuleNames s == "[]" = Just $
-        return $ makeLocalLHName s
-      | isTupleDC (symbolText s) = Just $
-        return $ makeLocalLHName s
+      | unqualifiedS == ":" = Just $
+        return $ makeLogicLHName unqualifiedS (GHC.nameModule consDataConName) (Just consDataConName)
+      | unqualifiedS == "[]" = Just $
+        return $ makeLogicLHName unqualifiedS (GHC.nameModule nilDataConName) (Just nilDataConName)
+      | Just arity <- isTupleDC (symbolText s) = Just $
+          let dcName = tupleDataConName arity
+           in return $ makeLogicLHName s (GHC.nameModule dcName) (Just dcName)
       where
+        unqualifiedS = LH.dropModuleNames s
+        nilDataConName = GHC.getName $ GHC.dataConWorkId $ GHC.nilDataCon
+        consDataConName = GHC.getName $ GHC.dataConWorkId $ GHC.consDataCon
+        tupleDataConName = GHC.getName . GHC.dataConWorkId . GHC.tupleDataCon GHC.Boxed
         s = val ls
-        isTupleDC t =
-          Text.isPrefixOf "(" t && Text.isSuffixOf ")" t &&
-          Text.all (== ',') (Text.init $ Text.tail t)
+        isTupleDC t
+          | Text.isPrefixOf "(" t && Text.isSuffixOf ")" t &&
+            Text.all (== ',') (Text.init $ Text.tail t)
+          = Just $ Text.length t - 2
+          | otherwise
+          = Nothing
     resolveDataConName s =
       case GHC.lookupGRE globalRdrEnv (mkLookupGRE (LHDataConName LHAnyModuleNameF) $ val s) of
         [e] -> do
           let n = GHC.greName e
           Just $ do
-            let lhName = makeLogicLHName (symbol n) (GHC.nameModule n)  (Just n)
+            let lhName = makeLogicLHName (symbol $ GHC.getOccString n) (GHC.nameModule n) (Just n)
             addName lhName
-            -- return lhName
-            return $ makeLocalLHName $ val s
+            return lhName
         [] ->
           Nothing
         es ->
@@ -687,10 +694,9 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
             let n = GHC.greName e
             if HM.member (symbol n) (lmSymDefs lmap) then
               Just $ do
-                let lhName = makeLogicLHName (symbol n) (GHC.nameModule n) Nothing
+                let lhName = makeLogicLHName (symbol $ GHC.getOccString n) (GHC.nameModule n) Nothing
                 addName lhName
-                -- return lhName
-                return $ makeLocalLHName $ val s
+                return lhName
             else
               Nothing
           [] ->

From 9240ed3b57af28a25eb46614c0794a94c01754e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 13:44:57 +0000
Subject: [PATCH 04/16] Remove the obsolete qualifyExpand

---
 .../src/Language/Haskell/Liquid/Bare.hs       | 30 +++++++------------
 .../Language/Haskell/Liquid/Bare/Expand.hs    | 23 ++------------
 .../Language/Haskell/Liquid/Bare/Measure.hs   | 14 ++++-----
 3 files changed, 20 insertions(+), 47 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index d1ff902fea..a7931b7dcf 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -317,14 +317,8 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
     simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
     simplifier = pure -- no simplification
     allowTC  = typeclass cfg
-    mySpec2  = Bare.qualifyExpand env name rtEnv l [] mySpec1    where l = F.dummyPos "expand-mySpec2"
-    iSpecs2  = Bare.qualifyExpand
-                 env
-                 name
-                 rtEnv
-                 (F.dummyPos "expand-iSpecs2")
-                 []
-                 (M.fromList dependencySpecs)
+    mySpec2  = Bare.expand rtEnv l mySpec1    where l = F.dummyPos "expand-mySpec2"
+    iSpecs2  = Bare.expand rtEnv (F.dummyPos "expand-iSpecs2") (M.fromList dependencySpecs)
     rtEnv    = Bare.makeRTEnv env name mySpec1 dependencySpecs lmap
     mspecs   = (name, mySpec0) : dependencySpecs
     (mySpec0, instMethods)  = if allowTC
@@ -713,7 +707,7 @@ addReflSigs env name rtEnv measEnv refl sig =
     -- the functions, we are left with a pair (Var, LocSpecType). The latter /needs/ to be qualified and
     -- expanded again, for example in case it has expression aliases derived from 'inlines'.
     expandReflectedSignature :: (Ghc.Var, LocSpecType) -> (Ghc.Var, LocSpecType)
-    expandReflectedSignature = fmap (Bare.qualifyExpand env name rtEnv (F.dummyPos "expand-refSigs") [])
+    expandReflectedSignature = fmap (Bare.expand rtEnv (F.dummyPos "expand-refSigs"))
 
     reflSigs = [ (x, t) | (x, t, _) <- gsHAxioms refl ]
     -- Get the set of all the actual functions (in assume-reflects)
@@ -811,7 +805,7 @@ 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                     spec
-  expSigs    <- makeTExpr  env name bareSigs rtEnv spec
+  expSigs    <- makeTExpr  env bareSigs rtEnv spec
   let rawSigs = Bare.resolveLocalBinds env expSigs
   return [ (x, cook x bt, z) | (x, bt, z) <- rawSigs ]
   where
@@ -858,24 +852,22 @@ myAsmSig v sigs = Mb.fromMaybe errImp (mbHome `mplus` mbImp)
     errImp      = impossible Nothing "myAsmSig: cannot happen as sigs is non-null"
     vName       = GM.takeModuleNames (F.symbol v)
 
-makeTExpr :: Bare.Env -> ModName -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec
+makeTExpr :: Bare.Env -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec
           -> Bare.Lookup [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
-makeTExpr env name tySigs rtEnv spec = do
+makeTExpr env tySigs rtEnv spec = do
   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 ]
+  return [ (v, t, qual <$> es) | (v, (t, es)) <- M.toList vSigExprs ]
   where
-    qual t es   = qualifyTermExpr env name rtEnv t <$> es
+    qual es   = expandTermExpr rtEnv <$> es
     vSigs       = M.fromList tySigs
 
-qualifyTermExpr :: Bare.Env -> ModName -> BareRTEnv -> LocBareType -> Located F.Expr
-                -> Located F.Expr
-qualifyTermExpr env name rtEnv t le
-        = F.atLoc le (Bare.qualifyExpand env name rtEnv l bs e)
+expandTermExpr :: BareRTEnv -> Located F.Expr -> Located F.Expr
+expandTermExpr rtEnv le
+        = F.atLoc le (Bare.expand rtEnv l e)
   where
     l   = F.loc le
     e   = F.val le
-    bs  = ty_binds . toRTypeRep . val $ t
 
 makeVarTExprs :: Bare.Env -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
 makeVarTExprs env spec =
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
index c992b940b2..372f283d9e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -11,8 +11,8 @@ module Language.Haskell.Liquid.Bare.Expand
   ( -- * Create alias expansion environment
     makeRTEnv
 
-    -- * Expand and Qualify
-  , qualifyExpand
+    -- * Expand
+  , Expand(expand)
 
     -- * Converting BareType to SpecType
   , cookSpecType
@@ -275,25 +275,6 @@ buildExprEdges table  = ordNub . go
 class Expand a where
   expand :: BareRTEnv -> F.SourcePos -> a -> a
 
-----------------------------------------------------------------------------------
--- | @qualifyExpand@ first qualifies names so that we can successfully resolve them during expansion.
---
--- When expanding, it's important we pass around a 'BareRTEnv' where the type aliases have been qualified as well.
--- This is subtle, see for example T1761. In that test, we had a type alias \"OneTyAlias a = {v:a | oneFunPred v}\" where
--- \"oneFunPred\" was marked inline. However, inlining couldn't happen because the 'BareRTEnv' had an
--- entry for \"T1761.oneFunPred\", so the relevant expansion of \"oneFunPred\" couldn't happen. This was
--- because the type alias entry inside 'BareRTEnv' mentioned the tuple (\"OneTyAlias\", \"{v:a | oneFunPred v}\") but
--- the 'snd' element needed to be qualified as well, before trying to expand anything.
-----------------------------------------------------------------------------------
-qualifyExpand :: (PPrint a, Expand a, Bare.Qualify a)
-              => Bare.Env -> ModName -> BareRTEnv -> F.SourcePos -> [F.Symbol] -> a -> a
-----------------------------------------------------------------------------------
-qualifyExpand env name rtEnv l bs
-  = expand qualifiedRTEnv l . Bare.qualify env name l bs
-  where
-    qualifiedRTEnv :: BareRTEnv
-    qualifiedRTEnv = rtEnv { typeAliases = M.map (Bare.qualify env name l bs) (typeAliases rtEnv) }
-
 ----------------------------------------------------------------------------------
 expandLoc :: (Expand a) => BareRTEnv -> Located a -> Located a
 expandLoc rtEnv lx = expand rtEnv (F.loc lx) <$> lx
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index 88d44d7d80..f106de4ceb 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
@@ -515,7 +515,7 @@ bareMSpec env sigEnv myName name spec = Ms.mkMSpec ms cms ims oms
     ms         = F.notracepp "UMS" $ filter inScope $ expMeas <$> Ms.measures  spec
     ims        = F.notracepp "IMS" $ filter inScope $ expMeas <$> Ms.imeasures spec
     oms        = F.notracepp "OMS" $ filter inScope $ expMeas <$> Ms.omeasures spec
-    expMeas    = expandMeasure env name  rtEnv
+    expMeas    = expandMeasure rtEnv
     rtEnv      = Bare.sigRTEnv          sigEnv
     force      = name == myName
     inScope z = F.notracepp ("inScope1: " ++ F.showpp (msName z)) (force ||  okSort z)
@@ -560,15 +560,15 @@ mkMeasureSort env name (Ms.MSpec c mm cm im) =
 --------------------------------------------------------------------------------
 -- type BareMeasure = Measure LocBareType LocSymbol
 
-expandMeasure :: Bare.Env -> ModName -> BareRTEnv -> BareMeasure -> BareMeasure
-expandMeasure env name rtEnv m = m
+expandMeasure :: BareRTEnv -> BareMeasure -> BareMeasure
+expandMeasure rtEnv m = m
   { msSort = RT.generalize                   <$> msSort m
-  , msEqns = expandMeasureDef env name rtEnv <$> msEqns m
+  , msEqns = expandMeasureDef rtEnv <$> msEqns m
   }
 
-expandMeasureDef :: Bare.Env -> ModName -> BareRTEnv -> Def t (Located LHName) -> Def t (Located LHName)
-expandMeasureDef env name rtEnv d = d
-  { body  = F.notracepp msg $ Bare.qualifyExpand env name rtEnv l bs (body d) }
+expandMeasureDef :: BareRTEnv -> Def t (Located LHName) -> Def t (Located LHName)
+expandMeasureDef rtEnv d = d
+  { body  = F.notracepp msg $ Bare.expand rtEnv l (body d) }
   where
     l     = loc (measure d)
     bs    = fst <$> binds d

From e33babc5b282fab5c6ea5a16771b7c35e783d345 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 13:47:25 +0000
Subject: [PATCH 05/16] Remove unneeded qualify call from resolveReft

---
 .../src/Language/Haskell/Liquid/Bare/Resolve.hs          | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
index 5ac532879e..675e60d659 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
@@ -839,12 +839,11 @@ ofBareType env name l ps t = either fail' id (ofBareTypeE env name l ps t)
     -- fail                   = Misc.errorP "error-ofBareType" . F.showpp
 
 ofBareTypeE :: HasCallStack => Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
-ofBareTypeE env name l ps t = ofBRType env name (resolveReft env name l ps t) l t
+ofBareTypeE env name l ps t = ofBRType env name (const (resolveReft l ps t)) l t
 
-resolveReft :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> [F.Symbol] -> RReft -> RReft
-resolveReft env name l ps t bs
-        = qualify env name l bs
-        . txParam l RT.subvUReft (RT.uPVar <$> πs) t
+resolveReft :: F.SourcePos -> Maybe [PVar BSort] -> BareType -> RReft -> RReft
+resolveReft l ps t
+        = txParam l RT.subvUReft (RT.uPVar <$> πs) t
         . fixReftTyVars t       -- same as fixCoercions
   where
     πs  = Mb.fromMaybe tπs ps

From 44dae071d826945943e3fca88f4b068faa26668d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 14:43:53 +0000
Subject: [PATCH 06/16] Make showLHNameDebug the show instance of LHName

---
 .../src/Language/Haskell/Liquid/Bare.hs       |  2 +-
 .../src/Language/Haskell/Liquid/Bare/Axiom.hs |  5 +-
 .../src/Language/Haskell/Liquid/Parse.hs      |  2 +-
 .../Language/Haskell/Liquid/Types/Names.hs    | 64 +++++++++++++------
 tests/basic/neg/AssmRefl02.hs                 |  2 +-
 tests/basic/neg/AssmRefl04.hs                 |  2 +-
 6 files changed, 53 insertions(+), 24 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index a7931b7dcf..652f123484 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -648,7 +648,7 @@ makeSpecRefl src specs env name sig tycEnv = do
   let impAxioms  = concatMap (filter ((`notElem` asmReflEls) . eqName) . Ms.axeqs . snd) (M.toList specs)
   case anyNonReflFn of
     Just (actSym , preSym) ->
-      let preSym' = show (val preSym) in
+      let preSym' = symbolString $ getLHNameSymbol (val preSym) in
       let errorMsg = preSym' ++ " must be reflected first using {-@ reflect " ++ preSym' ++ " @-}"
       in Ex.throw
            (ErrHMeas
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
index 8f0c8b9f34..2f73a3a83d 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
@@ -84,7 +84,10 @@ makeAssumeReflectAxioms src env tycEnv spSig spec = do
   -- Send an error message if we're redefining a reflection
   case findDuplicatePair val reflActSymbols <|> findDuplicateBetweenLists val refSymbols reflActSymbols of
     Just (x , y) -> Ex.throw $ mkError y $
-                      "Duplicate reflection of " ++ show x ++ " and " ++ show y
+                      "Duplicate reflection of " ++
+                      show (lhNameToUnqualifiedSymbol <$> x) ++
+                      " and " ++
+                      show (lhNameToUnqualifiedSymbol <$> y)
     Nothing -> return $ turnIntoAxiom <$> Ms.asmReflectSigs spec
   where
     turnIntoAxiom (actual, pretended) = makeAssumeReflectAxiom spSig env embs (actual, pretended)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index 991e453bad..db920b7565 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -953,7 +953,7 @@ ppAsserts k lxs t mles
 
 pprintSymbolWithParens :: LHName -> PJ.Doc
 pprintSymbolWithParens lhname =
-    case show lhname of
+    case symbolString $ getLHNameSymbol lhname of
       n@(c:_) | not (Char.isAlpha c) -> "(" <> PJ.text n <> ")"
       n -> PJ.text n
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index f6645cf116..c777c8d27b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -30,7 +30,6 @@ module Language.Haskell.Liquid.Types.Names
   , maybeReflectedLHName
   , reflectGHCName
   , reflectLHName
-  , showLHNameDebug
   , updateLHNameSymbol
   ) where
 
@@ -42,11 +41,11 @@ import Data.Hashable
 import Data.String (fromString)
 import qualified Data.Text                               as Text
 import GHC.Generics
+import GHC.Show
 import GHC.Stack
 import Language.Fixpoint.Types
 import Language.Haskell.Liquid.GHC.Misc (locNamedThing) -- Symbolic GHC.Name
 import qualified Liquid.GHC.API as GHC
-import Text.PrettyPrint.HughesPJ.Compat
 
 -- RJ: Please add docs
 lenLocSymbol :: Located Symbol
@@ -145,8 +144,47 @@ instance Ord LogicName where
   compare (GeneratedLogicName s1) (GeneratedLogicName s2) = compare s1 s2
 
 instance Show LHName where
-  show (LHNResolved _ s) = symbolString s
-  show (LHNUnresolved _ s) = symbolString s
+  showsPrec d n0 = showParen (d > app_prec) $ case n0 of
+      LHNResolved n s ->
+        showString "LHNResolved " .
+        showsPrec (app_prec + 1) n .
+        showSpace .
+        showsPrec (app_prec + 1) s
+      LHNUnresolved ns s ->
+        showString "LHNUnresolved " .
+        showsPrec (app_prec + 1) ns .
+        showSpace .
+        showsPrec (app_prec + 1) s
+    where
+      app_prec = 10
+
+instance Show LHResolvedName where
+  showsPrec d n0 = showParen (d > app_prec) $ case n0 of
+      LHRGHC n1 -> showString "LHRGHC " . showString (GHC.showPprDebug n1)
+      LHRLogic n1 -> showString "LHRLogic " . showsPrec (app_prec + 1) n1
+      LHRLocal n1 -> showString "LHRLocal " . showsPrec (app_prec + 1) n1
+      LHRIndex i -> showString "LHRIndex " . showsPrec (app_prec + 1) i
+    where
+      app_prec = 10
+
+instance Show LogicName where
+  showsPrec d n0 = showParen (d > app_prec) $ case n0 of
+      LogicName s1 m mr ->
+        showString "LogicName " .
+        showsPrec (app_prec + 1) s1 .
+        showSpace .
+        showString (GHC.showPprDebug m) .
+        showSpace .
+        showsPrecMaybeName mr
+      GeneratedLogicName s1 ->
+        showString "GeneratedLogicName " .
+        showsPrec (app_prec + 1) s1
+    where
+      app_prec = 10
+
+      showsPrecMaybeName mr = case mr of
+        Nothing -> showString "Nothing"
+        Just n -> showParen True $ showString "Just " . showString (GHC.showPprDebug n)
 
 instance NFData LHName
 instance NFData LHResolvedName
@@ -207,7 +245,7 @@ instance GHC.Binary LogicName where
     GHC.put_ bh (symbolString s)
 
 instance PPrint LHName where
-  pprintTidy _ = text . show
+  pprintTidy _ = pprint . getLHNameSymbol
 
 makeResolvedLHName :: LHResolvedName -> Symbol -> LHName
 makeResolvedLHName = LHNResolved
@@ -254,19 +292,7 @@ getLHNameSymbol (LHNUnresolved _ s) = s
 -- | Get the resolved Symbol from an LHName.
 getLHNameResolved :: HasCallStack => LHName -> LHResolvedName
 getLHNameResolved (LHNResolved n _) = n
-getLHNameResolved n@LHNUnresolved{} = error $ "getLHNameResolved: unresolved name: " ++ showLHNameDebug n
-
-showLHNameDebug :: LHName -> String
-showLHNameDebug (LHNResolved n s) = "LHNResolved (" ++ showLHResolved n ++ ") " ++ show s
-  where
-    showLHResolved (LHRGHC n1) = "LHRGHC " ++ GHC.showPprDebug n1
-    showLHResolved (LHRLogic n1) = "LHRLogic (" ++ showLogicName n1 ++ ")"
-    showLHResolved (LHRLocal n1) = "LHRLocal " ++ show n1
-    showLHResolved (LHRIndex i) = "LHRIndex " ++ show i
-
-    showLogicName (LogicName s1 m mr) = "LogicName " ++ show s1 ++ " " ++ GHC.showPprDebug m ++ " " ++ GHC.showPprDebug mr
-    showLogicName (GeneratedLogicName s1) = "GeneratedLogicName " ++ show s1
-showLHNameDebug (LHNUnresolved ns s) = "LHNUnresolved (" ++ show ns ++ ") " ++ show s
+getLHNameResolved n@LHNUnresolved{} = error $ "getLHNameResolved: unresolved name: " ++ show n
 
 getLHGHCName :: LHName -> Maybe GHC.Name
 getLHGHCName (LHNResolved (LHRGHC n) _) = Just n
@@ -330,7 +356,7 @@ lhNameToUnqualifiedSymbol n = error $ "lhNameToUnqualifiedSymbol: unexpected nam
 -- | Creates a name in the logic namespace for the given Haskell name.
 reflectLHName :: HasCallStack => GHC.Module -> LHName -> LHName
 reflectLHName thisModule (LHNResolved (LHRGHC n) _) = reflectGHCName thisModule n
-reflectLHName _ n = error $ "not a GHC Name: " ++ showLHNameDebug n
+reflectLHName _ n = error $ "not a GHC Name: " ++ show n
 
 -- | Creates a name in the logic namespace for the given Haskell name.
 reflectGHCName :: GHC.Module -> GHC.Name -> LHName
diff --git a/tests/basic/neg/AssmRefl02.hs b/tests/basic/neg/AssmRefl02.hs
index cf37181fd9..072121255a 100644
--- a/tests/basic/neg/AssmRefl02.hs
+++ b/tests/basic/neg/AssmRefl02.hs
@@ -1,5 +1,5 @@
 -- | Duplicate reflection
-{-@ LIQUID "--expect-error-containing=Duplicate reflection of foobar" @-}
+{-@ LIQUID "--expect-error-containing=Duplicate reflection of \"foobar\"" @-}
 {-@ LIQUID "--reflection" @-}
 {-@ LIQUID "--ple"        @-}
 
diff --git a/tests/basic/neg/AssmRefl04.hs b/tests/basic/neg/AssmRefl04.hs
index 16d13fedd1..35603e3417 100644
--- a/tests/basic/neg/AssmRefl04.hs
+++ b/tests/basic/neg/AssmRefl04.hs
@@ -1,5 +1,5 @@
 -- | Duplicate assume reflects
-{-@ LIQUID "--expect-error-containing=Duplicate reflection of alwaysFalse" @-}
+{-@ LIQUID "--expect-error-containing=Duplicate reflection of \"alwaysFalse\"" @-}
 {-@ LIQUID "--reflection" @-}
 {-@ LIQUID "--ple"        @-}
 

From 7c527a8dd006e15f5afa6f532908ed7b26dcf456 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 18:38:53 +0000
Subject: [PATCH 07/16] Resolve ealiases without depending on qualifying passes

---
 .../Haskell/Liquid/LHNameResolution.hs        | 22 +++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index 4ed57786c0..c15d1346ab 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -113,6 +113,19 @@ collectTypeAliases m spec deps =
      in
         HM.fromList $ bsAliases ++ depAliases
 
+collectExprAliases
+  :: BareSpecParsed
+  -> TargetDependencies
+  -> HS.HashSet Symbol
+collectExprAliases spec deps =
+    let bsAliases = HS.fromList $ map (rtName . val) (ealiases spec)
+        depAliases =
+          [ HS.map (rtName . val) $ liftedEaliases lspec
+          | (_, lspec) <- HM.toList (getDependencies deps)
+          ]
+     in
+        HS.unions $ bsAliases : depAliases
+
 -- | Converts occurrences of LHNUnresolved to LHNResolved using the provided
 -- type aliases and GlobalRdrEnv.
 resolveLHNames
@@ -152,6 +165,7 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
                          localVars
                          logicNameEnv0
                          privateReflectNames
+                         allEaliases
                          sp2
               return (sp3, logicNameEnv0)
             else
@@ -163,6 +177,7 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
       Left es
   where
     taliases = collectTypeAliases thisModule bareSpec0 dependencies
+    allEaliases = collectExprAliases bareSpec0 dependencies
 
     resolveFieldLogicName n =
       case n of
@@ -564,9 +579,10 @@ resolveLogicNames
   -> LocalVars
   -> LogicNameEnv
   -> HS.HashSet LocSymbol
+  -> HS.HashSet Symbol
   -> BareSpecParsed
   -> State RenameOutput BareSpecLHName
-resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv privateReflectNames sp = do
+resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv privateReflectNames allEaliases sp = do
     -- Instance measures must be defined for names of class measures.
     -- The names of class measures should be in @env@
     imeasures <- mapM (mapMeasureNamesM resolveIMeasLogicName) (imeasures sp)
@@ -692,7 +708,9 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
           -> case gres of
           [e] -> do
             let n = GHC.greName e
-            if HM.member (symbol n) (lmSymDefs lmap) then
+            -- TODO: The check for allEaliases should be redundant when
+            -- ealiases are put in the logic environments
+            if HM.member (symbol n) (lmSymDefs lmap) || HS.member (symbol n) allEaliases then
               Just $ do
                 let lhName = makeLogicLHName (symbol $ GHC.getOccString n) (GHC.nameModule n) Nothing
                 addName lhName

From f322610b37c3ddc31d6fa71b4f36623995b2df52 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 18:57:23 +0000
Subject: [PATCH 08/16] Remove calls to getLHNameSymbol from Bare.hs

---
 liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index 652f123484..c965fe85c9 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -430,7 +430,7 @@ reflectedVars spec cbs =
   where
     isReflSym x =
       S.member x (Ms.reflects spec) ||
-      S.member (fmap getLHNameSymbol x) (Ms.privateReflects spec)
+      S.member (fmap logicNameToSymbol x) (Ms.privateReflects spec)
 
 measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
 measureVars spec cbs =
@@ -648,7 +648,7 @@ makeSpecRefl src specs env name sig tycEnv = do
   let impAxioms  = concatMap (filter ((`notElem` asmReflEls) . eqName) . Ms.axeqs . snd) (M.toList specs)
   case anyNonReflFn of
     Just (actSym , preSym) ->
-      let preSym' = symbolString $ getLHNameSymbol (val preSym) in
+      let preSym' = symbolString $ lhNameToUnqualifiedSymbol (val preSym) in
       let errorMsg = preSym' ++ " must be reflected first using {-@ reflect " ++ preSym' ++ " @-}"
       in Ex.throw
            (ErrHMeas
@@ -670,7 +670,7 @@ makeSpecRefl src specs env name sig tycEnv = do
     lmap         = Bare.reLMap env
     notInReflOnes (_, a) = not $
       a `S.member` Ms.reflects mySpec ||
-      fmap getLHNameSymbol a `S.member` Ms.privateReflects mySpec
+      fmap logicNameToSymbol a `S.member` Ms.privateReflects mySpec
     anyNonReflFn = L.find notInReflOnes (Ms.asmReflectSigs mySpec)
 
 ------------------------------------------------------------------------------------------
@@ -1094,7 +1094,7 @@ mkReft :: Located LHName -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Exp
 mkReft x z _t tr
   | Just q <- stripRTypeBase tr
   = let Reft (v, p) = toReft q
-        su          = mkSubst [(v, mkEApp (fmap getLHNameSymbol x) [EVar v]), (z,EVar v)]
+        su          = mkSubst [(v, mkEApp (fmap logicNameToSymbol x) [EVar v]), (z,EVar v)]
         -- p'          = pAnd $ filter (\e -> z `notElem` syms e) $ conjuncts p
     in  Just (v, subst su p)
 mkReft _ _ _ _

From 78e96f2a132102d9f2893de45e8586003d09c597 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 19:33:27 +0000
Subject: [PATCH 09/16] Rename logicNameToSymbol to lhNameToResolvedSymbol

---
 .../src/Language/Haskell/Liquid/Bare.hs          | 14 +++++++-------
 .../src/Language/Haskell/Liquid/Bare/Class.hs    |  2 +-
 .../src/Language/Haskell/Liquid/Bare/DataType.hs |  6 +++---
 .../src/Language/Haskell/Liquid/Bare/Measure.hs  |  4 ++--
 .../src/Language/Haskell/Liquid/Bare/Resolve.hs  |  4 ++--
 .../Language/Haskell/Liquid/Bare/Typeclass.hs    |  6 +++---
 .../Language/Haskell/Liquid/LHNameResolution.hs  |  6 +++---
 .../src/Language/Haskell/Liquid/Measure.hs       |  2 +-
 .../Language/Haskell/Liquid/Name/LogicNameEnv.hs |  4 ++--
 .../Haskell/Liquid/Transforms/CoreToLogic.hs     |  2 +-
 .../src/Language/Haskell/Liquid/Types/Names.hs   | 16 ++++++++--------
 .../Language/Haskell/Liquid/Types/PredType.hs    |  2 +-
 .../src/Language/Haskell/Liquid/Types/RType.hs   |  6 +++---
 .../src/Language/Haskell/Liquid/Types/Specs.hs   | 10 +++++-----
 .../Language/Haskell/Liquid/UX/QuasiQuoter.hs    |  2 +-
 15 files changed, 43 insertions(+), 43 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index c965fe85c9..9ae76272dc 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -256,7 +256,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
 
     , _gsLSpec  = finalLiftedSpec
                 { expSigs   =
-                    [ (logicNameToSymbol $ reflectGHCName thisModule $ Ghc.getName v, F.sr_sort $ Bare.varSortedReft embs v)
+                    [ (lhNameToResolvedSymbol $ reflectGHCName thisModule $ Ghc.getName v, F.sr_sort $ Bare.varSortedReft embs v)
                     | v <- gsReflects refl
                     ]
                 , dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec
@@ -430,7 +430,7 @@ reflectedVars spec cbs =
   where
     isReflSym x =
       S.member x (Ms.reflects spec) ||
-      S.member (fmap logicNameToSymbol x) (Ms.privateReflects spec)
+      S.member (fmap lhNameToResolvedSymbol x) (Ms.privateReflects spec)
 
 measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
 measureVars spec cbs =
@@ -670,7 +670,7 @@ makeSpecRefl src specs env name sig tycEnv = do
     lmap         = Bare.reLMap env
     notInReflOnes (_, a) = not $
       a `S.member` Ms.reflects mySpec ||
-      fmap logicNameToSymbol a `S.member` Ms.privateReflects mySpec
+      fmap lhNameToResolvedSymbol a `S.member` Ms.privateReflects mySpec
     anyNonReflFn = L.find notInReflOnes (Ms.asmReflectSigs mySpec)
 
 ------------------------------------------------------------------------------------------
@@ -1094,7 +1094,7 @@ mkReft :: Located LHName -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Exp
 mkReft x z _t tr
   | Just q <- stripRTypeBase tr
   = let Reft (v, p) = toReft q
-        su          = mkSubst [(v, mkEApp (fmap logicNameToSymbol x) [EVar v]), (z,EVar v)]
+        su          = mkSubst [(v, mkEApp (fmap lhNameToResolvedSymbol x) [EVar v]), (z,EVar v)]
         -- p'          = pAnd $ filter (\e -> z `notElem` syms e) $ conjuncts p
     in  Just (v, subst su p)
 mkReft _ _ _ _
@@ -1202,14 +1202,14 @@ makeMeasEnv env tycEnv sigEnv specs = do
   let (cs, ms) = Bare.makeMeasureSpec'  (typeclass $ getConfig env)   measures
   let cms      = Bare.makeClassMeasureSpec measures
   let cms'     = [ (val l, cSort t <$ l)  | (l, t) <- cms ]
-  let ms'      = [ (logicNameToSymbol (F.val lx), F.atLoc lx t)
+  let ms'      = [ (lhNameToResolvedSymbol (F.val lx), F.atLoc lx t)
                  | (lx, t) <- ms
                  , Mb.isNothing (lookup (val lx) cms')
                  ]
   let cs'      = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec (typeclass (getConfig env)) embs cs (datacons ++ cls)]
   return Bare.MeasEnv
     { meMeasureSpec = measures
-    , meClassSyms   = map (first logicNameToSymbol) cms'
+    , meClassSyms   = map (first lhNameToResolvedSymbol) cms'
     , meSyms        = ms'
     , meDataCons    = cs'
     , meClasses     = cls
@@ -1250,7 +1250,7 @@ addOpaqueReflMeas cfg tycEnv env spec measEnv specs eqs = do
   -- `meSyms` (no class, data constructor or other stuff here).
   let measures = mconcat (Ms.mkMSpec' dcSelectors : measures0)
   let (cs, ms) = Bare.makeMeasureSpec'  (typeclass $ getConfig env)   measures
-  let ms'      = [ (logicNameToSymbol (F.val lx), F.atLoc lx t) | (lx, t) <- ms ]
+  let ms'      = [ (lhNameToResolvedSymbol (F.val lx), F.atLoc lx t) | (lx, t) <- ms ]
   let cs'      = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec (typeclass (getConfig env)) embs cs (val <$> datacons)]
   return $ measEnv <> mempty
     { Bare.meMeasureSpec = measures
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs
index ec3f2598d9..093934871b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs
@@ -63,7 +63,7 @@ makeMethodTypes allowTC (DEnv hm) cls cbs
         case filter ((==d) . Ghc.dataConWorkId . dcpCon) cls of
           (di:_) ->
             (dcpLoc di `F.atLoc`) . subst (zip (dcpFreeTyVars di) ts) <$>
-            L.lookup (mkSymbol x) (map (first logicNameToSymbol) $ dcpTyArgs di)
+            L.lookup (mkSymbol x) (map (first lhNameToResolvedSymbol) $ dcpTyArgs di)
           _      -> Nothing
 
       methodType d x m = ihastype (M.lookup d m) x
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
index 16d23c8362..a3ee66a4cf 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
@@ -346,7 +346,7 @@ makeDataCtor tce c (d, dp) = F.DCtor
   }
   where
     as          = dcpFreeTyVars dp
-    xts         = [ (fld $ logicNameToSymbol x, t) | (x, t) <- reverse (dcpTyArgs dp) ]
+    xts         = [ (fld $ lhNameToResolvedSymbol x, t) | (x, t) <- reverse (dcpTyArgs dp) ]
     fld         = F.atLoc dp . fieldName d dp
 
 fieldName :: Ghc.DataCon -> DataConP -> F.Symbol -> F.Symbol
@@ -800,10 +800,10 @@ makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne
              | (x, t) <- reverse args -- NOTE: the reverse here is correct
              , let vv = rTypeValueVar t
                -- the measure singleton refinement, eg `v = getBar foo`
-             , let mt = RT.uReft (vv, F.PAtom F.Eq (F.EVar vv) (F.EApp (F.EVar $ logicNameToSymbol x) (F.EVar z)))
+             , let mt = RT.uReft (vv, F.PAtom F.Eq (F.EVar vv) (F.EApp (F.EVar $ lhNameToResolvedSymbol x) (F.EVar z)))
              ]
 
-      su   = F.mkSubst [ (lhNameToUnqualifiedSymbol x, F.EApp (F.EVar (logicNameToSymbol x)) (F.EVar z)) | x <- fst <$> args ]
+      su   = F.mkSubst [ (lhNameToUnqualifiedSymbol x, F.EApp (F.EVar (lhNameToResolvedSymbol x)) (F.EVar z)) | x <- fst <$> args ]
       args = dcpTyArgs dcp
       z    = "lq$recSel"
       res  = dropPreds (dcpTyRes dcp)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index f106de4ceb..ef65dce9c7 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
@@ -104,7 +104,7 @@ makeUnSorted allowTC ty defs
 
     defToUnSortedExpr defn =
       (xx:(fst <$> binds defn),
-       Ms.bodyPred (F.eApps (F.EVar $ logicNameToSymbol $ F.val $ measure defn) [F.expr xx]) (body defn))
+       Ms.bodyPred (F.eApps (F.EVar $ lhNameToResolvedSymbol $ F.val $ measure defn) [F.expr xx]) (body defn))
 
     xx = F.vv $ Just 10000
     isErasable = if allowTC then GM.isEmbeddedDictType else Ghc.isClassPred
@@ -404,7 +404,7 @@ getDefinedSymbolsInLogic env measEnv specs =
       getFromDataCtor <$>
         concat (tycDCons `Mb.mapMaybe` (dataDecls spec ++ newtyDecls spec))
     getFromDataCtor decl = S.fromList $
-      map (dummyLoc . logicNameToSymbol) $ val (dcName decl) : (fst <$> dcFields decl)
+      map (dummyLoc . lhNameToResolvedSymbol) $ val (dcName decl) : (fst <$> dcFields decl)
     getAliases spec = S.fromList $ fmap rtName <$> Ms.ealiases spec
     localize :: F.Symbol -> F.LocSymbol
     localize sym = maybe (dummyLoc sym) varLocSym $ L.lookup sym (Bare.reSyms env)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
index 675e60d659..698c45ccd5 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
@@ -136,7 +136,7 @@ getGlobalSyms (_, spec)
       ++ (mbName <$> imeasures spec)
       ++ (mbName <$> omeasures spec)
   where
-    mbName = logicNameToSymbol . F.val . msName
+    mbName = lhNameToResolvedSymbol . F.val . msName
 
 makeLocalVars :: [Ghc.CoreBind] -> LocalVars
 makeLocalVars = localVarMap . localBinds
@@ -950,7 +950,7 @@ lookupTyThingMaybe env lc@(Loc _ _ c0) = unsafePerformIO $ do
       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 _ -> panic (Just $ GM.fSrcSpan lc) $ "lookupTyThing: cannot resolve a LHRLogic name " ++ show (logicNameToSymbol c0)
+        LHRLogic _ -> panic (Just $ GM.fSrcSpan lc) $ "lookupTyThing: cannot resolve a LHRLogic name " ++ show (lhNameToResolvedSymbol c0)
         LHRGHC n ->
           Ghc.reflectGhc (Interface.lookupTyThing (gtleTypeEnv env) n) (gtleSession env)
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs
index 01e5c53e30..fddb54356b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs
@@ -189,10 +189,10 @@ elaborateClassDcp
 elaborateClassDcp coreToLg simplifier dcp = do
   t' <- flip (zipWith addCoherenceOblig) prefts
     <$> forM fts (elaborateSpecType coreToLg simplifier)
-  let ts' = elaborateMethod (F.symbol dc) (S.fromList $ map logicNameToSymbol xs) <$> t'
+  let ts' = elaborateMethod (F.symbol dc) (S.fromList $ map lhNameToResolvedSymbol xs) <$> t'
   pure
     ( dcp { dcpTyArgs = zip xs (stripPred <$> ts') }
-    , dcp { dcpTyArgs = fmap (\(x, t) -> (x, strengthenTy (logicNameToSymbol x) t)) (zip xs t') }
+    , dcp { dcpTyArgs = fmap (\(x, t) -> (x, strengthenTy (lhNameToResolvedSymbol x) t)) (zip xs t') }
     )
  where
   addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType
@@ -393,7 +393,7 @@ makeClassAuxTypesOne elab (ldcp, inst, methods) =
     -- Monoid.mappend, ...
     clsMethods = filter (\x -> GM.dropModuleNames (F.symbol x) `elem` fmap mkSymbol methods) $
       Ghc.classAllSelIds (Ghc.is_cls inst)
-    yts = [(logicNameToSymbol y, t) | (y, t) <- dcpTyArgs dcp]
+    yts = [(lhNameToResolvedSymbol y, t) | (y, t) <- dcpTyArgs dcp]
     mkSymbol x
       | -- F.notracepp ("isDictonaryId:" ++ GM.showPpr x) $
         Ghc.isDictonaryId x = F.mappendSym "$" (F.dropSym 2 $ GM.simplesymbol x)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index c15d1346ab..2aa457b9c9 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -546,7 +546,7 @@ makeLogicEnvs impAvails thisModule spec dependencies =
 
     mkLogicNameEnv names =
       LogicNameEnv
-        { lneLHName = fromListSEnv [ (logicNameToSymbol n, n) | n <- names ]
+        { lneLHName = fromListSEnv [ (lhNameToResolvedSymbol n, n) | n <- names ]
         , lneReflected = GHC.mkNameEnv [(rn, n) | n <- names, Just rn <- [maybeReflectedLHName n]]
         }
 
@@ -625,7 +625,7 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
               ErrDupNames
                 (LH.fSrcSpan ls)
                 (pprint s)
-                [ pprint (logicNameToSymbol n) PJ.<+>
+                [ pprint (lhNameToResolvedSymbol n) PJ.<+>
                   PJ.text
                     ("imported from " ++ GHC.moduleNameString (GHC.moduleName m))
                 | (m, n) <- names
@@ -635,7 +635,7 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
         s = val ls
         wiredInNames =
            map fst wiredSortedSyms ++
-           map (logicNameToSymbol . fst) (concatMap (DataDecl.dcpTyArgs . val) wiredDataCons)
+           map (lhNameToResolvedSymbol . fst) (concatMap (DataDecl.dcpTyArgs . val) wiredDataCons)
 
     errResolveLogicName s alts =
       ErrResolve
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Measure.hs
index 2573a576a4..b7f74ba29d 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Measure.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Measure.hs
@@ -248,7 +248,7 @@ refineWithCtorBody dc f body t =
   case stripRTypeBase t of
     Just (Reft (v, _)) ->
       strengthen t $
-        Reft (v, bodyPred (eApps (EVar $ logicNameToSymbol $ val f) [eVar v]) body)
+        Reft (v, bodyPred (eApps (EVar $ lhNameToResolvedSymbol $ val f) [eVar v]) body)
     Nothing ->
       panic Nothing $ "measure mismatch " ++ showpp f ++ " on con " ++ showPpr dc
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs
index 6ec511133a..45320be4a3 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs
@@ -10,7 +10,7 @@ import           Language.Haskell.Liquid.Types.Names
 
 -- | For every symbol tells the corresponding LHName and Sort
 --
--- Symbols are expected to have been created by 'logicNameToSymbol'.
+-- Symbols are expected to have been created by 'lhNameToResolvedSymbol'.
 --
 data LogicNameEnv = LogicNameEnv
        { lneLHName :: SEnv LHName
@@ -22,5 +22,5 @@ extendLogicNameEnv :: LogicNameEnv -> [LHName] -> LogicNameEnv
 extendLogicNameEnv env ns =
     env
       { lneLHName =
-          foldr (uncurry insertSEnv) (lneLHName env) [ (logicNameToSymbol n, n) | n <- ns]
+          foldr (uncurry insertSEnv) (lneLHName env) [ (lhNameToResolvedSymbol n, n) | n <- ns]
       }
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
index 8bae734390..ca7703bf57 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
@@ -207,7 +207,7 @@ toArgs f args = [(symbol x, f $ varRType x) | x <- args]
 defArgs :: Monoid r => Located LHName -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
 defArgs x     = zipWith (\i t -> (defArg i, defRTyp t)) [0..]
   where
-    defArg    = tempSymbol (logicNameToSymbol $ val x)
+    defArg    = tempSymbol (lhNameToResolvedSymbol $ val x)
     defRTyp   = Just . F.atLoc x . ofType
 
 coreToDef :: Reftable r => Bool -> Located LHName -> Var -> C.CoreExpr
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index c777c8d27b..79cec5d6ab 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -15,7 +15,7 @@ module Language.Haskell.Liquid.Types.Names
   , getLHGHCName
   , getLHNameResolved
   , getLHNameSymbol
-  , logicNameToSymbol
+  , lhNameToResolvedSymbol
   , lhNameToUnqualifiedSymbol
   , makeGHCLHName
   , makeGHCLHNameFromId
@@ -314,13 +314,13 @@ updateLHNameSymbol :: (Symbol -> Symbol) -> LHName -> LHName
 updateLHNameSymbol f (LHNResolved n s) = LHNResolved n (f s)
 updateLHNameSymbol f (LHNUnresolved n s) = LHNUnresolved n (f s)
 
--- | Converts logic names to symbols.
+-- | Converts resolved names to symbols.
 --
 -- One important postcondition of this function is that the symbol for reflected
 -- names must match exactly the symbol for the corresponding Haskell function.
 -- Otherwise, LH would fail to link the two at various places where it is needed.
-logicNameToSymbol :: LHName -> Symbol
-logicNameToSymbol (LHNResolved (LHRLogic (LogicName s om mReflectionOf)) _) =
+lhNameToResolvedSymbol :: LHName -> Symbol
+lhNameToResolvedSymbol (LHNResolved (LHRLogic (LogicName s om mReflectionOf)) _) =
     let m = maybe om GHC.nameModule mReflectionOf
         msymbol = Text.pack $ GHC.moduleNameString $ GHC.moduleName m
      in symbol $ mconcat [msymbol, ".", symbolText s]
@@ -341,10 +341,10 @@ logicNameToSymbol (LHNResolved (LHRLogic (LogicName s om mReflectionOf)) _) =
           GHC.moduleUnitId m
      in symbol $ mconcat ["u", munique, "##", msymbol, ".", symbolText s]
           -}
-logicNameToSymbol (LHNResolved (LHRLogic (GeneratedLogicName s)) _) = s
-logicNameToSymbol (LHNResolved (LHRLocal s) _) = s
-logicNameToSymbol (LHNResolved (LHRGHC n) _) = symbol $ GHC.getOccString n
-logicNameToSymbol n = error $ "logicNameToSymbol: unexpected name: " ++ show n
+lhNameToResolvedSymbol (LHNResolved (LHRLogic (GeneratedLogicName s)) _) = s
+lhNameToResolvedSymbol (LHNResolved (LHRLocal s) _) = s
+lhNameToResolvedSymbol (LHNResolved (LHRGHC n) _) = symbol $ GHC.getOccString n
+lhNameToResolvedSymbol n = error $ "lhNameToResolvedSymbol: unexpected name: " ++ show n
 
 lhNameToUnqualifiedSymbol :: HasCallStack => LHName -> Symbol
 lhNameToUnqualifiedSymbol (LHNResolved (LHRLogic (LogicName s _ _)) _) = s
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs
index 9b22aeeb33..7bfd99f0bd 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs
@@ -185,7 +185,7 @@ dcWrapSpecType allowTC dc (DataConP _ _ vs ps cs yts rt _ _ _)
   where
     isCls    = Ghc.isClassTyCon $ Ghc.dataConTyCon dc
     (as0, sts) = unzip (reverse yts)
-    as = map logicNameToSymbol as0
+    as = map lhNameToResolvedSymbol as0
     as1 = map lhNameToUnqualifiedSymbol as0
     mkDSym z = F.symbol z `F.suffixSymbol` F.symbol dc
     bs       = mkDSym <$> as
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs
index ad4696e14a..9f65866a13 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs
@@ -607,7 +607,7 @@ instance TyConable BTyCon where
       LHRGHC n -> text $ showPpr n
       LHRLocal s -> ppTycon s
       LHRIndex i -> text $ "(Unknown LHRIndex " ++ show i ++ ")"
-      LHRLogic _ -> ppTycon $ logicNameToSymbol $ F.val $ btc_tc b
+      LHRLogic _ -> ppTycon $ lhNameToResolvedSymbol $ F.val $ btc_tc b
 
 instance Eq RTyCon where
   x == y = rtc_tc x == rtc_tc y
@@ -628,7 +628,7 @@ instance F.Fixpoint BTyCon where
       LHRGHC n -> text $ F.symbolString $ F.symbol n
       LHRLocal s -> text $ F.symbolString s
       LHRIndex i -> panic (Just $ fSrcSpan b) $ "toFix BTyCon: Unknown LHRIndex " ++ show i
-      LHRLogic _ -> text $ F.symbolString $ logicNameToSymbol $ F.val $ btc_tc b
+      LHRLogic _ -> text $ F.symbolString $ lhNameToResolvedSymbol $ F.val $ btc_tc b
 
 instance F.PPrint RTyCon where
   pprintTidy k c
@@ -645,7 +645,7 @@ instance F.PPrint BTyCon where
       LHRGHC n -> text $ F.symbolString $ F.symbol n
       LHRLocal s -> text $ F.symbolString s
       LHRIndex i -> text $ "(Unknown LHRIndex " ++ show i ++ ")"
-      LHRLogic _ -> text $ F.symbolString $ logicNameToSymbol $ F.val $ btc_tc b
+      LHRLogic _ -> text $ F.symbolString $ lhNameToResolvedSymbol $ F.val $ btc_tc b
 
 instance F.PPrint v => F.PPrint (RTVar v s) where
   pprintTidy k (RTVar x _) = F.pprintTidy k x
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index c58df276d9..6007c3427f 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -765,10 +765,10 @@ instance Show LiftedSpec where
 fromBareSpecLHName :: BareSpecLHName -> BareSpec
 fromBareSpecLHName sp =
     mapSpecTy
-      ( mapRTypeV logicNameToSymbol .
-        mapReft (mapUReftV logicNameToSymbol (fmap logicNameToSymbol))
+      ( mapRTypeV lhNameToResolvedSymbol .
+        mapReft (mapUReftV lhNameToResolvedSymbol (fmap lhNameToResolvedSymbol))
       ) $
-    mapSpecLName logicNameToSymbol sp
+    mapSpecLName lhNameToResolvedSymbol sp
 
 fromBareSpecParsed :: BareSpecParsed -> BareSpec
 fromBareSpecParsed sp =
@@ -946,7 +946,7 @@ toLiftedSpec :: BareSpecLHName -> LiftedSpec
 toLiftedSpec a = LiftedSpec
   { liftedMeasures   =
       M.fromList
-        [ (dropModuleNames $ logicNameToSymbol n, m)
+        [ (dropModuleNames $ lhNameToResolvedSymbol n, m)
         | m <- measures a
         , let n = val $ msName m
         ]
@@ -967,7 +967,7 @@ toLiftedSpec a = LiftedSpec
   , liftedAutosize   = autosize a
   , liftedCmeasures  =
       M.fromList
-        [ (dropModuleNames $ logicNameToSymbol n, m)
+        [ (dropModuleNames $ lhNameToResolvedSymbol n, m)
         | m <- cmeasures a
         , let n = val $ msName m
         ]
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs
index b991a3676f..b5f73438e5 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs
@@ -119,7 +119,7 @@ lhNameToName lname = case val lname of
       LHRLocal s -> symbolName s
       LHRIndex i -> panic (Just $ fSrcSpan lname) $ "Cannot produce a TH Name for a LHRIndex " ++ show i
       LHRLogic _ ->
-        panic (Just $ fSrcSpan lname) $ "Cannot produce a TH Name for a LogicName: " ++ show (logicNameToSymbol $ val lname)
+        panic (Just $ fSrcSpan lname) $ "Cannot produce a TH Name for a LogicName: " ++ show (lhNameToResolvedSymbol $ val lname)
 
   where
     toTHNameSpace :: GHC.NameSpace -> NameSpace

From dcac9991025ce61892ebdd861c5861c2c9ed9f57 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 19:36:09 +0000
Subject: [PATCH 10/16] Please hlint

---
 .../src/Language/Haskell/Liquid/LHNameResolution.hs           | 4 ++--
 liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs     | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index 2aa457b9c9..96bec9bdfc 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -659,8 +659,8 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
            in return $ makeLogicLHName s (GHC.nameModule dcName) (Just dcName)
       where
         unqualifiedS = LH.dropModuleNames s
-        nilDataConName = GHC.getName $ GHC.dataConWorkId $ GHC.nilDataCon
-        consDataConName = GHC.getName $ GHC.dataConWorkId $ GHC.consDataCon
+        nilDataConName = GHC.getName $ GHC.dataConWorkId GHC.nilDataCon
+        consDataConName = GHC.getName $ GHC.dataConWorkId GHC.consDataCon
         tupleDataConName = GHC.getName . GHC.dataConWorkId . GHC.tupleDataCon GHC.Boxed
         s = val ls
         isTupleDC t
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
index 9c3834ee84..5089ddbf90 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
@@ -189,7 +189,7 @@ listTyDataCons   = ( [TyConP l0 c [RTV tyv] [p] [Covariant] [Covariant] (Just fs
       lt         = rApp c [xt] [rPropP [] $ pdVarReft p] mempty
       xt         = rVar tyv
       xst        = rApp c [RVar (RTV tyv) px] [rPropP [] $ pdVarReft p] mempty
-      cargs      = map (first makeGeneratedLogicLHName) $ [(xTail, xst), (xHead, xt)]
+      cargs      = map (first makeGeneratedLogicLHName) [(xTail, xst), (xHead, xt)]
       fsize      = SymSizeFun (dummyLoc "GHC.Types_LHAssumptions.len")
 
 wiredInName :: F.Symbol

From fbe957bcb046cbdb3ab5fa0b7dda7bf5a11b9abf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Fri, 13 Dec 2024 10:56:01 +0000
Subject: [PATCH 11/16] Fix lhNameToResolvedSymbol in the LHRGHC case

---
 liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index 79cec5d6ab..7747477c41 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -343,7 +343,7 @@ lhNameToResolvedSymbol (LHNResolved (LHRLogic (LogicName s om mReflectionOf)) _)
           -}
 lhNameToResolvedSymbol (LHNResolved (LHRLogic (GeneratedLogicName s)) _) = s
 lhNameToResolvedSymbol (LHNResolved (LHRLocal s) _) = s
-lhNameToResolvedSymbol (LHNResolved (LHRGHC n) _) = symbol $ GHC.getOccString n
+lhNameToResolvedSymbol (LHNResolved (LHRGHC n) _) = symbol n
 lhNameToResolvedSymbol n = error $ "lhNameToResolvedSymbol: unexpected name: " ++ show n
 
 lhNameToUnqualifiedSymbol :: HasCallStack => LHName -> Symbol

From 1c09c08023d0ab749bc24f1a9a37b65481d292bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 12 Dec 2024 13:57:51 +0000
Subject: [PATCH 12/16] Remove qualifyTop calls

---
 .../src/Language/Haskell/Liquid/Bare.hs       | 36 ++++++++-----------
 .../src/Language/Haskell/Liquid/Bare/Axiom.hs | 13 ++++---
 .../Language/Haskell/Liquid/Bare/Expand.hs    |  5 ---
 .../Language/Haskell/Liquid/Bare/Measure.hs   | 24 ++++++-------
 .../Language/Haskell/Liquid/Bare/Resolve.hs   | 13 -------
 5 files changed, 32 insertions(+), 59 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index 9ae76272dc..374d906968 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -491,8 +491,7 @@ makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual
 
 makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec F.Symbol ty) -> [F.Qualifier]
 makeQualifiers env tycEnv (modn, spec)
-  = fmap        (Bare.qualifyTopDummy env        modn)
-  . Mb.mapMaybe (resolveQParams       env tycEnv modn)
+  = Mb.mapMaybe (resolveQParams       env tycEnv modn)
   $ Ms.qualifiers spec
 
 
@@ -633,16 +632,12 @@ makeSpecRefl src specs env name sig tycEnv = do
   autoInst <- makeAutoInst env mySpec
   rwr      <- makeRewrite env mySpec
   rwrWith  <- makeRewriteWith env mySpec
-  xtes     <- Bare.makeHaskellAxioms src env tycEnv name lmap sig mySpec
+  xtes     <- Bare.makeHaskellAxioms src env tycEnv lmap sig mySpec
   asmReflAxioms <- Bare.makeAssumeReflectAxioms src env tycEnv sig mySpec
   let otherAxioms = thd3 <$> asmReflAxioms
   let myAxioms =
-        [ Bare.qualifyTop
-            env
-            name
-            (F.loc lt)
-            e {eqRec = S.member (eqName e) (exprSymbolsSet (eqBody e))}
-        | (_, lt, e) <- xtes
+        [ e {eqRec = S.member (eqName e) (exprSymbolsSet (eqBody e))}
+        | (_, _, e) <- xtes
         ] ++ otherAxioms
   let asmReflEls = eqName <$> otherAxioms
   let impAxioms  = concatMap (filter ((`notElem` asmReflEls) . eqName) . Ms.axeqs . snd) (M.toList specs)
@@ -1004,7 +999,7 @@ makeSpecData src env sigEnv measEnv sig specs = SpData
                        , let tt  = Bare.plugHoles (typeclass $ getConfig env) sigEnv name (Bare.LqTV x) t
                    ]
   , gsMeas       = [ (F.symbol x, uRType <$> t) | (x, t) <- measVars ]
-  , gsMeasures   = Bare.qualifyTopDummy env name <$> (ms1 ++ ms2)
+  , gsMeasures   = (ms1 ++ ms2)
   , gsOpaqueRefls = fst <$> Bare.meOpaqueRefl measEnv
   , gsInvariants = Misc.nubHashOn (F.loc . snd) invs
   , gsIaliases   = concatMap (makeIAliases env sigEnv) (M.toList specs)
@@ -1018,7 +1013,7 @@ makeSpecData src env sigEnv measEnv sig specs = SpData
     ms2          = Ms.imeas   measuresSp
     mySpec       = M.lookupDefault mempty name specs
     name         = _giTargetMod      src
-    (minvs,usI)  = makeMeasureInvariants env name sig mySpec
+    (minvs,usI)  = makeMeasureInvariants sig mySpec
     invs         = minvs ++ concatMap (makeInvariants env sigEnv) (M.toList specs)
 
 makeIAliases :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(LocSpecType, LocSpecType)]
@@ -1050,19 +1045,18 @@ makeSizeInv s lst = lst{val = go (val lst)}
         nat  = MkUReft (Reft (vv_, PAtom Le (ECon $ I 0) (EApp (EVar s) (eVar vv_))))
                        mempty
 
-makeMeasureInvariants :: Bare.Env -> ModName -> GhcSpecSig -> Ms.BareSpec
-                      -> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
-makeMeasureInvariants env name sig mySpec
+makeMeasureInvariants :: GhcSpecSig -> Ms.BareSpec -> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
+makeMeasureInvariants sig mySpec
   = Mb.catMaybes <$>
-    unzip (measureTypeToInv env name <$> [(x, (y, ty)) | x <- xs, (y, ty) <- sigs
+    unzip (measureTypeToInv <$> [(x, (y, ty)) | x <- xs, (y, ty) <- sigs
                                          , x == makeGHCLHNameLocatedFromId y ])
   where
     sigs = gsTySigs sig
     xs   = S.toList (Ms.hmeas  mySpec)
 
-measureTypeToInv :: Bare.Env -> ModName -> (Located LHName, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr)
-measureTypeToInv env name (x, (v, t))
-  = notracepp "measureTypeToInv" ((Just v, t {val = Bare.qualifyTop env name (F.loc x) mtype}), usorted)
+measureTypeToInv :: (Located LHName, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr)
+measureTypeToInv (x, (v, t))
+  = notracepp "measureTypeToInv" ((Just v, t {val = mtype}), usorted)
   where
     trep = toRTypeRep (val t)
     rts  = ty_args  trep
@@ -1105,10 +1099,10 @@ mkReft _ _ _ _
 -------------------------------------------------------------------------------------------
 makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> ModName -> GhcSpecNames
 -------------------------------------------------------------------------------------------
-makeSpecName env tycEnv measEnv name = SpNames
+makeSpecName env tycEnv measEnv _name = SpNames
   { gsFreeSyms = Bare.reSyms env
   , gsDconsP   = [ F.atLoc dc (dcpCon dc) | dc <- datacons ++ cls ]
-  , gsTconsP   = Bare.qualifyTopDummy env name <$> tycons
+  , gsTconsP   = tycons
   -- , gsLits = mempty                                              -- TODO-REBARE, redundant with gsMeas
   , gsTcEmbeds = Bare.tcEmbs     tycEnv
   , gsADTs     = Bare.tcAdts     tycEnv
@@ -1146,7 +1140,7 @@ makeTycEnv0 cfg myName env embs mySpec iSpecs = (diag0 <> diag1, datacons, Bare.
     (diag0, conTys) = withDiagnostics $ Bare.makeConTypes myName env specs
     specs         = (myName, mySpec) : M.toList iSpecs
     tcs           = Misc.snd3 <$> tcDds
-    tyi           = Bare.qualifyTopDummy env myName (makeTyConInfo embs fiTcs tycons)
+    tyi           = makeTyConInfo embs fiTcs tycons
     -- tycons        = F.tracepp "TYCONS" $ Misc.replaceWith tcpCon tcs wiredTyCons
     -- datacons      =  Bare.makePluggedDataCons embs tyi (Misc.replaceWith (dcpCon . val) (F.tracepp "DATACONS" $ concat dcs) wiredDataCons)
     tycons        = tcs ++ knownWiredTyCons env myName
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
index 2f73a3a83d..bd46e9fbe3 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
@@ -62,12 +62,12 @@ findDuplicateBetweenLists key l1 l2 =
       [ (x, y) | x <- l2', Just y <- [Map.lookup (key' x) seen]]
 
 -----------------------------------------------------------------------------------------------
-makeHaskellAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec
+makeHaskellAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> LogicMap -> GhcSpecSig -> Ms.BareSpec
                   -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]
 -----------------------------------------------------------------------------------------------
-makeHaskellAxioms src env tycEnv name lmap spSig spec = do
+makeHaskellAxioms src env tycEnv lmap spSig spec = do
   let refDefs = getReflectDefs src spSig spec env
-  return (makeAxiom env tycEnv name lmap <$> refDefs)
+  return (makeAxiom env tycEnv lmap <$> refDefs)
 
 -----------------------------------------------------------------------------------------------
 --          Returns a list of elements, one per assume reflect                               --
@@ -309,15 +309,14 @@ getExprFromUnfolding (Ghc.CoreUnfolding expr _ _ _ _) = Just expr
 getExprFromUnfolding _ = Nothing
 
 --------------------------------------------------------------------------------
-makeAxiom :: Bare.Env -> Bare.TycEnv -> ModName -> LogicMap
+makeAxiom :: Bare.Env -> Bare.TycEnv -> LogicMap
           -> (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)
           -> (Ghc.Var, LocSpecType, F.Equation)
 --------------------------------------------------------------------------------
-makeAxiom env tycEnv name lmap (x, mbT, v, def)
+makeAxiom env tycEnv lmap (x, mbT, v, def)
             = (v, t, e)
   where
-    t       = Bare.qualifyTop env name (F.loc t0) t0
-    (t0, e) = makeAssumeType allowTC embs lmap dm x mbT v def
+    (t, e) = makeAssumeType allowTC embs lmap dm x mbT v def
     embs    = Bare.tcEmbs       tycEnv
     dm      = Bare.tcDataConMap tycEnv
     allowTC = typeclass (getConfig env)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
index 372f283d9e..ba01a207a1 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -491,10 +491,6 @@ cookSpecTypeE env sigEnv name@(ModName _ _) x bt
         . fmap txExpToBind -- What does this function DO
         . (specExpandType rtEnv . fmap (generalizeWith x))
         . (if doplug || not allowTC then maybePlug allowTC sigEnv name x else id)
-        -- we do not qualify/resolve Expr/Pred when typeclass is enabled
-        -- since ghci will not be able to recognize fully qualified names
-        -- instead, we leave qualification to ghc elaboration
-        . Bare.qualifyTop env name l
 
     allowTC = typeclass (getConfig env)
     -- modT   = mname `S.member` wiredInMods
@@ -509,7 +505,6 @@ cookSpecTypeE env sigEnv name@(ModName _ _) x bt
     rtEnv  = Bare.sigRTEnv    sigEnv
     embs   = Bare.sigEmbs     sigEnv
     tyi    = Bare.sigTyRTyMap sigEnv
-    l      = F.loc bt
 
 -- | We don't want to generalize type variables that maybe bound in the
 --   outer scope, e.g. see tests/basic/pos/LocalPlug00.hs
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index ef65dce9c7..4cdf7aca6b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
@@ -12,7 +12,6 @@ module Language.Haskell.Liquid.Bare.Measure
   , makeMeasureSelectors
   , makeMeasureSpec
   , makeMeasureSpec'
-  , getLocReflects
   , makeOpaqueReflMeasures
   , getReflDCs
   , varMeasures
@@ -372,18 +371,17 @@ makeMeasureSpec env sigEnv myName (name, spec)
 
 --- Returns all the reflected symbols.
 --- If Env is provided, the symbols are qualified using the environment.
-getLocReflects :: Maybe Bare.Env -> Bare.ModSpecs -> S.HashSet F.LocSymbol
-getLocReflects mbEnv = S.unions . fmap (uncurry $ names mbEnv) . M.toList
+getLocReflects :: Bare.ModSpecs -> S.HashSet F.LocSymbol
+getLocReflects = S.unions . map names . M.elems
   where
-    names (Just env) modName modSpec = Bare.qualifyLocSymbolTop env modName `S.map` unqualified modSpec
-    names Nothing _ modSpec = unqualified modSpec
+    names modSpec = unqualified modSpec
     unqualified modSpec = S.unions
-      [ S.map (fmap getLHNameSymbol) (Ms.reflects modSpec)
+      [ S.map (fmap lhNameToResolvedSymbol) (Ms.reflects modSpec)
       , Ms.privateReflects modSpec
-      , S.fromList (fmap getLHNameSymbol . snd <$> Ms.asmReflectSigs modSpec)
-      , S.fromList (fmap getLHNameSymbol . fst <$> Ms.asmReflectSigs modSpec)
-      , S.map (fmap getLHNameSymbol) (Ms.inlines modSpec)
-      , S.map (fmap getLHNameSymbol) (Ms.hmeas modSpec)
+      , S.fromList (fmap lhNameToResolvedSymbol . snd <$> Ms.asmReflectSigs modSpec)
+      , S.fromList (fmap lhNameToResolvedSymbol . fst <$> Ms.asmReflectSigs modSpec)
+      , S.map (fmap lhNameToResolvedSymbol) (Ms.inlines modSpec)
+      , S.map (fmap lhNameToResolvedSymbol) (Ms.hmeas modSpec)
       ]
 
 -- Get all the symbols that are defined in the logic, based on the environment and the specs.
@@ -391,14 +389,14 @@ getLocReflects mbEnv = S.unions . fmap (uncurry $ names mbEnv) . M.toList
 getDefinedSymbolsInLogic :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs -> S.HashSet F.LocSymbol
 getDefinedSymbolsInLogic env measEnv specs = 
   S.unions (uncurry getFromAxioms <$> specsList) -- reflections that ended up in equations
-    `S.union` getLocReflects (Just env) specs -- reflected symbols
+    `S.union` getLocReflects specs -- reflected symbols
     `S.union` measVars -- Get the data constructors, ex. for Lit00.0
     `S.union` S.unions (getDataDecls . snd <$> specsList) -- get the Predicated type defs, ex. for T1669.CSemigroup
     `S.union` S.unions (getAliases . snd <$> specsList) -- aliases, ex. for T1738Lib.incr
   where
     specsList = M.toList specs
-    getFromAxioms modName spec = S.fromList $
-      Bare.qualifyLocSymbolTop env modName . localize . F.eqName <$> Ms.axeqs spec
+    getFromAxioms _modName spec = S.fromList $
+      localize . F.eqName <$> Ms.axeqs spec
     measVars     = S.fromList $ localize . fst <$> getMeasVars env measEnv
     getDataDecls spec = S.unions $
       getFromDataCtor <$>
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
index 698c45ccd5..b09257eb4a 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
@@ -22,7 +22,6 @@ module Language.Haskell.Liquid.Bare.Resolve
   , ResolveSym (..)
   , Qualify (..)
   , Lookup
-  , qualifyTop, qualifyTopDummy, qualifyLocSymbolTop
 
   -- * Looking up names
   , maybeResolveSym
@@ -315,14 +314,6 @@ dataConVars dcs = (Ghc.dataConWorkId <$> dcs) ++ (Ghc.dataConWrapId <$> dcs)
 -------------------------------------------------------------------------------
 -- | Qualify various names
 -------------------------------------------------------------------------------
-qualifyTop :: (Qualify a) => Env -> ModName -> F.SourcePos -> a -> a
-qualifyTop env name l = qualify env name l []
-
-qualifyTopDummy :: (Qualify a) => Env -> ModName -> a -> a
-qualifyTopDummy env name = qualifyTop env name dummySourcePos
-
-dummySourcePos :: F.SourcePos
-dummySourcePos = F.loc (F.dummyLoc ())
 
 class Qualify a where
   qualify :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
@@ -360,10 +351,6 @@ qualifySymbol env name l bs x
   where
     isSpl     = isSplSymbol env bs x
 
-
-qualifyLocSymbolTop :: Env -> ModName -> F.LocSymbol -> F.LocSymbol
-qualifyLocSymbolTop env modName l  = l {val = qualifyTop env modName (loc l) (val l)}
-
 isSplSymbol :: Env -> [F.Symbol] -> F.Symbol -> Bool
 isSplSymbol env bs x
   =  isWiredInName x

From f7ca1d16f97a34330ee8f1299715f9825d038b8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Fri, 13 Dec 2024 11:39:59 +0000
Subject: [PATCH 13/16] Remove Qualify type class

---
 .../Language/Haskell/Liquid/Bare/Expand.hs    |   9 +-
 .../Language/Haskell/Liquid/Bare/Resolve.hs   | 155 +-----------------
 2 files changed, 3 insertions(+), 161 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
index ba01a207a1..f0b7441e50 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -75,13 +75,13 @@ makeRTEnv env modName mySpec dependencySpecs lmap
           = renameRTArgs $ makeRTAliases tAs $ makeREAliases eAs
   where
     tAs   = [ t                   | (_, s)  <- specs, t <- Ms.aliases  s ]
-    eAs   = [ specREAlias env m e | (m, s)  <- specs, e <- Ms.ealiases s ]
+    eAs   = [ e | (_m, s)  <- specs, e <- Ms.ealiases s ]
          ++ if typeclass (getConfig env) then []
                                               -- lmap expansion happens during elaboration
                                               -- this clearly breaks things if a signature
                                               -- contains lmap functions but never gets
                                               -- elaborated
-              else [ specREAlias env modName e | (_, xl) <- M.toList (lmSymDefs lmap)
+              else [ e | (_, xl) <- M.toList (lmSymDefs lmap)
                                   , let e    = lmapEAlias xl             ]
     specs = (modName, mySpec) : dependencySpecs
 
@@ -131,11 +131,6 @@ makeRTAliases lxts rte = graphExpand buildTypeEdges f rte lxts
   where
     f rtEnv xt         = setRTAlias rtEnv (expandLoc rtEnv xt)
 
-specREAlias :: Bare.Env -> ModName -> Located (RTAlias F.Symbol F.Expr) -> Located (RTAlias F.Symbol F.Expr)
-specREAlias env m la = F.atLoc la $ a { rtBody = Bare.qualify env m (loc la) (rtVArgs a) (rtBody a) }
-  where
-    a     = val la
-
 --------------------------------------------------------------------------------------------------------------
 
 graphExpand :: (PPrint t)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
index b09257eb4a..1e0976d2ae 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
@@ -20,7 +20,6 @@ module Language.Haskell.Liquid.Bare.Resolve
 
     -- * Resolving symbols
   , ResolveSym (..)
-  , Qualify (..)
   , Lookup
 
   -- * Looking up names
@@ -92,7 +91,6 @@ import           Language.Haskell.Liquid.Types.Specs
 import           Language.Haskell.Liquid.Types.Visitors
 import           Language.Haskell.Liquid.Bare.Types
 import           Language.Haskell.Liquid.UX.Config
-import           Language.Haskell.Liquid.WiredIn
 import           System.IO.Unsafe (unsafePerformIO)
 
 myTracepp :: (F.PPrint a) => String -> a -> a
@@ -311,157 +309,6 @@ srcVars src = filter Ghc.isId .  fmap Misc.thd3 . Misc.fstByRank $ concat
 dataConVars :: [Ghc.DataCon] -> [Ghc.Var]
 dataConVars dcs = (Ghc.dataConWorkId <$> dcs) ++ (Ghc.dataConWrapId <$> dcs)
 
--------------------------------------------------------------------------------
--- | Qualify various names
--------------------------------------------------------------------------------
-
-class Qualify a where
-  qualify :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
-
-instance Qualify TyConMap where
-  qualify env name l bs tyi = tyi
-    { tcmTyRTy = tx <$> tcmTyRTy tyi
-    , tcmFIRTy = tx <$> tcmFIRTy tyi
-    }
-    where
-      tx :: (Qualify a) => a -> a
-      tx = qualify env name l bs
-
-instance Qualify TyConP where
-  qualify env name _ bs tcp = tcp { tcpSizeFun = qualify env name (tcpLoc tcp) bs <$> tcpSizeFun tcp }
-
-instance Qualify v => Qualify (SizeFunV v) where
-  qualify env name _ bs (SymSizeFun x) = SymSizeFun (qualify env name (F.loc (F.dummyLoc x)) bs x)
-  qualify _   _    _ _  sf              = sf
-
-instance Qualify F.Equation where
-  qualify _env _name _l _bs x = x -- TODO-REBARE
--- REBARE: qualifyAxiomEq :: Bare.Env -> Var -> Subst -> AxiomEq -> AxiomEq
--- REBARE: qualifyAxiomEq v su eq = subst su eq { eqName = symbol v}
-
-instance Qualify F.Symbol where
-  qualify env name l bs x = qualifySymbol env name l bs x
-
-qualifySymbol :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> F.Symbol -> F.Symbol
-qualifySymbol env name l bs x
-  | isSpl     = x
-  | otherwise = case resolveLocSym env name "Symbol" (F.Loc l l x) of
-                  Left _ -> x
-                  Right v -> v
-  where
-    isSpl     = isSplSymbol env bs x
-
-isSplSymbol :: Env -> [F.Symbol] -> F.Symbol -> Bool
-isSplSymbol env bs x
-  =  isWiredInName x
-  || elem x bs
-  || S.member x (reGlobSyms env)
-
-instance (Qualify a) => Qualify (Located a) where
-  qualify env name l bs = fmap (qualify env name l bs)
-
-instance (Qualify a) => Qualify [a] where
-  qualify env name l bs = fmap (qualify env name l bs)
-
-instance (Qualify a) => Qualify (Maybe a) where
-  qualify env name l bs = fmap (qualify env name l bs)
-
-instance Qualify Body where
-  qualify env name l bs (P   p) = P   (qualify env name l bs p)
-  qualify env name l bs (E   e) = E   (qualify env name l bs e)
-  qualify env name l bs (R x p) = R x (qualify env name l bs p)
-
-instance Qualify TyConInfo where
-  qualify env name l bs tci = tci { sizeFunction = qualify env name l bs <$> sizeFunction tci }
-
-instance Qualify RTyCon where
-  qualify env name l bs rtc = rtc { rtc_info = qualify env name l bs (rtc_info rtc) }
-
-instance Qualify (Measure SpecType Ghc.DataCon) where
-  qualify env name _ bs m = m -- FIXME substEnv env name bs $
-    { msName = updateLHNameSymbol (qualify env name l bs) <$> lname
-    , msEqns = qualify env name l bs <$> msEqns m
-    }
-    where
-      l      = F.loc  lname
-      lname  = msName m
-
-
-instance Qualify (Def ty ctor) where
-  qualify env name l bs d = d
-    { body  = qualify env name l (bs ++ bs') (body d) }
-    where
-      bs'   = fst <$> binds d
-
-instance Qualify BareMeasure where
-  qualify env name l bs m = m
-    { msEqns = qualify env name l bs (msEqns m)
-    }
-
-instance Qualify DataCtor where
-  qualify env name l bs c = c
-    { dcTheta  = qualify env name l bs (dcTheta  c)
-    , dcFields = qualify env name l bs (dcFields c)
-    , dcResult = qualify env name l bs (dcResult c)
-    }
-
-instance Qualify DataDecl where
-  qualify env name l bs d = d
-    { tycDCons  = qualify env name l bs (tycDCons  d)
-    , tycPropTy = qualify env name l bs (tycPropTy d)
-    }
-
-instance Qualify ModSpecs where
-  qualify env name l bs = Misc.hashMapMapWithKey (\_ -> qualify env name l bs)
-
-instance Qualify b => Qualify (a, b) where
-  qualify env name l bs (x, y) = (x, qualify env name l bs y)
-
-instance Qualify BareSpec where
-  qualify = qualifyBareSpec
-
-qualifyBareSpec :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> BareSpec -> BareSpec
-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)
-  , dataDecls  = qualify env name l bs (dataDecls  sp)
-  , newtyDecls = qualify env name l bs (newtyDecls sp)
-  , ialiases   = [ (f x, f y) | (x, y) <- ialiases sp ]
-  }
-  where f      = qualify env name l bs
-
-instance Qualify a => Qualify (RTAlias F.Symbol a) where
-  qualify env name l bs rtAlias
-   = rtAlias { rtName  = qualify env name l bs (rtName rtAlias)
-             , rtTArgs = qualify env name l bs (rtTArgs rtAlias)
-             , rtVArgs = qualify env name l bs (rtVArgs rtAlias)
-             , rtBody  = qualify env name l bs (rtBody rtAlias)
-             }
-
-instance Qualify F.Expr where
-  qualify = substEnv
-
-instance Qualify RReft where
-  qualify = substEnv
-
-instance Qualify F.Qualifier where
-  qualify env name _ bs q = q { F.qBody = qualify env name (F.qPos q) bs' (F.qBody q) }
-    where
-      bs'                 = bs ++ (F.qpSym <$> F.qParams q)
-
-substEnv :: (F.Subable a) => Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
-substEnv env name l bs = F.substa (qualifySymbol env name l bs)
-
-instance Qualify SpecType where
-  qualify x1 x2 x3 x4 x5 = emapReft (substFreeEnv x1 x2 x3) x4 x5
-
-instance Qualify BareType where
-  qualify x1 x2 x3 x4 x5 = emapReft (substFreeEnv x1 x2 x3) x4 x5
-
-substFreeEnv :: (F.Subable a) => Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
-substFreeEnv env name l bs = F.substf (F.EVar . qualifySymbol env name l bs)
-
 -------------------------------------------------------------------------------
 lookupGhcNamedVar :: (Ghc.NamedThing a, F.Symbolic a) => Env -> ModName -> a -> Maybe Ghc.Var
 -------------------------------------------------------------------------------
@@ -907,7 +754,7 @@ ofBRType env name f l = go []
     go bs (RRTy xts r o t)  = RRTy  <$> xts' <*> goReft bs r <*> pure o <*> go bs t
       where xts'            = mapM (traverse (go bs)) xts
     go bs (RHole r)         = RHole    <$> goReft bs r
-    go bs (RExprArg le)     = return    $ RExprArg (qualify env name l bs le)
+    go _ (RExprArg le)      = return    $ RExprArg le
     goRef bs (RProp ss (RHole r)) = rPropP <$> mapM goSyms ss <*> goReft bs r
     goRef bs (RProp ss t)         = RProp  <$> mapM goSyms ss <*> go bs t
     goSyms (x, t)                 = (x,) <$> ofBSortE env name l t

From d316e9217c06c2f2d7dc604c4611fb1f9c82b223 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Fri, 13 Dec 2024 11:45:48 +0000
Subject: [PATCH 14/16] Please hlint

---
 liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index 374d906968..95a2356d2a 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -999,7 +999,7 @@ makeSpecData src env sigEnv measEnv sig specs = SpData
                        , let tt  = Bare.plugHoles (typeclass $ getConfig env) sigEnv name (Bare.LqTV x) t
                    ]
   , gsMeas       = [ (F.symbol x, uRType <$> t) | (x, t) <- measVars ]
-  , gsMeasures   = (ms1 ++ ms2)
+  , gsMeasures   = ms1 ++ ms2
   , gsOpaqueRefls = fst <$> Bare.meOpaqueRefl measEnv
   , gsInvariants = Misc.nubHashOn (F.loc . snd) invs
   , gsIaliases   = concatMap (makeIAliases env sigEnv) (M.toList specs)

From 737abf508f53ce0896a9d47ce2720835d4b04f8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Fri, 13 Dec 2024 14:02:18 +0000
Subject: [PATCH 15/16] Style changes

---
 .../src/Language/Haskell/Liquid/Bare.hs               | 11 +++++------
 .../src/Language/Haskell/Liquid/Bare/Axiom.hs         |  2 +-
 .../src/Language/Haskell/Liquid/Bare/DataType.hs      |  3 ++-
 .../src/Language/Haskell/Liquid/Bare/Expand.hs        |  2 +-
 .../src/Language/Haskell/Liquid/Bare/Measure.hs       |  2 +-
 .../src/Language/Haskell/Liquid/Bare/Plugged.hs       |  4 ++--
 6 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index 95a2356d2a..e8d1c56858 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -317,7 +317,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
     simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
     simplifier = pure -- no simplification
     allowTC  = typeclass cfg
-    mySpec2  = Bare.expand rtEnv l mySpec1    where l = F.dummyPos "expand-mySpec2"
+    mySpec2  = Bare.expand rtEnv (F.dummyPos "expand-mySpec2") mySpec1
     iSpecs2  = Bare.expand rtEnv (F.dummyPos "expand-iSpecs2") (M.fromList dependencySpecs)
     rtEnv    = Bare.makeRTEnv env name mySpec1 dependencySpecs lmap
     mspecs   = (name, mySpec0) : dependencySpecs
@@ -490,9 +490,8 @@ makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual
                    ++ (fst <$> Bare.meClassSyms measEnv)
 
 makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec F.Symbol ty) -> [F.Qualifier]
-makeQualifiers env tycEnv (modn, spec)
-  = Mb.mapMaybe (resolveQParams       env tycEnv modn)
-  $ Ms.qualifiers spec
+makeQualifiers env tycEnv (modn, spec) =
+    Mb.mapMaybe (resolveQParams env tycEnv modn) $ Ms.qualifiers spec
 
 
 -- | @resolveQualParams@ converts the sorts of parameters from, e.g.
@@ -854,8 +853,8 @@ makeTExpr env tySigs rtEnv spec = do
   let vSigExprs = Misc.hashMapMapWithKey (\v t -> (t, M.lookup v vExprs)) vSigs
   return [ (v, t, qual <$> es) | (v, (t, es)) <- M.toList vSigExprs ]
   where
-    qual es   = expandTermExpr rtEnv <$> es
-    vSigs       = M.fromList tySigs
+    qual es = expandTermExpr rtEnv <$> es
+    vSigs = M.fromList tySigs
 
 expandTermExpr :: BareRTEnv -> Located F.Expr -> Located F.Expr
 expandTermExpr rtEnv le
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
index bd46e9fbe3..905bc24aed 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs
@@ -316,7 +316,7 @@ makeAxiom :: Bare.Env -> Bare.TycEnv -> LogicMap
 makeAxiom env tycEnv lmap (x, mbT, v, def)
             = (v, t, e)
   where
-    (t, e) = makeAssumeType allowTC embs lmap dm x mbT v def
+    (t, e)  = makeAssumeType allowTC embs lmap dm x mbT v def
     embs    = Bare.tcEmbs       tycEnv
     dm      = Bare.tcDataConMap tycEnv
     allowTC = typeclass (getConfig env)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
index a3ee66a4cf..ad554e45f9 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
@@ -656,7 +656,8 @@ ofBDataCtorTc env name l l' tc αs ps πs _ctor@(DataCtor _c as _ xts res) c' =
     res'          = Bare.ofBareType env name l (Just ps) <$> res
     t0'           = dataConResultTy c' αs t0 res'
     _cfg          = getConfig env
-    (yts, ot)     = (zip xs ts', t0')
+    yts           = zip xs ts'
+    ot            = t0'
     zts           = zipWith (normalizeField c') [1..] (reverse yts)
     usedTvs       = S.fromList (ty_var_value <$> concatMap RT.freeTyVars (t0':ts'))
     cs            = [ p | p <- RT.ofType <$> Ghc.dataConTheta c', keepPredType usedTvs p ]
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
index f0b7441e50..8f1fcebd94 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -74,7 +74,7 @@ makeRTEnv
 makeRTEnv env modName mySpec dependencySpecs lmap
           = renameRTArgs $ makeRTAliases tAs $ makeREAliases eAs
   where
-    tAs   = [ t                   | (_, s)  <- specs, t <- Ms.aliases  s ]
+    tAs   = [ t | (_, s)  <- specs, t <- Ms.aliases  s ]
     eAs   = [ e | (_m, s)  <- specs, e <- Ms.ealiases s ]
          ++ if typeclass (getConfig env) then []
                                               -- lmap expansion happens during elaboration
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index 4cdf7aca6b..5abfd42820 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
@@ -560,7 +560,7 @@ mkMeasureSort env name (Ms.MSpec c mm cm im) =
 
 expandMeasure :: BareRTEnv -> BareMeasure -> BareMeasure
 expandMeasure rtEnv m = m
-  { msSort = RT.generalize                   <$> msSort m
+  { msSort = RT.generalize <$> msSort m
   , msEqns = expandMeasureDef rtEnv <$> msEqns m
   }
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
index 2326728f6d..4e18dc8a51 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
@@ -144,8 +144,8 @@ plugMany :: Bool -> F.TCEmb Ghc.TyCon -> Bare.TyConMap
 plugMany allowTC embs tyi ldcp (hsAs, hsArgs, hsRes) (lqAs, lqArgs, lqRes)
                      = F.notracepp msg (drop nTyVars (zip (map lookupLHName xs) ts), t)
   where
-    lookupLHName s = Mb.fromMaybe (panic (Just (GM.fSrcSpan ldcp)) $ "unexpected symbol: " ++ show s) $ lookup s lhNameMap
-    lhNameMap = [ (lhNameToUnqualifiedSymbol n, n) | n <- map fst lqArgs ]
+    lookupLHName s   = Mb.fromMaybe (panic (Just (GM.fSrcSpan ldcp)) $ "unexpected symbol: " ++ show s) $ lookup s lhNameMap
+    lhNameMap        = [ (lhNameToUnqualifiedSymbol n, n) | n <- map fst lqArgs ]
     ((xs,_,ts,_), t) = bkArrow (val pT)
     pT               = plugHoles allowTC (Bare.LqTV dcName) embs tyi (const killHoles) hsT (F.atLoc ldcp lqT)
     hsT              = foldr (Ghc.mkFunTy Ghc.FTF_T_T Ghc.ManyTy) hsRes hsArgs'

From 5ec07732692ad274faf647416112f69327af11e9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Fri, 13 Dec 2024 14:27:33 +0000
Subject: [PATCH 16/16] Remove unused parameter in makeSpecName

---
 liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index e8d1c56858..b7b4bfc0ed 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -250,7 +250,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
     , _gsRefl   = refl
     , _gsData   = sData
     , _gsQual   = qual
-    , _gsName   = makeSpecName env     tycEnv measEnv   name
+    , _gsName   = makeSpecName env     tycEnv measEnv
     , _gsVars   = spcVars
     , _gsTerm   = spcTerm
 
@@ -1096,9 +1096,9 @@ mkReft _ _ _ _
 
 -- REBARE: formerly, makeGhcSpec3
 -------------------------------------------------------------------------------------------
-makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> ModName -> GhcSpecNames
+makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> GhcSpecNames
 -------------------------------------------------------------------------------------------
-makeSpecName env tycEnv measEnv _name = SpNames
+makeSpecName env tycEnv measEnv = SpNames
   { gsFreeSyms = Bare.reSyms env
   , gsDconsP   = [ F.atLoc dc (dcpCon dc) | dc <- datacons ++ cls ]
   , gsTconsP   = tycons