Move tyConAppNeedsKindSig to Type

Previously it was awkwardly in TyCoFVs (and before that in TyCoRep).
Type seems like a sensible place for it to live.

4 files changed, 270 insertions, 276 deletions

diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs
index c49ce8acf2..6fd42ae18d 100644
--- a/compiler/hsSyn/HsUtils.hs
+++ b/compiler/hsSyn/HsUtils.hs
@@ -106,8 +106,7 @@ import TcEvidence
 import RdrName
 import Var
 import TyCoRep
-import TyCoFVs ( tyConAppNeedsKindSig )
-import Type   ( appTyArgFlags, splitAppTys, tyConArgFlags )
+import Type   ( appTyArgFlags, splitAppTys, tyConArgFlags, tyConAppNeedsKindSig )
 import TysWiredIn ( unitTy )
 import TcType
 import DataCon
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 47eaed3916..242028f578 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -74,7 +74,6 @@ import TcMType
 import TcHsType
 import TcIface
 import TyCoRep
-import TyCoFVs ( tyConAppNeedsKindSig )
 import FamInst
 import FamInstEnv
 import InstEnv
diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs
index 09ef6c4618..52dd945104 100644
--- a/compiler/types/TyCoFVs.hs
+++ b/compiler/types/TyCoFVs.hs
@@ -12,7 +12,7 @@ module TyCoFVs
         tyCoFVsOfCo, tyCoFVsOfCos,
         tyCoVarsOfCoList, tyCoVarsOfProv,
         almostDevoidCoVarOfCo,
-        injectiveVarsOfType, tyConAppNeedsKindSig,
+        injectiveVarsOfType,
 
         noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
 
@@ -623,278 +623,6 @@ noFreeVarsOfProv (PhantomProv co)    = noFreeVarsOfCo co
 noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co
 noFreeVarsOfProv (PluginProv {})     = True
 
-
--- | Does a 'TyCon' (that is applied to some number of arguments) need to be
--- ascribed with an explicit kind signature to resolve ambiguity if rendered as
--- a source-syntax type?
--- (See @Note [When does a tycon application need an explicit kind signature?]@
--- for a full explanation of what this function checks for.)
-
--- Morally, this function ought to belong in TyCon.hs, not TyCoRep.hs, but
--- accomplishing this requires a fair deal of futzing aruond with .hs-boot
--- files.
-tyConAppNeedsKindSig
-  :: Bool  -- ^ Should specified binders count towards injective positions in
-           --   the kind of the TyCon? (If you're using visible kind
-           --   applications, then you want True here.
-  -> TyCon
-  -> Int   -- ^ The number of args the 'TyCon' is applied to.
-  -> Bool  -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the
-           --   number of arguments)
-tyConAppNeedsKindSig spec_inj_pos tc n_args
-  | LT <- listLengthCmp tc_binders n_args
-  = False
-  | otherwise
-  = let (dropped_binders, remaining_binders)
-          = splitAt n_args tc_binders
-        result_kind  = mkTyConKind remaining_binders tc_res_kind
-        result_vars  = tyCoVarsOfType result_kind
-        dropped_vars = fvVarSet $
-                       mapUnionFV injective_vars_of_binder dropped_binders
-
-    in not (subVarSet result_vars dropped_vars)
-  where
-    tc_binders  = tyConBinders tc
-    tc_res_kind = tyConResKind tc
-
-    -- Returns the variables that would be fixed by knowing a TyConBinder. See
-    -- Note [When does a tycon application need an explicit kind signature?]
-    -- for a more detailed explanation of what this function does.
-    injective_vars_of_binder :: TyConBinder -> FV
-    injective_vars_of_binder (Bndr tv vis) =
-      case vis of
-        AnonTCB VisArg -> injectiveVarsOfType (varType tv)
-        NamedTCB argf  | source_of_injectivity argf
-                       -> unitFV tv `unionFV` injectiveVarsOfType (varType tv)
-        _              -> emptyFV
-
-    source_of_injectivity Required  = True
-    source_of_injectivity Specified = spec_inj_pos
-    source_of_injectivity Inferred  = False
-
-{-
-Note [When does a tycon application need an explicit kind signature?]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There are a couple of places in GHC where we convert Core Types into forms that
-more closely resemble user-written syntax. These include:
-
-1. Template Haskell Type reification (see, for instance, TcSplice.reify_tc_app)
-2. Converting Types to LHsTypes (in HsUtils.typeToLHsType, or in Haddock)
-
-This conversion presents a challenge: how do we ensure that the resulting type
-has enough kind information so as not to be ambiguous? To better motivate this
-question, consider the following Core type:
-
-  -- Foo :: Type -> Type
-  type Foo = Proxy Type
-
-There is nothing ambiguous about the RHS of Foo in Core. But if we were to,
-say, reify it into a TH Type, then it's tempting to just drop the invisible
-Type argument and simply return `Proxy`. But now we've lost crucial kind
-information: we don't know if we're dealing with `Proxy Type` or `Proxy Bool`
-or `Proxy Int` or something else! We've inadvertently introduced ambiguity.
-
-Unlike in other situations in GHC, we can't just turn on
--fprint-explicit-kinds, as we need to produce something which has the same
-structure as a source-syntax type. Moreover, we can't rely on visible kind
-application, since the first kind argument to Proxy is inferred, not specified.
-Our solution is to annotate certain tycons with their kinds whenever they
-appear in applied form in order to resolve the ambiguity. For instance, we
-would reify the RHS of Foo like so:
-
-  type Foo = (Proxy :: Type -> Type)
-
-We need to devise an algorithm that determines precisely which tycons need
-these explicit kind signatures. We certainly don't want to annotate _every_
-tycon with a kind signature, or else we might end up with horribly bloated
-types like the following:
-
-  (Either :: Type -> Type -> Type) (Int :: Type) (Char :: Type)
-
-We only want to annotate tycons that absolutely require kind signatures in
-order to resolve some sort of ambiguity, and nothing more.
-
-Suppose we have a tycon application (T ty_1 ... ty_n). Why might this type
-require a kind signature? It might require it when we need to fill in any of
-T's omitted arguments. By "omitted argument", we mean one that is dropped when
-reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and
-specified arguments (e.g., TH reification in TcSplice), and sometimes the
-omitted arguments are only the inferred ones (e.g., in HsUtils.typeToLHsType,
-which reifies specified arguments through visible kind application).
-Regardless, the key idea is that _some_ arguments are going to be omitted after
-reification, and the only mechanism we have at our disposal for filling them in
-is through explicit kind signatures.
-
-What do we mean by "fill in"? Let's consider this small example:
-
-  T :: forall {k}. Type -> (k -> Type) -> k
-
-Moreover, we have this application of T:
-
-  T @{j} Int aty
-
-When we reify this type, we omit the inferred argument @{j}. Is it fixed by the
-other (non-inferred) arguments? Yes! If we know the kind of (aty :: blah), then
-we'll generate an equality constraint (kappa -> Type) and, assuming we can
-solve it, that will fix `kappa`. (Here, `kappa` is the unification variable
-that we instantiate `k` with.)
-
-Therefore, for any application of a tycon T to some arguments, the Question We
-Must Answer is:
-
-* Given the first n arguments of T, do the kinds of the non-omitted arguments
-  fill in the omitted arguments?
-
-(This is still a bit hand-wavey, but we'll refine this question incrementally
-as we explain more of the machinery underlying this process.)
-
-Answering this question is precisely the role that the `injectiveVarsOfType`
-and `injective_vars_of_binder` functions exist to serve. If an omitted argument
-`a` appears in the set returned by `injectiveVarsOfType ty`, then knowing
-`ty` determines (i.e., fills in) `a`. (More on `injective_vars_of_binder` in a
-bit.)
-
-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, is `F` is a non-injective type family, then
-
-  injectiveVarsOfType(Either c (Maybe (a, F b c))) = {a, c}
-
-Now that we know what this function does, here is a second attempt at the
-Question We Must Answer:
-
-* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
-  of T that are instantiated by non-omitted arguments. Do the injective
-  variables of these binders fill in the remainder of T's kind?
-
-Alright, we're getting closer. Next, we need to clarify what the injective
-variables of a tycon binder are. This the role that the
-`injective_vars_of_binder` function serves. Here is what this function does for
-each form of tycon binder:
-
-* Anonymous binders are injective positions. For example, in the promoted data
-  constructor '(:):
-
-    '(:) :: forall a. a -> [a] -> [a]
-
-  The second and third tyvar binders (of kinds `a` and `[a]`) are both
-  anonymous, so if we had '(:) 'True '[], then the kinds of 'True and
-  '[] would contribute to the kind of '(:) 'True '[]. Therefore,
-  injective_vars_of_binder(_ :: a) = injectiveVarsOfType(a) = {a}.
-  (Similarly, injective_vars_of_binder(_ :: [a]) = {a}.)
-* Named binders:
-  - Inferred binders are never injective positions. For example, in this data
-    type:
-
-      data Proxy a
-      Proxy :: forall {k}. k -> Type
-
-    If we had Proxy 'True, then the kind of 'True would not contribute to the
-    kind of Proxy 'True. Therefore,
-    injective_vars_of_binder(forall {k}. ...) = {}.
-  - Required binders are injective positions. For example, in this data type:
-
-      data Wurble k (a :: k) :: k
-      Wurble :: forall k -> k -> k
-
-  The first tyvar binder (of kind `forall k`) has required visibility, so if
-  we had Wurble (Maybe a) Nothing, then the kind of Maybe a would
-  contribute to the kind of Wurble (Maybe a) Nothing. Hence,
-  injective_vars_of_binder(forall a -> ...) = {a}.
-  - Specified binders /might/ be injective positions, depending on how you
-    approach things. Continuing the '(:) example:
-
-      '(:) :: forall a. a -> [a] -> [a]
-
-    Normally, the (forall a. ...) tyvar binder wouldn't contribute to the kind
-    of '(:) 'True '[], since it's not explicitly instantiated by the user. But
-    if visible kind application is enabled, then this is possible, since the
-    user can write '(:) @Bool 'True '[]. (In that case,
-    injective_vars_of_binder(forall a. ...) = {a}.)
-
-    There are some situations where using visible kind application is appropriate
-    (e.g., HsUtils.typeToLHsType) and others where it is not (e.g., TH
-    reification), so the `injective_vars_of_binder` function is parametrized by
-    a Bool which decides if specified binders should be counted towards
-    injective positions or not.
-
-Now that we've defined injective_vars_of_binder, we can refine the Question We
-Must Answer once more:
-
-* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
-  of T that are instantiated by non-omitted arguments. For each such binder
-  b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
-  superset of the free variables of the remainder of T's kind?
-
-If the answer to this question is "no", then (T ty_1 ... ty_n) needs an
-explicit kind signature, since T's kind has kind variables leftover that
-aren't fixed by the non-omitted arguments.
-
-One last sticking point: what does "the remainder of T's kind" mean? You might
-be tempted to think that it corresponds to all of the arguments in the kind of
-T that would normally be instantiated by omitted arguments. But this isn't
-quite right, strictly speaking. Consider the following (silly) example:
-
-  S :: forall {k}. Type -> Type
-
-And suppose we have this application of S:
-
-  S Int Bool
-
-The Int argument would be omitted, and
-injective_vars_of_binder(_ :: Type) = {}. This is not a superset of {k}, which
-might suggest that (S Bool) needs an explicit kind signature. But
-(S Bool :: Type) doesn't actually fix `k`! This is because the kind signature
-only affects the /result/ of the application, not all of the individual
-arguments. So adding a kind signature here won't make a difference. Therefore,
-the fourth (and final) iteration of the Question We Must Answer is:
-
-* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
-  of T that are instantiated by non-omitted arguments. For each such binder
-  b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
-  superset of the free variables of the kind of (T ty_1 ... ty_n)?
-
-Phew, that was a lot of work!
-
-How can be sure that this is correct? That is, how can we be sure that in the
-event that we leave off a kind annotation, that one could infer the kind of the
-tycon application from its arguments? It's essentially a proof by induction: if
-we can infer the kinds of every subtree of a type, then the whole tycon
-application will have an inferrable kind--unless, of course, the remainder of
-the tycon application's kind has uninstantiated kind variables.
-
-What happens if T is oversaturated? That is, if T's kind has fewer than n
-arguments, in the case that the concrete application instantiates a result
-kind variable with an arrow kind? If we run out of arguments, we do not attach
-a kind annotation. 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 choose not to annotate the application of G with
-a kind signature. After all, we needn't do this, since that instance would
-be reified as:
-
-   type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool
-
-So the kind of G isn't ambiguous anymore due to the explicit kind annotation
-on its argument. See #8953 and test th/T8953.
--}
-
-
 {-
 %************************************************************************
 %*                                                                      *
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 0400a31ae1..e65861a9ea 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -123,6 +123,7 @@ module Type (
         isCoVarType, isEvVarType,
 
         isValidJoinPointType,
+        tyConAppNeedsKindSig,
 
         -- (Lifting and boxity)
         isLiftedType_maybe, isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
@@ -3065,3 +3066,270 @@ Most pretty-printing is either in TyCoRep or IfaceType.
 pprWithTYPE :: Type -> SDoc
 pprWithTYPE ty = updSDocDynFlags (flip gopt_set Opt_PrintExplicitRuntimeReps) $
                  ppr ty
+
+
+-- | Does a 'TyCon' (that is applied to some number of arguments) need to be
+-- ascribed with an explicit kind signature to resolve ambiguity if rendered as
+-- a source-syntax type?
+-- (See @Note [When does a tycon application need an explicit kind signature?]@
+-- for a full explanation of what this function checks for.)
+tyConAppNeedsKindSig
+  :: Bool  -- ^ Should specified binders count towards injective positions in
+           --   the kind of the TyCon? (If you're using visible kind
+           --   applications, then you want True here.
+  -> TyCon
+  -> Int   -- ^ The number of args the 'TyCon' is applied to.
+  -> Bool  -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the
+           --   number of arguments)
+tyConAppNeedsKindSig spec_inj_pos tc n_args
+  | LT <- listLengthCmp tc_binders n_args
+  = False
+  | otherwise
+  = let (dropped_binders, remaining_binders)
+          = splitAt n_args tc_binders
+        result_kind  = mkTyConKind remaining_binders tc_res_kind
+        result_vars  = tyCoVarsOfType result_kind
+        dropped_vars = fvVarSet $
+                       mapUnionFV injective_vars_of_binder dropped_binders
+
+    in not (subVarSet result_vars dropped_vars)
+  where
+    tc_binders  = tyConBinders tc
+    tc_res_kind = tyConResKind tc
+
+    -- Returns the variables that would be fixed by knowing a TyConBinder. See
+    -- Note [When does a tycon application need an explicit kind signature?]
+    -- for a more detailed explanation of what this function does.
+    injective_vars_of_binder :: TyConBinder -> FV
+    injective_vars_of_binder (Bndr tv vis) =
+      case vis of
+        AnonTCB VisArg -> injectiveVarsOfType (varType tv)
+        NamedTCB argf  | source_of_injectivity argf
+                       -> unitFV tv `unionFV` injectiveVarsOfType (varType tv)
+        _              -> emptyFV
+
+    source_of_injectivity Required  = True
+    source_of_injectivity Specified = spec_inj_pos
+    source_of_injectivity Inferred  = False
+
+{-
+Note [When does a tycon application need an explicit kind signature?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are a couple of places in GHC where we convert Core Types into forms that
+more closely resemble user-written syntax. These include:
+
+1. Template Haskell Type reification (see, for instance, TcSplice.reify_tc_app)
+2. Converting Types to LHsTypes (in HsUtils.typeToLHsType, or in Haddock)
+
+This conversion presents a challenge: how do we ensure that the resulting type
+has enough kind information so as not to be ambiguous? To better motivate this
+question, consider the following Core type:
+
+  -- Foo :: Type -> Type
+  type Foo = Proxy Type
+
+There is nothing ambiguous about the RHS of Foo in Core. But if we were to,
+say, reify it into a TH Type, then it's tempting to just drop the invisible
+Type argument and simply return `Proxy`. But now we've lost crucial kind
+information: we don't know if we're dealing with `Proxy Type` or `Proxy Bool`
+or `Proxy Int` or something else! We've inadvertently introduced ambiguity.
+
+Unlike in other situations in GHC, we can't just turn on
+-fprint-explicit-kinds, as we need to produce something which has the same
+structure as a source-syntax type. Moreover, we can't rely on visible kind
+application, since the first kind argument to Proxy is inferred, not specified.
+Our solution is to annotate certain tycons with their kinds whenever they
+appear in applied form in order to resolve the ambiguity. For instance, we
+would reify the RHS of Foo like so:
+
+  type Foo = (Proxy :: Type -> Type)
+
+We need to devise an algorithm that determines precisely which tycons need
+these explicit kind signatures. We certainly don't want to annotate _every_
+tycon with a kind signature, or else we might end up with horribly bloated
+types like the following:
+
+  (Either :: Type -> Type -> Type) (Int :: Type) (Char :: Type)
+
+We only want to annotate tycons that absolutely require kind signatures in
+order to resolve some sort of ambiguity, and nothing more.
+
+Suppose we have a tycon application (T ty_1 ... ty_n). Why might this type
+require a kind signature? It might require it when we need to fill in any of
+T's omitted arguments. By "omitted argument", we mean one that is dropped when
+reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and
+specified arguments (e.g., TH reification in TcSplice), and sometimes the
+omitted arguments are only the inferred ones (e.g., in HsUtils.typeToLHsType,
+which reifies specified arguments through visible kind application).
+Regardless, the key idea is that _some_ arguments are going to be omitted after
+reification, and the only mechanism we have at our disposal for filling them in
+is through explicit kind signatures.
+
+What do we mean by "fill in"? Let's consider this small example:
+
+  T :: forall {k}. Type -> (k -> Type) -> k
+
+Moreover, we have this application of T:
+
+  T @{j} Int aty
+
+When we reify this type, we omit the inferred argument @{j}. Is it fixed by the
+other (non-inferred) arguments? Yes! If we know the kind of (aty :: blah), then
+we'll generate an equality constraint (kappa -> Type) and, assuming we can
+solve it, that will fix `kappa`. (Here, `kappa` is the unification variable
+that we instantiate `k` with.)
+
+Therefore, for any application of a tycon T to some arguments, the Question We
+Must Answer is:
+
+* Given the first n arguments of T, do the kinds of the non-omitted arguments
+  fill in the omitted arguments?
+
+(This is still a bit hand-wavey, but we'll refine this question incrementally
+as we explain more of the machinery underlying this process.)
+
+Answering this question is precisely the role that the `injectiveVarsOfType`
+and `injective_vars_of_binder` functions exist to serve. If an omitted argument
+`a` appears in the set returned by `injectiveVarsOfType ty`, then knowing
+`ty` determines (i.e., fills in) `a`. (More on `injective_vars_of_binder` in a
+bit.)
+
+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, is `F` is a non-injective type family, then
+
+  injectiveVarsOfType(Either c (Maybe (a, F b c))) = {a, c}
+
+Now that we know what this function does, here is a second attempt at the
+Question We Must Answer:
+
+* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
+  of T that are instantiated by non-omitted arguments. Do the injective
+  variables of these binders fill in the remainder of T's kind?
+
+Alright, we're getting closer. Next, we need to clarify what the injective
+variables of a tycon binder are. This the role that the
+`injective_vars_of_binder` function serves. Here is what this function does for
+each form of tycon binder:
+
+* Anonymous binders are injective positions. For example, in the promoted data
+  constructor '(:):
+
+    '(:) :: forall a. a -> [a] -> [a]
+
+  The second and third tyvar binders (of kinds `a` and `[a]`) are both
+  anonymous, so if we had '(:) 'True '[], then the kinds of 'True and
+  '[] would contribute to the kind of '(:) 'True '[]. Therefore,
+  injective_vars_of_binder(_ :: a) = injectiveVarsOfType(a) = {a}.
+  (Similarly, injective_vars_of_binder(_ :: [a]) = {a}.)
+* Named binders:
+  - Inferred binders are never injective positions. For example, in this data
+    type:
+
+      data Proxy a
+      Proxy :: forall {k}. k -> Type
+
+    If we had Proxy 'True, then the kind of 'True would not contribute to the
+    kind of Proxy 'True. Therefore,
+    injective_vars_of_binder(forall {k}. ...) = {}.
+  - Required binders are injective positions. For example, in this data type:
+
+      data Wurble k (a :: k) :: k
+      Wurble :: forall k -> k -> k
+
+  The first tyvar binder (of kind `forall k`) has required visibility, so if
+  we had Wurble (Maybe a) Nothing, then the kind of Maybe a would
+  contribute to the kind of Wurble (Maybe a) Nothing. Hence,
+  injective_vars_of_binder(forall a -> ...) = {a}.
+  - Specified binders /might/ be injective positions, depending on how you
+    approach things. Continuing the '(:) example:
+
+      '(:) :: forall a. a -> [a] -> [a]
+
+    Normally, the (forall a. ...) tyvar binder wouldn't contribute to the kind
+    of '(:) 'True '[], since it's not explicitly instantiated by the user. But
+    if visible kind application is enabled, then this is possible, since the
+    user can write '(:) @Bool 'True '[]. (In that case,
+    injective_vars_of_binder(forall a. ...) = {a}.)
+
+    There are some situations where using visible kind application is appropriate
+    (e.g., HsUtils.typeToLHsType) and others where it is not (e.g., TH
+    reification), so the `injective_vars_of_binder` function is parametrized by
+    a Bool which decides if specified binders should be counted towards
+    injective positions or not.
+
+Now that we've defined injective_vars_of_binder, we can refine the Question We
+Must Answer once more:
+
+* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
+  of T that are instantiated by non-omitted arguments. For each such binder
+  b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
+  superset of the free variables of the remainder of T's kind?
+
+If the answer to this question is "no", then (T ty_1 ... ty_n) needs an
+explicit kind signature, since T's kind has kind variables leftover that
+aren't fixed by the non-omitted arguments.
+
+One last sticking point: what does "the remainder of T's kind" mean? You might
+be tempted to think that it corresponds to all of the arguments in the kind of
+T that would normally be instantiated by omitted arguments. But this isn't
+quite right, strictly speaking. Consider the following (silly) example:
+
+  S :: forall {k}. Type -> Type
+
+And suppose we have this application of S:
+
+  S Int Bool
+
+The Int argument would be omitted, and
+injective_vars_of_binder(_ :: Type) = {}. This is not a superset of {k}, which
+might suggest that (S Bool) needs an explicit kind signature. But
+(S Bool :: Type) doesn't actually fix `k`! This is because the kind signature
+only affects the /result/ of the application, not all of the individual
+arguments. So adding a kind signature here won't make a difference. Therefore,
+the fourth (and final) iteration of the Question We Must Answer is:
+
+* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
+  of T that are instantiated by non-omitted arguments. For each such binder
+  b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
+  superset of the free variables of the kind of (T ty_1 ... ty_n)?
+
+Phew, that was a lot of work!
+
+How can be sure that this is correct? That is, how can we be sure that in the
+event that we leave off a kind annotation, that one could infer the kind of the
+tycon application from its arguments? It's essentially a proof by induction: if
+we can infer the kinds of every subtree of a type, then the whole tycon
+application will have an inferrable kind--unless, of course, the remainder of
+the tycon application's kind has uninstantiated kind variables.
+
+What happens if T is oversaturated? That is, if T's kind has fewer than n
+arguments, in the case that the concrete application instantiates a result
+kind variable with an arrow kind? If we run out of arguments, we do not attach
+a kind annotation. 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 choose not to annotate the application of G with
+a kind signature. After all, we needn't do this, since that instance would
+be reified as:
+
+   type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool
+
+So the kind of G isn't ambiguous anymore due to the explicit kind annotation
+on its argument. See #8953 and test th/T8953.
+-}