Encapsulation of GADT pattern matches

Question

In this code there are repeated fragments:

insert x (AATree t) = case insert' x t of
    Same t -> AATree t
    Inc t  -> AATree t

insertBlack :: (Ord a) => a -> AANode Black (Succ n) a -> AnyColor (Succ n) a
insertBlack x (Black l y r)
    | x < y     = case insert' x l of
          Same l' -> AnyColor $ Black l' y r
          Inc  l' -> AnyColor $ skew l' y r
    | otherwise = case insert' x r of
          Same r' -> AnyColor $ Black l y r'
          Inc r'  -> AnyColor $ Red   l y r'

So it is tempting to write a function:

insert2 same inc x l = case insert' x l of
          Same aa -> same aa
          Inc aa  -> inc aa

And use it everywhere, e.g.:

insert x (AATree t) = insert2 AATree AATree x t

Is there a way to write insert2? The naive approach doesn't typecheck.

Answer 1

Since you are case branching on a GADT, presumably the entire type of aa is not known on the outside of the case expression. This means you need higher-rank types for the function arguments of insert2 so that they can be used at whatever type aa happens to be.

This requires {-# LANGUAGE Rank2Types #-} as well as an explicit type annotation for insert2. The exact annotation needed depends on your GADT and insert' types. Looking at your linked code I think you want something like

insert2 :: (Ord a) =>
    (AANode Black (Succ n) a -> b)
    -> (forall c. AANode c n a -> b)
    -> a -> AANode c n a -> b