ucsd-progsys/liquidhaskell — pull request #164 by nikivazou (2013-12-29 06:59:12+00:00)
Title: State and Non-Conflicting Substitutions

This branch work with `liquid-fixpoint/subst` and has the following modifications

* `tests/pos/State[|0|1].hs` define and use invariants on `State`

* the type arguments and the `VV` variables are refreshed to guarantee that substitutions are not conflicting

* The inline annotation is *ignored* by liquidHaskell, as it turns out (as in the bellow code) that inline annotations can make ghc use one variable in many lambda abstractions (ie., the invariant that ghc variables are unique breaks)

* `Reftable.top` is used with type `a -> a` (to keep the unique `VV`)

The branch gives the same failing tests as master (tests/pos/[malformed0|typeAliasDup].hs)

```
module Inline where
pop cmp a l u = popTo cmp a l u u
{-# INLINE pop #-}

popTo cmp a l u t = undefined
{-# INLINE popTo #-}

sortHeap cmp a l m u = loop (u-1) >> unsafeSwap a l m
where
loop k
| m < k = pop cmp a l k >> loop (k-1)
| otherwise = return ()
{-# INLINE sortHeap #-}

unsafeSwap = undefined
```