{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances, FlexibleContexts #-}

import GHC.TypeLits
import Data.Proxy

type family F a :: Nat where F ([] ([] b)) = 1 + F ([] b) ; F a = 1

proxy :: [a] -> Proxy (F [a])
proxy xs = Proxy

depth :: KnownNat (F [a]) => [a] -> Integer
depth = natVal . proxy

main = print $ depth [([]::[()])]

値としての()は消えるが型アノーテーションが必要になり余計に面倒臭くなった