Hi, here's my take on closed classes versus kinds. 1) Closed classes: Consider class Foo x instance Foo Int instance Foo Bool Assume we'd like to prevent that Foo has any other members besides Int and Bool. Haskell follows the open-world assumption. Hence, Foo t is assumed to be true for any type t unless otherwise stated. Oleg suggests to use functional dependency style improvement. Indeed, we'd like to state that "Foo x improves to False for any x different from Int and Bool". The question is how to enforce this condition? I don't think you can by just relying on functional dependencies. 1a) Closed classes in Chameleon: E.g., in Chameleon we can enumerate all cases which should yield False rule Foo Char ==> False rule Foo (a,b) ==> False rule Foo (a->b) ==> False ... But what happens if we define a new type such as data Erk = ...? Well, we'll need to add a new improvement rule rule Foo Erk ==> False 1b) Closed-world assumption: Alternatively, we might want to abandon the open-world assumption and switch to a Prolog-like closed world approach. See section 4.2 in [1] and section 8.1 in [2] for a discussion. Essentially, we impose that Foo x improves to x=Int or x=Bool We can close classes once and for all, however, we're in trouble in case instance declarations are recursive (e.g., Simon's example involves a recursive instance declaration!) Ref: [1] Object-Oriented Style Overloading for Haskell by Mark Shields and Simon Peyton Jones. [2] A Theory of Overloading by Peter J. Stuckey and Martin Sulzmann b) Kinds There's certainly a connection between closed classes and kinds. Assume we have a system that supports closed classes (either by following (1a) or (1b)). Then kind K = T1 | T2 class C (a::K) can be encoded by closed class K x instance K T1 instance K T2 -- T1 and T2 are the only members of K class K a => C a -- C t implies K t which yields failure if t differs from T1 or T2 Martin Oleg wrote:

Simon Peyton-Jones wrote:

...

kind HNat = HZero | HSucc HNat

class HNatC (a::HNat)

instance HNatC HZero instance HNatC n => HNatC (HSucc n)

There is no way to construct a value of type HZero, or (HSucc HZero); these are simply phantom types. ... A merit of declaring a kind is that the kind is closed -- the only types of kind HNat are HZero, HSucc HZero, and so on. So the class doesn't need to be closed; no one can add new instances to HNatC because they don't have any more types of kind HNat.

With the flag -fallow-overlapping-instances, could I still add an instance instance HNatC n => HNatC (HSucc (HSucc n)) or instance HNatC (HSucc HZero) ??

If I may I'd like to second the proposal for closed classes. In some sense, we already have them -- well, semi-closed. Functional dependencies is the way to close the world somewhat. If we have a class class Foo x y | x -> y instance Foo Int Bool we are positive there may not be any instance 'Foo Int <anything>' ever again, open world and -fallow-overlapping-instances notwithstanding. In fact, it is because we are so positive about that fact that we may conclude that "Foo Int x" implies x = Bool. At least in the case of functional dependencies, the way to close the world gives us type improvement rules. One might wonder if there are other ways to (semi-)close the world with similar nice properties.