Re: [Haskell-cafe] Lightweight type-level dependent programming in Haskell

I recently discovered an interesting way of closing typeclasses while playing with type-level peano naturals:

...

class Nat n where caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> r

I usually use this one: class Nat n where caseNat :: p Z -> (forall m. Nat m => p (S m)) -> p n instance Nat Z where caseNat pz _ = pz instance Nat n => Nat (S n) where caseNat _ psm = psm