[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 goldfire):

 I'm not sure what "if the tycon is applied to any required arguments, then
 apply their kinds to the tycon's kind before doing further analysis"
 means. I suppose it could mean that you try to solve for the kind
 variables by doing unification and seeing if unification fixes the kind
 variables. Then apply the unifying substitution to the remainder of the
 kind. But that's quite a bit of work!

 Define "remainder of the tycon's kind" to mean the portion of the kind
 left over after all components of the kind corresponding to provided type
 arguments are removed. Do no instantiation of kind variables here.

 The current rule is:

 A. Include a kind annotation when the remainder of the tycon's kind
 mentions a kind variable.

 What if we change it to:

 B. Include a kind annotation when the remainder of the tycon's kind
 mentions a kind variable ''and'' that kind variable is not mentioned in
 any arguments that have been dropped (when finding the remainder). (But
 don't count occurrences in the arguments to non-injective type families.)

 Why is this new rule good? Because we're assuming that any reified type
 will have a fixed, known kind. When reifying a type application, we reify
 all its type arguments as well. Thus, all the type arguments will have a
 fixed, known kind. And thus any kind variables in the tycon's kind
 mentioned in that argument's expected kind will also be fixed. The
 exception here is for type families, which aren't injective. Happily, this
 keeps the annotation on `'[]` but drops it on `'(:)`.

 I will restate (B) to be a bit more implementable:

 * We have a tyconapp `T ty1 ... tyn`. The tycon `T` has kind `ki0`.

 * If `T` is oversaturated, no annotation is necessary. Otherwise, we can
 assume `ki0` has the form `forall k1 ... km. s1 -> ... -> sn -> p`.

 * Let `K` be the set of kind variables (that is, a subset of `{k1, ...,
 km}`) that occur in "injective positions" in `s1 ... sn`. An injective
 position in a type `ty` is either `ty` itself, an injective position
 within an injective argument to a tycon, an injective position in a
 function, or an injective position in the argument to a type variable.

 * Include an annotation only when `p` (the remainder of the tycon's kind)
 contains a kind variable ''not'' in the set `K`.

 What do we think? Might this work? I do think this is considerably easier
 than invoking unification.

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