{-# LANGUAGE
    AllowAmbiguousTypes
  , FlexibleInstances
  , MultiParamTypeClasses
  , ScopedTypeVariables
  , TypeApplications
  , TypeInType
  , TypeFamilies
  , TypeOperators
  , UndecidableInstances
#-}
{-# OPTIONS_GHC
  -fno-warn-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 :: a -> b
cast = NP P rb -> b
forall a (r :: RecordCode). IsRecord a r => RecordRep a -> a
fromRecord (NP P rb -> b) -> (a -> NP P rb) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record ra -> NP P rb
forall (r1 :: RecordCode) (r2 :: RecordCode).
IsSubTypeOf r1 r2 =>
Record r1 -> Record r2
castRecord (Record ra -> NP P rb) -> (a -> Record ra) -> a -> NP P rb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Record ra
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 :: a -> b
getField = forall a (r :: RecordCode). IsElemOf s a r => Record r -> a
forall (s :: Symbol) a (r :: RecordCode).
IsElemOf s a r =>
Record r -> a
get @s (Record ra -> b) -> (a -> Record ra) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Record ra
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
_ = Record '[]
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 = Snd '(s2, a2) -> P '(s2, a2)
forall a (p :: (a, *)). Snd p -> P p
P (Record r1 -> a2
forall (s :: Symbol) a (r :: RecordCode).
IsElemOf s a r =>
Record r -> a
get @s2 Record r1
r) P '(s2, a2) -> NP P r2 -> Record ('(s2, a2) : r2)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* Record r1 -> NP P r2
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
forall a1 (s2 :: Symbol) a2 (r :: RecordCode).
IsElemOf' (SameFieldLabel s1 s2) 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
_) = a1
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) = NP P xs -> a1
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