    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE Rank2Types #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    #if __GLASGOW_HASKELL__ >= 706
    {-# LANGUAGE PolyKinds #-}
    #endif
    #if __GLASGOW_HASKELL__ >= 800
    {-# LANGUAGE TypeInType #-}
    #endif

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Control.Lens.Equality
    -- Copyright   :  (C) 2012-16 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  provisional
    -- Portability :  Rank2Types
    --
    ----------------------------------------------------------------------------
    module Control.Lens.Equality
      (
      -- * Type Equality
        Equality, Equality'
      , AnEquality, AnEquality'
      , (:~:)(..)
      , runEq
      , substEq
      , mapEq
      , fromEq
      , simply
      -- * The Trivial Equality
      , simple
      -- * 'Iso'-like functions
      , equality
      , equality'
      , withEquality
      , underEquality
      , overEquality
      , fromLeibniz
      , fromLeibniz'
      , cloneEquality
      -- * Implementation Details
      , Identical(..)
      ) where

    import Control.Lens.Type
    import Data.Proxy (Proxy)
    import Data.Type.Equality ((:~:)(..))
    #if __GLASGOW_HASKELL__ >= 800
    import GHC.Exts (TYPE)
    import Data.Kind (Type)
    #endif

    #ifdef HLINT
    {-# ANN module "HLint: ignore Use id" #-}
    {-# ANN module "HLint: ignore Eta reduce" #-}
    #endif

    -- $setup
    -- >>> import Control.Lens

    #include "lens-common.h"

    -----------------------------------------------------------------------------
    -- Equality
    -----------------------------------------------------------------------------

    -- | Provides witness that @(s ~ a, b ~ t)@ holds.
    data Identical a b s t where
      Identical :: Identical a b a b

    -- | When you see this as an argument to a function, it expects an 'Equality'.
    #if __GLASGOW_HASKELL__ >= 706
    type AnEquality (s :: k1) (t :: k2) (a :: k1) (b :: k2) = Identical a (Proxy b) a (Proxy b) -> Identical a (Proxy b) s (Proxy t)
    #else
    type AnEquality s t a b = Identical a (Proxy b) a (Proxy b) -> Identical a (Proxy b) s (Proxy t)
    #endif

    -- | A 'Simple' 'AnEquality'.
    type AnEquality' s a = AnEquality s s a a

    -- | Extract a witness of type 'Equality'.
    runEq :: AnEquality s t a b -> Identical s t a b
    runEq :: AnEquality s t a b -> Identical s t a b
    runEq l :: AnEquality s t a b
    l = case AnEquality s t a b
    l Identical a (Proxy b) a (Proxy b)
    forall k k (a :: k) (b :: k). Identical a b a b
    Identical of Identical -> Identical s t a b
    forall k k (a :: k) (b :: k). Identical a b a b
    Identical
    {-# INLINE runEq #-}

    -- | Substituting types with 'Equality'.
    #if __GLASGOW_HASKELL__ >= 800
    substEq :: forall s t a b rep (r :: TYPE rep).
               AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    #else
    substEq :: AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    #endif
    substEq :: AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    substEq l :: AnEquality s t a b
    l = case AnEquality s t a b -> Identical s t a b
    forall k k (s :: k) (t :: k) (a :: k) (b :: k).
    AnEquality s t a b -> Identical s t a b
    runEq AnEquality s t a b
    l of
      Identical -> \r :: (s ~ a, t ~ b) => r
    r -> r
    (s ~ a, t ~ b) => r
    r
    {-# INLINE substEq #-}

    -- | We can use 'Equality' to do substitution into anything.
    #if __GLASGOW_HASKELL__ >= 800
    mapEq :: forall k1 k2 (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> Type) . AnEquality s t a b -> f s -> f a
    #elif __GLASGOW_HASKELL__ >= 706
    mapEq :: forall (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> *) . AnEquality s t a b -> f s -> f a
    #else
    mapEq :: AnEquality s t a b -> f s -> f a
    #endif
    mapEq :: AnEquality s t a b -> f s -> f a
    mapEq l :: AnEquality s t a b
    l r :: f s
    r = AnEquality s t a b -> ((s ~ a, t ~ b) => f a) -> f a
    forall k k (s :: k) (t :: k) (a :: k) (b :: k) r.
    AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    substEq AnEquality s t a b
    l f s
    (s ~ a, t ~ b) => f a
    r
    {-# INLINE mapEq #-}

    -- | 'Equality' is symmetric.
    fromEq :: AnEquality s t a b -> Equality b a t s
    fromEq :: AnEquality s t a b -> Equality b a t s
    fromEq l :: AnEquality s t a b
    l = AnEquality s t a b
    -> ((s ~ a, t ~ b) => p t (f s) -> p b (f a))
    -> p t (f s)
    -> p b (f a)
    forall k k (s :: k) (t :: k) (a :: k) (b :: k) r.
    AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    substEq AnEquality s t a b
    l (s ~ a, t ~ b) => p t (f s) -> p b (f a)
    forall a. a -> a
    id
    {-# INLINE fromEq #-}

    -- | This is an adverb that can be used to modify many other 'Lens' combinators to make them require
    -- simple lenses, simple traversals, simple prisms or simple isos as input.
    #if __GLASGOW_HASKELL__ >= 800
    simply :: forall p f s a rep (r :: TYPE rep).
      (Optic' p f s a -> r) -> Optic' p f s a -> r
    #else
    simply :: (Optic' p f s a -> r) -> Optic' p f s a -> r
    #endif
    simply :: (Optic' p f s a -> r) -> Optic' p f s a -> r
    simply = (Optic' p f s a -> r) -> Optic' p f s a -> r
    forall a. a -> a
    id
    {-# INLINE simply #-}

    -- | Composition with this isomorphism is occasionally useful when your 'Lens',
    -- 'Control.Lens.Traversal.Traversal' or 'Iso' has a constraint on an unused
    -- argument to force that argument to agree with the
    -- type of a used argument and avoid @ScopedTypeVariables@ or other ugliness.
    simple :: Equality' a a
    simple :: p a (f a) -> p a (f a)
    simple = p a (f a) -> p a (f a)
    forall a. a -> a
    id
    {-# INLINE simple #-}

    cloneEquality :: AnEquality s t a b -> Equality s t a b
    cloneEquality :: AnEquality s t a b -> Equality s t a b
    cloneEquality an :: AnEquality s t a b
    an = AnEquality s t a b
    -> ((s ~ a, t ~ b) => p a (f b) -> p s (f t))
    -> p a (f b)
    -> p s (f t)
    forall k k (s :: k) (t :: k) (a :: k) (b :: k) r.
    AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    substEq AnEquality s t a b
    an (s ~ a, t ~ b) => p a (f b) -> p s (f t)
    forall a. a -> a
    id
    {-# INLINE cloneEquality #-}

    -- | Construct an 'Equality' from explicit equality evidence.
    equality :: s :~: a -> b :~: t -> Equality s t a b
    equality :: (s :~: a) -> (b :~: t) -> Equality s t a b
    equality Refl Refl = p a (f b) -> p s (f t)
    forall a. a -> a
    id
    {-# INLINE equality #-}

    -- | A 'Simple' version of 'equality'
    equality' :: a :~: b -> Equality' a b
    equality' :: (a :~: b) -> Equality' a b
    equality' Refl = p b (f b) -> p a (f a)
    forall a. a -> a
    id
    {-# INLINE equality' #-}

    -- | Recover a "profunctor lens" form of equality. Reverses 'fromLeibniz'.
    overEquality :: AnEquality s t a b -> p a b -> p s t
    overEquality :: AnEquality s t a b -> p a b -> p s t
    overEquality an :: AnEquality s t a b
    an = AnEquality s t a b
    -> ((s ~ a, t ~ b) => p a b -> p s t) -> p a b -> p s t
    forall k k (s :: k) (t :: k) (a :: k) (b :: k) r.
    AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    substEq AnEquality s t a b
    an (s ~ a, t ~ b) => p a b -> p s t
    forall a. a -> a
    id
    {-# INLINE overEquality #-}

    -- | The opposite of working 'overEquality' is working 'underEquality'.
    underEquality :: AnEquality s t a b -> p t s -> p b a
    underEquality :: AnEquality s t a b -> p t s -> p b a
    underEquality an :: AnEquality s t a b
    an = AnEquality s t a b
    -> ((s ~ a, t ~ b) => p t s -> p b a) -> p t s -> p b a
    forall k k (s :: k) (t :: k) (a :: k) (b :: k) r.
    AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    substEq AnEquality s t a b
    an (s ~ a, t ~ b) => p t s -> p b a
    forall a. a -> a
    id
    {-# INLINE underEquality #-}

    -- | Convert a "profunctor lens" form of equality to an equality. Reverses
    -- 'overEquality'.
    --
    -- The type should be understood as
    --
    -- @fromLeibniz :: (forall p. p a b -> p s t) -> Equality s t a b@
    fromLeibniz :: (Identical a b a b -> Identical a b s t) -> Equality s t a b
    fromLeibniz :: (Identical a b a b -> Identical a b s t) -> Equality s t a b
    fromLeibniz f :: Identical a b a b -> Identical a b s t
    f = case Identical a b a b -> Identical a b s t
    f Identical a b a b
    forall k k (a :: k) (b :: k). Identical a b a b
    Identical of Identical -> p a (f b) -> p s (f t)
    forall a. a -> a
    id
    {-# INLINE fromLeibniz #-}

    -- | Convert Leibniz equality to equality. Reverses 'mapEq' in 'Simple' cases.
    --
    -- The type should be understood as
    --
    -- @fromLeibniz' :: (forall f. f s -> f a) -> Equality' s a@
    fromLeibniz' :: (s :~: s -> s :~: a) -> Equality' s a
    -- Note: even though its type signature mentions (:~:), this function works just
    -- fine in base versions before 4.7.0; it just requires a polymorphic argument!
    fromLeibniz' :: ((s :~: s) -> s :~: a) -> Equality' s a
    fromLeibniz' f :: (s :~: s) -> s :~: a
    f = case (s :~: s) -> s :~: a
    f s :~: s
    forall k (a :: k). a :~: a
    Refl of Refl -> p a (f a) -> p s (f s)
    forall a. a -> a
    id
    {-# INLINE fromLeibniz' #-}

    -- | A version of 'substEq' that provides explicit, rather than implicit,
    -- equality evidence.
    #if __GLASGOW_HASKELL__ >= 800
    withEquality :: forall s t a b rep (r :: TYPE rep).
       AnEquality s t a b -> (s :~: a -> b :~: t -> r) -> r
    #else
    withEquality :: forall s t a b r.
       AnEquality s t a b -> (s :~: a -> b :~: t -> r) -> r
    #endif
    withEquality :: AnEquality s t a b -> ((s :~: a) -> (b :~: t) -> r) -> r
    withEquality an :: AnEquality s t a b
    an = AnEquality s t a b
    -> ((s ~ a, t ~ b) => ((s :~: a) -> (b :~: t) -> r) -> r)
    -> ((s :~: a) -> (b :~: t) -> r)
    -> r
    forall k k (s :: k) (t :: k) (a :: k) (b :: k) r.
    AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
    substEq AnEquality s t a b
    an (\f :: (a :~: a) -> (b :~: b) -> r
    f -> (a :~: a) -> (b :~: b) -> r
    f a :~: a
    forall k (a :: k). a :~: a
    Refl b :~: b
    forall k (a :: k). a :~: a
    Refl)
    {-# INLINE withEquality #-}