{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Trustworthy #-}

#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE PolyKinds #-}
#else
{-# 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 ((:~:)(..))
import GHC.Exts (TYPE)
import Data.Kind (Type)

-- $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'.
type AnEquality s t a b = Identical a (Proxy b) a (Proxy b) -> Identical a (Proxy b) s (Proxy t)

-- | 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 :: 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 = 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 a (Proxy b) s (Proxy t)
Identical -> Identical s t s t
Identical s t a b
forall {k} {k} (a :: k) (b :: k). Identical a b a b
Identical
{-# INLINE runEq #-}

-- | Substituting types with 'Equality'.
substEq :: forall s t a b rep (r :: TYPE rep).
           AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
substEq :: 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 = 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 s t a b
Identical -> \(s ~ a, t ~ b) => r
r -> r
(s ~ a, t ~ b) => r
r
{-# INLINE substEq #-}

-- | We can use 'Equality' to do substitution into anything.
mapEq :: forall k1 k2 (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> Type) . AnEquality s t a b -> f s -> f a
mapEq :: forall k1 k2 (s :: k1) (t :: k2) (a :: k1) (b :: k2)
       (f :: k1 -> *).
AnEquality s t a b -> f s -> f a
mapEq AnEquality s t a b
l 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
f a
(s ~ a, t ~ b) => f a
r
{-# INLINE mapEq #-}

-- | 'Equality' is symmetric.
fromEq :: AnEquality s t a b -> Equality b a t s
fromEq :: forall {k2} {k1} (s :: k2) (t :: k1) (a :: k2) (b :: k1).
AnEquality s t a b -> Equality b a t s
fromEq 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 p t (f s) -> p t (f s)
p t (f s) -> p b (f a)
(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.
simply :: forall p f s a rep (r :: TYPE rep).
  (Optic' p f s a -> r) -> Optic' p f s a -> r
simply :: forall {k} {k1} (p :: k -> k1 -> *) (f :: k -> k1) (s :: k)
       (a :: k) r.
(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 :: forall {k2} (a :: k2) k3 (p :: k2 -> k3 -> *) (f :: k2 -> k3).
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 :: forall {k1} {k2} (s :: k1) (t :: k2) (a :: k1) (b :: k2).
AnEquality s t a b -> Equality s t a b
cloneEquality 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 p a (f b) -> p s (f t)
p a (f b) -> p a (f b)
(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 :: forall {k1} {k2} (s :: k1) (a :: k1) (b :: k2) (t :: k2).
(s :~: a) -> (b :~: t) -> Equality s t a b
equality s :~: a
Refl b :~: t
Refl = p a (f b) -> p s (f t)
p a (f b) -> p a (f b)
forall a. a -> a
id
{-# INLINE equality #-}

-- | A 'Simple' version of 'equality'
equality' :: a :~: b -> Equality' a b
equality' :: forall {k2} (a :: k2) (b :: k2). (a :~: b) -> Equality' a b
equality' a :~: b
Refl = p b (f b) -> p a (f a)
p b (f b) -> p b (f b)
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 :: forall {k} {k} (s :: k) (t :: k) (a :: k) (b :: k)
       (p :: k -> k -> *).
AnEquality s t a b -> p a b -> p s t
overEquality 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 p a b -> p s t
p a b -> p a b
(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 :: forall {k} {k} (s :: k) (t :: k) (a :: k) (b :: k)
       (p :: k -> k -> *).
AnEquality s t a b -> p t s -> p b a
underEquality 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 p t s -> p t s
p t s -> p b a
(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 :: forall {k1} {k2} (a :: k1) (b :: k2) (s :: k1) (t :: k2).
(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
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 a b s t
Identical -> p a (f b) -> p a (f b)
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
fromLeibniz' :: forall {k2} (s :: k2) (a :: k2).
((s :~: s) -> s :~: a) -> Equality' s a
fromLeibniz' (s :~: s) -> s :~: a
f = case (s :~: s) -> s :~: a
f s :~: s
forall {k} (a :: k). a :~: a
Refl of s :~: a
Refl -> p a (f a) -> p s (f s)
p a (f a) -> p a (f a)
forall a. a -> a
id
{-# INLINE fromLeibniz' #-}

-- | A version of 'substEq' that provides explicit, rather than implicit,
-- equality evidence.
withEquality :: forall s t a b rep (r :: TYPE rep).
   AnEquality s t a b -> (s :~: a -> b :~: t -> r) -> r
withEquality :: forall {k} {k} (s :: k) (t :: k) (a :: k) (b :: k) r.
AnEquality s t a b -> ((s :~: a) -> (b :~: t) -> r) -> r
withEquality 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 (\(s :~: a) -> (b :~: t) -> r
f -> (s :~: a) -> (b :~: t) -> r
f s :~: s
s :~: a
forall {k} (a :: k). a :~: a
Refl b :~: t
b :~: b
forall {k} (a :: k). a :~: a
Refl)
{-# INLINE withEquality #-}