Бесплатный преобразователь монад - как реализовать привязку?

Я пытаюсь реализовать бесплатный преобразователь монад, аналогичный FreeT из "бесплатного" пакета haskell, но я не знаю, как написать bind, чтобы проверка завершения не жаловалась. Мне кажется, что параметр рекурсивного вызова p i должен быть меньше исходного параметра, но я не уверен, что это действительно так. Можно ли реализовать bind с --safe агда?

{-# OPTIONS --without-K --safe #-}

module Test where

import Data.Container.Combinator            as Cc
import Data.Container.Combinator.Properties as Ccp
import Function.Equality                    as Fun
import Function.Inverse                     as Fun
open import Data.Container.Core             as C        using (Container; ⟦_⟧)
open import Data.Container.Relation.Unary.Any           using (any)
open import Data.Product                                using (_,_)
open import Data.Sum.Base                               using (inj₁; inj₂)
open import Data.W                                      using (W; sup)
open import Effect.Monad                                using (RawMonad)
open import Function.Base                               using (_$_)
open import Level

module _ (M F : Container 0ℓ 0ℓ) ⦃ M-monad : RawMonad {f = 0ℓ} ⟦ M ⟧ ⦄ where
    module M = RawMonad M-monad
    
    module _ {A X : Set} where
        private
            ∘-correct = Ccp.Composition.correct M (F Cc.⊎ Cc.const A) {X = X}
        
        open Fun.Π (Fun.Inverse.to ∘-correct) public
            using () renaming (_⟨$⟩_ to [c∘c]⇒c[c])

        open Fun.Π (Fun.Inverse.from ∘-correct) public
            using () renaming (_⟨$⟩_ to c[c]⇒[c∘c])

    C : Set → Set
    C A = W $ M Cc.∘ (F Cc.⊎ Cc.const A)

    pure : ∀{A} → A → C A
    pure x = sup $ c[c]⇒[c∘c] $ M.pure $ inj₂ x , λ ()

    unsup : ∀{A} → C A → ⟦ M Cc.∘ (F Cc.⊎ Cc.const A) ⟧ (C A)
    unsup (sup x) = x

    bind : ∀{A B} → C A → (A → C B) → C B
    bind {A}{B} (sup ca) f = sup $ c[c]⇒[c∘c] $ M.join $
        M._<$>_ [c∘c]⇒c[c] $ [c∘c]⇒c[c] ca M.>>= λ where
            (inj₁ a , p) → M.pure $ c[c]⇒[c∘c] $ M.pure $ inj₁ a , λ i → bind (p i) f
            (inj₂ x , _) → M.pure $ unsup $ f x