ucsd-progsys/liquidhaskell — pull request #289 by nikivazou (2014-12-21 20:32:39+00:00)
Title: Logical Constraints

See [tests/pos/Constraints.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/1465a5cfd54c3077ce85306bfd2361ef4c6caab8/tests/pos/Constraints.hs)

Logical Constraints are of the form

{x1:a1 | r1} -> ... -> {xn:an | rn} -> {v:b | p} -> {v:b | q} (1)

and produce the formula

r1 /\ ... /\ rn => (p => q) (2)

Meaning if the constraint (1) appears in the type of a function `f`, then the formula (2) is
- assumed when the body of `f` is checked
- checked to hold when `f` is called