Ganesh Sittampalam:

Can I have some advice on translating the attached Test1.hs into type families? My attempt at doing so is in Test1a.hs, but firstly it requires FlexibleInstances where Test1.hs didn't, and secondly it fails because it can't infer the instance for Bar (Either Int Int) whereas the fundeps version had no problems there.

You need to write the instance as instance (b ~ TheFoo a, Foo a) => Bar (Either a b) where bar (Left a) = foo' a bar (Right b) = foo' (foo b :: a) Generally, you can't have type synonym families in instance heads. GHC should have complained about this despite your use of FlexibleInstances. (I'll fix that.) Unfortunately, the above will currently only go through if you specify UndecidableInstances. Nothing about it is undecidable, though, so the flag should not be required. Part of the trouble here is that, although we just completed a formal statement about the decidability of type checking for type families *without* taking context simplification into account <http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html

, we are still lacking a formal statement about type checking for type families *with* context simplification.

My conjecture at the moment is that equalities of the form tv ~ F tv1 .. tvn where tv and tvi are distinct type variables should always be fine in class instance contexts and correspond to what is permitted for FDs. (However, previous experience with FDs and TFs clearly shows that any statements about decidability and completeness in this space are to be regarded with caution until they have been formalised rigorously.) I'll create a trac ticket with your example. Cheers, Manuel