Lambda the Ultimate

From one of the examples:

module M2 where

  import X

  instance C Int Bool

  g :: T Int -> Bool

  g (MkT x) = x

I don't know Haskell too well but my 2 pennies: If you just follow the values, I think this is where any value may be converted to a boolean. It hints at that the definition of T should have been written/interpreted with probably an existential somewhere since type information is lost.

(x should have been typed with a skolem constant and not unify with Bool, therefor the problem is not with functional dependencies but with the definition of type T.)

I am not sure but isn't Haskell's type checking with `type families' an instance of a closed world assumption (proving with a database of facts), where the world just later turns out to be a bit more open than assumed?

If that is so, I don't think there's a lot wrong with the types being written, or unsoundness. It's just a matter of whether you want to use that closed world assumption or not, and the benefits/costs of that approach.

I am little bit puzzled what you mean by unsoundness here (but then again, I am really no expert on Haskell).

A problem where overlapping instances can lead to logical unsoundness in HOL is described here:

Checking Conservativity of Overloaded Definitions in Higher-Order Logic

I am not sure if there is a connection to your problem.

Haskell's module system provides a form of namespace support, but that support is not so well designed - c.f. http://hackage.haskell.org/trac/haskell-prime/wiki/FirstClassLabels

It also runs into problems which parallel ones commonly found in the implementation of multiple inheritance - i.e. what happens when different modules import from a common third module?

See also the discussion here - http://www.mail-archive.com/haskell@haskell.org/msg21158.html -

All of the above makes me want to ask why it is that you see "overlapping instance" as a feature to be copied rather than a hackish workaround for this problematic name space support in Haskell? Seems like it would be better to start with a different namespace model - e.g. like C++'s notion of namespace - and then improve on that.

I haven't scruitinized GHC enough to verify this, but I expect GHC is unsoundly mixing environments derived from conflicting instance declarations in different modules.

For soundness, each function needs to either be:

1. Typechecked and executed fully under the current module's instance declarations, not accepting any of the runtime typeclass environments implied by "MyClass t => .." constraints on the function. Here, any use of "C Int t" must unify t with Bool.

2. Typechecked solely on the basis of the current module's class definitions (ignoring its instance declarations), and relying on the caller's runtime typeclass environments. Here, any use of "C Int t" can't derive t from local instance declarations, since these may differ from other modules' instances.

I think Haskell mixes type inference from instances the current module with environments from the caller's module derived from a potentially different and conflicting set of instances.

At any rate, Haskell's underlying typeclass approach is so implicit that it complicates understanding which instance's bindings (local or caller's) are applicable in a given scenario, and fundeps then draw their types into question.

It's always useful to rethink a given program's typeclass semantics by rewriting it in Cayenne using dependent types, with classes represented as record types and instances are record values, and all environments passed around explicitly.

It should be stressed that GHC does NOT admit the problematic examples
in the Simon Peyton-Jones message. That is, they do not type check,
and no segmentation or other run-time faults arise. Even the example
Bad at the end of the message does not type check in GHC
6.10. Actually, even the module M does not type check.

For example, in the following program

class C a b | a -> b
instance C Int Bool
data T a = forall b. C a b => T b
foo :: T Int
foo = T True

bar :: T Int -> T Int
bar (T x) = T (not x)

although the definition foo is accepted, the definition bar is rejected.
Although the type checker could deduce from function dependencies that
x must be a boolean value, the type checker still refuses to type
check the program because T is existential, and quantification imposes
the abstraction barrier.

Simon Peyton-Jones message was discussing a general situation; it
seems that in general one has to check for conflicts between instances
eagerly. I personally think that GHC does the right thing when it
refuses to improve `rigid type variables' -- however irritating that
turns out to be.