{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

module TcInteract ( 
     solveInteractGiven,  -- Solves [EvVar],GivenLoc
     solveInteractCts,    -- Solves [Cts]
  ) where  

#include "HsVersions.h"


import BasicTypes ()
import TcCanonical
import VarSet
import Type
import Unify
import FamInstEnv
import Coercion( mkAxInstRHS )

import Var
import TcType
import PrelNames (singIClassName)

import Class
import TyCon
import Name

import FunDeps

import TcEvidence
import Outputable

import TcMType ( zonkTcPredType )

import TcRnTypes
import TcErrors
import TcSMonad
import Maybes( orElse )
import Bag

import Control.Monad ( foldM )

import VarEnv
import qualified Data.Traversable as Traversable

import Control.Monad( when, unless )
import Pair ()
import UniqFM
import FastString ( sLit ) 
import DynFlags
import Util

solveInteractCts :: [Ct] -> TcS (Bag Implication)
-- Returns a bag of residual implications that have arisen while solving
-- this particular worklist.
solveInteractCts cts 
  = do { traceTcS "solveInteractCtS" (vcat [ text "cts =" <+> ppr cts ]) 
       ; updWorkListTcS (appendWorkListCt cts) >> solveInteract 
       ; impls <- getTcSImplics
       ; updTcSImplics (const emptyBag) -- Nullify residual implications
       ; return impls }

solveInteractGiven :: GivenLoc -> [EvVar] -> TcS (Bag Implication)
-- In principle the givens can kick out some wanteds from the inert
-- resulting in solving some more wanted goals here which could emit
-- implications. That's why I return a bag of implications. Not sure
-- if this can happen in practice though.
solveInteractGiven gloc evs
  = solveInteractCts (map mk_noncan evs)
  where 
    mk_noncan ev = CNonCanonical { cc_ev = Given { ctev_gloc = gloc 
                                                 , ctev_evtm = EvId ev
                                                 , ctev_pred = evVarPred ev }
                                 , cc_depth = 0 }

-- The main solver loop implements Note [Basic Simplifier Plan]
---------------------------------------------------------------
solveInteract :: TcS ()
-- Returns the final InertSet in TcS, WorkList will be eventually empty.
solveInteract
  = {-# SCC "solveInteract" #-}
    do { dyn_flags <- getDynFlags
       ; let max_depth = ctxtStkDepth dyn_flags
             solve_loop
              = {-# SCC "solve_loop" #-}
                do { sel <- selectNextWorkItem max_depth
                   ; case sel of 
                      NoWorkRemaining     -- Done, successfuly (modulo frozen)
                        -> return ()
                      MaxDepthExceeded ct -- Failure, depth exceeded
                        -> wrapErrTcS $ solverDepthErrorTcS (cc_depth ct) [ct]
                      NextWorkItem ct     -- More work, loop around!
                        -> runSolverPipeline thePipeline ct >> solve_loop }
       ; solve_loop }

type WorkItem = Ct
type SimplifierStage = WorkItem -> TcS StopOrContinue

continueWith :: WorkItem -> TcS StopOrContinue
continueWith work_item = return (ContinueWith work_item) 

data SelectWorkItem 
       = NoWorkRemaining      -- No more work left (effectively we're done!)
       | MaxDepthExceeded Ct  -- More work left to do but this constraint has exceeded
                              -- the max subgoal depth and we must stop 
       | NextWorkItem Ct      -- More work left, here's the next item to look at 

selectNextWorkItem :: SubGoalDepth -- Max depth allowed
                   -> TcS SelectWorkItem
selectNextWorkItem max_depth
  = updWorkListTcS_return pick_next
  where 
    pick_next :: WorkList -> (SelectWorkItem, WorkList)
    pick_next wl = case selectWorkItem wl of
                     (Nothing,_) 
                         -> (NoWorkRemaining,wl)           -- No more work
                     (Just ct, new_wl) 
                         | cc_depth ct > max_depth         -- Depth exceeded
                         -> (MaxDepthExceeded ct,new_wl)
                     (Just ct, new_wl) 
                         -> (NextWorkItem ct, new_wl)      -- New workitem and worklist

runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline 
                  -> WorkItem                   -- The work item 
                  -> TcS () 
-- Run this item down the pipeline, leaving behind new work and inerts
runSolverPipeline pipeline workItem 
  = do { initial_is <- getTcSInerts 
       ; traceTcS "Start solver pipeline {" $ 
                  vcat [ ptext (sLit "work item = ") <+> ppr workItem 
                       , ptext (sLit "inerts    = ") <+> ppr initial_is]

       ; final_res  <- run_pipeline pipeline (ContinueWith workItem)

       ; final_is <- getTcSInerts
       ; case final_res of 
           Stop            -> do { traceTcS "End solver pipeline (discharged) }" 
                                       (ptext (sLit "inerts    = ") <+> ppr final_is)
                                 ; return () }
           ContinueWith ct -> do { traceTcS "End solver pipeline (not discharged) }" $
                                       vcat [ ptext (sLit "final_item = ") <+> ppr ct
                                            , ptext (sLit "inerts     = ") <+> ppr final_is]
                                 ; updInertSetTcS ct }
       }
  where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
        run_pipeline [] res = return res 
        run_pipeline _ Stop = return Stop 
        run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
          = do { traceTcS ("runStage " ++ stg_name ++ " {")
                          (text "workitem   = " <+> ppr ct) 
               ; res <- stg ct 
               ; traceTcS ("end stage " ++ stg_name ++ " }") empty
               ; run_pipeline stgs res 
               }

thePipeline :: [(String,SimplifierStage)]
thePipeline = [ ("lookup-in-inerts",        lookupInInertsStage)
              , ("canonicalization",        canonicalizationStage)
              , ("spontaneous solve",       spontaneousSolveStage)
              , ("interact with inerts",    interactWithInertsStage)
              , ("top-level reactions",     topReactionsStage) ]

-- A quick lookup everywhere to see if we know about this constraint
--------------------------------------------------------------------
lookupInInertsStage :: SimplifierStage
lookupInInertsStage ct
  | Wanted { ctev_evar = ev_id, ctev_pred = pred } <- cc_ev ct
  = do { is <- getTcSInerts
       ; case lookupInInerts is pred of
           Just ctev
             |  not (isDerived ctev)
             -> do { setEvBind ev_id (ctEvTerm ctev)
                   ; return Stop }
           _ -> continueWith ct }
  | otherwise -- I could do something like that for givens 
              -- as well I suppose but it is not a big deal
  = continueWith ct


-- The canonicalization stage, see TcCanonical for details
----------------------------------------------------------
canonicalizationStage :: SimplifierStage
canonicalizationStage = TcCanonical.canonicalize 

spontaneousSolveStage :: SimplifierStage 
spontaneousSolveStage workItem
  = do { mSolve <- trySpontaneousSolve workItem
       ; spont_solve mSolve } 
  where spont_solve SPCantSolve 
          | isCTyEqCan workItem                    -- Unsolved equality
          = do { kickOutRewritableInerts workItem  -- NB: will add workItem in inerts
               ; return Stop }
          | otherwise
          = continueWith workItem
        spont_solve (SPSolved workItem')           -- Post: workItem' must be equality
          = do { bumpStepCountTcS
               ; traceFireTcS (cc_depth workItem) $
                 ptext (sLit "Spontaneous:") <+> ppr workItem

                 -- NB: will add the item in the inerts
               ; kickOutRewritableInerts workItem'
               -- .. and Stop
               ; return Stop }

kickOutRewritableInerts :: Ct -> TcS () 
-- Pre:  ct is a CTyEqCan 
-- Post: The TcS monad is left with the thinner non-rewritable inerts; but which
--       contains the new constraint.
--       The rewritable end up in the worklist
kickOutRewritableInerts ct
  = {-# SCC "kickOutRewritableInerts" #-}
    do { traceTcS "kickOutRewritableInerts" $ text "workitem = " <+> ppr ct
       ; (wl,ieqs) <- {-# SCC "kick_out_rewritable" #-}
                      modifyInertTcS (kick_out_rewritable ct)
       ; traceTcS "Kicked out the following constraints" $ ppr wl
       ; is <- getTcSInerts 
       ; traceTcS "Remaining inerts are" $ ppr is

       -- Step 1: Rewrite as many of the inert_eqs on the spot!
       -- NB: if it is a given constraint just use the cached evidence
       -- to optimize e.g. mkRefl coercions from spontaneously solved cts.
       ; bnds <- getTcEvBindsMap
       ; let ct_coercion = getCtCoercion bnds ct 

       ; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
                     rewriteInertEqsFromInertEq (cc_tyvar ct,
                                                 ct_coercion,cc_ev ct) ieqs
       ; let upd_eqs is = is { inert_cans = new_ics }
                        where ics     = inert_cans is
                              new_ics = ics { inert_eqs = new_ieqs }
       ; modifyInertTcS (\is -> ((), upd_eqs is)) 
         
       ; is <- getTcSInerts 
       ; traceTcS "Final inerts are" $ ppr is
       
         -- Step 2: Add the new guy in
       ; updInertSetTcS ct

       ; traceTcS "Kick out" (ppr ct $$ ppr wl)
       ; updWorkListTcS (unionWorkList wl) }

rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtEvidence) -- A new substitution
                           -> TyVarEnv Ct                     -- All the inert equalities
                           -> TcS (TyVarEnv Ct)               -- The new inert equalities
rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs
-- The goal: traverse the inert equalities and throw some of them back to the worklist
-- if you have to rewrite and recheck them for occurs check errors. 
-- To see which ones we must throw out see Note [Delicate equality kick-out]
 = do { mieqs <- Traversable.mapM do_one ieqs 
      ; traceTcS "Original inert equalities:" (ppr ieqs)
      ; let flatten_justs elem venv
              | Just act <- elem = extendVarEnv venv (cc_tyvar act) act
              | otherwise = venv                                     
            final_ieqs = foldVarEnv flatten_justs emptyVarEnv mieqs
      ; traceTcS "Remaining inert equalities:" (ppr final_ieqs)
      ; return final_ieqs }

 where do_one ct
         | subst_fl `canRewrite` fl && (subst_tv `elemVarSet` tyVarsOfCt ct) 
         = if fl `canRewrite` subst_fl then
               -- If also the inert can rewrite the subst then there is no danger of 
               -- occurs check errors sor keep it there. No need to rewrite the inert equality
               -- (as we did in the past) because of point (8) of 
               -- Note [Detailed InertCans Invariants] and 
             return (Just ct)
             -- used to be: rewrite_on_the_spot ct >>= ( return . Just )
           else -- We have to throw inert back to worklist for occurs checks 
             updWorkListTcS (extendWorkListEq ct) >> return Nothing
         | otherwise -- Just keep it there
         = return (Just ct)
         where 
           fl  = cc_ev ct

kick_out_rewritable :: Ct 
                    -> InertSet 
                    -> ((WorkList, TyVarEnv Ct),InertSet)
-- Post: returns ALL inert equalities, to be dealt with later
-- 
kick_out_rewritable ct is@(IS { inert_cans = 
                                   IC { inert_eqs    = eqmap
                                      , inert_eq_tvs = inscope
                                      , inert_dicts  = dictmap
                                      , inert_funeqs = funeqmap
                                      , inert_irreds = irreds }
                              , inert_frozen = frozen })
  = ((kicked_out,eqmap), remaining)
  where
    rest_out = fro_out `andCts` dicts_out `andCts` irs_out
    kicked_out = WorkList { wl_eqs    = []
                          , wl_funeqs = bagToList feqs_out
                          , wl_rest   = bagToList rest_out }
  
    remaining = is { inert_cans = IC { inert_eqs = emptyVarEnv
                                     , inert_eq_tvs = inscope 
                                       -- keep the same, safe and cheap
                                     , inert_dicts = dicts_in
                                     , inert_funeqs = feqs_in
                                     , inert_irreds = irs_in }
                   , inert_frozen = fro_in } 
                -- NB: Notice that don't rewrite 
                -- inert_solved, inert_flat_cache and inert_solved_funeqs
                -- optimistically. But when we lookup we have to take the 
                -- subsitution into account
    fl = cc_ev ct
    tv = cc_tyvar ct

    (feqs_out,  feqs_in)    = partCtFamHeadMap rewritable funeqmap
    (dicts_out, dicts_in)   = partitionCCanMap rewritable dictmap

    (irs_out,   irs_in)   = partitionBag rewritable irreds
    (fro_out,   fro_in)   = partitionBag rewritable frozen

    rewritable ct = (fl `canRewrite` cc_ev ct)  &&
                    (tv `elemVarSet` tyVarsOfCt ct) 
                    -- NB: tyVarsOfCt will return the type 
                    --     variables /and the kind variables/ that are 
                    --     directly visible in the type. Hence we will
                    --     have exposed all the rewriting we care about
                    --     to make the most precise kinds visible for 
                    --     matching classes etc. No need to kick out 
                    --     constraints that mention type variables whose
                    --     kinds could contain this variable!

data SPSolveResult = SPCantSolve
                   | SPSolved WorkItem 

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

-- @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_ev = gw
                                       , cc_tyvar = tv1, cc_rhs = xi, cc_depth = d })
  | isGiven gw
  = return SPCantSolve
  | Just tv2 <- tcGetTyVar_maybe xi
  = do { tch1 <- isTouchableMetaTyVar tv1
       ; tch2 <- isTouchableMetaTyVar tv2
       ; case (tch1, tch2) of
           (True,  True)  -> trySpontaneousEqTwoWay d gw tv1 tv2
           (True,  False) -> trySpontaneousEqOneWay d gw tv1 xi
           (False, True)  -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
	   _ -> return SPCantSolve }
  | otherwise
  = do { tch1 <- isTouchableMetaTyVar tv1
       ; if tch1 then trySpontaneousEqOneWay d 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 :: SubGoalDepth 
                       -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
-- tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay d gw tv xi
  | not (isSigTyVar tv) || isTyVarTy xi
  = solveWithIdentity d gw tv xi
  | otherwise -- Still can't solve, sig tyvar and non-variable rhs
  = return SPCantSolve

----------------
trySpontaneousEqTwoWay :: SubGoalDepth 
                       -> CtEvidence -> TcTyVar -> TcTyVar -> TcS SPSolveResult
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here

trySpontaneousEqTwoWay d gw tv1 tv2
  = do { let k1_sub_k2 = k1 `tcIsSubKind` k2
       ; if k1_sub_k2 && nicer_to_update_tv2
         then solveWithIdentity d gw tv2 (mkTyVarTy tv1)
         else solveWithIdentity d gw tv1 (mkTyVarTy tv2) }
  where
    k1 = tyVarKind tv1
    k2 = tyVarKind tv2
    nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)

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

solveWithIdentity :: SubGoalDepth 
                  -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
-- Solve with the identity coercion 
-- Precondition: kind(xi) is a sub-kind of kind(tv)
-- Precondition: CtEvidence 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
--
-- NB: No need for an occurs check here, because solveWithIdentity always 
--     arises from a CTyEqCan, a *canonical* constraint.  Its invariants
--     say that in (a ~ xi), the type variable a does not appear in xi.
--     See TcRnTypes.Ct invariants.
solveWithIdentity d wd tv xi 
  = do { let tv_ty = mkTyVarTy tv
       ; traceTcS "Sneaky unification:" $ 
                       vcat [text "Constraint:" <+> ppr wd,
                             text "Coercion:" <+> pprEq tv_ty xi,
                             text "Left Kind is:" <+> ppr (typeKind tv_ty),
                             text "Right Kind is:" <+> ppr (typeKind xi) ]

       ; let xi' = defaultKind xi      
               -- We only instantiate kind unification variables
               -- with simple kinds like *, not OpenKind or ArgKind
               -- cf TcUnify.uUnboundKVar

       ; setWantedTyBind tv xi'
       ; let refl_evtm = EvCoercion (mkTcReflCo xi')
             refl_pred = mkTcEqPred tv_ty xi'

       ; when (isWanted wd) $ 
              setEvBind (ctev_evar wd) refl_evtm

       ; let given_fl = Given { ctev_gloc = mkGivenLoc (ctev_wloc wd) UnkSkol
                              , ctev_pred = refl_pred
                              , ctev_evtm = refl_evtm }
             
       ; return $ 
         SPSolved (CTyEqCan { cc_ev = given_fl
                            , cc_tyvar  = tv, cc_rhs = xi', cc_depth = d }) }

-- Interaction result of  WorkItem <~> Ct

data InteractResult 
    = IRWorkItemConsumed { ir_fire :: String } 
    | IRInertConsumed    { ir_fire :: String } 
    | IRKeepGoing        { ir_fire :: String }

irWorkItemConsumed :: String -> TcS InteractResult
irWorkItemConsumed str = return (IRWorkItemConsumed str) 

irInertConsumed :: String -> TcS InteractResult
irInertConsumed str = return (IRInertConsumed str) 

irKeepGoing :: String -> TcS InteractResult 
irKeepGoing str = return (IRKeepGoing str) 
-- You can't discard neither workitem or inert, but you must keep 
-- going. It's possible that new work is waiting in the TcS worklist. 


interactWithInertsStage :: WorkItem -> TcS StopOrContinue 
-- Precondition: if the workitem is a CTyEqCan then it will not be able to 
-- react with anything at this stage. 
interactWithInertsStage wi 
  = do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
       ; rels <- extractRelevantInerts wi 
       ; traceTcS "relevant inerts are:" $ ppr rels
       ; foldlBagM interact_next (ContinueWith wi) rels }

  where interact_next Stop atomic_inert 
          = updInertSetTcS atomic_inert >> return Stop
        interact_next (ContinueWith wi) atomic_inert 
          = do { ir <- doInteractWithInert atomic_inert wi
               ; let mk_msg rule keep_doc 
                       = vcat [ text rule <+> keep_doc
                              , ptext (sLit "InertItem =") <+> ppr atomic_inert
                              , ptext (sLit "WorkItem  =") <+> ppr wi ]
               ; case ir of 
                   IRWorkItemConsumed { ir_fire = rule } 
                       -> do { bumpStepCountTcS
                             ; traceFireTcS (cc_depth wi) 
                                            (mk_msg rule (text "WorkItemConsumed"))
                             ; updInertSetTcS atomic_inert
                             ; return Stop } 
                   IRInertConsumed { ir_fire = rule }
                       -> do { bumpStepCountTcS
                             ; traceFireTcS (cc_depth atomic_inert) 
                                            (mk_msg rule (text "InertItemConsumed"))
                             ; return (ContinueWith wi) }
                   IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
                       -> do { updInertSetTcS atomic_inert
                             ; return (ContinueWith wi) }
               }

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

doInteractWithInert :: Ct -> Ct -> TcS InteractResult
-- Identical class constraints.
doInteractWithInert
  inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1 })
   workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2 })

  | cls1 == cls2  
  = do { let pty1 = mkClassPred cls1 tys1
             pty2 = mkClassPred cls2 tys2
             inert_pred_loc     = (pty1, pprFlavorArising fl1)
             work_item_pred_loc = (pty2, pprFlavorArising fl2)

       ; traceTcS "doInteractWithInert" (vcat [ text "inertItem = " <+> ppr inertItem
                                              , text "workItem  = " <+> ppr workItem ])
 
       ; let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
       ; any_fundeps <- rewriteWithFunDeps fd_eqns tys2 fl2
                -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
                -- NB: We do create FDs for given to report insoluble equations that arise
                -- from pairs of Givens, and also because of floating when we approximate
                -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
                -- Also see Note [When improvement happens]
                -- 
       
       ; case any_fundeps of
           -- No Functional Dependencies 
           Nothing             
               | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
               | otherwise         -> irKeepGoing "NOP"

           -- Actual Functional Dependencies
           Just (_rewritten_tys2, fd_work)
              -- 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 { emitFDWorkAsDerived fd_work (cc_depth workItem)
                     ; irKeepGoing "Cls/Cls (new fundeps)" } -- Just keep going without droping the inert 
       }
 
-- Two pieces of irreducible evidence: if their types are *exactly identical* 
-- we can rewrite them. We can never improve using this: 
-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not 
-- mean that (ty1 ~ ty2)
doInteractWithInert (CIrredEvCan { cc_ev = ifl, cc_ty = ty1 })
           workItem@(CIrredEvCan { cc_ty = ty2 })
  | ty1 `eqType` ty2
  = solveOneFromTheOther "Irred/Irred" ifl workItem

doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
                                  , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
                    wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2
                                  , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
  | fl1 `canSolve` fl2 && lhss_match
  = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
         vcat [ text "workItem =" <+> ppr wi
              , text "inertItem=" <+> ppr ii ]

       ; let xev = XEvTerm xcomp xdecomp
             -- xcomp : [(xi2 ~ xi1)] -> (F args ~ xi2) 
             xcomp [x] = EvCoercion (co1 `mkTcTransCo` mk_sym_co x)
             xcomp _   = panic "No more goals!"
             -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]                 
             xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]

       ; ctevs <- xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev
                         -- Why not simply xCtFlavor? See Note [Cache-caused loops]
                         -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
       ; add_to_work d2 ctevs 
       ; irWorkItemConsumed "FunEq/FunEq" }

  | fl2 `canSolve` fl1 && lhss_match
  = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
         vcat [ text "workItem =" <+> ppr wi
              , text "inertItem=" <+> ppr ii ]

       ; let xev = XEvTerm xcomp xdecomp
              -- xcomp : [(xi2 ~ xi1)] -> [(F args ~ xi1)]
             xcomp [x] = EvCoercion (co2 `mkTcTransCo` evTermCoercion x)
             xcomp _ = panic "No more goals!"
             -- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
             xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]

       ; ctevs <- xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev 
                          -- Why not simply xCtFlavor? See Note [Cache-caused loops]
                          -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]

       ; add_to_work d1 ctevs 
       ; irInertConsumed "FunEq/FunEq"}
  where
    add_to_work d [ctev] = updWorkListTcS $ extendWorkListEq $
                           CNonCanonical {cc_ev = ctev, cc_depth = d}
    add_to_work _ _ = return ()

    lhss_match = tc1 == tc2 && eqTypes args1 args2 
    co1 = evTermCoercion $ ctEvTerm fl1
    co2 = evTermCoercion $ ctEvTerm fl2
    mk_sym_co x = mkTcSymCo (evTermCoercion x)
    
doInteractWithInert _ _ = irKeepGoing "NOP"

solveOneFromTheOther :: String    -- Info 
                     -> CtEvidence  -- Inert 
                     -> Ct        -- WorkItem 
                     -> TcS InteractResult
-- Preconditions: 
-- 1) inert and work item represent evidence for the /same/ predicate
-- 2) ip/class/irred evidence (no coercions) only
solveOneFromTheOther info ifl workItem
  | isDerived wfl
  = irWorkItemConsumed ("Solved[DW] " ++ info)

  | 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
  = irInertConsumed ("Solved[DI] " ++ info)
  
  | otherwise
  = ASSERT( ifl `canSolve` wfl )
      -- Because of Note [The Solver Invariant], plus Derived dealt with
    do { case wfl of
           Wanted { ctev_evar = ev_id } -> setEvBind ev_id (ctEvTerm ifl)
           _                            -> return ()
           -- Overwrite the binding, if one exists
	   -- If both are Given, we already have evidence; no need to duplicate
       ; irWorkItemConsumed ("Solved " ++ info) }
  where 
     wfl = cc_ev workItem

rewriteWithFunDeps :: [Equation]
                   -> [Xi] 
                   -> CtEvidence
                   -> TcS (Maybe ([Xi], [CtEvidence])) 
                                           -- Not quite a WantedEvVar unfortunately
                                           -- Because our intention could be to make 
                                           -- it derived at the end of the day
-- NB: The flavor of the returned EvVars will be decided by the caller
-- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
rewriteWithFunDeps eqn_pred_locs xis fl
 = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
      ; let fd_ev_pos :: [(Int,CtEvidence)]
            fd_ev_pos = concat fd_ev_poss
            rewritten_xis = rewriteDictParams fd_ev_pos xis
      ; if null fd_ev_pos then return Nothing
        else return (Just (rewritten_xis, map snd fd_ev_pos)) }
 where wloc | Given { ctev_gloc = gl } <- fl
            = setCtLocOrigin gl FunDepOrigin
            | otherwise
            = ctev_wloc fl

instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,CtEvidence)]
-- Post: Returns the position index as well as the corresponding FunDep equality
instFunDepEqn wl (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
                        , fd_pred1 = d1, fd_pred2 = d2 })
  = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
       ; foldM (do_one subst) [] eqs }
  where 
    do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
       = let sty1 = Type.substTy subst ty1 
             sty2 = Type.substTy subst ty2 
         in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
            else do { mb_eqv <- newDerived (push_ctx wl) (mkTcEqPred sty1 sty2)
                    ; case mb_eqv of
                         Just ctev -> return $ (i,ctev):ievs
                         Nothing   -> return ievs }
                           -- We are eventually going to emit FD work back in the work list so 
                           -- it is important that we only return the /freshly created/ and not 
                           -- some existing equality!
    push_ctx :: WantedLoc -> WantedLoc 
    push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc


mkEqnMsg :: (TcPredType, SDoc) 
         -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
  = do  { zpred1 <- zonkTcPredType pred1
        ; zpred2 <- zonkTcPredType pred2
	; let { tpred1 = tidyType tidy_env zpred1
              ; tpred2 = tidyType tidy_env zpred2 }
	; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
			  nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
			  nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
	; return (tidy_env, msg) }

rewriteDictParams :: [(Int,CtEvidence)] -- A set of coercions : (pos, ty' ~ ty)
                  -> [Type]             -- A sequence of types: tys
                  -> [Type]                   
rewriteDictParams param_eqs tys
  = zipWith do_one tys [0..]
  where
    do_one :: Type -> Int -> Type
    do_one ty n = case lookup n param_eqs of
                    Just wev -> get_fst_ty wev
                    Nothing  -> ty

    get_fst_ty ctev
      | Just (ty1, _) <- getEqPredTys_maybe (ctEvPred ctev)
      = ty1
      | otherwise 
      = panic "rewriteDictParams: non equality fundep!?"

        
emitFDWorkAsDerived :: [CtEvidence]   -- All Derived
                    -> SubGoalDepth -> TcS () 
emitFDWorkAsDerived evlocs d 
  = updWorkListTcS $ appendWorkListEqs (map mk_fd_ct evlocs)
  where 
    mk_fd_ct der_ev = CNonCanonical { cc_ev = der_ev, cc_depth = d }

topReactionsStage :: SimplifierStage 
topReactionsStage workItem 
 = tryTopReact workItem 
   

tryTopReact :: WorkItem -> TcS StopOrContinue
tryTopReact wi 
 = do { inerts <- getTcSInerts
      ; tir <- doTopReact inerts wi
      ; case tir of 
          NoTopInt -> return (ContinueWith wi)
          SomeTopInt rule what_next 
                   -> do { bumpStepCountTcS 
                         ; traceFireTcS (cc_depth wi) $
                           vcat [ ptext (sLit "Top react:") <+> text rule
                                , text "WorkItem =" <+> ppr wi ]
                         ; return what_next } }

data TopInteractResult 
 = NoTopInt
 | SomeTopInt { tir_rule :: String, tir_new_item :: StopOrContinue }


doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
-- The work item does not react with the inert set, so try interaction with top-level 
-- instances. Note:
--
--   (a) The place to add superclasses in not here in doTopReact stage. 
--       Instead superclasses are added in the worklist as part of the
--       canonicalization process. See Note [Adding superclasses].
--
--   (b) See Note [Given constraint that matches an instance declaration] 
--       for some design decisions for given dictionaries. 

doTopReact inerts workItem
  = do { traceTcS "doTopReact" (ppr workItem)
       ; case workItem of
      	   CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
      	            , cc_depth = d }
      	      -> doTopReactDict inerts workItem fl cls xis d

      	   CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
      	             , cc_rhs = xi, cc_depth = d }
      	      -> doTopReactFunEq fl tc args xi d

      	   _  -> -- Any other work item does not react with any top-level equations
      	         return NoTopInt  }

--------------------
doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
               -> SubGoalDepth -> TcS TopInteractResult
doTopReactDict inerts workItem fl cls xis depth
  = do { instEnvs <- getInstEnvs 
       ; let fd_eqns = improveFromInstEnv instEnvs 
                           (mkClassPred cls xis, arising_sdoc)
             
       ; m <- rewriteWithFunDeps fd_eqns xis fl
       ; case m of
           Just (_xis',fd_work) ->
               do { emitFDWorkAsDerived fd_work depth
                  ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
                                      , tir_new_item = ContinueWith workItem } }
           Nothing 
             | isWanted fl 
             -> do { lkup_inst_res  <- matchClassInst inerts cls xis (getWantedLoc fl)
                   ; case lkup_inst_res of
                       GenInst wtvs ev_term -> 
                         addToSolved fl >> doSolveFromInstance wtvs ev_term
                       NoInstance -> return NoTopInt }
             | otherwise
             -> return NoTopInt }
   where 
     arising_sdoc
       | isGiven fl = pprArisingAt $ getGivenLoc fl
       | otherwise  = pprArisingAt $ getWantedLoc fl
     
     dict_id = ctEvId fl
     
     doSolveFromInstance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
      -- Precondition: evidence term matches the predicate workItem
     doSolveFromInstance evs ev_term 
        | null evs
        = do { traceTcS "doTopReact/found nullary instance for" $
               ppr dict_id
             ; setEvBind dict_id ev_term
             ; return $ 
               SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" 
                          , tir_new_item = Stop } }
        | otherwise 
        = do { traceTcS "doTopReact/found non-nullary instance for" $ 
               ppr dict_id
             ; setEvBind dict_id ev_term
             ; let mk_new_wanted ev
                       = CNonCanonical { cc_ev   = ev
                                       , cc_depth = depth + 1 }
             ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
             ; return $
               SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
                          , tir_new_item = Stop } }

--------------------
doTopReactFunEq :: CtEvidence -> TyCon -> [Xi] -> Xi
                -> SubGoalDepth -> TcS TopInteractResult
doTopReactFunEq fl tc args xi d
  = ASSERT (isSynFamilyTyCon tc) -- No associated data families have 
                                 -- reached that far 

    -- First look in the cache of solved funeqs
    do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
       ; case lookupFamHead fun_eq_cache (mkTyConApp tc args) of {
            Just ctev -> ASSERT( not (isDerived ctev) )
                         ASSERT( isEqPred (ctEvPred ctev) )
                         succeed_with (evTermCoercion (ctEvTerm ctev)) 
                                      (snd (getEqPredTys (ctEvPred ctev))) ;
            Nothing -> 

    -- No cached solved, so look up in top-level instances
    do { match_res <- matchFam tc args   -- See Note [MATCHING-SYNONYMS]
       ; case match_res of {
           Nothing -> return NoTopInt ;
           Just (famInst, rep_tys) -> 

    -- Found a top-level instance
    do {    -- Add it to the solved goals
         unless (isDerived fl) $
         do { addSolvedFunEq fl            
            ; addToSolved fl }

       ; let coe_ax = famInstAxiom famInst 
       ; succeed_with (mkTcAxInstCo coe_ax rep_tys)
                      (mkAxInstRHS coe_ax rep_tys) } } } } }
  where
    succeed_with :: TcCoercion -> TcType -> TcS TopInteractResult
    succeed_with coe rhs_ty 
      = do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
           ; case ctevs of
               [ctev] -> updWorkListTcS $ extendWorkListEq $
                         CNonCanonical { cc_ev = ctev
                                       , cc_depth  = d+1 }
               ctevs -> -- No subgoal (because it's cached)
                        ASSERT( null ctevs) return () 
           ; return $ SomeTopInt { tir_rule = "Fun/Top"
                                 , tir_new_item = Stop } }
      where
        xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
        xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
        xcomp _   = panic "No more goals!"
        xev = XEvTerm xcomp xdecomp

data LookupInstResult
  = NoInstance
  | GenInst [CtEvidence] EvTerm 

matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult

matchClassInst _ clas [ _, ty ] _
  | className clas == singIClassName
  , Just n <- isNumLitTy ty = return $ GenInst [] $ EvLit $ EvNum n

  | className clas == singIClassName
  , Just s <- isStrLitTy ty = return $ GenInst [] $ EvLit $ EvStr s


matchClassInst inerts clas tys loc
   = do { dflags <- getDynFlags
        ; let pred = mkClassPred clas tys 
              incoherent_ok = xopt Opt_IncoherentInstances  dflags
        ; mb_result <- matchClass clas tys
        ; untch <- getUntouchables
        ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
                                           , text "inerts=" <+> ppr inerts
                                           , text "untouchables=" <+> ppr untch ]
        ; case mb_result of
            MatchInstNo   -> return NoInstance
            MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
                                               -- we learn more about the reagent 
            MatchInstSingle (_,_)
              | not incoherent_ok && given_overlap untch 
              -> -- see Note [Instance and Given overlap]
                 do { traceTcS "Delaying instance application" $ 
                       vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
                            , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
                     ; return NoInstance
                     }

            MatchInstSingle (dfun_id, mb_inst_tys) ->
              do { checkWellStagedDFun pred dfun_id loc

                       -- mb_inst_tys :: Maybe TcType 
                       -- See Note [DFunInstType: instantiating types] in InstEnv

                 ; (tys, dfun_phi) <- instDFunType dfun_id mb_inst_tys
                 ; let (theta, _) = tcSplitPhiTy dfun_phi
                 ; if null theta then
                       return (GenInst [] (EvDFunApp dfun_id tys []))
                   else do
                     { evc_vars <- instDFunConstraints loc theta
                     ; let new_ev_vars = freshGoals evc_vars
                           -- new_ev_vars are only the real new variables that can be emitted 
                           dfun_app = EvDFunApp dfun_id tys (getEvTerms evc_vars)
                     ; return $ GenInst new_ev_vars dfun_app } }
        }
   where 
     givens_for_this_clas :: Cts
     givens_for_this_clas 
         = lookupUFM (cts_given (inert_dicts $ inert_cans inerts)) clas 
             `orElse` emptyCts

     given_overlap :: TcsUntouchables -> Bool
     given_overlap untch = anyBag (matchable untch) givens_for_this_clas

     matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys
                               , cc_ev = fl })
       | isGiven fl
       = ASSERT( clas_g == clas )
         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)