diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver.hs | 70 |
1 files changed, 44 insertions, 26 deletions
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index 5319a52ad0..6a1f2d3315 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -1,4 +1,4 @@ - +{-# LANGUAGE RecursiveDo #-} module GHC.Tc.Solver( InferMode(..), simplifyInfer, findInferredDiff, @@ -59,6 +59,7 @@ import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType import GHC.Core.Type import GHC.Core.Ppr +import GHC.Core.TyCon ( TyConBinder ) import GHC.Builtin.Types ( liftedRepTy, manyDataConTy, liftedDataConTy ) import GHC.Core.Unify ( tcMatchTyKi ) import GHC.Utils.Misc @@ -164,17 +165,17 @@ simplifyTop wanteds ; return (evBindMapBinds binds1 `unionBags` binds2) } -pushLevelAndSolveEqualities :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a +pushLevelAndSolveEqualities :: SkolemInfoAnon -> [TyConBinder] -> TcM a -> TcM a -- Push level, and solve all resulting equalities -- If there are any unsolved equalities, report them -- and fail (in the monad) -- -- Panics if we solve any non-equality constraints. (In runTCSEqualities -- we use an error thunk for the evidence bindings.) -pushLevelAndSolveEqualities skol_info skol_tvs thing_inside +pushLevelAndSolveEqualities skol_info_anon tcbs thing_inside = do { (tclvl, wanted, res) <- pushLevelAndSolveEqualitiesX "pushLevelAndSolveEqualities" thing_inside - ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted + ; report_unsolved_equalities skol_info_anon (binderVars tcbs) tclvl wanted ; return res } pushLevelAndSolveEqualitiesX :: String -> TcM a @@ -228,11 +229,11 @@ simplifyAndEmitFlatConstraints wanted -- Emit the bad constraints, wrapped in an implication -- See Note [Wrapping failing kind equalities] ; tclvl <- TcM.getTcLevel - ; implic <- buildTvImplication UnkSkol [] (pushTcLevel tclvl) wanted - -- ^^^^^^ | ^^^^^^^^^^^^^^^^^ - -- it's OK to use UnkSkol | we must increase the TcLevel, - -- because we don't bind | as explained in - -- any skolem variables here | Note [Wrapping failing kind equalities] + ; implic <- buildTvImplication unkSkolAnon [] (pushTcLevel tclvl) wanted + -- ^^^^^^ | ^^^^^^^^^^^^^^^^^ + -- it's OK to use unkSkol | we must increase the TcLevel, + -- because we don't bind | as explained in + -- any skolem variables here | Note [Wrapping failing kind equalities] ; emitImplication implic ; failM } Just (simples, holes) @@ -461,13 +462,20 @@ reportUnsolvedEqualities :: SkolemInfo -> [TcTyVar] -> TcLevel -- -- The provided SkolemInfo and [TcTyVar] arguments are used in an implication to -- provide skolem info for any errors. --- reportUnsolvedEqualities skol_info skol_tvs tclvl wanted + = report_unsolved_equalities (getSkolemInfo skol_info) skol_tvs tclvl wanted + +report_unsolved_equalities :: SkolemInfoAnon -> [TcTyVar] -> TcLevel + -> WantedConstraints -> TcM () +report_unsolved_equalities skol_info_anon skol_tvs tclvl wanted | isEmptyWC wanted = return () - | otherwise + + | otherwise -- NB: we build an implication /even if skol_tvs is empty/, + -- just to ensure that our level invariants hold, specifically + -- (WantedInv). See Note [TcLevel invariants]. = checkNoErrs $ -- Fail - do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted + do { implic <- buildTvImplication skol_info_anon skol_tvs tclvl wanted ; reportAllUnsolved (mkImplicWC (unitBag implic)) } @@ -903,7 +911,7 @@ tcCheckGivens inerts given_ids = do (sat, new_inerts) <- runTcSInerts inerts $ do traceTcS "checkGivens {" (ppr inerts <+> ppr given_ids) lcl_env <- TcS.getLclEnv - let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env + let given_loc = mkGivenLoc topTcLevel (getSkolemInfo unkSkol) lcl_env let given_cts = mkGivens given_loc (bagToList given_ids) -- See Note [Superclasses and satisfiability] solveSimpleGivens given_cts @@ -1052,7 +1060,9 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds , pred <- sig_inst_theta sig ] ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus) - ; qtkvs <- quantifyTyVars DefaultNonStandardTyVars dep_vars + + ; skol_info <- mkSkolemInfo (InferSkol name_taus) + ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars dep_vars ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs) ; return (qtkvs, [], emptyTcEvBinds, False) } @@ -1104,10 +1114,16 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds -- NB: bound_theta are constraints we want to quantify over, -- 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 + ; rec { (qtvs, bound_theta, co_vars) <- decideQuantification skol_info infer_mode rhs_tclvl name_taus partial_sigs quant_pred_candidates - ; bound_theta_vars <- mapM TcM.newEvVar bound_theta + ; bound_theta_vars <- mapM TcM.newEvVar bound_theta + + ; let full_theta = map idType bound_theta_vars + ; skol_info <- mkSkolemInfo (InferSkol [ (name, mkSigmaTy [] full_theta ty) + | (name, ty) <- name_taus ]) + } + -- Now emit the residual constraint ; emitResidualConstraints rhs_tclvl ev_binds_var @@ -1189,7 +1205,7 @@ findInferredDiff annotated_theta inferred_theta do { lcl_env <- TcM.getLclEnv ; given_ids <- mapM TcM.newEvVar annotated_theta ; wanteds <- newWanteds AnnOrigin inferred_theta - ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env + ; let given_loc = mkGivenLoc topTcLevel (getSkolemInfo unkSkol) lcl_env given_cts = mkGivens given_loc given_ids ; residual <- runTcSDeriveds $ @@ -1332,7 +1348,8 @@ If the monomorphism restriction does not apply, then we quantify as follows: -} decideQuantification - :: InferMode + :: SkolemInfo + -> InferMode -> TcLevel -> [(Name, TcTauType)] -- Variables to be generalised -> [TcIdSigInst] -- Partial type signatures (if any) @@ -1341,7 +1358,7 @@ decideQuantification , [PredType] -- and this context (fully zonked) , VarSet) -- See Note [Deciding quantification] -decideQuantification infer_mode rhs_tclvl name_taus psigs candidates +decideQuantification skol_info 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 @@ -1351,7 +1368,7 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates -- Step 3: decide which kind/type variables to quantify over - ; qtvs <- decideQuantifiedTyVars name_taus psigs candidates + ; qtvs <- decideQuantifiedTyVars skol_info name_taus psigs candidates -- Step 4: choose which of the remaining candidate -- predicates to actually quantify over @@ -1436,7 +1453,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates -- If possible, we quantify over partial-sig qtvs, so they are -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs - ; psig_qtvs <- mapM zonkTcTyVarToTyVar $ binderVars $ + ; psig_qtvs <- zonkTcTyVarsToTcTyVars $ binderVars $ concatMap (map snd . sig_inst_skols) psigs ; psig_theta <- mapM TcM.zonkTcType $ @@ -1587,12 +1604,13 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates ------------------ decideQuantifiedTyVars - :: [(Name,TcType)] -- Annotated theta and (name,tau) pairs + :: SkolemInfo + -> [(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 name_taus psigs candidates +decideQuantifiedTyVars skol_info 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 @@ -1631,7 +1649,7 @@ decideQuantifiedTyVars name_taus psigs candidates , text "grown_tcvs =" <+> ppr grown_tcvs , text "dvs =" <+> ppr dvs_plus]) - ; quantifyTyVars DefaultNonStandardTyVars dvs_plus } + ; quantifyTyVars skol_info DefaultNonStandardTyVars dvs_plus } ------------------ growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet @@ -2192,7 +2210,7 @@ checkBadTelescope (Implic { ic_info = info | otherwise = go (later_skols `extendVarSet` one_skol) earlier_skols -warnRedundantGivens :: SkolemInfo -> Bool +warnRedundantGivens :: SkolemInfoAnon -> Bool warnRedundantGivens (SigSkol ctxt _ _) = case ctxt of FunSigCtxt _ rrc -> reportRedundantConstraints rrc @@ -2835,7 +2853,7 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds) | Just subst <- mb_subst = do { lcl_env <- TcS.getLclEnv ; tc_lvl <- TcS.getTcLevel - ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env + ; let loc = mkGivenLoc tc_lvl (getSkolemInfo unkSkol) lcl_env -- Equality constraints are possible due to type defaulting plugins ; wanted_evs <- mapM (newWantedNC loc . substTy subst . ctPred) wanteds |