#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