{-# 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.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