[bitc-dev] Type Classes and conflicting instantiations

[Mark P Jones]

| 1. (From Reading): It is an error to have two instantiations 
| for a type
| class that instantiate that class over the same types. That 
| is, given a
| single-parameter type class (TC 'a), it is an error to have two
| instantiations of that type class that both instantiate (TC char).

Correct.  In Haskell, for example, the following program will
trigger an error:

  module M where
  class TC a where c :: a -> Bool
  instance TC Char where c x = (x == 'a')
  instance TC Char where c x = False

It's clear that this should not be an acceptable program; if
it were, then we would have two distinct meanings for the
expression (c 'a').

| 2. (From your email): It is sufficient to make typing 
| decisions based on
| what is in scope at the moment you infer the type.

Not just sufficient; it is not possible to make typing judgments
based on information that is not in scope.

| How do these two statements interact? I could take them to 
| mean either:
| 
|   a) It is an error to have have two instantiations of (TC char) that
|      are simultaneously in scope

This is correct.

| OR
| 
|   b) The rule is a whole-program rule, and it is an error to have two
|      instantiations of (TC char) even if they are never simultaneously
|      in scope.
| 
| Question: Which interpretation is correct?

This is also correct, but there's a catch.  If a program contains two
instantiations of (TC char), then there is at least one module in the
program where both instances are in scope.  This is because of the
"viral" quality of instances in Haskell.  Here's a relevant part of
the Haskell report (Section 5.4):

  "Instance declarations cannot be explicitly named on import or export
  lists. All instances in scope within a module are always exported and
  any import brings all instances in from the imported module. Thus, an
  instance declaration is in scope if and only if a chain of import
  declarations leads to the module containing the instance declaration."

So, you can compile the following three Haskell modules without problem:

  module M where
  class TC a where c :: a -> Bool

  module M1 where
  import M -- brings the definition of TC into scope
  instance TC Char where c x = (x == 'a')

  module M2 where
  import M -- brings the definition of TC into scope
  instance TC Char where c x = False

However, if you try to write a module N that imports both M1 and M2,
either directly or indirectly, then, by the above rule, both instances
will be in scope in the body of N and you'll get an error!

All the best,
Mark