Totality checking failure for mutually recursive type class instances

Issue.idr

%default total

data Tree a = Leaf a | Fork (List (Tree a))

interface Encode a where
  encode : a -> List Bool

mutual
  Encode a => Encode (List a) where
    encode [] = [False]
    encode (x :: xs) = True :: encode x ++ encode xs

  Encode a => Encode (Tree a) where
    encode (Leaf x) = [False]
    encode (Fork []) = [True, False]
    encode (Fork (x :: xs)) = True :: True :: encode x ++ encode xs

Working.idr

%default total

data Tree a = Leaf a | Fork (List (Tree a))

interface Encode a where
  encode : a -> List Bool

mutual
  encodeList : Encode a => List (Tree a) -> List Bool
  encodeList [] = [False]
  encodeList (x :: xs) = True :: encodeTree x ++ encodeList xs

  encodeTree : Encode a => Tree a -> List Bool
  encodeTree (Leaf x) = [False]
  encodeTree (Fork []) = [True, False]
  encodeTree (Fork (x :: xs)) = True :: True :: encodeTree x ++ encodeList xs