From 84cc8394d075cea236faa0bcd9ef0a84de89ee8c Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Tue, 7 Apr 2020 15:23:18 +0100 Subject: Add a missing zonk in tcHsPartialType I omitted a vital zonk when refactoring tcHsPartialType in commit 48fb3482f8cbc8a4b37161021e846105f980eed4 Author: Simon Peyton Jones Date: Wed Jun 5 08:55:17 2019 +0100 Fix typechecking of partial type signatures This patch fixes it and adds commentary to explain why. Fixes #18008 --- compiler/GHC/Tc/Gen/HsType.hs | 95 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 81 insertions(+), 14 deletions(-) (limited to 'compiler/GHC/Tc/Gen') diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index be5b4f7694..094ed623ac 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -732,6 +732,7 @@ tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs m_telescope = Just (sep (map ppr hs_tvs)) ; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted + -- See Note [Skolem escape and forall-types] ; return (mkForAllTys bndrs ty') } @@ -920,6 +921,26 @@ under these conditions. See related Note [Wildcards in visible type application] here and Note [The wildcard story for types] in GHC.Hs.Types +Note [Skolem escape and forall-types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> () + +The Proxy '[a,b] forces a and b to have the same kind. But a's +kind must be bound outside the 'forall a', and hence escapes. +We discover this by building an implication constraint for +each forall. So the inner implication constraint will look like + forall kb (b::kb). kb ~ ka +where ka is a's kind. We can't unify these two, /even/ if ka is +unification variable, because it would be untouchable inside +this inner implication. + +That's what the pushLevelAndCaptureConstraints, plus subsequent +emitResidualTvConstraint is all about, when kind-checking +HsForAllTy. + +Note that we don't need to /simplify/ the constraints here +because we aren't generalising. We just capture them. -} {- ********************************************************************* @@ -2819,10 +2840,13 @@ kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty ; kindGeneralizeSome (const True) ty } -- | Specialized version of 'kindGeneralizeSome', but where no variables --- can be generalized. Use this variant when it is unknowable whether metavariables --- might later be constrained. --- See Note [Recipe for checking a signature] for why and where this --- function is needed. +-- can be generalized, but perhaps some may neeed to be promoted. +-- Use this variant when it is unknowable whether metavariables might +-- later be constrained. +-- +-- To see why this promotion is needed, see +-- Note [Recipe for checking a signature], and especially +-- Note [Promotion in signatures]. kindGeneralizeNone :: TcType -- needn't be zonked -> TcM () kindGeneralizeNone ty @@ -3160,7 +3184,7 @@ tcHsPartialSigType ctxt sig_ty ; return (wcs, wcx, theta, tau) } - -- No kind-generalization here: + -- No kind-generalization here, but perhaps some promotion ; kindGeneralizeNone (mkSpecForAllTys implicit_tvs $ mkSpecForAllTys explicit_tvs $ mkPhiTy theta $ @@ -3171,6 +3195,14 @@ tcHsPartialSigType ctxt sig_ty -- See Note [Extra-constraint holes in partial type signatures] ; emitNamedWildCardHoleConstraints wcs + -- Zonk, so that any nested foralls can "see" their occurrences + -- See Note [Checking partial type signatures], in + -- the bullet on Nested foralls. + ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs + ; explicit_tvs <- mapM zonkTcTyVarToTyVar explicit_tvs + ; theta <- mapM zonkTcType theta + ; tau <- zonkTcType tau + -- We return a proper (Name,TyVar) environment, to be sure that -- we bring the right name into scope in the function body. -- Test case: partial-sigs/should_compile/LocalDefinitionBug @@ -3179,7 +3211,7 @@ tcHsPartialSigType ctxt sig_ty -- NB: checkValidType on the final inferred type will be -- done later by checkInferredPolyId. We can't do it - -- here because we don't have a complete tuype to check + -- here because we don't have a complete type to check ; traceTc "tcHsPartialSigType" (ppr tv_prs) ; return (wcs, wcx, tv_prs, theta, tau) } @@ -3198,12 +3230,31 @@ tcPartialContext hs_theta {- Note [Checking partial type signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See also Note [Recipe for checking a signature] +This Note is about tcHsPartialSigType. See also +Note [Recipe for checking a signature] When we have a partial signature like - f,g :: forall a. a -> _ + 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 tyvar binders] in GHC.Tc.Gen.HsType + * In GHC.Tc.Gen.Sig.tcUserSigType we return a PartialSig, which (unlike the companion CompleteSig) contains the original, as-yet-unchecked source-code LHsSigWcType @@ -3218,12 +3269,28 @@ we do the following g x = True It's really as if we'd written two distinct signatures. -* Note that we don't 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. +* Nested foralls. Consider + f :: forall b. (forall a. a -> _) -> b + We do /not/ allow the "_" to be instantiated to 'a'; but we do + (as before) allow it to be instantiated to the (top level) 'b'. + Why not? Because suppose + f x = (x True, x 'c') + We must instantiate that (forall a. a -> _) when typechecking + f's body, so we must know precisely where all the a's are; they + must not be hidden under (filled-in) unification variables! + + We achieve this in the usual way: we push a level at a forall, + so now the unification variable for the "_" can't unify with + 'a'. + +* Just as for ordinary signatures, we must zonk the type after + kind-checking it, to ensure that all the nested forall binders can + see their occurrenceds + + 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. Note [Extra-constraint holes in partial type signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.1