Unbound symbol is$GHC.Types.[] for pattern match on empty list

[sertel]

Hi LiquidHaskellers,

I really like the idea of LH and would like to use it but I’m stuck on an error. Please excuse me if this error is only due to my minor knowledge about refinement types.

I tried the following program first in my local setup (config as described here: https://github.com/ucsd-progsys/lh-plugin-demo/blob/main/stack.yaml ) and then in your playground (http://goto.ucsd.edu:8090/index.html ):

module SimpleRefinements where
import Prelude hiding (NonEmpty, List, Text)
import Language.Haskell.Liquid.Prelude

import Data.List.NonEmpty
import Data.Text

data OutData
    = Direct Text
    | Dispatch (NonEmpty Text)

{-@ outLength :: OutData -> { v:Int | v > 0 } @-}
outLength :: OutData -> Int
outLength (Direct bnd) = 1
outLength (Dispatch os) = 
    case os of
        (b:|[]) -> 1
        (b0:|(b1:bs)) -> 1 + outLength (Dispatch (b1:|bs))

{-@ measure outLength @-}
{-@ data OutData [outLength] @-}

The error message that I receive is:

Bad Measure Specification
measure  SimpleRefinements.outLength
Unbound symbol is$GHC.Types.[] --- perhaps you meant: GHC.Types.[] ?

It seems to have problems pattern matching on the empty list not being able to resolve the symbol is$GHC.Types.[] which it uses in the conditional clause in the derived refinement type of the data constructor Dispatch. I have seen pattern matching on empty lists in many examples in the tutorial. So, is this me using the wrong imports?

Thanks a lot for your help.

[ranjitjhala]

Hmm I should really fix this issue - you need to add the --exact-data-cons flag, so the below works.

{-@ LIQUID "--exact-data-cons" @-}
module Demo.Bug where

import Prelude hiding (NonEmpty, List, Text)
import Data.List.NonEmpty

type Text = String
data OutData = Direct Text | Dispatch (NonEmpty Text)

{-@ measure outLength @-}
{-@ outLength :: OutData -> { v:Int | v > 0 } @-}
outLength :: OutData -> Int
outLength (Direct bnd) = 1
outLength (Dispatch os) = neSize os

{-@ measure neSize @-}
{-@ neSize :: l:NonEmpty a -> {v:Int | v > 0}  / [len (neList l)]  @-}
neSize :: NonEmpty a -> Int
neSize (b:|[]) = 1
neSize (b0:|(b1:bs))  = 1 + neSize (b1:|bs)

{-@ measure neList @-}
neList :: NonEmpty a -> [a]
neList (_:|l) = l

{-@ data OutData [outLength] @-}

[sertel]

Thanks a lot for your help! I guess the take-away is that I should avoid case statements in measures?

[ranjitjhala]

Not quite, see the discussion on measures here:

http://ucsd-progsys.github.io/liquidhaskell/specifications/

the real issue, which we need to fix, is to stop LH from yelling about the missing stuff for [] i.e. to switch on the exact-data-cons by default.

[ranjitjhala]

I think your original code would probably work fine if you just added that one flag, but still, each measure should have a single equation/case per data-constructor of the corresponding type.

[sertel]

Sadly, with my upgrade to the latest LH version (see #1794 ) the above solution that you proposed fails once more with the same type of error initially reported in this issue:

• Bad Measure Specification
measure  Ohua.Core.DFLang.Base.neSize
Unbound symbol GHC.Exts.toList --- perhaps you meant: GHC.Exts.$fIsList[] ?
• 
|
| {-@ measure neSize @-}
|             ^

[ranjitjhala]

Did you try to add the —exact-data-cons As suggested in the other issue?

[sertel]

You actually suggested it in this issue even ;) And yes, I did add this flag. In fact, I just copied your proposed solution into a .hs file.

I will create a small project tomorrow that contains the same setup and only this file just to isolate this. If it would help you in debugging this, I can share that with you.

[ranjitjhala]

Looking at your error it looks like you are defining a measure with the function GHC.Exts.toList -- which is not allowed.

A measure can only refer to other measures or definitions known to LH (not arbitrary haskell functions...)

On Mon, Nov 16, 2020 at 1:16 PM Sebastian notifications@github.com wrote:

You actually suggested it in this issue even ;) And yes, I did add this flag. In fact, I just copied your proposed solution into a .hs file.

I will create a small project tomorrow that contains the same setup and only this file just to isolate this. If it would help you in debugging this, I can share that with you.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1793*issuecomment-728334030__;Iw!!Mih3wA!VZpkDUmGvEk-2_S8lxLiNQNNhzxYw_iSnrXzwf0yv4CNghEvEzHJO3YO5nbxB0yS$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OHKULI26X6QZ4ZGDVDSQGJCJANCNFSM4TTCIF5Q__;!!Mih3wA!VZpkDUmGvEk-2_S8lxLiNQNNhzxYw_iSnrXzwf0yv4CNghEvEzHJO3YO5uVej8zJ$ .

[sertel]

I finally found the problem: I had the OverloadedLists language extension on by default. So this shows the error also at the playground:

{-@ LIQUID "--exact-data-cons" @-}
{-# LANGUAGE OverloadedLists #-}
module Demo.Bug where

import Prelude hiding (NonEmpty, List, Text)
import Data.List.NonEmpty

type Text = String
data OutData = Direct Text | Dispatch (NonEmpty Text)

{-@ measure outLength @-}
{-@ outLength :: OutData -> { v:Int | v > 0 } @-}
outLength :: OutData -> Int
outLength (Direct bnd) = 1
outLength (Dispatch os) = neSize os

{-@ measure neSize @-}
{-@ neSize :: l:NonEmpty a -> {v:Int | v > 0}  / [len (neList l)]  @-}
neSize :: NonEmpty a -> Int
neSize (b:|[]) = 1
neSize (b0:|(b1:bs))  = 1 + neSize (b1:|bs)

{-@ measure neList @-}
neList :: NonEmpty a -> [a]
neList (_:|l) = l

{-@ data OutData [outLength] @-}

Maybe it is a good idea to flag an error message on this language extension as well until these functions got lifted? (Although that would not have helped in my case because I had it in the default-extensions list of my stack configuration and as far as I understand LH only looks at source files -- which is totally fine at the moment.)