{-# LANGUAGE ConstraintKinds #-}
{-# 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
( Context
, gsmash
, gupcast
) 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)
import GHC.Generics (Generic (Rep))
import GHC.TypeLits (TypeError, ErrorMessage (..))
import Data.Kind (Constraint)
import Data.Generics.Internal.Errors
type Context a b
= ( Generic a
, Generic b
, GSmash (Rep a) (Rep b)
, GUpcast (Rep a) (Rep b)
, CustomError a b
)
type family CustomError a b :: Constraint where
CustomError a b =
( ErrorUnless b a (CollectFieldsOrdered (Rep b) \\ CollectFieldsOrdered (Rep a))
, Defined (Rep a)
(NoGeneric a '[ 'Text "arising from a generic lens focusing on " ':<>: QuoteType b
, 'Text "as a supertype of " ':<>: QuoteType a
])
(() :: Constraint)
, Defined (Rep b)
(NoGeneric b '[ 'Text "arising from a generic lens focusing on " ':<>: QuoteType b
, 'Text "as a supertype of " ':<>: QuoteType a
])
(() :: Constraint)
)
type family ErrorUnless (sup :: Type) (sub :: Type) (diff :: [Symbol]) :: Constraint where
ErrorUnless _ _ '[]
= ()
ErrorUnless sup sub fs
= TypeError
( 'Text "The type '"
':<>: 'ShowType sub
':<>: 'Text "' is not a subtype of '"
':<>: 'ShowType sup ':<>: 'Text "'."
':$$: 'Text "The following fields are missing from '"
':<>: 'ShowType sub ':<>: 'Text "':"
':$$: ShowSymbols fs
)
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 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 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 sup p
rep (a p
a :*: 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 p
sup (M1 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 p
sup (M1 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 p
sup S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
_ = 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 sup p
_ = 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