ucsd-progsys/liquidhaskell — pull request #177 by nikivazou (2014-02-20 22:30:48+00:00)
Title: add only checked binders into the environment binders

We used to add all type specifications into the environment, *before* we check them , so

~~~~
{-@ foo :: {v:Int| false} @-}
foo :: Int
foo = 1
~~~

was safe, because it assumes `false`.
Now, we first check and then add the specifications.

For the recursively defined variables, there are two choices

~~~~
{-@ foo :: {v:[Int]| false} @-}
foo :: [Int]
foo = 1:foo
~~~

Either assume the specification with a true top level refinement, ie., assume {-@ foo :: {v:[Int]| true} @-}
or assume the specification as it is {-@ foo :: {v:[Int]| false} @-}.

With the first choice we *cannot* prove
~~~~
{-@ foo :: {v:[Int]| false} @-}
foo :: [Int]
foo = foo
~~~

which is strange, as we can prove
~~~~
{-@ foo :: a @-}
foo :: a
foo = foo
~~~

Thus, I chose the second option.
In either case, recursive definitions with base types cannot be proven to terminate, so liquidHaskell will not allow then to be refinemented.