型付けされたTree とその上の関数

{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

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 subs where
    Nil :: Tree b (TNil,TNil)
    Node :: a -> Tree a subs1 -> Tree a subs2 -> Tree a (Tree a subs1,Tree a subs2)

type family TreeMap ty tr
type instance TreeMap ty TNil = TNil
type instance TreeMap ty (Tree a (left,right)) = Tree ty (TreeMap ty left,TreeMap ty right)

treeMap :: (a -> b) -> Tree a subs -> TreeMap b (Tree a subs)
treeMap (f :: a -> b) (Nil :: Tree a subs) = (Nil :: Tree b (TNil,TNil))
-- この先

leaf v = Node v Nil Nil

tree1 = leaf (1 :: Int)
tree2 = leaf (2 :: Int)

treeMapの実装で嵌り中

取りあえず

treeMap (f :: a -> b) (Node v left right :: Tree a (lefttype,righttype)) = undefined
    where
      l :: (Tree hoge1 hoge2 ~ lefttype) => Tree hoge1 hoge2
      l = left
      -- この後もhoge1とhoge2を使いたいよなぁっていう