{-#LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures, StandaloneDeriving  #-}
data Natural = Zero | Succ Natural deriving (Show,Eq,Ord)

data List el len  where
    Nil  ::                      List el Zero 
    Cons :: el -> List el len -> List el (Succ len) 

deriving instance Show el => Show (List el len)


class HasLength f  where len ::  f n -> Natural
-- class HasLength (f :: Natural -> *)  where len ::  f n -> Natural

instance HasLength (List el) where
    len Nil = Zero
    len (Cons _ xs) = Succ (len xs)
    
-- If I use the narrow kind signature I get 
-- the opposite 'kind mismatch' with this of course: 
instance HasLength [] where
  len [] = Zero
  len (x:xs) = Succ (len xs)
  
  
-- as it stands, ghc-7.6 infers 
-- > :k HasLength :: (k -> *) -> Constraint
-- ghc-7.4 infers thus:
-- *Main> :k HasLength 
-- HasLength :: (AnyK -> *) -> Constraint