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