Note [Inferring visible dependent quantification]
Consider
data T k :: k -> Type where
MkT1 :: T Type Int
MkT2 :: T (Type -> Type) Maybe
This looks like it should work. However, it is polymorphically recursive,
as the uses of T in the constructor types specialize the k in the kind
of T. This trips up our dear users (#17131, #17541), and so we add
a "landmark" context (which cannot be suppressed) whenever we
spot inferred visible dependent quantification (VDQ).
It's hard to know when we've actually been tripped up by polymorphic recursion
specifically, so we just include a note to users whenever we infer VDQ. The
testsuite did not show up a single spurious inclusion of this message.
The context is added in addVDQNote, which looks for a visible
TyConBinder that also appears in the TyCon's kind. (I first looked at
the kind for a visible, dependent quantifier, but
Note [No polymorphic recursion in type decls]
in GHC.Tc.Gen.HsType defeats that approach.) addVDQNote is used in
kcTyClDecl, which is used only when inferring the kind of a tycon
(never with a CUSK or SAKS).
Once upon a time, I (Richard E) thought that the tycon-kind could
not be a forall-type. But this is wrong: data T :: forall k. k -> Type
(with -XNoCUSKs) could end up here. And this is all OK. References 1
- No polymorphic recursion in type decls GHC.Tc.TyCl
Referenced by 2
- GHC.Tc.TyCl call site ×2