content: {-@ LIQUID "--reflection" @-}
  {-@ LIQUID "--aux-inline" @-}
  {-@ LIQUID "--ple" @-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  module Data.Maybe.Functor where
  import           Prelude                 hiding ( Functor(..)
                                                  , Applicative(..)
                                                  , Monad(..)
                                                  , Foldable(..)
                                                  , Maybe(..)
                                                  , Monoid(..)
                                                  , Semigroup(..)
                                                  , Either(..)
                                                  , id
                                                  , flip
                                                  , const
                                                  , apply
                                                  )
  import Liquid.ProofCombinators
  import Data.Function
  import Data.Maybe hiding (maybe)
  import Data.Functor.Classes
  
  instance Functor Maybe where
    fmap _ Nothing = Nothing
    fmap f (Just x) = Just (f x)
    _ <$ Nothing = Nothing
    x <$ (Just _) = Just x
  
  instance VFunctor Maybe where
      lawFunctorId Nothing = ()
      lawFunctorId (Just _) = ()
      lawFunctorComposition f g Nothing = ()
      lawFunctorComposition f g (Just x) = ()
  
  instance Applicative Maybe where
    pure = Just
    ap Nothing _ = Nothing
    ap _ Nothing = Nothing
    ap (Just f) (Just x) = Just (f x)
    liftA2 f (Just a) (Just b) = Just (f a b)
    liftA2 f _       _       = Nothing
    a1 *> a2 = ap (id <$ a1) a2
    a1 <* a2 = liftA2 const a1 a2
  
  instance VApplicative Maybe where
    lawApplicativeId Nothing = ()
    lawApplicativeId (Just x) = ap (pure id) (Just x) `cast` ()
    lawApplicativeComposition (Just f) (Just g) (Just x) = ()
    lawApplicativeComposition _ _ _ = ()
    lawApplicativeHomomorphism f x (Just y) = ()
    lawApplicativeHomomorphism f x Nothing = ()
    lawApplicativeInterchange Nothing _ = ()
    lawApplicativeInterchange (Just f) _ = ()
  
  
  instance Monad Maybe where
    bind Nothing _ = Nothing
    bind (Just x) f = f x
    return = Just
    mseq _ (Just x) = Just x
    mseq _ Nothing = Nothing
  
  instance VMonad Maybe where
    lawMonad1 x f = ()
    lawMonad2 Nothing = ()
    lawMonad2 (Just x) = ()
    lawMonad3 Nothing f g h = ()
    lawMonad3 (Just x) f g h = h x `cast` ()
    lawMonadReturn _ _ = ()
  