[Haskell-cafe] checking types with type families

[Kevin Quick]

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.  I don't seem to have the same ability with type families:


{-# LANGUAGE RankNTypes, TypeFamilies, UndecidableInstances #-}

class C a where
     type A2 a
     type A3 a
     op :: a -> A2 a -> A3 a

instance {-forall a.-} C Bool where
     type A2 Bool = {-forall a.-} a
     type A3 Bool = A2 Bool
     op _ = id

main = putStrLn $ op True "done"


I cannot get this to compile as above or with either of the existential quantifications of a.  The first example may be the more erroneous one because the use of type variables would seem to violate the functional dependency assertions, but GHC accepts it nonetheless.

Regards,

-- 
-KQ