Re: Treatment of unknown pragmas

Another option could be to introduce a lighter ANN that doesn’t actually embed anything into the module, instead just making the annotations available to plugins and API users during compilation of that particular module. It could also be restricted to string annotations to avoid invoking the type checker. IIRC HLint’s annotations are already strings, so this wouldn’t be a big deal. What is GHC providing in this case? Parsing the ANN pragmas (not the contents) and attaching them to the relevant Id, which is still a substantial benefit in my opinion. We have some code in LiquidHaskell that does this for local let-binders, and it’s a horrible hack; I’d much rather have GHC do it for us. Sent from my iPhone

On Oct 16, 2018, at 18:00, Ben Gamari wrote:

Brandon Allbery writes:

...

The problem with ANN is it's part of the plugins API, and as such does things like compiling the expression into the program in case a plugin generates code using its value, plus things like recompilation checking end up assuming plugins are in use and doing extra checking. Using it as a compile-time pragma is actually fairly weird from that standpoint.

True. That being said, I wonder if we solve most of these issues by simply type-checking ANNs lazily. That is, just forkM ANNs during typechecking. This would mean that the user wouldn't see an error if the expression contained inside is invalid. On the other hand, the cost of ANNs would decrease significantly and plugins which use them would continue to work unmodified. Strict typechecking behavior could be enabled via a flag.

Cheers,

- Ben