\begin{code}
module TcInteract (
- solveInteract, AtomicInert, tyVarsOfInert,
- InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, foldISEqCts
+ solveInteract, solveInteractGiven, solveInteractWanted,
+ AtomicInert, tyVarsOfInert,
+ InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
) where
#include "HsVersions.h"
import TcCanonical
import VarSet
import Type
+import Unify
import Id
import Var
import TcType
import HsBinds
-import InstEnv
+import Inst( tyVarsOfEvVar )
import Class
import TyCon
import Name
import FunDeps
-import Control.Monad ( when )
-
import Coercion
import Outputable
import TcRnTypes
+import TcMType ( isSilentEvVar )
import TcErrors
import TcSMonad
import Bag
import qualified Data.Map as Map
-import Control.Monad( unless )
+import Control.Monad( when )
+
import FastString ( sLit )
import DynFlags
\end{code}
will be marked as solved right before being pushed into the inert set.
See note [Touchables and givens].
- 8 No Given constraint mentions a touchable unification variable,
- except if the
+ 8 No Given constraint mentions a touchable unification variable, but
+ Given/Solved may do so.
+
+ 9 Given constraints will also have their superclasses in the inert set,
+ but Given/Solved will not.
Note that 6 and 7 are /not/ enforced by canonicalization but rather by
insertion in the inert list, ie by TcInteract.
\begin{code}
-data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts
- -- Invariant: all Given or Derived
+data CCanMap a = CCanMap { cts_given :: Map.Map a CanonicalCts
+ -- Invariant: all Given
+ , cts_derived :: Map.Map a CanonicalCts
+ -- Invariant: all Derived
, cts_wanted :: Map.Map a CanonicalCts }
-- Invariant: all Wanted
+
cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
-cCanMapToBag cmap = Map.fold unionBags rest_cts (cts_givder cmap)
- where rest_cts = Map.fold unionBags emptyCCan (cts_wanted cmap)
+cCanMapToBag cmap = Map.fold unionBags rest_wder (cts_given cmap)
+ where rest_wder = Map.fold unionBags rest_der (cts_wanted cmap)
+ rest_der = Map.fold unionBags emptyCCan (cts_derived cmap)
emptyCCanMap :: CCanMap a
-emptyCCanMap = CCanMap { cts_givder = Map.empty, cts_wanted = Map.empty }
+emptyCCanMap = CCanMap { cts_given = Map.empty
+ , cts_derived = Map.empty, cts_wanted = Map.empty }
updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
updCCanMap (a,ct) cmap
= case cc_flavor ct of
Wanted {}
-> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
- _
- -> cmap { cts_givder = Map.insertWith unionBags a this_ct (cts_givder cmap) }
+ Given {}
+ -> cmap { cts_given = Map.insertWith unionBags a this_ct (cts_given cmap) }
+ Derived {}
+ -> cmap { cts_derived = Map.insertWith unionBags a this_ct (cts_derived cmap) }
where this_ct = singleCCan ct
getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
-- Gets the relevant constraints and returns the rest of the CCanMap
getRelevantCts a cmap
- = let relevant = unionBags (Map.findWithDefault emptyCCan a (cts_wanted cmap))
- (Map.findWithDefault emptyCCan a (cts_givder cmap))
+ = let relevant = unionManyBags [ Map.findWithDefault emptyCCan a (cts_wanted cmap)
+ , Map.findWithDefault emptyCCan a (cts_given cmap)
+ , Map.findWithDefault emptyCCan a (cts_derived cmap) ]
residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
- , cts_givder = Map.delete a (cts_givder cmap) }
+ , cts_given = Map.delete a (cts_given cmap)
+ , cts_derived = Map.delete a (cts_derived cmap) }
in (relevant, residual_map)
-extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
--- Gets the wanted constraints and returns a residual CCanMap
-extractUnsolvedCMap cmap =
- let unsolved = Map.fold unionBags emptyCCan (cts_wanted cmap)
- in (unsolved, cmap { cts_wanted = Map.empty})
+extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
+-- Gets the wanted or derived constraints and returns a residual
+-- CCanMap with only givens.
+extractUnsolvedCMap cmap =
+ let wntd = Map.fold unionBags emptyCCan (cts_wanted cmap)
+ derd = Map.fold unionBags emptyCCan (cts_derived cmap)
+ in (wntd `unionBags` derd,
+ cmap { cts_wanted = Map.empty, cts_derived = Map.empty })
+
-- See Note [InertSet invariants]
data InertSet
= IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan)
-
- , inert_dicts :: CCanMap Class -- Dictionaries only
+ , inert_dicts :: CCanMap Class -- Dictionaries only
, inert_ips :: CCanMap (IPName Name) -- Implicit parameters
- , inert_funeqs :: CCanMap TyCon -- Type family equalities only
+ , inert_frozen :: CanonicalCts
+ , inert_funeqs :: CCanMap TyCon -- Type family equalities only
-- This representation allows us to quickly get to the relevant
-- inert constraints when interacting a work item with the inert set.
-
-
- , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already
- -- and reside either in the worklist or in the inerts
}
tyVarsOfInert :: InertSet -> TcTyVarSet
tyVarsOfInert (IS { inert_eqs = eqs
, inert_dicts = dictmap
, inert_ips = ipmap
- , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts
- where cts = eqs `andCCan` cCanMapToBag dictmap
- `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap
-
-type FDImprovement = (PredType,PredType)
-type FDImprovements = [(PredType,PredType)]
+ , inert_frozen = frozen
+ , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts
+ where
+ cts = eqs `andCCan` frozen `andCCan` cCanMapToBag dictmap
+ `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap
instance Outputable InertSet where
ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
- , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
+ , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
, vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
, vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
+ , text "Frozen errors =" <+> -- Clearly print frozen errors
+ vcat (map ppr (Bag.bagToList $ inert_frozen is))
]
emptyInert :: InertSet
emptyInert = IS { inert_eqs = Bag.emptyBag
+ , inert_frozen = Bag.emptyBag
, inert_dicts = emptyCCanMap
, inert_ips = emptyCCanMap
- , inert_funeqs = emptyCCanMap
- , inert_fds = [] }
+ , inert_funeqs = emptyCCanMap }
updInertSet :: InertSet -> AtomicInert -> InertSet
updInertSet is item
| Just tc <- isCFunEqCan_Maybe item -- Function equality
= is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
| otherwise
- = pprPanic "Unknown form of constraint!" (ppr item)
-
-updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet
-updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is }
-updInertSetFDImprs is Nothing = is
-
-foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
--- Fold over the equalities of the inerts
-foldISEqCtsM k z IS { inert_eqs = eqs }
- = Bag.foldlBagM k z eqs
-
-foldISEqCts :: (a -> AtomicInert -> a) -> a -> InertSet -> a
-foldISEqCts k z IS { inert_eqs = eqs }
- = Bag.foldlBag k z eqs
+ = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
--- Postcondition: the canonical cts returnd are the very same as the
--- WantedEvVars in their canonical form.
+-- Postcondition: the returned canonical cts are either Derived, or Wanted.
extractUnsolved is@(IS {inert_eqs = eqs})
= let is_solved = is { inert_eqs = solved_eqs
, inert_dicts = solved_dicts
, inert_ips = solved_ips
- , inert_funeqs = solved_funeqs }
+ , inert_frozen = emptyCCan
+ , inert_funeqs = solved_funeqs }
in (is_solved, unsolved)
- where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
+ where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenOrSolvedCt) eqs
(unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
(unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
(unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
- unsolved = unsolved_eqs `unionBags`
+ unsolved = unsolved_eqs `unionBags` inert_frozen is `unionBags`
unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
-
-haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool
-haveBeenImproved [] _ _ = False
-haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2'
- | tcEqPred pty1 pty1' && tcEqPred pty2 pty2'
- = True
- | tcEqPred pty1 pty2' && tcEqPred pty2 pty1'
- = True
- | otherwise
- = haveBeenImproved fdimprs pty1' pty2'
-
-getFDImprovements :: InertSet -> FDImprovements
--- Return a list of the improvements that have kicked in so far
-getFDImprovements = inert_fds
-
\end{code}
-{-- DV: This note will go away!
-
-Note [Touchables and givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Touchable variables will never show up in givens which are inputs to
-the solver. However, touchables may show up in givens generated by the flattener.
-For example,
-
- axioms:
- G Int ~ Char
- F Char ~ Int
-
- wanted:
- F (G alpha) ~w Int
-
-canonicalises to
-
- G alpha ~g b
- F b ~w Int
-
-which can be put in the inert set. Suppose we also have a wanted
-
- alpha ~w Int
-
-We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
-Int. Instead, after reacting alpha ~w Int with the whole inert set,
-we observe that we can solve it by unifying alpha with Int, so we mark
-it as solved and put it back in the *work list*. [We also immediately unify
-alpha := Int, without telling anyone, see trySpontaneousSolve function, to
-avoid doing this in the end.]
-
-Later, because it is solved (given, in effect), we can use it to rewrite
-G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
-we will dispatch the remaining wanted constraints using the top-level axioms.
-
-Finally, note that after reacting a wanted equality with the entire inert set
-we may end up with something like
-
- b ~w alpha
-
-which we should flip around to generate the solved constraint alpha ~s b.
-
--}
-
-
-
%*********************************************************************
%* *
* Main Interaction Solver *
type AtomicInert = CanonicalCt -- constraint pulled from InertSet
type WorkItem = CanonicalCt -- constraint pulled from WorkList
--- A mixture of Given, Wanted, and Derived constraints.
--- We split between equalities and the rest to process equalities first.
-type WorkList = CanonicalCts
-
-unionWorkLists :: WorkList -> WorkList -> WorkList
-unionWorkLists = andCCan
-
-isEmptyWorkList :: WorkList -> Bool
-isEmptyWorkList = isEmptyCCan
-
-emptyWorkList :: WorkList
-emptyWorkList = emptyCCan
-
-workListFromCCan :: CanonicalCt -> WorkList
-workListFromCCan = singleCCan
-
------------------------
data StopOrContinue
= Stop -- Work item is consumed
, ptext (sLit "new work =") <+> ppr work <> comma
, ptext (sLit "stop =") <+> ppr stop])
-type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
+type SubGoalDepth = Int -- Starts at zero; used to limit infinite
+ -- recursion of sub-goals
+type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult
-- Combine a sequence of simplifier 'stages' to create a pipeline
-runSolverPipeline :: [(String, SimplifierStage)]
- -> InertSet -> WorkItem
+runSolverPipeline :: SubGoalDepth
+ -> [(String, SimplifierStage)]
+ -> InertSet -> WorkItem
-> TcS (InertSet, WorkList)
-- Precondition: non-empty list of stages
-runSolverPipeline pipeline inerts workItem
+runSolverPipeline depth pipeline inerts workItem
= do { traceTcS "Start solver pipeline" $
vcat [ ptext (sLit "work item =") <+> ppr workItem
, ptext (sLit "inerts =") <+> ppr inerts]
; let itr_in = SR { sr_inerts = inerts
- , sr_new_work = emptyWorkList
- , sr_stop = ContinueWith workItem }
+ , sr_new_work = emptyWorkList
+ , sr_stop = ContinueWith workItem }
; itr_out <- run_pipeline pipeline itr_in
; let new_inert
= case sr_stop itr_out of
(SR { sr_new_work = accum_work
, sr_inerts = inerts
, sr_stop = ContinueWith work_item })
- = do { itr <- stage work_item inerts
+ = do { itr <- stage depth work_item inerts
; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
- ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
+ ; let itr' = itr { sr_new_work = accum_work `unionWorkList` sr_new_work itr }
; run_pipeline stages itr' }
\end{code}
-- returning an extended inert set.
--
-- See Note [Touchables and givens].
-solveInteract :: InertSet -> Bag (CtFlavor,EvVar) -> TcS InertSet
+solveInteractGiven :: InertSet -> GivenLoc -> [EvVar] -> TcS InertSet
+solveInteractGiven inert gloc evs
+ = do { (_, inert_ret) <- solveInteract inert $ listToBag $
+ map mk_given evs
+ ; return inert_ret }
+ where
+ flav = Given gloc GivenOrig
+ mk_given ev = mkEvVarX ev flav
+
+solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet
+solveInteractWanted inert wvs
+ = do { (_,inert_ret) <- solveInteract inert $ listToBag $
+ map wantedToFlavored wvs
+ ; return inert_ret }
+
+solveInteract :: InertSet -> Bag FlavoredEvVar -> TcS (Bool, InertSet)
+-- Post: (True, inert_set) means we managed to discharge all constraints
+-- without actually doing any interactions!
+-- (False, inert_set) means some interactions occurred
solveInteract inert ws
= do { dyn_flags <- getDynFlags
- ; sctx <- getTcSContext
-
- ; traceTcS "solveInteract, before clever canonicalization:" $
- ppr (mapBag (\(ct,ev) -> (ct,evVarPred ev)) ws)
-
- ; can_ws <- foldlBagM (tryPreSolveAndCanon sctx inert) emptyCCan ws
-
- ; traceTcS "solveInteract, after clever canonicalization:" $
- ppr can_ws
-
- ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert can_ws }
-
-tryPreSolveAndCanon :: SimplContext -> InertSet -> CanonicalCts -> (CtFlavor, EvVar) -> TcS CanonicalCts
--- Checks if this constraint can be immediately solved from a constraint in the
--- inert set or in the previously encountered CanonicalCts and only then
--- canonicalise it. See Note [Avoiding the superclass explosion]
-tryPreSolveAndCanon sctx is cts_acc (fl,ev_var)
- | ClassP clas tys <- evVarPred ev_var
- , not $ simplEqsOnly sctx -- And we *can* discharge constraints from other constraints
- = do { let (relevant_inert_dicts,_) = getRelevantCts clas (inert_dicts is)
- ; b <- dischargeFromCans (cts_acc `unionBags` relevant_inert_dicts)
- (fl,ev_var,clas,tys)
- ; extra_cts <- if b then return emptyCCan else mkCanonical fl ev_var
- ; return (cts_acc `unionBags` extra_cts) }
- | otherwise
- = do { extra_cts <- mkCanonical fl ev_var
- ; return (cts_acc `unionBags` extra_cts) }
-
-dischargeFromCans :: CanonicalCts -> (CtFlavor,EvVar,Class,[Type]) -> TcS Bool
-dischargeFromCans cans (fl,ev,clas,tys)
- = Bag.foldlBagM discharge_ct False cans
- where discharge_ct :: Bool -> CanonicalCt -> TcS Bool
- discharge_ct True _ct = return True
- discharge_ct False (CDictCan { cc_id = ev1, cc_flavor = fl1
- , cc_class = clas1, cc_tyargs = tys1 })
- | clas1 == clas
- , (and $ zipWith tcEqType tys tys1)
- , fl1 `canSolve` fl
- = setEvBind ev (EvId ev1) >> return True
- discharge_ct False _ct = return False
-\end{code}
+ ; sctx <- getTcSContext
-Note [Avoiding the superclass explosion]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ ; traceTcS "solveInteract, before clever canonicalization:" $
+ vcat [ text "ws = " <+> ppr (mapBag (\(EvVarX ev ct)
+ -> (ct,evVarPred ev)) ws)
+ , text "inert = " <+> ppr inert ]
+
+ ; can_ws <- mkCanonicalFEVs ws
+
+ ; (flag, inert_ret)
+ <- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws
-Consider the example:
- f = [(0,1,0,1,0)]
-We have 5 wanted (Num alpha) constraints. If we simply try to canonicalize and add them
-in our worklist, we will also get all of their superclasses as Derived, hence we will
-have an inert set that contains 5*n constraints, where n is the number of superclasses
-of of Num. That is bad for the additional reason that we keep *all* the Derived, even
-for identical class constraints (for reasons related to recursive dictionaries).
+ ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
+ vcat [ text "No interaction happened = " <+> ppr flag
+ , text "inert_ret = " <+> ppr inert_ret ]
-Instead, what we do with tryPreSolveAndCanon, is when we encounter a new constraint,
-such as the second (Num alpha) above we very quickly see if it can be immediately
-discharged by a class constraint in our inert set or the previous canonicals. If so,
-we add nothing to the returned canonical constraints.
+ ; return (flag, inert_ret) }
+
+tryPreSolveAndInteract :: SimplContext
+ -> DynFlags
+ -> CanonicalCt
+ -> (Bool, InertSet)
+ -> TcS (Bool, InertSet)
+-- Returns: True if it was able to discharge this constraint AND all previous ones
+tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert)
+ = do { let inert_cts = get_inert_cts (evVarPred ev_var)
+
+ ; this_one_discharged <-
+ if isCFrozenErr ct then
+ return False
+ else
+ dischargeFromCCans inert_cts ev_var fl
+
+ ; if this_one_discharged
+ then return (all_previous_discharged, inert)
+
+ else do
+ { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert
+ ; return (False, inert_ret) } }
+
+ where
+ ev_var = cc_id ct
+ fl = cc_flavor ct
+
+ get_inert_cts (ClassP clas _)
+ | simplEqsOnly sctx = emptyCCan
+ | otherwise = fst (getRelevantCts clas (inert_dicts inert))
+ get_inert_cts (IParam {})
+ = emptyCCan -- We must not do the same thing for IParams, because (contrary
+ -- to dictionaries), work items /must/ override inert items.
+ -- See Note [Overriding implicit parameters] in TcInteract.
+ get_inert_cts (EqPred {})
+ = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
+
+dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool
+-- See if this (pre-canonicalised) work-item is identical to a
+-- one already in the inert set. Reasons:
+-- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints
+-- b) Termination for improve_eqs in TcSimplify.simpl_loop
+dischargeFromCCans cans ev fl
+ = Bag.foldrBag discharge_ct (return False) cans
+ where
+ the_pred = evVarPred ev
+
+ discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool
+ discharge_ct ct _rest
+ | evVarPred (cc_id ct) `eqPred` the_pred
+ , cc_flavor ct `canSolve` fl
+ = do { when (isWanted fl) $ setEvBind ev (evVarTerm (cc_id ct))
+ -- Deriveds need no evidence
+ -- For Givens, we already have evidence, and we don't need it twice
+ ; return True }
+
+ discharge_ct _ct rest = rest
+\end{code}
-For our particular example this will reduce the size of the inert set that we use from
-5*n to just n. And hence the number of all possible interactions that we have to look
-through is significantly smaller!
+Note [Avoiding the superclass explosion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This note now is not as significant as it used to be because we no
+longer add the superclasses of Wanted as Derived, except only if they
+have equality superclasses or superclasses with functional
+dependencies. The fear was that hundreds of identical wanteds would
+give rise each to the same superclass or equality Derived's which
+would lead to a blo-up in the number of interactions.
+
+Instead, what we do with tryPreSolveAndCanon, is when we encounter a
+new constraint, we very quickly see if it can be immediately
+discharged by a class constraint in our inert set or the previous
+canonicals. If so, we add nothing to the returned canonical
+constraints.
\begin{code}
-solveOne :: InertSet -> WorkItem -> TcS InertSet
-solveOne inerts workItem
+solveOne :: WorkItem -> InertSet -> TcS InertSet
+solveOne workItem inerts
= do { dyn_flags <- getDynFlags
- ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
+ ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts
}
-----------------
solveInteractWithDepth :: (Int, Int, [WorkItem])
- -> InertSet -> WorkList -> TcS InertSet
-solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
+ -> WorkList -> InertSet -> TcS InertSet
+solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert
| isEmptyWorkList ws
= return inert
| otherwise
= do { traceTcS "solveInteractWithDepth" $
vcat [ text "Current depth =" <+> ppr n
- , text "Max depth =" <+> ppr max_depth ]
+ , text "Max depth =" <+> ppr max_depth
+ , text "ws =" <+> ppr ws ]
+
- -- Solve equalities first
- ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
- ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
- ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
+ ; foldrWorkListM (solveOneWithDepth ctxt) inert ws }
+ -- use foldr to preserve the order
------------------
-- Fully interact the given work item with an inert set, and return a
-- new inert set which has assimilated the new information.
solveOneWithDepth :: (Int, Int, [WorkItem])
- -> InertSet -> WorkItem -> TcS InertSet
-solveOneWithDepth (max_depth, n, stack) inert work
- = do { traceTcS0 (indent ++ "Solving {") (ppr work)
- ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
+ -> WorkItem -> InertSet -> TcS InertSet
+solveOneWithDepth (max_depth, depth, stack) work inert
+ = do { traceFireTcS depth (text "Solving {" <+> ppr work)
+ ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work
- ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
-
-- Recursively solve the new work generated
-- from workItem, with a greater depth
- ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
- new_inert new_work
+ ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_work new_inert
+
+ ; traceFireTcS depth (text "Done }" <+> ppr work)
- ; traceTcS0 (indent ++ "Done }") (ppr work)
; return res_inert }
- where
- indent = replicate (2*n) ' '
thePipeline :: [(String,SimplifierStage)]
thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
\begin{code}
spontaneousSolveStage :: SimplifierStage
-spontaneousSolveStage workItem inerts
+spontaneousSolveStage depth workItem inerts
= do { mSolve <- trySpontaneousSolve workItem
; case mSolve of
, sr_stop = ContinueWith workItem }
SPSolved workItem'
- | not (isGivenCt workItem)
+ | not (isGivenOrSolvedCt workItem)
-- Original was wanted or derived but we have now made him
-- given so we have to interact him with the inerts due to
-- its status change. This in turn may produce more work.
-- We do this *right now* (rather than just putting workItem'
-- back into the work-list) because we've solved
- -> do { (new_inert, new_work) <- runSolverPipeline
+ -> do { bumpStepCountTcS
+ ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem)
+ ; (new_inert, new_work) <- runSolverPipeline depth
[ ("recursive interact with inert eqs", interactWithInertEqsStage)
, ("recursive interact with inerts", interactWithInertsStage)
] inerts workItem'
| otherwise
-> -- Original was given; he must then be inert all right, and
-- workList' are all givens from flattening
- return $ SR { sr_new_work = emptyWorkList
- , sr_inerts = inerts `updInertSet` workItem'
- , sr_stop = Stop }
+ do { bumpStepCountTcS
+ ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem)
+ ; return $ SR { sr_new_work = emptyWorkList
+ , sr_inerts = inerts `updInertSet` workItem'
+ , sr_stop = Stop } }
SPError -> -- Return with no new work
return $ SR { sr_new_work = emptyWorkList
, sr_inerts = inerts
-- See Note [Touchables and givens]
trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
- | isGiven gw
+ | isGivenOrSolved gw
= return SPCantSolve
| Just tv2 <- tcGetTyVar_maybe xi
= do { tch1 <- isTouchableMetaTyVar tv1
| otherwise
= do { tch1 <- isTouchableMetaTyVar tv1
; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
- else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
+ else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:"
+ (ppr workItem)
; return SPCantSolve }
}
-- so we have its more specific kind in our hands
; if kxi `isSubKind` tyVarKind tv then
solveWithIdentity cv gw tv xi
- else if tyVarKind tv `isSubKind` kxi then
+ else return SPCantSolve
+{-
+ else if tyVarKind tv `isSubKind` kxi then
return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way
-- This case covers the a_touchable :: * ~ b_untouchable :: ??
-- which has to be deferred or floated out for someone else to solve
-- it in a scope where 'b' is no longer untouchable.
else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors]
; return SPError }
+-}
}
| otherwise -- Still can't solve, sig tyvar and non-variable rhs
= return SPCantSolve
| k2 `isSubKind` k1
= solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
| otherwise -- None is a subkind of the other, but they are both touchable!
- = do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
- ; return SPError }
+ = return SPCantSolve
+ -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
+ -- ; return SPError }
where
k1 = tyVarKind tv1
k2 = tyVarKind tv2
Note [Spontaneous solving and kind compatibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note that our canonical constraints insist that *all* equalities (tv ~
+xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
+the same kinds. ("compatible" means one is a subKind of the other.)
+
+ - It can't be *equal* kinds, because
+ b) wanted constraints don't necessarily have identical kinds
+ eg alpha::? ~ Int
+ b) a solved wanted constraint becomes a given
+
+ - SPJ thinks that *given* constraints (tv ~ tau) always have that
+ tau has a sub-kind of tv; and when solving wanted constraints
+ in trySpontaneousEqTwoWay we re-orient to achieve this.
-Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
-or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
-
- - We have to require this because:
- Given equalities can be freely used to rewrite inside
- other types or constraints.
- - We do not have to do the same for wanteds because:
- First, wanted equations (tv ~ xi) where tv is a touchable
- unification variable may have kinds that do not agree (the
- kind of xi must be a sub kind of the kind of tv). Second, any
- potential kind mismatch will result in the constraint not
- being soluble, which will be reported anyway. This is the
- reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
- will perform a kind compatibility check, and only then will
- they proceed to @solveWithIdentity@.
-
-Caveat:
+ - Note that the kind invariant is maintained by rewriting.
+ Eg wanted1 rewrites wanted2; if both were compatible kinds before,
+ wanted2 will be afterwards. Similarly givens.
+
+Caveat:
- Givens from higher-rank, such as:
type family T b :: * -> * -> *
type instance T Bool = (->)
text "Right Kind is : " <+> ppr (typeKind xi)
]
- ; setWantedTyBind tv xi -- Set tv := xi_unflat
- ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
-
- ; case wd of Wanted {} -> setWantedCoBind cv xi
- Derived {} -> setDerivedCoBind cv xi
- _ -> pprPanic "Can't spontaneously solve given!" empty
+ ; setWantedTyBind tv xi
+ ; let refl_xi = mkReflCo xi
+ ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_xi
+ ; when (isWanted wd) (setCoBind cv refl_xi)
+ -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
; return $ SPSolved (CTyEqCan { cc_id = cv_given
- , cc_flavor = mkGivenFlavor wd UnkSkol
- , cc_tyvar = tv, cc_rhs = xi })
- }
-
+ , cc_flavor = mkSolvedFlavor wd UnkSkol
+ , cc_tyvar = tv, cc_rhs = xi }) }
\end{code}
-
-
*********************************************************************************
* *
The interact-with-inert Stage
* *
*********************************************************************************
+Note [The Solver Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We always add Givens first. So you might think that the solver has
+the invariant
+
+ If the work-item is Given,
+ then the inert item must Given
+
+But this isn't quite true. Suppose we have,
+ c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
+After processing the first two, we get
+ c1: [G] beta ~ [alpha], c2 : [W] blah
+Now, c3 does not interact with the the given c1, so when we spontaneously
+solve c3, we must re-react it with the inert set. So we can attempt a
+reaction between inert c2 [W] and work-item c3 [G].
+
+It *is* true that [Solver Invariant]
+ If the work-item is Given,
+ AND there is a reaction
+ then the inert item must Given
+or, equivalently,
+ If the work-item is Given,
+ and the inert item is Wanted/Derived
+ then there is no reaction
+
\begin{code}
-- Interaction result of WorkItem <~> AtomicInert
data InteractResult
, ir_new_work :: WorkList
-- new work items to add to the WorkList
- , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in
+ , ir_fire :: Maybe String -- Tells whether a rule fired, and if so what
}
-- What to do with the inert reactant.
-data InertAction = KeepInert
- | DropInert
- | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert
+data InertAction = KeepInert | DropInert
-mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
-mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing
+mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
+mkIRContinue rule wi keep newWork
+ = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
+ , ir_new_work = newWork, ir_fire = Just rule }
-mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
-mkIRStop keep newWork = return $ IR Stop keep newWork Nothing
+mkIRStopK :: String -> WorkList -> TcS InteractResult
+mkIRStopK rule newWork
+ = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
+ , ir_new_work = newWork, ir_fire = Just rule }
-mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult
-mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr)
-
-dischargeWorkItem :: Monad m => m InteractResult
-dischargeWorkItem = mkIRStop KeepInert emptyWorkList
+mkIRStopD :: String -> WorkList -> TcS InteractResult
+mkIRStopD rule newWork
+ = return $ IR { ir_stop = Stop, ir_inert_action = DropInert
+ , ir_new_work = newWork, ir_fire = Just rule }
noInteraction :: Monad m => WorkItem -> m InteractResult
-noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
+noInteraction wi
+ = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
+ , ir_new_work = emptyWorkList, ir_fire = Nothing }
data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
-- See Note [Efficient Orientation]
---------------------------------------------------
--- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we
--- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've
+-- Interact a single WorkItem with the equalities of an inert set as
+-- far as possible, i.e. until we get a Stop result from an individual
+-- reaction (i.e. when the WorkItem is consumed), or until we've
-- interact the WorkItem with the entire equalities of the InertSet
interactWithInertEqsStage :: SimplifierStage
-interactWithInertEqsStage workItem inert
- = foldISEqCtsM interactNext initITR inert
- where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- Will fold over equalities
- , inert_dicts = inert_dicts inert
- , inert_ips = inert_ips inert
- , inert_funeqs = inert_funeqs inert
- , inert_fds = inert_fds inert
- }
- , sr_new_work = emptyWorkList
- , sr_stop = ContinueWith workItem }
-
+interactWithInertEqsStage depth workItem inert
+ = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert)
+ -- use foldr to preserve the order
+ where
+ initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan }
+ , sr_new_work = emptyWorkList
+ , sr_stop = ContinueWith workItem }
---------------------------------------------------
-- Interact a single WorkItem with *non-equality* constraints in the inert set.
-- "Other" constraints it contains!
interactWithInertsStage :: SimplifierStage
-interactWithInertsStage workItem inert
+interactWithInertsStage depth workItem inert
= let (relevant, inert_residual) = getISRelevant workItem inert
initITR = SR { sr_inerts = inert_residual
, sr_new_work = emptyWorkList
, sr_stop = ContinueWith workItem }
- in Bag.foldlBagM interactNext initITR relevant
+ in Bag.foldrBagM (interactNext depth) initITR relevant
+ -- use foldr to preserve the order
where
getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
- getISRelevant (CDictCan { cc_class = cls } ) is
- = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
+ getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
+ -- Nothing s relevant; we have alread interacted
+ -- it with the equalities in the inert set
+
+ getISRelevant (CDictCan { cc_class = cls } ) is
+ = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
in (relevant, is { inert_dicts = residual_map })
getISRelevant (CFunEqCan { cc_fun = tc } ) is
= let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
, inert_ips = emptyCCanMap
, inert_funeqs = emptyCCanMap })
-interactNext :: StageResult -> AtomicInert -> TcS StageResult
-interactNext it inert
- | ContinueWith workItem <- sr_stop it
- = do { let inerts = sr_inerts it
- fdimprs_old = getFDImprovements inerts
-
- ; ir <- interactWithInert fdimprs_old inert workItem
-
- -- New inerts depend on whether we KeepInert or not and must
- -- be updated with FD improvement information from the interaction result (ir)
- ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir)
- upd_inert = case ir_inert_action ir of
- KeepInert -> inerts `updInertSet` inert
- DropInert -> inerts
- KeepTransformedInert inert' -> inerts `updInertSet` inert'
+interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult
+interactNext depth inert it
+ | ContinueWith work_item <- sr_stop it
+ = do { let inerts = sr_inerts it
+
+ ; IR { ir_new_work = new_work, ir_inert_action = inert_action
+ , ir_fire = fire_info, ir_stop = stop }
+ <- interactWithInert inert work_item
+
+ ; let mk_msg rule
+ = text rule <+> keep_doc
+ <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
+ , ptext (sLit "Work =") <+> ppr work_item
+ , ppUnless (isEmptyWorkList new_work) $
+ ptext (sLit "New =") <+> ppr new_work ]
+ keep_doc = case inert_action of
+ KeepInert -> ptext (sLit "[keep]")
+ DropInert -> ptext (sLit "[drop]")
+ ; case fire_info of
+ Just rule -> do { bumpStepCountTcS
+ ; traceFireTcS depth (mk_msg rule) }
+ Nothing -> return ()
+
+ -- New inerts depend on whether we KeepInert or not
+ ; let inerts_new = case inert_action of
+ KeepInert -> inerts `updInertSet` inert
+ DropInert -> inerts
; return $ SR { sr_inerts = inerts_new
- , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
- , sr_stop = ir_stop ir } }
+ , sr_new_work = sr_new_work it `unionWorkList` new_work
+ , sr_stop = stop } }
| otherwise
= return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
-- Do a single interaction of two constraints.
-interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult
-interactWithInert fdimprs inert workitem
- = do { ctxt <- getTcSContext
- ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
- inert_ev = cc_id inert
- work_ev = cc_id workitem
-
- -- Never interact a wanted and a derived where the derived's evidence
- -- mentions the wanted evidence in an unguarded way.
- -- See Note [Superclasses and recursive dictionaries]
- -- and Note [New Wanted Superclass Work]
- -- We don't have to do this for givens, as we fully know the evidence for them.
- ; rec_ev_ok <-
- case (cc_flavor inert, cc_flavor workitem) of
- (Wanted {}, Derived {}) -> isGoodRecEv work_ev inert_ev
- (Derived {}, Wanted {}) -> isGoodRecEv inert_ev work_ev
- _ -> return True
-
- ; if is_allowed && rec_ev_ok then
- doInteractWithInert fdimprs inert workitem
+interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
+interactWithInert inert workItem
+ = do { ctxt <- getTcSContext
+ ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workItem
+
+ ; if is_allowed then
+ doInteractWithInert inert workItem
else
- noInteraction workitem
- }
+ noInteraction workItem
+ }
allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
-- Allowed interactions
allowedInteraction _ _ _ = True
--------------------------------------------
-doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult
+doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
-- Identical class constraints.
-doInteractWithInert fdimprs
- (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
- workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
- | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
- = solveOneFromTheOther (d1,fl1) workItem
+doInteractWithInert
+ inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
+ workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
- | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
- = -- See Note [When improvement happens]
- do { let pty1 = ClassP cls1 tys1
+ | cls1 == cls2
+ = do { let pty1 = ClassP cls1 tys1
pty2 = ClassP cls2 tys2
- work_item_pred_loc = (pty2, pprFlavorArising fl2)
inert_pred_loc = (pty1, pprFlavorArising fl1)
- loc = combineCtLoc fl1 fl2
- eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
- -- See Note [Efficient Orientation]
-
- ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
- ; fd_work <- canWanteds wevvars
- -- See Note [Generating extra equalities]
- ; traceTcS "Checking if improvements existed." (ppr fdimprs)
- ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
- -- Must keep going
- mkIRContinue workItem KeepInert fd_work
- else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
- ; mkIRStop_RecordImprovement KeepInert
- (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
- }
- -- See Note [FunDep Reactions]
+ work_item_pred_loc = (pty2, pprFlavorArising fl2)
+
+ ; any_fundeps
+ <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
+ -- NB: We don't create fds for given (and even solved), have not seen a useful
+ -- situation for these and even if we did we'd have to be very careful to only
+ -- create Derived's and not Wanteds.
+
+ else let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
+ wloc = get_workitem_wloc fl2
+ in rewriteWithFunDeps fd_eqns tys2 wloc
+ -- See Note [Efficient Orientation], [When improvement happens]
+
+ ; case any_fundeps of
+ -- No Functional Dependencies
+ Nothing
+ | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
+ | otherwise -> noInteraction workItem
+
+ -- Actual Functional Dependencies
+ Just (rewritten_tys2,cos2,fd_work)
+ | not (eqTypes tys1 rewritten_tys2)
+ -- Standard thing: create derived fds and keep on going. Importantly we don't
+ -- throw workitem back in the worklist because this can cause loops. See #5236.
+ -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
+ ; mkIRContinue "Cls/Cls fundep (not solved)" workItem KeepInert fd_cans }
+
+ -- This WHOLE otherwise branch is an optimization where the fd made the things match
+ | otherwise
+ , let dict_co = mkTyConAppCo (classTyCon cls1) cos2
+ -> case fl2 of
+ Given {}
+ -> pprPanic "Unexpected given!" (ppr inertItem $$ ppr workItem)
+ -- The only way to have created a fundep is if the inert was
+ -- wanted or derived, in which case the workitem can't be given!
+ Derived {}
+ -- The types were made to exactly match so we don't need
+ -- the workitem any longer.
+ -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
+ -- No rewriting really, so let's create deriveds fds
+ ; mkIRStopK "Cls/Cls fundep (solved)" fd_cans }
+ Wanted {}
+ | isDerived fl1
+ -> do { setDictBind d2 (EvCast d1 dict_co)
+ ; let inert_w = inertItem { cc_flavor = fl2 }
+ -- A bit naughty: we take the inert Derived,
+ -- turn it into a Wanted, use it to solve the work-item
+ -- and put it back into the work-list
+ -- Maybe rather than starting again, we could keep going
+ -- with the rewritten workitem, having dropped the inert, but its
+ -- safe to restart.
+
+ -- Also: we have rewriting so lets create wanted fds
+ ; fd_cans <- mkCanonicalFDAsWanted fd_work
+ ; mkIRStopD "Cls/Cls fundep (solved)" $
+ workListFromNonEq inert_w `unionWorkList` fd_cans }
+ | otherwise
+ -> do { setDictBind d2 (EvCast d1 dict_co)
+ -- Rewriting is happening, so we have to create wanted fds
+ ; fd_cans <- mkCanonicalFDAsWanted fd_work
+ ; mkIRStopK "Cls/Cls fundep (solved)" fd_cans }
}
+ where get_workitem_wloc (Wanted wl) = wl
+ get_workitem_wloc (Derived wl) = wl
+ get_workitem_wloc (Given {}) = panic "Unexpected given!"
+
-- Class constraint and given equality: use the equality to rewrite
-- the class constraint.
-doInteractWithInert _fdimprs
- (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
+doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
(CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
| ifl `canRewrite` wfl
, tv `elemVarSet` tyVarsOfTypes xis
= do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
-- Continue with rewritten Dictionary because we can only be in the
-- interactWithEqsStage, so the dictionary is inert.
- ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
+ ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
-doInteractWithInert _fdimprs
- (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
+doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfTypes xis
= do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
+ ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) }
-- Class constraint and given equality: use the equality to rewrite
-- the class constraint.
-doInteractWithInert _fdimprs
- (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
+doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
(CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
| ifl `canRewrite` wfl
, tv `elemVarSet` tyVarsOfType ty
= do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
- ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
+ ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList }
-doInteractWithInert _fdimprs
- (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
+doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfType ty
= do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
+ ; mkIRContinue "IP/Eq" workItem DropInert (workListFromNonEq rewritten_ip) }
-- Two implicit parameter constraints. If the names are the same,
-- but their types are not, we generate a wanted type equality
-- that equates the type (this is "improvement").
-- However, we don't actually need the coercion evidence,
-- so we just generate a fresh coercion variable that isn't used anywhere.
-doInteractWithInert _fdimprs
- (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
+doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
- | nm1 == nm2 && isGiven wfl && isGiven ifl
+ | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
= -- See Note [Overriding implicit parameters]
-- Dump the inert item, override totally with the new one
-- Do not require type equality
- mkIRContinue workItem DropInert emptyWorkList
+ -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
+ -- we must *override* the outer one with the inner one
+ mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
- | nm1 == nm2 && ty1 `tcEqType` ty2
- = solveOneFromTheOther (id1,ifl) workItem
+ | nm1 == nm2 && ty1 `eqType` ty2
+ = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
| nm1 == nm2
= -- See Note [When improvement happens]
- do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
- ; let flav = Wanted (combineCtLoc ifl wfl)
- ; cans <- mkCanonical flav co_var
- ; mkIRContinue workItem KeepInert cans }
-
-
+ do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation]
+ ; let flav = Wanted (combineCtLoc ifl wfl)
+ ; cans <- mkCanonical flav co_var
+ ; case wfl of
+ Given {} -> pprPanic "Unexpected given IP" (ppr workItem)
+ Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
+ Wanted {} ->
+ do { setIPBind (cc_id workItem) $
+ EvCast id1 (mkSymCo (mkCoVarCo co_var))
+ ; mkIRStopK "IP/IP interaction (solved)" cans }
+ }
-- Never rewrite a given with a wanted equality, and a type function
-- equality can never rewrite an equality. We rewrite LHS *and* RHS
-- we know about equalities.
-- Inert: equality, work item: function equality
-doInteractWithInert _fdimprs
- (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
+doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
(CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
, cc_tyargs = args, cc_rhs = xi2 })
| ifl `canRewrite` wfl
, tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
= do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
- ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
+ ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) }
-- Must Stop here, because we may no longer be inert after the rewritting.
-- Inert: function equality, work item: equality
-doInteractWithInert _fdimprs
- (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
+doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
, cc_tyargs = args, cc_rhs = xi1 })
workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
= do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
+ ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromEq rewritten_funeq) }
-- One may think that we could (KeepTransformedInert rewritten_funeq)
-- but that is wrong, because it may end up not being inert with respect
-- to future inerts. Example:
-- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] }
-- At the end, which is *not* inert. So we should unfortunately DropInert here.
-doInteractWithInert _fdimprs
- (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
+doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
, cc_tyargs = args1, cc_rhs = xi1 })
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
+ | tc1 == tc2 && and (zipWith eqType args1 args2)
+ , Just GivenSolved <- isGiven_maybe fl1
+ = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
+ | tc1 == tc2 && and (zipWith eqType args1 args2)
+ , Just GivenSolved <- isGiven_maybe fl2
+ = mkIRStopK "Funeq/Funeq" emptyWorkList
+
| fl1 `canSolve` fl2 && lhss_match
- = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
- ; mkIRStop KeepInert cans }
+ = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
+ ; mkIRStopK "FunEq/FunEq" cans }
| fl2 `canSolve` fl1 && lhss_match
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
- ; mkIRContinue workItem DropInert cans }
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
+ ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
where
- lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
+ lhss_match = tc1 == tc2 && eqTypes args1 args2
-doInteractWithInert _fdimprs
- (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
+doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
-- Check for matching LHS
| fl1 `canSolve` fl2 && tv1 == tv2
- = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
- ; mkIRStop KeepInert cans }
+ = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
+ ; mkIRStopK "Eq/Eq lhs" cans }
| fl2 `canSolve` fl1 && tv1 == tv2
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
- ; mkIRContinue workItem DropInert cans }
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
+ ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
+
-- Check for rewriting RHS
| fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
= do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
- ; mkIRStop KeepInert rewritten_eq }
+ ; mkIRStopK "Eq/Eq rhs" rewritten_eq }
+
| fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
= do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
- ; mkIRContinue workItem DropInert rewritten_eq }
+ ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq }
+
+doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
+ (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
+ | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
+ = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
+ ; mkIRStopK "Frozen/Eq" rewritten_frozen }
+
+doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
+ workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
+ | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
+ = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
+ ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }
-- Fall-through case for all other situations
-doInteractWithInert _fdimprs _ workItem = noInteraction workItem
+doInteractWithInert _ workItem = noInteraction workItem
-------------------------
-- Equational Rewriting
rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
- = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
+ = do { let cos = map (liftCoSubstWith [tv] [mkCoVarCo cv]) xis -- xis[tv] ~ xis[xi]
args = substTysWith [tv] [xi] xis
con = classTyCon cl
- dict_co = mkTyConCoercion con cos
+ dict_co = mkTyConAppCo con cos
; dv' <- newDictVar cl args
; case gw of
- Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
- _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
+ Wanted {} -> setDictBind dv (EvCast dv' (mkSymCo dict_co))
+ Given {} -> setDictBind dv' (EvCast dv dict_co)
+ Derived {} -> return () -- Derived dicts we don't set any evidence
+
; return (CDictCan { cc_id = dv'
, cc_flavor = gw
, cc_class = cl
rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
- = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
- ty' = substTyWith [tv] [xi] ty
+ = do { let ip_co = liftCoSubstWith [tv] [mkCoVarCo cv] ty -- ty[tv] ~ t[xi]
+ ty' = substTyWith [tv] [xi] ty
; ipid' <- newIPVar nm ty'
; case gw of
- Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
- _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
+ Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCo ip_co))
+ Given {} -> setIPBind ipid' (EvCast ipid ip_co)
+ Derived {} -> return () -- Derived ips: we don't set any evidence
+
; return (CIPCan { cc_id = ipid'
, cc_flavor = gw
, cc_ip_nm = nm
rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
- = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
- args' = substTysWith [tv] [xi1] args
- fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args'
+ = do { let co_subst = liftCoSubstWith [tv] [mkCoVarCo cv1]
+ arg_cos = map co_subst args
+ args' = substTysWith [tv] [xi1] args
+ fun_co = mkTyConAppCo tc arg_cos -- fun_co :: F args ~ F args'
xi2' = substTyWith [tv] [xi1] xi2
- xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2'
- ; cv2' <- case gw of
- Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2'
- ; setWantedCoBind cv2 $
- fun_co `mkTransCoercion`
- mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co
- ; return cv2' }
- _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2' $
- mkSymCoercion fun_co `mkTransCoercion`
- mkCoVarCoercion cv2 `mkTransCoercion` xi2_co
+ xi2_co = co_subst xi2 -- xi2_co :: xi2 ~ xi2'
+
+ ; cv2' <- newCoVar (mkTyConApp tc args') xi2'
+ ; case gw of
+ Wanted {} -> setCoBind cv2 (fun_co `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo xi2_co)
+ Given {} -> setCoBind cv2' (mkSymCo fun_co `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
+ xi2_co)
+ Derived {} -> return ()
+
; return (CFunEqCan { cc_id = cv2'
, cc_flavor = gw
, cc_tyargs = args'
rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
| Just tv2' <- tcGetTyVar_maybe xi2'
, tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
- = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
- ; return emptyCCan }
+ = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2'))
+ ; return emptyWorkList }
| otherwise
- = do { cv2' <-
- case gw of
- Wanted {}
- -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
- ; setWantedCoBind cv2 $
- mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
- ; return cv2' }
- _giv_or_der
- -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
- mkCoVarCoercion cv2 `mkTransCoercion` co2'
-
- ; canEq gw cv2' (mkTyVarTy tv2) xi2'
- }
+ = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
+ ; case gw of
+ Wanted {} -> setCoBind cv2 $ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo co2'
+ Given {} -> setCoBind cv2' $ mkCoVarCo cv2 `mkTransCo`
+ co2'
+ Derived {} -> return ()
+ ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
where
xi2' = substTyWith [tv1] [xi1] xi2
- co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
-
+ co2' = liftCoSubstWith [tv1] [mkCoVarCo cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
-- Used to ineract two equalities of the following form:
-- First Equality: co1: (XXX ~ xi1)
-- Second Equality: cv2: (XXX ~ xi2)
--- Where the cv1 `canSolve` cv2 equality
+-- Where the cv1 `canRewrite` cv2 equality
-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
-- See Note [Efficient Orientation] for that
-rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
- = do { cv2' <- case (isWanted gw, which) of
- (True,LeftComesFromInert) ->
- do { cv2' <- newWantedCoVar xi2 xi1
- ; setWantedCoBind cv2 $
- co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
- ; return cv2' }
- (True,RightComesFromInert) ->
- do { cv2' <- newWantedCoVar xi1 xi2
- ; setWantedCoBind cv2 $
- co1 `mkTransCoercion` mkCoVarCoercion cv2'
- ; return cv2' }
- (False,LeftComesFromInert) ->
- newGivOrDerCoVar xi2 xi1 $
- mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
- (False,RightComesFromInert) ->
- newGivOrDerCoVar xi1 xi2 $
- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
- ; mkCanonical gw cv2'
- }
-
-solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
--- First argument inert, second argument workitem. They both represent
--- wanted/given/derived evidence for the *same* predicate so we try here to
--- discharge one directly from the other.
+rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2)
+ = do { cv2' <- newCoVar xi2 xi1
+ ; case gw of
+ Wanted {} -> setCoBind cv2 $
+ co1 `mkTransCo` mkSymCo (mkCoVarCo cv2')
+ Given {} -> setCoBind cv2' $
+ mkSymCo (mkCoVarCo cv2) `mkTransCo` co1
+ Derived {} -> return ()
+ ; mkCanonical gw cv2' }
+
+rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2)
+ = do { cv2' <- newCoVar xi1 xi2
+ ; case gw of
+ Wanted {} -> setCoBind cv2 $
+ co1 `mkTransCo` mkCoVarCo cv2'
+ Given {} -> setCoBind cv2' $
+ mkSymCo co1 `mkTransCo` mkCoVarCo cv2
+ Derived {} -> return ()
+ ; mkCanonical gw cv2' }
+
+rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList
+rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
+ = do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
+ ; case fl2 of
+ Wanted {} -> setCoBind cv2 $ co2a' `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo co2b'
+
+ Given {} -> setCoBind cv2' $ mkSymCo co2a' `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
+ co2b'
+
+ Derived {} -> return ()
+
+ ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
+ where
+ (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b
+ ty2a' = substTyWith [tv1] [xi1] ty2a
+ ty2b' = substTyWith [tv1] [xi1] ty2b
+
+ co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
+ co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
+
+solveOneFromTheOther_ExtraWork :: String -> (EvTerm, CtFlavor)
+ -> CanonicalCt -> WorkList -> TcS InteractResult
+-- First argument inert, second argument work-item. They both represent
+-- wanted/given/derived evidence for the *same* predicate so
+-- we can discharge one directly from the other.
--
-- Precondition: value evidence only (implicit parameters, classes)
-- not coercion
-solveOneFromTheOther (iid,ifl) workItem
- -- Both derived needs a special case. You might think that we do not need
- -- two evidence terms for the same claim. But, since the evidence is partial,
- -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
- -- See also Example 3 in Note [Superclasses and recursive dictionaries]
- | isDerived ifl && isDerived wfl
- = noInteraction workItem
-
- | ifl `canSolve` wfl
- = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
- -- Overwrite the binding, if one exists
- -- For Givens, which are lambda-bound, nothing to overwrite,
- ; dischargeWorkItem }
-
- | otherwise -- wfl `canSolve` ifl
- = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
- ; mkIRContinue workItem DropInert emptyWorkList }
+solveOneFromTheOther_ExtraWork info (ev_term,ifl) workItem extra_work
+ | isDerived wfl
+ = mkIRStopK ("Solved[DW] " ++ info) extra_work
+
+ | isDerived ifl -- The inert item is Derived, we can just throw it away,
+ -- The workItem is inert wrt earlier inert-set items,
+ -- so it's safe to continue on from this point
+ = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert extra_work
+
+ | Just GivenSolved <- isGiven_maybe ifl, isGivenOrSolved wfl
+ -- Same if the inert is a GivenSolved -- just get rid of it
+ = mkIRContinue ("Solved[SI] " ++ info) workItem DropInert extra_work
+ | otherwise
+ = ASSERT( ifl `canSolve` wfl )
+ -- Because of Note [The Solver Invariant], plus Derived dealt with
+ do { when (isWanted wfl) $ setEvBind wid ev_term
+ -- Overwrite the binding, if one exists
+ -- If both are Given, we already have evidence; no need to duplicate
+ ; mkIRStopK ("Solved " ++ info) extra_work }
where
wfl = cc_flavor workItem
wid = cc_id workItem
+
+
+solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
+solveOneFromTheOther str evfl ct
+ = solveOneFromTheOther_ExtraWork str evfl ct emptyWorkList -- extra work is empty
+
\end{code}
Note [Superclasses and recursive dictionaries]
When we simplify a wanted constraint, if we first see a matching
instance, we may produce new wanted work. To (1) avoid doing this work
twice in the future and (2) to handle recursive dictionaries we may ``cache''
-this item as solved (in effect, given) into our inert set and with that add
-its superclass constraints (as given) in our worklist.
+this item as given into our inert set WITHOUT adding its superclass constraints,
+otherwise we'd be in danger of creating a loop [In fact this was the exact reason
+for doing the isGoodRecEv check in an older version of the type checker].
But now we have added partially solved constraints to the worklist which may
interact with other wanteds. Consider the example:
instance Eq a => Foo [a] a --- fooDFun
and wanted (Foo [t] t). We are first going to see that the instance matches
-and create an inert set that includes the solved (Foo [t] t) and its
-superclasses.
+and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
- d2 :_g Eq t d2 := EvSuperClass d1 0
Our work list is going to contain a new *wanted* goal
d3 :_w Eq t
-It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
-construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
-OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
-at all? Consider
+Ok, so how do we get recursive dictionaries, at all:
Example 2:
\begin{code}
-- If a work item has any form of interaction with top-level we get this
data TopInteractResult
- = NoTopInt -- No top-level interaction
+ = NoTopInt -- No top-level interaction
+ -- Equivalent to (SomeTopInt emptyWorkList (ContinueWith work_item))
| SomeTopInt
{ tir_new_work :: WorkList -- Sub-goals or new work (could be given,
-- for superclasses)
-- only reacted with functional dependencies
-- arising from top-level instances.
-topReactionsStage :: SimplifierStage
-topReactionsStage workItem inerts
- = do { tir <- tryTopReact workItem
- ; case tir of
- NoTopInt ->
- return $ SR { sr_inerts = inerts
- , sr_new_work = emptyWorkList
- , sr_stop = ContinueWith workItem }
- SomeTopInt tir_new_work tir_new_inert ->
- return $ SR { sr_inerts = inerts
- , sr_new_work = tir_new_work
- , sr_stop = tir_new_inert
- }
+topReactionsStage :: SimplifierStage
+topReactionsStage depth workItem inerts
+ = do { tir <- tryTopReact inerts workItem
+ -- NB: we pass the inerts as well. See Note [Instance and Given overlap]
+ ; case tir of
+ NoTopInt ->
+ return $ SR { sr_inerts = inerts
+ , sr_new_work = emptyWorkList
+ , sr_stop = ContinueWith workItem }
+ SomeTopInt tir_new_work tir_new_inert ->
+ do { bumpStepCountTcS
+ ; traceFireTcS depth (ptext (sLit "Top react")
+ <+> vcat [ ptext (sLit "Work =") <+> ppr workItem
+ , ptext (sLit "New =") <+> ppr tir_new_work ])
+ ; return $ SR { sr_inerts = inerts
+ , sr_new_work = tir_new_work
+ , sr_stop = tir_new_inert
+ } }
}
-tryTopReact :: WorkItem -> TcS TopInteractResult
-tryTopReact workitem
+tryTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
+tryTopReact inerts workitem
= do { -- A flag controls the amount of interaction allowed
-- See Note [Simplifying RULE lhs constraints]
ctxt <- getTcSContext
; if allowedTopReaction (simplEqsOnly ctxt) workitem
then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
- ; doTopReact workitem }
+ ; doTopReact inerts workitem }
else return NoTopInt
}
-allowedTopReaction :: Bool -> WorkItem -> Bool
+allowedTopReaction :: Bool -> WorkItem -> Bool
allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
-allowedTopReaction _ _ = True
+allowedTopReaction _ _ = True
-
-doTopReact :: WorkItem -> TcS TopInteractResult
+doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
-- The work item does not react with the inert set, so try interaction with top-level instances
-- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
-- added in the worklist as part of the canonicalisation process.
-- Given dictionary
-- See Note [Given constraint that matches an instance declaration]
-doTopReact (CDictCan { cc_flavor = Given {} })
+doTopReact _inerts (CDictCan { cc_flavor = Given {} })
= return NoTopInt -- NB: Superclasses already added since it's canonical
-- Derived dictionary: just look for functional dependencies
-doTopReact workItem@(CDictCan { cc_flavor = Derived loc _
- , cc_class = cls, cc_tyargs = xis })
- = do { fd_work <- findClassFunDeps cls xis loc
- ; if isEmptyWorkList fd_work then
- return NoTopInt
- else return $ SomeTopInt { tir_new_work = fd_work
- , tir_new_inert = ContinueWith workItem } }
+doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
+ , cc_class = cls, cc_tyargs = xis })
+ = do { instEnvs <- getInstEnvs
+ ; let fd_eqns = improveFromInstEnv instEnvs
+ (ClassP cls xis, pprArisingAt loc)
+ ; m <- rewriteWithFunDeps fd_eqns xis loc
+ ; case m of
+ Nothing -> return NoTopInt
+ Just (xis',_,fd_work) ->
+ let workItem' = workItem { cc_tyargs = xis' }
+ -- Deriveds are not supposed to have identity (cc_id is unused!)
+ in do { fd_cans <- mkCanonicalFDAsDerived fd_work
+ ; return $ SomeTopInt { tir_new_work = fd_cans
+ , tir_new_inert = ContinueWith workItem' }
+ }
+ }
+
+
-- Wanted dictionary
-doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
- , cc_class = cls, cc_tyargs = xis })
- = do { -- See Note [MATCHING-SYNONYMS]
- ; lkp_inst_res <- matchClassInst cls xis loc
- ; case lkp_inst_res of
- NoInstance ->
- do { traceTcS "doTopReact/ no class instance for" (ppr dv)
- ; fd_work <- findClassFunDeps cls xis loc
- ; if isEmptyWorkList fd_work then
- return $ SomeTopInt
- { tir_new_work = emptyWorkList
- , tir_new_inert = ContinueWith workItem }
- else -- More fundep work produced, just thow him back in the
- -- worklist to prioritize the solution of fd equalities
- return $ SomeTopInt
- { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem
- , tir_new_inert = Stop } }
-
- GenInst wtvs ev_term -> -- Solved
- -- No need to do fundeps stuff here; the instance
- -- matches already so we won't get any more info
- -- from functional dependencies
- do { traceTcS "doTopReact/ found class instance for" (ppr dv)
- ; setDictBind dv ev_term
- ; inst_work <- canWanteds wtvs
- ; if null wtvs
- -- Solved in one step and no new wanted work produced.
- -- i.e we directly matched a top-level instance
- -- No point in caching this in 'inert'
- then return $ SomeTopInt { tir_new_work = emptyWorkList
- , tir_new_inert = Stop }
-
- -- Solved and new wanted work produced, you may cache the
- -- (tentatively solved) dictionary as Derived
- else do { let solved = makeSolvedByInst workItem
- ; return $ SomeTopInt
- { tir_new_work = inst_work
- , tir_new_inert = ContinueWith solved } }
- } }
+doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
+ , cc_class = cls, cc_tyargs = xis })
+ -- See Note [MATCHING-SYNONYMS]
+ = do { traceTcS "doTopReact" (ppr workItem)
+ ; instEnvs <- getInstEnvs
+ ; let fd_eqns = improveFromInstEnv instEnvs $ (ClassP cls xis, pprArisingAt loc)
+
+ ; any_fundeps <- rewriteWithFunDeps fd_eqns xis loc
+ ; case any_fundeps of
+ -- No Functional Dependencies
+ Nothing ->
+ do { lkup_inst_res <- matchClassInst inerts cls xis loc
+ ; case lkup_inst_res of
+ GenInst wtvs ev_term
+ -> doSolveFromInstance wtvs ev_term workItem emptyWorkList
+ NoInstance
+ -> return NoTopInt
+ }
+ -- Actual Functional Dependencies
+ Just (xis',cos,fd_work) ->
+ do { lkup_inst_res <- matchClassInst inerts cls xis' loc
+ ; case lkup_inst_res of
+ NoInstance
+ -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
+ ; return $
+ SomeTopInt { tir_new_work = fd_cans
+ , tir_new_inert = ContinueWith workItem } }
+ -- This WHOLE branch is an optimization: we can immediately discharge the dictionary
+ GenInst wtvs ev_term
+ -> do { let dict_co = mkTyConAppCo (classTyCon cls) cos
+ ; fd_cans <- mkCanonicalFDAsWanted fd_work
+ ; dv' <- newDictVar cls xis'
+ ; setDictBind dv' ev_term
+ ; doSolveFromInstance wtvs (EvCast dv' dict_co) workItem fd_cans }
+ } }
+
+ where doSolveFromInstance :: [WantedEvVar]
+ -> EvTerm
+ -> CanonicalCt
+ -> WorkList -> TcS TopInteractResult
+ -- Precondition: evidence term matches the predicate of cc_id of workItem
+ doSolveFromInstance wtvs ev_term workItem extra_work
+ | null wtvs
+ = do { traceTcS "doTopReact/found nullary instance for" (ppr (cc_id workItem))
+ ; setDictBind (cc_id workItem) ev_term
+ ; return $ SomeTopInt { tir_new_work = extra_work
+ , tir_new_inert = Stop } }
+ | otherwise
+ = do { traceTcS "doTopReact/found non-nullary instance for" (ppr (cc_id workItem))
+ ; setDictBind (cc_id workItem) ev_term
+ -- Solved and new wanted work produced, you may cache the
+ -- (tentatively solved) dictionary as Solved given.
+ ; let solved = workItem { cc_flavor = solved_fl }
+ solved_fl = mkSolvedFlavor fl UnkSkol
+ ; inst_work <- canWanteds wtvs
+ ; return $ SomeTopInt { tir_new_work = inst_work `unionWorkList` extra_work
+ , tir_new_inert = ContinueWith solved } }
+
-- Type functions
-doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
- , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
+doTopReact _inerts (CFunEqCan { cc_flavor = fl })
+ | Just GivenSolved <- isGiven_maybe fl
+ = return NoTopInt -- If Solved, no more interactions should happen
+
+-- Otherwise, it's a Given, Derived, or Wanted
+doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, cc_flavor = fl
+ , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
= ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
; case match_res of
- MatchInstNo
- -> return NoTopInt
+ MatchInstNo -> return NoTopInt
MatchInstSingle (rep_tc, rep_tys)
-> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
-- RHS of a type function, so that it never
-- appears in an error message
-- See Note [Type synonym families] in TyCon
- coe = mkTyConApp coe_tc rep_tys
- ; cv' <- case fl of
- Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
- ; setWantedCoBind cv $
- coe `mkTransCoercion`
- mkCoVarCoercion cv'
- ; return cv' }
- _ -> newGivOrDerCoVar xi rhs_ty $
- mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
-
- ; can_cts <- mkCanonical fl cv'
- ; return $ SomeTopInt can_cts Stop }
+ coe = mkAxInstCo coe_tc rep_tys
+ ; case fl of
+ Wanted {} -> do { cv' <- newCoVar rhs_ty xi
+ ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv'
+ ; can_cts <- mkCanonical fl cv'
+ ; let solved = workItem { cc_flavor = solved_fl }
+ solved_fl = mkSolvedFlavor fl UnkSkol
+ ; if isEmptyWorkList can_cts then
+ return (SomeTopInt can_cts Stop) -- No point in caching
+ else return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = ContinueWith solved }
+ }
+ Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $
+ mkSymCo (mkCoVarCo cv) `mkTransCo` coe
+ ; can_cts <- mkCanonical fl cv'
+ ; return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = Stop }
+ }
+ Derived {} -> do { cv' <- newDerivedId (EqPred xi rhs_ty)
+ ; can_cts <- mkCanonical fl cv'
+ ; return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = Stop }
+ }
+ }
_
-> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
}
-- Any other work item does not react with any top-level equations
-doTopReact _workItem = return NoTopInt
-
-----------------------
-findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList
--- Look for a fundep reaction beween the wanted item
--- and a top-level instance declaration
-findClassFunDeps cls xis loc
- = do { instEnvs <- getInstEnvs
- ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
- (ClassP cls xis, pprArisingAt loc)
- ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
- -- NB: fundeps generate some wanted equalities, but
- -- we don't use their evidence for anything
- ; canWanteds wevvars }
+doTopReact _inerts _workItem = return NoTopInt
\end{code}
Note [New Wanted Superclass Work]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Even in the case of wanted constraints, we add all of its superclasses as
-new given work. There are several reasons for this:
- a) to minimise error messages;
- eg suppose we have wanted (Eq a, Ord a)
- then we report only (Ord a) unsoluble
-
- b) to make the smallest number of constraints when *inferring* a type
- (same Eq/Ord example)
-
- c) for recursive dictionaries we *must* add the superclasses
- so that we can use them when solving a sub-problem
+Even in the case of wanted constraints, we may add some superclasses
+as new given work. The reason is:
- d) To allow FD-like improvement for type families. Assume that
+ To allow FD-like improvement for type families. Assume that
we have a class
class C a b | a -> b
and we have to solve the implication constraint:
equalities that have a touchable in their RHS, *in addition*
to solving wanted equalities.
-Here is another example where this is useful.
+We also need to somehow use the superclasses to quantify over a minimal,
+constraint see note [Minimize by Superclasses] in TcSimplify.
+
+
+Finally, here is another example where this is useful.
Example 1:
----------
that participate in recursive dictionary bindings.
\begin{code}
-
-
data LookupInstResult
= NoInstance
| GenInst [WantedEvVar] EvTerm
-matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
-matchClassInst clas tys loc
+matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
+matchClassInst inerts clas tys loc
= do { let pred = mkClassPred clas tys
; mb_result <- matchClass clas tys
+ ; untch <- getUntouchables
; case mb_result of
MatchInstNo -> return NoInstance
- MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
+ MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
-- we learn more about the reagent
- MatchInstSingle (dfun_id, mb_inst_tys) ->
+ MatchInstSingle (_,_)
+ | given_overlap untch ->
+ do { traceTcS "Delaying instance application" $
+ vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys)
+ , text "Silents and their superclasses=" <+> ppr silents_and_their_scs
+ , text "All given dictionaries=" <+> ppr all_given_dicts ]
+ ; return NoInstance -- see Note [Instance and Given overlap]
+ }
+
+ MatchInstSingle (dfun_id, mb_inst_tys) ->
do { checkWellStagedDFun pred dfun_id loc
-- It's possible that not all the tyvars are in
-- (presumably there's a functional dependency in class C)
-- Hence mb_inst_tys :: Either TyVar TcType
- ; tys <- instDFunTypes mb_inst_tys
+ ; tys <- instDFunTypes mb_inst_tys
; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
; if null theta then
- return (GenInst [] (EvDFunApp dfun_id tys [] []))
+ return (GenInst [] (EvDFunApp dfun_id tys []))
else do
{ ev_vars <- instDFunConstraints theta
- ; let wevs = [WantedEvVar w loc | w <- ev_vars]
- ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars ev_vars) }
- -- NB: All the dependencies are ev_vars
+ ; let wevs = [EvVarX w loc | w <- ev_vars]
+ ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }
}
}
+ where given_overlap :: TcsUntouchables -> Bool
+ given_overlap untch
+ = foldlBag (\r d -> r || matchable untch d) False all_given_dicts
+
+ matchable untch (CDictCan { cc_class = clas', cc_tyargs = sys, cc_flavor = fl })
+ | Just GivenOrig <- isGiven_maybe fl
+ , clas' == clas
+ , does_not_originate_in_a_silent clas' sys
+ = case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv &&
+ tv `elemVarSet` tyVarsOfTypes tys
+ then BindMe else Skolem) tys sys of
+ -- We can't learn anything more about any variable at this point, so the only
+ -- cause of overlap can be by an instantiation of a touchable unification
+ -- variable. Hence we only bind touchable unification variables. In addition,
+ -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
+ Nothing -> False
+ Just _ -> True
+ | otherwise = False -- No overlap with a solved, already been taken care of
+ -- by the overlap check with the instance environment.
+ matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
+
+ does_not_originate_in_a_silent clas sys
+ -- UGLY: See Note [Silent parameters overlapping]
+ = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs
+
+ silents_and_their_scs
+ = foldlBag (\acc rvnt -> case rvnt of
+ CDictCan { cc_id = d, cc_class = c, cc_tyargs = s }
+ | isSilentEvVar d -> (ClassP c s) : (transSuperClasses c s) ++ acc
+ _ -> acc) [] all_given_dicts
+
+ -- TODO:
+ -- When silent parameters will go away we should simply select from
+ -- the given map of the inert set.
+ all_given_dicts = Map.fold unionBags emptyCCan (cts_given $ inert_dicts inerts)
+
\end{code}
+
+Note [Silent parameters overlapping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+DV 12/05/2011:
+The long-term goal is to completely remove silent superclass
+parameters when checking instance declarations. But until then we must
+make sure that we never prevent the application of an instance
+declaration because of a potential match from a silent parameter --
+after all we are supposed to have solved that silent parameter from
+some instance, anyway! In effect silent parameters behave more like
+Solved than like Given.
+
+A concrete example appears in typecheck/SilentParametersOverlapping.hs
+
+Note [Instance and Given overlap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Assume that we have an inert set that looks as follows:
+ [Given] D [Int]
+And an instance declaration:
+ instance C a => D [a]
+A new wanted comes along of the form:
+ [Wanted] D [alpha]
+
+One possibility is to apply the instance declaration which will leave us
+with an unsolvable goal (C alpha). However, later on a new constraint may
+arise (for instance due to a functional dependency between two later dictionaries),
+that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
+will be transformed to [Wanted] D [Int], which could have been discharged by the given.
+
+The solution is that in matchClassInst and eventually in topReact, we get back with
+a matching instance, only when there is no Given in the inerts which is unifiable to
+this particular dictionary.
+
+The end effect is that, much as we do for overlapping instances, we delay choosing a
+class instance if there is a possibility of another instance OR a given to match our
+constraint later on. This fixes bugs #4981 and #5002.
+
+This is arguably not easy to appear in practice due to our aggressive prioritization
+of equality solving over other constraints, but it is possible. I've added a test case
+in typecheck/should-compile/GivenOverlapping.hs
+
+Moreover notice that our goals here are different than the goals of the top-level
+overlapping checks. There we are interested in validating the following principle:
+
+ If we inline a function f at a site where the same global instance environment
+ is available as the instance environment at the definition site of f then we
+ should get the same behaviour.
+
+But for the Given Overlap check our goal is just related to completeness of
+constraint solving.
+
+
+
+
projects / ghc-hetmet.git / blobdiff