Background
I am working on writing a red black tree implementation in Haskell using dependent types and am having some trouble understanding why the code below does not work. What I wanted to do as a sort of warm up exercise was to find a subtree given an arbitrary value. Unfortunately, I had some trouble getting the code to compile and eventually moved on. However, I am still confused about exactly why this does not compile and what I could do to get it to work. I haven't been able to find any examples like this, nor anything showing why this doesn't work.
The Code
data NaturalNum = Z
| S NaturalNum
deriving Show
data Color :: * where
Red :: Color
Black :: Color
deriving Show
data Tree :: Color -> NaturalNum -> * -> * where
Empty :: Tree Black Z a
RTree :: Tree Black natNum a -> a -> Tree Black natNum a -> Tree Red natNum a
BTree :: Tree leftColor natNum a -> a -> Tree rightColor natNum a -> Tree Black (S natNum) a
deriving instance (Show a) => Show (Tree c n a)
findSubtree :: (Ord a) => Tree c n a -> a -> Tree cc nn a
findSubtree Empty _ = Empty
findSubtree (RTree left curr right) item
| curr == item = RTree left curr right
| curr < item = findSubtree left item
| otherwise = findSubtree right item
findSubtree (BTree left curr right) item
| curr == item = BTree left curr right
| curr < item = findSubtree left item
| otherwise = findSubtree right item
The Error Message
There are two more almost identical error messages complaining about the other constructors.
• Could not deduce: cc ~ 'Black
from the context: (c ~ 'Black, n ~ 'Z)
bound by a pattern with constructor:
Empty :: forall a. Tree 'Black 'Z a,
in an equation for ‘findSubtree’
at lib/RedBlackTree.hs:246:13-17
‘cc’ is a rigid type variable bound by
the type signature for:
findSubtree :: forall (c :: Color) (n :: NaturalNum) a (cc :: Color) (nn :: NaturalNum).
Tree c n a -> a -> Tree cc nn a
at lib/RedBlackTree.hs:245:16
Expected type: Tree cc nn a
Actual type: Tree 'Black 'Z a
• In the expression: Empty
In an equation for ‘findSubtree’: findSubtree Empty _ = Empty
• Relevant bindings include
findSubtree :: Tree c n a -> a -> Tree cc nn a
(bound at lib/RedBlackTree.hs:246:1)
My Confusion
Based on the error message it looks to me that I cannot return a GADT parameterized by an unconstrained color and black height. However, I find this fairly unsatisfactory. I see that it would be hard to check the types of other parts of the program if you had this little information about the return types of the findSubtree
function, but finding a subtree seems like a fairly reasonable thing to want to do. Is this a restriction that comes along with using GADTs?
Most importantly, What changes would I have to make to the above code to be able to return an arbitrary subtree from this data structure, and what is an explanation for exactly why the given code will not compile?