Lightweight dependent types + a proof of a 'mirror' function

gistfile1.hs

{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}

{-
based heavily on Ryan Ingram's lightweight type-level dependent programming
in haskell, posted to haskell-cafe:
http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html

I would suggest reading it before continuing further
-}

data Tip        = Tip
data Node x y z = Node x y z


-- the function we are making a proposition about, which mirrors a binary tree
type family   Mirror x :: *
type instance Mirror (Node x y z) = Node (Mirror z) y (Mirror x)
type instance Mirror Tip = Tip


-- haskell has 'open' type families, so we must close over them with a typeclass.
-- 'caseBinTree' represents a sort of 'type case', where the case structures must prove
-- that either 'b = Tip' or 'b = Node x y z' so we can 'close' the type class and not
-- have nonsensical instances potentially interfere with our proposition below.
class BinTree b where
	caseBinTree :: forall r.
				   b
				-> (b ~ Tip => r)
				-> (forall x y z. (BinTree x, BinTree z, b ~ Node x y z) => x -> z -> r)
				-> r

instance BinTree Tip where
	caseBinTree _ tip _ = tip
instance (BinTree x, BinTree z) => BinTree (Node x y z) where
	caseBinTree (Node x _ z) _ f = f x z

{-
Induction on trees.

This type states, that given a predicate 'p', closed over 'x' terms defined above by BinTree, if we have a proof of 'p Tip', and a proof
of 'forall b. p a -> p c -> p (Node a b c)' (i.e. that p holds for the left and right parts of a node), then p holds
for all 'p x'.
-}
treeInduction :: forall p x. BinTree x => x -> p Tip -> (forall a b c. (BinTree a, BinTree c) => p a -> p c -> p (Node a b c)) -> p x
treeInduction b tip node = caseBinTree b isTip isNode
  where
  	isTip :: x ~ Tip => p x
  	isTip = tip
  	isNode :: forall a x y z. (BinTree x, BinTree z, a ~ (Node x y z)) => x -> z -> p (Node x y z)
  	isNode x z = node (treeInduction x tip node) (treeInduction z tip node)
 

-- useful combinators at the type-level, just 'id' and 'const'
newtype I x   = I { unI :: x }
newtype K x y = K { unK :: x }

-- now prove that 'Mirror (Mirror x) = x'
proof1 :: (BinTree x, Mirror (Mirror x) ~ x) => x
proof1 = witness
  where
  	witness = unI $ treeInduction (undefined `asTypeOf` witness) (I Tip) (\x z -> I $ Node (unI x) undefined (unI z))