simplifyAmbiguityCheck,
simplifyDefault,
simplifyTop, simplifyTopImplic, captureTopConstraints,
- simplifyInteractive, solveSomeEqualities, 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 ErrUtils ( emptyMessages )
import qualified GHC.LanguageExtensions as LangExt
-import Control.Monad ( when, unless )
-import Data.List ( partition )
+import Control.Monad
+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) }
-{- Note [solveEqualities vs solveSomeEqualities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When kind-checking a type, GHC might generate equality constraints. (We know
-it will generate only *equalities*, not e.g. class constraints, because types
-don't contain class methods.) What should we do with these constraints?
-Before we can effectively zonk, generalize, or validity-check a type, we need
-to solve these equalities. The functions solveEqualities and solveSomeEqualities
-do precisely this.
-
-solveEqualities solves *all* equality constraints generated by the thing_inside.
-If any constraints are unable to be solved, fail. This is appropriate for a top-
-level type where we absolutely must, say, generalize right away. For example,
-in
-
- data G (a :: k) where
- MkG :: G Maybe
-
-The type G Maybe will make equality constraints that must be handled pronto.
-
-solveSomeEqualities, on the other hand, does the best it can, re-emitting those
-constraints it can't solve. This is appropriate when, for example, a type
-appears in the middle of an expression (either a type annotation or a visible
-type application) and there may be givens that have a bearing on whether or
-not a type-level equality is soluble. The use of solveEqualities in an type
-annotation is what gave rise to #13337.
-
-Why have solveSomeEqualities at all, instead of just letting all equality
-constraints go where all the other constraints do? Because we want to nail what
-equalities we can before doing validity checking. Otherwise, the validity checker
-may see casts and other nonsense in what should be a simple type.
-
-How to choose between these?
-
-Use solveEqualities when any of the following apply:
- * you are about to kind-generalize
- * you are about to call zonkTcTypeToType
- * you are in a top-level context, not inside of any expression
-
-Use solveSomeEqualities when:
- * none of the above applies
--}
+-- | 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
--- | Type-check a thing that emits only equality constraints, then
--- solve as many constraints as possible. Re-emits any unsolved constraints.
--- Never fails. This is useful when you're in a context where emitting
--- constraints is a good idea (e.g., in a expression type signature) but
--- you also want to use a function from TcValidity. TcValidity wants the
--- type to be as well-defined as possible. So this does what it can.
--- See also Note [solveEqualities vs solveSomeEqualities]
-solveSomeEqualities :: TcM a -> TcM a
-solveSomeEqualities thing_inside
- = do { (result, wanted) <- captureConstraints thing_inside
- ; traceTc "solveSomeEqualities {" $ text "wanted = " <+> ppr wanted
- ; final_wc <- runTcSEqualities $ simpl_top wanted
- ; traceTc "End solveESomequalities }" 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 final_wc
+ ; 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.
--- See also Note [solveEqualities vs solveSomeEqualities]
+-- 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 <- quantifyZonkedTyVars gbl_tvs dep_vars
+ ; 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]
; solveWanteds wanteds }
- ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
-- 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
- <- if insolubleWC wanted_transformed_incl_derivs
- then return [] -- See Note [Quantification with errors]
- -- NB: must include derived errors in this test,
- -- hence "incl_derivs"
-
- else do { let quant_cand = approximateWC False wanted_transformed
- meta_tvs = filter isMetaTyVar $
- tyCoVarsOfCtsList quant_cand
-
- ; gbl_tvs <- tcGetGlobalTyCoVars
- -- Miminise quant_cand. We are not interested in any evidence
- -- produced, because we are going to simplify wanted_transformed
- -- again later. All we want here are the predicates over which to
- -- quantify.
- --
- -- If any meta-tyvar unifications take place (unlikely),
- -- we'll pick that up later.
-
- -- See Note [Promote _and_ default when inferring]
- ; let def_tyvar tv
- = when (not $ tv `elemVarSet` gbl_tvs) $
- defaultTyVar tv
- ; mapM_ def_tyvar meta_tvs
- ; mapM_ (promoteTyVar rhs_tclvl) meta_tvs
-
- ; clone_wanteds <- mapM cloneWanted (bagToList quant_cand)
- ; WC { wc_simple = simples }
- <- setTcLevel rhs_tclvl $
- simplifyWantedsTcM clone_wanteds
- -- Discard evidence; result is zonked
-
- ; return [ ctEvPred ev | ct <- bagToList simples
- , let ev = ctEvidence ct ] }
-
- -- 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 name_taus psig_theta
+ -- 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
-
- -- 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]
- -- constraints = 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
- ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
- -- decideQuantification turned some meta tyvars into
- -- quantified skolems, so we have to zonk again
-
- ; let phi_tkvs = tyCoVarsOfTypes bound_theta -- Already zonked
- `unionVarSet` tyCoVarsOfTypes zonked_taus
- promote_tkvs = closeOverKinds phi_tkvs `delVarSetList` qtvs
-
- ; MASSERT2( closeOverKinds promote_tkvs `subVarSet` promote_tkvs
- , ppr phi_tkvs $$
- ppr (closeOverKinds phi_tkvs) $$
- ppr promote_tkvs $$
- ppr (closeOverKinds promote_tkvs) )
- -- we really don't want a type to be promoted when its kind isn't!
-
- -- promoteTyVar ignores coercion variables
- ; outer_tclvl <- TcM.getTcLevel
- ; mapM_ (promoteTyVar outer_tclvl) (nonDetEltsUniqSet promote_tkvs)
- -- It's OK to use nonDetEltsUniqSet here because promoteTyVar is
- -- commutative
-
- -- Emit an implication constraint for the
- -- remaining constraints from the RHS
- -- extra_qtvs: see Note [Quantification and partial signatures]
; bound_theta_vars <- mapM TcM.newEvVar bound_theta
- ; psig_theta_vars <- mapM zonkId psig_theta_vars
- ; all_qtvs <- add_psig_tvs qtvs
- [ tv | sig <- partial_sigs
- , (_,tv) <- sig_inst_skols sig ]
-
- ; 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 = all_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 "promote_tvs=" <+> ppr promote_tkvs
, text "psig_theta =" <+> ppr psig_theta
, text "bound_theta =" <+> ppr bound_theta
- , text "full_theta =" <+> ppr full_theta
- , text "all_qtvs =" <+> ppr all_qtvs
- , text "implic =" <+> ppr implic ]
+ , text "qtvs =" <+> ppr qtvs
+ , 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
+
+ | 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)
- ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var ) }
+ ; let inner_wanted = wanteds { wc_simple = inner_simple }
+ ; return (WC { wc_simple = outer_simple
+ , wc_impl = mk_implic inner_wanted })}
where
- add_psig_tvs qtvs [] = return qtvs
- add_psig_tvs qtvs (tv:tvs)
- = do { tv <- zonkTcTyVarToTyVar tv
- ; if tv `elem` qtvs
- then add_psig_tvs qtvs tvs
- else do { mb_tv <- zonkQuantifiedTyVar False tv
- ; case mb_tv of
- Nothing -> add_psig_tvs qtvs tvs
- Just tv -> add_psig_tvs (tv:qtvs) tvs } }
-
-{- Note [Add signature contexts as givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ 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 [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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the monomorphism restriction does not apply, then we quantify as follows:
- * Take the global tyvars, and "grow" them using the equality constraints
- E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
+* Step 1. Take the global tyvars, and "grow" them using the equality
+ constraints
+ E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
happen because alpha is untouchable here) then do not quantify over
beta, because alpha fixes beta, and beta is effectively free in
the environment too
- These are the mono_tvs
- * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
- using all the constraints. These are tau_tvs_plus
+ We also account for the monomorphism restriction; if it applies,
+ add the free vars of all the constraints.
+
+ Result is mono_tvs; we will not quantify over these.
- * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
+* Step 2. Default any non-mono tyvars (i.e ones that are definitely
+ not going to become further constrained), and re-simplify the
+ candidate constraints.
+
+ Motivation for re-simplification (Trac #7857): imagine we have a
+ constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
+ not free in the envt, and instance forall (a::*) (b::*). (C a) => C
+ (a -> b) The instance doesn't match while l1,l2 are polymorphic, but
+ it will match when we default them to LiftedRep.
+
+ This is all very tiresome.
+
+* Step 3: decide which variables to quantify over, as follows:
+
+ - Take the free vars of the tau-type (zonked_tau_tvs) and "grow"
+ them using all the constraints. These are tau_tvs_plus
+
+ - Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
careful to close over kinds, and to skolemise the quantified tyvars.
(This actually unifies each quantifies meta-tyvar with a fresh skolem.)
- Result is qtvs.
- * Filter the constraints using pickQuantifiablePreds and the qtvs.
- We have to zonk the constraints first, so they "see" the freshly
- created skolems.
+ Result is qtvs.
-If the MR does apply, mono_tvs includes all the constrained tyvars --
-including all covars -- and the quantified constraints are empty/insoluble.
+* Step 4: Filter the constraints using pickQuantifiablePreds and the
+ qtvs. We have to zonk the constraints first, so they "see" the
+ freshly created skolems.
-}
decideQuantification
:: InferMode
+ -> TcLevel
-> [(Name, TcTauType)] -- Variables to be generalised
- -> [PredType] -- All annotated constraints from signatures
+ -> [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 name_taus psig_theta candidates
- = do { ovl_strings <- xoptM LangExt.OverloadedStrings
- ; gbl_tvs <- tcGetGlobalTyCoVars
- ; let (gbl_cand, quant_cand) -- gbl_cand = do not quantify me
- = case infer_mode of -- quant_cand = try to quantify me
- ApplyMR -> (candidates, [])
- NoRestrictions -> ([], candidates)
- EagerDefaulting -> partition is_interactive_ct candidates
- where
- is_interactive_ct ct
- | Just (cls, _) <- getClassPredTys_maybe ct
- = isInteractiveClass ovl_strings cls
- | otherwise
- = False
-
- eq_constraints = filter isEqPred quant_cand
- constrained_tvs = tyCoVarsOfTypes gbl_cand
- mono_tvs = growThetaTyVars eq_constraints $
- gbl_tvs `unionVarSet` constrained_tvs
-
- ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
- -- psig_theta: see Note [Quantification and partial signatures]
-
- ; let -- The candidate tyvars are the ones free in
- -- either quant_cand or zonked_taus.
- DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
- = candidateQTyVarsOfTypes (quant_cand ++ zonked_taus)
-
- -- Now keep only the ones reachable
- -- (via growThetaTyVars) from zonked_taus.
- grown_tvs = growThetaTyVars quant_cand (tyCoVarsOfTypes zonked_taus)
- pick = filterDVarSet (`elemVarSet` grown_tvs)
- dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
-
- ; qtvs <- quantifyZonkedTyVars mono_tvs dvs_plus
- -- We don't grow the kvs, as there's no real need to. Recall
- -- that quantifyTyVars uses the separation between kvs and tvs
- -- only for defaulting, and we don't want (ever) to default a tv
- -- to *. So, don't grow the kvs.
-
- ; quant_cand <- TcM.zonkTcTypes quant_cand
- -- quantifyTyVars turned some meta tyvars into
- -- quantified skolems, so we have to zonk again
-
- ; let qtv_set = mkVarSet qtvs
- theta = pickQuantifiablePreds qtv_set quant_cand
- min_theta = mkMinimalBySCs theta
- -- See Note [Minimize by Superclasses]
+decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
+ = do { -- Step 1: find the mono_tvs
+ ; (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
+ ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+
+ -- Step 3: decide which kind/type variables to quantify over
+ ; qtvs <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+
+ -- Step 4: choose which of the remaining candidate
+ -- predicates to actually quantify over
+ -- NB: decideQuantifiedTyVars turned some meta tyvars
+ -- into quantified skolems, so we have to zonk again
+ ; candidates <- TcM.zonkTcTypes 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 "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], 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 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, 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
+
+ ; 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
- ; let mr_bites | ApplyMR <- infer_mode
- = constrained_tvs `intersectsVarSet` grown_tvs
- | otherwise
- = False
- ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
- hang (text "The Monomorphism Restriction applies to the binding"
- <> plural bndrs <+> text "for" <+> pp_bndrs)
- 2 (text "Consider giving a type signature for"
- <+> if isSingleton bndrs then pp_bndrs
- else text "these binders")
+ ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
+ warnTc (Reason Opt_WarnMonomorphism)
+ (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
+ mr_msg
+
+ ; traceTc "decideMonoTyVars" $ vcat
+ [ text "mono_tvs0 =" <+> ppr mono_tvs0
+ , text "mono_tvs1 =" <+> ppr mono_tvs1
+ , text "no_quant =" <+> ppr no_quant
+ , text "maybe_quant =" <+> ppr maybe_quant
+ , text "eq_constraints =" <+> ppr eq_constraints
+ , text "mono_tvs =" <+> ppr mono_tvs
+ , text "co_vars =" <+> ppr co_vars ]
+
+ ; return (mono_tvs, maybe_quant, co_vars) }
+ where
+ pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
+ -- Split the candidates into ones we definitely
+ -- won't quantify, and ones that we might
+ pick NoRestrictions cand = return ([], cand)
+ pick ApplyMR cand = return (cand, [])
+ pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings
+ ; return (partition (is_int_ct os) cand) }
+
+ -- For EagerDefaulting, do not quantify over
+ -- over any interactive class constraint
+ is_int_ct ovl_strings pred
+ | Just (cls, _) <- getClassPredTys_maybe pred
+ = isInteractiveClass ovl_strings cls
+ | otherwise
+ = False
- ; traceTc "decideQuantification"
- (vcat [ text "infer_mode:" <+> ppr infer_mode
- , text "gbl_cand:" <+> ppr gbl_cand
- , text "quant_cand:" <+> ppr quant_cand
- , text "zonked_taus:" <+> ppr zonked_taus
- , text "gbl_tvs:" <+> ppr gbl_tvs
- , text "mono_tvs:" <+> ppr mono_tvs
- , text "cand_tvs" <+> ppr cand_tvs
- , text "grown_tvs:" <+> ppr grown_tvs
- , text "qtvs:" <+> ppr qtvs
- , text "min_theta:" <+> ppr min_theta ])
- ; return (qtvs, min_theta) }
+ 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"])
+
+-------------------
+defaultTyVarsAndSimplify :: TcLevel
+ -> TyCoVarSet
+ -> [PredType] -- Assumed zonked
+ -> TcM [PredType] -- Guaranteed zonked
+-- Default any tyvar free in the constraints,
+-- and re-simplify in case the defaulting allows further simplification
+defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+ = do { -- Promote any tyvars that we cannot generalise
+ -- See Note [Promote momomorphic tyvars]
+ ; 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}
+ = candidateQTyVarsOfTypes candidates
+ ; poly_kinds <- xoptM LangExt.PolyKinds
+ ; default_kvs <- mapM (default_one poly_kinds True)
+ (dVarSetElems cand_kvs)
+ ; default_tvs <- mapM (default_one poly_kinds False)
+ (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
+ ; let some_default = or default_kvs || or default_tvs
+
+ ; case () of
+ _ | some_default -> simplify_cand candidates
+ | prom -> mapM TcM.zonkTcType candidates
+ | otherwise -> return candidates
+ }
where
- pp_bndrs = pprWithCommas (quotes . ppr) bndrs
- (bndrs, taus) = unzip name_taus
+ default_one poly_kinds is_kind_var tv
+ | not (isMetaTyVar tv)
+ = return False
+ | tv `elemVarSet` mono_tvs
+ = return False
+ | otherwise
+ = defaultTyVar (not poly_kinds && is_kind_var) tv
+
+ simplify_cand candidates
+ = do { clone_wanteds <- newWanteds DefaultOrigin candidates
+ ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $
+ simplifyWantedsTcM clone_wanteds
+ -- Discard evidence; simples is fully zonked
+
+ ; let new_candidates = ctsPreds simples
+ ; traceTc "Simplified after defaulting" $
+ vcat [ text "Before:" <+> ppr candidates
+ , text "After:" <+> ppr new_candidates ]
+ ; return new_candidates }
+
+------------------
+decideQuantifiedTyVars
+ :: TyCoVarSet -- Monomorphic tyvars
+ -> [(Name,TcType)] -- Annotated theta and (name,tau) pairs
+ -> [TcIdSigInst] -- Partial signatures
+ -> [PredType] -- Candidates, zonked
+ -> TcM [TyVar]
+-- Fix what tyvars we are going to quantify over, and quantify them
+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
+ ; 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
+ ; 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_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
+ --
+ -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces
+ -- them in that order, so that the final qtvs quantifies in the same
+ -- order as the partial signatures do (Trac #13524)
+ ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
+ = candidateQTyVarsOfTypes $
+ psig_tys ++ candidates ++ tau_tys
+ pick = (`dVarSetIntersectVarSet` grown_tcvs)
+ dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_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 [Quantification and partial signatures]
+
+{- Note [Promote momomorphic tyvars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Promote any type variables that are free in the environment. Eg
+ f :: forall qtvs. bound_theta => zonked_tau
+The free vars of f's type 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]
+ constraints = 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
+
+NB: promoteTyVar ignores coercion variables
+
+Note [Quantification and partial signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When choosing type variables to quantify, the basic plan is to
quantify over all type variables that are
f x = ...
or
g :: (Eq _a) => _b -> _b
-In both cases we use plan InferGen, and hence call simplifyInfer.
-But those 'a' variables are skolems, and we should be sure to quantify
-over them, for two reasons
+In both cases we use plan InferGen, and hence call simplifyInfer. But
+those 'a' variables are skolems (actually SigTvs), and we should be
+sure to quantify over them. This leads to several wrinkles:
-* In the case of a type error
+* Wrinkle 1. In the case of a type error
f :: _ -> Maybe a
f x = True && x
The inferred type of 'f' is f :: Bool -> Bool, but there's a
left-over error of form (HoleCan (Maybe a ~ Bool)). The error-reporting
machine expects to find a binding site for the skolem 'a', so we
- add it to the ic_skols of the residual implication.
+ add it to the quantified tyvars.
- Note that we /only/ do this to the residual implication. We don't
- complicate the quantified type variables of 'f' for downstream code;
- it's just a device to make the error message generator know what to
- report.
-
-* Consider the partial type signature
+* Wrinkle 2. Consider the partial type signature
f :: (Eq _) => Int -> Int
f x = x
In normal cases that makes sense; e.g.
(thereby correctly triggering an ambiguity error later). If we don't
we'll end up with a strange open type
f :: Eq alpha => Int -> Int
- which isn't ambiguous but is still very wrong. That's why include
- psig_theta in the variables to quantify over, passed to
- decideQuantification.
+ which isn't ambiguous but is still very wrong.
+
+ Bottom line: Try to quantify over any variable free in psig_theta,
+ just like the tau-part of the type.
+
+* Wrinkle 3 (Trac #13482). Also consider
+ f :: forall a. _ => Int -> Int
+ 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'. But we still want to quantify
+ over 'a' even if the monomorphism restriction is on.
+
+* 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
- ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
+ -- Any insoluble constraints are in 'simples' and so get rewritten
+ -- See Note [Rewrite insolubles] in TcSMonad
- ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
- ; (no_new_scs, simples2) <- expandSuperClasses simples1
+ ; (floated_eqs, implics2) <- solveNestedImplications $
+ implics `unionBags` wc_impl wc1
- ; 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_impl = implics2
- , wc_insol = insols `unionBags` insols1 })
+ (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)
- -- 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
+ solveSimpleWanteds $
+ 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_impl = implics2
- , wc_insol = insols `unionBags` insols1 }) }
-
-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
+
+ ; bad_telescope <- checkBadTelescope implic
- final_needs = all_needs `delVarSetList` givens
+ ; 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 ()
+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) }
- | otherwise
- = return ()
-
-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 ()
-
--- | If the tyvar is a RuntimeRep var, set it to LiftedRep.
-defaultTyVar :: TcTyVar -> TcM ()
--- Precondition: MetaTyVars only
--- See Note [DefaultTyVar]
-defaultTyVar the_tv
- | isRuntimeRepVar the_tv
- = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
- ; writeMetaTyVar the_tv liftedRepTy }
-
- | otherwise = return () -- The common case
+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]
+
| otherwise
- = do { outer_tclvl <- TcS.getTcLevel
- ; mapM_ (promoteTyVarTcS outer_tclvl)
- (tyCoVarsOfCtsList float_eqs)
- -- See Note [Promoting unification variables]
+ = do { -- First zonk: the inert set (from whence they came) is fully
+ -- zonked, but unflattening may have filled in unification
+ -- 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
+ -- 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]
+ ; 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 } ) }
- where
- skol_set = mkVarSet skols
- (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
+ , text "Eqs =" <+> ppr eqs
+ , text "Floated eqs =" <+> ppr flt_eqs])
+ ; return ( flt_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)
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