Local Definitions Proposal

The Issue

Suppose we are working with the following Liquid Haskell code:

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

module Example where

import Language.Haskell.Liquid.ProofCombinators
import Prelude hiding (id)

{-@ reflect id @-}
id :: Int -> Int
id x = x

data Term where
    {-@ MkId :: Prop (Term id) @-}
    MkId :: Term
data TERM = Term (Int -> Int)

Parametrizing a type with some value is a common pattern in dependently typed programming languages.

We would like to prove statements that depend on these parameters.

{-@ doSomething :: f:_ -> Prop (Term f) -> {f = id} @-}
doSomething :: (a -> a) -> Term -> Proof
doSomething _ MkId = trivial

The above passes verification because the SMT solver can easily infer that if the term was constructed using the MkId constructor, then f = id.

However, in many cases, this is not enough because there are contexts where the SMT solver's knowledge is insufficient, but letting PLE unfold f can lead to verification. Take the following as an example:

{-@ doSomething' :: f:_ -> Prop (Term f) -> {f 42 = 42} @-}
doSomething' :: (a -> a) -> Term -> Proof
doSomething' _ MkId = trivial

Since for the SMT solver, f is still an opaque term (even though it knows that f = id), and PLE doesn't have any equation stating that f = id, the verification fails.

This issue could be solved by assessing that f must be equal to id when we are case-splitting and by informing PLE to expand f -> id. However, this expansion must be local. Suppose we add another constructor to Term; then f = id will not hold everywhere.

data Term where
    {-@ MkId :: Prop (Term id) @-}
    MkId :: Term
    {-@ MkAny :: f:_ -> Prop (Term f) @-}
    MkAny :: (Int -> Int) -> Term
data TERM = Term (Int -> Int)

Currently, the way Liquid Haskell communicates with Liquid Fixpoint, and by extension PLE, is through the define directive. For example, for id, it would generate the following definition:

define Example.id (x : Int) = {(x)}

The issue here is that this mechanism is global—we cannot specify that the rewrite must happen only in certain specific subconstraints.

Proposal

This proposal suggests the following steps:

• Introduce a mechanism to provide local definitions in the .fq file format. For example: define n f = {(Example.id)}, where n is the binding ID that contains the equation introducing the rewrite.

• Extend the PLE mechanism to account for these local rewrites.

• Modify Liquid Haskell to generate such rewrites during the constraint generation phase (Liquidhaskell-boot/src/Language/Haskell/Liquid/constraint/Generate.hs).