Defining equality for a non-dependent type hosting a dependent type

A.idr

module A

import Data.Vect

data T
  = Val Int
  | Vec (Vect len T)

vectEq : Eq a => Vect n a -> Vect m a -> Bool
vectEq {n} {m} v w = n == m && Just v == (exactLength n w)

Eq T where
  (==) (Val i) (Val j) = i == j
  (==) (Vec v) (Vec w) = vectEq v w
  (==) _ _ = False

{-

A.idr:13:3:
Prelude.Interfaces.A.T implementation of Prelude.Interfaces.Eq, method ==
is possibly not total due to recursive path Prelude.Interfaces.A.T
implementation of Prelude.Interfaces.Eq, method == -->
Prelude.Interfaces.A.T implementation of Prelude.Interfaces.Eq, method ==
./Prelude/Interfaces.idr:30:5:
Prelude.Interfaces.A.T implementation of Prelude.Interfaces.Eq, method /=
is possibly not total due to: Prelude.Interfaces.A.T implementation of
Prelude.Interfaces.Eq, method ==

-}