Nested instances

With the introduction of DataKinds it became possible to define class instances that cover all type constructors of a kind:

class SomeClass (b :: Bool) where
  boolStr :: Proxy b -> String
instance SomeClass 'True where
  boolStr _ = "True"
instance SomeClass 'False where
  boolStr _ = "False"

It is clear that all types of kind 'Bool are instances of SomeClass. However the compiler doesn't know about this, and we always have to put a class restriction on a function that wants to use SomeClass, which is quite superfluous.

printBool :: (SomeClass b) => Proxy (b :: Bool) -> IO ()
printBool = putStrLn . boolStr

If we had an instance like this:

instance SomeClass (b :: 'Bool) where
  {...}

then the restriction would not be needed. So I think a consistent way of handling this would be to create "nested" instances:

instance SomeClass (b :: 'Bool) where
  instance SomeClass 'True where
    boolStr _ = "True"
  instance SomeClass 'False where
    boolStr _ = "False"

An instance body could therefore either be the list of function definitions, or a list of sub-instances. This would also ensure that all relevant instances are defined in the same module. The nesting could be of arbitrary depth which would allow the handling of more complicated cases:

instance SomeOtherClass (bs :: [Bool]) where
  instance SomeOtherClass '[] where
    {...}
  instance SomeOtherClass (b ': bs) where
    instance SomeOtherClass ('True ': bs) where
      {...}
    instance SomeOtherClass ('False ': bs) where
      {...}

The compiler's job would be to essentially check that all type "patterns" are matched.

Trac metadata

Trac field	Value
Version	7.4.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture