Improperly scoped type annotations

[themattchan]

I have the following excerpt of a function:

stitch :: forall a . (a -> Maybe (a -> Maybe (a -> a))) -> [a] -> [a]
stitch combineable = go where
  {-@ go :: xs:[a] -> [a] / [len xs, 0] @-}
  go :: [a] -> [a]
  go [] = []
  go (h : t) = NE.toList $ nonempty h t
...

When I run with liquidhaskell-cabal on my entire project, I get this mysterious failure:

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

 /Users/matt/packet-analysis/src/Awake/Util.hs:438:11: Error: GHC Error

 438 |   let {-@ go :: xs:[a] -> [a] / [len xs, 0] @-}
                 ^

     Not in scope: variable or data constructor ` Awake.Util.go '

But, if I run liquid on the offending file directly, I get the proper error, which looks wrong in its own right:

LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

 /Users/matt/packet-analysis/src/Awake/Util.hs:438:13-26: Error: Specified type does not refine Haskell type for `go` (Plugged Init types)

 438 |   {-@ go :: xs:[a] -> [a] / [len xs, 0] @-}
                   ^^^^^^^^^^^^^^

 The Liquid type

     [a] -> [a]

 is inconsistent with the Haskell type

     forall a ->
(a -> GHC.Base.Maybe (a -> GHC.Base.Maybe (a -> a))) -> [a] -> [a]

 defined at /Users/matt/packet-analysis/src/Awake/Util.hs:440:3-4

I don't understand this enough yet to reduce this failure, and so far my attempts to do so all seem to work fine. Any ideas?

[nikivazou]

Well, local annotations are not properly exported/checked.

As a "fix" make your go a global function for now (as I definitely will not have time soon to get into that)

[ranjitjhala]

To elaborate: ghc can modify the types of the non top level cars in various odd ways that make this kind of name resolution brittle.

Is there a standalone file you can send us to reproduce the problem?

Another thing I often do is to use "holes" for the inner binders types and just leave the termination expression in.

On Sat, Oct 14, 2017 at 6:47 AM Niki Vazou notifications@github.com wrote:

Well, local annotations are not properly exported/checked.

As a "fix" make your go a global function for now (as I definitely will not have time soon to get into that)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1130#issuecomment-336635961, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOOxIH6NX7TSkdBwwl7arLliKulx0ks5ssLttgaJpZM4P5Gv4 .

[themattchan]

I wrote a function with the same type in a standalone file, and it did not have this problem. I also tried using holes, but that gave me the same error. What's strange is that when I removed the annotation for go, I got this failure deep inside the core set of specifications:

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

 /nix/store/jfnj6ylk3n5zp36dxzik4ic594r9cp5k-liquidhaskell-0.8.0.2/share/x86_64-osx-ghc-8.0.2/liquidhaskell-0.8.0.2/include/Prelude.spec:47:20: Error: GHC Error

 47 | type FF      = {v: Bool          | not v}
                         ^

     Not in scope: type constructor or class
 matchTyCon ` Bool '

[ranjitjhala]

Are you "hiding prelude"? When that happens LH doesn't know what Bool is...

On Mon, Oct 16, 2017 at 11:13 PM Matt Chan notifications@github.com wrote:

I wrote a function with the same type in a standalone file, and it did not have this problem. I also tried using holes, but that gave me the same error. What's strange is that when I removed those annotations, I got this failure deep inside the core set of specifications:

** DONE: annotate *****

RESULT: ERROR ****

*

/nix/store/jfnj6ylk3n5zp36dxzik4ic594r9cp5k-liquidhaskell-0.8.0.2/share/x86_64-osx-ghc-8.0.2/liquidhaskell-0.8.0.2/include/Prelude.spec:47:20: Error: GHC Error

47 | type FF = {v: Bool | not v} ^

 Not in scope: type constructor or class

matchTyCon ` Bool '

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1130#issuecomment-337054831, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOBtKriUAsS6WgoE5My5w7PeQSp-1ks5ss9BBgaJpZM4P5Gv4 .

[themattchan]

There's this line, which indicates to me that LH's import resolution needs a bit of work:

import           Prelude hiding (unzip)

[ranjitjhala]

Hmm. That shouldn't hide the Bool stuff. You cannot replicate this on a standalone file, right?

On Tue, Oct 17, 2017 at 12:55 PM, Matt Chan notifications@github.com wrote:

There's this line, which indicates to me that LH's import resolution needs a bit of work:

import Prelude hiding (unzip)

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1130#issuecomment-337351116, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuODgQ2PAgCC_dADQ_WuaioJ9VuIDiks5stQY8gaJpZM4P5Gv4 .

[themattchan]

I just tried it on this, which works fine (imports and where-binders)

module NoPrelude where
import Prelude hiding (zip, unzip)

{-@ foo :: Nat -> Nat @-}
foo :: Int -> Int
foo = go
  where
    {-@ go :: x:Nat -> Nat / [x] @-}
    go :: Int -> Int
    go 0 = 0
    go x = go ( x-1)