Liquid Haskell has a flag called --no-case-expand which can make verification of your code much faster, especially when your code is using ADTs with many alternatives. This flag says relax precision to get fast verification, thus may lead to rejecting safe code.

In this post, I explain how --no-case-expand works using a trivial example!

(Click here to demo)

28: 
29: module MeasuresAndCaseSplitting where

Measures

Let’s define a simple data type with three alternatives

40: data ABC = A | B | C 

and a measure that turns ABD into an integer

46: {-@ measure toInt @-}
47: toInt :: ABC -> Int 
48: x1:MeasuresAndCaseSplitting.ABC -> {VV : GHC.Types.Int | VV == MeasuresAndCaseSplitting.toInt x1}toInt A = 1 
49: toInt B = 2
50: toInt C = 3 

Though obvious to us, Liquid Haskell will fail to check that toInt of any ABC argument gives back a natural number. Or, the following call leads to a refinement type error.

59: {-@ unsafe :: x:ABC -> {o:() | 0 <= toInt x } @-}
60: unsafe     :: ABC -> () 
61: x1:MeasuresAndCaseSplitting.ABC -> {o : () | 0 <= MeasuresAndCaseSplitting.toInt x1}unsafe MeasuresAndCaseSplitting.ABCx   = ()

Why? By turning toInt into a measure, Liquid Haskell gives precise information to each data constructor of ABC. Thus it knows that toInt or A, B, and C is respectively 1, 2, and 3, by automatically generating the following types:

72: A :: {v:ABC | toInt v == 1 }
73: B :: {v:ABC | toInt v == 2 }
74: C :: {v:ABC | toInt v == 3 }

Thus, to get the toInt information one need to explicitly perform case analysis on an ABC argument. The following code is safe

82: {-@ safe :: x:ABC -> {o:() | 0 <= toInt x} @-}
83: safe     :: ABC -> ()
84: x1:MeasuresAndCaseSplitting.ABC -> {o : () | 0 <= MeasuresAndCaseSplitting.toInt x1}safe A   = () 
85: safe B   = () 
86: safe C   = () 

Liquid Haskell type check the above code because in the first case the body is checked under the assumption that the argument, call it x, is an A. Under this assumption, toInt x is indeed non negative. Yet, this is the case for the rest two alternatives, where x is either B or C. So, 0 <= toInt x holds for all the alternatives, because case analysis on x automatically reasons about the value of the measure toInt.

Now, what if I match the argument x only with A and provide a default body for the rest?

104: {-@ safeBut :: x:ABC -> {o:() | 0 <= toInt x} @-}
105: safeBut     :: ABC -> ()
106: x1:MeasuresAndCaseSplitting.ABC -> {o : () | 0 <= MeasuresAndCaseSplitting.toInt x1}safeBut A   = () 
107: safeBut _   = () 

Liquid Haskell knows that if the argument x is actually an A, then toInt x is not negative, but does not know the value of toInt for the default case.

But, by default Liquid Haskell will do the the case expansion of the default case for you and rewrite your code to match _ with all the possible cases. Thus, Liquid Haskell will internally rewrite safeBut as

119: {-@ safeButLH :: x:ABC -> {o:() | 0 <= toInt x} @-}
120: safeButLH     :: ABC -> ()
121: x1:MeasuresAndCaseSplitting.ABC -> {o : () | 0 <= MeasuresAndCaseSplitting.toInt x1}safeButLH A   = () 
122: safeButLH B   = () 
123: safeButLH C   = () 

With this rewrite Liquid Haskell gets precision! Thus, it has all the information it needs to prove safeBut as safe. Yet, it repeats the code of the default case, thus verification slows down.

In this example, we only have three case alternatives, so we only repeat the code two times with a minor slow down. In cases with many more alternatives repeating the code of the default case can kill the verification time.

For that reason, Liquid Haskell comes with the no-case-expand flag that deactivates this expansion of the default cases. With the no-case-expand flag on, the safeBut code will not type check and to fix it the user needs to perform the case expansion manually.

In short, the no-case-expand increases verification speed but reduces precision. Then it is up to the user to manually expand the default cases, as required, to restore all the precision required for the code to type check.