consider class FD a b | a -> b instance CFD a b => FD a b class CFD a b instance CFD Bool Char and the constraint 'CFD Bool c'. logically, we know that if we have 'CFD Bool c', we also have 'FD Bool c', which implies that 'c' is uniquely determined, which implies that 'c~Char'. practically, the need to find an instance for 'CFD Bool c' does not generate a demand for implied instances that could lead to this improvement. q1: should there be such a forward demand? ie, instead of failing to find the instance for 'CFD Bool c', should the transitive closure of forward implications be taken into account for FDs, similar to the transitive closure of backward implications? without such forward inferences, consistency of FDs seems hard to guarantee, unless one conservatively rules out everything that might lead to an inconsistency. without such forward inference, implementations differ in their interpretation of this kind of code (as so often): Hugs rejects the program ("Instance is more general than a dependency allows"), which is conservative, but seems to make perfect sense: there's no FD for class 'CFD', so there's no guarantee that all those implied instances of class 'FD' will conform to its own FD. that is easily fixed, it seems: class FD a b | a -> b instance CFD a b => FD a b class FD a b => CFD a b instance CFD Bool Char now, there cannot be an instance of 'CFD' unless there also is an instance of 'FD', in such a way that the parameters of 'CFD' obey the FD of 'FD'. and, in fact, Hugs does now accept this code, and is able to improve 'CFD Bool c' to 'CFD Bool Char', reducing the latter as given: :t undefined :: CFD Bool c => c undefined :: Char but wait a second: we have given an instance of 'CFD', which according to the superclass constraint for that class, is valid only if there is a corresponding instance of 'FD', and there is such an instance of 'FD' if there is an instance of 'CFD'. in other words: if the 'CFD' instance is accepted, it is valid, if it isn't accepted, it is not valid. q2: is this treatment of recursion for class instances intended, or is it an unexpected artifact of the special treatment of superclass constraints? GHCi also accepts this code, but it doesn't seem to do the reduction or improvement: :t undefined :: CFD Bool c => c undefned :: CFD Bool c => c :: (CFD Bool c) => c actually, GHCi accepts the first program, too! perhaps it is delaying the FD consistency check until there is an actual rather than a possible FD conflict? unfortunately not, as we can see if we add a conflicting 'CFD' instance: class FD a b | a -> b instance CFD a b => FD a b class {- FD a b => -} CFD a b instance CFD Bool Char instance CFD Bool Bool note that the conflict is not in 'CFD' but in the implied instances of 'FD', which GHCi doesn't seem to take into account for any FD consistency check: *Main> :t undefined :: CFD Bool c => c undefined :: CFD Bool c => c :: (CFD Bool c) => c *Main> :t undefined :: CFD Bool Char => c undefined :: CFD Bool Char => c :: c *Main> :t undefined :: FD Bool c => c undefined :: FD Bool c => c :: (CFD Bool c) => c *Main> :t undefined :: FD Bool Char => c undefined :: FD Bool Char => c :: c only if we explicitly mention the inconsistent constraints together, and directly in terms of 'FD', not just in terms of 'CFD', do we get the expected error, and even then, the FD isn't used for improvement: *Main> :t undefined :: (CFD Bool Char,CFD Bool Bool) => c undefined :: (CFD Bool Char,CFD Bool Bool) => c :: c *Main> :t undefined :: (FD Bool Char,FD Bool Bool) => c <interactive>:1:0: Couldn't match expected type `Char' against inferred type `Bool' When using functional dependencies to combine FD Bool Bool, arising from the polymorphic type `forall c. (FD Bool Char, FD Bool Bool) => c' at <interactive>:1:0-44 FD Bool Char, arising from the polymorphic type `forall c. (FD Bool Char, FD Bool Bool) => c' at <interactive>:1:0-44 *Main> :t undefined :: (FD Bool Char,FD Bool c) => c undefined :: (FD Bool Char,FD Bool c) => c :: (CFD Bool c) => c this looks like a bug to me, or am i missing something? perhaps we fare better with TFs, as FD development in GHC was put on hold while the new foundations for TFs were put in place? unfortunately, we can't even define TFs in terms of classes, as has been discussed here before (in the context of using FD-based libaries in TF-based client code). what we'd like to write is something like: type family TF a type instance TF a = CTF a b => b -- won't work.. class {- FD a b => -} CTF a b instance CTF Bool Char instance CTF Bool Bool as with the FD-based variant, the definition of TF should not work unless there is a functional relationship between the parameters of 'CTF', but the 'TF' instance isn't even accepted syntactically ("Illegal polymorphic type in type instance"). q3: (a) are qualified types in type instances problematic, or just not yet implemented, or not yet investigated in theory? (b) what about the intended interaction of TFs and FDs in the example. it would seem to permit the use of FD-based code in TFs, as requested here earlier, but is this ever going to be supported? questions, questions,.. does anybody have answers?-) claus