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