diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2021-03-13 23:46:50 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-03-31 11:12:52 -0400 |
commit | dbadd672ba7da67533c34d8594ac7f91dde0f415 (patch) | |
tree | 4c40cc05d77aa270d754c4090ebcaa1fbe62d8f4 /compiler | |
parent | 44774dc591206291d06e6181f599151631062332 (diff) | |
download | haskell-dbadd672ba7da67533c34d8594ac7f91dde0f415.tar.gz |
The result kind of a signature can't mention quantified vars
This patch fixes a small but egregious bug, which allowed
a type signature like
f :: forall a. blah
not to fail if (blah :: a). Acutally this only showed
up as a ASSERT error (#19495).
The fix is very short, but took quite a bit of head scratching
Hence the long Note [Escaping kind in type signatures]
While I was in town, I also added a short-cut for the
common case of having no quantifiers to tcImplicitTKBndrsX.
Metric Decrease:
T9198
Metric Increase:
T9198
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 88 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 7 |
2 files changed, 86 insertions, 9 deletions
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index f7ad3a2af6..bf836e5602 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -445,17 +445,22 @@ tc_lhs_sig_type :: SkolemInfo -> LHsSigType GhcRn -- This will never emit constraints, as it uses solveEqualities internally. -- No validity checking or zonking -- Returns also an implication for the unsolved constraints -tc_lhs_sig_type skol_info (L loc (HsSig { sig_bndrs = hs_outer_bndrs - , sig_body = hs_ty })) ctxt_kind +tc_lhs_sig_type skol_info full_hs_ty@(L loc (HsSig { sig_bndrs = hs_outer_bndrs + , sig_body = hs_ty })) ctxt_kind = setSrcSpanA loc $ - do { (tc_lvl, wanted, (outer_bndrs, ty)) + do { (tc_lvl, wanted, (exp_kind, (outer_bndrs, ty))) <- pushLevelAndSolveEqualitiesX "tc_lhs_sig_type" $ -- See Note [Failure in local type signatures] - tcOuterTKBndrs skol_info hs_outer_bndrs $ - do { kind <- newExpectedKind ctxt_kind - ; tcLHsType hs_ty kind } - -- Any remaining variables (unsolved in the solveEqualities) - -- should be in the global tyvars, and therefore won't be quantified + do { exp_kind <- newExpectedKind ctxt_kind + -- See Note [Escaping kind in type signatures] + ; stuff <- tcOuterTKBndrs skol_info hs_outer_bndrs $ + tcLHsType hs_ty exp_kind + ; return (exp_kind, stuff) } + + -- Default any unconstrained variables free in the kind + -- See Note [Escaping kind in type signatures] + ; exp_kind_dvs <- candidateQTyVarsOfType exp_kind + ; doNotQuantifyTyVars exp_kind_dvs (mk_doc exp_kind) ; traceTc "tc_lhs_sig_type" (ppr hs_outer_bndrs $$ ppr outer_bndrs) ; (outer_tv_bndrs :: [InvisTVBinder]) <- scopedSortOuter outer_bndrs @@ -469,9 +474,68 @@ tc_lhs_sig_type skol_info (L loc (HsSig { sig_bndrs = hs_outer_bndrs ; implic <- buildTvImplication skol_info kvs tc_lvl wanted ; return (implic, mkInfForAllTys kvs ty1) } + where + mk_doc exp_kind tidy_env + = do { (tidy_env2, exp_kind) <- zonkTidyTcType tidy_env exp_kind + ; return (tidy_env2, hang (text "The kind" <+> ppr exp_kind) + 2 (text "of type signature:" <+> ppr full_hs_ty)) } + -{- Note [Skolem escape in type signatures] + +{- Note [Escaping kind in type signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider kind-checking the signature for `foo` (#19495): + type family T (r :: RuntimeRep) :: TYPE r + + foo :: forall (r :: RuntimeRep). T r + foo = ... + +We kind-check the type with expected kind `TYPE delta` (see newExpectedKind), +where `delta :: RuntimeRep` is as-yet unknown. (We can't use `TYPE LiftedRep` +because we allow signatures like `foo :: Int#`.) + +Suppose we are at level L currently. We do this + * pushLevelAndSolveEqualitiesX: moves to level L+1 + * newExpectedKind: allocates delta{L+1} + * tcOuterTKBndrs: pushes the level again to L+2, binds skolem r{L+2} + * kind-check the body (T r) :: TYPE delta{L+1} + +Then +* We can't unify delta{L+1} with r{L+2}. + And rightly so: skolem would escape. + +* If delta{L+1} is unified with some-kind{L}, that is fine. + This can happen + \(x::a) -> let y :: a; y = x in ...(x :: Int#)... + Here (x :: a :: TYPE gamma) is in the environment when we check + the signature y::a. We unify delta := gamma, and all is well. + +* If delta{L+1} is unconstrained, we /must not/ quantify over it! + E.g. Consider f :: Any where Any :: forall k. k + We kind-check this with expected kind TYPE kappa. We get + Any @(TYPE kappa) :: TYPE kappa + We don't want to generalise to forall k. Any @k + because that is ill-kinded: the kind of the body of the forall, + (Any @k :: k) mentions the bound variable k. + + Instead we want to default it to LiftedRep. + + An alternative would be to promote it, similar to the monomorphism + restriction, but the MR is pretty confusing. Defaulting seems better + +How does that defaulting happen? Well, since we /currently/ default +RuntimeRep variables during generalisation, it'll happen in +kindGeneralize. But in principle we might allow generalisation over +RuntimeRep variables in future. Moreover, what if we had + kappa{L+1} := F alpha{L+1} +where F :: Type -> RuntimeRep. Now it's alpha that is free in the kind +and it /won't/ be defaulted. + +So we use doNotQuantifyTyVars to either default the free vars of +exp_kind (if possible), or error (if not). + +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. @@ -3210,6 +3274,12 @@ tcImplicitTKBndrsX :: SkolemMode -> SkolemInfo -- and emit an implication constraint with a ForAllSkol ic_info, -- so that it is subject to a telescope test. tcImplicitTKBndrsX skol_mode skol_info bndrs thing_inside + | null bndrs -- Short-cut the common case with no quantifiers + -- E.g. f :: Int -> Int + -- makes a HsOuterImplicit with empty bndrs, + -- and tcOuterTKBndrsX goes via here + = do { res <- thing_inside; return ([], res) } + | otherwise = do { (tclvl, wanted, (skol_tvs, res)) <- pushLevelAndCaptureConstraints $ bindImplicitTKBndrsX skol_mode bndrs $ diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index b6f5065997..519a2b37a8 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -1252,6 +1252,9 @@ skolems are in scope within the type itself (e.g. that 'forall arg'). This change is inspired by and described in Section 7.2 of "Kind Inference for Datatypes", POPL'20. +NB: this is all rather similar to, but sadly not the same as + Note [Error on unconstrained meta-variables] + Wrinkle: We must make absolutely sure that alpha indeed is not @@ -1919,6 +1922,9 @@ on kappa. What to do? We choose (D), as described in #17567. Discussion of alternatives is below. +NB: this is all rather similar to, but sadly not the same as + Note [Naughty quantification candidates] + (One last example: type instance F Int = Proxy Any, where the unconstrained kind variable is the inferred kind of Any. The four examples here illustrate all cases in which this Note applies.) @@ -1998,6 +2004,7 @@ doNotQuantifyTyVars :: CandidatesQTvs -> (TidyEnv -> TcM (TidyEnv, SDoc)) -- ^ like "the class context (D a b, E foogle)" -> TcM () +-- See Note [Error on unconstrained meta-variables] doNotQuantifyTyVars dvs where_found | isEmptyCandidates dvs = traceTc "doNotQuantifyTyVars has nothing to error on" empty |