Note [Skolem escape in type signatures]
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
- Skolem escape and forall-types GHC.Tc.Gen.HsType
- Failure in local type signatures GHC.Tc.Solver
Referenced by 1
- GHC.Tc.Gen.HsType call site