Kind-polymorphic typechecking requires better documentation.

Hi. I faced some difficulties using kind-polymorphic instances and I think documentation should be improved. Consider following code:

{-# LANGUAGE DataKinds, TypeOperators, PolyKinds, FlexibleInstances, FlexibleContexts #-}

data Wrapped t = Wrapped 

class Len l where
    len :: l -> Int

instance Len (Wrapped '[]) where
    len = const 0

instance (Len (Wrapped xs)) => Len (Wrapped (x ': xs)) where
    len x = 1 + (len $ wrappedTail x)   

wrappedTail :: Wrapped (x ': xs) -> Wrapped xs
wrappedTail = const Wrapped  

-- | test1 == zero just as excepted. 
test1 = len (undefined  :: Wrapped '[])

-- | Since I have typeclasses defined for Wrapped (* ': [*]) and for (Wrapped '[])
-- I except to get 1 here, but this does not typecheck with following  message:
-- No instance for (Len (Wrapped [*] ([] *)))  
test2 = len (undefined  :: Wrapped '[Int]) 

It will not typecheck. Of couse it is possible to fix it by adding type signature to Wrapped:

{-# LANGUAGE DataKinds, TypeOperators, PolyKinds, FlexibleInstances, FlexibleContexts, KindSignatures #-}

data Wrapped (t :: [*]) = Wrapped 

but it is extremely hard to figure out relaying just on information provided here: http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-polymorphism-and-promotion.html, especially in complex scenarios. I think this page should provide more information on type-checker messages format related to polymorphic kind, and some common pitfalls.

Trac metadata

Trac field	Value
Version	7.4.2
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Documentation
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture