Andras Slemmer wrote:
I stumbled upon something pretty neat, and although I'm 95% sure Oleg did this already 10 years ago in Haskell98
You're quite right about this: Chung-chieh Shan and I did this reification of constraint in December 2003, and almost in Haskell 98 (we needed Rank2 types though). It was described in the following paper http://okmij.org/ftp/Haskell/types.html#Prepose We called this transformation reflection/reification. I'm writing though to show a dual formulation to your development of using singletons. It gets by without GADTs and uses very few extensions: essentially Haskell98 with Rank2 types. {-# LANGUAGE RankNTypes #-} data Zero data Succ a class Class n instance Class Zero instance (Class m) => Class (Succ m) -- Tagless final class Sym repr where z :: repr Zero s :: repr n -> repr (Succ n) newtype R x = R{unR:: x} -- the identity interpreter instance Sym R where z = R undefined s _ = R undefined newtype S x = S Integer -- for show instance Sym S where z = S 0 s (S x) = S (x + 1) newtype Reify n = Reify (forall a. (Class n => n -> a) -> a) instance Sym Reify where z = Reify (\f -> f (unR z)) s (Reify f) = Reify (\g -> f (g . unR . s . R)) genericClass :: (forall repr. Sym repr => repr n) -> (Class n => a) -> a genericClass m f = case m of Reify k -> k (const f)