Note [Inferring visible dependent quantification]

GHC/Tc/TyCl.hs:1782 compiler 2 tickets

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

Referenced by 2