[GHC] #9858: Typeable instances should be kind-aware

[GHC]

#9858: Typeable instances should be kind-aware
-------------------------------------+-------------------------------------
        Reporter:  dreixel           |                   Owner:
            Type:  bug               |                  Status:  merge
        Priority:  highest           |               Milestone:  7.10.2
       Component:  Compiler          |                 Version:  7.9
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |  typecheck/should_fail/T9858a,
                                     |  should_run/T9858b
                                     |                Blocking:
                                     |  Differential Revisions:  Phab:D652
-------------------------------------+-------------------------------------

Comment (by ekmett):

 Rather than just say it is sad, let's see if we can tackle this issue head
 on.

 A while back, Simon, you posed a sketch of an idea of how to remove the
 superkinding / existing type hacks by adding another very simple level we
 can quantify over.

 It could be adapted to address this situation.

 Consider a type checker where we've removed `*`, `Constraint` and `#` and
 made a single unified kind `Sort a b` where `a` and `b` are allowed to
 range over a binary alphabet, lets consider `{T,F}` as that alphabet. [*]

 Then

 {{{
 * = Sort T T
 Constraint = Sort T F
 # = Sort F T
 }}}

 and we can talk about the kinds of existing types:

 {{{
 () :: forall a. Sort T a
 }}}

 lets `()` work as both a `Constraint` or `*`.

 {{{
 (,) :: forall a. Sort T a -> Sort T a -> Sort T a
 }}}

 lets us tuple up anything as long as both are *'s or both are Constraints.

 Unboxed tuples fit:

 {{{
 (#,#) :: forall a b. Sort a T -> Sort a T -> Sort F T
 }}}

 lets unboxed tuples carry `*`'s and `#`'s.

 and the existing function overloads fit:

 {{{
 (->) :: forall a b. Sort a T -> Sort b T -> Sort T T
 }}}

 All of this then works without the typechecker ever internally lying to
 itself which then solves this issue in a principled way, as the Typeable
 instance can know the full choice of kind without subversion.

 This removes all of the hacks where `(->) :: * -> * -> *`   but `a -> b`
 might have `a` and `b` have kinds other than `*`, etc. in the typechecker,
 and lets us talk about `(->) Int#`, or `(,) (Eq Int)` which are both types
 we currently can't write:

 {{{
 ghci> :k (->) Int#

 <interactive>:1:6:
     Expecting a lifted type, but ‘Int#’ is unlifted
     In a type in a GHCi command: (->) Int#
 }}}

 I already have to work around the lack of the latter by constructing my
 own product for constraints.

 {{{
 class (p,q) => p & q
 instance (p,q) => p & q
 }}}

 Now I can talk about `(&) (Eq Int) :: Constraint -> Constraint`, but there
 is no corresponding partial application trick for `(->)`.

 We've already implemented a related trick in Ermine without appreciable
 impact, our kinds there are a little different, so the details vary a bit.

 [*] To prevent weird quantifier abuse, you may want to require each of the
 arguments of Sort to have different ranges, otherwise `Sort a a` becomes
 weird.

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