content: {-# LANGUAGE RankNTypes      #-}
  {-# LANGUAGE GADTs           #-}
  {-# LANGUAGE KindSignatures  #-}
  
  {-@ LIQUID "--reflection"  @-} 
  {-@ LIQUID "--ple"         @-}
  {-@ LIQUID "--fast"        @-}
  
  module T1660 where
  
  import Language.Haskell.Liquid.ProofCombinators
  import Prelude hiding (id, fmap)
  
  {-@ measure eqT :: a -> a -> Bool @-}
  {-@ type EqRT a E1 E2 = {v:EqT a | eqT E1 E2} @-}
  
  data EqT  :: * -> *  where 
     EqSMT  :: Eq a => a -> a -> () -> EqT a 
     EqFun  :: (a -> b) -> (a -> b) -> (a -> EqT b) -> EqT (a -> b)
  
  {-@ data EqT  :: * -> *  where 
         EqSMT  :: Eq a => x:a -> y:a -> {v:() | x == y} -> EqRT a {x} {y}
         EqFun  :: ff:(a -> b) -> gg:(a -> b) -> (x:a -> {v:EqT b | eqT (ff x) (gg x)}) -> EqRT (a -> b) {ff} {gg}
  @-}   
  
  
  type Reader a b = a -> b
  
  
  
  functorLaw_identity :: Eq a => EqT (Reader r a -> Reader r a)
  {-@ functorLaw_identity :: Eq a -> EqRT (Reader r a -> Reader r a) (fmap id) id @-}
  functorLaw_identity =
    EqFun (fmap id) id
    (\r -> EqFun (fmap id r) (id r)
      (\a -> EqSMT (fmap id r a) (id r a? lemmaId r a) ()))
  
  {-@ reflect id @-}
  id :: a -> a 
  id x = x
  
  {-@ reflect fmap @-}
  fmap :: (a -> b) -> Reader r a -> Reader r b
  fmap fab fra = \r -> fab (fra r)
  
  lemmaId :: Eq b => (a -> b) -> a -> ()
  {-@ lemmaId :: f:(a -> b) -> x:a -> {id f x = id (f x) } @-}
  lemmaId _ _ = ()
  