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.

[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?

[jneira]

@ranjitjhala have been some progress in the liquid plugin? thanks!

[ranjitjhala]

Hi @jneira -- hmm not sure what the blockage was here, my impression was there was some glitch in the GHCi API, not so much the liquid-plugin? @kosmikus or @adinapoli do you recall?

[adinapoli]

Hi @jneira -- hmm not sure what the blockage was here, my impression was there was some glitch in the GHCi API, not so much the liquid-plugin? @kosmikus or @adinapoli do you recall?

Yes, I think this was some transient failure specific to your machine, IIRC. I have tried using the plugin both on Mac and Linux around the time it was first developed and it worked just fine. I guess we should try to give things a shot now and report back 😉

[MathiasSven]

I am not sure if this is the right issue to ask, but given that it seems that having it as a plugin seems to work, and I believe this relates to HLS-LH integration. Is HLS able to see liquidhaskell type definitions and treat them as the same for the purpose of code lenses? That is, disable type annotation suggestions when a liquidhaskell type has already been given:

Currently, it seems that while HLS passes the error produced by LH, it is otherwise transparent to its presence.

[michaelpj]

I agree, it's not clear what if anything we need to do here. It should mostly Just Work, since GHC knows about it.

[MathiasSven]

@michaelpj Yes, however, that issue persists, but it might not be a HLS issue... Maybe the culprit is the VSCode extension. I don't know much about LSPs, but my guess is that what happens is that the VSCode extension doesn't recognize that annotation, so it goes:

Hey HLS, I have this function which has no signature, could you provide me with the inferred one, so I can display it to the user.

But maybe it is:

Hey HLS, could you show me which functions lack an accompanying signature?
Now could you give me the inferred signature for this function which lacks a signature?

In which case the issue would be HLS.

[MathiasSven]

I had time to read a bit more of the source code of both, and see now that the VSCode extension is a very thin client, I believe the issue is in HLS. Could this part of code be relevant in this issue?

haskell-language-server/ghcide/src/Development/IDE/Plugin/TypeLenses.hs

Lines 308 to 317 in 10b5f3b

	gblBindingType :: Maybe HscEnv -> Maybe TcGblEnv -> IO (Maybe GlobalBindingTypeSigsResult)
	gblBindingType (Just hsc) (Just gblEnv) = do
	let exports = availsToNameSet $ tcg_exports gblEnv
	sigs = tcg_sigs gblEnv
	binds = collectHsBindsBinders $ tcg_binds gblEnv
	patSyns = tcg_patsyns gblEnv
	rdrEnv = tcg_rdr_env gblEnv
	showDoc = showDocRdrEnv hsc rdrEnv
	hasSig :: (Monad m) => Name -> m a -> m (Maybe a)
	hasSig name f = whenMaybe (name `elemNameSet` sigs) f

I am not sure on the specifics or whether this is relevant or not since I am unfamiliar with the codebase, but this seems promising... If the way HLS tells if something has a signature or not is by consulting the tcg_sigs NameSet from TcGblEnv, It might be that those annotations provided by LiquidHaskell are not in there.

[soulomoon]

properties :: Properties '[ 'PropertyKey "mode" (TEnum Mode)]
properties = emptyProperties
& defineEnumProperty #mode "Control how type lenses are shown"
[ (Always, "Always displays type lenses of global bindings")
, (Exported, "Only display type lenses of exported global bindings")
, (Diagnostics, "Follows error messages produced by GHC about missing signatures")
] Always

We have three options here
Which one you are using? @MathiasSven

[michaelpj]

If there's a specific issue with using HLS with GHC then maybe open a specific issue for that?

Type signature lenses work off GHC's diagnostic for missing type signatures, so is GHC giving you a warning for that?

[MathiasSven]

Apologies, after digging a little further I believe this to, in general, be for the better. HLS should show lenses for such functions (annotated by LH), since LH works on top of the inferred signatures. The behaviour I sought after would only be useful in the trivial cases. And as you said, GHC does indeed give warnings for such functions. A principled solution to this (if one were to be desired) would have to be implemented in the Liquid Haskell side.