token types and migration (WIP, does not compile)

This commit is contained in:
Evgeny Poberezkin
2025-09-16 21:29:38 +01:00
parent c56b04fb6b
commit f5a8d8b21c
8 changed files with 175 additions and 94 deletions

View File

@@ -261,7 +261,6 @@ library
Simplex.Messaging.Notifications.Server.Push
Simplex.Messaging.Notifications.Server.Push.APNS
Simplex.Messaging.Notifications.Server.Push.WebPush
Simplex.Messaging.Notifications.Server.Push
Simplex.Messaging.Notifications.Server.Push.APNS.Internal
Simplex.Messaging.Notifications.Server.Stats
Simplex.Messaging.Notifications.Server.Store
@@ -307,8 +306,6 @@ library
, directory ==1.3.*
, filepath ==1.4.*
, hourglass ==0.2.*
, http-client ==0.7.*
, http-client-tls ==0.3.6.*
, http-types ==0.12.*
, http2 >=4.2.2 && <4.3
, iproute ==1.7.*
@@ -340,6 +337,8 @@ library
case-insensitive ==1.2.*
, hashable ==1.4.*
, ini ==0.4.1
, http-client ==0.7.*
, http-client-tls ==0.3.6.*
, optparse-applicative >=0.15 && <0.17
, process ==1.6.*
, temporary ==1.3.*

View File

@@ -897,7 +897,7 @@ data CryptoError
| -- | duplicate message number
CERatchetDuplicateMessage
| -- | unable to decode ecc key
CryptoInvalidECCKey CE.CryptoError
CryptoInvalidECCKey CE.CryptoError -- TODO [webpush] remove this error, it will be parsing error
deriving (Eq, Show, Exception)
aesKeySize :: Int

View File

@@ -12,6 +12,8 @@
module Simplex.Messaging.Notifications.Protocol where
import Control.Applicative (optional, (<|>))
import Control.Monad
import qualified Crypto.PubKey.ECC.Types as ECC
import Data.Aeson (FromJSON (..), ToJSON (..), (.:), (.=))
import qualified Data.Aeson as J
import qualified Data.Aeson.Encoding as JE
@@ -35,7 +37,6 @@ import Simplex.Messaging.Encoding.String
import Simplex.Messaging.Notifications.Transport (NTFVersion, invalidReasonNTFVersion, ntfClientHandshake)
import Simplex.Messaging.Protocol hiding (Command (..), CommandTag (..))
import Simplex.Messaging.Util (eitherToMaybe, (<$?>))
import Control.Monad (when)
data NtfEntity = Token | Subscription
deriving (Show)
@@ -373,63 +374,102 @@ instance StrEncoding SMPQueueNtf where
notifierId <- A.char '/' *> strP
pure SMPQueueNtf {smpServer, notifierId}
data PushProvider
data PushProvider = PPAPNS APNSProvider | PPWP WPProvider
deriving (Eq, Ord, Show)
data APNSProvider
= PPApnsDev -- provider for Apple development environment
| PPApnsProd -- production environment, including TestFlight
| PPApnsTest -- used for tests, to use APNS mock server
| PPApnsNull -- used to test servers from the client - does not communicate with APNS
| PPWebPush -- used for webpush (FCM, UnifiedPush, potentially desktop)
deriving (Eq, Ord, Show)
newtype WPProvider = WPP (ProtocolServer 'PHTTPS)
deriving (Eq, Ord, Show)
instance Encoding PushProvider where
smpEncode = \case
PPAPNS p -> smpEncode p
PPWP p -> smpEncode p
smpP =
A.peekChar' >>= \case
'A' -> PPAPNS <$> smpP
_ -> PPWP <$> smpP
instance Encoding APNSProvider where
smpEncode = \case
PPApnsDev -> "AD"
PPApnsProd -> "AP"
PPApnsTest -> "AT"
PPApnsNull -> "AN"
PPWebPush -> "WP"
smpP =
A.take 2 >>= \case
"AD" -> pure PPApnsDev
"AP" -> pure PPApnsProd
"AT" -> pure PPApnsTest
"AN" -> pure PPApnsNull
"WP" -> pure PPWebPush
_ -> fail "bad PushProvider"
_ -> fail "bad APNSProvider"
instance StrEncoding PushProvider where
strEncode = \case
PPAPNS p -> strEncode p
PPWP p -> strEncode p
strP =
A.peekChar' >>= \case
'a' -> PPAPNS <$> strP
_ -> PPWP <$> strP
instance StrEncoding APNSProvider where
strEncode = \case
PPApnsDev -> "apns_dev"
PPApnsProd -> "apns_prod"
PPApnsTest -> "apns_test"
PPApnsNull -> "apns_null"
PPWebPush -> "webpush"
strP =
A.takeTill (== ' ') >>= \case
"apns_dev" -> pure PPApnsDev
"apns_prod" -> pure PPApnsProd
"apns_test" -> pure PPApnsTest
"apns_null" -> pure PPApnsNull
"webpush" -> pure PPWebPush
_ -> fail "bad PushProvider"
_ -> fail "bad APNSProvider"
instance FromField PushProvider where fromField = fromTextField_ $ eitherToMaybe . strDecode . encodeUtf8
instance Encoding WPProvider where
smpEncode (WPP srv) = "WP" <> smpEncode srv
smpP = WPP <$> ("WP" *> smpP)
instance ToField PushProvider where toField = toField . decodeLatin1 . strEncode
instance StrEncoding WPProvider where
strEncode (WPP srv) = "webpush " <> strEncode srv
strP = WPP <$> ("webpush " *> strP)
data WPEndpoint = WPEndpoint { endpoint::ByteString, auth::ByteString, p256dh::ByteString }
instance FromField APNSProvider where fromField = fromTextField_ $ eitherToMaybe . strDecode . encodeUtf8
instance ToField APNSProvider where toField = toField . decodeLatin1 . strEncode
data WPTokenParams = WPTokenParams
{ wpPath :: Text, -- parser should validate it's a valid type
wpAuth :: ByteString, -- if we enforce size constraints, should also be in parser.
wpKey :: WPKey -- or another correct type that is needed for encryption, so it fails in parser and not there
}
newtype WPKey = WPKey ECC.Point
data WPEndpoint = WPEndpoint
{ endpoint :: ByteString,
auth :: ByteString,
p256dh :: ByteString
}
deriving (Eq, Ord, Show)
instance Encoding WPEndpoint where
smpEncode WPEndpoint { endpoint, auth, p256dh } = smpEncode (endpoint, auth, p256dh)
smpEncode WPEndpoint {endpoint, auth, p256dh} = smpEncode (endpoint, auth, p256dh)
smpP = do
endpoint <- smpP
auth <- smpP
p256dh <- smpP
pure WPEndpoint { endpoint, auth, p256dh }
pure WPEndpoint {endpoint, auth, p256dh}
instance StrEncoding WPEndpoint where
strEncode WPEndpoint { endpoint, auth, p256dh } = endpoint <> " " <> strEncode auth <> " " <> strEncode p256dh
strEncode WPEndpoint {endpoint, auth, p256dh} = endpoint <> " " <> strEncode auth <> " " <> strEncode p256dh
strP = do
endpoint <- A.takeWhile (/= ' ')
_ <- A.char ' '
@@ -439,80 +479,79 @@ instance StrEncoding WPEndpoint where
-- p256dh is a public key on the P-256 curve, encoded in uncompressed format
-- 0x04 + the 2 points = 65 bytes
when (B.length p256dh /= 65) $ fail "Invalid p256dh key length"
-- TODO [webpush] parse it here (or rather in WPTokenParams)
when (B.take 1 p256dh /= "\x04") $ fail "Invalid p256dh key, doesn't start with 0x04"
pure WPEndpoint { endpoint, auth, p256dh }
pure WPEndpoint {endpoint, auth, p256dh}
instance ToJSON WPEndpoint where
toEncoding WPEndpoint { endpoint, auth, p256dh } = J.pairs $ "endpoint" .= decodeLatin1 endpoint <> "auth" .= decodeLatin1 (strEncode auth) <> "p256dh" .= decodeLatin1 (strEncode p256dh)
toJSON WPEndpoint { endpoint, auth, p256dh } = J.object ["endpoint" .= decodeLatin1 endpoint, "auth" .= decodeLatin1 (strEncode auth), "p256dh" .= decodeLatin1 (strEncode p256dh) ]
toEncoding WPEndpoint {endpoint, auth, p256dh} = J.pairs $ "endpoint" .= decodeLatin1 endpoint <> "auth" .= decodeLatin1 (strEncode auth) <> "p256dh" .= decodeLatin1 (strEncode p256dh)
toJSON WPEndpoint {endpoint, auth, p256dh} = J.object ["endpoint" .= decodeLatin1 endpoint, "auth" .= decodeLatin1 (strEncode auth), "p256dh" .= decodeLatin1 (strEncode p256dh) ]
instance FromJSON WPEndpoint where
parseJSON = J.withObject "WPEndpoint" $ \o -> do
endpoint <- encodeUtf8 <$> o .: "endpoint"
auth <- strDecode . encodeUtf8 <$?> o .: "auth"
p256dh <- strDecode . encodeUtf8 <$?> o .: "p256dh"
pure WPEndpoint { endpoint, auth, p256dh }
pure WPEndpoint {endpoint, auth, p256dh}
data DeviceToken
= APNSDeviceToken PushProvider ByteString
| WPDeviceToken WPEndpoint
= APNSDeviceToken APNSProvider ByteString
| WPDeviceToken WPProvider WPEndpoint
-- TODO [webpush] replace with WPTokenParams
-- | WPDeviceToken WPProvider WPTokenParams
deriving (Eq, Ord, Show)
instance Encoding DeviceToken where
smpEncode token = case token of
APNSDeviceToken p t -> smpEncode (p, t)
WPDeviceToken t -> smpEncode (PPWebPush, t)
smpP = do
pp <- smpP
case pp of
PPWebPush -> WPDeviceToken <$> smpP
_ -> APNSDeviceToken pp <$> smpP
WPDeviceToken p t -> smpEncode (p, t)
smpP =
smpP >>= \case
PPAPNS p -> APNSDeviceToken p <$> smpP
PPWP p -> WPDeviceToken p <$> smpP
instance StrEncoding DeviceToken where
strEncode token = case token of
APNSDeviceToken p t -> strEncode p <> " " <> t
WPDeviceToken t -> strEncode PPWebPush <> " " <> strEncode t
WPDeviceToken p t -> strEncode (p, t)
strP = nullToken <|> deviceToken
where
nullToken = "apns_null test_ntf_token" $> APNSDeviceToken PPApnsNull "test_ntf_token"
deviceToken = do
pp <- strP_
case pp of
PPWebPush -> WPDeviceToken <$> strP
_ -> APNSDeviceToken pp <$> hexStringP
deviceToken =
strP_ >>= \case
PPAPNS p -> APNSDeviceToken p <$> hexStringP
PPWP p -> WPDeviceToken p <$> strP
hexStringP =
A.takeWhile (`B.elem` "0123456789abcdef") >>= \s ->
if even (B.length s) then pure s else fail "odd number of hex characters"
-- TODO [webpush] is it needed?
instance ToJSON DeviceToken where
toEncoding token = case token of
APNSDeviceToken pp t -> J.pairs $ "pushProvider" .= decodeLatin1 (strEncode pp) <> "token" .= decodeLatin1 t
WPDeviceToken t -> J.pairs $ "pushProvider" .= decodeLatin1 (strEncode PPWebPush) <> "token" .= toJSON t
APNSDeviceToken p t -> J.pairs $ "pushProvider" .= decodeLatin1 (strEncode p) <> "token" .= decodeLatin1 t
WPDeviceToken p t -> J.pairs $ "pushProvider" .= decodeLatin1 (strEncode p) <> "token" .= toJSON t
toJSON token = case token of
APNSDeviceToken pp t -> J.object ["pushProvider" .= decodeLatin1 (strEncode pp), "token" .= decodeLatin1 t]
WPDeviceToken t -> J.object ["pushProvider" .= decodeLatin1 (strEncode PPWebPush), "token" .= toJSON t]
APNSDeviceToken p t -> J.object ["pushProvider" .= decodeLatin1 (strEncode p), "token" .= decodeLatin1 t]
WPDeviceToken p t -> J.object ["pushProvider" .= decodeLatin1 (strEncode p), "token" .= toJSON t]
instance FromJSON DeviceToken where
parseJSON = J.withObject "DeviceToken" $ \o -> do
pp <- strDecode . encodeUtf8 <$?> o .: "pushProvider"
case pp of
PPWebPush -> do
WPDeviceToken <$> (o .: "token")
_ -> do
t <- encodeUtf8 <$> (o .: "token")
pure $ APNSDeviceToken pp t
parseJSON = J.withObject "DeviceToken" $ \o ->
(strDecode . encodeUtf8 <$?> o .: "pushProvider") >>= \case
PPAPNS p -> APNSDeviceToken p . encodeUtf8 <$> (o .: "token")
PPWP p -> WPDeviceToken p <$> (o .: "token")
-- | Returns fields for the device token (pushProvider, token)
-- TODO [webpush] save token as separate fields
deviceTokenFields :: DeviceToken -> (PushProvider, ByteString)
deviceTokenFields dt = case dt of
APNSDeviceToken pp t -> (pp, t)
WPDeviceToken t -> (PPWebPush, strEncode t)
APNSDeviceToken p t -> (PPAPNS p, t)
WPDeviceToken p t -> (PPWP p, strEncode t)
-- | Returns the device token from the fields (pushProvider, token)
deviceToken' :: PushProvider -> ByteString -> DeviceToken
deviceToken' pp t = case pp of
PPWebPush -> WPDeviceToken <$> either error id $ strDecode t
_ -> APNSDeviceToken pp t
PPAPNS p -> APNSDeviceToken p t
PPWP p -> WPDeviceToken p <$> either error id $ strDecode t
-- List of PNMessageData uses semicolon-separated encoding instead of strEncode,
-- because strEncode of NonEmpty list uses comma for separator,

View File

@@ -46,7 +46,6 @@ import Simplex.Messaging.Transport.Server (AddHTTP, ServerCredentials, Transport
import System.Exit (exitFailure)
import System.Mem.Weak (Weak)
import UnliftIO.STM
import Simplex.Messaging.Notifications.Server.Push (PushNotification, PushProviderClient)
import Simplex.Messaging.Notifications.Server.Push.WebPush (wpPushProviderClient)
import Network.HTTP.Client (newManager)
import Network.HTTP.Client.TLS (tlsManagerSettings)

View File

@@ -124,13 +124,12 @@ data APNSPushClientConfig = APNSPushClientConfig
caStoreFile :: FilePath
}
apnsProviderHost :: PushProvider -> Maybe HostName
apnsProviderHost :: APNSProvider -> Maybe HostName
apnsProviderHost = \case
PPApnsNull -> Nothing
PPApnsTest -> Just "localhost"
PPApnsDev -> Just "api.sandbox.push.apple.com"
PPApnsProd -> Just "api.push.apple.com"
_ -> Nothing
defaultAPNSPushClientConfig :: APNSPushClientConfig
defaultAPNSPushClientConfig =
@@ -256,6 +255,7 @@ data APNSErrorResponse = APNSErrorResponse {reason :: Text}
$(JQ.deriveFromJSON defaultJSON ''APNSErrorResponse)
-- TODO [webpush] change type accept token components so it only allows APNS token
apnsPushProviderClient :: APNSPushClient -> PushProviderClient
apnsPushProviderClient c@APNSPushClient {nonceDrg, apnsCfg} tkn@NtfTknRec {token} pn = do
tknStr <- deviceToken token

View File

@@ -3,13 +3,11 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use newtype instead of data" #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use newtype instead of data" #-}
module Simplex.Messaging.Notifications.Server.Push.WebPush where
@@ -46,33 +44,36 @@ import GHC.Base (when)
wpPushProviderClient :: Manager -> PushProviderClient
wpPushProviderClient mg tkn pn = do
e <- endpoint tkn
r <- liftPPWPError $ parseUrlThrow $ B.unpack e.endpoint
logDebug $ "Request to " <> tshow r.host
encBody <- body e
let requestHeaders = [
("TTL", "2592000") -- 30 days
, ("Urgency", "high")
, ("Content-Encoding", "aes128gcm")
-- TODO: topic for pings and interval
]
req = r {
method = "POST"
, requestHeaders
, requestBody = RequestBodyBS encBody
, redirectCount = 0
}
_ <- liftPPWPError $ httpNoBody req mg
pure ()
-- TODO [webpush] parsing will happen in DeviceToken parser, so it won't fail here
-- TODO [webpush] this function should accept type that is restricted to WP token (so, possibly WPProvider and WPTokenParams)
wpe@WPEndpoint {endpoint} <- tokenEndpoint tkn
r <- liftPPWPError $ parseUrlThrow $ B.unpack endpoint
logDebug $ "Request to " <> tshow (host r)
encBody <- body wpe
let requestHeaders =
[ ("TTL", "2592000"), -- 30 days
("Urgency", "high"),
("Content-Encoding", "aes128gcm")
-- TODO: topic for pings and interval
]
req =
r
{ method = "POST",
requestHeaders,
requestBody = RequestBodyBS encBody,
redirectCount = 0
}
_ <- liftPPWPError $ httpNoBody req mg
pure ()
where
endpoint :: NtfTknRec -> ExceptT PushProviderError IO WPEndpoint
endpoint NtfTknRec {token} = do
tokenEndpoint :: NtfTknRec -> ExceptT PushProviderError IO WPEndpoint
tokenEndpoint NtfTknRec {token} = do
case token of
WPDeviceToken e -> pure e
WPDeviceToken _p e -> pure e
_ -> fail "Wrong device token"
-- TODO: move to PPIndalidPusher ? WPEndpoint should be invalidated and removed if the key is invalid, but the validation key is never sent
body :: WPEndpoint -> ExceptT PushProviderError IO B.ByteString
body e = withExceptT PPCryptoError $ wpEncrypt e.auth e.p256dh (BL.toStrict $ encodePN pn)
body WPEndpoint {auth, p256dh} = withExceptT PPCryptoError $ wpEncrypt auth p256dh (BL.toStrict $ encodePN pn)
-- | encrypt :: auth -> key -> clear -> cipher
-- | https://www.rfc-editor.org/rfc/rfc8291#section-3.4
@@ -80,6 +81,7 @@ wpEncrypt :: B.ByteString -> B.ByteString -> B.ByteString -> ExceptT C.CryptoErr
wpEncrypt auth uaPubKS clearT = do
salt :: B.ByteString <- liftIO $ getRandomBytes 16
asPrivK <- liftIO $ ECDH.generatePrivate $ ECC.getCurveByName ECC.SEC_p256r1
-- TODO [webpush] key parsing will happen in DeviceToken parser, so it won't fail here
uaPubK <- point uaPubKS
let asPubK = BL.toStrict . uncompressEncode . ECDH.calculatePublic (ECC.getCurveByName ECC.SEC_p256r1) $ asPrivK
ecdhSecret = ECDH.getShared (ECC.getCurveByName ECC.SEC_p256r1) asPrivK uaPubK
@@ -112,12 +114,12 @@ wpEncrypt auth uaPubKS clearT = do
-- | Elliptic-Curve-Point-to-Octet-String Conversion without compression
-- | as required by RFC8291
-- | https://www.secg.org/sec1-v2.pdf#subsubsection.2.3.3
-- TODO [webpush] add them to the encoding of WPKey
uncompressEncode :: ECC.Point -> BL.ByteString
uncompressEncode (ECC.Point x y) = "\x04" <>
encodeBigInt x <>
encodeBigInt y
uncompressEncode (ECC.Point x y) = "\x04" <> encodeBigInt x <> encodeBigInt y
uncompressEncode ECC.PointO = "\0"
-- TODO [webpush] should be -> Either ... (which it would be in StrEncoding)
uncompressDecode :: BL.ByteString -> ExceptT CE.CryptoError IO ECC.Point
uncompressDecode "\0" = pure ECC.PointO
uncompressDecode s = do
@@ -135,24 +137,26 @@ encodeBigInt i = do
let s1 = Bits.shiftR i 64
s2 = Bits.shiftR s1 64
s3 = Bits.shiftR s2 64
Bin.encode ( w64 s3, w64 s2, w64 s1, w64 i )
Bin.encode (w64 s3, w64 s2, w64 s1, w64 i)
where
w64 :: Integer -> Bin.Word64
w64 = fromIntegral
-- TODO [webpush] should be -> Either ... (which it would be in StrEncoding)
decodeBigInt :: BL.ByteString -> ExceptT CE.CryptoError IO Integer
decodeBigInt s = do
when (BL.length s /= 32) $ throwError CE.CryptoError_PointSizeInvalid
let (w3, w2, w1, w0) = Bin.decode s :: (Bin.Word64, Bin.Word64, Bin.Word64, Bin.Word64 )
pure $ shift 3 w3 + shift 2 w2 + shift 1 w1 + shift 0 w0
where
shift i w = Bits.shiftL (fromIntegral w) (64*i)
shift i w = Bits.shiftL (fromIntegral w) (64 * i)
-- TODO [webpush] use ToJSON
encodePN :: PushNotification -> BL.ByteString
encodePN pn = J.encode $ case pn of
PNVerification code -> J.object [ "verification" .= code ]
PNMessage d -> J.object [ "message" .= encodeData d ]
PNCheckMessages -> J.object [ "checkMessages" .= True ]
PNVerification code -> J.object ["verification" .= code]
PNMessage d -> J.object ["message" .= encodeData d]
PNCheckMessages -> J.object ["checkMessages" .= True]
where
encodeData :: NonEmpty PNMessageData -> String
encodeData a = T.unpack . T.decodeUtf8 $ encodePNMessages a

View File

@@ -12,7 +12,8 @@ import Text.RawString.QQ (r)
ntfServerSchemaMigrations :: [(String, Text, Maybe Text)]
ntfServerSchemaMigrations =
[ ("20250417_initial", m20250417_initial, Nothing),
("20250517_service_cert", m20250517_service_cert, Just down_m20250517_service_cert)
("20250517_service_cert", m20250517_service_cert, Just down_m20250517_service_cert),
("20250916_webpush", m20250916_webpush, Just down_m20250916_webpush)
]
-- | The list of migrations in ascending order by date
@@ -104,3 +105,34 @@ ALTER TABLE smp_servers DROP COLUMN ntf_service_id;
ALTER TABLE subscriptions DROP COLUMN ntf_service_assoc;
|]
m20250916_webpush :: Text
m20250916_webpush =
T.pack
[r|
CREATE TABLE webpush_servers(
wp_server_id BIGINT PRIMARY KEY GENERATED ALWAYS AS IDENTITY,
wp_host TEXT NOT NULL,
wp_port TEXT NOT NULL,
wp_keyhash BYTEA NOT NULL
);
ALTER TABLE tokens
ADD COLUMN wp_server_id BIGINT REFERENCES webpush_servers ON DELETE RESTRICT ON UPDATE RESTRICT,
ADD COLUMN wp_path TEXT,
ADD COLUMN wp_auth BYTEA,
ADD COLUMN wp_key BYTEA;
|]
down_m20250916_webpush :: Text
down_m20250916_webpush =
T.pack
[r|
ALTER TABLE tokens
DROP COLUMN wp_server_id,
DROP COLUMN wp_path,
DROP COLUMN wp_auth,
DROP COLUMN wp_key;
DROP TABLE webpush_servers;
|]

View File

@@ -1144,7 +1144,7 @@ sameSrvAddr :: ProtocolServer p -> ProtocolServer p -> Bool
sameSrvAddr ProtocolServer {host, port} ProtocolServer {host = h', port = p'} = host == h' && port == p'
{-# INLINE sameSrvAddr #-}
data ProtocolType = PSMP | PNTF | PXFTP
data ProtocolType = PSMP | PNTF | PXFTP | PHTTPS
deriving (Eq, Ord, Show)
instance StrEncoding ProtocolType where
@@ -1152,17 +1152,20 @@ instance StrEncoding ProtocolType where
PSMP -> "smp"
PNTF -> "ntf"
PXFTP -> "xftp"
PHTTPS -> "https"
strP =
A.takeTill (\c -> c == ':' || c == ' ') >>= \case
"smp" -> pure PSMP
"ntf" -> pure PNTF
"xftp" -> pure PXFTP
"https" -> pure PHTTPS
_ -> fail "bad ProtocolType"
data SProtocolType (p :: ProtocolType) where
SPSMP :: SProtocolType 'PSMP
SPNTF :: SProtocolType 'PNTF
SPXFTP :: SProtocolType 'PXFTP
SPHTTPS :: SProtocolType 'PHTTPS
deriving instance Eq (SProtocolType p)
@@ -1181,6 +1184,7 @@ instance TestEquality SProtocolType where
testEquality SPSMP SPSMP = Just Refl
testEquality SPNTF SPNTF = Just Refl
testEquality SPXFTP SPXFTP = Just Refl
testEquality SPHTTPS SPHTTPS = Just Refl
testEquality _ _ = Nothing
protocolType :: SProtocolType p -> ProtocolType
@@ -1188,12 +1192,14 @@ protocolType = \case
SPSMP -> PSMP
SPNTF -> PNTF
SPXFTP -> PXFTP
SPHTTPS -> PHTTPS
aProtocolType :: ProtocolType -> AProtocolType
aProtocolType = \case
PSMP -> AProtocolType SPSMP
PNTF -> AProtocolType SPNTF
PXFTP -> AProtocolType SPXFTP
PHTTPS -> AProtocolType SPHTTPS
instance ProtocolTypeI p => StrEncoding (SProtocolType p) where
strEncode = strEncode . protocolType
@@ -1231,6 +1237,8 @@ instance ProtocolTypeI 'PNTF where protocolTypeI = SPNTF
instance ProtocolTypeI 'PXFTP where protocolTypeI = SPXFTP
instance ProtocolTypeI 'PHTTPS where protocolTypeI = SPHTTPS
type family UserProtocol (p :: ProtocolType) :: Constraint where
UserProtocol PSMP = ()
UserProtocol PXFTP = ()