diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Interact.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 128 |
1 files changed, 87 insertions, 41 deletions
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index dc20b90260..e8ab8ad82a 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP #-} +{-# LANGUAGE CPP, MultiWayIf #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -14,7 +14,6 @@ import GHC.Prelude import GHC.Types.Basic ( SwapFlag(..), infinity, IntWithInf, intGtLimit ) import GHC.Tc.Solver.Canonical -import GHC.Tc.Utils.Unify( canSolveByUnification ) import GHC.Types.Var.Set import GHC.Core.Type as Type import GHC.Core.InstEnv ( DFunInstType ) @@ -39,6 +38,7 @@ import GHC.Tc.Types import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Types.Origin +import GHC.Tc.Utils.TcMType( promoteMetaTyVarTo ) import GHC.Tc.Solver.Monad import GHC.Data.Bag import GHC.Utils.Monad ( concatMapM, foldlM ) @@ -106,8 +106,6 @@ solveSimpleGivens givens go new_givens } solveSimpleWanteds :: Cts -> TcS WantedConstraints --- NB: 'simples' may contain /derived/ equalities, floated --- out from a nested implication. So don't discard deriveds! -- The result is not necessarily zonked solveSimpleWanteds simples = do { traceTcS "solveSimpleWanteds {" (ppr simples) @@ -430,12 +428,11 @@ interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct) interactWithInertsStage wi = do { inerts <- getTcSInerts - ; lvl <- getTcLevel ; let ics = inert_cans inerts ; case wi of - CEqCan {} -> interactEq lvl ics wi - CIrredCan {} -> interactIrred ics wi - CDictCan {} -> interactDict ics wi + CEqCan {} -> interactEq ics wi + CIrredCan {} -> interactIrred ics wi + CDictCan {} -> interactDict ics wi _ -> pprPanic "interactWithInerts" (ppr wi) } -- CNonCanonical have been canonicalised @@ -734,25 +731,26 @@ Example of (b): assume a top-level class and instance declaration: Assume we have started with an implication: - forall c. Eq c => { wc_simple = D [c] c [W] } + forall c. Eq c => { wc_simple = [W] D [c] c } -which we have simplified to: +which we have simplified to, with a Derived constraing coming from +D's functional dependency: - forall c. Eq c => { wc_simple = D [c] c [W] - (c ~ [c]) [D] } + forall c. Eq c => { wc_simple = [W] D [c] c [W] + [D] (c ~ [c]) } -For some reason, e.g. because we floated an equality somewhere else, -we might try to re-solve this implication. If we do not do a -dropDerivedWC, then we will end up trying to solve the following -constraints the second time: +When iterating the solver, we might try to re-solve this +implication. If we do not do a dropDerivedWC, then we will end up +trying to solve the following constraints the second time: - (D [c] c) [W] - (c ~ [c]) [D] + [W] (D [c] c) + [D] (c ~ [c]) which will result in two Deriveds to end up in the insoluble set: - wc_simple = D [c] c [W] - (c ~ [c]) [D], (c ~ [c]) [D] + wc_simple = [W] D [c] c + [D] (c ~ [c]) + [D] (c ~ [c]) -} {- @@ -1439,8 +1437,8 @@ inertsCanDischarge inerts lhs rhs fr | otherwise = False -- Work item is fully discharged -interactEq :: TcLevel -> InertCans -> Ct -> TcS (StopOrContinue Ct) -interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs +interactEq :: InertCans -> Ct -> TcS (StopOrContinue Ct) +interactEq inerts workItem@(CEqCan { cc_lhs = lhs , cc_rhs = rhs , cc_ev = ev , cc_eq_rel = eq_rel }) @@ -1465,24 +1463,43 @@ interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs = do { traceTcS "Not unifying representational equality" (ppr workItem) ; continueWith workItem } - -- try improvement, if possible - | TyFamLHS fam_tc fam_args <- lhs - , isImprovable ev - = do { improveLocalFunEqs ev inerts fam_tc fam_args rhs - ; continueWith workItem } - - | TyVarLHS tv <- lhs - , canSolveByUnification tclvl tv rhs - = do { solveByUnification ev tv rhs - ; n_kicked <- kickOutAfterUnification tv - ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) } - | otherwise - = continueWith workItem - -interactEq _ _ wi = pprPanic "interactEq" (ppr wi) - -solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS () + = case lhs of + TyVarLHS tv -> tryToSolveByUnification workItem ev tv rhs + + TyFamLHS tc args -> do { when (isImprovable ev) $ + -- Try improvement, if possible + improveLocalFunEqs ev inerts tc args rhs + ; continueWith workItem } + +interactEq _ wi = pprPanic "interactEq" (ppr wi) + +---------------------- +-- We have a meta-tyvar on the left, and metaTyVarUpateOK has said "yes" +-- So try to solve by unifying. +-- Three reasons why not: +-- Skolem escape +-- Given equalities (GADTs) +-- Unifying a TyVarTv with a non-tyvar type +tryToSolveByUnification :: Ct -> CtEvidence + -> TcTyVar -- LHS tyvar + -> TcType -- RHS + -> TcS (StopOrContinue Ct) +tryToSolveByUnification work_item ev tv rhs + = do { can_unify <- unifyTest ev tv rhs + ; traceTcS "tryToSolveByUnification" (vcat [ ppr tv <+> char '~' <+> ppr rhs + , ppr can_unify ]) + + ; case can_unify of + NoUnify -> continueWith work_item + -- For the latter two cases see Note [Solve by unification] + UnifySameLevel -> solveByUnification ev tv rhs + UnifyOuterLevel free_metas tv_lvl + -> do { wrapTcS $ mapM_ (promoteMetaTyVarTo tv_lvl) free_metas + ; setUnificationFlag tv_lvl + ; solveByUnification ev tv rhs } } + +solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS (StopOrContinue Ct) -- Solve with the identity coercion -- Precondition: kind(xi) equals kind(tv) -- Precondition: CtEvidence is Wanted or Derived @@ -1504,9 +1521,10 @@ solveByUnification wd tv xi text "Coercion:" <+> pprEq tv_ty xi, text "Left Kind is:" <+> ppr (tcTypeKind tv_ty), text "Right Kind is:" <+> ppr (tcTypeKind xi) ] - ; unifyTyVar tv xi - ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) } + ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) + ; n_kicked <- kickOutAfterUnification tv + ; return (Stop wd (text "Solved by unification" <+> pprKicked n_kicked)) } {- Note [Avoid double unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1542,6 +1560,34 @@ and we want to get alpha := N b. See also #15144, which was caused by unifying a representational equality. +Note [Solve by unification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we solve + alpha[n] ~ ty +by unification, there are two cases to consider + +* UnifySameLevel: if the ambient level is 'n', then + we can simply update alpha := ty, and do nothing else + +* UnifyOuterLevel free_metas n: if the ambient level is greater than + 'n' (the level of alpha), in addition to setting alpha := ty we must + do two other things: + + 1. Promote all the free meta-vars of 'ty' to level n. After all, + alpha[n] is at level n, and so if we set, say, + alpha[n] := Maybe beta[m], + we must ensure that when unifying beta we do skolem-escape checks + etc relevent to level n. Simple way to do that: promote beta to + level n. + + 2. Set the Unification Level Flag to record that a level-n unification has + taken place. See Note [The Unification Level Flag] in GHC.Tc.Solver.Monad + +NB: UnifySameLevel is just an optimisation for UnifyOuterLevel. Promotion +would be a no-op, and setting the unification flag unnecessarily would just +make the solver iterate more often. (We don't need to iterate when unifying +at the ambient level becuase of the kick-out mechanism.) + ************************************************************************ * * |