defaultCallStack ct
| ClassPred cls tys <- classifyPredType (ctPred ct)
, Just {} <- isCallStackPred cls tys
- = do { solveCallStack (cc_ev ct) EvCsEmpty
+ = 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 }
-> TcM ([TcTyVar], -- Quantify over these type variables
[EvVar], -- ... and these constraints (fully zonked)
TcEvBinds, -- ... binding these evidence variables
- Bool) -- True <=> there was an insoluble type error
- -- in these bindings
+ 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, False) }
+ ; 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]
, ctev_loc = ct_loc }
| psig_theta_var <- psig_theta_vars ]
- -- Now we can emil the residual constraints
- ; emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
- name_taus co_vars qtvs
- bound_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!
, text "qtvs =" <+> ppr qtvs
, text "definite_error =" <+> ppr definite_error ]
- ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
+ ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var
+ , residual_wanted, definite_error ) }
-- NB: bound_theta_vars must be fully zonked
--------------------
-emitResidualConstraints :: TcLevel -> TcLclEnv -> EvBindsVar
- -> [(Name, TcTauType)]
- -> VarSet -> [TcTyVar] -> [EvVar]
- -> WantedConstraints -> TcM ()
+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]
-emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
+mkResidualConstraints rhs_tclvl tc_env ev_binds_var
name_taus co_vars qtvs full_theta_vars wanteds
| isEmptyWC wanteds
- = return ()
+ = return wanteds
+
| otherwise
= do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple)
- ; unless (isEmptyCts outer_simple) $
- do { traceTc "emitResidualConstrants:simple" (ppr outer_simple)
- ; emitSimples outer_simple }
-
; let inner_wanted = wanteds { wc_simple = inner_simple }
- implic = mk_implic inner_wanted
- ; unless (isEmptyWC inner_wanted) $
- do { traceTc "emitResidualConstraints:implic" (ppr implic)
- ; emitImplication implic }
- }
+ ; return (WC { wc_simple = outer_simple
+ , wc_impl = mk_implic inner_wanted })}
where
mk_implic inner_wanted
- = newImplication { ic_tclvl = rhs_tclvl
- , ic_skols = qtvs
- , ic_given = full_theta_vars
- , ic_wanted = inner_wanted
- , ic_binds = ev_binds_var
- , ic_info = skol_info
- , ic_env = tc_lcl_env }
+ | 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)
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.)
+constraints out. (NB: this set of CoVars should be closed-over-kinds.)
All rather subtle; see Trac #14584.
; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
; let quantifiable_candidates
= pickQuantifiablePreds (mkVarSet qtvs) candidates
- -- NB: do /not/ run pickQuantifieablePreds over psig_theta,
+ -- 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
-- Any insoluble constraints are in 'simples' and so get rewritten
-- See Note [Rewrite insolubles] in TcSMonad
- ; let WC { wc_simple = simples1, 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_impl = implics2 })
+ (wc1 { wc_impl = implics2 })
; ev_binds_var <- getTcEvBindsVar
; bb <- TcS.getTcEvBindsMap ev_binds_var
; 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_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
- -- Notes:
- -- - 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_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_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 {" (ppr unsolved)
- ; 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 { traceTcS "expandSuperClasses mid"
- (vcat [ text "pending_given:" <+> ppr pending_given
- , text "pending_wanted:" <+> ppr pending_wanted ])
- ; 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 (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_status = status
- , ic_info = info
- , ic_skols = skols
- , ic_telescope = m_telescope
- , ic_wanted = wc
- , 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
not (isSolvedWC pruned_wc)
-- See Note [Tracking redundant constraints]
= do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic)
- ; implic <- neededEvVars implic
- ; skols <- mapM TcS.zonkTcTyCoVarBndr skols
+ ; implic@(Implic { ic_need_inner = need_inner
+ , ic_need_outer = need_outer }) <- neededEvVars implic
+
+ ; bad_telescope <- checkBadTelescope implic
; let dead_givens | warnRedundantGivens info
- = filterOut (`elemVarSet` ic_need_inner implic) givens
+ = filterOut (`elemVarSet` need_inner) givens
| otherwise = [] -- None to report
- bad_telescope = check_telescope skols
-
discard_entire_implication -- Can we discard the entire implication?
= null dead_givens -- No warning from this implication
&& not bad_telescope
- && isEmptyBag pruned_implics -- No live children
- && isEmptyVarSet (ic_need_outer implic) -- No needed vars to pass up to parent
+ && isEmptyWC pruned_wc -- No live children
+ && isEmptyVarSet need_outer -- No needed vars to pass up to parent
final_status
| bad_telescope = IC_BadTelescope
| otherwise
= True -- Otherwise, keep it
- -- See Note [Keeping scoped variables in order: Explicit] in TcHsType
- check_telescope sks = isJust m_telescope && go emptyVarSet (reverse sks)
- 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
+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 _ _)
git.haskell.org / ghc.git / blobdiff