[Haskell] Problem with superclass entailment in "A Static Semantics for Haskell"

[Stefan Wehr]

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