Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in / Register
Toggle navigation
Open sidebar
Dylan Yudaken
GHC
Commits
e88e083d
Commit
e88e083d
authored
Feb 05, 2019
by
Ryan Scott
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix #14579 by defining tyConAppNeedsKindSig, and using it
parent
ab493423
Changes
9
Hide whitespace changes
Inline
Sidebyside
Showing
9 changed files
with
422 additions
and
206 deletions
+422
206
compiler/hsSyn/HsUtils.hs
compiler/hsSyn/HsUtils.hs
+46
41
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcSplice.hs
+7
113
compiler/types/TyCoRep.hs
compiler/types/TyCoRep.hs
+289
16
testsuite/tests/deriving/should_compile/T14578.stderr
testsuite/tests/deriving/should_compile/T14578.stderr
+10
20
testsuite/tests/deriving/should_compile/T14579.stderr
testsuite/tests/deriving/should_compile/T14579.stderr
+39
0
testsuite/tests/deriving/should_compile/T14579b.hs
testsuite/tests/deriving/should_compile/T14579b.hs
+21
0
testsuite/tests/deriving/should_compile/all.T
testsuite/tests/deriving/should_compile/all.T
+2
1
testsuite/tests/deriving/should_fail/T15073.stderr
testsuite/tests/deriving/should_fail/T15073.stderr
+7
14
utils/haddock
utils/haddock
+1
1
No files found.
compiler/hsSyn/HsUtils.hs
View file @
e88e083d
...
...
@@ 57,7 +57,7 @@ module HsUtils(
 Types
mkHsAppTy
,
mkHsAppKindTy
,
userHsTyVarBndrs
,
userHsLTyVarBndrs
,
mkLHsSigType
,
mkLHsSigWcType
,
mkClassOpSigs
,
mkHsSigEnv
,
nlHsAppTy
,
nlHsTyVar
,
nlHsFunTy
,
nlHsParTy
,
nlHsTyConApp
,
nlHsAppTy
,
nlHsAppKindTy
,
nlHsTyVar
,
nlHsFunTy
,
nlHsParTy
,
nlHsTyConApp
,
 Stmts
mkTransformStmt
,
mkTransformByStmt
,
mkBodyStmt
,
mkBindStmt
,
mkTcBindStmt
,
...
...
@@ 105,14 +105,14 @@ import TcEvidence
import
RdrName
import
Var
import
TyCoRep
import
Type
(
filterOutInvisibleType
s
)
import
Type
(
tyConArgFlag
s
)
import
TysWiredIn
(
unitTy
)
import
TcType
import
DataCon
import
ConLike
import
Id
import
Name
import
NameSet
import
NameSet
hiding
(
unitFV
)
import
NameEnv
import
BasicTypes
import
SrcLoc
...
...
@@ 121,7 +121,6 @@ import Util
import
Bag
import
Outputable
import
Constants
import
TyCon
import
Data.Either
import
Data.Function
...
...
@@ 501,6 +500,10 @@ nlHsParTy t = noLoc (HsParTy noExt t)
nlHsTyConApp
::
IdP
(
GhcPass
p
)
>
[
LHsType
(
GhcPass
p
)]
>
LHsType
(
GhcPass
p
)
nlHsTyConApp
tycon
tys
=
foldl'
nlHsAppTy
(
nlHsTyVar
tycon
)
tys
nlHsAppKindTy
::
LHsType
(
GhcPass
p
)
>
LHsKind
(
GhcPass
p
)
>
LHsType
(
GhcPass
p
)
nlHsAppKindTy
f
k
=
noLoc
(
HsAppKindTy
noExt
f
(
parenthesizeHsType
appPrec
k
))
{
Tuples. All these functions are *pretypechecker* because they lack
types on the tuple.
...
...
@@ 660,14 +663,24 @@ typeToLHsType ty
go
(
LitTy
(
StrTyLit
s
))
=
noLoc
$
HsTyLit
NoExt
(
HsStrTy
NoSourceText
s
)
go
ty
@
(
TyConApp
tc
args
)

any
isInvisibleTyConBinder
(
tyConBinders
tc
)

tyConAppNeedsKindSig
True
tc
(
length
args
)
 We must produce an explicit kind signature here to make certain
 programs kindcheck. See Note [Kind signatures in typeToLHsType].
=
nlHsParTy
$
noLoc
$
HsKindSig
NoExt
lhs_ty
(
go
(
typeKind
ty
))

otherwise
=
lhs_ty
where
lhs_ty
=
nlHsTyConApp
(
getRdrName
tc
)
(
map
go
args'
)
args'
=
filterOutInvisibleTypes
tc
args
arg_flags
::
[
ArgFlag
]
arg_flags
=
tyConArgFlags
tc
args
lhs_ty
::
LHsType
GhcPs
lhs_ty
=
foldl'
(
\
f
(
arg
,
flag
)
>
let
arg'
=
go
arg
in
case
flag
of
Inferred
>
f
Specified
>
f
`
nlHsAppKindTy
`
arg'
Required
>
f
`
nlHsAppTy
`
arg'
)
(
nlHsTyVar
(
getRdrName
tc
))
(
zip
args
arg_flags
)
go
(
CastTy
ty
_
)
=
go
ty
go
(
CoercionTy
co
)
=
pprPanic
"toLHsSigWcType"
(
ppr
co
)
...
...
@@ 684,48 +697,40 @@ Note [Kind signatures in typeToLHsType]
There are types that typeToLHsType can produce which require explicit kind
signatures in order to kindcheck. Here is an example from Trac #14579:
newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a) deriving Eq
newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a)) deriving Eq
 type P :: forall {k} {t :: k}. Proxy t
type P = 'Proxy
 type Wat :: forall a. Proxy a > *
newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
deriving Eq
 type Wat2 :: forall {a}. Proxy a > *
type Wat2 = Wat
 type Glurp :: * > *
newtype Glurp a = MkGlurp (Wat2 (P :: Proxy a))
deriving Eq
The derived Eq instance for Glurp (without any kind signatures) would be:
instance Eq a => Eq (Glurp a) where
(==) = coerce @(Wat
'Proxy > Wat 'Proxy
> Bool)
@(Glurp a
> Glurp a
> Bool)
(==) = coerce @(Wat
2 P > Wat2 P
> Bool)
@(Glurp a > Glurp a > Bool)
(==) :: Glurp a > Glurp a > Bool
(Where the visible type applications use types produced by typeToLHsType.)
The type 'Proxy has an underspecified kind, so we must ensure that
typeToLHsType ascribes it with its kind: ('Proxy :: Proxy a).
We must be careful not to produce too many kind signatures, or else
typeToLHsType can produce noisy types like
('Proxy :: Proxy (a :: (Type :: Type))). In pursuit of this goal, we adopt the
following criterion for choosing when to annotate types with kinds:
* If there is a tycon application with any invisible arguments, annotate
the tycon application with its kind.
Why is this the right criterion? The problem we encountered earlier was the
result of an invisible argument (the `a` in ('Proxy :: Proxy a)) being
underspecified, so producing a kind signature for 'Proxy will catch this.
If there are no invisible arguments, then there is nothing to do, so we can
avoid polluting the result type with redundant noise.
What about a more complicated tycon, such as this?
T :: forall {j} (a :: j). a > Type
Unlike in the previous 'Proxy example, annotating an application of `T` to an
argument (e.g., annotating T ty to obtain (T ty :: Type)) will not fix
its invisible argument `j`. But because we apply this strategy recursively,
`j` will be fixed because the kind of `ty` will be fixed! That is to say,
something to the effect of (T (ty :: j) :: Type) will be produced.
This strategy certainly isn't foolproof, as tycons that contain type families
in their kind might break down. But we'd likely need visible kind application
to make those work.
The type P (in Wat2 P) has an underspecified kind, so we must ensure that
typeToLHsType ascribes it with its kind: Wat2 (P :: Proxy a). To accomplish
this, whenever we see an application of a tycon to some arguments, we use
the tyConAppNeedsKindSig function to determine if it requires an explicit kind
signature to resolve some ambiguity. (See Note
Note [When does a tycon application need an explicit kind signature?] for a
more detailed explanation of how this works.)
Note that we pass True to tyConAppNeedsKindSig since we are generated code with
visible kind applications, so even specified arguments count towards injective
positions in the kind of the tycon.
}
{ *********************************************************************
...
...
compiler/typecheck/TcSplice.hs
View file @
e88e083d
...
...
@@ 57,7 +57,6 @@ import GHCi
import
HscMain
 These imports are the reason that TcSplice
 is very high up the module hierarchy
import
FV
import
RnSplice
(
traceSplice
,
SpliceInfo
(
..
))
import
RdrName
import
HscTypes
...
...
@@ 1890,109 +1889,12 @@ reifyTyVarsToMaybe :: [TyVar] > TcM (Maybe [TH.TyVarBndr])
reifyTyVarsToMaybe
[]
=
pure
Nothing
reifyTyVarsToMaybe
tys
=
Just
<$>
reifyTyVars
tys
{
Note [Kind annotations on TyConApps]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A polykinded 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 we have a tycon application (T ty1 ... tyn). Assuming that T is not
oversatured (more on this later), we can assume T's declaration is of the form
T (tvb1 :: s1) ... (tvbn :: sn) :: p. If any kind variable that
is free in p is not free in an injective position in tvb1 ... tvbn,
then we put on a kind annotation, since we would not otherwise be able to infer
the kind of the whole tycon application.
The injective positions in a tyvar binder are the injective positions in the
kind of its tyvar, provided the tyvar binder is either:
* Anonymous. 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 inferred kinds of 'True and
'[] would contribute to the inferred kind of '(:) 'True '[].
* Has required visibility. For example, in the type family:
type family 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 inferred kind of Maybe a would
contribute to the inferred kind of Wurble (Maybe a) Nothing.
An injective position in a type is one that does not occur as an argument to
a noninjective type constructor (e.g., noninjective type families). See
injectiveVarsOfType.
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 kindunless, of course, the remainder of
the tycon application's kind has uninstantiated kind variables.
An earlier implementation of this algorithm only checked if p contained any
free variables. But this was unsatisfactory, since a datatype like this:
data Foo = Foo (Proxy '[False, True])
Would be reified like this:
data Foo = Foo (Proxy ('(:) False ('(:) True ('[] :: [Bool])
:: [Bool]) :: [Bool]))
Which has a rather excessive amount of kind annotations. With the current
algorithm, we instead reify Foo to this:
data Foo = Foo (Proxy ('(:) False ('(:) True ('[] :: [Bool]))))
Since in the case of '[], the kind p is [a], and there are no arguments in the
kind of '[]. On the other hand, in the case of '(:) True '[], the kind p is
(forall a. [a]), but a occurs free in the first and second arguments of the
full kind of '(:), which is (forall a. a > [a] > [a]). (See Trac #14060.)
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.
}
reify_tc_app
::
TyCon
>
[
Type
.
Type
]
>
TcM
TH
.
Type
reify_tc_app
tc
tys
=
do
{
tys'
<
reifyTypes
(
filterOutInvisibleTypes
tc
tys
)
;
maybe_sig_t
(
mkThAppTs
r_tc
tys'
)
}
where
arity
=
tyConArity
tc
tc_binders
=
tyConBinders
tc
tc_res_kind
=
tyConResKind
tc
r_tc

isUnboxedSumTyCon
tc
=
TH
.
UnboxedSumT
(
arity
`
div
`
2
)

isUnboxedTupleTyCon
tc
=
TH
.
UnboxedTupleT
(
arity
`
div
`
2
)
...
...
@@ 2013,28 +1915,20 @@ reify_tc_app tc tys

isPromotedDataCon
tc
=
TH
.
PromotedT
(
reifyName
tc
)

otherwise
=
TH
.
ConT
(
reifyName
tc
)
 See Note [Kind annotations on TyConApps]
 See Note [When does a tycon application need an explicit kind
 signature?] in TyCoRep
maybe_sig_t
th_type

needs_kind_sig

tyConAppNeedsKindSig
False
 We don't reify types using visible kind applications, so
 don't count specified binders as contributing towards
 injective positions in the kind of the tycon.
tc
(
length
tys
)
=
do
{
let
full_kind
=
tcTypeKind
(
mkTyConApp
tc
tys
)
;
th_full_kind
<
reifyKind
full_kind
;
return
(
TH
.
SigT
th_type
th_full_kind
)
}

otherwise
=
return
th_type
needs_kind_sig

GT
<
compareLength
tys
tc_binders
=
False

otherwise
=
let
(
dropped_binders
,
remaining_binders
)
=
splitAtList
tys
tc_binders
result_kind
=
mkTyConKind
remaining_binders
tc_res_kind
result_vars
=
tyCoVarsOfType
result_kind
dropped_vars
=
fvVarSet
$
mapUnionFV
injectiveVarsOfBinder
dropped_binders
in
not
(
subVarSet
result_vars
dropped_vars
)

reifyName
::
NamedThing
n
=>
n
>
TH
.
Name
reifyName
thing
...
...
compiler/types/TyCoRep.hs
View file @
e88e083d
...
...
@@ 90,7 +90,7 @@ module TyCoRep (
tyCoFVsOfCo
,
tyCoFVsOfCos
,
tyCoVarsOfCoList
,
tyCoVarsOfProv
,
almostDevoidCoVarOfCo
,
injectiveVarsOf
Binder
,
injectiveVarsOfType
,
injectiveVarsOf
Type
,
tyConAppNeedsKindSig
,
noFreeVarsOfType
,
noFreeVarsOfCo
,
...
...
@@ 2103,20 +2103,21 @@ almost_devoid_co_var_of_types (ty:tys) cv
 Injective free vars 
  Returns the free variables of a 'TyConBinder' that are in injective
 positions. (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an
 explanation of what an injective position is.)
injectiveVarsOfBinder
::
TyConBinder
>
FV
injectiveVarsOfBinder
(
Bndr
tv
vis
)
=
case
vis
of
AnonTCB
>
injectiveVarsOfType
(
varType
tv
)
NamedTCB
Required
>
unitFV
tv
`
unionFV
`
injectiveVarsOfType
(
varType
tv
)
NamedTCB
_
>
emptyFV
  Returns the free variables of a 'Type' that are in injective positions.
 (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an explanation
 of what an injective position is.)
 For example, if @F@ is a noninjective type family, then:

 @
 injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}
 @

 If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@.
 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.

 See @Note [When does a tycon application need an explicit kind signature?]@.
injectiveVarsOfType
::
Type
>
FV
injectiveVarsOfType
=
go
where
...
...
@@ 2132,12 +2133,284 @@ injectiveVarsOfType = go
filterByList
(
inj
++
repeat
True
)
tys
 Oversaturated arguments to a tycon are
 always injective, hence the repeat True
go
(
ForAllTy
tvb
ty
)
=
tyCoFVsBndr
tvb
$
go
(
binderType
tvb
)
`
unionFV
`
go
ty
go
(
ForAllTy
tvb
ty
)
=
tyCoFVsBndr
tvb
$
go
ty
go
LitTy
{}
=
emptyFV
go
(
CastTy
ty
_
)
=
go
ty
go
CoercionTy
{}
=
emptyFV
  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 sourcesyntax 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 .hsboot
 files.
tyConAppNeedsKindSig
::
Bool
 ^ Should specified binders count towards injective positions in
 the kind of the TyCon?
>
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
spec_inj_pos
)
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
::
Bool
 Should specified binders count towards injective positions?
 (If you're using visible kind applications, then you want True
 here.)
>
TyConBinder
>
FV
injective_vars_of_binder
spec_inj_pos
(
Bndr
tv
vis
)
=
case
vis
of
AnonTCB
>
injectiveVarsOfType
(
varType
tv
)
NamedTCB
argf

(
argf
==
Required
)

(
spec_inj_pos
&&
(
argf
==
Specified
))
>
unitFV
tv
`
unionFV
`
injectiveVarsOfType
(
varType
tv
)

otherwise
>
emptyFV
{
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 userwritten 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
fprintexplicitkinds, as we need to produce something which has the same
structure as a sourcesyntax 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 (noninferred) 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 nonomitted arguments
fill in the omitted arguments?
(This is still a bit handwavey, 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 noninjective 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 nonomitted 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 nonomitted 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 nonomitted 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 nonomitted 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 kindunless, 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.
}