Another localSpec issue

[nikivazou]

We are unable to type go as a local function in the following code (see tests/todo/LocalSpec1.hs)

{-@ filterElts :: forall <p :: a -> Prop>. Eq a => [a<p>] -> [a] -> [a<p>] @-}
 filterElts :: Eq a => [a] -> [a] -> [a]
 filterElts xs ys = go xs xs ys

 {-@ go :: forall <p :: a -> Prop>. Eq a => xs:[a<p>] -> ws:[a<p>] -> zs:[a] -> [a<p>] /[(len zs), (len ws)] @-}
 go :: Eq a => [a] -> [a] -> [a] -> [a]
 go xs (w:ws) (z:zs) | w == z    = z : go xs xs zs
                     | otherwise = go xs ws (z:zs)
 go xs []     (z:zs)             = go xs xs zs
 go xs ws     []                 = []

[gridaphobe]

Yea, this looks like the same issue as #154, but we can't rely on holes this time due to the abstract refinement..

I think the general solution is to expand the scope available in type annotations to match the Haskell scoping rules, e.g.

{-@ filterElts :: forall <p :: a -> Prop>. Eq a => [a<p>] -> [a] -> [a<p>] @-}
 filterElts :: Eq a => [a] -> [a] -> [a]
 filterElts xs ys = go xs xs ys
   where
     {-@ go :: xs:[a<p>] -> ws:[a<p>] -> zs:[a] -> [a<p>] /[(len zs), (len ws)] @-}
     go xs (w:ws) (z:zs) | w == z    = z : go xs xs zs
                         | otherwise = go xs ws (z:zs)
     go xs []     (z:zs)             = go xs xs zs
     go xs ws     []                 = []