Lazy pattern match causes program to become unsafe

[RyanGlScott]

LH accepts this program:

{-@ LIQUID "--higherorder"    @-}
{-@ LIQUID "--totality"       @-}
{-@ LIQUID "--exactdc"        @-}
module Eq where

import Language.Haskell.Liquid.ProofCombinators

{-@ data VerifiedEq a = VerifiedEq {
      eq :: a -> a -> Bool
    , refl :: x:a -> { v:() | eq x x }
    , sym :: x:a -> y:a -> { v:() | eq x y ==> eq y x }
    , trans :: x:a -> y:a -> z:a -> { v:() | eq x y && eq y z ==> eq x z }
    }
@-}
data VerifiedEq a = VerifiedEq {
    eq    :: a -> a -> Bool
  , refl  :: a -> Proof
  }

{-@ axiomatize eqContra @-}
eqContra :: (a -> a -> Bool)
         -> (b -> a)
         -> (b -> b -> Bool)
eqContra eqa g x y = eqa (g x) (g y)
{-# INLINE eqContra #-}

{-@ eqContraRefl :: eqa:(a -> a -> Bool) -> eqaRefl:(x:a -> { eqa x x })
                 -> g:(b -> a) -> x:b -> { eqContra eqa g x x }
@-}
eqContraRefl :: (a -> a -> Bool) -> (a -> Proof)
             -> (b -> a) -> b -> Proof
eqContraRefl eqa eqaRefl g x =
      eqContra eqa g x x
  ==. eqa (g x) (g x)
  ==. True ? eqaRefl (g x)
  *** QED

veqContra :: (b -> a) -> VerifiedEq a -> VerifiedEq b
veqContra g (VerifiedEq eqa eqaRefl) =
  VerifiedEq (eqContra eqa g) (eqContraRefl eqa eqaRefl g)

But if you change veqContra to use a lazy pattern match:

veqContra :: (b -> a) -> VerifiedEq a -> VerifiedEq b
veqContra g ~(VerifiedEq eqa eqaRefl) =
  VerifiedEq (eqContra eqa g) (eqContraRefl eqa eqaRefl g)

Then it becomes unsafe!

**** RESULT: UNSAFE ************************************************************

 /home/rgscott/Documents/Hacking/Haskell/verified-instances/generic-proofs/Eq.hs:40:49-55: Error: Liquid Type Mismatch

 40 |   VerifiedEq (eqContra eqa g) (eqContraRefl eqa eqaRefl g)
                                                      ^^^^^^^
   Inferred type
     VV : ()

   not a subtype of Required type
     VV : {VV : () | eqa ?a ?a}

   In Context
     ?a : a

[ranjitjhala]

The lazy pattern matching basically converts the above program into here I am writing wrapped "accessors" for eq and refl (namely getEq and getRefl).

The below program works (but read on)

{-@ LIQUID "--higherorder"    @-}
{-@ LIQUID "--totality"       @-}
{-@ LIQUID "--exactdc"        @-}

module Eq where

import Language.Haskell.Liquid.ProofCombinators

{-@ data VerifiedEq a = VerifiedEq {
      eq   :: a -> a -> Bool
    , refl :: x:a -> { eq x x }
    }
@-}
data VerifiedEq a = VerifiedEq {
    eq    :: a -> a -> Bool
  , refl  :: a -> Proof
  }

{-@ reflect eqContra @-}
eqContra :: (a -> a -> Bool)
         -> (b -> a)
         -> (b -> b -> Bool)
eqContra eqa g x y = eqa (g x) (g y)
{-# INLINE eqContra #-}

{-@ eqContraRefl :: eqa:(a -> a -> Bool) -> eqaRefl:(x:a -> { eqa x x })
                 -> g:(b -> a) -> x:b -> { eqContra eqa g x x }
@-}
eqContraRefl :: (a -> a -> Bool) -> (a -> Proof)
             -> (b -> a) -> b -> Proof
eqContraRefl eqa eqaRefl g x =
      eqContra eqa g x x
  ==. eqa (g x) (g x)
  ==. True ? eqaRefl (g x)
  *** QED

veqContra :: (b -> a) -> VerifiedEq a -> VerifiedEq b
veqContra g p = VerifiedEq (eqContra eqa g) (eqContraRefl eqa eqaRefl g)
  where
    eqa     = getEq   p
    eqaRefl = getRefl p

{-@ assume getEq :: p:VerifiedEq a -> {f:(a -> a -> Bool) | f = eq p} @-}
getEq :: VerifiedEq a -> (a -> a -> Bool)
getEq = eq

{-@ assume getRefl :: p:VerifiedEq a -> x:a -> { eq p x x } @-}
getRefl :: VerifiedEq a -> a -> Proof
getRefl = refl

@nikivazou unfortunately LH rejects the above signatures for the wrappers (hence the assume). Do we need to suitably strengthen the types of the fields? Or is there a flag for this already?

[ranjitjhala]

OK, the following works without any assume and I believe (looking at the GHC-CORE) that it is what the lazy pattern matching generates:

{-@ getEq :: p:VerifiedEq a -> {f:(a -> a -> Bool) | f = eq p} @-}
getEq :: VerifiedEq a -> (a -> a -> Bool)
getEq (VerifiedEq x y) = x

{-@ getRefl :: p:VerifiedEq a -> x:a -> { eq p x x } @-}
getRefl :: VerifiedEq a -> a -> Proof
getRefl (VerifiedEq x y) = y

@RyanGlScott can you check if the above works? That is, is it a suitable substitute for lazy-pattern-matching? Or is the generated code still non-terminating?

[vikraman]

I had to add a {-@ measure eq @-}, and I can confirm that it terminates at runtime. https://github.com/iu-parfunc/verified-instances/commit/16635ff14552aef402761fa3c59cc80a16d6c610

$ stack repl
λ> :m +GenericProofs.VerifiedEq GenericProofs.VerifiedEq.Instances GenericProofs.VerifiedEq.Examples.List
λ> eq (veqList veqInt) (Cons 2 Nil) (Cons 2 (Cons 3 Nil))
False
λ> eq (veqList veqInt) (Cons 2 Nil) (Cons 2 Nil)
True