{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#if MIN_VERSION_base(4,12,0)
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
#else
{-# LANGUAGE TypeInType #-}
#endif
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module Generics.SOP.Record.SubTyping
  ( cast
  , IsSubTypeOf
  , IsElemOf
  , get
  , getField
  )
  where

import Data.Type.Equality
import Generics.SOP.NP
import GHC.Types

import Generics.SOP.Record

-- | Cast one record type to another if there is a subtype relationship
-- between them. Currently, only width subtyping is considered, which means
-- that we can forget and reorder fields.
--
cast :: (IsRecord a ra, IsRecord b rb, IsSubTypeOf ra rb) => a -> b
cast :: forall a (ra :: RecordCode) b (rb :: RecordCode).
(IsRecord a ra, IsRecord b rb, IsSubTypeOf ra rb) =>
a -> b
cast = forall a (r :: RecordCode). IsRecord a r => RecordRep a -> a
fromRecord forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r1 :: RecordCode) (r2 :: RecordCode).
IsSubTypeOf r1 r2 =>
Record r1 -> Record r2
castRecord forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (_r :: RecordCode). IsRecord a _r => a -> RecordRep a
toRecord

-- | Extract a record field based on the symbolic name of a field.
-- Requires an explicit type application for the field name.
--
getField :: forall s a b ra . (IsRecord a ra, IsElemOf s b ra) => a -> b
getField :: forall (s :: Symbol) a b (ra :: RecordCode).
(IsRecord a ra, IsElemOf s b ra) =>
a -> b
getField = forall (s :: Symbol) a (r :: RecordCode).
IsElemOf s a r =>
Record r -> a
get @s forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (_r :: RecordCode). IsRecord a _r => a -> RecordRep a
toRecord

-- | Class that checks whether one record code is convertible into another.
--
-- Conversion works if the first record contains at least the labels of the
-- second record, and if the types of the corresponding fields match exactly.
--
class IsSubTypeOf (r1 :: RecordCode) (r2 :: RecordCode) where
  -- | Perform a safe cast between two records.
  castRecord :: Record r1 -> Record r2

instance IsSubTypeOf r1 '[] where
  castRecord :: Record r1 -> Record '[]
castRecord Record r1
_ = forall {k} (a :: k -> *). NP a '[]
Nil

instance (IsSubTypeOf r1 r2, IsElemOf s2 a2 r1) => IsSubTypeOf r1 ( '(s2, a2) : r2 ) where
  castRecord :: Record r1 -> Record ('(s2, a2) : r2)
castRecord Record r1
r = forall a (p :: (a, *)). Snd p -> P p
P (forall (s :: Symbol) a (r :: RecordCode).
IsElemOf s a r =>
Record r -> a
get @s2 Record r1
r) forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall (r1 :: RecordCode) (r2 :: RecordCode).
IsSubTypeOf r1 r2 =>
Record r1 -> Record r2
castRecord Record r1
r

-- | Class that checks whether a field of a particular type is contained
-- in a record.
--
class IsElemOf (s :: Symbol) (a :: Type) (r :: RecordCode) where
  -- | Perform an extraction of a given field. Field name has to be passed
  -- via type application.
  --
  get :: Record r -> a

-- | Helper class. Isn't strictly needed, but allows us to avoid
-- overlapping instances for the 'IsElemOf' class.
--
class IsElemOf' (b :: Bool)
  (s1 :: FieldLabel) (a1 :: Type)
  (s2 :: FieldLabel) (a2 :: Type)
  (r :: RecordCode)
  where
  get' :: Record ( '(s2, a2) : r ) -> a1

instance
  IsElemOf' (SameFieldLabel s1 s2) s1 a1 s2 a2 r =>
  IsElemOf s1 a1 ( '(s2, a2) : r )
  where
  get :: Record ('(s2, a2) : r) -> a1
get = forall (b :: Bool) (s1 :: Symbol) a1 (s2 :: Symbol) a2
       (r :: RecordCode).
IsElemOf' b s1 a1 s2 a2 r =>
Record ('(s2, a2) : r) -> a1
get' @(SameFieldLabel s1 s2) @s1

instance (a1 ~ a2) => IsElemOf' True s a1 s a2 r where
  get' :: Record ('(s, a2) : r) -> a1
get' (P Snd x
a :* NP P xs
_) = Snd x
a

instance IsElemOf s1 a1 r => IsElemOf' False s1 a1 s2 a2 r where
  get' :: Record ('(s2, a2) : r) -> a1
get' (P x
_ :* NP P xs
r) = forall (s :: Symbol) a (r :: RecordCode).
IsElemOf s a r =>
Record r -> a
get @s1 NP P xs
r

-- | Decide the equality of two field labels.
--
-- Just a special case of polymorphic type equality.
--
type family
  SameFieldLabel (s1 :: FieldLabel) (s2 :: FieldLabel) :: Bool where
  SameFieldLabel s1 s2 = s1 == s2