[Haskell-cafe] translating from fundeps into type families
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Mon Apr 7 23:56:07 EDT 2008
> 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.
More information about the Haskell-Cafe