How to determine whether a dependent type that doesn't fit the monad instance is categorically a monad
So, there are potentially many answers to this sort of question. One is that there are many possible categories on which there can be monads. The rules for establishing that something is a monad will ultimately be the same, but the details will differ depending on the specific category chosen. So, since there is a natural number index involved, perhaps a monad on a category of natural number indexed types is in order, although your presentation is not precisely that. Or, perhaps you can also quantify over the natural number to get a monad that is the 'total space' of all the individual fibers. (It's also not clear to me why you need the index in this example, unless Idris has a feature that makes the type small because of it.)

However, another answer is that whether something 'is a monad' is kind of the wrong thing to worry about. Especially with examples like this, what is going on is that we are constructing the 'free algebra' of some embedded language we want to work with. Monads show up because they are one of the ways that algebra is dealt with in category theory. So because we're doing algebra, we can phrase it in terms of (a particular construction of certain) monads. But it can also be presented it in other ways as well.

The presentation you're using originates in Haskell (I think), and it's convenient there, because of impredicativity and no concern for logical consistency/termination. You can easily write down the, 'free monad over a type operator.' It's also convenient because Haskell has features that make things presented as Monad nicer to use than other presentations.

However, if Idris is not (as) accepting of definitions like that, it seems sensible to re-evaluate whether some other presentation that is accepted can encode all the things you want. For instance, there are ways of specifying strictly positive functors in more obvious ways, which give rise to e.g. W-types:

data W (A : Type) (B : A → Type) : Type where
  con : (a : A) → (y : B a → W A B) → W A B


and it's possible to construct free monads based on this:

data Free (A : Type) (B : A → Type) (X : Type) : Type where
  pure : X → Free A B X
  branch : (a : A) → (B a → Free A B X) → Free A B X


This is the free monad over the polynomial functor given by A and B (the A-fold sum of B a-fold products of X). But this is by no means the only option.

So, it seems to me that unless there is some syntax sugar or similar reason to prefer a particular solution (or you have other reasons), it's better to worry about whether you have built the algebraic structure you wanted in a way that is easy to use for whatever you actually wanted to use it for, and not whether it adheres to some particular way of doing it that works well in a different language.

And to loop around, if the size is just there for getting everything to termination check, maybe it also doesn't matter if it's any actual notion of monad from category theory. If you erased the sizes and it fit the definition of a normal monad, and the sizes are only there for book keeping, maybe that's good enough (as long as it doesn't obstruct you in more practical ways).