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.
References 2
- No polymorphic recursion in type decls GHC.Tc.TyCl
- TcTyCon, MonoTcTyCon, and PolyTcTyCon GHC.Tc.TyCl
Referenced by 2
- GHC.Tc.Gen.HsType call site
- No polymorphic recursion in type decls GHC.Tc.TyCl