Idris function getting pattern matching error on red black tree implementation

Question

I'm working on a red black tree implementation in Idris. In this implementation, the node, in addition to carrying information about its value and colour, also carries information about its black height (which is the number of black nodes from that node to any leaf, not including itself).

data Colour = Red | Black

data RBTree : Nat -> Type -> Type where
      Empty : Ord elem => RBTree Z elem
      Node : Ord elem => (left: RBTree p elem) -> (val: elem) -> (col: Colour) ->
                          (h: Nat) -> (right: RBTree q elem) -> RBTree h elem

In order to implement the insert function, I have to implement a balance function, which fixes any situation where a red node has a red child (which breaks a red-black rule). Here's one of the situation it fixes.

           (n)  Bz                                       (S n) Ry
               /  \                                           /  \
              /    \                                         /    \
        (n)  Ry     d          ---->                    (n) Bx     Bz (n)
            /  \                                           / \     / \
           /    \                                         /   \   /   \
      (n) Rx     c                                       a     b c     d
         /  \
        /    \
       a      b

Bx means node x is Black, Rx means node x is Red. The n in brackets is the black height of that node.

Here's the code for balance.

balance : Ord elem => RBTree p elem -> elem -> Colour -> Nat -> RBTree q elem -> RBTree h elem
balance (Node (Node a x Red n b) y Red n c) z Black n d = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
balance (Node a x Red n (Node b y Red n c)) z Black n d = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
balance a x Black n (Node (Node b y Red n c) z Red n d) = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
balance a x Black n (Node b y Red n (Node c z Red n d)) = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
balance left val col ht right = (Node left val col ht right)

The first line (not the type definition) is what is in the diagram.

When I run it, I get this:

   |
27 | balance (Node (Node a x Red n b) y Red n c) z Black n d = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking left hand side of balance:
Can't match on balance (Node (Node a x Red n b) y Red n c) z Black n d

I'm not sure what the error is. Could it be related to the p and q in the type definition?