refine definition of Subscribe to prevent subscription in None and Disabled states

This commit is contained in:
Evgeny Poberezkin
2020-05-10 09:50:09 +01:00
parent 7520c681da
commit f3f39e760a
@@ -134,7 +134,15 @@ data Command res (from :: Participant) (to :: Participant) state state' :: Type
('None <==> 'None <==| s)
('New <==> 'New <==| s)
Subscribe :: Command () 'Recipient 'Broker state state -- TODO
Subscribe :: ( (r == 'None) ~ 'False
, (r == 'Disabled) ~ 'False
, (b == 'None) ~ 'False
, (b == 'Disabled) ~ 'False
, Prf HasState 'Sender s )
=> Command ()
'Recipient 'Broker
(r <==> b <==| s)
(r <==> b <==| s)
SendInvite :: Prf HasState 'Broker s
=> String -- invitation - TODO