[SOLVED] Using * as a primitive on Nat

Using * as a primitive on Nat

I'm currently going through Sandy Maguire's Thinking with Types, and chapter 2 covers Terms, Types and Kinds. In it, there's an example of a simple interaction with the type-level primitives for performing arithmetic on Nats.

The following session is shown to work in the book, but fails on my machine:

Prelude> import GHC.TypeLits
Prelude GHC.TypeLits> :set -XDataKinds
Prelude GHC.TypeLits> :set -XTypeOperators
Prelude GHC.TypeLits> :kind! (1 + 17) * 3

<interactive>:1:1: error:
    * Expected kind `* -> Nat -> k0', but `1 + 17' has kind `Nat'
    * In the type `(1 + 17) * 3'

The next example in the book works, though:

Prelude GHC.TypeLits> :kind! (128 `Div` 8) ^ 2
(128 `Div` 8) ^ 2 :: Nat
= 256

I suspect the problem has something to do with * also indicates a kind. Sandy Maguire writes that this syntax is slated for deprecation, but if it's still around, I can see how GHCi thinks I mean the kind * instead of the type-level function *.

Am I on the right track, and if so, is there some flag I can use to make the example work?

Solution

I suspect the problem has something to do with * also indicates a kind.

Yes, that's the problem. It can be solved by using the -XNoStarIsType extension, that lets you treat * as just another type operator.

To refer to the kind formerly known as * you can import Type form Data.Kind. For example, the kind of Maybe is Type -> Type and the kind of StateT is Type -> (Type -> Type) -> Type -> Type.

Hopefully, at some point in the future -XNoStarIsType will become the default and we'll always use Type.