diff options
| -rw-r--r-- | compiler/typecheck/TcSimplify.hs | 90 | ||||
| -rw-r--r-- | testsuite/tests/partial-sigs/should_compile/T11016.hs | 9 | ||||
| -rw-r--r-- | testsuite/tests/partial-sigs/should_compile/T11016.stderr | 11 | ||||
| -rw-r--r-- | testsuite/tests/partial-sigs/should_compile/all.T | 1 |
4 files changed, 76 insertions, 35 deletions
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index fae58ade35..467ea9c2f0 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -426,30 +426,25 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds ] - -- Historical note: Before step 2 we used to have a - -- HORRIBLE HACK described in Note [Avoid unnecessary - -- constraint simplification] but, as described in Trac - -- #4361, we have taken in out now. That's why we start - -- with step 2! - - -- Step 2) First try full-blown solving - - -- NB: we must gather up all the bindings from doing - -- this solving; hence (runTcSWithEvBinds ev_binds_var). - -- And note that since there are nested implications, - -- calling solveWanteds will side-effect their evidence - -- bindings, so we can't just revert to the input - -- constraint. + -- First do full-blown solving + -- NB: we must gather up all the bindings from doing + -- this solving; hence (runTcSWithEvBinds ev_binds_var). + -- And note that since there are nested implications, + -- calling solveWanteds will side-effect their evidence + -- bindings, so we can't just revert to the input + -- constraint. ; ev_binds_var <- TcM.newTcEvBinds ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $ - runTcSWithEvBinds ev_binds_var (solveWanteds wanteds) + do { sig_derived <- concatMapM mkSigDerivedWanteds sigs + ; runTcSWithEvBinds ev_binds_var $ + solveWanteds (wanteds `addSimples` listToBag sig_derived) } ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs - -- Step 4) Candidates for quantification are an approximation of wanted_transformed - -- NB: Already the fixpoint of any unifications that may have happened - -- NB: We do not do any defaulting when inferring a type, this can lead - -- to less polymorphic types, see Note [Default while Inferring] + -- Find quant_pred_candidates, the predicates that + -- we'll consider quantifying over + -- NB: We do not do any defaulting when inferring a type, this can lead + -- to less polymorphic types, see Note [Default while Inferring] ; tc_lcl_env <- TcRn.getLclEnv ; null_ev_binds_var <- TcM.newTcEvBinds @@ -484,14 +479,14 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds -- NB: quant_pred_candidates is already fully zonked - -- Decide what type variables and constraints to quantify + -- Decide what type variables and constraints to quantify ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus ; let zonked_tau_tvs = tyVarsOfTypes zonked_taus ; (qtvs, bound_theta) <- decideQuantification apply_mr sigs name_taus quant_pred_candidates zonked_tau_tvs - -- Emit an implication constraint for the - -- remaining constraints from the RHS + -- Emit an implication constraint for the + -- remaining constraints from the RHS ; bound_ev_vars <- mapM TcM.newEvVar bound_theta ; let skol_info = InferSkol [ (name, mkSigmaTy [] bound_theta ty) | (name, ty) <- name_taus ] @@ -510,18 +505,18 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds , ic_env = tc_lcl_env } ; emitImplication implic - -- Promote any type variables that are free in the inferred type - -- of the function: - -- f :: forall qtvs. bound_theta => zonked_tau - -- These variables now become free in the envt, and hence will show - -- up whenever 'f' is called. They may currently at rhs_tclvl, but - -- they had better be unifiable at the outer_tclvl! - -- Example: envt mentions alpha[1] - -- tau_ty = beta[2] -> beta[2] - -- consraints = alpha ~ [beta] - -- we don't quantify over beta (since it is fixed by envt) - -- so we must promote it! The inferred type is just - -- f :: beta -> beta + -- Promote any type variables that are free in the inferred type + -- of the function: + -- f :: forall qtvs. bound_theta => zonked_tau + -- These variables now become free in the envt, and hence will show + -- up whenever 'f' is called. They may currently at rhs_tclvl, but + -- they had better be unifiable at the outer_tclvl! + -- Example: envt mentions alpha[1] + -- tau_ty = beta[2] -> beta[2] + -- consraints = alpha ~ [beta] + -- we don't quantify over beta (since it is fixed by envt) + -- so we must promote it! The inferred type is just + -- f :: beta -> beta ; outer_tclvl <- TcRn.getTcLevel ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV zonked_tau_tvs -- decideQuantification turned some meta tyvars into @@ -544,7 +539,32 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds ; return ( qtvs, bound_ev_vars, TcEvBinds ev_binds_var) } -{- +mkSigDerivedWanteds :: TcIdSigInfo -> TcM [Ct] +-- See Note [Add deriveds for signature contexts] +mkSigDerivedWanteds (TISI { sig_bndr = PartialSig { sig_name = name } + , sig_theta = theta, sig_tau = tau }) + = do { let skol_info = InferSkol [(name, mkSigmaTy [] theta tau)] + ; loc <- getCtLocM (GivenOrigin skol_info) + ; return [ mkNonCanonical (CtDerived { ctev_pred = pred + , ctev_loc = loc }) + | pred <- theta ] } +mkSigDerivedWanteds _ = return [] + +{- Note [Add deriveds for signature contexts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this (Trac #11016): + f2 :: (?x :: Int) => _ + f2 = ?x +We'll use plan InferGen because there are holes in the type. But we want +to have the (?x :: Int) constraint floating around so that the functional +dependencies kick in. Otherwise the occurrence of ?x on the RHS produces +constraint (?x :: alpha), and we wont unify alpha:=Int. + +Solution: in simplifyInfer, just before simplifying the constraints +gathered from the RHS, add Derived constraints for the context of any +type signatures. This is rare; if there is a type signature we'll usually +be doing CheckGen. But it happens for signatures with holes. + ************************************************************************ * * Quantification diff --git a/testsuite/tests/partial-sigs/should_compile/T11016.hs b/testsuite/tests/partial-sigs/should_compile/T11016.hs new file mode 100644 index 0000000000..02b7d4d3a8 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_compile/T11016.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE ImplicitParams, PartialTypeSignatures #-} + +module T11016 where + +f1 :: (?x :: Int, _) => Int +f1 = ?x + +f2 :: (?x :: Int) => _ +f2 = ?x diff --git a/testsuite/tests/partial-sigs/should_compile/T11016.stderr b/testsuite/tests/partial-sigs/should_compile/T11016.stderr new file mode 100644 index 0000000000..74dd18d9bf --- /dev/null +++ b/testsuite/tests/partial-sigs/should_compile/T11016.stderr @@ -0,0 +1,11 @@ + +T11016.hs:5:19: warning: + Found constraint wildcard ‘_’ standing for ‘()’ + In the type signature: + f1 :: (?x :: Int, _) => Int + +T11016.hs:8:22: warning: + • Found type wildcard ‘_’ standing for ‘Int’ + • In the type signature: + f2 :: (?x :: Int) => _ + • Relevant bindings include f2 :: Int (bound at T11016.hs:9:1) diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T index 142d3318c8..5567ef1bdf 100644 --- a/testsuite/tests/partial-sigs/should_compile/all.T +++ b/testsuite/tests/partial-sigs/should_compile/all.T @@ -57,3 +57,4 @@ test('T10438', normal, compile, ['']) test('T10519', normal, compile, ['']) test('T10463', normal, compile, ['']) test('ExprSigLocal', normal, compile, ['']) +test('T11016', normal, compile, ['']) |