Note [No polymorphic recursion in type decls]
In GHC.Tc.HsType.kcInferDeclHeader we use mkAnonTyConBinders to make the TyConBinders for the MonoTcTyCon. Here is why. Should this kind-check (cf #16344)? data T ka (a::ka) b = MkT (T Type Int Bool) (T (Type -> Type) Maybe Bool) Notice that T is used at two different kinds in its RHS. No! This should not kind-check. Polymorphic recursion is known to be a tough nut. Many moons ago, we laboriously (with help from the renamer) tried to give T the polymorphic kind T :: forall ka -> ka -> kappa -> Type where kappa is a unification variable, even in the inferInitialKinds phase (which is what kcInferDeclHeader is all about). But that is dangerously fragile (see #16344), because `kappa` might get unified with `ka`, and depending on just /when/ that unification happens, the instantiation of T's kind would vary between different call sites of T. We encountered similar trickiness with invisible binders in type declarations: see Note [No inference for invisible binders in type decls] Solution: the Monomorphic Recursion Principle: A MonoTcTyCon has a monomoprhic kind (no foralls!) See the invariants on MonoTcTyCon in Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]. So kcInferDeclHeader gives T a straightforward monomorphic kind, with no quantification whatsoever. That's why we always use mkAnonTyConBinder for all arguments when figuring out tc_binders. But notice that (#16344 comment:3) * Consider this declaration: data T2 ka (a::ka) = MkT2 (T2 Type a) Starting with inferInitialKinds (Step 1 of Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]): MonoTcTyCon binders: ka[tyv] :: (kappa1[tau] :: Type) a[tyv] :: (ka[tyv] :: Type) MonoTcTyCon kind: T2 :: kappa1[tau] -> ka[tyv] -> Type Given this kind for T2, in Step 2 we kind-check (T2 Type a) from where we see T2's first arg: (kappa1 ~ Type) T2's second arg: (ka ~ ka) These constraints are soluble by (kappa1 := Type) so generaliseTcTyCon (Step 3) gives T2 :: forall (k::Type) -> k -> * But now the /typechecking/ (Step 4, aka desugaring, tcTyClDecl) phase fails, because the call (T2 Type a) in the RHS is ill-kinded. We'd really prefer all errors to show up in the kind checking phase. * This algorithm still accepts (in all phases) data T3 ka (a::ka) = forall b. MkT3 (T3 Type b) although T3 is really polymorphic-recursive too. Perhaps we should somehow reject that.
References 2
- No inference for invisible binders in type decls GHC.Tc.TyCl
- TcTyCon, MonoTcTyCon, and PolyTcTyCon GHC.Tc.TyCl
Referenced by 6
- TcTyCon, MonoTcTyCon, and PolyTcTyCon GHC.Tc.TyCl ×2
- No inference for invisible binders in type decls GHC.Tc.TyCl ×2
- GHC.Tc.Gen.HsType call site
- Inferring visible dependent quantification GHC.Tc.TyCl