Full-feature liquid haskell plugin

[alanz]

There is now a liquid haskell GHC typechecker plugin. This has some level of support in ghcide, but needs first class hover etc support.

Ping @kosmikus . More detail/requirements please

cc @ranjitjhala

[alanz]

https://hackage.haskell.org/package/liquidhaskell-0.8.10.1/docs/Language-Haskell-Liquid-GHC-Plugin-Tutorial.html

[jneira]

Afaik liquid haskell functionality will be included in the ghc itself. If it needs some adaptation in the ide i guess it should be in ghcide, as linear type errors will be reported directly by ghc. So a dedicated plugin only would be needed to support older ghc versions.

Imo we should only invest in the ghc builtin functionality.

[Anrock]

Afaik liquid haskell functionality will be included in the ghc itself.

Can you share source on that? I've only seen liquid haskell ghc plugin.

[fendor]

https://well-typed.com/blog/2020/08/implementing-a-ghc-plugin-for-liquid-haskell/

[jneira]

@Anrock thanks for the correction, i had assimilated incorrectly refinement and linear types (but the former subsumes the latter? or did i imagine its relation entirely?)

[Anrock]

@jneira afaik refinement and linear types are unrelated in this sense. But I may be wrong.

[ndmitchell]

Linear types is a type extension in GHC. LiquidHaskell is a plugin static checker, but one that wires itself quite closely to the internals of GHC. They're quite different, although can express some of the same properties (but not that many).

[ranjitjhala]

Yes, LH is a plugin, and not part of GHC as such.

Not sure this is the right place -- but I haven't been able to get the LH plugin to work with the
VSCODE language server on my mac :-(

According to @kosmikus this is a macos issue because he is able to get the basic support
working fine on his linux box.

Currently I work around this by:

1. defining two cabal components -- with and without the LH-plugin
2. tell the hie.yaml cradle to use the plugin-less component
3. run a separate ghcid using plugin-component to get LH-errors.

Any suggestions on how I can help provide more information as to why
the language-server and LH-plugin aren't playing nice?

[wz1000]

@ranjitjhala have you started encountering this after ucsd-progsys/liquidhaskell@86f48a6 ? Because we always set Opt_Haddock while parsing to get documentation for the hover tooltips.

[kosmikus]

It's quite possible that I haven't checked after we merged the Haddock fix. I will try.

Also, just to clarify, @ranjitjhala: I'm by no means certain this is a MacOS issue. You've been observing double-conversion-related duplicate symbol errors in your logs, and I've been saying that I recall having seen this on MacOS once before, but never on Linux.

Regarding the original purpose of this issue (sorry, I had not noticed this issue): I have created a proof-of-concept "full" LH plugin for haskell-language-server. It's proof-of-concept right now primarily because it reads annotation info from the place LH naturally writes it to, which is in a .liquid subdirectory underneath where the source file is located. This is not good for IDE use, because the IDE is working with temporary files. So LH should make the location where to write the annotation info configurable. I have to add that.

Apart from this issue, the plugin is working. I hope I'll be able to submit a PR at some point.