{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

{-|
Module: Data.Generic.Labels.Internal

Internal module containing the generics machinery to provide the instances
exported by this library, using 'Data.Generics.Product.Internal.GLens.GLens'.

__Warnings__:

  * contains an incoherent instance for 'GAdapt' which is used to
    prioritise built-in record field names over explicitly labelled types;
  * contains an orphan overlapping instance for @generic-lens@'s 'Data.Generics.Product.Internal.GLens.GLens'
    typeclass, which is used to additionally unwrap through labelled types.

-}

module Data.Generic.Labels.Internal
  ( GAdapt(..) )
  where

-- base

import Data.Kind
  ( Constraint, Type )
import GHC.Generics
import GHC.TypeLits
  ( Symbol )

-- generic-lens-core

import Data.Generics.Product.Internal.GLens
  ( Eval, GLens(..), GLens', TyFun )
import Data.Generics.Internal.Profunctor.Lens
  ( view )
import Data.Generics.Internal.Profunctor.Iso 
  ( Iso, iso, kIso )

-- generic-labels

import Data.Label
  ( (:=)(..), Label(..) )
import Data.Generic.Labels.Internal.Errors
  ( AdaptLabelMessage )

--------------------------------------------------------------------------------

-- Generics machinery for 'Adapt'.


-- | Generic version of 'Data.Generic.Labels.Adapt'.

type GAdapt :: ( Type -> Type ) -> ( Type -> Type ) -> ( Type -> Type ) -> Constraint
class GAdapt args opt all where
  gAdapt :: args p -> opt p -> all p

instance ( GAdapt args opt all1, GAdapt args opt all2 ) => GAdapt args opt ( all1 :*: all2 ) where
  gAdapt :: args p -> opt p -> (:*:) all1 all2 p
gAdapt args p
args opt p
opt = args p -> opt p -> all1 p
forall (args :: Type -> Type) (opt :: Type -> Type)
       (all :: Type -> Type) p.
GAdapt args opt all =>
args p -> opt p -> all p
gAdapt args p
args opt p
opt all1 p -> all2 p -> (:*:) all1 all2 p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: args p -> opt p -> all2 p
forall (args :: Type -> Type) (opt :: Type -> Type)
       (all :: Type -> Type) p.
GAdapt args opt all =>
args p -> opt p -> all p
gAdapt args p
args opt p
opt

instance GAdapt args opt all => GAdapt args opt ( C1 c all ) where
  gAdapt :: args p -> opt p -> C1 c all p
gAdapt args p
args opt p
opt = all p -> C1 c all p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (all p -> C1 c all p) -> all p -> C1 c all p
forall a b. (a -> b) -> a -> b
$ args p -> opt p -> all p
forall (args :: Type -> Type) (opt :: Type -> Type)
       (all :: Type -> Type) p.
GAdapt args opt all =>
args p -> opt p -> all p
gAdapt args p
args opt p
opt

instance GAdapt args opt all => GAdapt args opt ( D1 c all ) where
  gAdapt :: args p -> opt p -> D1 c all p
gAdapt args p
args opt p
opt = all p -> D1 c all p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (all p -> D1 c all p) -> all p -> D1 c all p
forall a b. (a -> b) -> a -> b
$ args p -> opt p -> all p
forall (args :: Type -> Type) (opt :: Type -> Type)
       (all :: Type -> Type) p.
GAdapt args opt all =>
args p -> opt p -> all p
gAdapt args p
args opt p
opt

-- | This instance is INCOHERENT because we assume that no type variable (say @all0@)

-- will later be instantiated to a labelled type @lbl := all@.

--

-- The end result is that, when we have both a built-in Haskell record field name

-- as well as an explicit label, we prioritise the built-in record field name over the label.

instance {-# INCOHERENT #-}
         ( GLens' ( HasTotalLabelPSym lbl ) ( args :*: opts ) all )
      => GAdapt args opts ( M1 m meta ( Rec0 ( lbl := all ) ) )
      where
  gAdapt :: args p -> opts p -> M1 m meta (Rec0 (lbl := all)) p
gAdapt args p
args opts p
opt = K1 R (lbl := all) p -> M1 m meta (Rec0 (lbl := all)) p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (K1 R (lbl := all) p -> M1 m meta (Rec0 (lbl := all)) p)
-> (all -> K1 R (lbl := all) p)
-> all
-> M1 m meta (Rec0 (lbl := all)) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (lbl := all) -> K1 R (lbl := all) p
forall k i c (p :: k). c -> K1 i c p
K1 ((lbl := all) -> K1 R (lbl := all) p)
-> (all -> lbl := all) -> all -> K1 R (lbl := all) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( Label lbl
forall (lbl :: Symbol). Label lbl
Label @lbl Label lbl -> all -> lbl := all
forall (lbl :: Symbol) a. Label lbl -> a -> lbl := a
:= ) (all -> M1 m meta (Rec0 (lbl := all)) p)
-> all -> M1 m meta (Rec0 (lbl := all)) p
forall a b. (a -> b) -> a -> b
$ Lens ((:*:) args opts p) ((:*:) args opts p) all all
-> (:*:) args opts p -> all
forall s a. Lens s s a a -> s -> a
view ( forall (s :: Type -> Type) (t :: Type -> Type) a b x.
GLens (HasTotalLabelPSym lbl) s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: Type -> Type) (t :: Type -> Type) a b
       x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @( HasTotalLabelPSym lbl ) ) ( args p
args args p -> opts p -> (:*:) args opts p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: opts p
opt )

instance ( GLens' ( HasTotalLabelPSym lbl ) ( args :*: opts ) all )
      => GAdapt args opts ( S1 ( MetaSel ( Just lbl ) p f b ) ( Rec0 all ) )
      where
  gAdapt :: args p -> opts p -> S1 ('MetaSel ('Just lbl) p f b) (Rec0 all) p
gAdapt args p
args opts p
opt = K1 R all p -> S1 ('MetaSel ('Just lbl) p f b) (Rec0 all) p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (K1 R all p -> S1 ('MetaSel ('Just lbl) p f b) (Rec0 all) p)
-> (all -> K1 R all p)
-> all
-> S1 ('MetaSel ('Just lbl) p f b) (Rec0 all) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. all -> K1 R all p
forall k i c (p :: k). c -> K1 i c p
K1 (all -> S1 ('MetaSel ('Just lbl) p f b) (Rec0 all) p)
-> all -> S1 ('MetaSel ('Just lbl) p f b) (Rec0 all) p
forall a b. (a -> b) -> a -> b
$ Lens ((:*:) args opts p) ((:*:) args opts p) all all
-> (:*:) args opts p -> all
forall s a. Lens s s a a -> s -> a
view ( forall (s :: Type -> Type) (t :: Type -> Type) a b x.
GLens (HasTotalLabelPSym lbl) s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: Type -> Type) (t :: Type -> Type) a b
       x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @( HasTotalLabelPSym lbl ) ) ( args p
args args p -> opts p -> (:*:) args opts p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: opts p
opt )

--------------------------------------------------------------------------------

-- Generic lens machinery.


type And :: Maybe a -> Maybe a -> Maybe a
type family m1 `And` m2 where
  Just a `And` Just a = Just a
  _      `And` _      = Nothing

type Or :: Maybe a -> Maybe a -> Maybe a
type family m1 `Or` m2 where
  Just a `Or` _ = Just a
  _      `Or` b = b

type HasTotalLabelP :: Symbol -> ( Type -> Type ) -> Maybe Type
type family HasTotalLabelP lbl f where
  HasTotalLabelP lbl ( S1 ( MetaSel ( Just lbl ) _ _ _ ) ( Rec0 ty ) ) = 
    Just ty
  HasTotalLabelP lbl ( S1 ( MetaSel ( Just lbl' ) _ _ _ ) _ ) = 
    Nothing
  HasTotalLabelP lbl ( S1 _ ( K1 _ ( lbl := ty ) ) ) =
    Just ty
  HasTotalLabelP lbl ( S1 _ ( K1 _ ( lbl' := _ ) ) ) =
    Nothing
  HasTotalLabelP lbl ( l :*: r ) =
    HasTotalLabelP lbl l `Or` HasTotalLabelP lbl r
  HasTotalLabelP lbl ( l :+: r ) =
    HasTotalLabelP lbl l `And` HasTotalLabelP lbl r
  HasTotalLabelP lbl ( S1 _ _ ) =
    Nothing
  HasTotalLabelP lbl ( C1 _ f ) =
    HasTotalLabelP lbl f
  HasTotalLabelP lbl ( D1 _ f ) =
    HasTotalLabelP lbl f
  HasTotalLabelP lbl ( K1 _ _ ) =
    Nothing
  HasTotalLabelP lbl U1 =
    Nothing
  HasTotalLabelP lbl V1 =
    Nothing

type HasTotalLabelPSym :: Symbol -> TyFun ( Type -> Type ) ( Maybe Type )
data HasTotalLabelPSym lbl f mbTy
type instance Eval ( HasTotalLabelPSym lbl ) f = HasTotalLabelP lbl f

class LabelIso mbLbl1 mbLbl2 s t a b | mbLbl1 s -> a, mbLbl2 t -> b where
  lblIso :: Iso s t a b
instance
  ( AdaptLabelMessage lbl ( Just a1 ) Nothing b1
  , a1 ~ a, b1 ~ b
  ) => LabelIso ( Just lbl ) ( Just lbl ) ( lbl := a1 ) ( lbl := b1 ) a b where
  lblIso :: p i a b -> p i (lbl := a1) (lbl := b1)
lblIso = ((lbl := a1) -> a1)
-> (b1 -> lbl := b1) -> Iso (lbl := a1) (lbl := b1) a1 b1
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso ( \ ( Label lbl
_ := a1
a ) -> a1
a ) ( Label lbl
forall (lbl :: Symbol). Label lbl
Label @lbl Label lbl -> b1 -> lbl := b1
forall (lbl :: Symbol) a. Label lbl -> a -> lbl := a
:= )
  {-# INLINE lblIso #-}
instance LabelIso Nothing Nothing a b a b where
  lblIso :: p i a b -> p i a b
lblIso = p i a b -> p i a b
forall a. a -> a
id
  {-# INLINE lblIso #-}

type GetLabel :: Type -> Maybe Symbol
type family GetLabel ty where
 GetLabel ( lbl := _ ) = Just lbl
 GetLabel _            = Nothing

instance {-# OVERLAPPABLE #-} LabelIso ( GetLabel a' ) ( GetLabel b' ) a' b' a b
      => GLens pred ( K1 r a' ) ( K1 r b' ) a b where
  glens :: p i a b -> p i (K1 r a' x) (K1 r b' x)
glens = p i a' b' -> p i (K1 r a' x) (K1 r b' x)
forall r a p b. Iso (K1 r a p) (K1 r b p) a b
kIso (p i a' b' -> p i (K1 r a' x) (K1 r b' x))
-> (p i a b -> p i a' b') -> p i a b -> p i (K1 r a' x) (K1 r b' x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k k (mbLbl1 :: k) (mbLbl2 :: k) s t a b.
LabelIso mbLbl1 mbLbl2 s t a b =>
Iso s t a b
forall s t a b.
LabelIso (GetLabel a') (GetLabel b') s t a b =>
Iso s t a b
lblIso @( GetLabel a' ) @( GetLabel b' )
  {-# INLINE glens #-}