Note [Skolem escape in type signatures]

GHC/Tc/Gen/HsType.hs:557 compiler

tcHsSigType is tricky.  Consider (T11142)
  foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
This is ill-kinded because of a nested skolem-escape.

That will show up as an un-solvable constraint in the implication
returned by buildTvImplication in tc_lhs_sig_type.  See Note [Skolem
escape prevention] in GHC.Tc.Utils.TcType for why it is unsolvable
(the unification variable for b's kind is untouchable).

Then, in GHC.Tc.Solver.simplifyAndEmitFlatConstraints (called from tcHsSigType)
we'll try to float out the constraint, be unable to do so, and fail.
See GHC.Tc.Solver Note [Failure in local type signatures] for more
detail on this.

The separation between tcHsSigType and tc_lhs_sig_type is because
tcClassSigType wants to use the latter, but *not* fail fast, because
there are skolems from the class decl which are in scope; but it's fine
not to because tcClassDecl1 has a solveEqualities wrapped around all
the tcClassSigType calls.

That's why tcHsSigType does simplifyAndEmitFlatConstraints (which
fails fast) but tcClassSigType just does emitImplication (which does
not).  Ugh.

c.f. see also Note [Skolem escape and forall-types]. The difference
is that we don't need to simplify at a forall type, only at the
top level of a signature.

References 2

Referenced by 1