Hi, I stumbled upon something pretty neat, and although I'm 95% sure Oleg did this already 10 years ago in Haskell98 I thought I'd share it because I find it gorgeous! The basic issue I was having is that whenever I wrote class instances for a lifted type (we'll use Nat): class Class (n :: Nat) instance Class Zero instance (Class m) => Class (Succ m) I always had to litter my code with "(Class n) =>" restrictions even in places where they just shouldn't belong. However my gut feeling was that the generic instance "should" be implied, as we covered all cases. A while ago I proposed a new syntax to do just this ( https://ghc.haskell.org/trac/ghc/ticket/6150) which failed miserably, and for good reason! However there is a way to do it anyway:) What we need is basically a way to "construct" an instance for the fully polymorpic case: "instance Class n". We cannot do this directly as it would overlap with our original instances (and we couldn't implement it anyway), we need another way of representing class instances: type W p = forall a. (p => a) -> a W p simply "wraps" the constraint p into a function that eliminates the constraint on a passed in value. Now we can treat a constraint as a function. We will also need a way to "pattern match" on our lifted types, we will do this with an indexed GADT: data WNat n where -- W for Witness WZero :: WNat Zero WSucc :: WNat n -> WNat (Succ n) And finally the neat part; one can write a general typeclass-polymorphic induction principle on these wrapped constraints (or a "constraint-fold"): natFold :: WNat n -> W (p Zero) -> (forall m. W (p m) -> W (p (Succ m))) -> W (p n) W (p Zero) in the p ~ Class case corresponds to "instance Class Zero", and (forall m. W (p m) -> W (p (Succ m))) corresponds to "instance (Class m) => Class (Succ m)" This function is precisely what we need in order to construct the generic instance! (Note: the implementation of natFold is NOT trivial as we need to wrestle with the type checker in the inductive case, but it is a nice excercise. The solution is here: http://lpaste.net/96429) Now we can construct the generic instance: genericClass :: WNat n -> (Class n => a) -> a genericClass n = natFold n (\x -> x) (\f x -> f x) -- Cannot use id as that would try to unify away our constraints Or equivalently: class WNatClass n where witness :: WNat n instance WNatClass Zero where witness = WZero instance (WNatClass m) => WNatClass (Succ m) where witness = WSucc witness genericClass' :: (WNatClass n) => (Class n => a) -> a genericClass' = genericClass witness Now we can decouple all our "(Class n) =>" and similar constraints, all we need is a WNatClass restriction, which I think is a good enough trade-off (and it's not really a restriction anyway). What do you think? ex