Playing with DataKinds - Kind mis-match errors

Question

I've been teaching myself about type-level programming and wanted to write a simple natural number addition type function. My first version which works is as follows:

data Z
data S n

type One = S Z
type Two = S (S Z)

type family Plus m n :: *
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n)

So in GHCi I can do:

ghci> :t undefined :: Plus One Two
undefined :: Plus One Two :: S * (S * (S * Z))

Which works as expected. I then decided to try out the DataKinds extension by modifying the Z and S types to:

data Nat = Z | S Nat

And the Plus family now returns a Nat kind:

type family Plus m n :: Nat

The modified code compiles but the problem is I now get an error when testing it:

Kind mis-match
Expected kind `OpenKind', but `Plus One Two' has kind `Nat'
In an expression type signature: Plus One Two
In the expression: undefined :: Plus One Two

I've searched for a solution but Google has failed me. Does a solution exist or have I hit some limit of the language?

I think in undefined :: SomeType, SomeType has to be of kind * only. — Satvik
If you really want to carry around a type witness at runtime, you can use the standard Proxy trick. — Daniel Wagner

Satvik Satvik · Accepted Answer · 2012-10-15T12:38:16

I think way you are testing is not correct. undefined can be of any type of kind * (I maybe wrong here).

Try this in ghci

ghci>:t (undefined :: 'Z)

<interactive>:1:15:
    Kind mis-match
    Expected kind `OpenKind', but `Z' has kind `Nat'
    In an expression type signature: Z
    In the expression: (undefined :: Z)

You can still get the type of Plus One Two by using :kind! in ghci

ghci>:kind! Plus One Two
Plus One Two :: Nat
= S (S (S 'Z))

Playing with DataKinds - Kind mis-match errors

1 Answers