Resolve names only once

[facundominguez]

#2303 adds a minimal test showing the problem.

Currently, names in specifications are resolved multiple times. Name resolution determines for each name in a spec, what is the Haskell definition it is associated to. Type and data constructors exist both in the logic and in Haskell, and signatures with refinement types are also linked to Haskell definitions.

These names are resolved once when compiling the module containing the specs, and they are resolved again when compiling a module that transitively imports the module containing the specs. This is not ideal for the duplicated work, but it is also problematic because the implementation doesn't ensure that names would resolve in the same way on all of the attempts.

Resolving names requires looking up an identifier in an environment storing all the things that GHC knows to be in scope. When resolving names for transitive dependencies, a single environment is used to resolve the names of all of the transitively imported modules. In order to disambiguate names that could refer to one of many definitions in Haskell, the resolution algorithm considers whether the name has a qualifier, and what is the name in which the spec has been defined. But this strategy not always yields the same resolution as obtained when compiling the imported module, which uses, understandably, a smaller environment to resolve the names.

This issue is about making name resolution more predictable. The current workaround is to manually fully qualify names in specifications, although there are restrictions to do this when it comes to data specifications.

Part of the solution would likely be storing specifications in interface files after their names have been fully qualified with the module of origin of the thing referred by the name.

Another related concern is that variable names should also include the package of origin, in case multiple packages define modules with the same names.

There is work in progress in liquidhaskell and liquid-fixpoint.

[kd1729]

Hi @facundominguez, I would like to take up this idea for GSOC. I am making the proposal, how can I get it reviewed?

[facundominguez]

Hello @kd1729! You can email it to me. I'm also reachable via the liquidhaskell slack.

[ninioArtillero]

Greetings @facundominguez , I'm also interested in the idea! Would get in touch :)