{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK not-home #-}
module Optics.Internal.Optic
( Optic(..)
, Optic'
, Optic_
, Optic__
, castOptic
, (%)
, (%%)
, (%&)
, IsProxy(..)
, LabelOptic(..)
, LabelOptic'
, module Optics.Internal.Optic.Subtyping
, module Optics.Internal.Optic.Types
, module Optics.Internal.Optic.TypeLevel
) where
import Data.Function ((&))
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import Data.Type.Equality
import GHC.OverloadedLabels
import GHC.TypeLits
import Data.Profunctor.Indexed
import Optics.Internal.Optic.Subtyping
import Optics.Internal.Optic.TypeLevel
import Optics.Internal.Optic.Types
import Unsafe.Coerce (unsafeCoerce)
newtype Optic (k :: OpticKind) (is :: IxList) s t a b = Optic
{ Optic k is s t a b
-> forall (p :: * -> * -> * -> *) i.
(Profunctor p, Constraints k p) =>
Optic__ p i (Curry is i) s t a b
getOptic :: forall p i. Profunctor p
=> Optic_ k p i (Curry is i) s t a b
}
type Optic' k is s a = Optic k is s s a a
type Optic_ k p i j s t a b = Constraints k p => Optic__ p i j s t a b
type Optic__ p i j s t a b = p i a b -> p j s t
data IsProxy (k :: Type) (l :: Type) (p :: Type -> Type -> Type -> Type) =
IsProxy
castOptic
:: forall destKind srcKind is s t a b
. Is srcKind destKind
=> Optic srcKind is s t a b
-> Optic destKind is s t a b
castOptic :: Optic srcKind is s t a b -> Optic destKind is s t a b
castOptic (Optic o :: forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ srcKind p i (Curry is i) s t a b
o) = (forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ destKind p i (Curry is i) s t a b)
-> Optic destKind is s t a b
forall k (is :: IxList) s t a b.
(forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ k p i (Curry is i) s t a b)
-> Optic k is s t a b
Optic (Optic_ srcKind p i (Curry is i) s t a b
-> Optic_ destKind p i (Curry is i) s t a b
forall (p :: * -> * -> * -> *) i.
Optic_ srcKind p i (Curry is i) s t a b
-> Optic_ destKind p i (Curry is i) s t a b
implies' Optic_ srcKind p i (Curry is i) s t a b
forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ srcKind p i (Curry is i) s t a b
o)
where
implies'
:: forall p i
. Optic_ srcKind p i (Curry is i) s t a b
-> Optic_ destKind p i (Curry is i) s t a b
implies' :: Optic_ srcKind p i (Curry is i) s t a b
-> Optic_ destKind p i (Curry is i) s t a b
implies' x :: Optic_ srcKind p i (Curry is i) s t a b
x = IsProxy srcKind destKind p
-> Optic_ srcKind p i (Curry is i) s t a b
-> Optic_ destKind p i (Curry is i) s t a b
forall k l (proxy :: * -> * -> (* -> * -> * -> *) -> *)
(p :: * -> * -> * -> *) r.
Is k l =>
proxy k l p -> (Constraints k p => r) -> Constraints l p => r
implies (IsProxy srcKind destKind p
forall k l (p :: * -> * -> * -> *). IsProxy k l p
IsProxy :: IsProxy srcKind destKind p) Optic_ srcKind p i (Curry is i) s t a b
x
{-# INLINE castOptic #-}
infixl 9 %
(%) :: (Is k m, Is l m, m ~ Join k l, ks ~ Append is js)
=> Optic k is s t u v
-> Optic l js u v a b
-> Optic m ks s t a b
o :: Optic k is s t u v
o % :: Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% o' :: Optic l js u v a b
o' = Optic k is s t u v -> Optic m is s t u v
forall destKind srcKind (is :: IxList) s t a b.
Is srcKind destKind =>
Optic srcKind is s t a b -> Optic destKind is s t a b
castOptic Optic k is s t u v
o Optic m is s t u v -> Optic m js u v a b -> Optic m ks s t a b
forall k (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a b.
(ks ~ Append is js) =>
Optic k is s t u v -> Optic k js u v a b -> Optic k ks s t a b
%% Optic l js u v a b -> Optic m js u v a b
forall destKind srcKind (is :: IxList) s t a b.
Is srcKind destKind =>
Optic srcKind is s t a b -> Optic destKind is s t a b
castOptic Optic l js u v a b
o'
{-# INLINE (%) #-}
infixl 9 %%
(%%) :: forall k is js ks s t u v a b. ks ~ Append is js
=> Optic k is s t u v
-> Optic k js u v a b
-> Optic k ks s t a b
Optic o :: forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ k p i (Curry is i) s t u v
o %% :: Optic k is s t u v -> Optic k js u v a b -> Optic k ks s t a b
%% Optic o' :: forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ k p i (Curry js i) u v a b
o' = (forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ k p i (Curry ks i) s t a b)
-> Optic k ks s t a b
forall k (is :: IxList) s t a b.
(forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ k p i (Curry is i) s t a b)
-> Optic k is s t a b
Optic forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ k p i (Curry ks i) s t a b
oo
where
oo :: forall p i. Profunctor p => Optic_ k p i (Curry ks i) s t a b
oo :: Optic__ p i (Curry ks i) s t a b
oo = (Optic_ k p i (Curry is (Curry js i)) s t a b
-> Constraints k p => Optic__ p i (Curry ks i) s t a b
forall a b. a -> b
unsafeCoerce
:: Optic_ k p i (Curry is (Curry js i)) s t a b
-> Optic_ k p i (Curry ks i ) s t a b)
(Optic__ p (Curry js i) (Curry is (Curry js i)) s t u v
forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ k p i (Curry is i) s t u v
o Optic__ p (Curry js i) (Curry is (Curry js i)) s t u v
-> (p i a b -> p (Curry js i) u v)
-> p i a b
-> p (Curry is (Curry js i)) s t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p i a b -> p (Curry js i) u v
forall (p :: * -> * -> * -> *) i.
Profunctor p =>
Optic_ k p i (Curry js i) u v a b
o')
{-# INLINE (%%) #-}
infixl 9 %&
(%&) :: Optic k is s t a b
-> (Optic k is s t a b -> Optic l js s' t' a' b')
-> Optic l js s' t' a' b'
%& :: Optic k is s t a b
-> (Optic k is s t a b -> Optic l js s' t' a' b')
-> Optic l js s' t' a' b'
(%&) = Optic k is s t a b
-> (Optic k is s t a b -> Optic l js s' t' a' b')
-> Optic l js s' t' a' b'
forall a b. a -> (a -> b) -> b
(&)
{-# INLINE (%&) #-}
class Append xs ys ~ zs => AppendProof (xs :: [Type]) (ys :: [Type]) (zs :: [Type])
| xs ys -> zs, zs xs -> ys where
appendProof :: Proxy i -> Curry xs (Curry ys i) :~: Curry zs i
instance ys ~ zs => AppendProof '[] ys zs where
appendProof :: Proxy i -> Curry '[] (Curry ys i) :~: Curry zs i
appendProof _ = Curry '[] (Curry ys i) :~: Curry zs i
forall k (a :: k). a :~: a
Refl
instance
(Append (x : xs) ys ~ (x : zs), AppendProof xs ys zs
) => AppendProof (x ': xs) ys (x ': zs) where
appendProof
:: forall i. Proxy i
-> Curry (x ': xs) (Curry ys i) :~: Curry (x ': zs) i
appendProof :: Proxy i -> Curry (x : xs) (Curry ys i) :~: Curry (x : zs) i
appendProof i :: Proxy i
i = case Proxy i -> Curry xs (Curry ys i) :~: Curry zs i
forall (xs :: IxList) (ys :: IxList) (zs :: IxList) i.
AppendProof xs ys zs =>
Proxy i -> Curry xs (Curry ys i) :~: Curry zs i
appendProof @xs @ys @zs Proxy i
i of
Refl -> Curry (x : xs) (Curry ys i) :~: Curry (x : zs) i
forall k (a :: k). a :~: a
Refl
class LabelOptic (name :: Symbol) k s t a b | name s -> k a
, name t -> k b
, name s b -> t
, name t a -> s where
labelOptic :: Optic k NoIx s t a b
instance {-# OVERLAPPABLE #-}
(LabelOptic name k s t a b,
TypeError
('Text "No instance for LabelOptic " ':<>: 'ShowType name
':<>: 'Text " " ':<>: QuoteType k
':<>: 'Text " " ':<>: QuoteType s
':<>: 'Text " " ':<>: QuoteType t
':<>: 'Text " " ':<>: QuoteType a
':<>: 'Text " " ':<>: QuoteType b
':$$: 'Text " (maybe you forgot to define it or misspelled a name?)")
) => LabelOptic name k s t a b where
labelOptic :: Optic k '[] s t a b
labelOptic = [Char] -> Optic k '[] s t a b
forall a. HasCallStack => [Char] -> a
error "unreachable"
type LabelOptic' name k s a = LabelOptic name k s s a a
instance
(LabelOptic name k s t a b, is ~ NoIx
) => IsLabel name (Optic k is s t a b) where
#if __GLASGOW_HASKELL__ >= 802
fromLabel :: Optic k is s t a b
fromLabel = LabelOptic name k s t a b => Optic k '[] s t a b
forall (name :: Symbol) k s t a b.
LabelOptic name k s t a b =>
Optic k '[] s t a b
labelOptic @name @k @s @t @a @b
#else
fromLabel _ = labelOptic @name @k @s @t @a @b
#endif