I want to make my mutually recursive functions stack-safe, but because they have different signatures - one traverses a list and other a tree(?) of sorts - I'm not clear how to go about this.

Here's an mwe.

data A : Type where
  AL : List A -> A
  A0 : A

data B : Type where
  BL : List B -> B
  B0 : B

mutual
  as2bs : List A -> List B
  as2bs [] = []
  as2bs (x :: xs) = a2b x :: as2bs xs

  a2b : A -> B
  a2b (AL as) = BL (as2bs as)
  a2b A0 = B0

I want the function a2b : A -> B.

I has crossed my mind to just create a single function as2bs, and extract the resulting B from an [a], but I need to know I get a single B from my single A, so that's not going to work (short of auxiliary proofs which are a last resort).

Extra helpful if you can comment on whether a solution exists even where the conversion A -> B might fail with a Maybe.