[Haskell-cafe] Could FDs help usurp an ATs syntactic restriction?

[Manuel M T Chakravarty]

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