## Equality Constraints with Type Families

For the implementation of fixpoint recursive definitions for a datatype I have defined the family:

```
type family F a :: * -> *
type FList a x = Either () (a,x)
type instance F [a] = FList a
type instance F Int = Either One
```

for which we can define functor instances

```
instance (Functor (F [a])) where
fmap _ (Left _) = Left ()
fmap f (Right (a,x)) = Right (a,f x)
...
```

However, in the definition of recursive patterns over these representation, I need some coercions to hold such as

`F d c ~ F a (c,a)`

but in the current implementation they are evaluated as

`F d ~ F a /\ c ~(c,a)`

what does not express the semantics of "fully parameterized equality" that I was expecting

You can find a pratical example in (my conversions at the haskell-cafe mailing list)

In order to avoid this, the family could be redefined as

```
type family F a x :: *
type instance F [a] x = Either() (a,x)
type instance F Int x = Either One x
```

but this would mean that I cannot define instances for Functor (F a) because not enough parameters passed to F.

PS. This might sound more as a feature request than a bug, so sorry if I misplaced this information. I am willing to work on this subject to help supporting my test case.

## Trac metadata

Trac field | Value |
---|---|

Version | 6.9 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | Unknown |

Architecture | Unknown |