{-# 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
-- Copyright   :  (C) 2020 Csongor Kiss
-- License     :  BSD3
-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Structural subtype relationships between product types.
--
-----------------------------------------------------------------------------

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
        )

--------------------------------------------------------------------------------
-- * Generic upcasting

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

--------------------------------------------------------------------------------
-- * Generic smashing

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