Document that specs can depend on arguments of enclosing functions

[facundominguez]

Today I learned that the meaning of specs of local bindings can depend on arguments of an enclosing function. For instance, in the following function from the test suite, arg0 is available to the spec of bar.

{-@ foo :: x:_ -> y:_ -> {v:Int | v = x + y} @-}
foo :: Int -> Int -> Int
foo arg0 = bar
  where
    {-@ bar :: x:_ -> {v:Int | v = x + arg0} @-}
    bar arg1 = arg0 + arg1

It doesn't work for other things than arguments though, e.g. z is not in scope in the following spec.

{-@ foo :: x:_ -> y:_ -> {v:Int | v = x + y} @-}
foo :: Int -> Int -> Int
foo arg0 = bar
  where
    z = arg0
    {-@ bar :: x:_ -> {v:Int | v = x + z} @-}
    bar arg1 = arg0 + arg1

@ranjitjhala, should the fact that arguments of enclosing functions are in scope be documented?

[facundominguez]

Sheesh, z is brought into the scope of a local spec if used in the local function. For instance, the following passes verification.

foo :: Int -> Int -> Int
foo arg0 = bar
  where
    z = arg0
    {-@ bar :: x:_ -> {v:Int | v = x + z} @-}
    bar arg1 = const (arg0 + arg1) z

That's not what users will expect. Should we try to make it be always in scope?

[facundominguez]

I think that bindings are in scope only if GHC doesn't consider them deadcode. This is because when we get to analyse the desugared program, GHC has already pruned unused bindings.