回答編集履歴

- すべてご認識の通りです。 `DataKinds` という拡張はまさにそのように、`Nat`という本来であればただの型でしかないものを種として扱えるようにして、`Zero`や`Succ`などの、本来であれば｀Nat`型の値でしかないものを「`Nat`種の型」として扱えるようにするためのものです。