[GHC] #8917: :kind! does not work under type constructors

[GHC]

#8917: :kind! does not work under type constructors
------------------------------------+-------------------------------------
       Reporter:  goldfire          |             Owner:  goldfire
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:  7.8.1
      Component:  Compiler          |           Version:  7.8.1-rc2
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 Say I have the following:

 {{{
 {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}

 module Scratch where

 data Nat = Zero | Succ Nat
 type family a + b where
   Zero + a = a
   (Succ n) + m = Succ (n + m)
 }}}

 I load this into ghci. See what happens next:

 {{{
 GHCi, version 7.8.0.20140228: http://www.haskell.org/ghc/  :? for help
 Loading package ghc-prim ... linking ... done.
 Loading package integer-gmp ... linking ... done.
 Loading package base ... linking ... done.
 [1 of 1] Compiling Scratch          ( Scratch.hs, interpreted )
 Ok, modules loaded: Scratch.
 *Scratch> :kind! Zero + Succ Zero
 Zero + Succ Zero :: Nat
 = 'Succ 'Zero
 *Scratch> :kind! Succ (Zero + Zero)
 Succ (Zero + Zero) :: Nat
 = 'Succ ('Zero + 'Zero)
 }}}

 Note the last line. It doesn't reduce under the `Succ`!

 I will fix shortly.

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