ucsd-progsys/liquidhaskell — pull request #204 by nikivazou (2014-04-23 18:49:26+00:00)
Title: Deriving Measures for Record Selectors

see [tests/pos/RecSelector.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/recSelector/tests/pos/RecSelector.hs) for an example.

Two notes:
* measure record selectors are imported from imported data definitions.
* the record selector `r` defined the Symbol `r`, ie, its name is not made unique so that the user can use it in the refinements. This can clash with the only other symbol that is not made unique, the symbol for abstract refinements. Eg, the below definitions, with two conflicting `r`s was problimatic:

~~~
{-@ data RGRef a

Prop, r :: a -> a -> Prop >
= Wrap (r :: R.IORef a

) @-}
~~~

But I suggest postponing this name-resolution issue.