Проверка целостности с косвенными взаимно рекурсивными типами данных в Idris

Question

Я работаю с абстрактным синтаксическим деревом, где я хотел бы дать связующим их собственный тип. Это, кажется, вызывает проблемы для проверки целостности Идриса...

С типичной референцией Tree Идрис прекрасно справляется с проверкой целостности.

data TreeShape = Last | More TreeShape TreeShape

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

Аналогично с взаимной 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

Но введите косвенное обращение путем параметризации извлеченного типа, и проверка целостности завершится неудачно:

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

Есть ли способ заставить Idris правильно проверить целостность рекурсивных типов последнего вида? Если не считать, есть ли что-то кроме посыпания кода assert_totals?