totality checking with indirect mutually recursive datatypes in Idris

Question

I am working with an abstract syntax tree, where I'd like to give the binders their own type. This seems to cause problems for Idris's totality checking...

With a typical self-referencial Tree Idris does fine with totality checking.

data TreeShape = Last | More TreeShape TreeShape

Show TreeShape where
  show Last = "Leaf"
  show (More left right) = "Branch " ++ show left ++ " " ++ show right

Likewise with a mutual Tree:

mutual
  data MuTree = Another MuMuTree
  data MuMuTree = TheLeaf | TheBranch MuTree MuMuTree

  Show MuTree where
    show (Another x) = show x

  Show MuMuTree where
    show TheLeaf = "Leaf"
    show (TheBranch left right) = "Branch " ++ show left ++ " " ++ show right

But, introduce indirection by paramaterizing the extracted type, and totality checking fails:

data LeftBranch t = L t
(Show t) => Show (LeftBranch t) where
  show (L x) = show x
data TreeOutline = Final | Split (LeftBranch TreeOutline) TreeOutline

Show TreeOutline where
  show Final = "Leaf"
  show (Split left right) = "Branch " ++ show left ++ " " ++ show right

Is there a way to get Idris to properly check totality on recursive types of the last sort? Short of that, is there something other than sprinkling the code with assert_totals?