Can we be very generic?

[treeowl]

The current tools can do a lot of things. For instance:

class c => IdC c
instance c => IdC c

class ForallT IdC p => Forall2 (p :: k1 -> k2 -> Constraint)
instance ForallT IdC p => Forall2 p

inst2 :: forall (p :: k1 -> k2 -> Constraint) . (a :: k1) (b :: k2)  . Forall2 p :- p a b
inst2 = Sub $ case instT :: ForallT IdC p :- IdC (p a b) of Sub Dict -> Dict

Forall can also do other fancy things:

class con c (s c) => What con s c
instance con c (s c) => What con s c

Now Forall (What con s) means that for all c, the constraint con c (s c) holds. This can be used to express that a class like

class C elem container | container -> elem where
  insert :: elem -> container -> container

is a "superclass" of a corresponding constructor class:

class Forall (What C f) => D f where
  mapIt :: (a -> b) -> f a -> f b
insert1 :: D f => a -> f a -> f a
insert1 = -- something using `inst`

Unfortunately, each such case must currently be constructed entirely by hand. Is there some way we can do this "generically", letting the user provide some representation of the structure of a constraint expression, where the holes should be, and (ugh) which holes should be tied together?

[ekmett]

I build up a bunch of interesting constructions in the category of constraints in my ekmett/hask package, maybe some of those ideas will help you. I'm not sure how well the result would fit here in the scope of this package though.

[oerjan]

I had an idea purely in my mind last autumn of doing something like this with de Bruijn indices and a Constraint-returning continuation monad in the type system.

Then I realized this was not just crazy, but also ridiculously verbose, and thought up InstV instead.