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