Теория типов: типы типов

Я читал много интересного о типах типов, типах более высокого порядка и так далее. По умолчанию Haskell поддерживает два типа:

• Простой тип: *
• Конструктор типа: * → *

Последние расширения языка GHC ConstraintKinds добавляет новый тип:

• Ограничение параметра типа: Ограничение

Также после прочтения этого списка рассылки становится ясно, что может существовать другой тип типа, но он не поддерживается GHC (но такая поддержка реализована в .NET):

• Тип без упаковки: #

Я узнал о полиморфных видах и думаю, что понимаю идею. Также Haskell поддерживает явную количественную оценку.

Итак, у меня следующие вопросы:

• Существуют ли какие-либо другие типы типов?
• Существуют ли какие-либо другие языковые функции с выделенными типами?
• Что означает subkinding ? Где это реализовано / полезно?
• Существует ли система типов поверх типов , например, видов - это система типов поверх типов ? (просто интересно)