@@ -63,6 +63,7 @@ import Language.Haskell.Liquid.Types.Names
6363import Language.Haskell.Liquid.Types.RType
6464import Language.Haskell.Liquid.Types.RTypeOp
6565
66+ import Control.Monad.Except (ExceptT , runExceptT , throwError )
6667import Control.Monad ((<=<) , mplus , unless , void )
6768import Control.Monad.Identity
6869import Control.Monad.State.Strict
@@ -163,57 +164,60 @@ resolveLHNames
163164 -> BareSpecParsed
164165 -> TargetDependencies
165166 -> Either [Error ] (BareSpec , LogicNameEnv , LogicMap )
166- resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies = do
167- let ((bs, logicNameEnv, lmap2), ro) =
168- flip runState RenameOutput {roErrors = [] , roUsedNames = [] , roUsedDataCons = mempty } $ do
169- sp0 <- fixExpressionArgsOfTypeAliases taliases $ resolveBoundVarsInTypeAliases bareSpec0
170- -- First pass: A generic traversal that resolves names
171- -- of Haskell entities and type aliases.
172- sp1 <- mapMLocLHNames (\ l -> (<$ l) <$> resolveLHName l) sp0
173- -- Data decls contain fieldnames that introduce measures with the
174- -- same names. We resolve them before constructing the logic
175- -- environment.
176- dataDecls <- mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
177- let sp2 = sp1 {dataDecls}
178-
179- es0 <- gets roErrors
180- if null es0 then do
181-
182- -- Second pass: a traversal to resolve logic names using the following
183- -- lookup environments.
184- let (inScopeEnv, logicNameEnv0, privateReflectNames) =
185- makeLogicEnvs impMods thisModule sp2 dependencies
186- -- Add resolved local defines to the logic map.
187- lmap1 =
188- lmap <> mkLogicMap (HM. fromList $
189- (\ (k , v) ->
190- let k' = lhNameToResolvedSymbol <$> k in
191- (F. val k', (val <$> v) { lmVar = k' }))
192- <$> defines sp2)
193- sp3 <- fromBareSpecLHName <$>
194- resolveLogicNames
195- cfg
196- thisModule
197- inScopeEnv
198- globalRdrEnv
199- lmap1
200- localVars
201- logicNameEnv0
202- privateReflectNames
203- depsInlinesAndDefines
204- sp2
205- dcs <- gets roUsedDataCons
206- return (sp3 {usedDataCons = dcs} , logicNameEnv0, lmap1)
207- else
208- return ( error " resolveLHNames: invalid spec"
209- , error " resolveLHNames: invalid logic environment"
210- , error " resolveLHNames: invalid logic map" )
211- logicNameEnv' = extendLogicNameEnv logicNameEnv (roUsedNames ro)
212- if null (roErrors ro) then
213- Right (bs, logicNameEnv', lmap2)
214- else
215- Left (roErrors ro)
167+ resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies =
168+ flip evalState RenameOutput { roErrors = [] , roUsedNames = [] , roUsedDataCons = mempty } $
169+ runExceptT $ do
170+ -- Prepare type aliases for resolution.
171+ sp0 <- lift $ fixExpressionArgsOfTypeAliases taliases $ resolveBoundVarsInTypeAliases bareSpec0
172+
173+ checkErrors
174+
175+ -- First resolution pass: A generic traversal that resolves names
176+ -- of Haskell entities and type alias binders.
177+ sp1 <- lift $ mapMLocLHNames (\ l -> (<$ l) <$> resolveLHName l) sp0
178+
179+ -- Data decls contain fieldnames that introduce measures with the
180+ -- same names. We resolve them before constructing the logic
181+ -- environments.
182+ dataDecls <- lift $ mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
183+ let sp2 = sp1 {dataDecls}
184+
185+ checkErrors
186+
187+ -- Second resolution pass: a traversal to resolve logic names using the following
188+ -- lookup environments.
189+ let (inScopeEnv, logicNameEnv0, privateReflectNames) =
190+ makeLogicEnvs impMods thisModule sp2 dependencies
191+
192+ -- Add resolved local defines to the logic map.
193+ lmap1 = lmap <> mkLogicMap (HM. fromList $
194+ [ (F. val $ lhNameToResolvedSymbol <$> k,
195+ (val <$> v) { lmVar = lhNameToResolvedSymbol <$> k })
196+ | (k,v) <- defines sp2 ])
197+ sp3 <- lift $ fromBareSpecLHName <$>
198+ resolveLogicNames
199+ cfg
200+ thisModule
201+ inScopeEnv
202+ globalRdrEnv
203+ lmap1
204+ localVars
205+ logicNameEnv0
206+ privateReflectNames
207+ depsInlinesAndDefines
208+ sp2
209+
210+ checkErrors
211+
212+ dcs <- gets roUsedDataCons
213+ return (sp3 { usedDataCons = dcs }, logicNameEnv0, lmap1)
216214 where
215+ -- Early exit name resolution if errors are found and pass them to the output.
216+ checkErrors :: ExceptT [Error ] (StateT RenameOutput Identity ) ()
217+ checkErrors = do
218+ es <- gets roErrors
219+ unless (null es) (throwError es)
220+
217221 -- We collect type aliases before resolving names so we have a means to disambiguate
218222 -- imported and local ones (according to their resolution status).
219223 taliases = collectTypeAliases impMods thisModule bareSpec0 dependencies
@@ -285,6 +289,7 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependenc
285289 addError
286290 (ErrDupNames
287291 (LH. fSrcSpan lname)
292+ " variable"
288293 (pprint s)
289294 (map (PJ. text . GHC. showPprUnsafe) es)
290295 )
@@ -360,6 +365,7 @@ resolveSymbolToTcName globalRdrEnv lx
360365 [] -> Left $ errResolve [] " type constructor" " Cannot resolve name" lx
361366 es -> Left $ ErrDupNames
362367 (LH. fSrcSpan lx)
368+ " type constructor"
363369 (pprint s)
364370 (map (PJ. text . GHC. showPprUnsafe) es)
365371 where
@@ -542,20 +548,38 @@ data TypeAliasResolution a
542548 , tarLocallyDefined :: [(GHC. Module , LHName , a )]
543549 }
544550
545- errResolveTypeAlias :: LocSymbol -> TypeAliasResolution b -> Error
551+ errResolveTypeAlias :: LocSymbol -> TypeAliasResolution ( RTAlias x a ) -> Error
546552errResolveTypeAlias ls (FoundTypeAliases imported local) =
547- ErrDupNames (LH. fSrcSpan ls) (pprint $ val ls)
553+ ErrDupNames (LH. fSrcSpan ls) " type alias " (pprint $ val ls)
548554 (
549- map (\ (m, lhn, _) -> pprint (LH. qualifySymbol (symbol . GHC. moduleNameString . GHC. moduleName $ m)
550- $ getLHNameSymbol lhn)
551- PJ. <+>
552- PJ. text " defined in current module" )
553- local
555+ -- Currently, multiple local definitions prevent this error from being raised,
556+ -- because duplicate names are discarded when constructing the alias environment
557+ -- for each individual module,
558+ -- and a local alias always shadows any imported one. Such duplicates are detected
559+ -- later during validation of the final target spec.
560+ --
561+ -- Also, note that collected local type alias names remain unresolved at this stage,
562+ -- so we must extract their symbol using a function that can safely handle unresolved
563+ -- names.
564+ map (\ (_, lhn, rta) -> pprint (getLHNameSymbol lhn)
565+ PJ. <+>
566+ PJ. text " defined in current module at"
567+ PJ. <+>
568+ pprint (LH. fSrcSpan . rtName $ rta)
569+ )
570+ local
554571 ++
555- map (\ (m, lhn, _) -> pprint (lhNameToResolvedSymbol lhn)
556- PJ. <+>
557- PJ. text (" imported from " ++ GHC. moduleNameString (GHC. moduleName m)))
558- imported
572+ map (\ (m, lhn, rta) -> pprint (lhNameToUnqualifiedSymbol lhn)
573+ PJ. <+>
574+ PJ. text " imported from module"
575+ PJ. <+>
576+ PJ. text (GHC. moduleNameString (GHC. moduleName m))
577+ PJ. <+>
578+ PJ. text " defined at"
579+ PJ. <+>
580+ pprint (LH. fSrcSpan . rtName $ rta)
581+ )
582+ imported
559583 )
560584errResolveTypeAlias ls (NoSuchTypeAlias alts) =
561585 errResolve alts " type alias" " Cannot resolve name" ls
@@ -670,7 +694,10 @@ mkAliasEnv:: GHC.Module -> GHC.ImportedMods -> (GHC.Module, [(LHName, a)]) -> In
670694mkAliasEnv thisModule impMods (m, lhnames) =
671695 let aliases = moduleAliases thisModule impMods m
672696 in fromListSEnv
673- [ (LH. dropModuleNames $ getLHNameSymbol lhname, map (,(m, lhname, x)) aliases)
697+ -- Note that when building a name environment for the current module
698+ -- we might process unresolved names here.
699+ [ (LH. dropModuleNames $ getLHNameSymbol lhname
700+ , map (,(m, lhname, x)) aliases)
674701 | (lhname, x) <- lhnames
675702 ]
676703
@@ -792,6 +819,7 @@ resolveLogicNames cfg thisModule env globalRdrEnv lmap0 localVars lnameEnv priva
792819 errDupInScopeNames locSym inScopeNames =
793820 ErrDupNames
794821 (LH. fSrcSpan locSym)
822+ " non-reflected logic entity"
795823 (pprint (val locSym))
796824 [ pprint (lhNameToResolvedSymbol n) PJ. <+>
797825 PJ. text
@@ -835,6 +863,7 @@ resolveLogicNames cfg thisModule env globalRdrEnv lmap0 localVars lnameEnv priva
835863 addError
836864 (ErrDupNames
837865 (LH. fSrcSpan s)
866+ " data constructor"
838867 (pprint $ val s)
839868 (map (PJ. text . GHC. showPprUnsafe) es)
840869 )
@@ -874,6 +903,7 @@ resolveLogicNames cfg thisModule env globalRdrEnv lmap0 localVars lnameEnv priva
874903 addError
875904 (ErrDupNames
876905 (LH. fSrcSpan s)
906+ " variable"
877907 (pprint $ val s)
878908 (map (PJ. text . GHC. showPprUnsafe) es)
879909 )
0 commit comments