Download Code

A.hs

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveGeneric #-}
 
module A where
 
import EffectCapabilities
import GHC.Generics
import {-# SOURCE #-} B
 
data Cap a = Cap a deriving Generic
instance Capability Cap a
 
instance Send BChannel Cap ()

B.hs

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveGeneric #-}
 
module B where
 
import EffectCapabilities
import GHC.Generics
import {-# SOURCE #-} C
import {-# SOURCE #-} A
 
data BChannel = BChannelV deriving Generic
instance Channel BChannel
 
instance Send CChannel Cap () where
         receive CChannelV () = (receive BChannelV () :: Cap ())
 
-- This fails because A does not send a capabitiliy with permissiom Perm to B
-- instance Send CChannel Cap SomePerm where
--          receive CChannelV SomePermV = (receive BChannelV SomePermV :: Cap SomePerm)

C.hs

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveGeneric #-}
 
module C where
 
import EffectCapabilities
import GHC.Generics
import A
 
data CChannel = CChannelV deriving Generic
instance Channel CChannel
 
capV :: Cap ()
capV = receive CChannelV ()

A.hs-boot

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
 
module A where
 
import EffectCapabilities
 
data Cap a = Cap a
instance Capability Cap a

B.hs-boot

module B where
 
import EffectCapabilities
 
data BChannel = BChannelV
instance Channel BChannel

C.hs-boot

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveGeneric #-}
 
module C where
 
import EffectCapabilities
import GHC.Generics
import A
 
data CChannel = CChannelV deriving Generic
instance Channel CChannel
 
capV :: Cap ()
capV = receive CChannelV ()