手抜きした

{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

data Zero where
    Zero :: Zero
data Succ a where
    Succ :: (Nat a) => a -> Succ a

class Nat a
instance Nat Zero
instance (Nat a) => Nat (Succ a)

data TNil

data Tree a left right  where
    Nil :: Tree b TNil TNil
    Node :: a -> Tree a ll lr -> Tree a rl rr -> Tree a (Tree a ll lr) (Tree a rl rr)

instance Show (Tree b TNil TNil) where
    show Nil = "nil"

instance (Show a,Show (Tree a ll lr),Show (Tree a rl rr)) => Show (Tree a (Tree a ll lr) (Tree a rl rr)) where
    show (Node v l r) = "{ " ++ show v ++ " | " ++ show l ++ " , " ++ show r ++ " }"

type family TreeMap newT l
type instance TreeMap newT TNil = TNil
type instance TreeMap newT (Tree a left right) = Tree newT (TreeMap newT left) (TreeMap newT right)

treeMap :: (a -> b) -> Tree a left right -> Tree b (TreeMap b left) (TreeMap b right)
treeMap f Nil = Nil
treeMap (f :: a -> b) (Node v l r :: Tree a left right) = goal
    where
      g :: (Tree a ll lr ~ left) => Tree a ll lr -> Tree b (TreeMap b ll) (TreeMap b lr)
      g tr = (treeMap f tr :: TreeMap b left)

      h :: (Tree a rl rr ~ right) => Tree a rl rr -> Tree b (TreeMap b rl) (TreeMap b rr)
      h tr = (treeMap f tr :: TreeMap b right)

      {-
        (Tree a ll lr ~ left)で
        TreeMap b left => TreeMap b (Tree a ll lr) => Tree b (TreeMap b ll) (TreeMap b lr)
       -}

      goal :: Tree b (TreeMap b left) (TreeMap b right)
      goal = Node (f v) (g l) (h r)


leftsubtree :: Tree a l r -> l
leftsubtree (Node a l r) = l

rightsubtree :: Tree a l r -> r
rightsubtree (Node a l r) = r

leaf v = Node v Nil Nil

tree1 = leaf (1 :: Int)
tree2 = leaf (2 :: Int)
tree3 = Node 3 tree1 tree2
tree4 = leaf (4 :: Int)
tree5 = Node 5 tree3 tree4

tree1_ :: Tree Int (Tree Int TNil TNil) (Tree Int TNil TNil)
tree1_ = treeMap pred tree1
tree3_ = treeMap show tree3
tree5_ = treeMap succ tree5

眠いので寝ます。