Which inductive schemes can encode the following Agda definition?

Question

Which induction schemes (e.g. induction-recursion by Dybjer and Setzer, "Irish" induction-recursion by McBride or induction-induction by Forsberg and Setzer or perhaps some simpler ones) allow one to encode the following Agda definition

  data A : Set where
    a : Maybe (List A) → A

I can think of some tricks to reformulate List in this definition so that induction-recursion becomes applicable, but are there any schemes that would allow me to first say what a list is and then refer to this information to say what A is the way it's done in Agda?

Edit: As follows from András Kovács's answer, this particular definition can be reformulated as an inductive family. Here is how to do it:

data Three : Set where one two three : Three

data AG : Three → Set where
  a'       : AG three → AG one
  nil'     : AG two
  cons'    : AG one → AG two → AG two
  nothing' : AG three
  just'    : AG two → AG three

A = AG one
ListA = AG two
MaybeListA = AG three

a : MaybeListA → A
a = a'

nil : ListA
nil = nil'

cons : A → ListA → ListA
cons = cons'

nothing : MaybeListA
nothing = nothing'

just : ListA → MaybeListA
just = just'

Answer 1

No scheme that I know of directly encodes that type. Sometimes it's called a "nested" inductive definition. The complication here is that Maybe and List are type constructors which are external to the signature, and we have to formalize strict positivity for external type operators in general, if we want to allow such definitions.

In other words, the consistency of A depends on the definition on Maybe and List. Some external type operators are not positive, as in:

data Neg (A : Set) : Set where
  neg : (A -> Bool) -> Neg A

data B : Set where
  b : Neg B -> B

Agda does look into all the external definitions and tries to determine the variance of type parameters. While I don't know a reference for a direct formal specification of this, an easy way to reformulate nested definitions as non-nested is to include the external type operators into a mutual inductive signature. For example:

data A : Set 
data ListA : Set
data MaybeListA : Set

data A where
  a : MaybeListA -> A

data ListA where
  nil : ListA
  cons : A -> ListA -> ListA

data MaybeListA where
  nothing : MaybeListA
  just : ListA -> MaybeListA

This is an ordinary mutual inductive type, which is covered (modulo cosmetic details) by Dybjer's inductive families.