Unusual Kinds and Data Constructors

Question

I don't know how I didn't notice this, but data constructors and function definitions alike can't use types with kinds other than * and it's variants * -> * etc., due to (->)'s kind signature, even under -XPolyKinds.

Here is the code I have tried:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data Nat = S Nat | Z

data Foo where
  Foo :: 'Z -> Foo -- Fails

foo :: 'Z -> Int -- Fails
foo _ = 1

The error I'm getting is the following:

<interactive>:8:12:
    Expected a type, but ‘Z’ has kind ‘Nat’
    In the type signature for ‘foo’: foo :: 'Z -> Int

Why shouldn't we allow pattern matching with non-traditional kinds?

Answer 1

There is no¹ such thing as "types with kinds other than *". Kind * is the kind for types, much like Int is the type for machine-sized numbers; other kinds may contain stuff that resembles types or can be converted to types or is used to index types or whatever – but is not types as such, merely "type level entities".

---

¹_{As usually, I disregard unbox-kinds here.}