On Tue, Mar 09, 2010 at 09:56:45AM -0500, Jan-Willem Maessen wrote:

It occurs to me to observe: if we give class constraints in data types some force, and write:

data Ord a => Set a = ...[internals go here]...

Would this be enough to cue us that Set has a more interesting kind than just * -> * ?

Yes. I was thinking something along the same lines. Could this just be another example of contravariance flipping the meaning of quantification? If we take the simpler example given:

class Iso a where conv :: item a -> item Int

let's give the whole type

class Iso a where conv :: forall (item :: * -> *) . item a -> item Int

It seems to me the issue may not be with newtype deriving, but with that universal quantification over a type constructor. If we were to declare 'Set' like so

data Ord a => Set a = ...

like Jan-Willem suggests, then it seems that 'Set' should not be able to unify with 'item' since it has the extra 'Ord' consraint on the contravariant argument to item and item is universally quantified. Item would need a psuedo-type like (Ord a => item :: a -> *) to match. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/