Approved

I've copied the definitions at the end of the initial solution.

Fixed, thank you.

Great kata!

I suggest to add types from Kata.AdditionCommutes.Definitions as a comment after import to the initial task code, so that if working in an editor/IDE, it would be easier to start witout copying definitions 3 times from the task details.

import Kata.AdditionCommutes.Definitions
  ( Z, S
  , Natural(..), Equal(..)
  , (:+:))

{-
data Z
data S n

data Natural :: * -> * where
  NumZ :: Natural Z
  NumS :: Natural n -> Natural (S n)

data Equal :: * -> * -> * where
    EqlZ :: Equal Z Z
    EqlS :: Equal n m -> Equal (S n) (S m)

type family (:+:) (n :: *) (m :: *) :: *
type instance Z :+: m = m
type instance S n :+: m = S (n :+: m)
-}