Iavor Diatchki wrote:
http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies#Lo...
There is nothing about the system being unsound there. Furthermore, I am unclear about the problem described by the link... The two sets of predicates are logically equivalent (have the same set of ground instances), here is a full derivation:
(B a b, C [a] c d) using the instance (B a b, C [a] c d, C [a] b Bool) using the FD rule (B a b, C [a] c d, C [a] b Bool, b = c) using b = c (B a b, C [a] c d, C [a] b Bool, b = c, C [a] b d) omitting unnecessary predicates and rearranging: (b = c, B a b, C [a] b d)
The derivation in the other direction is much simpler: (b = c, B a b, C [a] b d) using b = c (b = c, B a b, C [a] b d, C [a] c d) omitting unnecessary predicates (B a b, C [a] c d)
You're right, I think I'm mixing up soundness with completeness and termination. My thought was that not explicitly mentioning the b=c constraint could lead to the type inference silently dropping this fact and letting an inconsistent set of instance declarations "go through" without noticing. But that would only be important in a setting where inconsistent instances are not reported early via the consistency condition but late when actually constructing terms. The consistency condition should be enough for soundness (no inconsistent axioms accepted), but I didn't dwell enough into FD to know such things for sure. Regards, apfelmus