Haskell-language-server: 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 https://github.com/ucsd-progsys/liquidhaskell/commit/86f48a623b9a52ddbe07efc9949353518ea8185f ? 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.

[ranjitjhala]

I fixed the double-conversion thing -- LH doesn't depend on it now. So now I'm not sure what's killing the language server, it seems to keep spawning more processes ... I can post a screen shot if that helps?

[wz1000]

@ranjitjhala The output of running haskell-language-server /some/file/using/liquid.hs would be useful.

@kosmikus could you possibly share what you have so far? I've started work on my own LH plugin, but I'm primarily interested in taking advantage of the synthesis abilities of LH for the IDE.

[kosmikus]

@wz1000 https://github.com/kosmikus/haskell-language-server/tree/liquid-plugin This is based on @alanz 's plugin for haskell-ide-engine and totally unpolished so far.

[kosmikus]

@wz1000 So in particular, the only feature it adds is to use the annotations LH generates for giving refinement type signatures as part of hover. There's lot of cool other things that could in principle be done, including indeed synthesis.

[ranjitjhala]

Hi all, this gist shows the contents of the output pane -- AFAICT it downloads and builds the plugin just fine, but something is causing Server will restart. and after 5 tries it gives up...?

[ranjitjhala]

Here's a second log,

https://gist.github.com/ranjitjhala/d37fb858fd38ea9f8bdddc8a19840fec

that I got just now by firing up vscode on this haskell package (the hls branch)

https://github.com/ucsd-progsys/lh-plugin-demo/tree/hls

AFAICT it builds LH but then something is causing the process to get killed...

[ranjitjhala]

As suggested I ran the server locally:

rjhala@khao-soi ~/r/lh-demo-hls (hls)> /Users/rjhala/Library/Application\ Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 src/Demo/Bug.hs --debug
haskell-language-server version: 0.5.1.0 (GHC: 8.10.2) (PATH: /Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2) (GIT hash: e3fe0e7546aa91e44cc56cfe8ec078a026cf533a)
(haskell-language-server)Ghcide setup tester in /Users/rjhala/research/lh-demo-hls.
Report bugs at https://github.com/haskell/haskell-language-server/issues

Tool versions found on the $PATH
cabal:      3.2.0.0
stack:      2.5.1
ghc:        8.10.2


Step 1/4: Finding files to test in /Users/rjhala/research/lh-demo-hls
Found 1 files

Step 2/4: Looking for hie.yaml files that control setup
Found 1 cradle

Step 3/4: Initializing the IDE

Step 4/4: Type checking the files
[INFO] Consulting the cradle for "src/Demo/Bug.hs"
NotShowMessage (NotificationMessage {_jsonrpc = "2.0", _method = WindowShowMessage, _params = ShowMessageParams {_xtype = MtWarning, _message = "No [cradle](https://github.com/mpickering/hie-bios#hie-bios) found for src/Demo/Bug.hs.\n Proceeding with [implicit cradle](https://hackage.haskell.org/package/implicit-hie)"}})
Output from setting up the cradle Cradle {cradleRootDir = "/Users/rjhala/research/lh-demo-hls", cradleOptsProg = CradleAction: Cabal}
> Resolving dependencies...
> Build profile: -w ghc-8.10.2 -O1
> In order, the following will be built (use -v for more details):
>  - liquid-fixpoint-0.8.10.2.1 (lib) (configuration changed)
>  - liquidhaskell-0.8.10.2.1 (lib) (configuration changed)
>  - liquid-ghc-prim-0.6.1 (lib:liquid-ghc-prim) (configuration changed)
>  - liquid-base-4.14.1.0 (lib:liquid-base) (configuration changed)
>  - liquid-vector-0.12.1.2 (lib:liquid-vector) (configuration changed)
>  - liquid-prelude-0.8.10.2 (lib:liquid-prelude) (configuration changed)
>  - liquid-containers-0.6.2.1 (lib:liquid-containers) (configuration changed)
>  - lh-plugin-demo-0.1.0.0 (lib) (configuration changed)
> Configuring library for liquid-fixpoint-0.8.10.2.1..
> Preprocessing library for liquid-fixpoint-0.8.10.2.1..
> Building library for liquid-fixpoint-0.8.10.2.1..
> Configuring library for liquidhaskell-0.8.10.2.1..
> Preprocessing library for liquidhaskell-0.8.10.2.1..
> Building library for liquidhaskell-0.8.10.2.1..
> Configuring liquid-ghc-prim-0.6.1...
> Preprocessing library for liquid-ghc-prim-0.6.1..
> Building library for liquid-ghc-prim-0.6.1..
> Configuring liquid-base-4.14.1.0...
> Preprocessing library for liquid-base-4.14.1.0..
> Building library for liquid-base-4.14.1.0..
> Configuring liquid-containers-0.6.2.1...
> Configuring liquid-prelude-0.8.10.2...
> Configuring liquid-vector-0.12.1.2...
> Preprocessing library for liquid-prelude-0.8.10.2..
> Building library for liquid-prelude-0.8.10.2..
> Preprocessing library for liquid-containers-0.6.2.1..
> Building library for liquid-containers-0.6.2.1..
> Preprocessing library for liquid-vector-0.12.1.2..
> Building library for liquid-vector-0.12.1.2..
> Configuring library for lh-plugin-demo-0.1.0.0..
> Preprocessing library for lh-plugin-demo-0.1.0.0..
[INFO] Using interface files cache dir: /Users/rjhala/.cache/ghcide/lh-plugin-demo-0.1.0.0-inplace-59e26a4d4e468f0875d43f4c51948f50cf65b6b6
[INFO] Making new HscEnv[lh-plugin-demo-0.1.0.0-inplace]
fish: '/Users/rjhala/Library/Applicati…' terminated by signal SIGSEGV (Address boundary error)

so looks like a segfault?