diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver.hs | 59 |
1 files changed, 28 insertions, 31 deletions
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index 96fe5cbca2..f08622d8f1 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -718,22 +718,22 @@ simplifyDefault theta ; return () } ------------------ -tcCheckSatisfiability :: Bag EvVar -> TcM Bool --- Return True if satisfiable, False if definitely contradictory -tcCheckSatisfiability given_ids - = do { lcl_env <- TcM.getLclEnv - ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env - ; (res, _ev_binds) <- runTcS $ - do { traceTcS "checkSatisfiability {" (ppr given_ids) - ; let given_cts = mkGivens given_loc (bagToList given_ids) - -- See Note [Superclasses and satisfiability] - ; solveSimpleGivens given_cts - ; insols <- getInertInsols - ; insols <- try_harder insols - ; traceTcS "checkSatisfiability }" (ppr insols) - ; return (isEmptyBag insols) } - ; return res } - where +tcCheckSatisfiability :: InertSet -> Bag EvVar -> TcM (Maybe InertSet) +-- Return (Just new_inerts) if satisfiable, Nothing if definitely contradictory +tcCheckSatisfiability inerts given_ids = do + (sat, new_inerts) <- runTcSInerts inerts $ do + traceTcS "checkSatisfiability {" (ppr inerts <+> ppr given_ids) + lcl_env <- TcS.getLclEnv + let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env + let given_cts = mkGivens given_loc (bagToList given_ids) + -- See Note [Superclasses and satisfiability] + solveSimpleGivens given_cts + insols <- getInertInsols + insols <- try_harder insols + traceTcS "checkSatisfiability }" (ppr insols) + return (isEmptyBag insols) + return $ if sat then Just new_inerts else Nothing + where try_harder :: Cts -> TcS Cts -- Maybe we have to search up the superclass chain to find -- an unsatisfiable constraint. Example: pmcheck/T3927b. @@ -749,15 +749,11 @@ tcCheckSatisfiability given_ids -- | Normalise a type as much as possible using the given constraints. -- See @Note [tcNormalise]@. -tcNormalise :: Bag EvVar -> Type -> TcM Type -tcNormalise given_ids ty - = do { lcl_env <- TcM.getLclEnv - ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env - ; norm_loc <- getCtLocM PatCheckOrigin Nothing - ; (res, _ev_binds) <- runTcS $ - do { traceTcS "tcNormalise {" (ppr given_ids) - ; let given_cts = mkGivens given_loc (bagToList given_ids) - ; solveSimpleGivens given_cts +tcNormalise :: InertSet -> Type -> TcM Type +tcNormalise inerts ty + = do { norm_loc <- getCtLocM PatCheckOrigin Nothing + ; (res, _new_inerts) <- runTcSInerts inerts $ + do { traceTcS "tcNormalise {" (ppr inerts) ; ty' <- flattenType norm_loc ty ; traceTcS "tcNormalise }" (ppr ty') ; pure ty' } @@ -788,8 +784,9 @@ Note [tcNormalise] tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas most invocations of the constraint solver are intended to simplify a set of constraints or to decide if a particular set of constraints is satisfiable, -the purpose of tcNormalise is to take a type, plus some local constraints, and -normalise the type as much as possible with respect to those constraints. +the purpose of tcNormalise is to take a type, plus some locally solved +constraints in the form of an InertSet, and normalise the type as much as +possible with respect to those constraints. It does *not* reduce type or data family applications or look through newtypes. @@ -798,9 +795,9 @@ expression, it's possible that the type of the scrutinee will only reduce if some local equalities are solved for. See "Wrinkle: Local equalities" in Note [Type normalisation] in "GHC.HsToCore.PmCheck". -To accomplish its stated goal, tcNormalise first feeds the local constraints -into solveSimpleGivens, then uses flattenType to simplify the desired type -with respect to the givens. +To accomplish its stated goal, tcNormalise first initialises the solver monad +with the given InertCans, then uses flattenType to simplify the desired type +with respect to the Givens in the InertCans. *********************************************************************************** * * @@ -893,7 +890,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds ; psig_theta_vars <- mapM TcM.newEvVar psig_theta ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $ - runTcSWithEvBinds ev_binds_var $ + runTcSWithEvBinds ev_binds_var True $ do { let loc = mkGivenLoc rhs_tclvl UnkSkol $ env_lcl tc_env psig_givens = mkGivens loc psig_theta_vars |