Return GADT from function

Question

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?

Answer 1

The problem lies in your quantifiers in the type signature for findSubtree.

findSubtree :: (Ord a) => Tree c n a -> a -> Tree cc nn a

Although you obviously want c, n, and a to be universally quantified, not that cc and nn should be existentially quantified (the subtree found will have some color).

The way to deal with existentials in Haskell is to wrap them in a datatype. It isn't immediately obvious, but having a forall inside a data type is equivalent to an exists (if it existed in Haskell).

-- An existential type to represent a tree with _some_ color and depth
data SomeTree a where
  SomeTree :: Tree c n a -> SomeTree a

findSubtree :: (Ord a) => Tree c n a -> a -> SomeTree a
findSubtree Empty _ = SomeTree Empty
findSubtree (RTree left curr right) item
  | curr == item = SomeTree (RTree left curr right)
  | curr < item  = findSubtree left item
  | otherwise    = findSubtree right item
findSubtree (BTree left curr right) item
  | curr == item = SomeTree (BTree left curr right)
  | curr < item  = findSubtree left item
  | otherwise    = findSubtree right item

Answer 2

The problem is here:

findSubtree :: (Ord a) => Tree c n a -> a -> Tree cc nn a

Type variables a,c,n,cc,nn are universally quantified, meaning that the caller can choose whatever type/color they want for those variables. Clearly, the caller must be able to choose a,c,n, but in the code it is the function itself which chooses cc,nn.

The compiler complains that the result does not match with the caller's choice, much as in

foo :: Int -> a
foo x = x -- error: what if the caller chooses e.g. a ~ Bool ?

A possible solution is to wrap the result in an existential wrapper, as @Alec showed.