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

[GHC]

#9568: Type classes that fully cover closed kinds
-------------------------------------+-------------------------------------
              Reporter:  dmcclean    |            Owner:
                  Type:  feature     |           Status:  new
  request                            |        Milestone:  ⊥
              Priority:  lowest      |          Version:  7.8.3
             Component:  Compiler    |         Keywords:
  (Type checker)                     |     Architecture:  Unknown/Multiple
            Resolution:              |       Difficulty:  Unknown
      Operating System:              |       Blocked By:
  Unknown/Multiple                   |  Related Tickets:
       Type of failure:              |
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by rwbarton):

 This is a natural thing to want but, alas, it's not so simple. It's not
 enough for the compiler to know that some instance exists. It has to know
 which instance to use, because the choice of instance affects the runtime
 semantics of the program.

 From a theory point of view, polymorphism over closed kinds has the same
 parametricity properties as polymorphism over open kinds like `*`. If I
 have a function `f :: forall (b :: Bool). Proxy b -> String` then `f`'s
 behavior cannot depend on the choice of `b`, so `f (Proxy :: Proxy False)`
 must be equal to `f (Proxy :: Proxy True)`, just like a function `g ::
 Maybe a -> String` must satisfy `g (Nothing :: Maybe Int)` = `g (Nothing
 :: Maybe Bool)`.

 From an implementation point of view there is no difference at all at
 runtime between `Proxy :: Proxy False` and `Proxy :: Proxy True`, so
 simply for that reason it's impossible for any function to distinguish
 them.

 But with a class constraint `C b`, even when `C` has instances for both
 `False` and `True`, `f`'s behavior can depend on `b`, as I'm sure you
 know. This is possible because the `C b` constraint gets translated to an
 extra value-level argument to the function. So, `f :: forall (b :: Bool).
 C b => Proxy b -> String` is really different from `f :: forall (b ::
 Bool). Proxy b -> String` even when `C b` is satisfied for each individual
 type `b :: Bool`.

 In light of all this, I'm not sure what change along the lines of your
 suggestion would be possible. IIRC Richard Eisenberg's "dependent Haskell"
 project includes a non-parametric universal quantifier; perhaps that is
 related.

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