[clean-list] State-transformer monad and uniqueness typing...

[Isabelle]

Dear Cleaners,

I have defined as follows the state-transformer monad type :

:: STM s x = { stm :: s -> ( s , x ) }

I do not want to use a type-synonym in order to define later on an
overloaded (bind) operator so as to be able to compose monads and monads
transformer in a modular fashion.

I write (bind) as follows, letting the compiler infer the
uniqueness-attributed type :

(bind) infixr 0 // :: !.(STM a b) (b -> .STM a c) -> .STM a c
(bind) { stm } f = { stm = \ s0 -> let ( s1 , x ) = stm s0 in ( f x
).stm s1 }

Now, when I try to use ( STM * File x ) or ( STM * World x ) to carry
out IO in a monadic fashion, I get error messages from the compiler
about required uniqueness attributes for File...

I do not send detailed sources here because I suspect there is a basic
flaw in the STM type definition, clashing with uniqueness typing, but I
can't see where...

Anybody's help will be greatly appreciated.

Thanks (Fabien Todescato)

PS.Please reply to the clean-list...