Multiplication problem involving kind `Nat`

Question

Why does addition, subtraction and division of Nats work, but not multiplication?

λ> :set -XDataKinds
λ> :set -XTypeOperators
λ> import GHC.TypeLits
λ> :k! 1 + 2
1 + 2 :: Nat
= 3
λ> :k! 1 - 2
1 - 2 :: Nat
= 1 - 2
λ> :k! 5 `Div` 2
5 `Div` 2 :: Nat
= 2
λ> :k! 1 * 2

<interactive>:1:1: error:
    • Expected kind ‘* -> Nat -> k0’, but ‘1’ has kind ‘Nat’
    • In the type ‘1 * 2’

Intercontinental

With * refers to the Type kind. You should explicitly use * so :k 1 GHC.TypeLits.* 2. – Giefer

Answer 1

The * was used to specify a simple Type. As a result 1 is seen as something that takes as first type parameter a * (so Type) and as second type parameter a 2, and thus 1 should have kind * -> Nat -> something. GHC will parse an asterisk (*) as a reference to Type if the StarIsType extension is enabled, which is the default.

If you disable it, then the asterisk (*) will refer to the multiplication, for example:

Prelude> :set -XDataKinds 
Prelude> :set -XTypeOperators
Prelude> :set -XNoStarIsType
Prelude> import GHC.TypeLits
Prelude GHC.TypeLits> :k 1 * 2
1 * 2 :: Nat
Prelude GHC.TypeLits> :kind! 1 * 2
1 * 2 :: Nat
= 2

You can also explicitly specify the module where you use the * type family family from with:

Prelude> :set -XDataKinds 
Prelude> :set -XTypeOperators
Prelude> import GHC.TypeLits
Prelude GHC.TypeLits> :k 1 GHC.TypeLits.* 2
1 GHC.TypeLits.* 2 :: Nat
Prelude GHC.TypeLits> :kind! 1 GHC.TypeLits.* 2
1 GHC.TypeLits.* 2 :: Nat
= 2

Giefer

Great! Also, with -XNoStarIsType, GHC prints the kind for types as Type rather than *, which is clearer. – Intercontinental