Creating instances of a type class based on runtime comparisons in Haskell

Following the technique described here, I've been using the constraints and reflection packages to create local instances of a type class Rel that represents (at the type level) a relation on values of type t.

Now I would to create instances based on comparisons of runtime values, allowing code that requires those comparisons to hold at runtime to express that requirement as a constraint where the values are represented by some kind of type-level 'variable'. I can "sort of" accomplish this with the following code.

usingIf :: t -> t -- Two values of type t to compare -> (forall s1 s2 . Proxy s1 -> Proxy s2 -> Rel (Var s1) (Var s2) => b) -- ^ Then branch: a term with a constraint that requires -- two type-level "variables" to be in a relation 'Rel' -> b -- Else branch: the term to evaluate if the values (of type t) are -- not in the relation -> b usingIf v1 v2 ifTrue ifFalse = if cmp v1 v2 then using (Def Rel (DVar (Proxy :: Proxy 0)) (DVar (Proxy :: Proxy 1))) (ifTrue (Proxy :: Proxy 0) (Proxy :: Proxy 1)) else ifFalse

This code takes two t values, v1 and v2, and compares them. If cmp returns true, then an instance, Def Rel ..., of the type class Rel is created to represent the fact that these values are in the relation, where v1 and v2 are represented at the type level by two variables with id 0 and 1.

This code compiles and runs as I would expect (in my project), but the problem is that the ids of the variables will not be unique if multiple usingIf applications are composed. What I really need is, for instance, a way of tracking how many instances have been added to the Rel dictionary or something equivalent to that so that I can create fresh ids for each Var.

Any suggestions on how I could tackle this problem? I'd prefer not to use Template Haskell, but am willing to if that's the only/cleanest option.