Algebraic effects are one approach to tackling modularity is- sues arising in structuring side effects. One such application area is in (formalised) programming language semantics. We observe that in this setting, there is a need to separate the model of effects of the language being formalised from the effects arising as incidental artefacts of the formalisation. In this work, we focus on failure as such an incidental effect. We thus seek an extension to the usual underlying mathematical structures for capturing algebraic effects to incorporate (non-handleable) failure. We show how the MaybeT monad transformer over a free monad construction can be used, studying the implications on the underlying theory via a (work in progress) mechanisation in type theory. Our aim is to host both the language formalisation and its associated theory within one mechanised framework. Along the way, we also give a graded monadic view of algebraic effects.