[Haskell-cafe] checking types with type families

[Dan Doel]

On Saturday 03 July 2010 2:11:37 pm David Menendez wrote:
> > {-# LANGUAGE MultiParamTypeClasses #-}
> > {-# LANGUAGE FunctionalDependencies #-}
> > {-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
> > 
> > class C a b c | a -> b, a -> c where
> >    op :: a -> b -> c
> > 
> > instance C Bool a a where op _ = id
> > 
> > main = putStrLn $ op True "done"
> > 
> > 
> > In this case, I've (arbitrarily) chosen the Bool instance to be a no-op
> > and pass through the types.  Because the dependent types are part of the
> > declaration header I can use type variables for them.
> 
> That's really weird. In particular, I can add this line to your code
> without problems:
> 
> foo = putStrLn $ if op True True then "done" else "."
> 
> but GHC complains about this one:
> 
> bar = putStrLn $ if op True True then op True "done" else "."
> 
> fd.hs:14:0:
>     Couldn't match expected type `Bool' against inferred type `[Char]'
>     When using functional dependencies to combine
>       C Bool [Char] String, arising from a use of `op' at fd.hs:14:38-51
>       C Bool Bool Bool, arising from a use of `op' at fd.hs:14:20-31
>     When generalising the type(s) for `bar'
> 
> On the other hand, this is fine, but only with a type signature:
> 
> baz :: a -> a
> baz = op True
> 
> I don't think this is an intended feature of functional dependencies.

Indeed. That instance declaration doesn't really make sense, and should 
probably be rejected. The functional dependencies on C say that b and c are 
dependent on a, so for any particular a, there should be exactly one b and one 
c such that C a b c is an instance.

Then the instance declares infinitely many instances C Bool a a. This is a 
violation of the fundep. Based on your error message, it looks like it ends up 
treating the instance as the first concrete 'a' it comes across, but who 
knows?

-- Dan