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.