Allow reflecting functions with local definitions

[facundominguez]

Functions with local definitions cannot be reflected at the moment. If the user wants to reflect them, she must rewrite them to not use local definitions.

For instance, the following fails at the moment.

{-@ LIQUID "--reflection" @-}
import Prelude()

{-@ reflect foldr @-}
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z = go
  where
    go [] = z
    go (x:xs) = f x (go xs)

The error is

Test2.hs:6:13: error:
    Cannot lift Haskell function `foldr` to logic
    Cannot make Logical Substitution of Recursive Definitions
  |
6 | {-@ reflect foldr @-}
  |

The following rewritten definition can be reflected instead.

{-@ LIQUID "--reflection" @-}
import Prelude()

{-@ reflect foldr @-}
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z
foldr f z (x:xs) = f x (foldr f z xs)

The designs of the solution need to be explored. One approach is to use local rewrites.

[AlecsFerra]

I think that it should work with local rewrites by rewriting go as a lambda: go = \(x:xs) -> f x (go xs) as I guess the termination checker can already check if go is terminating, one down side is that we will lock the user in using --eta-beta but personally I think it is fine