Commit 28035c09 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Add derived constraints for wildcard signatures

This fixes Trac #11016

See Note [Add deriveds for signature contexts] in TcSimplify]
parent 1c9fd3f1
......@@ -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
......
{-# LANGUAGE ImplicitParams, PartialTypeSignatures #-}
module T11016 where
f1 :: (?x :: Int, _) => Int
f1 = ?x
f2 :: (?x :: Int) => _
f2 = ?x
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)
......@@ -57,3 +57,4 @@ test('T10438', normal, compile, [''])
test('T10519', normal, compile, [''])
test('T10463', normal, compile, [''])
test('ExprSigLocal', normal, compile, [''])
test('T11016', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment