I think you can simplify the example. Given class HasFoo a b | a -> b where foo :: a -> b instance HasFoo Int Bool where ... Is this legal? f :: HasFoo Int b => Int -> b f x = foo x You might think so, since HasFoo Int b => Int -> b is a substitution instance of HasFoo a b => a -> b but if we infer the type (HasFoo Int b => Int -> b) for f's RHS, we can then "improve" it using the instance decl to (HasFoo Int Bool => Int -> Bool), and now the signature isn't a substitution insance of the type of the RHS. Indeed, this is just what will happen if you try with GHC, because GHC takes advantage of type signatures when typechecking a function defn, rather than first typechecking the defn and only then comparing with the signature. I don't know what the answers are here, but there's more to this functional dependency stuff than meets the eye. Even whether one type is more general than another has changed! Simon | -----Original Message----- | From: qrczak@knm.org.pl [mailto:qrczak@knm.org.pl] | Sent: 17 December 2000 19:30 | To: haskell@haskell.org | Subject: Problem with functional dependencies | | | The following module is rejected by both | ghc -fglasgow-exts -fallow-undecidable-instances | and | hugs -98 | | -------------------------------------------------------------- | ---------- | class HasFoo a foo | a -> foo where | foo :: a -> foo | | data A = A Int | data B = B A | | instance HasFoo A Int where | foo (A x) = x | | instance HasFoo A foo => HasFoo B foo where | foo (B a) = foo a | -------------------------------------------------------------- | ---------- | | The error messsage says that the type inferred for foo in B's instance | is not general enough: the rhs has type "HasFoo B Int => B -> | Int", but | "HasFoo B foo => B -> foo" was expected.