型レベル高階関数 （？）

id:eagletmt さんが Haskell の型レをやっているのでコメントをポチポチ書いています

ただ，これだとちょっと残念なことがあって，例えば2つ足す場合，

data Succ2F = Succ2F
instance Apply Succ2F x (Succ (Succ x))

と，わざわざ書かなければならない．
最初のコードがうまくいってくれれば，

apply (undefined :: n -> Succ (Succ n)) Zero :: Succ (Succ Zero)

となってくれると思うのに．

この発想は自分にはなかったので，ちょっと考えました． 型レベルのλ (System FのΛ)があったらいいのにーという風に理解したのですがそりゃ難しそうに思えます．
その代わりといってはなんですが，

data DoubleF f
instance (Apply f x x', Apply f x' x'') => Apply (Double f) x x''

とやっておけば，

apply (undefined :: DoubleF SuccF) Zero :: Succ (Succ Zero)

となるのではないかと思います． 他の型構築子についても DoubleF が使えるので，ある意味，型レの高階関数，といえるかもしれません．
型レベル継続渡し計算 なんてこともできます．