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