[Haskell-cafe] checking types with type families

[David Menendez]

On Sat, Jul 3, 2010 at 3:32 AM, Kevin Quick <quick at sparq.org> wrote:
> On Wed, 23 Jun 2010 00:14:03 -0700, Simon Peyton-Jones
> <simonpj at microsoft.com> wrote:
>
>> I'm interested in situations where you think fundeps work and type
>> families don't.  Reason: no one knows how to make fundeps work cleanly with
>> local type constraints (such as GADTs).
>
> Simon,
>
> I have run into a case where fundeps+MPTC seems to allow a more generalized
> instance declaration than type families.
>
> The fundep+MPTC case:
>
> {-# 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.

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>