Uniform effects

F* currently possess 2 slightly different effect declaration mechanisms : primitive effects and DMForFree effects. This proposal try to unify and generalize the 2 presentations.

High-level plan

Both DMForFree and primitive effects specify a predicate transformer monad. Among the current examples of effect definitions, these predicate transformer monads seem to always be provided by the application of a monad transformer to the monotonic continuation monad to Prop (or Type).