ucsd-progsys/liquidhaskell — pull request #149 by nikivazou (2013-11-05 01:43:15+00:00)
Title: Terminating expressions

A fix for #129.

See `tests/pos/GeneralizedTermination.hs` and `tests/pos/Even0.hs` as examples.

Some implementation info:
In the example,
```
foo :: Int -> Int -> Int
{-@ foo :: x:Nat -> y:Nat -> Nat /[x+y] @-}

foo n m
| cond 1 = 0
| cond 2 && n > 1 = foo (n-1) m
| cond 3 && m > 2 = foo (n+1) (m-2)
```

We need to give `foo` a type that checks that `n - 1 + m < n + m`
So I defined a new type
```
RRTy r t
```
with meaning "if you prove r you get a type t"
So the inner foo has type
``` foo :: x:Nat -> y:Nat -> RRTy (x+y γ |- r <=> true => true

A nice consequence of having this different kind of constraints is that when they fail we can provide a "more precise" warning. See `tests/neg/GeneralizedTermination.hs` that returns:
```
**** UNSAFE: Termination Check Error: tests/neg/GeneralizedTermination.hs:9:23-38
```