[GHC] #14060: TH-reified types can suffer from kind signature oversaturation

[GHC]

#14060: TH-reified types can suffer from kind signature oversaturation
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Template Haskell  |              Version:  8.2.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 [http://git.haskell.org/ghc.git/blob/7089dc2f12f9616771fc1de143e9b974157405d8:/compiler/typecheck/TcSplice.hs#l1772
 Here] is why Template Haskell is choosing to attach a kind signature to
 every occurrence of `'[]` and `'(:)`:

 {{{#!hs
 {-
 Note [Kind annotations on TyConApps]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A poly-kinded tycon sometimes needs a kind annotation to be unambiguous.
 For example:

    type family F a :: k
    type instance F Int  = (Proxy :: * -> *)
    type instance F Bool = (Proxy :: (* -> *) -> *)

 It's hard to figure out where these annotations should appear, so we do
 this:
 Suppose the tycon is applied to n arguments. We strip off the first n
 arguments of the tycon's kind. If there are any variables left in the
 result
 kind, we put on a kind annotation. But we must be slightly careful: it's
 possible that the tycon's kind will have fewer than n arguments, in the
 case
 that the concrete application instantiates a result kind variable with an
 arrow kind. So, if we run out of arguments, we conservatively put on a
 kind
 annotation anyway. This should be a rare case, indeed. Here is an example:

    data T1 :: k1 -> k2 -> *
    data T2 :: k1 -> k2 -> *

    type family G (a :: k) :: k
    type instance G T1 = T2

    type instance F Char = (G T1 Bool :: (* -> *) -> *)   -- F from above

 Here G's kind is (forall k. k -> k), and the desugared RHS of that last
 instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According
 to
 the algorithm above, there are 3 arguments to G so we should peel off 3
 arguments in G's kind. But G's kind has only two arguments. This is the
 rare special case, and we conservatively choose to put the annotation
 in.

 See #8953 and test th/T8953.
 -}
 }}}

 To summarize, `'[]` gets a kind annotation because its kind is `[k]`,
 which has a kind variable. Fair enough. But what about `'(:) 'False ('[]
 :: [Bool])`? The kind of `'(:)` is `forall k. k -> [k] -> [k]`. It is
 applied to two arguments, so we drop the first two arguments to `'(:)`'s
 kind, leaving us with `[k]`. That has a kind variable, so TH chooses to
 attach a kind signature to it.

 But this doesn't feel right, does it? After all, `'(:)`'s first arguments
 have monomorphic kinds, which makes the kind of `'(:) 'False ('[] ::
 [Bool])` (`[Bool]`) monomorphic as well. Therefore, I propose this
 additional stipulation: if the tycon is applied to any required arguments,
 then apply their kinds to the tycon's kind before doing further analysis.

 That way, in the `'(:) 'False ('[] :: [Bool])` example, we'd start with
 `'(:)`'s kind being `Bool -> [Bool] -> [Bool]`, drop the first two
 arguments and be left with `[Bool]`, which is monomorphic (and thus does
 not warrant a kind annotation). On the other hand, `[]`'s argument `Bool`
 is not required, so we end up with a kind of `[k]`, which warrants a kind
 annotation as expected.

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