[GHC] #9568: Type classes that fully cover closed kinds

[GHC]

#9568: Type classes that fully cover closed kinds
-------------------------------------+-------------------------------------
       Reporter:  dmcclean           |                   Owner:
           Type:  feature request    |                  Status:  new
       Priority:  lowest             |               Milestone:  ⊥
      Component:  Compiler (Type     |                 Version:  7.8.3
  checker)                           |        Operating System:
       Keywords:                     |  Unknown/Multiple
   Architecture:  Unknown/Multiple   |         Type of failure:
     Difficulty:  Unknown            |  None/Unknown
     Blocked By:                     |               Test Case:
Related Tickets:                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 When we have a closed kind (I think data kinds may be the only ones that
 are closed?), and a type class that takes only that kind as a parameter,
 and we have instances of the typeclass for every type in the kind, it
 would be nice if we didn't have to list it in the context of every
 function that uses it.

 Example:

 in `GHC.TypeLits`, this relationship exists between `Nat` and `KnownNat`,
 `Symbol` and `KnownSymbol`.

 It also arises in many of my uses of data kinds, because I often end up
 with a `KnownX` class that provides term-level things related to whatever
 the type is.

 The constraints tend to end up everywhere, which is noisy. As far as I can
 tell they don't really carry any information: a `KnownNat n` constraint
 where `n :: Nat` should be able to be discharged in the same way that
 something like `Show Bool` is, because regardless of which `n` we pick we
 know there will be an instance.

 (This is trickier for closed kinds like `Nat` and `Symbol` than for user-
 defined ones through the data kinds feature, because the former are
 inhabited by infinitely many types.)

 Perhaps we could have a pragma to inform the compiler that this situation
 exists for a certain typeclass, which the compiler could check in finite
 cases (like the ones arising for user-defined data kinds) by enumerating
 all the cases.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9568>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler