Note [CUSKs and PolyKinds]
Consider
data T (a :: *) = MkT (S a) -- Has CUSK
data S a = MkS (T Int) (S a) -- No CUSK
Via inferInitialKinds we get
T :: * -> *
S :: kappa -> *
Then we call kcTyClDecl on each decl in the group, to constrain the
kind unification variables. BUT we /skip/ the RHS of any decl with
a CUSK. Here we skip the RHS of T, so we eventually get
S :: forall k. k -> *
This gets us more polymorphism than we would otherwise get, similar
(but implemented strangely differently from) the treatment of type
signatures in value declarations.
However, we only want to do so when we have PolyKinds.
When we have NoPolyKinds, we don't skip those decls, because we have defaulting
(#16609). Skipping won't bring us more polymorphism when we have defaulting.
Consider
data T1 a = MkT1 T2 -- No CUSK
data T2 = MkT2 (T1 Maybe) -- Has CUSK
If we skip the rhs of T2 during kind-checking, the kind of a remains unsolved.
With PolyKinds, we do generalization to get T1 :: forall a. a -> *. And the
program type-checks.
But with NoPolyKinds, we do defaulting to get T1 :: * -> *. Defaulting happens
in quantifyTyVars, which is called from generaliseTcTyCon. Then type-checking
(T1 Maybe) will throw a type error.
Summary: with PolyKinds, we must skip; with NoPolyKinds, we must /not/ skip.
Open type families
~~~~~~~~~~~~~~~~~~
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.
The kind of an open type family is solely determined by its kind signature;
hence, only kind signatures participate in the construction of the initial
kind environment (as constructed by `inferInitialKind'). In fact, we ignore
instances of families altogether in the following. However, we need to include
the kinds of *associated* families into the construction of the initial kind
environment. (This is handled by `allDecls').
See also Note [Kind checking recursive type and class declarations] References 1
Referenced by 1
- GHC.Tc.TyCl call site