Note [Checking partial type signatures]
This Note is about tcHsPartialSigType. See also Note [Recipe for checking a signature] When we have a partial signature like f :: forall a. a -> _ we do the following * tcHsPartialSigType does not make quantified type (forall a. blah) and then instantiate it -- it makes no sense to instantiate a type with wildcards in it. Rather, tcHsPartialSigType just returns the 'a' and the 'blah' separately. Nor, for the same reason, do we push a level in tcHsPartialSigType. * We instantiate 'a' to a unification variable, a TyVarTv, and /not/ a skolem; hence the "_Tv" in bindExplicitTKBndrs_Tv. Consider f :: forall a. a -> _ g :: forall b. _ -> b f = g g = f They are typechecked as a recursive group, with monomorphic types, so 'a' and 'b' will get unified together. Very like kind inference for mutually recursive data types (sans CUSKs or SAKS); see Note [Cloning for type variable binders] * In GHC.Tc.Gen.Sig.tcUserSigType we return a PartialSig, which (unlike the companion CompleteSig) contains the original, as-yet-unchecked source-code LHsSigWcType * Then, for f and g /separately/, we call tcInstSig, which in turn call tcHsPartialSig (defined near this Note). It kind-checks the LHsSigWcType, creating fresh unification variables for each "_" wildcard. It's important that the wildcards for f and g are distinct because they might get instantiated completely differently. E.g. f,g :: forall a. a -> _ f x = a g x = True It's really as if we'd written two distinct signatures. * Nested foralls. See Note [Levels for wildcards] * Just as for ordinary signatures, we must solve local equalities and zonk the type after kind-checking it, to ensure that all the nested forall binders can "see" their occurrences Just as for ordinary signatures, this zonk also gets any Refl casts out of the way of instantiation. Example: #18008 had foo :: (forall a. (Show a => blah) |> Refl) -> _ and that Refl cast messed things up. See #18062.
References 3
- Cloning for type variable binders GHC.Tc.Gen.HsType
- Levels for wildcards GHC.Tc.Gen.HsType
- Recipe for checking a signature GHC.Tc.Gen.HsType
Referenced by 7
- GHC.Tc.Gen.HsType call site ×5
- GHC.Tc.Gen.Sig call site
- Failure in local type signatures GHC.Tc.Solver