#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... 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