diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Dict.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Dict.hs | 105 |
1 files changed, 75 insertions, 30 deletions
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs index a329711cad..558ff24002 100644 --- a/compiler/GHC/Tc/Solver/Dict.hs +++ b/compiler/GHC/Tc/Solver/Dict.hs @@ -10,9 +10,8 @@ module GHC.Tc.Solver.Dict ( import GHC.Prelude import GHC.Tc.Errors.Types -import GHC.Tc.Utils.TcType import GHC.Tc.Instance.FunDeps -import GHC.Tc.Instance.Class( safeOverlap ) +import GHC.Tc.Instance.Class( safeOverlap, matchEqualityInst ) import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint import GHC.Tc.Types.Origin @@ -20,6 +19,8 @@ import GHC.Tc.Types.EvTerm( evCallStack ) import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Monad import GHC.Tc.Solver.Types +import GHC.Tc.Utils.TcType +import GHC.Tc.Utils.Unify( uType ) import GHC.Hs.Type( HsIPName(..) ) @@ -53,6 +54,7 @@ import GHC.Driver.Session import qualified GHC.LanguageExtensions as LangExt import Data.Maybe ( listToMaybe, mapMaybe, isJust ) +import Data.Void( Void ) import Control.Monad.Trans.Maybe( MaybeT, runMaybeT ) import Control.Monad.Trans.Class( lift ) @@ -65,15 +67,27 @@ import Control.Monad( mzero, when ) * * ********************************************************************* -} -solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage () +{- Note [Solving equality classes] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We have a special solver for the "equality classes" + (t1 ~ t2), (t1 ~~ t2), and (Coercible t1 t2) + + TODO: expand this Note +-} + +solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void -- NC: this comes from CNonCanonical or CIrredCan -- Precondition: already rewritten by inert set solveDictNC ev cls tys + | isEqualityClass cls + = solveEqualityDict ev cls tys + + | otherwise = do { simpleStage $ traceTcS "solveDictNC" (ppr (mkClassPred cls tys) $$ ppr ev) ; dict_ct <- canDictCt ev cls tys ; solveDict dict_ct } -solveDict :: DictCt -> SolverStage () +solveDict :: DictCt -> SolverStage Void -- Preconditions: `tys` are already rewritten by the inert set solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys }) = assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $ @@ -96,7 +110,7 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys }) updInertDicts :: DictCt -> TcS () updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev }) - = do { -- See [Kick out existing binding for implicit parameter] + = do { -- See Note [Shadowing of Implicit Parameters] ; when (isGiven ev && isIPClass cls) $ updInertCans (updDicts (delIPDict dict_ct)) @@ -113,19 +127,10 @@ canDictCt ev cls tys do { dflags <- getDynFlags ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] + ; emitWork (listToBag sc_cts) - -- For equality classes, /replace/ the current constraint with its - -- superclasses, rather than /adding/ them. - -- See (NC1) in Note [Naturally coherent classes] - ; if isEqualityClass cls - then case sc_cts of - [ct] -> startAgainWith ct - _ -> pprPanic "canDictCt" (ppr cls) - else - - do { emitWork (listToBag sc_cts) ; continueWith (DictCt { di_ev = ev, di_cls = cls - , di_tys = tys, di_pend_sc = doNotExpand }) } } + , di_tys = tys, di_pend_sc = doNotExpand }) } -- doNotExpand: We have already expanded superclasses for /this/ dict -- so set the fuel to doNotExpand to avoid repeating expansion @@ -183,10 +188,17 @@ solveCallStack ev ev_cs ; setEvBindIfWanted ev IsCoherent ev_tm } -{- Note [Kick out existing binding for implicit parameter] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Shadowing of Implicit Parameters] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we add a new /given/ implicit parameter to the inert set, it /replaces/ -any existing givens for the same implicit parameter. +any existing givens for the same implicit parameter. This makes a difference +in two places: + +* In `GHC.Tc.Solver.InertSet.solveOneFromTheOther`, be careful when we have + (?x :: ty) in the inert set and an identical (?x :: ty) as the work item. + +* In `updInertDicts` in this module, when adding [G] (?x :: ty), remove any + existing [G] (?x :: ty'), regardless of ty' Example 1: @@ -265,6 +277,37 @@ I can think of two ways to fix this: {- ****************************************************************************** * * + solveEqualityDict +* * +****************************************************************************** -} + +solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void +-- Precondition: (isEqualityClass cls) True, so cls is (~), (~~), or Coercible +solveEqualityDict ev cls tys + | CtWanted { ctev_dest = dest } <- ev + = Stage $ + do { let (data_con, role, t1, t2) = matchEqualityInst cls tys + -- Unify t1~t2, putting anything that can't be solved + -- immediately into the work list + ; (co, _, _) <- wrapUnifierTcS ev role $ \uenv -> + uType uenv t1 t2 + -- Set d :: (t1~t2) = Eq# co + ; setWantedEvTerm dest IsCoherent $ + evDataConApp data_con tys [Coercion co] + ; stopWith ev "Solved wanted lifted equality" } + + | CtGiven { ctev_evar = ev_id, ctev_loc = loc } <- ev + , [sel_id] <- classSCSelIds cls -- Equality classes have just one superclass + = Stage $ + do { let sc_pred = classMethodInstTy sel_id tys + ev_expr = EvExpr $ Var sel_id `mkTyApps` tys `App` evId ev_id + ; given_ev <- newGivenEvVar loc (sc_pred, ev_expr) + ; startAgainWith (mkNonCanonical given_ev) } + | otherwise + = pprPanic "solveEqualityDict" (ppr cls) + +{- ****************************************************************************** +* * interactDict * * ********************************************************************************* @@ -770,7 +813,6 @@ matchClassInst dflags inerts clas tys loc -- whether top level, or local quantified constraints. -- See Note [Instance and Given overlap] | not (xopt LangExt.IncoherentInstances dflags) - , not (naturallyCoherentClass clas) -- See (NC3) in Note [Naturally coherent classes] , not (noMatchableGivenDicts inerts loc clas tys) = do { traceTcS "Delaying instance application" $ vcat [ text "Work item=" <+> pprClassPred clas tys ] @@ -796,6 +838,7 @@ matchClassInst dflags inerts clas tys loc where pred = mkClassPred clas tys +{- -- | If a class is "naturally coherent", then we needn't worry at all, in any -- way, about overlapping/incoherent instances. Just solve the thing! -- See Note [Naturally coherent classes] @@ -803,6 +846,7 @@ matchClassInst dflags inerts clas tys loc naturallyCoherentClass :: Class -> Bool naturallyCoherentClass cls = isCTupleClass cls || isEqualityClass cls +-} isEqualityClass :: Class -> Bool -- True of (~), (~~), and Coercible @@ -903,14 +947,15 @@ this: (See Note [The equality types story] in GHC.Builtin.Types.Prim.) PS: the term "naturally coherent" doesn't really seem helpful. -Perhaps "invertible" or something? I left it for now though. +Perhaps "invertible" or "bidirectional" or something? I left it for +now though. For naturally coherent classes: -(NC1) For Givens, when expanding superclasses, we /replace/ the constraint - with its superclasses (which, remember, are equally powerful) rather than - /adding/ them. This can make a huge difference. Consider T17836, which - has a constraint like +(NC1) For Givens, when expanding the superclasses of a naturally coherent class, + we can /replace/ the constraint with its superclasses (which, remember, are + equally powerful) rather than /adding/ them. This can make a huge difference. + Consider T17836, which has a constraint like forall b,c. a ~ (b,c) => forall d,e. c ~ (d,e) => ...etc... @@ -923,7 +968,7 @@ For naturally coherent classes: Originally I tried this for all naturally-coherent classes, including tuples. But discarding the tuple Given (which "replacing" does) means that we may have to reconstruct it for a recursive call, and the optimiser isn't - quite clever enought to figure that out: see #10359 and its test case. + quite clever enough to figure that out: see #10359 and its test case. This is less pressing for equality classes because they have to be unpacked strictly, so CSE-ing away the reconstuction works fine. Hence the use of isEqualityClass rather than naturallyCoherentClass in canDictCt. @@ -944,7 +989,7 @@ For naturally coherent classes: so the reduction of the [W] constraint does not risk losing any solutions. On the other hand, it can be fatal to /fail/ to reduce such equalities - on the grounds of Note [Instance and Given overlap], fbecause many good + on the grounds of Note [Instance and Given overlap], because many good things flow from [W] t1 ~# t2. The same reasoning applies to @@ -1923,8 +1968,8 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc = | otherwise = do { given_ev <- newGivenEvVar sc_loc $ mk_given_desc sel_id sc_pred - ; assertFuelPrecondition fuel - $ mk_superclasses fuel rec_clss given_ev tvs theta sc_pred } + ; assertFuelPrecondition fuel $ + mk_superclasses fuel rec_clss given_ev tvs theta sc_pred } where sc_pred = classMethodInstTy sel_id tys @@ -1952,7 +1997,7 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc = `App` (evId evar `mkVarApps` (tvs ++ dict_ids)) `mkVarApps` sc_tvs - sc_loc | naturallyCoherentClass cls + sc_loc | isCTupleClass cls = loc -- See (NC2) in Note [Naturally coherent classes] | otherwise = loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) } |