UVerb support?

[GulinSS]

As I see from the code Servant Auth does not support UVerb still.

I would like to try implement this support if nobody has free time for that but I need help from where and what I should start.

[GulinSS]

I did the following:

type A :: Type -> Type
type family A a where
  A (WithStatus n (Headers ls a)) = WithStatus n (Headers (Header "Set-Cookie" SetCookie ': ls) a)
  A (WithStatus n a) = WithStatus n (Headers '[Header "Set-Cookie" SetCookie] a)
  A (Headers ls a) = Headers (Header "Set-Cookie" SetCookie ': ls) a
  A a = Headers '[Header "Set-Cookie" SetCookie] a

type AddSetCookieApiUVerb :: [Type] -> [Type]
type family AddSetCookieApiUVerb a where
  AddSetCookieApiUVerb '[] = '[]
  AddSetCookieApiUVerb (a:as) = A a : AddSetCookieApiUVerb as

type instance AddSetCookieApi (UVerb method ctyps a)
  = UVerb method ctyps (AddSetCookieApiUVerb a)

But after that I was needed to write

instance {-# OVERLAPPABLE #-}
  ( Applicative m, ... ) => AddSetCookies ('S n) (m (Union oldA)) (m (Union newA))  where
  addSetCookies (mCookie `SetCookieCons` rest) oldVal =
    case mCookie of
      Nothing     -> ...
      Just cookie -> ...

I need help with writing constraints to let haskell deduce them.

I tried these:

  ( Applicative m
  , IsMember old oldA
  , IsMember cookied cookiedA
  , IsMember new newA
  , oldU ~ Union oldA
  , cookiedU ~ Union cookiedA
  , newU ~ Union newA
  , cookied ~ new
  , AddSetCookies n (m (Union oldA)) (m (Union cookiedA))
  , AddHeader "Set-Cookie" SetCookie cookied new
  ) => AddSetCookies ('S n) (m (Union oldA)) (m (Union newA))  where

But still getting issues with

[Sorokin-Anton]

Obviosly< it is not enough that one of new Union elements is correct Header of one of old Union elements. I will try to use constraint like this, it compiles with undefined:
(Also I added new row to A for avoid extra headers)

type A :: Type -> Type
type family A a where
  A (WithStatus n (Headers (Header "Set-Cookie" SetCookie ': ls) a)) = WithStatus n (Headers (Header "Set-Cookie" SetCookie ': ls) a)
  A (WithStatus n (Headers ls a)) = WithStatus n (Headers (Header "Set-Cookie" SetCookie ': ls) a)
  A (WithStatus n a) = WithStatus n (Headers '[Header "Set-Cookie" SetCookie] a)
  A a = Headers '[Header "Set-Cookie" SetCookie] a

type MapA :: [Type] -> [Type]
type family MapA a where
  MapA '[] = '[]
  MapA (a:as) = A a : MapA as

type instance AddSetCookieApi (UVerb method ctyps a)
  = UVerb method ctyps (MapA a)

instance {-# OVERLAPPING #-}
  newA ~ MapA oldA =>
  AddSetCookies ('S n) (m (Union oldA)) (m (Union newA)) where
  addSetCookies = undefined

Full example of App with this instance:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
module Servant.Auth.Uverb where
import Servant
import Data.UUID (UUID)
import Servant.Auth.JWT
import Servant.Auth.Server
import Servant.Auth.Server.Internal.AddSetCookie
import Data.Kind (Type)
type API = UVerb 'GET '[JSON] '[WithStatus 200 Int, WithStatus 403 Int, WithStatus 404 Bool]

type ProtectedAPI = Auth '[JWT, Cookie] UUID :> API


instance ToJWT UUID
instance FromJWT UUID

server :: Server ProtectedAPI
server (Authenticated _uid) = respond (WithStatus @200 (12 :: Int))
server _ = respond (WithStatus @403 (1 :: Int))


app :: Application
app = serveWithContext
    (Proxy @ProtectedAPI)
    (defaultCookieSettings :. defaultJWTSettings undefined :. EmptyContext) server

<instance here>

[dciug]

Could you perhaps provide the full implementation for addSetCookies? I'm looking through https://github.com/haskell-servant/servant-auth/blob/master/servant-auth-server/src/Servant/Auth/Server/Internal/AddSetCookie.hs and It's sitll quite unclear as to what is should be.