Show implementation not total

Test.idr

module Test

%default total

data Box : Type -> Type where
  MkBox : t -> Box t
   
data Test : Type where
  T1 : Test
  T2 : Box Test -> Test

mutual
  (Show a) => Show (Box a) where
    show (MkBox x) = show x

  Show Test where
    show (T1) = "t1"
    show (T2 x) = show x

{- Errors:
Test.idr:17:3-11:
   |
17 |   Show Test where
   |   ~~~~~~~~~
Test.Test implementation of Prelude.Show.Show is possibly not total due to recursive path Prelude.Show.Test.Test implementation of Prelude.Show.Show, method show --> Prelude.Show.Test.Test implementation of Prelude.Show.Show, method show
-}