change data familiy to type family

This commit is contained in:
Evgeny Poberezkin
2020-05-09 13:40:32 +01:00
parent 7dce45ea2a
commit 3923de9b49

View File

@@ -90,12 +90,16 @@ data (<==>) (rs :: ConnectionState) (bs :: ConnectionState) :: Type where
-> Sing bs
-> rs <==> bs
data family (<==|) rb (ss :: ConnectionState)
data instance (<==|) (rs <==> bs) ss :: Type where
data AllConnState (rs :: ConnectionState)
(bs :: ConnectionState)
(ss :: ConnectionState) where
(:<==|) :: Prf HasState 'Sender ss
=> rs <==> bs
-> Sing ss
-> rs <==> bs <==| ss
-> AllConnState rs bs ss
type family (<==|) rb ss where
(rs <==> bs) <==| (ss :: ConnectionState) = AllConnState rs bs ss
-- recipient <==> broker <==| sender
st2 :: 'Pending <==> 'New <==| 'Confirmed