{-# 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 :: (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
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 IsSubTypeOf (r1 :: RecordCode) (r2 :: RecordCode) where
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 IsElemOf (s :: Symbol) (a :: Type) (r :: RecordCode) where
get :: Record r -> a
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
type family
SameFieldLabel (s1 :: FieldLabel) (s2 :: FieldLabel) :: Bool where
SameFieldLabel s1 s2 = s1 == s2