Improve error messages related to termination checking

[hexaglow]

liquidhaskell: fc26851c3401ba797fdb8cf3a2982d990f25035a from git, used as a GHC plugin liquid-fixpoint: 5501659 from git GHC: 8.10.2

liquid-base, liquid-vector and liquidhaskell listed as dependencies of the package.

This example from the book

loop :: Int -> Int -> a -> (Int -> a -> a) -> a
loop lo hi base f =  go base lo
  where
    go acc i
      | i < hi    = go (f i acc) (i + 1)
      | otherwise = acc

fails Liquid type-checking, producing the following error:

**** LIQUID: UNSAFE ************************************************************

/os/shared/matt/Documents/hs/liquid-tutorial/src/Lib.hs:54:34: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == i + 1}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | VV >= lo
                                 && VV < i
                                 && VV >= 0}
    .
    in the context
      lo : GHC.Types.Int

      i : {i : GHC.Types.Int | i >= lo}
   |
54 |       | i < hi    = go (f i acc) (i + 1)
   |                                  ^^^^^^^

Am I misunderstanding the book, or perhaps the book is out-of-date?

[ranjitjhala]

Hi,

This example requires the termination checker be disabled {-@ LIQUID --no-termination @-} somewhere in your source. Otherwise, you need to specify the termination metric which is a topic we have not yet covered.) The source file has this flag already set, but you should add it to yours. Alternately, you can specify the metric by specifying something like:

{-@ go :: _ -> i:_ -> _ / [ hi - i ] @-}

Let me add this to the text so you don't miss it.

Hope this helps!

• Ranjit.

On Mon, Sep 21, 2020 at 7:56 AM Matt Randell notifications@github.com wrote:

liquidhaskell: fc26851 https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/commit/fc26851c3401ba797fdb8cf3a2982d990f25035a__;!!Mih3wA!X_2Epro-KPL0xnF6PT18PNHtorgXCmvagWSh1_eOVd46b0P8cF92MtvUKyT5i0UH$ from git, used as a GHC plugin liquid-fixpoint: 5501659 https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/commit/5501659ccb6dbbd53a859cdda8e4a76d62fc31df__;!!Mih3wA!X_2Epro-KPL0xnF6PT18PNHtorgXCmvagWSh1_eOVd46b0P8cF92MtvUK3bUg-nI$ from git GHC: 8.10.2

liquid-base, liquid-vector and liquidhaskell listed as dependencies of the package.

This example from the book https://urldefense.com/v3/__http://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_04_Polymorphism.html__;!!Mih3wA!X_2Epro-KPL0xnF6PT18PNHtorgXCmvagWSh1_eOVd46b0P8cF92MtvUK9hEGqQ3$

loop :: Int -> Int -> a -> (Int -> a -> a) -> a loop lo hi base f = go base lo where go acc i | i < hi = go (f i acc) (i + 1) | otherwise = acc

fails Liquid type-checking, producing the following error:

LIQUID: UNSAFE ****

/os/shared/matt/Documents/hs/liquid-tutorial/src/Lib.hs:54:34: error: Liquid Type Mismatch . The inferred type VV : {v : GHC.Types.Int | v == i + 1} . is not a subtype of the required type VV : {VV : GHC.Types.Int | VV >= lo && VV < i && VV >= 0} . in the context lo : GHC.Types.Int

  i : {i : GHC.Types.Int | i >= lo}

| 54 | | i < hi = go (f i acc) (i + 1) | ^^^^^^^

Am I misunderstanding the book, or perhaps the book is out-of-date?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1760__;!!Mih3wA!X_2Epro-KPL0xnF6PT18PNHtorgXCmvagWSh1_eOVd46b0P8cF92MtvUK7GSqEyl$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OEIFRYUVV6WNHQI3WTSG5SSZANCNFSM4RUUJ6ZQ__;!!Mih3wA!X_2Epro-KPL0xnF6PT18PNHtorgXCmvagWSh1_eOVd46b0P8cF92MtvUK7F7MQen$ .

[plredmond]

@hexaglow I think you can disable termination checking for a single binding with the following annotation:

{-@ lazy myNontermDef @-}

So if the problem is with go then you'd pop that to the top level and add this annotation, perhaps? I don't know whether it's actually necessary to push it to the top level.

Link to specification reference "disabling termination checking"

[hexaglow]

I thought I had disabled termination checking - hence my confusion, but I had put -fplugin-opt=LiquidHakell:--no-termination instead of -fplugin-opt=LiquidHaskell:--no-termination (notice the typo!). Apparently specifying an option for a non-existent plugin doesn't cause an error.

It wasn't really clear to me from the diagnostic that it was caused by termination checking, which is why it took me a while to track this down. This might be difficult, but I would suggest it would be useful if Liquid could point out in error messages that disabling termination checking might be necessary.

[ranjitjhala]

Yes, you're right -- it would be great to mark those errors specifically, and the totality etc. errors too.

@nikivazou, I think this may not be too hard, maybe via the following strategy:

1. Extend fixpoint refinements with a constructor data Pred = ... | Tagged Text Pred
2. When we add refinements e.g. for totality or termination we can decorate them as Tagged msg p (instead of just p)
3. Extend the FP solver so that, given a constraint (i.e. p => And [q1...qn]) it splits it up into constraints [p => q1, ... ,p => qn]
4. Now, when constraint (subtyping) solving fails instead of telling the user that the WHOLE conjunction failed, we can narrow it down to the SPECIFIC goal that fails; if that goal is "tagged" then we can even use that as part of the error message.

[nikivazou]

Yes! This is a great idea! Following ghc the tag does not have to be Text, it can be some annotation that clearly signifies termination.

[kosmikus]

FWIW, I think it'd be good if GHC would warn about passing options to nonexisting plugins as well.

It might be somewhat easier to pass options via {-@ LIQUID "--option-name" @-} at the top of the file, unless of course you want to enable for a large number of files all at once.