--   This Source Code Form is subject to the terms of the Mozilla Public
--   License, v. 2.0. If a copy of the MPL was not distributed with this
--   file, You can obtain one at http://mozilla.org/MPL/2.0/.

{-# 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 #-}

-- | Collection of functions, types and type families that are needed to implement type-safe private claims.
--
--   This is essentially an implementation of /open product/ type as described in Sandy Maguire "Thinking with Types".
--   The only difference to the book is that the implementation is backed by HashMap to make lookups by name easier.
--   In addition, there are also 'FromPrivateClaims' and 'ToPrivateClaims' type-classes and 
--   /view pattern/ ':<' to help create and deconstruct values.
module Libjwt.PrivateClaims
  ( 
    -- * Kinds
    Claim(..)
  , type (->>)
  , Namespace(..)
  , KnownNamespace(..)
  -- * Value-level counterparts
  , ClaimName(..)
  , claimNameVal
  , Ns(..)
  , ClaimWitness
  , testify
  , (->>)
  -- * Private claims type
  , PrivateClaims
  , type Empty
  -- * Construction
  , nullClaims
  , addClaim
  , (.:)
  , CanAdd
  , RestrictedName
  -- * Lookup
  , getClaim
  , (.!)
  , CanGet
  , LookupClaimType
  -- * Patern matching
  , pattern (:<)
  -- * Namespaces
  , withNs
  , someNs
  , noNs
  -- * Conversions
  , 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 :<

-- | Kind of claims
--   
--   A claim is made up of a type-level literal and a type (this is essentialy a /type-level tuple/ @(Symbol, *)@)
data Claim (a :: Type) = Grant Symbol a

-- | A convenient alias.
--   Let's you write @'["claimName" ->> Int, "anotherName" ->> String]@ to indicate a list of types of kind 'Claim',
--   instead of @'[Grant "claimName" Int, Grant "anotherName" String]@,
--   
type name ->> a = 'Grant name a

-- | Kind of namespaces
--
--   These types represent a URL-like claim prefix
data Namespace = NoNs | SomeNs Symbol

-- | Class of 'Namespace' with known compile-time value
class KnownNamespace (ns :: Namespace) where
  -- | Convert namespace to a string (if any)
  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)

-- | Type-level literal representing a claim name
--
--   Can be used with @-XOverloadedLabels@
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

-- | Retrieve the string associated with '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)

-- | Type-level literal representing a namespace
--
--   Can be used with @-XOverloadedLabels@ 
--  (the limited label syntax makes this rarely possibble though, a more common use is to write /Ns @"https://example.com"/)
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

-- | Keeps the value of type @a@ and the name (type-level) with which it is associated
newtype ClaimWitness (name :: Symbol) a = Witness { ClaimWitness name a -> a
testify :: a }

-- | Associate @name@ with a value
--
--   With @-XOverloadedLabels@
--
-- >>> :t #someName ->> True
-- #someName ->> True :: ClaimWitness "someName" Bool
(->>) :: 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

-- | Container of named claims @ts@, possibly prefixed with some namespace @ns@
--   
--   For example @PrivateClaims '["string" t'->>' String, "int" t'->>' Int] ''NoNs'@ denotes a structure containing
--   a String under the "string" key plus an int under the "int" key.
--   There is no namespace, so the keys will not be prefixed by any prefix when serializing the structure
newtype PrivateClaims (ts :: [Claim Type]) (ns :: Namespace) = PrivateClaims { PrivateClaims ts ns -> HashMap String Any
unsafeClaimsMap :: HashMap String Any }

type Empty = ('[] :: [Claim Type])

-- | Empty claims
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

-- | Insert the claim.
--
--   The claim can be safely added iff:
--
--       * there is no claim of the same @name@ in the container,
--       * its name is not the name of any public claim (like /iss/ or /sub/)
--
--   Otherwise it is a compile-time error (see 'CanAdd' constraint)
--   
--   With @-XOverloadedLabels@
--
-- >>> addClaim #string "Value of claim" nullClaims
-- (#string ->> "Value of claim")
--
--   With @-XTypeApplications@ and @-XDataKinds@
--
-- >>> addClaim (ClaimName @"string") "Value of claim" nullClaims
-- (#string ->> "Value of claim")
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)

-- | Alias for 'addClaim' (binds to the right)
--
--   With @-XOverloadedLabels@
--
-- >>> #string ->> "Value of claim" .: nullClaims
-- (#string ->> "Value of claim")
(.:)
  :: 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

-- | Constraint specifying when a claim named @n@ can be added to the list of claims @ns@
--
--   Satisfied iff:
--
--       * @n@ is a type-level literal,
--       * in the names of @ns@ claims there is no @n@ (uniqueness),
--       * @n@ is not one of the restricted names (see 'RestrictedName')
--
-- >>> :kind! CanAdd "name" '["n1" ->> Int, "n2" ->> String]
-- CanAdd "name" '["n1" ->> Int, "n2" ->> String] :: Constraint
-- = (GHC.TypeLits.KnownSymbol "name", () :: Constraint,
--   () :: Constraint)
--
-- >>> :kind! CanAdd "n1" '["n1" ->> Int, "n2" ->> String]
-- CanAdd "n1" '["n1" ->> Int, "n2" ->> String] :: Constraint
-- = (GHC.TypeLits.KnownSymbol "n1", () :: Constraint,
--   (TypeError ...))
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

-- | Look up the claim value associated with @name@.
--
--   Value can be retrieved if proven to exists in the container.
--   Otherwise it is a compile-time error (see 'CanGet' constraint)
--   
--   With @-XOverloadedLabels@
--
-- >>> getClaim #bool $ #string ->> "Value of claim" .: #bool ->> False .: nullClaims
-- False
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 #-}

-- | Alias for 'getClaim' (container goes first)
--
--   With @-XOverloadedLabels@
--
-- >>> (#string ->> "Value of claim" .: #bool ->> False .: nullClaims) .! #bool
-- False
(.!)
  :: 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

-- | Constraint specifying when a claim named @n@ can be looked up in the list of claims @ns@
--
--   Satisfied iff @ns@ contains a claim named @n@ and @n@ is a type-level literal
--
-- >>> :kind! CanGet "n1" '["n1" ->> Int, "n2" ->> String]
-- CanGet "n1" '["n1" ->> Int, "n2" ->> String] :: Constraint
-- = (GHC.TypeLits.KnownSymbol "n1", () :: Constraint)
--
-- >>> :kind! CanGet "n" '["n1" ->> Int, "n2" ->> String]
-- CanGet "n" '["n1" ->> Int, "n2" ->> String] :: Constraint
-- = (GHC.TypeLits.KnownSymbol "n", (TypeError ...))
type family CanGet n ns :: Constraint where
  CanGet n ns = (KnownSymbol n, RequireExists (NameExists n ns) n)

-- | Looks up the type associated with @name@ in the @'[n1 t'->>' a, n2 t'->>' b, ...]@ pairs list. Gets stuck if @name@ is not in @ts@
--
-- >>> :kind! LookupClaimType "n1" '["n1" ->> Int, "n2" ->> String]
-- LookupClaimType "n1" '["n1" ->> Int, "n2" ->> String] :: *
-- = Int
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

-- | Extract values from the container in the order in which they appear in the claim list
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 #-}

-- | Convert to private claims with some namespace
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

-- | Set namespace
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

-- | Unset namespace
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 of types that can be converted to 'PrivateClaims'
class ToPrivateClaims a where
  type Claims a :: [Claim Type]
  type Claims a = ClaimsFromRecord (Rep a)

  type OutNs a :: Namespace
  type OutNs a = 'NoNs

  -- | Convert to claims
  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 of types that can be constructed from @PrivateClaims@
class FromPrivateClaims a where
  -- | Convert from claims
  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