module Control.Provide.ARec where import Control.Lens import Data.Reflection import Data.Proxy import Data.Vinyl hiding (Dict) import Data.Vinyl.ARec import Data.Vinyl.TypeLevel import Data.Kind (Type) import Control.Provide data ARecProvider tctx recVal type instance ProviderTypeContext (ARecProvider tctx recVal) = tctx newtype ProviderField tctx (key :: Type) = ProviderField { forall tctx key. ProviderField tctx key -> ValueType tctx key unProviderField :: ValueType tctx key } instance (Reifies recVal (ARec (ProviderField tctx) items), RecElem ARec key key items items (RIndex key items)) => ARecProvider tctx recVal `Provides` key where provided :: ValueType (ProviderTypeContext (ARecProvider tctx recVal)) key provided = ProviderField tctx key -> ValueType tctx key forall tctx key. ProviderField tctx key -> ValueType tctx key unProviderField (ProviderField tctx key -> ValueType tctx key) -> ProviderField tctx key -> ValueType tctx key forall a b. (a -> b) -> a -> b $ Proxy recVal -> ARec (ProviderField tctx) items forall {k} (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a forall (proxy :: k -> *). proxy recVal -> ARec (ProviderField tctx) items reflect (forall (t :: k). Proxy t forall {k} (t :: k). Proxy t Proxy @recVal) ARec (ProviderField tctx) items -> Getting (ProviderField tctx key) (ARec (ProviderField tctx) items) (ProviderField tctx key) -> ProviderField tctx key forall s a. s -> Getting a s a -> a ^. forall {k} (r :: k) (record :: (k -> *) -> [k] -> *) (rs :: [k]) (f :: k -> *) (g :: * -> *). (RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f, Functor g) => (f r -> g (f r)) -> record f rs -> g (record f rs) forall r (record :: (* -> *) -> [*] -> *) (rs :: [*]) (f :: * -> *) (g :: * -> *). (RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f, Functor g) => (f r -> g (f r)) -> record f rs -> g (record f rs) rlens @key provideARec :: forall tctx items r . ( NatToInt (RLength items) , ToARec items ) => Rec (ProviderField tctx) items -> (forall (recVal :: Type). Reifies recVal (ARec (ProviderField tctx) items) => Proxy (ARecProvider tctx recVal) -> r) -> r provideARec :: forall tctx (items :: [*]) r. (NatToInt (RLength items), ToARec items) => Rec (ProviderField tctx) items -> (forall recVal. Reifies recVal (ARec (ProviderField tctx) items) => Proxy (ARecProvider tctx recVal) -> r) -> r provideARec Rec (ProviderField tctx) items items forall recVal. Reifies recVal (ARec (ProviderField tctx) items) => Proxy (ARecProvider tctx recVal) -> r r = ARec (ProviderField tctx) items -> (forall {s}. Reifies s (ARec (ProviderField tctx) items) => Proxy s -> r) -> r forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r reify (Rec (ProviderField tctx) items -> ARec (ProviderField tctx) items forall {k} (f :: k -> *) (ts :: [k]). (NatToInt (RLength ts), ToARec ts) => Rec f ts -> ARec f ts toARec Rec (ProviderField tctx) items items) ((forall {s}. Reifies s (ARec (ProviderField tctx) items) => Proxy s -> r) -> r) -> (forall {s}. Reifies s (ARec (ProviderField tctx) items) => Proxy s -> r) -> r forall a b. (a -> b) -> a -> b $ \(Proxy s Proxy :: Proxy recVal) -> Proxy (ARecProvider tctx s) -> r forall recVal. Reifies recVal (ARec (ProviderField tctx) items) => Proxy (ARecProvider tctx recVal) -> r r (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @(ARecProvider tctx recVal))