Idris returning dependent type signature error with if statement in type definition

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

I'm trying to get specific with the node definition is relation to the black height of its children. NodeEq - both children have same bh, NodeLh means left child has bh greater than right child by 1 and NodeRh is the reverse of NodeLh.

data Colour = Red | Black

data RBTree : Nat -> Colour -> Type -> Type where
      Empty : Ord elem => RBTree Z Black elem
      NodeEq : Ord elem => (left: RBTree p X elem) -> (val: elem) -> (col: Colour) ->
                          (h: Nat) -> (right: RBTree p Y elem) -> RBTree {h: Nat | if X == Black && Y == Black then (S p) else p} col elem
      NodeLh : Ord elem => (left: RBTree (S p) _ elem) -> (val: elem) -> (col: Colour) ->
                            (h: Nat) -> (right: RBTree p _ elem) -> RBTree (S (S p)) col elem
      NodeRh : Ord elem => (left: RBTree p _ elem) -> (val: elem) -> (col: Colour) ->
                            (h: Nat) -> (right: RBTree (S p) _ elem) -> RBTree (S (S p)) col elem

I'm having problem setting the black height for the NodeEq. What I'm trying to achieve, which might be obvious in the code below, is that if both children are black nodes, then the black height should be their bh + 1, else the black height should equal their height. However, I don't know how to write that into the definition. As you can see, I'm using to general {x:b|p} format.

This is the error I'm getting

  |
9 |                           (h: Nat) -> (right: RBTree p Y elem) -> RBTree {h: Nat | if X == Black && Y == Black then (S p) else p} col elem
  |                                                                            ^
unexpected ':'
expecting dependent type signature

I've also considered creating a 'where' or 'let' block but I'm not sure how to go about it.

Answer 1

The syntax in

RBTree {h: Nat | if X == Black && Y == Black then (S p) else p} col elem

is incorrect. The first index of RBTree has type Nat so you simply want to put a Nat-typed term there:

RBTree (if X == Black && Y == Black then (S p) else p) col elem

You are probably mixing up refinement type syntax (from something like Liquid Haskell) with Idris.