Henning Thielemann wrote:

However the interesting part of a complete case analysis on type level peano numbers was only sketched in section "8.4 Closed type families". Thus I tried again and finally found a solution that works with existing GHC extensions:

You might like the following message posted in January 2005 http://www.haskell.org/pipermail/haskell-cafe/2005-January/008239.html (the whole discussion thread is relevant). In particular, the following excerpt -- data OpenExpression env r where -- Lambda :: OpenExpression (a,env) r -> OpenExpression env (a -> r); -- Symbol :: Sym env r -> OpenExpression env r; -- Constant :: r -> OpenExpression env r; -- Application :: OpenExpression env (a -> r) -> OpenExpression env a -> -- OpenExpression env r -- Note that the types of the efold alternatives are essentially -- the "inversion of arrows" in the GADT declaration above class OpenExpression t env r | t env -> r where efold :: t -> env -> (forall r. r -> c r) -- Constant -> (forall r. r -> c r) -- Symbol -> (forall a r. (a -> c r) -> c (a->r)) -- Lambda -> (forall a r. c (a->r) -> c a -> c r) -- Application -> c r shows the idea of the switch, but on more complex example (using higher-order rather than first-order language). That message has anticipated the tagless-final approach.