Fixed description (in fact the description is inconsistent with itself)

The behaviour of p2 specified in the kata description is inconsistent with the sample tests.

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)
-}

I've done this kata just with the help of the type signatures. Totally clueless about what's going on tho.

Type signature for symmetric is incorrect.

It's been 5 months and this issue is still not fixed. Please update the test!