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

Question

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.

Answer 1

A possible trick is to hook in to the generativity that already exists in the type system.

The following function is ill-typed:

f :: a -> b -> a
f x y = x `asTypeOf` y

Even though b might actually be the same as a in some instantiation, since it also may not, a and b are treated as different types. Particularly for higher rank types, the way this is implemented is that the compiler makes up a type on the fly for each quantified type variable, so x :: Fresh_a and y :: Fresh_b. These Fresh_as are the "rigid" variables the compiler complains about. Essentially, the dual thing happens when opening an existential. In fact, I'll use an existential since it seems a bit clearer and more explicit.

-- Needs ExistentialQuantification and PolyKinds, but the same effect
-- could be accomplished without either.
data Gen = forall (n :: k). Gen (Proxy n)
gen = Gen Proxy -- Probably need to turn off the monomorphism restriction

usingIf :: t -> t
        -> (forall s1 s2 . Proxy s1 -> Proxy s2 -> Rel (Var s1) (Var s2) => b)
        -> b 
        -> b
usingIf v1 v2 ifTrue ifFalse = 
    if cmp v1 v2 then
      case gen of Gen p -> -- the compiler has forgotten what went in to gen so it must
          case gen of Gen q -> -- assume p and q have types distinct from everything
              using (Def Rel (DVar p) (DVar q)) (ifTrue p q)
    else 
      ifFalse

I don't have your code so I have no idea if this will actually work for you, but it is how I would start attacking it. You may need to massage it a little.