How to specify a type family with multiparameter injectivity?

Question

I have a typeclass A with a non injective associated type Context

class A a where
   type Context a

so many instances of A can have the same Context.

Some instances of A are also instances of the class AA, that has two additional associated types, B and C.

class (A a) => AA a where
   type B a
   type C a
   problematic :: Context a -> B a -> C a -> a

The intention is that given a Context, the combination of B a and C a uniquely identify a, but I don't know how to express this.

I know it's possible to make constraints like

class A a where
   type B a = b | b -> a

, but what I need is some kind of constraint with multiple parameters, like (Context a, B a, C a) -> a. How can this be achieved?

Answer 1

Perhaps you could return a pair. I haven't tested this, but it would look something like this:

type family Fst a where Fst '(a, b) = a
type family Snd a where Snd '(a, b) = b
type B a = Fst (BC a)
type C a = Snd (BC a)

class A a => AA a where
    type BC a = b | b -> a

You may need some kind signatures in there to give the type checker a hint; the compile-time-level version of the type checker tends to monomorph its types a bit earlier than the runtime-level one.

Answer 2

This neat solution was posted by Edward Kmett on reddit.

class A a where
  type Context a

class (A a, Context a ~ ctx, B a ~ b, C a ~ b,) => AA' a ctx b c | a -> ctx b c, ctx b c -> a where
  type B a 
  type C a

type AA a = AA' a (Context a) (B a) (C a)