# Measures and Case Splitting

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!

## 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.

Niki Vazou
2018-02-23