Kind inference for invisible binders in type declarations
GHC Proposal #425 "Invisible binders in type declarations" states that we allow @k
-binders without standalone kind signatures:
Kind Inference
When a declaration has no standalone kind signature, a
@k
-binder gives rise to aforall k.
quantifier in the inferred kind signature. The inferredforall k.
does not float to the left; the order of quantifiers continues to match the order of binders in the header.
At the moment, however, we reject @k
-binders in declarations without a signature:
-- No signature:
type F @a (b :: a) = '(a, b)
Error message:
Test.hs:8:1: error: [GHC-92337]
• Invalid invisible type variable binder: @a
Either a standalone kind signature (SAKS)
or a complete user-supplied kind (CUSK, legacy feature)
is required to use invisible binders.
• In the type synonym declaration for ‘F’
Suggested fix: Add a standalone kind signature for ‘F’
Instead, GHC should have inferred type F :: forall k. k -> (Type, k)
.
The reason for this is an implementation difficulty described in Note [No inference for invisible binders in type decls]
, cited here for completeness:
Note [No inference for invisible binders in type decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have (#22560):
data T @k (a::k) = MkT (...(T ty)...)
What monokind can we give to T after step 1 of the kind inference
algorithm described in Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]?
Remember: Step 1 generates a MonoTcTyCon.
It can't be
T :: kappa1 -> kappa2 -> Type
because the invocation `(T ty)` doesn't have a visible argument for `kappa`.
Nor can it be
T :: forall k. kappa2 -> Type
because that breaks the Monomorphic Recursion Principle: MonoTcTyCons have
monomorphic kinds; see Note [No polymorphic recursion in type decls]. It could be
T :: kappa1 ->. kappa2 -> type
where `->.` is a new kind of arrow in kinds, which (like a type-class argument
in terms) is invisibly instantiated. Or we could fake it with
T :: forall _. kappa2 -> Type
where `_` is a completely fresh variable, but that seems very smelly and makes it
harder to talk about the Monomorphic Recursion Principle. Moreover we'd need
some extra fancy types in TyConBinders to record this extra information.
Note that in *terms* we do not allow
f @a (x::a) = rhs
unless `f` has a type signature. So we do the same for types:
We allow `@` binders in data type declarations ONLY if the
type constructor has a standalone kind signature (or a CUSK).
That means that GHC.Tc.Gen.HsType.kcInferDeclHeader, which is used when we
don't have a kind signature or CUSK, and builds a MonoTcTyCon, we can simply
reject invisible binders outright (GHC.Tc.Gen.HsType.rejectInvisibleBinders);
and continue to use mkAnonTyConBinders as described in
Note [No polymorphic recursion in type decls].
If we get cries of pain we can revist this decision.
It should be possible to implement this (I prefer the idea with a dedicated ->.
arrow), but it also doesn't seem worth the implementation cost until we find a compelling example.