Why does addition, subtraction and division of Nat
s 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