Add idea for name resolution in Liquid Haskell

Author: facundominguez

content/ideas/liquidhaskell-name-resolution.md

@@ -0,0 +1,55 @@
+---
+title: Resolve names only once in Liquid Haskell
+---
+
+Liquid Haskell is a tool to verify Haskell programs. The programmer supplies
+specifications for functions and data types in special comments, and the tool
+produces error messages when it cannot automatically prove that the program
+behaves as specified. The programmer can then improve the specifications or the
+program until the tool reports no errors. More information is available on the
+[Liquid Haskell website](https://ucsd-progsys.github.io/liquidhaskell/).
+
+Liquid Haskell has been around for a decade and is a versatile tool, but it
+still has a few issues which hinder the user experience. This project is to
+address one of these shortcomings.
+
+When analyzing a program, Liquid Haskell needs to link identifiers that appear
+in specifications to the entities they refer to, much in the same way that a
+compiler needs to link identifiers in the text of a function to the language
+entities that they represent. This task is called name resolution.
+
+The identifiers in a specification can refer to other specifications, or they
+can refer to Haskell entities like functions and types. The output of name
+resolution tells for each identifier the module in which the referred entity is
+defined and the package it comes from.
+
+At the moment, name resolution in Liquid Haskell is done twice for the same
+specifications, and the outcomes of both passes do not always yield the same
+result, leading to confusing errors and tedious workarounds. This task is about
+having name resolution done only once. For more details please see [the github
+issue](https://github.com/ucsd-progsys/liquidhaskell/issues/2169).
+
+A proposal must include at least a description of a tentative solution, and
+a plan to implement it. The proposal should also account for the writing of
+a blog post summarizing the contributions at the end.
+
+As a stretch goal, the project might specify and implement the scope rules
+and mechanisms to use in Liquid Haskell specifications.
+While the intention of Liquid Haskell maintainers over time has been to
+imitate GHC scoping rules as much as possible, there are case where Liquid
+Haskell just deviates from them.
+
+The following aspects haven't been answered explicitly so far for the Liquid
+Haskell scenario.
+
+* What names are in scope when writing the specifications of a module?
+
+* How should ambiguities be resolved when imports offer definitions with the same Liquid Haskell names?
+
+* What Liquid Haskell names are exported from modules and when?
+
+**Potential Mentors**: Facundo Domínguez
+
+**Difficulty**: Medium
+
+**Size**: 350 hours but they are flexible by adjusting the scope