I think one can change my earlier proposal to include this, but there are zero examples of this syntax, so I am likely making up some syntax that does not exist:
type instance (A_T a ~ A_T (RHS (Var x) a)) => A_B_C (RHS (Var x) a) (x->b) = A_B_C a b
type instance (A_T a ~ A_T (RHS (Var x) a)) => A_C_B (RHS (Var x) a) c = x -> A_C_B a c
type instance (A_T a ~ A_T (RHS [t] a)) => A_B_C (RHS [t] a) b = A_B_C a b type instance (A_T a ~ A_T (RHS [t] a)) => A_C_B (RHS [t] a) c = A_C_B a c
I am afraid you are right: this syntax does not exist. Type family instances cannot have a context. They are unconditional. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be