content: {-@ LIQUID "--reflection"  @-}
  
  {-# LANGUAGE RankNTypes #-}
  
  module T1013A where
  
  import Prelude hiding (fmap)
  
  import Language.Haskell.Liquid.ProofCombinators
  
  {-@ reflect _compose @-}
  _compose :: (b -> c) -> (a -> b) -> a -> c
  _compose f g x = f (g x)
  {-# INLINE _compose #-}
  
  {-@ data Rec1 f p = Rec1 { unRec1 :: f p } @-}
  data Rec1 f p = Rec1 { unRec1 :: f p }
  
  {-@ data VerifiedFunctor m = VerifiedFunctor {
          fmap        :: forall a b. (a -> b) -> m a -> m b
        , fmapCompose :: forall a b c. f:(b -> c) -> g:(a -> b) -> x:m a
                      -> { fmap (_compose f g) x == _compose (fmap f) (fmap g) x }
        }
    @-}
  data VerifiedFunctor m = VerifiedFunctor {
      fmap        :: forall a b. (a -> b) -> m a -> m b
    , fmapCompose :: forall a b c. (b -> c) -> (a -> b) -> m a -> Proof
    }
  
  {-@ reflect fmapRec1 @-}
  fmapRec1 :: (forall a b. (a -> b) -> f a -> f b)
           -> (p -> q) -> Rec1 f p -> Rec1 f q
  fmapRec1 fmapF f (Rec1 fp) = Rec1 (fmapF f fp)
  
  {-@ fmapRec1Compose :: fmapF:(forall a b. (a -> b) -> f a -> f b)
                      -> fmapFId:(forall a b c. f':(b -> c) -> g':(a -> b) -> y:(f a) -> { fmapF (_compose f' g') y == _compose (fmapF f') (fmapF g') y })
                      -> f:(q -> r)
                      -> g:(p -> q)
                      -> x:Rec1 f p
                      -> { fmapRec1 fmapF (_compose f g) x == _compose (fmapRec1 fmapF f) (fmapRec1 fmapF g) x }
  @-}
  fmapRec1Compose :: (forall a b. (a -> b) -> f a -> f b)
                  -> (forall a b c. (b -> c) -> (a -> b) -> f a -> Proof)
                  -> (q -> r) -> (p -> q) -> Rec1 f p -> Proof
  fmapRec1Compose fmapF fmapFCompose f g r@(Rec1 fp)
    =   fmapRec1 fmapF (_compose f g) r
    === fmapRec1 fmapF (_compose f g) (Rec1 fp)
    === Rec1 (fmapF (_compose f g) fp)
        ? fmapFCompose f g fp
    === Rec1 (_compose (fmapF f) (fmapF g) fp) 
    === Rec1 (fmapF f (fmapF g fp))
    === fmapRec1 fmapF f (Rec1 (fmapF g fp))
    === fmapRec1 fmapF f (fmapRec1 fmapF g (Rec1 fp))
    === _compose (fmapRec1 fmapF f) (fmapRec1 fmapF g) (Rec1 fp)
    === _compose (fmapRec1 fmapF f) (fmapRec1 fmapF g) r
    *** QED
  
  vfunctorRec1 :: VerifiedFunctor f -> VerifiedFunctor (Rec1 f)
  vfunctorRec1 (VerifiedFunctor fmapF fmapFCompose)
    = VerifiedFunctor (fmapRec1        fmapF)
                      (fmapRec1Compose fmapF fmapFCompose)
  