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. <span></span><br><br>On Sunday, December 1, 2013, Andras Slemmer <<a href="mailto:0slemi0@gmail.com">0slemi0@gmail.com</a>> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hi,<br><br>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!<br>
<br>The basic issue I was having is that whenever I wrote class instances for a lifted type (we'll use Nat):<br>
<br>class Class (n :: Nat)<br>instance Class Zero<br>instance (Class m) => Class (Succ m)<br><br>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 (<a href="https://ghc.haskell.org/trac/ghc/ticket/6150" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/6150</a>) which failed miserably, and for good reason!<br>

<br>However there is a way to do it anyway:)<br><br>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:<br>

<br>type W p = forall a. (p => a) -> a<br><br>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.<br><br>We will also need a way to "pattern match" on our lifted types, we will do this with an indexed GADT:<br>

<br>data WNat n where -- W for Witness<br>    WZero :: WNat Zero<br>    WSucc :: WNat n -> WNat (Succ n)<br><br>And finally the neat part; one can write a general typeclass-polymorphic induction principle on these wrapped constraints (or a "constraint-fold"):<br>

<br>natFold :: WNat n -> W (p Zero) -> (forall m. W (p m) -> W (p (Succ m))) -> W (p n)<br><br>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)"<br>

This function is precisely what we need in order to construct the generic instance!<br><br>(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: <a href="http://lpaste.net/96429" target="_blank">http://lpaste.net/96429</a>)<br>

<br>Now we can construct the generic instance:<br><br>genericClass :: WNat n -> (Class n => a) -> a<br>genericClass n = natFold n (\x -> x) (\f x -> f x) -- Cannot use id as that would try to unify away our constraints<br>

<br>Or equivalently:<br><br>class WNatClass n where<br>    witness :: WNat n<br>instance WNatClass Zero where<br>    witness = WZero<br>instance (WNatClass m) => WNatClass (Succ m) where<br>    witness = WSucc witness<br>

<br>genericClass' :: (WNatClass n) => (Class n => a) -> a<br>genericClass' = genericClass witness<br><br>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).<br>

<br>What do you think?<br><br></div>ex<br></div>
</blockquote>