{-# OPTIONS_GHC -Wno-missing-methods #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Libjwt.PrivateClaims
(
Claim(..)
, type (->>)
, Namespace(..)
, KnownNamespace(..)
, ClaimName(..)
, claimNameVal
, Ns(..)
, ClaimWitness
, testify
, (->>)
, PrivateClaims
, type Empty
, nullClaims
, addClaim
, (.:)
, CanAdd
, RestrictedName
, getClaim
, (.!)
, CanGet
, LookupClaimType
, pattern (:<)
, withNs
, someNs
, noNs
, ToPrivateClaims(..)
, FromPrivateClaims(..)
)
where
import Libjwt.Encoding
import Libjwt.Decoding
import Libjwt.FFI.Jwt (JwtT)
import Control.Applicative ( liftA2 )
import Data.Coerce
import Data.Default
import Data.HashMap.Lazy ( HashMap
, (!)
)
import qualified Data.HashMap.Lazy as HashMap
import Data.Kind
import Data.Proxied ( selNameProxied )
import Data.Proxy
import GHC.Generics
import GHC.OverloadedLabels
import GHC.Show
import GHC.TypeLits
import Unsafe.Coerce ( unsafeCoerce )
infix 6 ->>
infixr 5 .:
infixr 5 :<
data Claim (a :: Type) = Grant Symbol a
type name ->> a = 'Grant name a
data Namespace = NoNs | SomeNs Symbol
class KnownNamespace (ns :: Namespace) where
namespaceValue :: proxy ns -> Maybe String
instance KnownNamespace 'NoNs where
namespaceValue :: proxy 'NoNs -> Maybe String
namespaceValue proxy 'NoNs
_ = Maybe String
forall a. Maybe a
Nothing
instance KnownSymbol ns => KnownNamespace ('SomeNs ns) where
namespaceValue :: proxy ('SomeNs ns) -> Maybe String
namespaceValue proxy ('SomeNs ns)
_ = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Proxy ns -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy ns
forall k (t :: k). Proxy t
Proxy :: Proxy ns)
fullClaimName :: (KnownNamespace ns) => proxy ns -> String -> String
fullClaimName :: proxy ns -> String -> String
fullClaimName proxy ns
p String
claimName =
String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
claimName (String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char
'/' Char -> String -> String
forall a. a -> [a] -> [a]
: String
claimName) (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ proxy ns -> Maybe String
forall (ns :: Namespace) (proxy :: Namespace -> *).
KnownNamespace ns =>
proxy ns -> Maybe String
namespaceValue proxy ns
p
{-# INLINE fullClaimName #-}
fullClaimName' :: forall ns name . (KnownNamespace ns, KnownSymbol name) => String
fullClaimName' :: String
fullClaimName' = Proxy ns -> String -> String
forall (ns :: Namespace) (proxy :: Namespace -> *).
KnownNamespace ns =>
proxy ns -> String -> String
fullClaimName (Proxy ns
forall k (t :: k). Proxy t
Proxy :: Proxy ns) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy :: Proxy name)
data ClaimName (name :: Symbol) = ClaimName
instance (name ~ name') => IsLabel name (ClaimName name') where
fromLabel :: ClaimName name'
fromLabel = ClaimName name'
forall (name :: Symbol). ClaimName name
ClaimName
claimNameVal :: forall name . KnownSymbol name => ClaimName name -> String
claimNameVal :: ClaimName name -> String
claimNameVal ClaimName name
_ = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy :: Proxy name)
data Ns (ns :: Symbol) = Ns
instance (name ~ name') => IsLabel name (Ns name') where
fromLabel :: Ns name'
fromLabel = Ns name'
forall (ns :: Symbol). Ns ns
Ns
newtype ClaimWitness (name :: Symbol) a = Witness { ClaimWitness name a -> a
testify :: a }
(->>) :: ClaimName name -> a -> ClaimWitness name a
ClaimName name
_ ->> :: ClaimName name -> a -> ClaimWitness name a
->> a
a = a -> ClaimWitness name a
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness a
a
data Any = forall a . Any a
newtype PrivateClaims (ts :: [Claim Type]) (ns :: Namespace) = PrivateClaims { PrivateClaims ts ns -> HashMap String Any
unsafeClaimsMap :: HashMap String Any }
type Empty = ('[] :: [Claim Type])
nullClaims :: PrivateClaims Empty 'NoNs
nullClaims :: PrivateClaims Empty 'NoNs
nullClaims = HashMap String Any -> PrivateClaims Empty 'NoNs
forall (ts :: [Claim *]) (ns :: Namespace).
HashMap String Any -> PrivateClaims ts ns
PrivateClaims HashMap String Any
forall k v. HashMap k v
HashMap.empty
addClaim
:: forall name a ts ns
. CanAdd name ts
=> ClaimName name
-> a
-> PrivateClaims ts ns
-> PrivateClaims (name ->> a : ts) ns
addClaim :: ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName name
_ a
a (PrivateClaims HashMap String Any
store) = HashMap String Any -> PrivateClaims ((name ->> a) : ts) ns
forall (ts :: [Claim *]) (ns :: Namespace).
HashMap String Any -> PrivateClaims ts ns
PrivateClaims
(HashMap String Any -> PrivateClaims ((name ->> a) : ts) ns)
-> HashMap String Any -> PrivateClaims ((name ->> a) : ts) ns
forall a b. (a -> b) -> a -> b
$ String -> Any -> HashMap String Any -> HashMap String Any
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert String
claimName (a -> Any
forall a. a -> Any
Any a
a) HashMap String Any
store
where claimName :: String
claimName = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy :: Proxy name)
(.:)
:: forall name a ts ns
. CanAdd name ts
=> ClaimWitness name a
-> PrivateClaims ts ns
-> PrivateClaims (name ->> a : ts) ns
(Witness a
a) .: :: ClaimWitness name a
-> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
.: PrivateClaims ts ns
pc = ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName name
forall (name :: Symbol). ClaimName name
ClaimName a
a PrivateClaims ts ns
pc
type family CanAdd n ns :: Constraint where
CanAdd n ns = (KnownSymbol n, DisallowRestrictedName (RestrictedName n) n, RequireUniqueName (UniqueName n ns) n)
type family UniqueName (name :: Symbol) (ts :: [Claim Type]) :: Bool where
UniqueName _ '[] = 'True
UniqueName n (n ->> _ : _) = 'False
UniqueName n (_ : rest) = UniqueName n rest
type family RequireUniqueName (isUnique :: Bool) (name :: Symbol) :: Constraint where
RequireUniqueName 'True _ = ()
RequireUniqueName 'False n = TypeError ('Text "Claim " ':<>: 'ShowType n ':<>: 'Text " is not unique in this claim set")
type family RestrictedName (name :: Symbol) :: Bool where
RestrictedName "iss" = 'True
RestrictedName "sub" = 'True
RestrictedName "aud" = 'True
RestrictedName "exp" = 'True
RestrictedName "nbf" = 'True
RestrictedName "iat" = 'True
RestrictedName "jti" = 'True
RestrictedName _ = 'False
type family DisallowRestrictedName (isRestricted :: Bool) (name :: Symbol) :: Constraint where
DisallowRestrictedName 'False _ = ()
DisallowRestrictedName 'True n = TypeError
( 'ShowType n
':<>:
'Text " is the name of the registered claim (it is exposed as a field that must be set directly or use JwtBuilder)"
)
unsafeLookup :: String -> PrivateClaims ts ns -> p
unsafeLookup :: String -> PrivateClaims ts ns -> p
unsafeLookup String
claimName PrivateClaims ts ns
pc = Any -> p
forall p. Any -> p
unAny (Any -> p) -> Any -> p
forall a b. (a -> b) -> a -> b
$ PrivateClaims ts ns -> HashMap String Any
forall (ts :: [Claim *]) (ns :: Namespace).
PrivateClaims ts ns -> HashMap String Any
unsafeClaimsMap PrivateClaims ts ns
pc HashMap String Any -> String -> Any
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
! String
claimName
where unAny :: Any -> p
unAny (Any a
a) = a -> p
forall a b. a -> b
unsafeCoerce a
a
getClaim
:: forall name ts ns
. CanGet name ts
=> ClaimName name
-> PrivateClaims ts ns
-> LookupClaimType name ts
getClaim :: ClaimName name -> PrivateClaims ts ns -> LookupClaimType name ts
getClaim ClaimName name
_ = String -> PrivateClaims ts ns -> LookupClaimType name ts
forall (ts :: [Claim *]) (ns :: Namespace) p.
String -> PrivateClaims ts ns -> p
unsafeLookup String
name where name :: String
name = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy :: Proxy name)
{-# INLINE getClaim #-}
(.!)
:: forall name ts ns
. CanGet name ts
=> PrivateClaims ts ns
-> ClaimName name
-> LookupClaimType name ts
PrivateClaims ts ns
pc .! :: PrivateClaims ts ns -> ClaimName name -> LookupClaimType name ts
.! ClaimName name
name = ClaimName name -> PrivateClaims ts ns -> LookupClaimType name ts
forall (name :: Symbol) (ts :: [Claim *]) (ns :: Namespace).
CanGet name ts =>
ClaimName name -> PrivateClaims ts ns -> LookupClaimType name ts
getClaim ClaimName name
name PrivateClaims ts ns
pc
type family CanGet n ns :: Constraint where
CanGet n ns = (KnownSymbol n, RequireExists (NameExists n ns) n)
type family LookupClaimType (name :: Symbol) (ts :: [Claim Type]) :: Type where
LookupClaimType n (n ->> a : _) = a
LookupClaimType n (_ : rest) = LookupClaimType n rest
type family NameExists (name :: Symbol) (ts :: [Claim Type]) :: Bool where
NameExists _ '[] = 'False
NameExists n (n ->> _ : _) = 'True
NameExists n (_ : rest ) = NameExists n rest
type family RequireExists (exists :: Bool) (name :: Symbol) :: Constraint where
RequireExists 'True _ = ()
RequireExists 'False n = TypeError ('Text "Claim " ':<>: 'ShowType n ':<>: 'Text " does not exist in this claim set")
getTail :: PrivateClaims (name ->> a : tl) ns -> PrivateClaims tl ns
getTail :: PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
getTail = PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
coerce
view :: forall name a tl ns . KnownSymbol name => PrivateClaims (name ->> a : tl) ns -> (a, PrivateClaims tl ns)
view :: PrivateClaims ((name ->> a) : tl) ns -> (a, PrivateClaims tl ns)
view PrivateClaims ((name ->> a) : tl) ns
pc = (a
LookupClaimType name ((name ->> a) : tl)
a, PrivateClaims tl ns
tl)
where
a :: LookupClaimType name ((name ->> a) : tl)
a = PrivateClaims ((name ->> a) : tl) ns
pc PrivateClaims ((name ->> a) : tl) ns
-> ClaimName name -> LookupClaimType name ((name ->> a) : tl)
forall (name :: Symbol) (ts :: [Claim *]) (ns :: Namespace).
CanGet name ts =>
PrivateClaims ts ns -> ClaimName name -> LookupClaimType name ts
.! (ClaimName name
forall (name :: Symbol). ClaimName name
ClaimName @name)
tl :: PrivateClaims tl ns
tl = PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
forall (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
getTail PrivateClaims ((name ->> a) : tl) ns
pc
pattern (:<) :: KnownSymbol name => a -> PrivateClaims tl ns -> PrivateClaims (name ->> a : tl) ns
pattern head $m:< :: forall r (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
KnownSymbol name =>
PrivateClaims ((name ->> a) : tl) ns
-> (a -> PrivateClaims tl ns -> r) -> (Void# -> r) -> r
:< tail <- (view -> (head, tail))
{-# COMPLETE (:<) :: PrivateClaims #-}
withNs
:: ToPrivateClaims a => Ns ns -> a -> PrivateClaims (Claims a) ( 'SomeNs ns)
withNs :: Ns ns -> a -> PrivateClaims (Claims a) ('SomeNs ns)
withNs Ns ns
_ = PrivateClaims (Claims a) (OutNs a)
-> PrivateClaims (Claims a) ('SomeNs ns)
coerce (PrivateClaims (Claims a) (OutNs a)
-> PrivateClaims (Claims a) ('SomeNs ns))
-> (a -> PrivateClaims (Claims a) (OutNs a))
-> a
-> PrivateClaims (Claims a) ('SomeNs ns)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> PrivateClaims (Claims a) (OutNs a)
forall a.
ToPrivateClaims a =>
a -> PrivateClaims (Claims a) (OutNs a)
toPrivateClaims
someNs :: Ns ns -> PrivateClaims ts 'NoNs -> PrivateClaims ts ( 'SomeNs ns)
someNs :: Ns ns -> PrivateClaims ts 'NoNs -> PrivateClaims ts ('SomeNs ns)
someNs Ns ns
_ = PrivateClaims ts 'NoNs -> PrivateClaims ts ('SomeNs ns)
coerce
noNs :: PrivateClaims ts any -> PrivateClaims ts 'NoNs
noNs :: PrivateClaims ts any -> PrivateClaims ts 'NoNs
noNs = PrivateClaims ts any -> PrivateClaims ts 'NoNs
coerce
getHead
:: forall name a tl ns . (KnownSymbol name, KnownNamespace ns) => PrivateClaims (name ->> a : tl) ns -> (String, a)
getHead :: PrivateClaims ((name ->> a) : tl) ns -> (String, a)
getHead PrivateClaims ((name ->> a) : tl) ns
pc = (Proxy ns -> String -> String
forall (ns :: Namespace) (proxy :: Namespace -> *).
KnownNamespace ns =>
proxy ns -> String -> String
fullClaimName (Proxy ns
forall k (t :: k). Proxy t
Proxy :: Proxy ns) String
claimName, a
claimValue)
where
claimName :: String
claimName = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy :: Proxy name)
claimValue :: a
claimValue = String -> PrivateClaims ((name ->> a) : tl) ns -> a
forall (ts :: [Claim *]) (ns :: Namespace) p.
String -> PrivateClaims ts ns -> p
unsafeLookup String
claimName PrivateClaims ((name ->> a) : tl) ns
pc
{-# INLINE getHead #-}
instance (ts ~ Empty, ns ~ 'NoNs) => Default (PrivateClaims ts ns) where
def :: PrivateClaims ts ns
def = PrivateClaims ts ns
PrivateClaims Empty 'NoNs
nullClaims
instance Encode (PrivateClaims Empty ns) where
encode :: PrivateClaims Empty ns -> JwtT -> EncodeResult
encode PrivateClaims Empty ns
_ = JwtT -> EncodeResult
forall b. b -> EncodeResult
nullEncode
instance
( ClaimEncoder a
, KnownSymbol name
, KnownNamespace ns
, Encode (PrivateClaims tl ns)
)
=> Encode (PrivateClaims (name ->> a : tl) ns) where
encode :: PrivateClaims ((name ->> a) : tl) ns -> JwtT -> EncodeResult
encode PrivateClaims ((name ->> a) : tl) ns
pc JwtT
jwt = String -> a -> JwtT -> EncodeResult
forall t. ClaimEncoder t => String -> t -> JwtT -> EncodeResult
encodeClaim String
claimName a
a JwtT
jwt EncodeResult -> EncodeResult -> EncodeResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PrivateClaims tl ns -> JwtT -> EncodeResult
forall c. Encode c => c -> JwtT -> EncodeResult
encode (PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
forall (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
getTail PrivateClaims ((name ->> a) : tl) ns
pc) JwtT
jwt
where (String
claimName, a
a) = PrivateClaims ((name ->> a) : tl) ns -> (String, a)
forall (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
(KnownSymbol name, KnownNamespace ns) =>
PrivateClaims ((name ->> a) : tl) ns -> (String, a)
getHead PrivateClaims ((name ->> a) : tl) ns
pc
instance Decode (PrivateClaims Empty ns) where
decode :: JwtT -> JwtIO (PrivateClaims Empty ns)
decode = JwtIO (PrivateClaims Empty ns)
-> JwtT -> JwtIO (PrivateClaims Empty ns)
forall a b. a -> b -> a
const (JwtIO (PrivateClaims Empty ns)
-> JwtT -> JwtIO (PrivateClaims Empty ns))
-> JwtIO (PrivateClaims Empty ns)
-> JwtT
-> JwtIO (PrivateClaims Empty ns)
forall a b. (a -> b) -> a -> b
$ PrivateClaims Empty ns -> JwtIO (PrivateClaims Empty ns)
forall (m :: * -> *) a. Monad m => a -> m a
return (PrivateClaims Empty ns -> JwtIO (PrivateClaims Empty ns))
-> PrivateClaims Empty ns -> JwtIO (PrivateClaims Empty ns)
forall a b. (a -> b) -> a -> b
$ PrivateClaims Empty 'NoNs -> PrivateClaims Empty ns
coerce PrivateClaims Empty 'NoNs
nullClaims
instance
( ty ~ DecodeAuxDef a
, DecodeAux ty ns name a
, CanAdd name tl
, Decode (PrivateClaims tl ns)
)
=> Decode (PrivateClaims (name ->> a : tl) ns) where
decode :: JwtT -> JwtIO (PrivateClaims ((name ->> a) : tl) ns)
decode JwtT
jwt = (ClaimWitness name a
-> PrivateClaims tl ns -> PrivateClaims ((name ->> a) : tl) ns)
-> JwtIO (ClaimWitness name a)
-> JwtIO (PrivateClaims tl ns)
-> JwtIO (PrivateClaims ((name ->> a) : tl) ns)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ClaimWitness name a
-> PrivateClaims tl ns -> PrivateClaims ((name ->> a) : tl) ns
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimWitness name a
-> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
(.:) JwtIO (ClaimWitness name a)
decodeHead JwtIO (PrivateClaims tl ns)
decodeTail
where
decodeHead :: JwtIO (ClaimWitness name a)
decodeHead = JwtT -> JwtIO (ClaimWitness name a)
forall (ty :: DecodeTy) (ns :: Namespace) (name :: Symbol) a.
DecodeAux ty ns name a =>
JwtT -> JwtIO (ClaimWitness name a)
decodeAux @ty @ns @name JwtT
jwt
decodeTail :: JwtIO (PrivateClaims tl ns)
decodeTail = JwtT -> JwtIO (PrivateClaims tl ns)
forall c. Decode c => JwtT -> JwtIO c
decode JwtT
jwt
data DecodeTy = Opt | Req | Mono
class DecodeAux (ty :: DecodeTy) (ns :: Namespace) (name :: Symbol) (a :: Type) where
decodeAux :: JwtT -> JwtIO (ClaimWitness name a)
instance
( b ~ Maybe a
, Decodable a
, KnownNamespace ns
, KnownSymbol name
)
=> DecodeAux 'Opt ns name b where
decodeAux :: JwtT -> JwtIO (ClaimWitness name b)
decodeAux = JwtIO (Maybe a) -> JwtIO (ClaimWitness name b)
coerce (JwtIO (Maybe a) -> JwtIO (ClaimWitness name b))
-> (JwtT -> JwtIO (Maybe a)) -> JwtT -> JwtIO (ClaimWitness name b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DecodeResult a -> JwtIO (Maybe a)
forall t. DecodeResult t -> JwtIO (Maybe t)
getOptional (DecodeResult a -> JwtIO (Maybe a))
-> (JwtT -> DecodeResult a) -> JwtT -> JwtIO (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Proxy a -> JwtT -> DecodeResult a
forall t (proxy :: * -> *).
ClaimDecoder t =>
String -> proxy t -> JwtT -> DecodeResult t
decodeClaimProxied ((KnownNamespace ns, KnownSymbol name) => String
forall (ns :: Namespace) (name :: Symbol).
(KnownNamespace ns, KnownSymbol name) =>
String
fullClaimName' @ns @name) (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)
instance
( Decodable a
, KnownNamespace ns
, KnownSymbol name
)
=> DecodeAux 'Req ns name a where
decodeAux :: JwtT -> JwtIO (ClaimWitness name a)
decodeAux = JwtIO a -> JwtIO (ClaimWitness name a)
coerce (JwtIO a -> JwtIO (ClaimWitness name a))
-> (JwtT -> JwtIO a) -> JwtT -> JwtIO (ClaimWitness name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Proxy a -> JwtT -> JwtIO a
forall t (proxy :: * -> *).
ClaimDecoder t =>
String -> proxy t -> JwtT -> JwtIO t
decodeClaimOrThrow ((KnownNamespace ns, KnownSymbol name) => String
forall (ns :: Namespace) (name :: Symbol).
(KnownNamespace ns, KnownSymbol name) =>
String
fullClaimName' @ns @name) (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)
instance
( b ~ [a]
, Decodable [a]
, KnownNamespace ns
, KnownSymbol name
)
=> DecodeAux 'Mono ns name b where
decodeAux :: JwtT -> JwtIO (ClaimWitness name b)
decodeAux = JwtIO b -> JwtIO (ClaimWitness name b)
coerce (JwtIO b -> JwtIO (ClaimWitness name b))
-> (JwtT -> JwtIO b) -> JwtT -> JwtIO (ClaimWitness name b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DecodeResult b -> JwtIO b
forall a. Monoid a => DecodeResult a -> JwtIO a
getOrEmpty (DecodeResult b -> JwtIO b)
-> (JwtT -> DecodeResult b) -> JwtT -> JwtIO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Proxy b -> JwtT -> DecodeResult b
forall t (proxy :: * -> *).
ClaimDecoder t =>
String -> proxy t -> JwtT -> DecodeResult t
decodeClaimProxied ((KnownNamespace ns, KnownSymbol name) => String
forall (ns :: Namespace) (name :: Symbol).
(KnownNamespace ns, KnownSymbol name) =>
String
fullClaimName' @ns @name) (Proxy b
forall k (t :: k). Proxy t
Proxy :: Proxy b)
type family DecodeAuxDef a :: DecodeTy where
DecodeAuxDef (Maybe b) = 'Opt
DecodeAuxDef String = 'Req
DecodeAuxDef [b] = 'Mono
DecodeAuxDef _ = 'Req
type family Showable pc :: Constraint where
Showable (PrivateClaims (name ->> a : tl) ns) = (KnownSymbol name, KnownNamespace ns, Show a, ShowL (PrivateClaims tl ns))
instance Show (PrivateClaims Empty ns) where
show :: PrivateClaims Empty ns -> String
show PrivateClaims Empty ns
_ = String
"()"
instance Showable (PrivateClaims (name ->> a : tl) ns) => Show (PrivateClaims (name ->> a : tl) ns) where
showsPrec :: Int -> PrivateClaims ((name ->> a) : tl) ns -> String -> String
showsPrec Int
_ PrivateClaims ((name ->> a) : tl) ns
pc =
Char -> String -> String
showChar Char
'(' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrivateClaims ((name ->> a) : tl) ns -> String -> String
forall (name :: Symbol) (ns :: Namespace) a (tl :: [Claim *]).
(KnownSymbol name, KnownNamespace ns, Show a) =>
PrivateClaims ((name ->> a) : tl) ns -> String -> String
showHead PrivateClaims ((name ->> a) : tl) ns
pc (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrivateClaims tl ns -> String -> String
forall a. ShowL a => a -> String -> String
showl (PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
forall (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
getTail PrivateClaims ((name ->> a) : tl) ns
pc) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
')'
showHead
:: (KnownSymbol name, KnownNamespace ns, Show a) => PrivateClaims ((name ->> a) : tl) ns -> ShowS
showHead :: PrivateClaims ((name ->> a) : tl) ns -> String -> String
showHead PrivateClaims ((name ->> a) : tl) ns
pc =
Char -> String -> String
showChar Char
'#' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
claimName (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
" ->> " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
6 a
a
where (String
claimName, a
a) = PrivateClaims ((name ->> a) : tl) ns -> (String, a)
forall (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
(KnownSymbol name, KnownNamespace ns) =>
PrivateClaims ((name ->> a) : tl) ns -> (String, a)
getHead PrivateClaims ((name ->> a) : tl) ns
pc
class ShowL a where
showl :: a -> ShowS
instance ShowL (PrivateClaims Empty ns) where
showl :: PrivateClaims Empty ns -> String -> String
showl PrivateClaims Empty ns
_ = String -> String
forall a. a -> a
id
instance Showable (PrivateClaims (name ->> a : tl) ns) => ShowL (PrivateClaims (name ->> a : tl) ns) where
showl :: PrivateClaims ((name ->> a) : tl) ns -> String -> String
showl PrivateClaims ((name ->> a) : tl) ns
pc = String -> String
showCommaSpace (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrivateClaims ((name ->> a) : tl) ns -> String -> String
forall (name :: Symbol) (ns :: Namespace) a (tl :: [Claim *]).
(KnownSymbol name, KnownNamespace ns, Show a) =>
PrivateClaims ((name ->> a) : tl) ns -> String -> String
showHead PrivateClaims ((name ->> a) : tl) ns
pc (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrivateClaims tl ns -> String -> String
forall a. ShowL a => a -> String -> String
showl (PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
forall (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
getTail PrivateClaims ((name ->> a) : tl) ns
pc)
instance Eq (PrivateClaims Empty any) where
PrivateClaims Empty any
_ == :: PrivateClaims Empty any -> PrivateClaims Empty any -> Bool
== PrivateClaims Empty any
_ = Bool
True
instance (Eq a, KnownSymbol name, Eq (PrivateClaims tl ns)) => Eq (PrivateClaims (name ->> a : tl) ns) where
PrivateClaims ((name ->> a) : tl) ns
pc1 == :: PrivateClaims ((name ->> a) : tl) ns
-> PrivateClaims ((name ->> a) : tl) ns -> Bool
== PrivateClaims ((name ->> a) : tl) ns
pc2 = PrivateClaims ((name ->> a) : tl) ns
pc1 PrivateClaims ((name ->> a) : tl) ns
-> ClaimName name -> LookupClaimType name ((name ->> a) : tl)
forall (name :: Symbol) (ts :: [Claim *]) (ns :: Namespace).
CanGet name ts =>
PrivateClaims ts ns -> ClaimName name -> LookupClaimType name ts
.! (ClaimName name
forall (name :: Symbol). ClaimName name
ClaimName @name) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== PrivateClaims ((name ->> a) : tl) ns
pc2 PrivateClaims ((name ->> a) : tl) ns
-> ClaimName name -> LookupClaimType name ((name ->> a) : tl)
forall (name :: Symbol) (ts :: [Claim *]) (ns :: Namespace).
CanGet name ts =>
PrivateClaims ts ns -> ClaimName name -> LookupClaimType name ts
.! (ClaimName name
forall (name :: Symbol). ClaimName name
ClaimName @name) Bool -> Bool -> Bool
&& PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
forall (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
getTail PrivateClaims ((name ->> a) : tl) ns
pc1 PrivateClaims tl ns -> PrivateClaims tl ns -> Bool
forall a. Eq a => a -> a -> Bool
== PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
forall (name :: Symbol) a (tl :: [Claim *]) (ns :: Namespace).
PrivateClaims ((name ->> a) : tl) ns -> PrivateClaims tl ns
getTail PrivateClaims ((name ->> a) : tl) ns
pc2
class ToPrivateClaims a where
type Claims a :: [Claim Type]
type Claims a = ClaimsFromRecord (Rep a)
type OutNs a :: Namespace
type OutNs a = 'NoNs
toPrivateClaims :: a -> PrivateClaims (Claims a) (OutNs a)
default toPrivateClaims
:: ( Generic a
, RecordToPrivateClaims (Rep a)
, Claims a ~ ClaimsFromRecord (Rep a)
, OutNs a ~ 'NoNs
)
=> a -> PrivateClaims (Claims a) (OutNs a)
toPrivateClaims = Rep a Any -> PrivateClaims (ClaimsFromRecord (Rep a)) 'NoNs
forall k (g :: k -> *) (p :: k).
RecordToPrivateClaims g =>
g p -> PrivateClaims (ClaimsFromRecord g) 'NoNs
genericToPrivateClaims (Rep a Any -> PrivateClaims (ClaimsFromRecord (Rep a)) 'NoNs)
-> (a -> Rep a Any)
-> a
-> PrivateClaims (ClaimsFromRecord (Rep a)) 'NoNs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from
class FromPrivateClaims a where
fromPrivateClaims :: ts ~ Claims a => PrivateClaims ts ns -> a
default fromPrivateClaims
:: ( Generic a
, RecordFromPrivateClaims (Rep a)
, ts ~ ClaimsFromRecord(Rep a)
)
=> PrivateClaims ts ns -> a
fromPrivateClaims = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (Rep a Any -> a)
-> (PrivateClaims ts ns -> Rep a Any) -> PrivateClaims ts ns -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrivateClaims ts ns -> Rep a Any
forall k (g :: k -> *) (ns :: Namespace) (p :: k).
RecordFromPrivateClaims g =>
PrivateClaims (ClaimsFromRecord g) ns -> g p
genericFromPrivateClaims
class RecordToPrivateClaims g where
type ClaimsFromRecord g :: [Claim Type]
genericToPrivateClaims :: g p -> PrivateClaims (ClaimsFromRecord g) 'NoNs
class RecordFromPrivateClaims g where
genericFromPrivateClaims :: PrivateClaims (ClaimsFromRecord g) ns -> g p
instance RecordToPrivateClaims c => RecordToPrivateClaims (D1 m c) where
type ClaimsFromRecord (D1 m c) = ClaimsFromRecord c
genericToPrivateClaims :: D1 m c p -> PrivateClaims (ClaimsFromRecord (D1 m c)) 'NoNs
genericToPrivateClaims (M1 c p
c) = c p -> PrivateClaims (ClaimsFromRecord c) 'NoNs
forall k (g :: k -> *) (p :: k).
RecordToPrivateClaims g =>
g p -> PrivateClaims (ClaimsFromRecord g) 'NoNs
genericToPrivateClaims c p
c
instance RecordFromPrivateClaims c => RecordFromPrivateClaims (D1 m c) where
genericFromPrivateClaims :: PrivateClaims (ClaimsFromRecord (D1 m c)) ns -> D1 m c p
genericFromPrivateClaims = c p -> D1 m c p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (c p -> D1 m c p)
-> (PrivateClaims (ClaimsFromRecord c) ns -> c p)
-> PrivateClaims (ClaimsFromRecord c) ns
-> D1 m c p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrivateClaims (ClaimsFromRecord c) ns -> c p
forall k (g :: k -> *) (ns :: Namespace) (p :: k).
RecordFromPrivateClaims g =>
PrivateClaims (ClaimsFromRecord g) ns -> g p
genericFromPrivateClaims
instance RecordToPrivateClaims f => RecordToPrivateClaims (C1 m f) where
type ClaimsFromRecord (C1 m f) = ClaimsFromRecord f
genericToPrivateClaims :: C1 m f p -> PrivateClaims (ClaimsFromRecord (C1 m f)) 'NoNs
genericToPrivateClaims (M1 f p
f) = f p -> PrivateClaims (ClaimsFromRecord f) 'NoNs
forall k (g :: k -> *) (p :: k).
RecordToPrivateClaims g =>
g p -> PrivateClaims (ClaimsFromRecord g) 'NoNs
genericToPrivateClaims f p
f
instance RecordFromPrivateClaims f => RecordFromPrivateClaims (C1 m f) where
genericFromPrivateClaims :: PrivateClaims (ClaimsFromRecord (C1 m f)) ns -> C1 m f p
genericFromPrivateClaims = f p -> C1 m f p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f p -> C1 m f p)
-> (PrivateClaims (ClaimsFromRecord f) ns -> f p)
-> PrivateClaims (ClaimsFromRecord f) ns
-> C1 m f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrivateClaims (ClaimsFromRecord f) ns -> f p
forall k (g :: k -> *) (ns :: Namespace) (p :: k).
RecordFromPrivateClaims g =>
PrivateClaims (ClaimsFromRecord g) ns -> g p
genericFromPrivateClaims
type family (+++) (lhs :: [k]) (rhs :: [k]) :: [k] where
'[] +++ rhs = rhs
(a : rest) +++ rhs = a : (rest +++ rhs)
instance (RecordToPrivateClaims s1, RecordToPrivateClaims s2) => RecordToPrivateClaims (s1 :*: s2) where
type ClaimsFromRecord (s1 :*: s2) = ClaimsFromRecord s1 +++ ClaimsFromRecord s2
genericToPrivateClaims :: (:*:) s1 s2 p -> PrivateClaims (ClaimsFromRecord (s1 :*: s2)) 'NoNs
genericToPrivateClaims (s1 p
s1 :*: s2 p
s2) = HashMap String Any
-> PrivateClaims
(ClaimsFromRecord s1 +++ ClaimsFromRecord s2) 'NoNs
forall (ts :: [Claim *]) (ns :: Namespace).
HashMap String Any -> PrivateClaims ts ns
PrivateClaims (HashMap String Any
-> PrivateClaims
(ClaimsFromRecord s1 +++ ClaimsFromRecord s2) 'NoNs)
-> HashMap String Any
-> PrivateClaims
(ClaimsFromRecord s1 +++ ClaimsFromRecord s2) 'NoNs
forall a b. (a -> b) -> a -> b
$ HashMap String Any -> HashMap String Any -> HashMap String Any
forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HashMap.union HashMap String Any
store1 HashMap String Any
store2
where
store1 :: HashMap String Any
store1 = PrivateClaims (ClaimsFromRecord s1) 'NoNs -> HashMap String Any
forall (ts :: [Claim *]) (ns :: Namespace).
PrivateClaims ts ns -> HashMap String Any
unsafeClaimsMap (PrivateClaims (ClaimsFromRecord s1) 'NoNs -> HashMap String Any)
-> PrivateClaims (ClaimsFromRecord s1) 'NoNs -> HashMap String Any
forall a b. (a -> b) -> a -> b
$ s1 p -> PrivateClaims (ClaimsFromRecord s1) 'NoNs
forall k (g :: k -> *) (p :: k).
RecordToPrivateClaims g =>
g p -> PrivateClaims (ClaimsFromRecord g) 'NoNs
genericToPrivateClaims s1 p
s1
store2 :: HashMap String Any
store2 = PrivateClaims (ClaimsFromRecord s2) 'NoNs -> HashMap String Any
forall (ts :: [Claim *]) (ns :: Namespace).
PrivateClaims ts ns -> HashMap String Any
unsafeClaimsMap (PrivateClaims (ClaimsFromRecord s2) 'NoNs -> HashMap String Any)
-> PrivateClaims (ClaimsFromRecord s2) 'NoNs -> HashMap String Any
forall a b. (a -> b) -> a -> b
$ s2 p -> PrivateClaims (ClaimsFromRecord s2) 'NoNs
forall k (g :: k -> *) (p :: k).
RecordToPrivateClaims g =>
g p -> PrivateClaims (ClaimsFromRecord g) 'NoNs
genericToPrivateClaims s2 p
s2
instance (RecordFromPrivateClaims s1, RecordFromPrivateClaims s2) => RecordFromPrivateClaims (s1 :*: s2) where
genericFromPrivateClaims :: PrivateClaims (ClaimsFromRecord (s1 :*: s2)) ns -> (:*:) s1 s2 p
genericFromPrivateClaims PrivateClaims (ClaimsFromRecord (s1 :*: s2)) ns
pc = s1 p
s1 s1 p -> s2 p -> (:*:) s1 s2 p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: s2 p
s2 where
s1 :: s1 p
s1 = PrivateClaims (ClaimsFromRecord s1) Any -> s1 p
forall k (g :: k -> *) (ns :: Namespace) (p :: k).
RecordFromPrivateClaims g =>
PrivateClaims (ClaimsFromRecord g) ns -> g p
genericFromPrivateClaims (PrivateClaims (ClaimsFromRecord s1 +++ ClaimsFromRecord s2) ns
-> PrivateClaims (ClaimsFromRecord s1) Any
coerce PrivateClaims (ClaimsFromRecord s1 +++ ClaimsFromRecord s2) ns
PrivateClaims (ClaimsFromRecord (s1 :*: s2)) ns
pc)
s2 :: s2 p
s2 = PrivateClaims (ClaimsFromRecord s2) Any -> s2 p
forall k (g :: k -> *) (ns :: Namespace) (p :: k).
RecordFromPrivateClaims g =>
PrivateClaims (ClaimsFromRecord g) ns -> g p
genericFromPrivateClaims (PrivateClaims (ClaimsFromRecord s1 +++ ClaimsFromRecord s2) ns
-> PrivateClaims (ClaimsFromRecord s2) Any
coerce PrivateClaims (ClaimsFromRecord s1 +++ ClaimsFromRecord s2) ns
PrivateClaims (ClaimsFromRecord (s1 :*: s2)) ns
pc)
type family HasSelectorName (m :: Meta) :: Constraint where
HasSelectorName ('MetaSel ('Just s) _ _ _) = ()
HasSelectorName _ = TypeError
( 'Text "Only records with named fields can be converted to PrivateClaims. For instance, "
':$$:
'Text "data Good = MkGood { a :: Int, b :: String } is ok, but "
':$$:
'Text "data Bad = MkBad Int String is not"
)
type family SelectorName (m :: Meta) :: Symbol where
SelectorName ('MetaSel ('Just s) _ _ _) = s
instance (Selector s, HasSelectorName s) => RecordToPrivateClaims (S1 s (Rec0 a)) where
type ClaimsFromRecord (S1 s (Rec0 a)) = '[SelectorName s ->> a]
genericToPrivateClaims :: S1 s (Rec0 a) p
-> PrivateClaims (ClaimsFromRecord (S1 s (Rec0 a))) 'NoNs
genericToPrivateClaims (M1 (K1 a
a)) = HashMap String Any
-> PrivateClaims ((SelectorName s ->> a) : Empty) 'NoNs
forall (ts :: [Claim *]) (ns :: Namespace).
HashMap String Any -> PrivateClaims ts ns
PrivateClaims (HashMap String Any
-> PrivateClaims ((SelectorName s ->> a) : Empty) 'NoNs)
-> HashMap String Any
-> PrivateClaims ((SelectorName s ->> a) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$ String -> Any -> HashMap String Any
forall k v. Hashable k => k -> v -> HashMap k v
HashMap.singleton String
fieldName (Any -> HashMap String Any) -> Any -> HashMap String Any
forall a b. (a -> b) -> a -> b
$ a -> Any
forall a. a -> Any
Any a
a
where
fieldName :: String
fieldName = Proxy (M1 S s (Rec0 a) Any) -> String
forall k1 k2 (proxy :: * -> *) (t :: k1 -> (k2 -> *) -> k2 -> *)
(s :: k1) (f :: k2 -> *) (a :: k2).
Selector s =>
proxy (t s f a) -> String
selNameProxied (forall k (t :: k). Proxy t
forall k (p :: k). Proxy (S1 s (Rec0 a) p)
Proxy :: Proxy (S1 s (Rec0 a) p))
instance (Selector s, HasSelectorName s) => RecordFromPrivateClaims (S1 s (Rec0 a)) where
genericFromPrivateClaims :: PrivateClaims (ClaimsFromRecord (S1 s (Rec0 a))) ns
-> S1 s (Rec0 a) p
genericFromPrivateClaims = K1 R a p -> S1 s (Rec0 a) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (K1 R a p -> S1 s (Rec0 a) p)
-> (PrivateClaims ((SelectorName s ->> a) : Empty) ns -> K1 R a p)
-> PrivateClaims ((SelectorName s ->> a) : Empty) ns
-> S1 s (Rec0 a) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> K1 R a p
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 R a p)
-> (PrivateClaims ((SelectorName s ->> a) : Empty) ns -> a)
-> PrivateClaims ((SelectorName s ->> a) : Empty) ns
-> K1 R a p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> PrivateClaims ((SelectorName s ->> a) : Empty) ns -> a
forall (ts :: [Claim *]) (ns :: Namespace) p.
String -> PrivateClaims ts ns -> p
unsafeLookup String
fieldName
where
fieldName :: String
fieldName = Proxy (M1 S s (Rec0 a) Any) -> String
forall k1 k2 (proxy :: * -> *) (t :: k1 -> (k2 -> *) -> k2 -> *)
(s :: k1) (f :: k2 -> *) (a :: k2).
Selector s =>
proxy (t s f a) -> String
selNameProxied (forall k (t :: k). Proxy t
forall k (p :: k). Proxy (S1 s (Rec0 a) p)
Proxy :: Proxy (S1 s (Rec0 a) p))
instance
( TypeError
( 'Text "Only records with named fields can be converted to PrivateClaims. For instance, "
':$$:
'Text "data Good = MkGood { a :: Int, b :: String } is ok, but "
':$$:
'Text "data Bad = Bad1 Int | Bad2 String is not"
)
)
=> RecordToPrivateClaims (any :+: thing) where
genericToPrivateClaims :: (:+:) any thing p
-> PrivateClaims (ClaimsFromRecord (any :+: thing)) 'NoNs
genericToPrivateClaims = String
-> (:+:) any thing p
-> PrivateClaims (ClaimsFromRecord (any :+: thing)) 'NoNs
forall a. HasCallStack => String -> a
error String
"impossible"
instance
( TypeError
( 'Text "Only records with named fields can be constructed from PrivateClaims. For instance, "
':$$:
'Text "data Good = MkGood { a :: Int, b :: String } is ok, but "
':$$:
'Text "data Bad = Bad1 Int | Bad2 String is not"
)
)
=> RecordFromPrivateClaims (any :+: thing) where
genericFromPrivateClaims :: PrivateClaims (ClaimsFromRecord (any :+: thing)) ns
-> (:+:) any thing p
genericFromPrivateClaims = String
-> PrivateClaims (ClaimsFromRecord (any :+: thing)) ns
-> (:+:) any thing p
forall a. HasCallStack => String -> a
error String
"impossible"
instance ToPrivateClaims () where
type Claims () = Empty
toPrivateClaims :: () -> PrivateClaims (Claims ()) (OutNs ())
toPrivateClaims ()
_ = PrivateClaims Empty 'NoNs
PrivateClaims (Claims ()) (OutNs ())
nullClaims
instance CanAdd n '[] => ToPrivateClaims (ClaimWitness n a) where
type Claims (ClaimWitness n a) = '[n ->> a]
toPrivateClaims :: ClaimWitness n a
-> PrivateClaims
(Claims (ClaimWitness n a)) (OutNs (ClaimWitness n a))
toPrivateClaims (Witness a
a) = ClaimName n
-> a
-> PrivateClaims Empty 'NoNs
-> PrivateClaims ((n ->> a) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n
forall (name :: Symbol). ClaimName name
ClaimName a
a PrivateClaims Empty 'NoNs
nullClaims
instance (CanAdd n2 '[], CanAdd n1 '[n2 ->> b]) => ToPrivateClaims (ClaimWitness n1 a, ClaimWitness n2 b) where
type Claims (ClaimWitness n1 a, ClaimWitness n2 b) = '[n1 ->> a, n2 ->> b]
toPrivateClaims :: (ClaimWitness n1 a, ClaimWitness n2 b)
-> PrivateClaims
(Claims (ClaimWitness n1 a, ClaimWitness n2 b))
(OutNs (ClaimWitness n1 a, ClaimWitness n2 b))
toPrivateClaims (Witness a
a, Witness b
b) =
ClaimName n1
-> a
-> PrivateClaims ((n2 ->> b) : Empty) 'NoNs
-> PrivateClaims ((n1 ->> a) : (n2 ->> b) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n1
forall (name :: Symbol). ClaimName name
ClaimName a
a (PrivateClaims ((n2 ->> b) : Empty) 'NoNs
-> PrivateClaims ((n1 ->> a) : (n2 ->> b) : Empty) 'NoNs)
-> PrivateClaims ((n2 ->> b) : Empty) 'NoNs
-> PrivateClaims ((n1 ->> a) : (n2 ->> b) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$ ClaimName n2
-> b
-> PrivateClaims Empty 'NoNs
-> PrivateClaims ((n2 ->> b) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n2
forall (name :: Symbol). ClaimName name
ClaimName b
b PrivateClaims Empty 'NoNs
nullClaims
instance (KnownSymbol n1, KnownSymbol n2) => FromPrivateClaims (ClaimWitness n1 a, ClaimWitness n2 b) where
fromPrivateClaims :: PrivateClaims ts ns -> (ClaimWitness n1 a, ClaimWitness n2 b)
fromPrivateClaims (a :< b :< _) = (a -> ClaimWitness n1 a
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness a
a, b -> ClaimWitness n2 b
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness b
b)
instance
( CanAdd n1 '[n2 ->> b, n3 ->> c]
, CanAdd n2 '[n3 ->> c]
, CanAdd n3 '[]
)
=> ToPrivateClaims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c) where
type Claims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c) = '[n1 ->> a, n2 ->> b, n3 ->> c]
toPrivateClaims :: (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c)
-> PrivateClaims
(Claims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c))
(OutNs (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c))
toPrivateClaims (Witness a
a, Witness b
b, Witness c
c) =
ClaimName n1
-> a
-> PrivateClaims ((n2 ->> b) : (n3 ->> c) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a) : (n2 ->> b) : (n3 ->> c) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n1
forall (name :: Symbol). ClaimName name
ClaimName a
a (PrivateClaims ((n2 ->> b) : (n3 ->> c) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a) : (n2 ->> b) : (n3 ->> c) : Empty) 'NoNs)
-> PrivateClaims ((n2 ->> b) : (n3 ->> c) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a) : (n2 ->> b) : (n3 ->> c) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n2
-> b
-> PrivateClaims ((n3 ->> c) : Empty) 'NoNs
-> PrivateClaims ((n2 ->> b) : (n3 ->> c) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n2
forall (name :: Symbol). ClaimName name
ClaimName b
b (PrivateClaims ((n3 ->> c) : Empty) 'NoNs
-> PrivateClaims ((n2 ->> b) : (n3 ->> c) : Empty) 'NoNs)
-> PrivateClaims ((n3 ->> c) : Empty) 'NoNs
-> PrivateClaims ((n2 ->> b) : (n3 ->> c) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n3
-> c
-> PrivateClaims Empty 'NoNs
-> PrivateClaims ((n3 ->> c) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n3
forall (name :: Symbol). ClaimName name
ClaimName c
c PrivateClaims Empty 'NoNs
nullClaims
instance
( KnownSymbol n1
, KnownSymbol n2
, KnownSymbol n3
) => FromPrivateClaims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c) where
fromPrivateClaims :: PrivateClaims ts ns
-> (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c)
fromPrivateClaims (a :< b :< c :< _) = (a -> ClaimWitness n1 a
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness a
a, b -> ClaimWitness n2 b
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness b
b ,c -> ClaimWitness n3 c
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness c
c)
instance
( CanAdd n1 '[n2 ->> b, n3 ->> c, n4 ->> d]
, CanAdd n2 '[n3 ->> c, n4 ->> d]
, CanAdd n3 '[n4 ->> d]
, CanAdd n4 '[]
)
=> ToPrivateClaims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c, ClaimWitness n4 d) where
type Claims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c, ClaimWitness n4 d) = '[n1 ->> a, n2 ->> b, n3 ->> c, n4 ->> d]
toPrivateClaims :: (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d)
-> PrivateClaims
(Claims
(ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d))
(OutNs
(ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d))
toPrivateClaims (Witness a
a, Witness b
b, Witness c
c, Witness d
d) =
ClaimName n1
-> a
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a) : (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n1
forall (name :: Symbol). ClaimName name
ClaimName a
a (PrivateClaims ((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a) : (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs)
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a) : (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n2
-> b
-> PrivateClaims ((n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n2
forall (name :: Symbol). ClaimName name
ClaimName b
b (PrivateClaims ((n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs)
-> PrivateClaims ((n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n3
-> c
-> PrivateClaims ((n4 ->> d) : Empty) 'NoNs
-> PrivateClaims ((n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n3
forall (name :: Symbol). ClaimName name
ClaimName c
c (PrivateClaims ((n4 ->> d) : Empty) 'NoNs
-> PrivateClaims ((n3 ->> c) : (n4 ->> d) : Empty) 'NoNs)
-> PrivateClaims ((n4 ->> d) : Empty) 'NoNs
-> PrivateClaims ((n3 ->> c) : (n4 ->> d) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n4
-> d
-> PrivateClaims Empty 'NoNs
-> PrivateClaims ((n4 ->> d) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n4
forall (name :: Symbol). ClaimName name
ClaimName d
d PrivateClaims Empty 'NoNs
nullClaims
instance
( KnownSymbol n1
, KnownSymbol n2
, KnownSymbol n3
, KnownSymbol n4
)
=> FromPrivateClaims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c, ClaimWitness n4 d) where
fromPrivateClaims :: PrivateClaims ts ns
-> (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d)
fromPrivateClaims (a :< b :< c :< d :< _) =
(a -> ClaimWitness n1 a
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness a
a, b -> ClaimWitness n2 b
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness b
b, c -> ClaimWitness n3 c
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness c
c, d -> ClaimWitness n4 d
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness d
d)
instance
( CanAdd n1 '[n2 ->> b, n3 ->> c, n4 ->> d, n5 ->> e]
, CanAdd n2 '[n3 ->> c, n4 ->> d, n5 ->> e]
, CanAdd n3 '[n4 ->> d, n5 ->> e]
, CanAdd n4 '[n5 ->> e]
, CanAdd n5 '[]
)
=> ToPrivateClaims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c, ClaimWitness n4 d, ClaimWitness n5 e) where
type Claims
( ClaimWitness n1 a
, ClaimWitness n2 b
, ClaimWitness n3 c
, ClaimWitness n4 d
, ClaimWitness n5 e) = '[n1 ->> a, n2 ->> b, n3 ->> c, n4 ->> d, n5 ->> e]
toPrivateClaims :: (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e)
-> PrivateClaims
(Claims
(ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e))
(OutNs
(ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e))
toPrivateClaims (Witness a
a, Witness b
b, Witness c
c, Witness d
d, Witness e
e) =
ClaimName n1
-> a
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty)
'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n1
forall (name :: Symbol). ClaimName name
ClaimName a
a (PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty)
'NoNs)
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty)
'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n2
-> b
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n2
forall (name :: Symbol). ClaimName name
ClaimName b
b (PrivateClaims ((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs)
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n3
-> c
-> PrivateClaims ((n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n3
forall (name :: Symbol). ClaimName name
ClaimName c
c (PrivateClaims ((n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs)
-> PrivateClaims ((n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n4
-> d
-> PrivateClaims ((n5 ->> e) : Empty) 'NoNs
-> PrivateClaims ((n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n4
forall (name :: Symbol). ClaimName name
ClaimName d
d (PrivateClaims ((n5 ->> e) : Empty) 'NoNs
-> PrivateClaims ((n4 ->> d) : (n5 ->> e) : Empty) 'NoNs)
-> PrivateClaims ((n5 ->> e) : Empty) 'NoNs
-> PrivateClaims ((n4 ->> d) : (n5 ->> e) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n5
-> e
-> PrivateClaims Empty 'NoNs
-> PrivateClaims ((n5 ->> e) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n5
forall (name :: Symbol). ClaimName name
ClaimName e
e PrivateClaims Empty 'NoNs
nullClaims
instance
( KnownSymbol n1
, KnownSymbol n2
, KnownSymbol n3
, KnownSymbol n4
, KnownSymbol n5
)
=> FromPrivateClaims (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c, ClaimWitness n4 d, ClaimWitness n5 e) where
fromPrivateClaims :: PrivateClaims ts ns
-> (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e)
fromPrivateClaims (a :< b :< c :< d :< e :< _) = (a -> ClaimWitness n1 a
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness a
a, b -> ClaimWitness n2 b
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness b
b, c -> ClaimWitness n3 c
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness c
c, d -> ClaimWitness n4 d
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness d
d, e -> ClaimWitness n5 e
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness e
e)
instance
( CanAdd n1 '[n2 ->> b, n3 ->> c, n4 ->> d, n5 ->> e, n6 ->> f]
, CanAdd n2 '[n3 ->> c, n4 ->> d, n5 ->> e, n6 ->> f]
, CanAdd n3 '[n4 ->> d, n5 ->> e, n6 ->> f]
, CanAdd n4 '[n5 ->> e, n6 ->> f]
, CanAdd n5 '[n6 ->> f]
, CanAdd n6 '[]
)
=> ToPrivateClaims
( ClaimWitness n1 a
, ClaimWitness n2 b
, ClaimWitness n3 c
, ClaimWitness n4 d
, ClaimWitness n5 e
, ClaimWitness n6 f) where
type Claims
( ClaimWitness n1 a
, ClaimWitness n2 b
, ClaimWitness n3 c
, ClaimWitness n4 d
, ClaimWitness n5 e
, ClaimWitness n6 f) = '[n1 ->> a, n2 ->> b, n3 ->> c, n4 ->> d, n5 ->> e, n6 ->> f]
toPrivateClaims :: (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e, ClaimWitness n6 f)
-> PrivateClaims
(Claims
(ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e, ClaimWitness n6 f))
(OutNs
(ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e, ClaimWitness n6 f))
toPrivateClaims (Witness a
a, Witness b
b, Witness c
c, Witness d
d, Witness e
e, Witness f
f) =
ClaimName n1
-> a
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty)
'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f)
: Empty)
'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n1
forall (name :: Symbol). ClaimName name
ClaimName a
a (PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty)
'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f)
: Empty)
'NoNs)
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty)
'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f)
: Empty)
'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n2
-> b
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty)
'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n2
forall (name :: Symbol). ClaimName name
ClaimName b
b (PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty)
'NoNs)
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty)
'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n3
-> c
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n3
forall (name :: Symbol). ClaimName name
ClaimName c
c (PrivateClaims ((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs)
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n4
-> d
-> PrivateClaims ((n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n4
forall (name :: Symbol). ClaimName name
ClaimName d
d (PrivateClaims ((n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs)
-> PrivateClaims ((n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n5
-> e
-> PrivateClaims ((n6 ->> f) : Empty) 'NoNs
-> PrivateClaims ((n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n5
forall (name :: Symbol). ClaimName name
ClaimName e
e (PrivateClaims ((n6 ->> f) : Empty) 'NoNs
-> PrivateClaims ((n5 ->> e) : (n6 ->> f) : Empty) 'NoNs)
-> PrivateClaims ((n6 ->> f) : Empty) 'NoNs
-> PrivateClaims ((n5 ->> e) : (n6 ->> f) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n6
-> f
-> PrivateClaims Empty 'NoNs
-> PrivateClaims ((n6 ->> f) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n6
forall (name :: Symbol). ClaimName name
ClaimName f
f PrivateClaims Empty 'NoNs
nullClaims
instance
( KnownSymbol n1
, KnownSymbol n2
, KnownSymbol n3
, KnownSymbol n4
, KnownSymbol n5
, KnownSymbol n6
)
=> FromPrivateClaims
( ClaimWitness n1 a
, ClaimWitness n2 b
, ClaimWitness n3 c
, ClaimWitness n4 d
, ClaimWitness n5 e
, ClaimWitness n6 f) where
fromPrivateClaims :: PrivateClaims ts ns
-> (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e, ClaimWitness n6 f)
fromPrivateClaims (a :< b :< c :< d :< e :< f :< _) =
(a -> ClaimWitness n1 a
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness a
a, b -> ClaimWitness n2 b
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness b
b, c -> ClaimWitness n3 c
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness c
c, d -> ClaimWitness n4 d
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness d
d, e -> ClaimWitness n5 e
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness e
e, f -> ClaimWitness n6 f
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness f
f)
instance
( CanAdd n1 '[n2 ->> b, n3 ->> c, n4 ->> d, n5 ->> e, n6 ->> f, n7 ->> g]
, CanAdd n2 '[n3 ->> c, n4 ->> d, n5 ->> e, n6 ->> f, n7 ->> g]
, CanAdd n3 '[n4 ->> d, n5 ->> e, n6 ->> f, n7 ->> g]
, CanAdd n4 '[n5 ->> e, n6 ->> f, n7 ->> g]
, CanAdd n5 '[n6 ->> f, n7 ->> g]
, CanAdd n6 '[n7 ->> g]
, CanAdd n7 '[]
)
=> ToPrivateClaims
( ClaimWitness n1 a
, ClaimWitness n2 b
, ClaimWitness n3 c
, ClaimWitness n4 d
, ClaimWitness n5 e
, ClaimWitness n6 f
, ClaimWitness n7 g) where
type Claims
( ClaimWitness n1 a
, ClaimWitness n2 b
, ClaimWitness n3 c
, ClaimWitness n4 d
, ClaimWitness n5 e
, ClaimWitness n6 f
, ClaimWitness n7 g) = '[n1 ->> a, n2 ->> b, n3 ->> c, n4 ->> d, n5 ->> e, n6 ->> f, n7 ->> g]
toPrivateClaims :: (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e, ClaimWitness n6 f,
ClaimWitness n7 g)
-> PrivateClaims
(Claims
(ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e, ClaimWitness n6 f,
ClaimWitness n7 g))
(OutNs
(ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e, ClaimWitness n6 f,
ClaimWitness n7 g))
toPrivateClaims (Witness a
a, Witness b
b, Witness c
c, Witness d
d, Witness e
e, Witness f
f, Witness g
g) =
ClaimName n1
-> a
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g)
: Empty)
'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f)
: (n7 ->> g) : Empty)
'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n1
forall (name :: Symbol). ClaimName name
ClaimName a
a (PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g)
: Empty)
'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f)
: (n7 ->> g) : Empty)
'NoNs)
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g)
: Empty)
'NoNs
-> PrivateClaims
((n1 ->> a)
: (n2 ->> b) : (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f)
: (n7 ->> g) : Empty)
'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n2
-> b
-> PrivateClaims
((n3 ->> c)
: (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty)
'NoNs
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g)
: Empty)
'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n2
forall (name :: Symbol). ClaimName name
ClaimName b
b (PrivateClaims
((n3 ->> c)
: (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty)
'NoNs
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g)
: Empty)
'NoNs)
-> PrivateClaims
((n3 ->> c)
: (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty)
'NoNs
-> PrivateClaims
((n2 ->> b)
: (n3 ->> c) : (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g)
: Empty)
'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n3
-> c
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c)
: (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty)
'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n3
forall (name :: Symbol). ClaimName name
ClaimName c
c (PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c)
: (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty)
'NoNs)
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n3 ->> c)
: (n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty)
'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n4
-> d
-> PrivateClaims
((n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n4
forall (name :: Symbol). ClaimName name
ClaimName d
d (PrivateClaims ((n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs)
-> PrivateClaims
((n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n4 ->> d) : (n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n5
-> e
-> PrivateClaims ((n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n5
forall (name :: Symbol). ClaimName name
ClaimName e
e (PrivateClaims ((n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs)
-> PrivateClaims ((n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
-> PrivateClaims
((n5 ->> e) : (n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n6
-> f
-> PrivateClaims ((n7 ->> g) : Empty) 'NoNs
-> PrivateClaims ((n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n6
forall (name :: Symbol). ClaimName name
ClaimName f
f (PrivateClaims ((n7 ->> g) : Empty) 'NoNs
-> PrivateClaims ((n6 ->> f) : (n7 ->> g) : Empty) 'NoNs)
-> PrivateClaims ((n7 ->> g) : Empty) 'NoNs
-> PrivateClaims ((n6 ->> f) : (n7 ->> g) : Empty) 'NoNs
forall a b. (a -> b) -> a -> b
$
ClaimName n7
-> g
-> PrivateClaims Empty 'NoNs
-> PrivateClaims ((n7 ->> g) : Empty) 'NoNs
forall (name :: Symbol) a (ts :: [Claim *]) (ns :: Namespace).
CanAdd name ts =>
ClaimName name
-> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) : ts) ns
addClaim ClaimName n7
forall (name :: Symbol). ClaimName name
ClaimName g
g PrivateClaims Empty 'NoNs
nullClaims
instance
( KnownSymbol n1
, KnownSymbol n2
, KnownSymbol n3
, KnownSymbol n4
, KnownSymbol n5
, KnownSymbol n6
, KnownSymbol n7
)
=> FromPrivateClaims
( ClaimWitness n1 a
, ClaimWitness n2 b
, ClaimWitness n3 c
, ClaimWitness n4 d
, ClaimWitness n5 e
, ClaimWitness n6 f
, ClaimWitness n7 g) where
fromPrivateClaims :: PrivateClaims ts ns
-> (ClaimWitness n1 a, ClaimWitness n2 b, ClaimWitness n3 c,
ClaimWitness n4 d, ClaimWitness n5 e, ClaimWitness n6 f,
ClaimWitness n7 g)
fromPrivateClaims (a :< b :< c :< d :< e :< f :< g :< _) =
(a -> ClaimWitness n1 a
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness a
a, b -> ClaimWitness n2 b
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness b
b, c -> ClaimWitness n3 c
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness c
c, d -> ClaimWitness n4 d
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness d
d, e -> ClaimWitness n5 e
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness e
e, f -> ClaimWitness n6 f
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness f
f, g -> ClaimWitness n7 g
forall (name :: Symbol) a. a -> ClaimWitness name a
Witness g
g)
instance ToPrivateClaims (PrivateClaims ts ns) where
type Claims (PrivateClaims ts ns) = ts
type OutNs (PrivateClaims ts ns) = ns
toPrivateClaims :: PrivateClaims ts ns
-> PrivateClaims
(Claims (PrivateClaims ts ns)) (OutNs (PrivateClaims ts ns))
toPrivateClaims = PrivateClaims ts ns
-> PrivateClaims
(Claims (PrivateClaims ts ns)) (OutNs (PrivateClaims ts ns))
forall a. a -> a
id