GHC 8.0.0.20160511. Example from the user guide: Constraints in kinds

type family IsTypeLit a where
  IsTypeLit Nat    = 'True
  IsTypeLit Symbol = 'True
  IsTypeLit a      = 'False

data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
  MkNat    :: T 42
  MkSymbol :: T "Don't panic!"

Deriving a standalone Show instance *without* the constraint (IsTypeLit a ~ 'True) => works fine

deriving instance Show (T a)

but I couldn't define a Show instance given the constraints:

-- • Couldn't match expected kind ‘'True’
--               with actual kind ‘IsTypeLit a0’
--   The type variable ‘a0’ is ambiguous
-- • In the first argument of ‘Show’, namely ‘T a’
--   In the stand-alone deriving instance for ‘Show (T a)’
deriving instance Show (T a)

let's add constraints

-- • Couldn't match expected kind ‘'True’
--               with actual kind ‘IsTypeLit lit’
-- • In the first argument of ‘Show’, namely ‘T (a :: lit)’
--   In the instance declaration for ‘Show (T (a :: lit))’
instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where

let's derive for a single literal

-- • Illegal type synonym family application in instance:
--     T Nat
--       ('Data.Type.Equality.C:~
--          Bool
--          (IsTypeLit Nat)
--          'True
--          ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>))
--       42
-- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’
deriving instance Show (T (42 :: Nat))

same happens with

instance Show (T 42) where

---

The documentation

Note that explicitly quantifying with forall a is not necessary here.

seems to be wrong since removing it results in

tVDv.hs:10:17-18: error: …
    • Expected kind ‘a’, but ‘42’ has kind ‘Nat’
    • In the first argument of ‘T’, namely ‘42’
      In the type ‘T 42’
      In the definition of data constructor ‘MkNat’
Compilation failed.