Recently I needed to define a class with a restricted set of instances. After some failed attempts I looked into the DataKinds extension and in "Giving Haskell a Promotion" I found the example of a new kind Nat for type level peano numbers. 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: data Zero data Succ n class Nat n where switch :: f Zero -> (forall m. Nat m => f (Succ m)) -> f n instance Nat Zero where switch x _ = x instance Nat n => Nat (Succ n) where switch _ x = x That's all. I do not need more methods in Nat, since I can express everything by the type case analysis provided by "switch". I can implement any method on Nat types using a newtype around the method which instantiates the f. E.g. newtype Append m a n = Append {runAppend :: Vec n a -> Vec m a -> Vec (Add n m) a} type family Add n m :: * type instance Add Zero m = m type instance Add (Succ n) m = Succ (Add n m) append :: Nat n => Vec n a -> Vec m a -> Vec (Add n m) a append = runAppend $ switch (Append $ \_empty x -> x) (Append $ \x y -> case decons x of (a,as) -> cons a (append as y)) decons :: Vec (Succ n) a -> (a, Vec n a) cons :: a -> Vec n a -> Vec (Succ n) a The technique reminds me on GADTless programming. Has it already a name?