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