Nicolas Frisby:

...

From the error below, I'm inferring that the RHS of the associated type definition can only contain type variables from the instance head, not the instance context. I didn't explicitly see this restriction when reading the GHC/Type_families entry.

Could perhaps the "a b -> bn" functional dependency of the TypeEq class lift this restriction for bn? This isn't my ball park, but that idea has my hopes up :).

<haskell> {-# LANGUAGE TypeFamilies #-}

import TypeEq

-- Attempting to encapsulate TypeEq behind an associated type.

class EQ a b where type BN a b

instance TypeEq a b bn => EQ a b where type BN a b = bn </haskell>

results in an error

<ghci> /tmp/Test.hs:9:16: Not in scope: type variable `bn' Failed, modules loaded: none. </ghci>

GHC is right, you cannot use 'bn' in the definition of the type family instance. I agree that the documentation needs to make this clearer. Generally,

class EQ a b where type BN a b

instance TypeEq a b bn => EQ a b where type BN a b = bn

is really just syntactic sugar for

type family BN a b class EQ a b

type instance BN a b = bn instance TypeEq a b bn => EQ a b

where it is clear that 'bn' is not in scope in the rhs of the type instance. Unfortunately, you cannot wrap a type class constraint into a type synonym family (independent of whether it is associated or not). Incidentally, type equalities (which are part of the type family implementation) enable a much more compact definition of the type equality predicate: data True; data False; class EqTyP a b result instance (result ~ True) => EqTyP a a result instance (result ~ False) => EqTyP a b result Manuel