Annotations are ignored when comment is not closed with @-}

[nikivazou]

The following is SAFE

{-@ incr :: x:Int -> {v:Int | x < v } -}
incr :: Int -> Int 
incr x = x - 1

Because the annotation is not closing with @.
Maybe we need to create a warning in this case?

[ranjitjhala]

Whoa! Are the annotations even parsed? Actually I think not, because the parser literally sucks out text between {-@ ... @-} before doing any parsing, so if you don't close, then ... that text is just empty... :-/

[nikivazou]

Exactly, the annotations are not parsed.

I just got an email from a user wondering what is wrong with an annotation like this and took me a log time to spot the typo. So, maybe a warning could be helpful.

[ranjitjhala]

Hmm. Maybe tweak the "between" parser to warn if there is an "open" {-@ ? (should be easy...)

[gridaphobe]

GHC throws an error if you have an improperly closed pragma, e.g.

{-# LANGUAGE Blah -}

    /Users/gridaphobe/Source/liquid/haskell/src/Language/Haskell/Liquid/GHC/Interface.hs:1:14: error:
        Cannot parse LANGUAGE pragma
        Expecting comma-separated list of language options,
        each starting with a capital letter
          E.g. {-# LANGUAGE TemplateHaskell, GADTs #-}

I think this is a good idea (but we can do better with the error message)!