[plugin] Undeclared type-variable error not properly reported for GHC to render as a compilation error

[plredmond]

In this example Bool is typo'd to bool, which is an undeclared/out-of-scope type variable. LH correctly identifies this error, but doesn't report it properly when LH is used as a GHC plugin. As a result, third party tools which integrate with GHC cannot detect the error condition. In slack @ranjitjhala said, "we should trap these too" and suggested @adinapoli.

{-@ bad :: {v:bool | v} @-}
bad = False

Expected behavior:

• Error is reported via GHC in a way that third-party programs (eg. GHCID) can detect.

Actual behavior:

• Error isn't reported via GHC in a way that third-party programs can detect.

---

Versions in use:

• liquidhaskell@26cad4f, liquid-fixpoint@a4e303b

[plredmond]

Here's another example of this sort of problem, though I don't know whether this generates the exact same kind of error as the first:

ax1 :: Integral a => a -> Bool
{-@ ax1 :: Int -> TRUE @-}
ax1 x = x < x + 1

This shows a human-readable "does not refine Haskell type" error when you build, but third-party tools like GHCID cannot see the error.

[plredmond]

Here's a third example. This produces a "multiple specifications for .." error when you build, but third party tools like GHCID cannot see the error.

{-@ i7 :: { i : Int | i == 6 } @-}
{-@ i7 :: { i : Int | i >= 0 } @-}
{-@ i7 :: { i : Int | i <= 10 } @-}
{-@ i7 :: { i : Int | i >= 0 && i <= 10 } @-}
{-@ i7 :: Int @-}
i7 :: Int
i7 = 6

This example is actually lifted directly from a tutorial linked from the LiquidHaskell homepage, so it's a little strange that it causes an error.

[adinapoli]

@plredmond Thanks for taking the time to write this ticket!

@plredmond @ranjitjhala I confess I haven't look too deeply into this issue, but having spent a fair amount of time on LiquidHaskell's internals, I'll have a guess: I think the culprit is that not all (parsing, or otherwise) errors are correctly routed through the error-handling mechanism we put in place for the plugin, which uses the GHC API to log any warning or error so that tools like ghcid and ghcide could correctly interpret it.

Part of the problem is that the parser's code has a bit of rough edges (but luckily we have @kosmikus 's patch which will fix that) but also that some functions throws exceptions from pure code (see for example extractSpecComment).

I would suggest that if the fix is easy in this case, we go for it (and I will take a look later today) but if we find like we are just hitting the tip of the iceberg, perhaps it would have more sense to wait for @kosmikus 's patch to be merged and then perhaps redesign the error-handling, if not from the ground up in a way that prevents all the different permutations of these errors to crop up?

[adinapoli]

I have reproduced the first example and indeed there are two things going wrong here:

1. The parser should arguably catch this as a parsing error, so that we fail preemptively;
2. In the current codebase, this misbehave due to the fact plugHoles_old throws an exception (from pure code).

Ditto for the second and third example, with exceptions being thrown in different parts of the codebase. I wonder if we could jerry-rig this for now by using try and evaluate in the plugin for now, before venturing in a more pervasive refactoring.

[ranjitjhala]

Your plan sounds good to me @adinapoli Thanks!!

On Tue, Jul 21, 2020 at 2:21 AM Alfredo Di Napoli notifications@github.com wrote:

I have reproduced the first example and indeed there are two things going wrong here:

1. The parser should arguably catch this as a parsing error, so that we fail preemptively;
2. In the current codebase, this misbehave due to the fact plugHoles_old throws an exception (from pure code).

Ditto for the second and third example, with exceptions being thrown in different parts of the codebase. I wonder if we could jerry-rig this for now by using try and evaluate in the plugin for now, before venturing in a more pervasive refactoring.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1711*issuecomment-661741862__;Iw!!Mih3wA!UJX_hjxK7-3ToScBIADbSFkn3xW2T6gdnUwCSbHh0F5WZ2Q-pZkQ912O1TJxSLnI$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OHFQ5DYQP3A7B4AWRTR4VM2TANCNFSM4PC3R2VA__;!!Mih3wA!UJX_hjxK7-3ToScBIADbSFkn3xW2T6gdnUwCSbHh0F5WZ2Q-pZkQ912O1Q9nnvdz$ .

[plredmond]

@adinapoli FYI there's another instance of this bug in #1758, example (2).