module TcInteract ( 
     solveInteract, solveInteractGiven, solveInteractWanted,
     AtomicInert, tyVarsOfInert, 
     InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
  ) where  

#include "HsVersions.h"


import BasicTypes 
import TcCanonical
import VarSet
import Type

import Id 
import Var

import TcType
import HsBinds

import Inst( tyVarsOfEvVar )
import Class
import TyCon
import Name

import FunDeps

import Coercion
import Outputable

import TcRnTypes
import TcErrors
import TcSMonad
import Bag
import qualified Data.Map as Map

import Control.Monad( when )

import FastString ( sLit ) 
import DynFlags

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_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_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) } 
      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 = 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_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 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_ips          :: CCanMap (IPName Name)      -- Implicit parameters 
       , 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.
       }

tyVarsOfInert :: InertSet -> TcTyVarSet 
tyVarsOfInert (IS { inert_eqs    = eqs
                  , inert_dicts  = dictmap
                  , inert_ips    = ipmap
                  , 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_ips is))) 
                , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
                , 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 }

updInertSet :: InertSet -> AtomicInert -> InertSet 
updInertSet is item 
  | isCTyEqCan item                     -- Other equality 
  = let eqs' = inert_eqs is `Bag.snocBag` item 
    in is { inert_eqs = eqs' } 
  | Just cls <- isCDictCan_Maybe item   -- Dictionary 
  = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) } 
  | Just x  <- isCIPCan_Maybe item      -- IP 
  = is { inert_ips   = updCCanMap (x,item) (inert_ips is) }  
  | Just tc <- isCFunEqCan_Maybe item   -- Function equality 
  = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
  | otherwise 
  = is { inert_frozen = inert_frozen is `Bag.snocBag` item }

extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
-- 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_frozen = emptyCCan
                        , inert_funeqs = solved_funeqs }
    in (is_solved, unsolved)

  where (unsolved_eqs, solved_eqs)       = Bag.partitionBag (not.isGivenCt) 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` inert_frozen is `unionBags`
                   unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs

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
  | ContinueWith WorkItem	-- Not consumed

instance Outputable StopOrContinue where
  ppr Stop             = ptext (sLit "Stop")
  ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w

-- Results after interacting a WorkItem as far as possible with an InertSet
data StageResult
  = SR { sr_inerts     :: InertSet
           -- The new InertSet to use (REPLACES the old InertSet)
       , sr_new_work   :: WorkList
           -- Any new work items generated (should be ADDED to the old WorkList)
           -- Invariant: 
           --    sr_stop = Just workitem => workitem is *not* in sr_inerts and
           --                               workitem is inert wrt to sr_inerts
       , sr_stop       :: StopOrContinue
       }

instance Outputable StageResult where
  ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
    = ptext (sLit "SR") <+> 
      braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
             	  , ptext (sLit "new work =") <+> ppr work <> comma
             	  , ptext (sLit "stop =") <+> ppr stop])

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 :: SubGoalDepth
                  -> [(String, SimplifierStage)]
		  -> InertSet -> WorkItem 
                  -> TcS (InertSet, WorkList)
-- Precondition: non-empty list of stages 
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 }
       ; itr_out <- run_pipeline pipeline itr_in
       ; let new_inert 
              = case sr_stop itr_out of 
       	          Stop              -> sr_inerts itr_out
                  ContinueWith item -> sr_inerts itr_out `updInertSet` item
       ; return (new_inert, sr_new_work itr_out) }
  where 
    run_pipeline :: [(String, SimplifierStage)]
                 -> StageResult -> TcS StageResult
    run_pipeline [] itr                         = return itr
    run_pipeline _  itr@(SR { sr_stop = Stop }) = return itr

    run_pipeline ((name,stage):stages) 
                 (SR { sr_new_work = accum_work
                     , sr_inerts   = inerts
                     , sr_stop     = ContinueWith work_item })
      = 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 }
           ; run_pipeline stages itr' }

-- Main interaction solver: we fully solve the worklist 'in one go', 
-- returning an extended inert set.
--
-- See Note [Touchables and givens].
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
    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:" $
         vcat [ text "ws = " <+>  ppr (mapBag (\(EvVarX ev ct)
                                                   -> (ct,evVarPred ev)) ws)
              , text "inert = " <+> ppr inert ]

       ; (flag, inert_ret) <- foldlBagM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) ws 

       ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
         vcat [ text "No interaction happened = " <+> ppr flag
              , text "inert_ret = " <+> ppr inert_ret ]

       ; return (flag, inert_ret) }


tryPreSolveAndInteract :: SimplContext
                       -> DynFlags
                       -> (Bool, InertSet)
                       -> FlavoredEvVar
                       -> TcS (Bool, InertSet)
-- Returns: True if it was able to discharge this constraint AND all previous ones
tryPreSolveAndInteract sctx dyn_flags (all_previous_discharged, inert)
                       flavev@(EvVarX ev_var fl)
  = do { let inert_cts = get_inert_cts (evVarPred ev_var)

       ; this_one_discharged <- dischargeFromCCans inert_cts flavev

       ; if this_one_discharged
         then return (all_previous_discharged, inert)

         else do
       { extra_cts <- mkCanonical fl ev_var
       ; inert_ret <- solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[])
                                             inert extra_cts
       ; return (False, inert_ret) } }

  where
    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 -> FlavoredEvVar -> 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 (EvVarX 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) `tcEqPred` the_pred
      , cc_flavor ct `canSolve` fl
      = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) 
           	 -- Deriveds need no evidence
    	         -- For Givens, we already have evidence, and we don't need it twice 
           ; return True }
      where 
         set_ev_bind x y
            | EqPred {} <- evVarPred y = setEvBind x (EvCoercion (mkCoVarCoercion y))
            | otherwise                = setEvBind x (EvId y)

    discharge_ct _ct rest = rest

solveOne :: InertSet -> WorkItem -> TcS InertSet 
solveOne inerts workItem 
  = do { dyn_flags <- getDynFlags
       ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
       }

-----------------
solveInteractWithDepth :: (Int, Int, [WorkItem])
                       -> InertSet -> WorkList -> TcS InertSet
solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws 
  | isEmptyWorkList ws
  = return inert

  | n > max_depth 
  = solverDepthErrorTcS n stack

  | otherwise 
  = do { traceTcS "solveInteractWithDepth" $ 
              vcat [ text "Current depth =" <+> ppr n
                   , text "Max depth =" <+> ppr max_depth ]

	      -- 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 }

------------------
-- 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, depth, stack) inert work
  = do { traceFireTcS depth (text "Solving {" <+> ppr work)
       ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work
         
	 -- Recursively solve the new work generated 
         -- from workItem, with a greater depth
       ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack)
                                new_inert new_work 

       ; traceFireTcS depth (text "Done }" <+> ppr work) 

       ; return res_inert }

thePipeline :: [(String,SimplifierStage)]
thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
              , ("interact with inerts",    interactWithInertsStage)
              , ("spontaneous solve",       spontaneousSolveStage)
              , ("top-level reactions",     topReactionsStage) ]

spontaneousSolveStage :: SimplifierStage 
spontaneousSolveStage depth workItem inerts 
  = do { mSolve <- trySpontaneousSolve workItem

       ; case mSolve of 
           SPCantSolve -> -- No spontaneous solution for him, keep going
               return $ SR { sr_new_work   = emptyWorkList
                           , sr_inerts     = inerts
                           , sr_stop       = ContinueWith workItem }

           SPSolved workItem'
               | not (isGivenCt 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 { 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'
                     ; return $ SR { sr_new_work = new_work 
                                   , sr_inerts   = new_inert -- will include workItem' 
                                   , sr_stop     = Stop }
                     }
               | otherwise 
                   -> -- Original was given; he must then be inert all right, and
                      -- workList' are all givens from flattening
                      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
                           , sr_stop     = Stop }
       }

data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError
-- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
-- SPSolved workItem' gives us a new *given* to go on 
-- SPError means that it's completely impossible to solve this equality, eg due to a kind error


-- @trySpontaneousSolve wi@ solves equalities where one side is a
-- touchable unification variable.
--     	    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
  = return SPCantSolve
  | Just tv2 <- tcGetTyVar_maybe xi
  = do { tch1 <- isTouchableMetaTyVar tv1
       ; tch2 <- isTouchableMetaTyVar tv2
       ; case (tch1, tch2) of
           (True,  True)  -> trySpontaneousEqTwoWay cv gw tv1 tv2
           (True,  False) -> trySpontaneousEqOneWay cv gw tv1 xi
           (False, True)  -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
	   _ -> return SPCantSolve }
  | 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) 
                         ; return SPCantSolve }
       }

  -- No need for 
  --      trySpontaneousSolve (CFunEqCan ...) = ...
  -- See Note [No touchables as FunEq RHS] in TcSMonad
trySpontaneousSolve _ = return SPCantSolve

----------------
trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
-- tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay cv gw tv xi	
  | not (isSigTyVar tv) || isTyVarTy xi 
  = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts 
                               -- so we have its more specific kind in our hands
       ; if kxi `isSubKind` tyVarKind tv then
             solveWithIdentity cv gw tv xi
         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

----------------
trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
trySpontaneousEqTwoWay cv gw tv1 tv2
  | k1 `isSubKind` k2
  , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
  | k2 `isSubKind` k1 
  = solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
  | otherwise -- None is a subkind of the other, but they are both touchable! 
  = return SPCantSolve
    -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
    --   ; return SPError }
  where
    k1 = tyVarKind tv1
    k2 = tyVarKind tv2
    nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)

----------------

solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
-- Solve with the identity coercion 
-- Precondition: kind(xi) is a sub-kind of kind(tv)
-- Precondition: CtFlavor is Wanted or Derived
-- See [New Wanted Superclass Work] to see why solveWithIdentity 
--     must work for Derived as well as Wanted
-- Returns: workItem where 
--        workItem = the new Given constraint
solveWithIdentity cv wd tv xi 
  = do { traceTcS "Sneaky unification:" $ 
                       vcat [text "Coercion variable:  " <+> ppr wd, 
                             text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
                             text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
                             text "Right Kind is     : " <+> ppr (typeKind xi)
                  ]

       ; setWantedTyBind tv xi
       ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi

       ; when (isWanted wd) (setCoBind cv 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 }) }

-- Interaction result of  WorkItem <~> AtomicInert
data InteractResult
   = IR { ir_stop         :: StopOrContinue
            -- Stop
            --   => Reagent (work item) consumed.
            -- ContinueWith new_reagent
            --   => Reagent transformed but keep gathering interactions. 
            --      The transformed item remains inert with respect 
            --      to any previously encountered inerts.

        , ir_inert_action :: InertAction
            -- Whether the inert item should remain in the InertSet.

        , ir_new_work     :: WorkList
            -- new work items to add to the WorkList

        , ir_fire :: Maybe String    -- Tells whether a rule fired, and if so what
        }

-- What to do with the inert reactant.
data InertAction = KeepInert | DropInert 

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 }

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 }

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 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 the WorkItem with the entire equalities of the InertSet

interactWithInertEqsStage :: SimplifierStage 
interactWithInertEqsStage depth workItem inert
  = Bag.foldlBagM (interactNext depth) initITR (inert_eqs inert)
  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. 
-- Precondition: equality interactions must have already happened, hence we have 
-- to pick up some information from the incoming inert, before folding over the 
-- "Other" constraints it contains!

interactWithInertsStage :: SimplifierStage
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 depth) initITR relevant 
  where 
    getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) 
    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) 
        in (relevant, is { inert_funeqs = residual_map })
    getISRelevant (CIPCan { cc_ip_nm = nm }) is 
      = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
        in (relevant, is { inert_ips = residual_map }) 
    -- An equality, finally, may kick everything except equalities out 
    -- because we have already interacted the equalities in interactWithInertEqsStage
    getISRelevant _eq_ct is  -- Equality, everything is relevant for this one 
                             -- TODO: if we were caching variables, we'd know that only 
                             --       some are relevant. Experiment with this for now. 
      = let cts = cCanMapToBag (inert_ips is) `unionBags` 
                    cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
        in (cts, is { inert_dicts  = emptyCCanMap
                    , inert_ips    = emptyCCanMap
                    , inert_funeqs = emptyCCanMap })

interactNext :: SubGoalDepth -> StageResult -> AtomicInert -> TcS StageResult 
interactNext depth it inert  
  | 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 (isEmptyBag 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` new_work
                     , sr_stop     = stop } }
  | otherwise 
  = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }

-- Do a single interaction of two constraints.
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 
       }

allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool 
-- Allowed interactions 
allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
allowedInteraction eqs_only (CIPCan {})   (CIPCan {})   = not eqs_only
allowedInteraction _ _ _ = True 

--------------------------------------------
doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
-- Identical class constraints.

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 && (and $ zipWith tcEqType tys1 tys2)
  = solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem 

  | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
  = 	 -- See Note [When improvement happens]
    do { let pty1 = ClassP cls1 tys1
             pty2 = ClassP cls2 tys2
             inert_pred_loc     = (pty1, pprFlavorArising fl1)
             work_item_pred_loc = (pty2, pprFlavorArising fl2)
             fd_eqns = improveFromAnother 
                                  inert_pred_loc     -- the template
                                  work_item_pred_loc -- the one we aim to rewrite
                                  -- See Note [Efficient Orientation]

       ; m <- rewriteWithFunDeps fd_eqns tys2 fl2
       ; case m of 
           Nothing -> noInteraction workItem
           Just (rewritten_tys2, cos2, fd_work)
             | tcEqTypes tys1 rewritten_tys2
             -> -- Solve him on the spot in this case
	     	case fl2 of
	          Given   {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
                  Derived {} -> mkIRStopK "Cls/Cls fundep (solved)" fd_work
		  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 *replace* the
			   -- inert item, but its safe and simple to restart
                         ; mkIRStopD "Cls/Cls fundep (solved)" (inert_w `consBag` fd_work) }

		    | otherwise 
                    -> do { setDictBind d2 (EvCast d1 dict_co)
                          ; mkIRStopK "Cls/Cls fundep (solved)" fd_work }

             | otherwise
             -> -- We could not quite solve him, but we still rewrite him
	        -- Example: class C a b c | a -> b
		--          Given: C Int Bool x, Wanted: C Int beta y
		--          Then rewrite the wanted to C Int Bool y
		--          but note that is still not identical to the given
		-- The important thing is that the rewritten constraint is
		-- inert wrt the given.
		-- However it is not necessarily inert wrt previous inert-set items.
                --      class C a b c d |  a -> b, b c -> d
		--      Inert: c1: C b Q R S, c2: C P Q a b
		--      Work: C P alpha R beta
		--      Does not react with c1; reacts with c2, with alpha:=Q
		--      NOW it reacts with c1!
		-- So we must stop, and put the rewritten constraint back in the work list
                do { d2' <- newDictVar cls1 rewritten_tys2
                   ; case fl2 of
                       Given {}   -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
                       Wanted {}  -> setDictBind d2 (EvCast d2' dict_co)
                       Derived {} -> return ()
                   ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 }
                   ; mkIRStopK "Cls/Cls fundep (partial)" (workItem' `consBag` fd_work) } 

             where
               dict_co = mkTyConCoercion (classTyCon cls1) cos2
  }

-- Class constraint and given equality: use the equality to rewrite
-- the class constraint. 
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 "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
    
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 "Cls/Eq" workItem DropInert (workListFromCCan rewritten_dict) }

-- Class constraint and given equality: use the equality to rewrite
-- the class constraint.
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 "Eq/IP" rewritten_ip KeepInert emptyWorkList } 

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 "IP/Eq" workItem DropInert (workListFromCCan 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 (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
  = 	-- See Note [Overriding implicit parameters]
        -- Dump the inert item, override totally with the new one
	-- Do not require type equality
	-- 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 "IP/IP" (EvId id1,ifl) workItem 

  | nm1 == nm2
  =  	-- See Note [When improvement happens]
    do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation]
       ; let flav = Wanted (combineCtLoc ifl wfl) 
       ; cans <- mkCanonical flav co_var 
       ; mkIRContinue "IP/IP fundep" workItem KeepInert cans }

-- Never rewrite a given with a wanted equality, and a type function
-- equality can never rewrite an equality. We rewrite LHS *and* RHS 
-- of function equalities so that our inert set exposes everything that 
-- we know about equalities.

-- Inert: equality, work item: function equality
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) 
       ; mkIRStopK "Eq/FunEq" (workListFromCCan rewritten_funeq) } 
         -- Must Stop here, because we may no longer be inert after the rewritting.

-- Inert: function equality, work item: equality
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 "FunEq/Eq" workItem DropInert (workListFromCCan 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: 
         -- Original inert = {    F xis ~  [a], b ~ Maybe Int } 
         -- Work item comes along = a ~ [b] 
         -- If we keep { F xis ~ [b] } in the inert set we will end up with: 
         --      { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] } 
         -- At the end, which is *not* inert. So we should unfortunately DropInert here.

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 })
  | fl1 `canSolve` fl2 && lhss_match
  = do { cans <- rewriteEqLHS LeftComesFromInert  (mkCoVarCoercion 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 "FunEq/FunEq" workItem DropInert cans }
  where
    lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) 

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) 
       ; mkIRStopK "Eq/Eq lhs" cans } 

  | fl2 `canSolve` fl1 && tv1 == tv2 
  = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion 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) 
       ; 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 "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 _ 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]
             args = substTysWith [tv] [xi] xis
             con  = classTyCon cl 
             dict_co = mkTyConCoercion con cos 
       ; dv' <- newDictVar cl args 
       ; case gw of 
           Wanted {}         -> setDictBind dv (EvCast dv' (mkSymCoercion 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 
                          , cc_tyargs = args }) } 

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
       ; ipid' <- newIPVar nm ty' 
       ; case gw of 
           Wanted {}         -> setIPBind ipid  (EvCast ipid' (mkSymCoercion 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
                        , cc_ip_ty = ty' }) }
   
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'

             xi2'    = substTyWith [tv] [xi1] xi2
             xi2_co  = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2' 

       ; cv2' <- newCoVar (mkTyConApp tc args') xi2'
       ; case gw of 
           Wanted {} -> setCoBind cv2  (fun_co               `mkTransCoercion` 
                                        mkCoVarCoercion cv2' `mkTransCoercion` 
                                        mkSymCoercion xi2_co)
           Given {}  -> setCoBind cv2' (mkSymCoercion fun_co `mkTransCoercion` 
                                        mkCoVarCoercion cv2  `mkTransCoercion` 
                                        xi2_co)
           Derived {} -> return () 

       ; return (CFunEqCan { cc_id = cv2'
                           , cc_flavor = gw
                           , cc_tyargs = args'
                           , cc_fun = tc 
                           , cc_rhs = xi2' }) }


rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
-- Use the first equality to rewrite the second, flavors already checked. 
-- E.g.          c1 : tv1 ~ xi1   c2 : tv2 ~ xi2
-- rewrites c2 to give
--               c2' : tv2 ~ xi2[xi1/tv1]
-- We must do an occurs check to sure the new constraint is canonical
-- So we might return an empty bag
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) (setCoBind cv2 (mkSymCoercion co2')) 
       ; return emptyCCan } 
  | otherwise
  = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
       ; case gw of
             Wanted {} -> setCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion` 
                                          mkSymCoercion co2'
             Given {}  -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion` 
                                           co2'
             Derived {} -> return ()
       ; canEq gw cv2' (mkTyVarTy tv2) xi2' }
  where 
    xi2' = substTyWith [tv1] [xi1] xi2 
    co2' = substTyWith [tv1] [mkCoVarCoercion 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 `canRewrite` cv2 equality 
-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1), 
--    See Note [Efficient Orientation] for that 
rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2) 
  = do { cv2' <- newCoVar xi2 xi1 
       ; case gw of 
           Wanted {} -> setCoBind cv2 $ 
                        co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
           Given {}  -> setCoBind cv2' $ 
                        mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` 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 `mkTransCoercion` mkCoVarCoercion cv2'
           Given {}  -> setCoBind cv2' $
                        mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion 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'                `mkTransCoercion`
                       	         	  mkCoVarCoercion cv2' `mkTransCoercion`
                       	         	  mkSymCoercion co2b'

             Given {} -> setCoBind cv2' $ mkSymCoercion co2a'  `mkTransCoercion`
                      	 		  mkCoVarCoercion cv2  `mkTransCoercion`
                      	 		  co2b'

             Derived {} -> return ()

      ; return (singleCCan $ 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' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a  -- ty2a ~ ty2a[xi1/tv1]
    co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b  -- ty2b ~ ty2b[xi1/tv1]

solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> 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 info (ev_term,ifl) workItem
  | isDerived wfl
  = mkIRStopK ("Solved[DW] " ++ info) emptyWorkList

  | 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 emptyWorkList
  
  | 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) emptyWorkList }
  where 
     wfl = cc_flavor workItem
     wid = cc_id workItem

-- If a work item has any form of interaction with top-level we get this 
data TopInteractResult 
  = 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)
      , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now: 
      }                       		-- NB: in ``given'' (solved) form if the 
                              		-- original was wanted or given and instance match
                              		-- was found, but may also be in wanted form if we 
                                        -- only reacted with functional dependencies 
					-- arising from top-level instances.

topReactionsStage :: SimplifierStage 
topReactionsStage depth 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 -> 
               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 
  = 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 }
         else return NoTopInt 
       } 

allowedTopReaction :: Bool -> WorkItem -> Bool
allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
allowedTopReaction _        _             = True

doTopReact :: 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. 
-- See Note [Adding superclasses] in TcCanonical.

-- Given dictionary
-- See Note [Given constraint that matches an instance declaration]
doTopReact (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 = fl@(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 fl
       ; 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 return $ SomeTopInt { tir_new_work  = fd_work 
                                      , tir_new_inert = ContinueWith workItem' } }

-- Wanted dictionary
doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(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)

                ; instEnvs <- getInstEnvs
                ; let fd_eqns = improveFromInstEnv instEnvs
                                                         (ClassP cls xis, pprArisingAt loc)
                ; m <- rewriteWithFunDeps fd_eqns xis fl
                ; case m of
                    Nothing -> return NoTopInt
                    Just (xis',cos,fd_work) ->
                        do { let dict_co = mkTyConCoercion (classTyCon cls) cos
                           ; dv'<- newDictVar cls xis'
                           ; setDictBind dv (EvCast dv' dict_co)
                           ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl, 
                                                        cc_class = cls, cc_tyargs = xis' }
                           ; return $ 
                             SomeTopInt { tir_new_work  = singleCCan workItem' `andCCan` fd_work
                                        , 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
             | null wtvs
             -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) 
                   ; setDictBind dv ev_term 
                    -- 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'; hence Stop
                   ; return $ SomeTopInt { tir_new_work  = emptyWorkList 
                                         , tir_new_inert = Stop } }

             | otherwise
             -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) 
                   ; setDictBind dv ev_term 
                        -- Solved and new wanted work produced, you may cache the 
                        -- (tentatively solved) dictionary as Given! (used to be: Derived)
                   ; let solved   = workItem { cc_flavor = given_fl }
                         given_fl = Given (setCtLocOrigin loc UnkSkol) 
                   ; inst_work <- canWanteds wtvs
                   ; return $ SomeTopInt { tir_new_work  = inst_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 })
  = 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 
           MatchInstSingle (rep_tc, rep_tys)
             -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
                         Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
			    -- Eagerly expand away the type synonym on the
			    -- 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' <- newCoVar rhs_ty xi
                                              ; setCoBind cv $ 
                                                    coe `mkTransCoercion`
                                                      mkCoVarCoercion cv'
                                              ; return cv' }
                              Given {}   -> newGivenCoVar xi rhs_ty $ 
                                            mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe 
                              Derived {} -> newDerivedId (EqPred xi rhs_ty)
                   ; can_cts <- mkCanonical fl cv'
                   ; return $ SomeTopInt can_cts Stop }
           _ 
             -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
       }


-- Any other work item does not react with any top-level equations
doTopReact _workItem = return NoTopInt 

data LookupInstResult
  = NoInstance
  | GenInst [WantedEvVar] EvTerm 

matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
matchClassInst clas tys loc
   = do { let pred = mkClassPred clas tys 
        ; mb_result <- matchClass clas tys
        ; case mb_result of
            MatchInstNo   -> return NoInstance
            MatchInstMany -> return NoInstance -- defer any reactions of a multitude until 
                                               -- we learn more about the reagent 
            MatchInstSingle (dfun_id, mb_inst_tys) -> 
              do { checkWellStagedDFun pred dfun_id loc

 	-- It's possible that not all the tyvars are in
	-- the substitution, tenv. For example:
	--	instance C X a => D X where ...
	-- (presumably there's a functional dependency in class C)
	-- Hence mb_inst_tys :: Either TyVar TcType 

                 ; tys <- instDFunTypes mb_inst_tys 
                 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
                 ; if null theta then
                       return (GenInst [] (EvDFunApp dfun_id tys []))
                   else do
                     { ev_vars <- instDFunConstraints theta
                     ; let wevs = [EvVarX w loc | w <- ev_vars]
                     ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }
                 }
        }