Is it possible to get the infinite kind error in Haskell 98?

Question

I am implementing a kind system for a new functional programming language and I am currently writing the function to unify two kinds. There are four cases two consider:

+---------+---------+-------------------------------------------------------+ |   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 | +---------+---------+-------------------------------------------------------+ 

1. When both k1 and k2 are variables then they are instantiated to each other.
2. When only k1 is a variable then it is instantiated to k2 iff k1 doesn't occur in k2.
3. When only k2 is a variable then it is instantiated to k1 iff k2 doesn't occur in k1.
4. Otherwise we check whether k1 and k2 have the same name and arity, and unify their respective arguments.

For the second and third cases we need to implement the occurs check so that we don't get stuck in an infinite loop. However, I doubt that a programmer will be able to construct an infinite kind at all.

In Haskell, it's easy to construct an infinite type:

let f x = f 

However, I haven't been able to construct an infinite kind no matter how hard I tried. Note, that I didn't make use of any language extensions.

The reason I am asking this is because if it's not possible to construct an infinite kind at all then I won't even bother implementing the occurs check for kinds in my kind system.

Answer 1

data F f = F (f F) 

On GHC 7.10.1, I get the message:

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’ 

The message doesn't say it's an infinite kind, but that's essentially what it is when the occurs check fails.

Answer 2

Another simple example

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