Возможно ли получить ошибку бесконечного рода в Haskell 98?

Я внедряю добрую систему для нового функционального языка программирования, и в настоящее время я пишу функцию для объединения двух видов. Рассмотрим четыре случая:

+---------+---------+-------------------------------------------------------+
|   k1    |   k2    |                        action                         |
+=========+=========+=======================================================+
|   var   |   var   |                  k1 := k2 ^ k2 := k1                  |
+---------+---------+-------------------------------------------------------+
|   var   | non var |             if (!occurs(k1, k2)) k1 := k2             |
+---------+---------+-------------------------------------------------------+
| non var |   var   |             if (!occurs(k2, k1)) k2 := k1             |
+---------+---------+-------------------------------------------------------+
| non var | non var | ensure same name and arity, and unify respective args |
+---------+---------+-------------------------------------------------------+

• Когда оба k1 и k2 являются переменными, они создаются друг с другом.
• Когда только k1 является переменной, тогда она создается в k2, если if k1 не встречается в k2.
• Когда только k2 является переменной, тогда она создается в k1 iff k2 не встречается в k1.
• В противном случае мы проверяем, имеют ли теги k1 и k2 одно и то же имя и arity и унифицируют их соответствующие аргументы.

Для второго и третьего случаев нам необходимо выполнить проверку на наличие ошибок, чтобы мы не застревали в бесконечном цикле. Однако я сомневаюсь, что программист сможет построить бесконечный вид вообще.

В Haskell легко построить бесконечный тип:

let f x = f

Однако я не смог построить бесконечный вид, как бы я ни старался. Обратите внимание, что я не использовал никаких языковых расширений.

Причина, по которой я спрашиваю об этом, состоит в том, что, если вообще невозможно построить бесконечный вид, я даже не буду пытаться выполнить проверку на наличие видов в моей доброй системе.

Ответы

data F f = F (f F)

kind.hs:1:17:
    Kind occurs check
    The first argument of ‘f’ should have kind ‘k0’,
      but ‘F’ has kind ‘(k0 -> k1) -> *’
    In the type ‘f F’
    In the definition of data constructor ‘F’
    In the data declaration for ‘F’

GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
Prelude> let x = undefined :: f f

<interactive>:2:24:
    Kind occurs check
    The first argument of ‘f’ should have kind ‘k0’,
      but ‘f’ has kind ‘k0 -> k1’
    In an expression type signature: f f
    In the expression: undefined :: f f
    In an equation for ‘x’: x = undefined :: f f