simplifyAmbiguityCheck,
simplifyDefault,
simplifyTop, simplifyTopImplic, captureTopConstraints,
- simplifyInteractive, solveEqualities,
+ simplifyInteractive,
+ solveEqualities, solveLocalEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
+ simpl_top,
+
+ promoteTyVar,
+ promoteTyVarSet,
+
-- For Rules we need these
solveWanteds, solveWantedsAndDrop,
approximateWC, runTcSDeriveds
#include "HsVersions.h"
+import GhcPrelude
+
import Bag
import Class ( Class, classKey, classTyCon )
import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
, WarnReason ( Reason )
, DynFlags( solverIterations ) )
+import Id ( idType )
import Inst
import ListSetOps
-import Maybes
import Name
import Outputable
import PrelInfo
import TcErrors
import TcEvidence
import TcInteract
-import TcCanonical ( makeSuperClasses )
+import TcCanonical ( makeSuperClasses, solveCallStack )
import TcMType as TcM
import TcRnMonad as TcM
import TcSMonad as TcS
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
-import Data.List ( partition )
+import Data.Foldable ( toList )
+import Data.List ( partition )
+import Data.List.NonEmpty ( NonEmpty(..) )
+import Maybes ( isJust )
{-
*********************************************************************************
; TcM.writeTcRef errs_var emptyMessages
; warnAllUnsolved $ WC { wc_simple = unsafe_ol
- , wc_insol = emptyCts
, wc_impl = emptyBag }
; whyUnsafe <- fst <$> TcM.readTcRef errs_var
; return (evBindMapBinds binds1 `unionBags` binds2) }
+-- | Type-check a thing that emits only equality constraints, solving any
+-- constraints we can and re-emitting constraints that we can't. The thing_inside
+-- should generally bump the TcLevel to make sure that this run of the solver
+-- doesn't affect anything lying around.
+solveLocalEqualities :: TcM a -> TcM a
+solveLocalEqualities thing_inside
+ = do { traceTc "solveLocalEqualities {" empty
+
+ ; (result, wanted) <- captureConstraints thing_inside
+
+ ; traceTc "solveLocalEqualities: running solver {" (ppr wanted)
+ ; reduced_wanted <- runTcSEqualities (solveWanteds wanted)
+ ; traceTc "solveLocalEqualities: running solver }" (ppr reduced_wanted)
+
+ ; emitConstraints reduced_wanted
+
+ ; traceTc "solveLocalEqualities end }" empty
+ ; return result }
+
-- | Type-check a thing that emits only equality constraints, then
-- solve those constraints. Fails outright if there is trouble.
+-- Use this if you're not going to get another crack at solving
+-- (because, e.g., you're checking a datatype declaration)
solveEqualities :: TcM a -> TcM a
solveEqualities thing_inside
= checkNoErrs $ -- See Note [Fail fast on kind errors]
do { (result, wanted) <- captureConstraints thing_inside
; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
; final_wc <- runTcSEqualities $ simpl_top wanted
+ -- NB: Use simpl_top here so that we potentially default RuntimeRep
+ -- vars to LiftedRep. This is needed to avoid #14991.
; traceTc "End solveEqualities }" empty
; traceTc "reportAllUnsolved {" empty
; traceTc "reportAllUnsolved }" empty
; return result }
+-- | Simplify top-level constraints, but without reporting any unsolved
+-- constraints nor unsafe overlapping.
simpl_top :: WantedConstraints -> TcS WantedConstraints
-- See Note [Top-level Defaulting Plan]
simpl_top wanteds
; setImplicationStatus (implic { ic_wanted = wanteds }) }
defaultCallStack ct
- | Just _ <- isCallStackPred (ctPred ct)
- = do { solveCallStack (cc_ev ct) EvCsEmpty
+ | ClassPred cls tys <- classifyPredType (ctPred ct)
+ , Just {} <- isCallStackPred cls tys
+ = do { solveCallStack (ctEvidence ct) EvCsEmpty
; return Nothing }
defaultCallStack ct
| not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
= return insols -- Hurrah -- stop now.
| otherwise
- = do { pending_given <- getPendingScDicts
+ = do { pending_given <- getPendingGivenScs
; new_given <- makeSuperClasses pending_given
; solveSimpleGivens new_given
; getInertInsols }
-> WantedConstraints
-> TcM ([TcTyVar], -- Quantify over these type variables
[EvVar], -- ... and these constraints (fully zonked)
- TcEvBinds) -- ... binding these evidence variables
+ TcEvBinds, -- ... binding these evidence variables
+ WantedConstraints, -- Redidual as-yet-unsolved constraints
+ Bool) -- True <=> the residual constraints are insoluble
+
simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
| isEmptyWC wanteds
= do { gbl_tvs <- tcGetGlobalTyCoVars
; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
; qtkvs <- quantifyTyVars gbl_tvs dep_vars
; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
- ; return (qtkvs, [], emptyTcEvBinds) }
+ ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) }
| otherwise
= do { traceTc "simplifyInfer {" $ vcat
-- bindings, so we can't just revert to the input
-- constraint.
- ; tc_lcl_env <- TcM.getLclEnv
+ ; tc_env <- TcM.getEnv
; ev_binds_var <- TcM.newTcEvBinds
; psig_theta_vars <- mapM TcM.newEvVar psig_theta
; wanted_transformed_incl_derivs
<- setTcLevel rhs_tclvl $
runTcSWithEvBinds ev_binds_var $
- do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
+ do { let loc = mkGivenLoc rhs_tclvl UnkSkol $
+ env_lcl tc_env
psig_givens = mkGivens loc psig_theta_vars
; _ <- solveSimpleGivens psig_givens
-- See Note [Add signature contexts as givens]
- ; wanteds' <- solveWanteds wanteds
- ; TcS.zonkWC wanteds' }
+ ; solveWanteds wanteds }
-- Find quant_pred_candidates, the predicates that
-- we'll consider quantifying over
-- the psig_theta; it's just the extra bit
-- NB2: We do not do any defaulting when inferring a type, this can lead
-- to less polymorphic types, see Note [Default while Inferring]
-
- ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
- quant_pred_candidates -- Fully zonked
- | insolubleWC wanted_transformed_incl_derivs
- = [] -- See Note [Quantification with errors]
- -- NB: must include derived errors in this test,
- -- hence "incl_derivs"
-
- | otherwise
- = ctsPreds (approximateWC False wanted_transformed)
-
- -- NB: quant_pred_candidates is already fully zonked
+ ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
+ ; let definite_error = insolubleWC wanted_transformed_incl_derivs
+ -- See Note [Quantification with errors]
+ -- NB: must include derived errors in this test,
+ -- hence "incl_derivs"
+ wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
+ quant_pred_candidates
+ | definite_error = []
+ | otherwise = ctsPreds (approximateWC False wanted_transformed)
-- Decide what type variables and constraints to quantify
+ -- NB: quant_pred_candidates is already fully zonked
-- NB: bound_theta are constraints we want to quantify over,
- -- /apart from/ the psig_theta, which we always quantify over
- ; (qtvs, bound_theta) <- decideQuantification infer_mode rhs_tclvl
+ -- including the psig_theta, which we always quantify over
+ -- NB: bound_theta are fully zonked
+ ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
name_taus partial_sigs
quant_pred_candidates
-
- -- Emit an implication constraint for the
- -- remaining constraints from the RHS.
- -- We must retain the psig_theta_vars, because we've used them in
- -- evidence bindings constructed by solveWanteds earlier
- ; psig_theta_vars <- mapM zonkId psig_theta_vars
; bound_theta_vars <- mapM TcM.newEvVar bound_theta
- ; let full_theta = psig_theta ++ bound_theta
- full_theta_vars = psig_theta_vars ++ bound_theta_vars
- skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
- | (name, ty) <- name_taus ]
- -- Don't add the quantified variables here, because
- -- they are also bound in ic_skols and we want them
- -- to be tidied uniformly
-
- implic = Implic { ic_tclvl = rhs_tclvl
- , ic_skols = qtvs
- , ic_no_eqs = False
- , ic_given = full_theta_vars
- , ic_wanted = wanted_transformed
- , ic_status = IC_Unsolved
- , ic_binds = ev_binds_var
- , ic_info = skol_info
- , ic_needed = emptyVarSet
- , ic_env = tc_lcl_env }
- ; emitImplication implic
+
+ -- We must produce bindings for the psig_theta_vars, because we may have
+ -- used them in evidence bindings constructed by solveWanteds earlier
+ -- Easiest way to do this is to emit them as new Wanteds (Trac #14643)
+ ; ct_loc <- getCtLocM AnnOrigin Nothing
+ ; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var
+ , ctev_dest = EvVarDest psig_theta_var
+ , ctev_nosh = WDeriv
+ , ctev_loc = ct_loc }
+ | psig_theta_var <- psig_theta_vars ]
+
+ -- Now construct the residual constraint
+ ; residual_wanted <- mkResidualConstraints rhs_tclvl tc_env ev_binds_var
+ name_taus co_vars qtvs bound_theta_vars
+ (wanted_transformed `andWC` mkSimpleWC psig_wanted)
-- All done!
; traceTc "} simplifyInfer/produced residual implication for quantification" $
vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
, text "psig_theta =" <+> ppr psig_theta
, text "bound_theta =" <+> ppr bound_theta
- , text "full_theta =" <+> ppr full_theta
, text "qtvs =" <+> ppr qtvs
- , text "implic =" <+> ppr implic ]
+ , text "definite_error =" <+> ppr definite_error ]
+
+ ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var
+ , residual_wanted, definite_error ) }
+ -- NB: bound_theta_vars must be fully zonked
+
+
+--------------------
+mkResidualConstraints :: TcLevel -> Env TcGblEnv TcLclEnv -> EvBindsVar
+ -> [(Name, TcTauType)]
+ -> VarSet -> [TcTyVar] -> [EvVar]
+ -> WantedConstraints -> TcM WantedConstraints
+-- Emit the remaining constraints from the RHS.
+-- See Note [Emitting the residual implication in simplifyInfer]
+mkResidualConstraints rhs_tclvl tc_env ev_binds_var
+ name_taus co_vars qtvs full_theta_vars wanteds
+ | isEmptyWC wanteds
+ = return wanteds
- ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var ) }
- -- NB: full_theta_vars must be fully zonked
+ | otherwise
+ = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
+ ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
+ is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
+ ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple)
+ ; let inner_wanted = wanteds { wc_simple = inner_simple }
+ ; return (WC { wc_simple = outer_simple
+ , wc_impl = mk_implic inner_wanted })}
+ where
+ mk_implic inner_wanted
+ | isEmptyWC inner_wanted
+ = emptyBag
+ | otherwise
+ = unitBag (implicationPrototype { ic_tclvl = rhs_tclvl
+ , ic_skols = qtvs
+ , ic_telescope = Nothing
+ , ic_given = full_theta_vars
+ , ic_wanted = inner_wanted
+ , ic_binds = ev_binds_var
+ , ic_no_eqs = False
+ , ic_info = skol_info
+ , ic_env = tc_env })
+
+ full_theta = map idType full_theta_vars
+ skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
+ | (name, ty) <- name_taus ]
+ -- Don't add the quantified variables here, because
+ -- they are also bound in ic_skols and we want them
+ -- to be tidied uniformly
+
+--------------------
ctsPreds :: Cts -> [PredType]
ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
, let ev = ctEvidence ct ]
-{- Note [Add signature contexts as givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Emitting the residual implication in simplifyInfer]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ f = e
+where f's type is inferred to be something like (a, Proxy k (Int |> co))
+and we have an as-yet-unsolved, or perhaps insoluble, constraint
+ [W] co :: Type ~ k
+We can't form types like (forall co. blah), so we can't generalise over
+the coercion variable, and hence we can't generalise over things free in
+its kind, in the case 'k'. But we can still generalise over 'a'. So
+we'll generalise to
+ f :: forall a. (a, Proxy k (Int |> co))
+Now we do NOT want to form the residual implication constraint
+ forall a. [W] co :: Type ~ k
+because then co's eventual binding (which will be a value binding if we
+use -fdefer-type-errors) won't scope over the entire binding for 'f' (whose
+type mentions 'co'). Instead, just as we don't generalise over 'co', we
+should not bury its constraint inside the implication. Instead, we must
+put it outside.
+
+That is the reason for the partitionBag in emitResidualConstraints,
+which takes the CoVars free in the inferred type, and pulls their
+constraints out. (NB: this set of CoVars should be closed-over-kinds.)
+
+All rather subtle; see Trac #14584.
+
+Note [Add signature contexts as givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (Trac #11016):
f2 :: (?x :: Int) => _
f2 = ?x
-> [TcIdSigInst] -- Partial type signatures (if any)
-> [PredType] -- Candidate theta; already zonked
-> TcM ( [TcTyVar] -- Quantify over these (skolems)
- , [PredType] ) -- and this context (fully zonked)
+ , [PredType] -- and this context (fully zonked)
+ , VarSet)
-- See Note [Deciding quantification]
decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
= do { -- Step 1: find the mono_tvs
- ; (mono_tvs, candidates) <- decideMonoTyVars infer_mode
- name_taus psigs candidates
+ ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode
+ name_taus psigs candidates
-- Step 2: default any non-mono tyvars, and re-simplify
-- This step may do some unification, but result candidates is zonked
-- NB: decideQuantifiedTyVars turned some meta tyvars
-- into quantified skolems, so we have to zonk again
; candidates <- TcM.zonkTcTypes candidates
- ; let theta = pickQuantifiablePreds (mkVarSet qtvs) $
- mkMinimalBySCs $ -- See Note [Minimize by Superclasses]
- candidates
+ ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
+ ; let quantifiable_candidates
+ = pickQuantifiablePreds (mkVarSet qtvs) candidates
+ -- NB: do /not/ run pickQuantifiablePreds over psig_theta,
+ -- because we always want to quantify over psig_theta, and not
+ -- drop any of them; e.g. CallStack constraints. c.f Trac #14658
+
+ theta = mkMinimalBySCs id $ -- See Note [Minimize by Superclasses]
+ (psig_theta ++ quantifiable_candidates)
; traceTc "decideQuantification"
- (vcat [ text "infer_mode:" <+> ppr infer_mode
- , text "candidates:" <+> ppr candidates
- , text "mono_tvs:" <+> ppr mono_tvs
- , text "qtvs:" <+> ppr qtvs
- , text "theta:" <+> ppr theta ])
- ; return (qtvs, theta) }
+ (vcat [ text "infer_mode:" <+> ppr infer_mode
+ , text "candidates:" <+> ppr candidates
+ , text "psig_theta:" <+> ppr psig_theta
+ , text "mono_tvs:" <+> ppr mono_tvs
+ , text "co_vars:" <+> ppr co_vars
+ , text "qtvs:" <+> ppr qtvs
+ , text "theta:" <+> ppr theta ])
+ ; return (qtvs, theta, co_vars) }
------------------
decideMonoTyVars :: InferMode
-> [(Name,TcType)]
-> [TcIdSigInst]
-> [PredType]
- -> TcM (TcTyCoVarSet, [PredType])
--- Decide which tyvars cannot be generalised:
+ -> TcM (TcTyCoVarSet, [PredType], CoVarSet)
+-- Decide which tyvars and covars cannot be generalised:
-- (a) Free in the environment
-- (b) Mentioned in a constraint we can't generalise
-- (c) Connected by an equality to (a) or (b)
--- Also return the reduced set of constraint we can generalise
+-- Also return CoVars that appear free in the final quatified types
+-- we can't quantify over these, and we must make sure they are in scope
decideMonoTyVars infer_mode name_taus psigs candidates
- = do { (no_quant, yes_quant) <- pick infer_mode candidates
-
- ; gbl_tvs <- tcGetGlobalTyCoVars
- ; let eq_constraints = filter isEqPred candidates
- mono_tvs1 = growThetaTyVars eq_constraints gbl_tvs
- constrained_tvs = growThetaTyVars eq_constraints (tyCoVarsOfTypes no_quant)
- `minusVarSet` mono_tvs1
- mono_tvs2 = mono_tvs1 `unionVarSet` constrained_tvs
- -- A type variable is only "constrained" (so that the MR bites)
- -- if it is not free in the environment (Trac #13785)
-
- -- Always quantify over partial-sig qtvs, so they are not mono
- -- Need to zonk them because they are meta-tyvar SigTvs
- -- Note [Quantification and partial signatures], wrinkle 3
+ = do { (no_quant, maybe_quant) <- pick infer_mode candidates
+
+ -- If possible, we quantify over partial-sig qtvs, so they are
+ -- not mono. Need to zonk them because they are meta-tyvar SigTvs
; psig_qtvs <- mapM zonkTcTyVarToTyVar $
concatMap (map snd . sig_inst_skols) psigs
- ; let mono_tvs = mono_tvs2 `delVarSetList` psig_qtvs
+
+ ; psig_theta <- mapM TcM.zonkTcType $
+ concatMap sig_inst_theta psigs
+
+ ; taus <- mapM (TcM.zonkTcType . snd) name_taus
+
+ ; mono_tvs0 <- tcGetGlobalTyCoVars
+ ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
+
+ co_vars = coVarsOfTypes (psig_tys ++ taus)
+ co_var_tvs = closeOverKinds co_vars
+ -- The co_var_tvs are tvs mentioned in the types of covars or
+ -- coercion holes. We can't quantify over these covars, so we
+ -- must include the variable in their types in the mono_tvs.
+ -- E.g. If we can't quantify over co :: k~Type, then we can't
+ -- quantify over k either! Hence closeOverKinds
+
+ mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
+
+ eq_constraints = filter isEqPred candidates
+ mono_tvs2 = growThetaTyVars eq_constraints mono_tvs1
+
+ constrained_tvs = (growThetaTyVars eq_constraints
+ (tyCoVarsOfTypes no_quant)
+ `minusVarSet` mono_tvs2)
+ `delVarSetList` psig_qtvs
+ -- constrained_tvs: the tyvars that we are not going to
+ -- quantify solely because of the moonomorphism restriction
+ --
+ -- (`minusVarSet` mono_tvs1`): a type variable is only
+ -- "constrained" (so that the MR bites) if it is not
+ -- free in the environment (Trac #13785)
+ --
+ -- (`delVarSetList` psig_qtvs): if the user has explicitly
+ -- asked for quantification, then that request "wins"
+ -- over the MR. Note: do /not/ delete psig_qtvs from
+ -- mono_tvs1, because mono_tvs1 cannot under any circumstances
+ -- be quantified (Trac #14479); see
+ -- Note [Quantification and partial signatures], Wrinkle 3, 4
+
+ mono_tvs = mono_tvs2 `unionVarSet` constrained_tvs
-- Warn about the monomorphism restriction
; warn_mono <- woptM Opt_WarnMonomorphism
; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
- do { taus <- mapM (TcM.zonkTcType . snd) name_taus
- ; warnTc (Reason Opt_WarnMonomorphism)
- (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
- mr_msg }
+ warnTc (Reason Opt_WarnMonomorphism)
+ (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
+ mr_msg
; traceTc "decideMonoTyVars" $ vcat
- [ text "gbl_tvs =" <+> ppr gbl_tvs
+ [ text "mono_tvs0 =" <+> ppr mono_tvs0
+ , text "mono_tvs1 =" <+> ppr mono_tvs1
, text "no_quant =" <+> ppr no_quant
- , text "yes_quant =" <+> ppr yes_quant
+ , text "maybe_quant =" <+> ppr maybe_quant
, text "eq_constraints =" <+> ppr eq_constraints
- , text "mono_tvs =" <+> ppr mono_tvs ]
+ , text "mono_tvs =" <+> ppr mono_tvs
+ , text "co_vars =" <+> ppr co_vars ]
- ; return (mono_tvs, yes_quant) }
+ ; return (mono_tvs, maybe_quant, co_vars) }
where
pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
-- Split the candidates into ones we definitely
= False
pp_bndrs = pprWithCommas (quotes . ppr . fst) name_taus
- mr_msg = hang (sep [ text "The Monomorphism Restriction applies to the binding"
- <> plural name_taus
- , text "for" <+> pp_bndrs ])
- 2 (hsep [ text "Consider giving"
- , text (if isSingleton name_taus then "it" else "them")
- , text "a type signature"])
+ mr_msg =
+ hang (sep [ text "The Monomorphism Restriction applies to the binding"
+ <> plural name_taus
+ , text "for" <+> pp_bndrs ])
+ 2 (hsep [ text "Consider giving"
+ , text (if isSingleton name_taus then "it" else "them")
+ , text "a type signature"])
-------------------
defaultTyVarsAndSimplify :: TcLevel
defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
= do { -- Promote any tyvars that we cannot generalise
-- See Note [Promote momomorphic tyvars]
- ; outer_tclvl <- TcM.getTcLevel
- ; let prom_tvs = nonDetEltsUniqSet mono_tvs
- -- It's OK to use nonDetEltsUniqSet here
- -- because promoteTyVar is commutative
- ; traceTc "decideMonoTyVars: promotion:" (ppr prom_tvs)
- ; proms <- mapM (promoteTyVar outer_tclvl) prom_tvs
+ ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
+ ; prom <- promoteTyVarSet mono_tvs
-- Default any kind/levity vars
; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
; case () of
_ | some_default -> simplify_cand candidates
- | or proms -> mapM TcM.zonkTcType candidates
+ | prom -> mapM TcM.zonkTcType candidates
| otherwise -> return candidates
}
where
decideQuantifiedTyVars mono_tvs name_taus psigs candidates
= do { -- Why psig_tys? We try to quantify over everything free in here
-- See Note [Quantification and partial signatures]
- -- wrinkles 2 and 3
+ -- Wrinkles 2 and 3
; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
, (_,tv) <- sig_inst_skols sig ]
; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
, pred <- sig_inst_theta sig ]
- ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
+ ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
+ ; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
; let -- Try to quantify over variables free in these types
psig_tys = psig_tv_tys ++ psig_theta
seed_tys = psig_tys ++ tau_tys
-- Now "grow" those seeds to find ones reachable via 'candidates'
- grown_tvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
+ grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
-- Now we have to classify them into kind variables and type variables
-- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars
; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
= candidateQTyVarsOfTypes $
psig_tys ++ candidates ++ tau_tys
- pick = (`dVarSetIntersectVarSet` grown_tvs)
+ pick = (`dVarSetIntersectVarSet` grown_tcvs)
dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
- ; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
+ ; traceTc "decideQuantifiedTyVars" (vcat
+ [ text "seed_tys =" <+> ppr seed_tys
+ , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
+ , text "grown_tcvs =" <+> ppr grown_tcvs])
+
; quantifyTyVars mono_tvs dvs_plus }
------------------
-growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
+growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
-- See Note [Growing the tau-tvs using constraints]
--- NB: only returns tyvars, never covars
-growThetaTyVars theta tvs
- | null theta = tvs_only
- | otherwise = filterVarSet isTyVar $
- transCloVarSet mk_next seed_tvs
+growThetaTyVars theta tcvs
+ | null theta = tcvs
+ | otherwise = transCloVarSet mk_next seed_tcvs
where
- tvs_only = filterVarSet isTyVar tvs
- seed_tvs = tvs `unionVarSet` tyCoVarsOfTypes ips
+ seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
(ips, non_ips) = partition isIPPred theta
-- See Note [Inheriting implicit parameters] in TcType
mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
- grow_one so_far pred tvs
- | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
- | otherwise = tvs
+ grow_one so_far pred tcvs
+ | pred_tcvs `intersectsVarSet` so_far = tcvs `unionVarSet` pred_tcvs
+ | otherwise = tcvs
where
- pred_tvs = tyCoVarsOfType pred
+ pred_tcvs = tyCoVarsOfType pred
+
{- Note [Promote momomorphic tyvars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Wrinkle 3 (Trac #13482). Also consider
f :: forall a. _ => Int -> Int
- f x = if undefined :: a == undefined then x else 0
+ f x = if (undefined :: a) == undefined then x else 0
Here we get an (Eq a) constraint, but it's not mentioned in the
- psig_theta nor the type of 'f'. Moreover, if we have
- f :: forall a. a -> _
- f x = not x
- and a constraint (a ~ g), where 'g' is free in the environment,
- we would not usually quanitfy over 'a'. But here we should anyway
- (leading to a justified subsequent error) since 'a' is explicitly
- quantified by the programmer.
+ psig_theta nor the type of 'f'. But we still want to quantify
+ over 'a' even if the monomorphism restriction is on.
- Bottom line: always quantify over the psig_tvs, regardless.
+* Wrinkle 4 (Trac #14479)
+ foo :: Num a => a -> a
+ foo xxx = g xxx
+ where
+ g :: forall b. Num b => _ -> b
+ g y = xxx + y
+
+ In the signature for 'g', we cannot quantify over 'b' because it turns out to
+ get unified with 'a', which is free in g's environment. So we carefully
+ refrain from bogusly quantifying, in TcSimplify.decideMonoTyVars. We
+ report the error later, in TcBinds.chooseInferredQuantifiers.
Note [Quantifying over equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Quantification with errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we find that the RHS of the definition has some absolutely-insoluble
-constraints, we abandon all attempts to find a context to quantify
-over, and instead make the function fully-polymorphic in whatever
-type we have found. For two reasons
- a) Minimise downstream errors
- b) Avoid spurious errors from this function
-
-But NB that we must include *derived* errors in the check. Example:
+constraints (including especially "variable not in scope"), we
+
+* Abandon all attempts to find a context to quantify over,
+ and instead make the function fully-polymorphic in whatever
+ type we have found
+
+* Return a flag from simplifyInfer, indicating that we found an
+ insoluble constraint. This flag is used to suppress the ambiguity
+ check for the inferred type, which may well be bogus, and which
+ tends to obscure the real error. This fix feels a bit clunky,
+ but I failed to come up with anything better.
+
+Reasons:
+ - Avoid downstream errors
+ - Do not perform an ambiguity test on a bogus type, which might well
+ fail spuriously, thereby obfuscating the original insoluble error.
+ Trac #14000 is an example
+
+I tried an alternative approach: simply failM, after emitting the
+residual implication constraint; the exception will be caught in
+TcBinds.tcPolyBinds, which gives all the binders in the group the type
+(forall a. a). But that didn't work with -fdefer-type-errors, because
+the recovery from failM emits no code at all, so there is no function
+to run! But -fdefer-type-errors aspires to produce a runnable program.
+
+NB that we must include *derived* errors in the check for insolubles.
+Example:
(a::*) ~ Int#
We get an insoluble derived error *~#, and we don't want to discard
it before doing the isInsolubleWC test! (Trac #8262)
solveWanteds :: WantedConstraints -> TcS WantedConstraints
-- so that the inert set doesn't mindlessly propagate.
-- NB: wc_simples may be wanted /or/ derived now
-solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
+solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
= do { traceTcS "solveWanteds {" (ppr wc)
- ; wc1 <- solveSimpleWanteds (simples `unionBags` insols)
- -- Why solve 'insols'? See Note [Rewrite insolubles] in TcSMonad
+ ; wc1 <- solveSimpleWanteds simples
+ -- Any insoluble constraints are in 'simples' and so get rewritten
+ -- See Note [Rewrite insolubles] in TcSMonad
- ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
+ ; (floated_eqs, implics2) <- solveNestedImplications $
+ implics `unionBags` wc_impl wc1
- ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
- ; (no_new_scs, simples2) <- expandSuperClasses simples1
-
- ; traceTcS "solveWanteds middle" $ vcat [ text "simples1 =" <+> ppr simples1
- , text "simples2 =" <+> ppr simples2 ]
-
- ; dflags <- getDynFlags
+ ; dflags <- getDynFlags
; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
- no_new_scs
- (WC { wc_simple = simples2
- , wc_insol = insols1
- , wc_impl = implics2 })
+ (wc1 { wc_impl = implics2 })
- ; bb <- TcS.getTcEvBindsMap
+ ; ev_binds_var <- getTcEvBindsVar
+ ; bb <- TcS.getTcEvBindsMap ev_binds_var
; traceTcS "solveWanteds }" $
vcat [ text "final wc =" <+> ppr final_wc
, text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
; return final_wc }
-simpl_loop :: Int -> IntWithInf -> Cts -> Bool
- -> WantedConstraints
- -> TcS WantedConstraints
-simpl_loop n limit floated_eqs no_new_deriveds
- wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
- | isEmptyBag floated_eqs && no_new_deriveds
- = return wc -- Done!
-
+simpl_loop :: Int -> IntWithInf -> Cts
+ -> WantedConstraints -> TcS WantedConstraints
+simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples })
| n `intGtLimit` limit
= do { -- Add an error (not a warning) if we blow the limit,
-- Typically if we blow the limit we are going to report some other error
2 (vcat [ text "Unsolved:" <+> ppr wc
, ppUnless (isEmptyBag floated_eqs) $
text "Floated equalities:" <+> ppr floated_eqs
- , ppUnless no_new_deriveds $
- text "New deriveds found"
, text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
]))
; return wc }
+ | not (isEmptyBag floated_eqs)
+ = simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples })
+ -- Put floated_eqs first so they get solved first
+ -- NB: the floated_eqs may include /derived/ equalities
+ -- arising from fundeps inside an implication
+
+ | superClassesMightHelp wc
+ = -- We still have unsolved goals, and apparently no way to solve them,
+ -- so try expanding superclasses at this level, both Given and Wanted
+ do { pending_given <- getPendingGivenScs
+ ; let (pending_wanted, simples1) = getPendingWantedScs simples
+ ; if null pending_given && null pending_wanted
+ then return wc -- After all, superclasses did not help
+ else
+ do { new_given <- makeSuperClasses pending_given
+ ; new_wanted <- makeSuperClasses pending_wanted
+ ; solveSimpleGivens new_given -- Add the new Givens to the inert set
+ ; simplify_again n limit (null pending_given)
+ wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
+
| otherwise
- = do { let n_floated = lengthBag floated_eqs
- ; csTraceTcS $
+ = return wc
+
+simplify_again :: Int -> IntWithInf -> Bool
+ -> WantedConstraints -> TcS WantedConstraints
+-- We have definitely decided to have another go at solving
+-- the wanted constraints (we have tried at least once already
+simplify_again n limit no_new_given_scs
+ wc@(WC { wc_simple = simples, wc_impl = implics })
+ = do { csTraceTcS $
text "simpl_loop iteration=" <> int n
- <+> (parens $ hsep [ text "no new deriveds =" <+> ppr no_new_deriveds <> comma
- , int n_floated <+> text "floated eqs" <> comma
+ <+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma
, int (lengthBag simples) <+> text "simples to solve" ])
+ ; traceTcS "simpl_loop: wc =" (ppr wc)
- -- solveSimples may make progress if either float_eqs hold
; (unifs1, wc1) <- reportUnifications $
solveSimpleWanteds $
- floated_eqs `unionBags` simples `unionBags` insols
- -- Notes:
- -- - Why solve 'insols'? See Note [Rewrite insolubles] in TcSMonad
- -- - Put floated_eqs first so they get solved first
- -- NB: the floated_eqs may include /derived/ equalities
- -- arising from fundeps inside an implication
-
- ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
- ; (no_new_scs, simples2) <- expandSuperClasses simples1
+ simples
+ -- See Note [Cutting off simpl_loop]
-- We have already tried to solve the nested implications once
-- Try again only if we have unified some meta-variables
- -- (which is a bit like adding more givens)
- -- See Note [Cutting off simpl_loop]
- ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
- then return (emptyBag, implics)
- else solveNestedImplications (implics `unionBags` implics1)
-
- ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
- (WC { wc_simple = simples2
- , wc_insol = insols1
- , wc_impl = implics2 }) }
-
-
-expandSuperClasses :: Cts -> TcS (Bool, Cts)
--- If there are any unsolved wanteds, expand one step of
--- superclasses for deriveds
--- Returned Bool is True <=> no new superclass constraints added
--- See Note [The superclass story] in TcCanonical
-expandSuperClasses unsolved
- | not (anyBag superClassesMightHelp unsolved)
- = return (True, unsolved)
- | otherwise
- = do { traceTcS "expandSuperClasses {" empty
- ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
- get acc ct | Just ct' <- isPendingScDict ct
- = (ct':acc, ct')
- | otherwise
- = (acc, ct)
- ; pending_given <- getPendingScDicts
- ; if null pending_given && null pending_wanted
- then do { traceTcS "End expandSuperClasses no-op }" empty
- ; return (True, unsolved) }
- else
- do { new_given <- makeSuperClasses pending_given
- ; solveSimpleGivens new_given
- ; new_wanted <- makeSuperClasses pending_wanted
- ; traceTcS "End expandSuperClasses }"
- (vcat [ text "Given:" <+> ppr pending_given
- , text "Wanted:" <+> ppr new_wanted ])
- ; return (False, unsolved' `unionBags` listToBag new_wanted) } }
+ -- (which is a bit like adding more givens), or we have some
+ -- new Given superclasses
+ ; let new_implics = wc_impl wc1
+ ; if unifs1 == 0 &&
+ no_new_given_scs &&
+ isEmptyBag new_implics
+
+ then -- Do not even try to solve the implications
+ simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics })
+
+ else -- Try to solve the implications
+ do { (floated_eqs2, implics2) <- solveNestedImplications $
+ implics `unionBags` new_implics
+ ; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 })
+ } }
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
, ic_given = given_ids
, ic_wanted = wanteds
, ic_info = info
- , ic_status = status
- , ic_env = env })
+ , ic_status = status })
| isSolvedStatus status
= return (emptyCts, Just imp) -- Do nothing
= do { inerts <- getTcSInerts
; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
+ ; when debugIsOn check_tc_level
+
-- Solve the nested constraints
; (no_given_eqs, given_insols, residual_wanted)
<- nestImplicTcS ev_binds_var tclvl $
- do { let loc = mkGivenLoc tclvl info env
+ do { let loc = mkGivenLoc tclvl info (implicLclEnv imp)
givens = mkGivens loc given_ids
; solveSimpleGivens givens
; return (no_eqs, given_insols, residual_wanted) }
; (floated_eqs, residual_wanted)
- <- floatEqualities skols no_given_eqs residual_wanted
+ <- floatEqualities skols given_ids ev_binds_var
+ no_given_eqs residual_wanted
; traceTcS "solveImplication 2"
(ppr given_insols $$ ppr residual_wanted)
; let final_wanted = residual_wanted `addInsols` given_insols
+ -- Don't lose track of the insoluble givens,
+ -- which signal unreachable code; put them in ic_wanted
; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
, ic_wanted = final_wanted })
- ; (evbinds, tcvs) <- TcS.getTcEvBindsAndTCVs ev_binds_var
+ ; evbinds <- TcS.getTcEvBindsMap ev_binds_var
+ ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
; traceTcS "solveImplication end }" $ vcat
[ text "no_given_eqs =" <+> ppr no_given_eqs
, text "floated_eqs =" <+> ppr floated_eqs
; return (floated_eqs, res_implic) }
+ where
+ -- TcLevels must be strictly increasing (see (ImplicInv) in
+ -- Note [TcLevel and untouchable type variables] in TcType),
+ -- and in fact I thinkthey should always increase one level at a time.
+ check_tc_level = do { cur_lvl <- TcS.getTcLevel
+ ; MASSERT2( tclvl == pushTcLevel cur_lvl
+ , text "Cur lvl =" <+> ppr cur_lvl $$
+ text "Imp lvl =" <+> ppr tclvl ) }
+
----------------------
setImplicationStatus :: Implication -> TcS (Maybe Implication)
-- Finalise the implication returned from solveImplication:
-- * Trim the ic_wanted field to remove Derived constraints
-- Precondition: the ic_status field is not already IC_Solved
-- Return Nothing if we can discard the implication altogether
-setImplicationStatus implic@(Implic { ic_binds = ev_binds_var
- , ic_status = status
- , ic_info = info
- , ic_wanted = wc
- , ic_needed = old_discarded_needs
- , ic_given = givens })
+setImplicationStatus implic@(Implic { ic_status = status
+ , ic_info = info
+ , ic_wanted = wc
+ , ic_given = givens })
| ASSERT2( not (isSolvedStatus status ), ppr info )
-- Precondition: we only set the status if it is not already solved
- some_insoluble
- = return $ Just $
- implic { ic_status = IC_Insoluble
- , ic_needed = new_discarded_needs
- , ic_wanted = pruned_wc }
-
- | some_unsolved
- = do { traceTcS "setImplicationStatus" $
- vcat [ppr givens $$ ppr simples $$ ppr insols $$ ppr mb_implic_needs]
- ; return $ Just $
- implic { ic_status = IC_Unsolved
- , ic_needed = new_discarded_needs
- , ic_wanted = pruned_wc }
- }
-
- | otherwise -- Everything is solved; look at the implications
+ not (isSolvedWC pruned_wc)
+ = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)
+
+ ; implic <- neededEvVars implic
+
+ ; let new_status | insolubleWC pruned_wc = IC_Insoluble
+ | otherwise = IC_Unsolved
+ new_implic = implic { ic_status = new_status
+ , ic_wanted = pruned_wc }
+
+ ; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic)
+
+ ; return $ Just new_implic }
+
+ | otherwise -- Everything is solved
+ -- Set status to IC_Solved,
+ -- and compute the dead givens and outer needs
-- See Note [Tracking redundant constraints]
- = do { ev_binds <- TcS.getTcEvBindsAndTCVs ev_binds_var
- ; let all_needs = neededEvVars ev_binds $
- solved_implic_needs `unionVarSet` new_discarded_needs
+ = do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic)
- dead_givens | warnRedundantGivens info
- = filterOut (`elemVarSet` all_needs) givens
- | otherwise = [] -- None to report
+ ; implic@(Implic { ic_need_inner = need_inner
+ , ic_need_outer = need_outer }) <- neededEvVars implic
- final_needs = all_needs `delVarSetList` givens
+ ; bad_telescope <- checkBadTelescope implic
+
+ ; let dead_givens | warnRedundantGivens info
+ = filterOut (`elemVarSet` need_inner) givens
+ | otherwise = [] -- None to report
discard_entire_implication -- Can we discard the entire implication?
= null dead_givens -- No warning from this implication
- && isEmptyBag pruned_implics -- No live children
- && isEmptyVarSet final_needs -- No needed vars to pass up to parent
+ && not bad_telescope
+ && isEmptyWC pruned_wc -- No live children
+ && isEmptyVarSet need_outer -- No needed vars to pass up to parent
- final_status = IC_Solved { ics_need = final_needs
- , ics_dead = dead_givens }
+ final_status
+ | bad_telescope = IC_BadTelescope
+ | otherwise = IC_Solved { ics_dead = dead_givens }
final_implic = implic { ic_status = final_status
- , ic_needed = emptyVarSet -- Irrelevant for IC_Solved
, ic_wanted = pruned_wc }
- -- Check that there are no term-level evidence bindings
- -- in the cases where we have no place to put them
- ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap (fst ev_binds)
- , ppr info $$ ppr ev_binds )
+ ; traceTcS "setImplicationStatus(all-solved) }" $
+ vcat [ text "discard:" <+> ppr discard_entire_implication
+ , text "new_implic:" <+> ppr final_implic ]
- ; traceTcS "setImplicationStatus 2" $
- vcat [ppr givens $$ ppr ev_binds $$ ppr all_needs]
; return $ if discard_entire_implication
then Nothing
else Just final_implic }
where
- WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
-
- some_insoluble = insolubleWC wc
- some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
- || isNothing mb_implic_needs
+ WC { wc_simple = simples, wc_impl = implics } = wc
pruned_simples = dropDerivedSimples simples
- pruned_insols = dropDerivedInsols insols
- (pruned_implics, discarded_needs) = partitionBagWith discard_me implics
- pruned_wc = wc { wc_simple = pruned_simples
- , wc_insol = pruned_insols
+ pruned_implics = filterBag keep_me implics
+ pruned_wc = WC { wc_simple = pruned_simples
, wc_impl = pruned_implics }
- new_discarded_needs = foldrBag unionVarSet old_discarded_needs discarded_needs
-
- mb_implic_needs :: Maybe VarSet
- -- Just vs => all implics are IC_Solved, with 'vs' needed
- -- Nothing => at least one implic is not IC_Solved
- mb_implic_needs = foldrBag add_implic (Just emptyVarSet) pruned_implics
- Just solved_implic_needs = mb_implic_needs
-
- add_implic implic acc
- | Just vs_acc <- acc
- , IC_Solved { ics_need = vs } <- ic_status implic
- = Just (vs `unionVarSet` vs_acc)
- | otherwise = Nothing
-
- discard_me :: Implication -> Either Implication VarSet
- discard_me ic
- | IC_Solved { ics_dead = dead_givens, ics_need = needed } <- ic_status ic
+
+ keep_me :: Implication -> Bool
+ keep_me ic
+ | IC_Solved { ics_dead = dead_givens } <- ic_status ic
-- Fully solved
, null dead_givens -- No redundant givens to report
, isEmptyBag (wc_impl (ic_wanted ic))
-- And no children that might have things to report
- = Right needed
+ = False -- Tnen we don't need to keep it
| otherwise
- = Left ic
+ = True -- Otherwise, keep it
+
+checkBadTelescope :: Implication -> TcS Bool
+-- True <=> the skolems form a bad telescope
+-- See Note [Keeping scoped variables in order: Explicit] in TcHsType
+checkBadTelescope (Implic { ic_telescope = m_telescope
+ , ic_skols = skols })
+ | isJust m_telescope
+ = do{ skols <- mapM TcS.zonkTcTyCoVarBndr skols
+ ; return (go emptyVarSet (reverse skols))}
+
+ | otherwise
+ = return False
+
+ where
+ go :: TyVarSet -- skolems that appear *later* than the current ones
+ -> [TcTyVar] -- ordered skolems, in reverse order
+ -> Bool -- True <=> there is an out-of-order skolem
+ go _ [] = False
+ go later_skols (one_skol : earlier_skols)
+ | tyCoVarsOfType (tyVarKind one_skol) `intersectsVarSet` later_skols
+ = True
+ | otherwise
+ = go (later_skols `extendVarSet` one_skol) earlier_skols
warnRedundantGivens :: SkolemInfo -> Bool
warnRedundantGivens (SigSkol ctxt _ _)
warnRedundantGivens (InstSkol {}) = True
warnRedundantGivens _ = False
-neededEvVars :: (EvBindMap, TcTyVarSet) -> VarSet -> VarSet
+neededEvVars :: Implication -> TcS Implication
-- Find all the evidence variables that are "needed",
--- and then delete all those bound by the evidence bindings
--- See Note [Tracking redundant constraints]
-neededEvVars (ev_binds, tcvs) initial_seeds
- = (needed `unionVarSet` tcvs) `minusVarSet` bndrs
+-- and delete dead evidence bindings
+-- See Note [Tracking redundant constraints]
+-- See Note [Delete dead Given evidence bindings]
+--
+-- - Start from initial_seeds (from nested implications)
+--
+-- - Add free vars of RHS of all Wanted evidence bindings
+-- and coercion variables accumulated in tcvs (all Wanted)
+--
+-- - Generate 'needed', the needed set of EvVars, by doing transitive
+-- closure through Given bindings
+-- e.g. Needed {a,b}
+-- Given a = sc_sel a2
+-- Then a2 is needed too
+--
+-- - Prune out all Given bindings that are not needed
+--
+-- - From the 'needed' set, delete ev_bndrs, the binders of the
+-- evidence bindings, to give the final needed variables
+--
+neededEvVars implic@(Implic { ic_given = givens
+ , ic_binds = ev_binds_var
+ , ic_wanted = WC { wc_impl = implics }
+ , ic_need_inner = old_needs })
+ = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
+ ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
+
+ ; let seeds1 = foldrBag add_implic_seeds old_needs implics
+ seeds2 = foldEvBindMap add_wanted seeds1 ev_binds
+ seeds3 = seeds2 `unionVarSet` tcvs
+ need_inner = findNeededEvVars ev_binds seeds3
+ live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
+ need_outer = foldEvBindMap del_ev_bndr need_inner live_ev_binds
+ `delVarSetList` givens
+
+ ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds
+ -- See Note [Delete dead Given evidence bindings]
+
+ ; traceTcS "neededEvVars" $
+ vcat [ text "old_needs:" <+> ppr old_needs
+ , text "seeds3:" <+> ppr seeds3
+ , text "ev_binds:" <+> ppr ev_binds
+ , text "live_ev_binds:" <+> ppr live_ev_binds ]
+
+ ; return (implic { ic_need_inner = need_inner
+ , ic_need_outer = need_outer }) }
where
- seeds = foldEvBindMap add_wanted initial_seeds ev_binds
- needed = transCloVarSet also_needs seeds
- bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds
+ add_implic_seeds (Implic { ic_need_outer = needs, ic_given = givens }) acc
+ = (needs `delVarSetList` givens) `unionVarSet` acc
+
+ needed_ev_bind needed (EvBind { eb_lhs = ev_var
+ , eb_is_given = is_given })
+ | is_given = ev_var `elemVarSet` needed
+ | otherwise = True -- Keep all wanted bindings
+
+ del_ev_bndr :: EvBind -> VarSet -> VarSet
+ del_ev_bndr (EvBind { eb_lhs = v }) needs = delVarSet needs v
add_wanted :: EvBind -> VarSet -> VarSet
add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
| is_given = needs -- Add the rhs vars of the Wanted bindings only
| otherwise = evVarsOfTerm rhs `unionVarSet` needs
- also_needs :: VarSet -> VarSet
- also_needs needs
- = nonDetFoldUniqSet add emptyVarSet needs
- -- It's OK to use nonDetFoldUFM here because we immediately forget
- -- about the ordering by creating a set
- where
- add v needs
- | Just ev_bind <- lookupEvBind ev_binds v
- , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
- , is_given
- = evVarsOfTerm rhs `unionVarSet` needs
- | otherwise
- = needs
- add_bndr :: EvBind -> VarSet -> VarSet
- add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
+{- Note [Delete dead Given evidence bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As a result of superclass expansion, we speculatively
+generate evidence bindings for Givens. E.g.
+ f :: (a ~ b) => a -> b -> Bool
+ f x y = ...
+We'll have
+ [G] d1 :: (a~b)
+and we'll specuatively generate the evidence binding
+ [G] d2 :: (a ~# b) = sc_sel d
+Now d2 is available for solving. But it may not be needed! Usually
+such dead superclass selections will eventually be dropped as dead
+code, but:
+
+ * It won't always be dropped (Trac #13032). In the case of an
+ unlifted-equality superclass like d2 above, we generate
+ case heq_sc d1 of d2 -> ...
+ and we can't (in general) drop that case exrpession in case
+ d1 is bottom. So it's technically unsound to have added it
+ in the first place.
+
+ * Simply generating all those extra superclasses can generate lots of
+ code that has to be zonked, only to be discarded later. Better not
+ to generate it in the first place.
+
+ Moreover, if we simplify this implication more than once
+ (e.g. because we can't solve it completely on the first iteration
+ of simpl_looop), we'll generate all the same bindings AGAIN!
+
+Easy solution: take advantage of the work we are doing to track dead
+(unused) Givens, and use it to prune the Given bindings too. This is
+all done by neededEvVars.
+
+This led to a remarkable 25% overall compiler allocation decrease in
+test T12227.
-{-
Note [Tracking redundant constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With Opt_WarnRedundantConstraints, GHC can report which
----- How tracking works
+* The ic_need fields of an Implic records in-scope (given) evidence
+ variables bound by the context, that were needed to solve this
+ implication (so far). See the declaration of Implication.
+
* When the constraint solver finishes solving all the wanteds in
an implication, it sets its status to IC_Solved
- The ics_dead field, of IC_Solved, records the subset of this
implication's ic_given that are redundant (not needed).
- - The ics_need field of IC_Solved then records all the
- in-scope (given) evidence variables bound by the context, that
- were needed to solve this implication, including all its nested
- implications. (We remove the ic_given of this implication from
- the set, of course.)
-
* We compute which evidence variables are needed by an implication
in setImplicationStatus. A variable is needed if
a) it is free in the RHS of a Wanted EvBind,
allow the implication to make progress.
-}
-promoteTyVar :: TcLevel -> TcTyVar -> TcM Bool
+promoteTyVar :: TcTyVar -> TcM Bool
-- When we float a constraint out of an implication we must restore
--- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
+-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
-- Return True <=> we did some promotion
-- See Note [Promoting unification variables]
-promoteTyVar tclvl tv
- | isFloatedTouchableMetaTyVar tclvl tv
- = do { cloned_tv <- TcM.cloneMetaTyVar tv
- ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
- ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
- ; return True }
- | otherwise
- = return False
-
-promoteTyVarTcS :: TcLevel -> TcTyVar -> TcS ()
+promoteTyVar tv
+ = do { tclvl <- TcM.getTcLevel
+ ; if (isFloatedTouchableMetaTyVar tclvl tv)
+ then do { cloned_tv <- TcM.cloneMetaTyVar tv
+ ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+ ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
+ ; return True }
+ else return False }
+
+-- Returns whether or not *any* tyvar is defaulted
+promoteTyVarSet :: TcTyVarSet -> TcM Bool
+promoteTyVarSet tvs
+ = or <$> mapM promoteTyVar (nonDetEltsUniqSet tvs)
+ -- non-determinism is OK because order of promotion doesn't matter
+
+promoteTyVarTcS :: TcTyVar -> TcS ()
-- When we float a constraint out of an implication we must restore
--- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
+-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
-- See Note [Promoting unification variables]
-- We don't just call promoteTyVar because we want to use unifyTyVar,
-- not writeMetaTyVar
-promoteTyVarTcS tclvl tv
- | isFloatedTouchableMetaTyVar tclvl tv
- = do { cloned_tv <- TcS.cloneMetaTyVar tv
- ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
- ; unifyTyVar tv (mkTyVarTy rhs_tv) }
- | otherwise
- = return ()
+promoteTyVarTcS tv
+ = do { tclvl <- TcS.getTcLevel
+ ; when (isFloatedTouchableMetaTyVar tclvl tv) $
+ do { cloned_tv <- TcS.cloneMetaTyVar tv
+ ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+ ; unifyTyVar tv (mkTyVarTy rhs_tv) } }
-- | Like 'defaultTyVar', but in the TcS monad.
defaultTyVarTcS :: TcTyVar -> TcS Bool
defaultTyVarTcS the_tv
| isRuntimeRepVar the_tv
+ , not (isSigTyVar the_tv) -- SigTvs should only be unified with a tyvar
+ -- never with a type; c.f. TcMType.defaultTyVar
+ -- See Note [Kind generalisation and SigTvs]
= do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
; unifyTyVar the_tv liftedRepTy
; return True }
where
float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
- = filterBag is_floatable simples `unionBags`
+ = filterBag (is_floatable trapping_tvs) simples `unionBags`
do_bag (float_implic trapping_tvs) implics
where
- is_floatable ct = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs
float_implic :: TcTyCoVarSet -> Implication -> Cts
float_implic trapping_tvs imp
= emptyCts -- See (1) under Note [ApproximateWC]
where
new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
+
do_bag :: (a -> Bag c) -> Bag a -> Bag c
do_bag f = foldrBag (unionBags.f) emptyBag
+ is_floatable skol_tvs ct
+ | isGivenCt ct = False
+ | isHoleCt ct = False
+ | insolubleEqCt ct = False
+ | otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+
{- Note [ApproximateWC]
~~~~~~~~~~~~~~~~~~~~~~~
approximateWC takes a constraint, typically arising from the RHS of a
approximateWC to produce a list of candidate constraints. Then we MUST
a) Promote any meta-tyvars that have been floated out by
- approximateWC, to restore invariant (MetaTvInv) described in
+ approximateWC, to restore invariant (WantedInv) described in
Note [TcLevel and untouchable type variables] in TcType.
b) Default the kind of any meta-tyvars that are not mentioned in
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we float an equality out of an implication we must "promote" free
unification variables of the equality, in order to maintain Invariant
-(MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
-leftover implication.
+(WantedInv) from Note [TcLevel and untouchable type variables] in
+TcType. for the leftover implication.
This is absolutely necessary. Consider the following example. We start
with two implications and a class with a functional dependency.
they carry evidence).
-}
-floatEqualities :: [TcTyVar] -> Bool
+floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool
-> WantedConstraints
-> TcS (Cts, WantedConstraints)
-- Main idea: see Note [Float Equalities out of Implications]
--
-- Subtleties: Note [Float equalities from under a skolem binding]
-- Note [Skolem escape]
-floatEqualities skols no_given_eqs
+-- Note [What prevents a constraint from floating]
+floatEqualities skols given_ids ev_binds_var no_given_eqs
wanteds@(WC { wc_simple = simples })
| not no_given_eqs -- There are some given equalities, so don't float
= return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
-- variables, and we /must/ see them. Otherwise we may float
-- constraints that mention the skolems!
simples <- TcS.zonkSimples simples
+ ; binds <- TcS.getTcEvBindsMap ev_binds_var
-- Now we can pick the ones to float
- ; let (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
- skol_set = mkVarSet skols
+ -- The constraints are un-flattened and de-canonicalised
+ ; let seed_skols = mkVarSet skols `unionVarSet`
+ mkVarSet given_ids `unionVarSet`
+ foldEvBindMap add_one emptyVarSet binds
+ add_one bind acc = extendVarSet acc (evBindVar bind)
+ -- seed_skols: See Note [What prevents a constraint from floating] (1,2,3)
+
+ (eqs, non_eqs) = partitionBag is_eq_ct simples
+ extended_skols = transCloVarSet (extra_skols eqs) seed_skols
+ (flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols) eqs
+ remaining_simples = non_eqs `andCts` no_flt_eqs
+ -- extended_skols: See Note [What prevents a constraint from floating] (3)
-- Promote any unification variables mentioned in the floated equalities
-- See Note [Promoting unification variables]
- ; outer_tclvl <- TcS.getTcLevel
- ; mapM_ (promoteTyVarTcS outer_tclvl)
- (tyCoVarsOfCtsList float_eqs)
+ ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs)
; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
+ , text "Extended skols =" <+> ppr extended_skols
, text "Simples =" <+> ppr simples
- , text "Floated eqs =" <+> ppr float_eqs])
- ; return ( float_eqs
- , wanteds { wc_simple = remaining_simples } ) }
-
-usefulToFloat :: VarSet -> Ct -> Bool
-usefulToFloat skol_set ct -- The constraint is un-flattened and de-canonicalised
- = is_meta_var_eq pred &&
- (tyCoVarsOfType pred `disjointVarSet` skol_set)
+ , text "Eqs =" <+> ppr eqs
+ , text "Floated eqs =" <+> ppr flt_eqs])
+ ; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) }
+
where
- pred = ctPred ct
+ is_floatable :: VarSet -> Ct -> Bool
+ is_floatable skols ct
+ | isDerivedCt ct = not (tyCoVarsOfCt ct `intersectsVarSet` skols)
+ | otherwise = not (ctEvId ct `elemVarSet` skols)
+
+ is_eq_ct ct | CTyEqCan {} <- ct = True
+ | is_homo_eq (ctPred ct) = True
+ | otherwise = False
+
+ extra_skols :: Cts -> VarSet -> VarSet
+ extra_skols eqs skols = foldrBag extra_skol emptyVarSet eqs
+ where
+ extra_skol ct acc
+ | isDerivedCt ct = acc
+ | tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct)
+ | otherwise = acc
-- Float out alpha ~ ty, or ty ~ alpha
-- which might be unified outside
-- See Note [Which equalities to float]
- is_meta_var_eq pred
+ is_homo_eq pred
| EqPred NomEq ty1 ty2 <- classifyPredType pred
+ , typeKind ty1 `tcEqType` typeKind ty2
= case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
(Just tv1, _) -> float_tv_eq tv1 ty2
(_, Just tv2) -> float_tv_eq tv2 ty1
= isMetaTyVar tv1
&& (not (isSigTyVar tv1) || isTyVarTy ty2)
+
{- Note [Float equalities from under a skolem binding]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Which of the simple equalities can we float out? Obviously, only
is a decent chance that floating outwards will allow unification to
happen. In particular:
- Float out equalities of form (alpha ~ ty) or (ty ~ alpha), where
+ Float out homogeneous equalities of form (alpha ~ ty) or (ty ~ alpha), where
* alpha is a meta-tyvar.
case, floating out won't help either, and it may affect grouping
of error messages.
+Why homogeneous (i.e., the kinds of the types are the same)? Because heterogeneous
+equalities have derived kind equalities. See Note [Equalities with incompatible kinds]
+in TcCanonical. If we float out a hetero equality, then it will spit out the
+same derived kind equality again, which might create duplicate error messages.
+Instead, we do float out the kind equality (if it's worth floating out, as
+above). If/when we solve it, we'll be able to rewrite the original hetero equality
+to be homogeneous, and then perhaps make progress / float it out. The duplicate
+error message was spotted in typecheck/should_fail/T7368.
+
Note [Skolem escape]
~~~~~~~~~~~~~~~~~~~~
You might worry about skolem escape with all this floating.
But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
+Note [What prevents a constraint from floating]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What /prevents/ a constraint from floating? If it mentions one of the
+"bound variables of the implication". What are they?
+
+The "bound variables of the implication" are
+
+ 1. The skolem type variables `ic_skols`
+
+ 2. The "given" evidence variables `ic_given`. Example:
+ forall a. (co :: t1 ~# t2) => [W] co : (a ~# b |> co)
+
+ 3. The binders of all evidence bindings in `ic_binds`. Example
+ forall a. (d :: t1 ~ t2)
+ EvBinds { (co :: t1 ~# t2) = superclass-sel d }
+ => [W] co2 : (a ~# b |> co)
+ Here `co` is gotten by superclass selection from `d`, and the
+ wanted constraint co2 must not float.
+
+ 4. And the evidence variable of any equality constraint (incl
+ Wanted ones) whose type mentions a bound variable. Example:
+ forall k. [W] co1 :: t1 ~# t2 |> co2
+ [W] co2 :: k ~# *
+ Here, since `k` is bound, so is `co2` and hence so is `co1`.
+
+Here (1,2,3) are handled by the "seed_skols" calculation, and
+(4) is done by the transCloVarSet call.
+
+The possible dependence on givens, and evidence bindings, is more
+subtle than we'd realised at first. See Trac #14584.
+
*********************************************************************************
* *
= []
| otherwise
= [ (tv, map fstOf3 group)
- | group@((_,_,tv):_) <- unary_groups
+ | group'@((_,_,tv) :| _) <- unary_groups
+ , let group = toList group'
, defaultable_tyvar tv
, defaultable_classes (map sndOf3 group) ]
where
(unaries, non_unaries) = partitionWith find_unary (bagToList simples)
unary_groups = equivClasses cmp_tv unaries
- unary_groups :: [[(Ct, Class, TcTyVar)]] -- (C tv) constraints
- unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
- non_unaries :: [Ct] -- and *other* constraints
+ unary_groups :: [NonEmpty (Ct, Class, TcTyVar)] -- (C tv) constraints
+ unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
+ non_unaries :: [Ct] -- and *other* constraints
-- Finds unary type-class constraints
-- But take account of polykinded classes like Typeable,
try_group
| Just subst <- mb_subst
= do { lcl_env <- TcS.getLclEnv
- ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
- , ctl_env = lcl_env
- , ctl_t_or_k = Nothing
- , ctl_depth = initialSubGoalDepth }
+ ; tc_lvl <- TcS.getTcLevel
+ ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
wanteds
; fmap isEmptyWC $
git.haskell.org / ghc.git / blobdiff