[GHC] #8953: Reification drops necessary kind annotations (was: Reifying poly-kinded type families misses kind annotations)

[GHC]

#8953: Reification drops necessary kind annotations
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |            Owner:  goldfire
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Template    |          Version:  7.9
  Haskell                            |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:              |  Related Tickets:
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Still getting worse!

 Now, look at this:

 {{{
 a :: Proxy (Proxy :: * -> *)
 a = undefined

 b :: Proxy (Proxy :: (* -> *) -> *)
 b = undefined

 $( do info_a <- reify 'a
       info_b <- reify 'b
       runIO $ mapM putStrLn $ map pprint [info_a, info_b]
       return [] )
 }}}

 produces

 {{{
 Main.a :: Data.Proxy.Proxy Data.Proxy.Proxy
 Main.b :: Data.Proxy.Proxy Data.Proxy.Proxy
 }}}

 Yet, the types of `a` and `b` are ''not'' the same, and assigning one to
 the other rightly results in a type error.

 Furthermore, we really need to give the kind of ''every'' type variable
 binder. Consider

 {{{
 type StarProxy (a :: *) = Proxy a
 }}}

 Reifying tyvar binders omits any kinds that are `*`, yet the kind
 annotation here is very relevant (if `-XPolyKinds` is on).

 Oh, and the original problem (not reifying kind annotation on type
 variable patterns) can affect ''class'' instances, too, not just ''type''
 instances.

 So, new plan:
 1. Never reify a tyvar binder into a `PlainTV`. Always use `KindedTV`.

 2. Include a kind annotation (`SigT`) wrapping every use of a poly-kinded
 tycon. This wrapping will wrap around any arguments the tycon is applied
 to.

 3. If a class or family tyvar is polykinded, include a kind annotation on
 any pattern used to specialize this tyvar in instance declarations.

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