Opened 5 years ago

Closed 5 years ago

#6150 closed feature request (invalid)

Nested instances

Reported by: exFalso Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.4.1
Keywords: DataKinds, typeclass, nested Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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.

Change History (1)

comment:1 Changed 5 years ago by simonpj

difficulty: Unknown
Resolution: invalid
Status: newclosed

Lots of reasons not to do this:

  • You propose to give printBool this type
    printBool :: Proxy (b :: Bool) -> IO ()
    but it really is not as polymorphic as that, and the "free theorems" won't hold. The class restriction tells you that the polymorphism is not parametric.
  • GHC uses "evidence passing" to implement type classes. That means that even in your example, printBool must take a hidden value parameter, which is the dictionary of methods for SomeClass. So if you suppressed it from the visible type, it would still have to be present in the real type.
  • In your example the instances occur right with the class declaration. But what if they don't. Then in some places you'd see it as exhaustive and in some not.

Sorry, but I don't think this is a runner.

Note: See TracTickets for help on using tickets.