Are fundeps the right model at all?

[Marcin 'Qrczak' Kowalczyk]

Could somebody show an example which requires fundeps and cannot be
expressed using a simpler model explained below - a model that I can
even understand? Is the model self-consistent at all?

Each class is associated with a set of subsets of type variables in
its head. Let's call it the set of keys. The intuitive meaning of a
key is that types corresponding to these variables are sufficient to
determine which instance to choose. They correspond to lhss of some
fundeps.

Plain classes without explicitly written keys correspond to having
a single key consisting of all type variables. Keys influence the
typechecking thus:

- A type is unambiguous if for every class constraint in it there
  exists its key such that types in the constraint corresponding to
  type variables from the key contain no type variables which are
  absent in the type itself.

- All class methods must have unambiguous types, i.e. for each method
  there must be a key whose all type variables are present in the
  method's type.

- For each key, there must be no pair of instances whose heads
  projected to the class parameters from the key overlap.

- For each class constraint of an unambiguous type an each its key
  there must be an instance found basing on this key, or the type is
  incorrect because of missing instances. Moreover, instances found
  basing on all keys must be identical.

- Perhaps something must be said about class contexts and instance
  contexts. I'm not sure what yet.


Examples:

class Collection c e | c where
    empty  :: c
    insert :: c -> e -> c

class Monad m => MonadState s m | m where
    get :: m s
    put :: s -> m ()

newtype State s a = State {runState :: s -> (a,s)}
instance Monad (State s)
instance MonadState s (State s)
test1:: Int -> Int
test1 x = snd (runState get x) -- Not ambiguous.

class IOvsST io st | io, st where
    -- Two single-element keys.
    ioToST :: io -> st
    stToIO :: st -> io

instance IOvsST (IORef a) (STRef s a) where
    ioToST = unsafeCoerce#
    stToIO = unsafeCoerce#

test2:: IORef a -> IORef a
test2 = ioToST . stToIO -- Not ambiguous.

class Foo a b | a
instance Foo Int [a]
-- This is rejected by Hugs (with fundep a->b) but I would definitely
-- accept it.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK