Add idea for name resolution in Liquid Haskell

Author: facundominguez

content/ideas/liquidhaskell-name-resolution.md

@@ -0,0 +1,53 @@
+---
+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 10 years 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 should include answers to at least the following questions plus any
+others that the candidate considers relevant:
+
+* What names should be accessible in the specifications of a given module?
+
+* What should be the mechanism to bring names in scope?
+
+* How should the system negotiate or resolve ambiguous names?
+
+* Which design and/or implementation steps should be done to adjust Liquid
+  Haskell to the proposed behaviors?
+
+* How much effort would the previous steps take?
+
+Proposals should also account for the writing of a blog post summarizing the
+contributions at the end.
+
+**Potential Mentors**: Facundo Domínguez
+
+**Difficulty**: Medium
+
+**Size**: 350 hours but they are flexible by adjusting the scope