From: John Meacham <john@repetae.net> Subject: Re: Restricted Data Types however, what prevents the following from being _infered_ return Foo :: Moand m => m Foo so, we think we can specialize it to return Foo :: Set Foo however, we no longer have the constraint that Foo must be in Eq! Maybe I wasn't up-front enough about this in the paper: RDTs add a new form of constraint in contexts, wft t, meaning that type t is well-formed. While base types and type variables can be assumed to be well-formed, other types may only be used at all in the context of a suitable well-formedness constraint. That means that the Monad class is not allowed to declare return :: a -> m a because there's no guarantee that the type m a would be well-formed. The type declared for return has to become return :: wft (m a) => a -> m a i.e. when return is called, it has to be passed a dictionary proving that m a is well-formed. In the case of Set, that's an Eq a dictionary. In your example, the most general type of return Foo is (Monad m, wft (m Foo)) => m Foo, and when you instantiate m to Set, you're left with the contraint wft (Set Foo), which reduces to Eq Foo. The changes to the type system are that all typing rules have to add wft t constraints to the context, for every type t that appears in them. Fortunately most can be immediately discarded, since base types are always well-formed, and data type definitions imply constraint reduction rules that eliminate wft constraints unless the datatype is restricted. For example, wft [a] reduces to wft a, because lists place no restriction on their element type. Wft constraints on type *variables* can be discarded where the variables are generalised, *provided* the instantiation rule only permits variables to be instantiated at well-formed types. There's no need to write the type of reverse as wft a => [a] -> [a], if polymorphic type variables can only every be instantiated to well formed types. The only wft constraints that cannot be discarded are thus those where the type that must be well-formed is an application of a type constructor variable, such as wft (m a) in the type of return. That suggests that wft constraints ought not to be too common in real code, but they do crop up in monadic library code-- class Monad m where return :: wft (m a) => a -> m a (>>=) :: (wft (m a), wft (m b)) => m a -> (a -> m b) -> m b That's why, without some clever optimisation, RDTs will lead to massive extra dictionary passing (in implementations that use dictionaries). "It'll be just fine as long as you don't use monads" isn't really a good enough argument, is it?! John