[Haskell-cafe] translating from fundeps into type families

[Manuel M T Chakravarty]

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