ucsd-progsys/liquidhaskell — pull request #137 by gridaphobe (2013-10-24 00:09:41+00:00)
Title: Add preliminary support for attaching specs to type class methods

This branch adds support for generic measures that can be used with multiple types, the syntax is modeled after type classes, e.g.

```haskell
class Sized s where
{-@ class measure size :: forall a. a -> Int @-}

{-@ size :: forall s. Sized s => forall a. x:s a -> {v:Int | v = (size x)} @-}
size :: s a -> Int

instance Sized [] where
{-@ instance measure size :: [a] -> Int
size ([]) = 0
size (x:xs) = 1 + (size xs)
@-}
size = length

{-@ x :: {v:[Int] | (size v) = 3} @-}
x :: [Int]
x = [1,2,3]
```

**NOTE**: as of right now we do not check that the instance definitions match the spec for the class method. This is unsound, but will be addressed shortly and in the meantime this branch will allow progress on verifying `vector`.