After many experiments, some error tracing, and much code analysis, a comment on the progress is due:

• Some local functions—used to build an InScopeNonReflectedEnv at makeLogicEnvs—were moved to the top level in 98d3d51. This is the first step in the updated solution strategy to allow qualify type aliases: reusing the implementation of InScopeNonReflectedEnv, which includes the aliases a module is imported with and has a lookup function that matches against both qualified and unqualified names (providing close matches in case of failure to report to the user).

• In 6fd94aa the InScopeNonReflectedEnv was parameterized to an InScopeEnv a to reimplement the key-value map produced by collectTypeAliases. The new parameter lets us include the type alias representation of type RTAlias Symbol () (where the unit comes from emptying its body) in the environment, which is needed just before the first name resolution pass—when fixing the expression arguments in fixExpressionArgsOfTypeAliases—.¹ Now lookupInScopeNonReflectedEnv is also used for type alias lookup during the first name resolution pass (implemented as a generic traversal of the spec using resolveLHName). After this change, liquidhaskell failed to compile and complained about not being able to resolve a PtrV alias in src/Foreigh/Concurrent_LHAssumptions.hs.

• It turned out that the original implementation depends on bringing along—in the TargetDependencies build at ...GHC.Plugin.loadDependencies—some transitive dependencies that are queried when collecting the aliases (and perhaps for other purposes, which I'm looking into). 8441f2e made this explicit by giving an empty module alias to names coming from a transitive dependency to prevent them from mapping over an empty list in mkAliasEnv and getting discarded—. But as @facundominguez pointed out:

  If I understand correctly, the type aliases should be in scope in the modules that are imported directly. Once imported, type aliases would be accumulated transitively. If T exports a type alias that has been imported from a transitive dependency, the following should work:

  import qualified T as Q
  
  {-@ f :: Q.TypeAlias @-}
  f :: Int
  f = 0
  

  Using a empty module alias gives a behavior that the user would not expect.

  My opinion was that having an empty module alias for transitive dependencies reflected the fact that type aliases of transitive dependencies are not included in the LiftedSpec of the imported module, but rather are accessed directly from the specs of those dependencies themselves (as this change fixing the error mentioned in the previous point seems to suggest). As far as we could tell by reading the code that builds the LiftedSpec, that is not the case. I'm currently investigating this matter.

• fab4891 fixes a bug that prevented an expected name ambiguity from arising in a regression test (namely, names-neg), while a6a8357 was introduced as a safeguard, given that at that point no unresolved names are expected.

We speculate that a comprehensive solution to this matter would be to have a mechanism to explicitly export and re-export aliases (or other LH specs). Nevertheless, that approach exceeds the scope of my GSoC project and is left for future work.

Going forward, I'll make sure that aliases from transitive dependencies actually populate a module's LiftedSpec (which is the one used by clients for verification) and that local definitions can shadow them.

Now that this PR is ready for review, I'll provide an overview of the proposed changes:

In brief, we can now qualify aliases to disambiguate cases where two imports export type aliases with the same name. The approach we followed succeeded: by using the InScopeEnv for alias symbol lookup, we are now able to resolve qualified type aliases.

It turns out type alias environments are created at four different stages:

1. By collectTypeAliases at the start of name resolution (resolveLHNames) to resolve variable names upfront, fix the term/value arguments of the aliases themselves (since all such arguments are initially parsed as type arguments), and finally—during the first name resolution pass—for resolving type constructor names.
2. By makeRTEnv during the construction of the TargetSpec (in makeGhcSpec0) to expand all type alias uses.
3. By myRTEnv, to prepare the type aliases to be added into the LiftedSpec. Here, both expression (predicate) and type aliases are normalized and filtered to include only locally defined aliases.
4. During checkTargetSpec, to throw an error on duplicate alias names among all known aliases (from the current module’s BareSpec and the LiftedSpecs of dependencies).

In all these cases, the environments were built from the aliases of the current module and all its transitive dependencies. For the qualified alias approach to work, I had to make changes at all of these sites. Accordingly:

1. We now use an InScopeEnv for symbol lookup (via lookupInScopeNonReflectedEnv) to resolve qualified names. All aliases originate either from the current module or a direct import. See liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs.
2. I decoupled the expansion of type and expression aliases. Now, for type aliases, we use LHNames as keys for an AliasTable' (used to order the aliases for expansion and check for cyclic dependencies among them) and, most importantly, for the BareRTEnv. This last environment is used to expand aliases at all use sites, ultimately by calling expandBareType. See liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs.
3. Only expression aliases are filtered to include just those defined locally (for now), while all type aliases are gathered, ensuring we keep only one per unqualified name. Among these ambiguous cases, we keep the locally defined one or the last—according to the lexicographic ordering of the modules they are imported from—. In other words, even though we may have used any such aliases when creating the specification, only one of them is stored in the resulting spec. This is reasonable compromise until a mechanism exists for explicitly exporting and importing type aliases. See liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs.
4. We only check for duplicate type alias definitions within the current module. See liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs.

To summarize:

Previously, all transitive dependencies were considered during collectTypeAliases to build an environment (a symbol hash map) for name resolution. This posed no issue, as the (unqualified) symbol was intended to uniquely identify each alias. In this setting, aliases from dependencies could shadow local aliases—or aliases from other dependencies—during name resolution based on the accidental order in which their symbols were concatenated when the relevant hash map was created. This ambiguity would be caught later at checkTargetSpec: If no duplicate name was detected, only the locally defined aliases were stored in the final LiftedSpec.

Now, we ensure that all type aliases from transitive dependencies are included in the LiftedSpec, so that during name resolution we gather type aliases from direct imports only. This allows us to disambiguate cases where two imports export an alias with the same name by qualifying its use (with the module name or a qualified import alias). Nevertheless, we had to make a compromise due to the lack of a mechanism for explicitly exporting and importing type aliases: when storing an ambiguous alias into the LiftedSpec, we give preference to the locally defined or pick the one from the lexicographical last module (similar to how conflicting measures are handled).