ucsd-progsys/liquidhaskell — pull request #17 by ranjitjhala (2012-11-20 05:02:06+00:00)
Title: Self: Allow for cyclic/self referential invariants

Many changes to allow "Self-Invariants" -- see README.md. Most importantly,

* now we have distinct VVars all over the place,
* this causes all sorts of hassles with free and bound variables getting captured and freed in refts.
So:
* We always "unify" refinements with FRESH VV so there is no danger of capture.
* We always "bind" the top-level refinement for a RApp in the relevant SubC and WfC environments so that they are visible and hence, can be referred to at inner levels.