# “Constraints in kinds” illegal family application in instance (+ documentation issues?)

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.
```