{-# LANGUAGE TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Generics.Product.Internal.Subtype
( GUpcast (..)
, GSmash (..)
) where
import Data.Generics.Internal.Families
import Data.Generics.Product.Internal.GLens
import Data.Kind (Type)
import GHC.Generics
import GHC.TypeLits (Symbol)
import Data.Generics.Internal.Profunctor.Lens (view)
class GUpcast (sub :: Type -> Type) (sup :: Type -> Type) where
gupcast :: sub p -> sup p
instance (GUpcast sub a, GUpcast sub b) => GUpcast sub (a :*: b) where
gupcast :: sub p -> (:*:) a b p
gupcast rep :: sub p
rep = sub p -> a p
forall (sub :: * -> *) (sup :: * -> *) p.
GUpcast sub sup =>
sub p -> sup p
gupcast sub p
rep a p -> b p -> (:*:) a b p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: sub p -> b p
forall (sub :: * -> *) (sup :: * -> *) p.
GUpcast sub sup =>
sub p -> sup p
gupcast sub p
rep
instance
GLens' (HasTotalFieldPSym field) sub t
=> GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where
gupcast :: sub p -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
gupcast r :: sub p
r = K1 R t p -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (t -> K1 R t p
forall k i c (p :: k). c -> K1 i c p
K1 (Lens (sub p) (sub p) t t -> sub p -> t
forall s a. Lens s s a a -> s -> a
view (forall (s :: * -> *) (t :: * -> *) a b x.
GLens (HasTotalFieldPSym field) s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @(HasTotalFieldPSym field)) sub p
r))
instance GUpcast sub sup => GUpcast sub (C1 c sup) where
gupcast :: sub p -> C1 c sup p
gupcast = sup p -> C1 c sup p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (sup p -> C1 c sup p) -> (sub p -> sup p) -> sub p -> C1 c sup p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub p -> sup p
forall (sub :: * -> *) (sup :: * -> *) p.
GUpcast sub sup =>
sub p -> sup p
gupcast
instance GUpcast sub sup => GUpcast sub (D1 c sup) where
gupcast :: sub p -> D1 c sup p
gupcast = sup p -> D1 c sup p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (sup p -> D1 c sup p) -> (sub p -> sup p) -> sub p -> D1 c sup p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub p -> sup p
forall (sub :: * -> *) (sup :: * -> *) p.
GUpcast sub sup =>
sub p -> sup p
gupcast
class GSmash sub sup where
gsmash :: sup p -> sub p -> sub p
instance (GSmash a sup, GSmash b sup) => GSmash (a :*: b) sup where
gsmash :: sup p -> (:*:) a b p -> (:*:) a b p
gsmash rep :: sup p
rep (a :: a p
a :*: b :: b p
b) = sup p -> a p -> a p
forall k (sub :: k -> *) (sup :: k -> *) (p :: k).
GSmash sub sup =>
sup p -> sub p -> sub p
gsmash sup p
rep a p
a a p -> b p -> (:*:) a b p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: sup p -> b p -> b p
forall k (sub :: k -> *) (sup :: k -> *) (p :: k).
GSmash sub sup =>
sup p -> sub p -> sub p
gsmash sup p
rep b p
b
instance
( leaf ~ (S1 ('MetaSel ('Just field) p f b) t)
, GSmashLeaf leaf sup (HasTotalFieldP field sup)
) => GSmash (S1 ('MetaSel ('Just field) p f b) t) sup where
gsmash :: sup p
-> S1 ('MetaSel ('Just field) p f b) t p
-> S1 ('MetaSel ('Just field) p f b) t p
gsmash = forall (p :: k).
GSmashLeaf
(S1 ('MetaSel ('Just field) p f b) t)
sup
(HasTotalFieldP field sup) =>
sup p
-> S1 ('MetaSel ('Just field) p f b) t p
-> S1 ('MetaSel ('Just field) p f b) t p
forall k (sub :: k -> *) (sup :: k -> *) (w :: Maybe *) (p :: k).
GSmashLeaf sub sup w =>
sup p -> sub p -> sub p
gsmashLeaf @_ @_ @(HasTotalFieldP field sup)
instance GSmash sub sup => GSmash (C1 c sub) sup where
gsmash :: sup p -> C1 c sub p -> C1 c sub p
gsmash sup :: sup p
sup (M1 sub :: sub p
sub) = sub p -> C1 c sub p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (sup p -> sub p -> sub p
forall k (sub :: k -> *) (sup :: k -> *) (p :: k).
GSmash sub sup =>
sup p -> sub p -> sub p
gsmash sup p
sup sub p
sub)
instance GSmash sub sup => GSmash (D1 c sub) sup where
gsmash :: sup p -> D1 c sub p -> D1 c sub p
gsmash sup :: sup p
sup (M1 sub :: sub p
sub) = sub p -> D1 c sub p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (sup p -> sub p -> sub p
forall k (sub :: k -> *) (sup :: k -> *) (p :: k).
GSmash sub sup =>
sup p -> sub p -> sub p
gsmash sup p
sup sub p
sub)
class GSmashLeaf sub sup (w :: Maybe Type) where
gsmashLeaf :: sup p -> sub p -> sub p
instance
GLens' (HasTotalFieldPSym field) sup t
=> GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup ('Just t) where
gsmashLeaf :: sup p
-> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
-> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
gsmashLeaf sup :: sup p
sup _ = K1 R t p -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (t -> K1 R t p
forall k i c (p :: k). c -> K1 i c p
K1 (Lens (sup p) (sup p) t t -> sup p -> t
forall s a. Lens s s a a -> s -> a
view (forall (s :: * -> *) (t :: * -> *) a b x.
GLens (HasTotalFieldPSym field) s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @(HasTotalFieldPSym field)) sup p
sup))
instance GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'Nothing where
gsmashLeaf :: sup p
-> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
-> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
gsmashLeaf _ = S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
-> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
forall a. a -> a
id
data HasTotalFieldPSym :: Symbol -> (TyFun (Type -> Type) (Maybe Type))
type instance Eval (HasTotalFieldPSym sym) tt = HasTotalFieldP sym tt