Liquid Haskell issues

LH.hs

{-@ LIQUID "--exact-data-con"                      @-}
{-@ LIQUID "--higherorder"                         @-}
{-@ LIQUID "--totality"                            @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}

module A where

import qualified Prelude
import           Prelude (Char, Int, Bool (..))
import Language.Haskell.Liquid.ProofCombinators

-- TODO: import Basics and Induction

{-@ data Peano [toNat] = O | S Peano @-}
data Peano = O | S Peano

{-@ measure toNat @-}
{-@ toNat :: Peano -> Nat @-}
toNat :: Peano -> Int
toNat O     = 0
toNat (S n) = 1 Prelude.+ toNat n

{-@ reflect plus @-}
plus :: Peano -> Peano -> Peano
plus O     n = n
plus (S m) n = S (plus m n)

{-@ safeEq :: x : a -> { y : a | x = y } -> a @-}
safeEq :: a -> a -> a
safeEq x y = x

{-@ data BBool = BTrue | BFalse @-}
data BBool = BTrue | BFalse

{-@ reflect negb @-}
negb :: BBool -> BBool
negb BTrue  = BFalse
negb BFalse = BTrue

{-@ reflect evenb @-}
evenb :: Peano -> BBool
evenb O         = BTrue
evenb (S O)     = BFalse
evenb (S (S n)) = evenb n

{-@ reflect nonzero @-}
nonzero :: Peano -> BBool
nonzero O = BFalse
nonzero _ = BTrue

{-@ test :: { plus (S O) (S O) = S (S O) } @-}
test = plus (S O) (S O)
   `safeEq` S (plus O (S O))
   `safeEq` S (S O)
   *** QED

{-@ thm' :: { x : Peano | toNat x > 0 }
         -> { y : Peano | toNat y > 0 }
         -> { toNat (plus x y) > 0 } @-}
thm' :: Peano -> Peano -> Proof
thm' (S O) _ = trivial
thm' _ (S O) = trivial
thm' (S x@(S _)) (S y@(S _)) = (thm' x y, trivial) *** QED

{-@ thm :: { x : Peano | nonzero x = BTrue }
        -> { y : Peano | nonzero y = BTrue }
        -> { nonzero (plus x y) = BTrue } @-}
thm :: Peano -> Peano -> Proof
thm (S O) _ = trivial
thm _ (S O) = trivial
thm (S x@(S _)) (S y@(S _)) = (thm x y, trivial) *** QED