T1025.hs

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

module T1025 where

import Language.Haskell.Liquid.ProofCombinators

{-@ data Either a b = Left a | Right b @-}

{-@ reflect eqEither @-}
eqEither :: (a -> a -> Bool) -> (b -> b -> Bool)
         -> Either a b -> Either a b -> Bool
eqEither eqA _   (Left  x) (Left  y) = eqA x y
eqEither _   eqB (Right x) (Right y) = eqB x y
eqEither _   _   (Left  _) (Right _) = False
eqEither _   _   (Right _) (Left  _) = False

{-@ eqEitherRefl :: eqA:(a -> a -> Bool) -> eqARefl:(x:a -> { eqA x x })
                 -> eqB:(b -> b -> Bool) -> eqBRefl:(y:b -> { eqB y y })
                 -> p:Either a b
                 -> { eqEither eqA eqB p p }
@-}
eqEitherRefl :: (a -> a -> Bool) -> (a -> Proof)
             -> (b -> b -> Bool) -> (b -> Proof)
             -> Either a b -> Proof
eqEitherRefl eqA eqARefl eqB _ p@(Left x) =
      eqEither eqA eqB p p
  === eqA x x
    ? eqARefl x
  === True 
  *** QED
eqEitherRefl eqA _ eqB eqBRefl p@(Right y) =
      eqEither eqA eqB p p
  === eqB y y
    ? eqBRefl y
  === True 
  *** QED