Hi all, I believe there is a problem in the rule for instance declarations in "A Static Semantics For Haskell" [1] because the premise which ensures that instances for all superclasses are defined seems to hold trivially. [2] seems to have the same problem. I now describe the problem by showing how an incorrect program is accepted by the rules given in [1]. I omit many, many details that are irrelevant to this problem. Consider the following program: class C a class C a => D a instance D Int The instance environment IE for this program is built recursively by the rule for modules bodies (Fig. 15) and looks like this: IE = {forall a. D a => C a, D Int} We would expect that the rule for instance declarations (Fig. 26) rejects the program because there is no instance declaration for C Int. However, the rule uses the *whole* instance environment IE to check whether there is an instance declaration for C Int. But this holds trivially, because we have D Int in IE and the implication (forall a. D a => C a) lets us the conclude that C Int holds!! In other words: The rule uses the implication (forall a. D a => C a) to make sure that the very same implication is valid for a = Int. A possible solution might be to remove the constraint D Int before checking whether C Int holds. However, I am not sure whether the resulting rule is complete. An alternative solution would be to use a weaker entailment judgment. Any thoughts? Am I just missing some implicit condition on the instance environment? References: [1] @Article{Faxen02, title = "A static semantics for {Haskell}", author = "Karl-Filip Fax{\'e}n", journal = "Journal of Functional Programming", year = "2002", number = "4\&5", volume = "12", pages = "295--357", } [2] @Article{Hall1996, author = "Cordelia V. Hall and Kevin Hammond and Simon L. {Peyton Jones} and Philip L. Wadler", title = "Type classes in {Haskell}", journal = "ACM Transactions on Programming Languages and Systems", volume = "18", number = "2", pages = "109--138", year = "1996", } Cheers, Stefan Wehr -- Stefan Wehr Web: http://www.stefanwehr.de PGP: Key is available from pgp.mit.edu, ID 0B9F5CE4