[GHC] #14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code

[GHC]

#14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14579{a}
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D4264,
                                     |  Phab:D5229,
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/261
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I've read the patch, but I'm commenting here because Trac
 has greater longevity than code reviews.

 You have written a commendably detailed Note -- thank you.
 Still, it took me a solid hour of head-scratching to really
 understand it.  Here are some thoughts that may (or may not)
 help to make it clearer.

 First, it took me ages reslise that `tyConAppNeedsKindSig` can
 be done without knowing the actual arguments to `T`.  Only once
 I'd realised that did I discover that, sure enough, it doesn't rely
 on `args`, only on `length args`!  So I ''strongly'' suggest
 {{{
 tyConAppNeedsKindSig
   :: Bool -- ^ Should specified binders count towards injective positions
 in
           --   the kind of the TyCon?
   -> TyCon
   -> Int    -- Number of args
   -> Bool   -- Does (T t1 .. tn) need a signature
 tyConAppNeedsKindSig spec_inj_pos tc n_args = ...
 }}}
 That is, pass the ''number'' of args, not the actual args.

 That makes it clear that the function could, in principle, live in
 `TyCon`.  It could even be cached in the TyCon, as a list of `Bools` or,
 because
 of the Inferred/Specified thing, two lists of `Bools`.  But the caching
 is probably not worth it.

 Ok then, my thought process went like this.  Given a application
 `T t1 .. tn`, does it need a kind signature? Why might it need a kind
 signature?  So that we can fill in any of T's omitted arguments.  By
 an "omitted argument" I mean one that we do not reify expicitly in the
 `HsType`.  Sometimes the omitted ones are Inferred ones (in
 `typeToHsType`); sometimes both Inferred and Specified (in
 `TcSplice`); but the key thing is that they don't appear in the
 `HsType`.

 What do we mean by "fill in"? Suppose
 {{{
 T :: forall {k}. Type -> (k->*) -> k
 }}}
 and we have the application `T {j} Int aty`. When we convert to
 `HsType` we are going to omit the inferred arg `{j}`.  Is it fixed
 by the other non-inferred args?  Yes: if we know the kind of `aty ::
 blah`,
 we'll generate an equality constraint `(kappa->*) ~ blah` and, assuming
 we can solve it, that will fix `kappa`.  (Here `kappa` is the unification
 variable that we instantiate `k` with.)

 So the question becomes this.

 * Consider the first `n` args of T: do the kinds of the non-omitted
   arguments determine the omitted arguments?

 We'll only handle the case were the omitted arguments are `NamedTCB`,
 so we need to determine a variable.
 When does a kind "determine" a variable?  This is what
 `injectiveVarsOfType` computes.
 {{{
 -- (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an
 explanation
 -- of what an injective position is.)
 injectiveVarsOfType :: Type -> FV
 }}}
 Rather than speak of "injective positions" I think of it like this:
 if `a` is in `injectiveVarsOfType ty` then knowing `ty` fixes, or
 determines, `a`.
 More formally:
 {{{
   If a is in (injectiveVarsOfType ty)
   and S1(ty) ~ S2(ty)
   then S1(a) ~ S2(a)
   where S1 and S2 are arbitrary substitutions
 }}}
 For example, if `F` is a non-injective type family, then
 {{{
   injectiveTyVarsOf( Either c (Maybe (a, F b c)) )  =  {a,c}
 }}}
 (This part about `injectiveVarsOfType` is not new -- but I'd suggest
 adding it as comments to the function.)

 So we can refine the question:

 * Consider the first `n` args of T, and each omitted argument `i <= n`:
   is argument `i` a `NamedTCB` binder `b`, and does `b` appear in
 `injectiveVarsOfTtype (k(i+1) .. k(n))`?
   Where `kj` is the kind of the j'th argument of T.

 Much of this is as you have it, except that I'm not lookin at
 `result_kind` (in your `tyConAppNeedsKindSig`.
 If I can't fill in all omitted arguments, I'll add a kind signature.  So
 for a silly thing like
 {{{
   T :: forall k. Type -> Type
 }}}
 and the type `(T {j} Int)`, I'll add a kind signature, which actually does
 no good since `k` is unused.
 But it's a silly example.  And you'll add one for a different silly
 example.
 {{{
   T :: forall k. Type -> F k
 }}}
 which equally does no good.

 Nothing here is radically different from what you have.  But I
 find the chain of thought here easier to follow.

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