Deriving false is possible with termination checking enabled

[hetzenmat]

In the code below, all functions are shown terminating and can be reflected, but one can derive false.
Is this expected behavior?

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}

module A where

data L a = LNil | LCons a (L a)

{-@ reflect infList @-}
{-@ infList :: L a -> Bool @-}
infList :: L a -> Bool
infList LNil = False
infList (LCons _ t) = infList t

{-@ reflect g @-}
{-@ g :: {l:L () | infList l} -> {r:Bool | r && (not r)} @-}
g :: L () -> Bool
g (LCons () r) = g r

I tested this code with the latest git version of LH as well as the online Demo.

[facundominguez]

👋 Hello @hetzenmat. The specification of g is essentially equivalent to

{-@ g :: {l:L () | false } -> {r:Bool | false } @-}

I think it is expected that you can prove false from false.

[ranjitjhala]

To add to @facundominguez 's observation above -- LH will not let you "call" the function g as it's precondition is false for any (finite) list you give it...

[hetzenmat]

Thank you for the fast reply.
I crafted this example in such a way that one gets no warning if false could be proved.
If I replace r && (not r) by false, a warning is generated.

I guess with an additional check even for my example a warning can be generated, i.e., check if the refinement is of the form P && (not P) for some expression P.

[AlecsFerra]

I think is more of a bug to warn the user here, as we are expected to prove false in this context