Data families allow arbitrarily extending non-Type kinds

Summary

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}

import GHC.TypeLits

data family Z :: k
data family S :: k -> k

type family Plus (m :: Nat) (n :: Nat) :: Nat where
  Plus Z n = n
  Plus (S m) n = S (Plus m n)

ghci> :kind! Plus (S (S Z)) (S (S Z))
Plus (S (S Z)) (S (S Z)) :: Nat
= S (S (S (S Z)))

Who dares say Nat is not inductive now? :-)

It also looks like we can close #11080 – all kinds are open! Take the example from that ticket:

-- declares a new kind which initially has no inhabitants
data open ContentType

-- declares a new type of kind ContentType, which is distinct
-- from any others that may have been declared elsewhere,
-- even if they have the same non-module-qualified name
data constructor JSON :: ContentType

We can encode it as:

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}

data ContentType

data family JSON' :: k
type JSON = JSON' :: ContentType

Expected behavior

In the examples above, neither Z :: Nat nor JSON' :: ContentType should kind-check.

Environment

• GHC version used: GHC 8.10.3, GHC HEAD 34a8a0e4