Have you looked at The singleton lib on hackage by Richard Eisenberg? Seems like it may be related. Or at least touches on related matters. 

On Sunday, December 1, 2013, Andras Slemmer <0slemi0@gmail.com> wrote:

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