compiler/typecheck/TcInteract.lhs

   1 \begin{code}
   2 module TcInteract (
   3      solveInteract, solveInteractGiven, solveInteractWanted,
   4      AtomicInert, tyVarsOfInert,
   5      InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
   6   ) where
   7
   8 #include "HsVersions.h"
   9
  10
  11 import BasicTypes
  12 import TcCanonical
  13 import VarSet
  14 import Type
  15
  16 import Id
  17 import Var
  18
  19 import TcType
  20 import HsBinds
  21
  22 import Inst( tyVarsOfEvVar )
  23 import InstEnv
  24 import Class
  25 import TyCon
  26 import Name
  27
  28 import FunDeps
  29
  30 import Coercion
  31 import Outputable
  32
  33 import TcRnTypes
  34 import TcErrors
  35 import TcSMonad
  36 import Bag
  37 import qualified Data.Map as Map
  38
  39 import Control.Monad( when )
  40
  41 import FastString ( sLit )
  42 import DynFlags
  43 \end{code}
  44
  45 Note [InertSet invariants]
  46 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
  47 An InertSet is a bag of canonical constraints, with the following invariants:
  48
  49   1 No two constraints react with each other.
  50
  51     A tricky case is when there exists a given (solved) dictionary
  52     constraint and a wanted identical constraint in the inert set, but do
  53     not react because reaction would create loopy dictionary evidence for
  54     the wanted. See note [Recursive dictionaries]
  55
  56   2 Given equalities form an idempotent substitution [none of the
  57     given LHS's occur in any of the given RHS's or reactant parts]
  58
  59   3 Wanted equalities also form an idempotent substitution
  60
  61   4 The entire set of equalities is acyclic.
  62
  63   5 Wanted dictionaries are inert with the top-level axiom set
  64
  65   6 Equalities of the form tv1 ~ tv2 always have a touchable variable
  66     on the left (if possible).
  67
  68   7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
  69     will be marked as solved right before being pushed into the inert set.
  70     See note [Touchables and givens].
  71
  72   8 No Given constraint mentions a touchable unification variable,
  73     except if the
  74
  75 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
  76 insertion in the inert list, ie by TcInteract.
  77
  78 During the process of solving, the inert set will contain some
  79 previously given constraints, some wanted constraints, and some given
  80 constraints which have arisen from solving wanted constraints. For
  81 now we do not distinguish between given and solved constraints.
  82
  83 Note that we must switch wanted inert items to given when going under an
  84 implication constraint (when in top-level inference mode).
  85
  86 \begin{code}
  87
  88 data CCanMap a = CCanMap { cts_given   :: Map.Map a CanonicalCts
  89                                           -- Invariant: all Given
  90                          , cts_derived :: Map.Map a CanonicalCts
  91                                           -- Invariant: all Derived
  92                          , cts_wanted  :: Map.Map a CanonicalCts }
  93                                           -- Invariant: all Wanted
  94
  95 cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
  96 cCanMapToBag cmap = Map.fold unionBags rest_wder (cts_given cmap)
  97   where rest_wder = Map.fold unionBags rest_der  (cts_wanted cmap)
  98         rest_der  = Map.fold unionBags emptyCCan (cts_derived cmap)
  99
 100 emptyCCanMap :: CCanMap a
 101 emptyCCanMap = CCanMap { cts_given = Map.empty
 102                        , cts_derived = Map.empty, cts_wanted = Map.empty }
 103
 104 updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
 105 updCCanMap (a,ct) cmap
 106   = case cc_flavor ct of
 107       Wanted {}
 108           -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
 109       Given {}
 110           -> cmap { cts_given = Map.insertWith unionBags a this_ct (cts_given cmap) }
 111       Derived {}
 112           -> cmap { cts_derived = Map.insertWith unionBags a this_ct (cts_derived cmap) }
 113   where this_ct = singleCCan ct
 114
 115 getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
 116 -- Gets the relevant constraints and returns the rest of the CCanMap
 117 getRelevantCts a cmap
 118     = let relevant = unionManyBags [ Map.findWithDefault emptyCCan a (cts_wanted cmap)
 119                                    , Map.findWithDefault emptyCCan a (cts_given cmap)
 120                                    , Map.findWithDefault emptyCCan a (cts_derived cmap) ]
 121           residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
 122                               , cts_given = Map.delete a (cts_given cmap)
 123                               , cts_derived = Map.delete a (cts_derived cmap) }
 124       in (relevant, residual_map)
 125
 126 extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
 127 -- Gets the wanted or derived constraints and returns a residual
 128 -- CCanMap with only givens.
 129 extractUnsolvedCMap cmap =
 130   let wntd = Map.fold unionBags emptyCCan (cts_wanted cmap)
 131       derd = Map.fold unionBags emptyCCan (cts_derived cmap)
 132   in (wntd `unionBags` derd,
 133            cmap { cts_wanted = Map.empty, cts_derived = Map.empty })
 134
 135
 136 -- See Note [InertSet invariants]
 137 data InertSet
 138   = IS { inert_eqs          :: CanonicalCts               -- Equalities only (CTyEqCan)
 139        , inert_dicts        :: CCanMap Class              -- Dictionaries only
 140        , inert_ips          :: CCanMap (IPName Name)      -- Implicit parameters
 141        , inert_frozen       :: CanonicalCts
 142        , inert_funeqs       :: CCanMap TyCon              -- Type family equalities only
 143                -- This representation allows us to quickly get to the relevant
 144                -- inert constraints when interacting a work item with the inert set.
 145        }
 146
 147 tyVarsOfInert :: InertSet -> TcTyVarSet
 148 tyVarsOfInert (IS { inert_eqs    = eqs
 149                   , inert_dicts  = dictmap
 150                   , inert_ips    = ipmap
 151                   , inert_frozen = frozen
 152                   , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts
 153   where
 154     cts = eqs `andCCan` frozen `andCCan` cCanMapToBag dictmap
 155               `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap
 156
 157 instance Outputable InertSet where
 158   ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
 159                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
 160                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
 161                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
 162                 , vcat (map ppr (Bag.bagToList $ inert_frozen is))
 163                 ]
 164
 165 emptyInert :: InertSet
 166 emptyInert = IS { inert_eqs    = Bag.emptyBag
 167                 , inert_frozen = Bag.emptyBag
 168                 , inert_dicts  = emptyCCanMap
 169                 , inert_ips    = emptyCCanMap
 170                 , inert_funeqs = emptyCCanMap }
 171
 172 updInertSet :: InertSet -> AtomicInert -> InertSet
 173 updInertSet is item
 174   | isCTyEqCan item                     -- Other equality
 175   = let eqs' = inert_eqs is `Bag.snocBag` item
 176     in is { inert_eqs = eqs' }
 177   | Just cls <- isCDictCan_Maybe item   -- Dictionary
 178   = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
 179   | Just x  <- isCIPCan_Maybe item      -- IP
 180   = is { inert_ips   = updCCanMap (x,item) (inert_ips is) }
 181   | Just tc <- isCFunEqCan_Maybe item   -- Function equality
 182   = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
 183   | otherwise
 184   = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
 185
 186 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
 187 -- Postcondition: the returned canonical cts are either Derived, or Wanted.
 188 extractUnsolved is@(IS {inert_eqs = eqs})
 189   = let is_solved  = is { inert_eqs    = solved_eqs
 190                         , inert_dicts  = solved_dicts
 191                         , inert_ips    = solved_ips
 192                         , inert_frozen = emptyCCan
 193                         , inert_funeqs = solved_funeqs }
 194     in (is_solved, unsolved)
 195
 196   where (unsolved_eqs, solved_eqs)       = Bag.partitionBag (not.isGivenCt) eqs
 197         (unsolved_ips, solved_ips)       = extractUnsolvedCMap (inert_ips is)
 198         (unsolved_dicts, solved_dicts)   = extractUnsolvedCMap (inert_dicts is)
 199         (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
 200
 201         unsolved = unsolved_eqs `unionBags` inert_frozen is `unionBags`
 202                    unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
 203 \end{code}
 204
 205 %*********************************************************************
 206 %*                                                                   *
 207 *                      Main Interaction Solver                       *
 208 *                                                                    *
 209 **********************************************************************
 210
 211 Note [Basic plan]
 212 ~~~~~~~~~~~~~~~~~
 213 1. Canonicalise (unary)
 214 2. Pairwise interaction (binary)
 215     * Take one from work list
 216     * Try all pair-wise interactions with each constraint in inert
 217
 218    As an optimisation, we prioritize the equalities both in the
 219    worklist and in the inerts.
 220
 221 3. Try to solve spontaneously for equalities involving touchables
 222 4. Top-level interaction (binary wrt top-level)
 223    Superclass decomposition belongs in (4), see note [Superclasses]
 224
 225 \begin{code}
 226 type AtomicInert = CanonicalCt     -- constraint pulled from InertSet
 227 type WorkItem    = CanonicalCt     -- constraint pulled from WorkList
 228
 229 -- A mixture of Given, Wanted, and Derived constraints.
 230 -- We split between equalities and the rest to process equalities first.
 231 type WorkList = CanonicalCts
 232
 233 unionWorkLists :: WorkList -> WorkList -> WorkList
 234 unionWorkLists = andCCan
 235
 236 isEmptyWorkList :: WorkList -> Bool
 237 isEmptyWorkList = isEmptyCCan
 238
 239 emptyWorkList :: WorkList
 240 emptyWorkList = emptyCCan
 241
 242 workListFromCCan :: CanonicalCt -> WorkList
 243 workListFromCCan = singleCCan
 244
 245 ------------------------
 246 data StopOrContinue
 247   = Stop                        -- Work item is consumed
 248   | ContinueWith WorkItem       -- Not consumed
 249
 250 instance Outputable StopOrContinue where
 251   ppr Stop             = ptext (sLit "Stop")
 252   ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
 253
 254 -- Results after interacting a WorkItem as far as possible with an InertSet
 255 data StageResult
 256   = SR { sr_inerts     :: InertSet
 257            -- The new InertSet to use (REPLACES the old InertSet)
 258        , sr_new_work   :: WorkList
 259            -- Any new work items generated (should be ADDED to the old WorkList)
 260            -- Invariant:
 261            --    sr_stop = Just workitem => workitem is *not* in sr_inerts and
 262            --                               workitem is inert wrt to sr_inerts
 263        , sr_stop       :: StopOrContinue
 264        }
 265
 266 instance Outputable StageResult where
 267   ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
 268     = ptext (sLit "SR") <+>
 269       braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
 270                   , ptext (sLit "new work =") <+> ppr work <> comma
 271                   , ptext (sLit "stop =") <+> ppr stop])
 272
 273 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
 274
 275 -- Combine a sequence of simplifier 'stages' to create a pipeline
 276 runSolverPipeline :: [(String, SimplifierStage)]
 277                   -> InertSet -> WorkItem
 278                   -> TcS (InertSet, WorkList)
 279 -- Precondition: non-empty list of stages
 280 runSolverPipeline pipeline inerts workItem
 281   = do { traceTcS "Start solver pipeline" $
 282             vcat [ ptext (sLit "work item =") <+> ppr workItem
 283                  , ptext (sLit "inerts    =") <+> ppr inerts]
 284
 285        ; let itr_in = SR { sr_inerts = inerts
 286                         , sr_new_work = emptyWorkList
 287                         , sr_stop = ContinueWith workItem }
 288        ; itr_out <- run_pipeline pipeline itr_in
 289        ; let new_inert
 290               = case sr_stop itr_out of
 291                   Stop              -> sr_inerts itr_out
 292                   ContinueWith item -> sr_inerts itr_out `updInertSet` item
 293        ; return (new_inert, sr_new_work itr_out) }
 294   where
 295     run_pipeline :: [(String, SimplifierStage)]
 296                  -> StageResult -> TcS StageResult
 297     run_pipeline [] itr                         = return itr
 298     run_pipeline _  itr@(SR { sr_stop = Stop }) = return itr
 299
 300     run_pipeline ((name,stage):stages)
 301                  (SR { sr_new_work = accum_work
 302                      , sr_inerts   = inerts
 303                      , sr_stop     = ContinueWith work_item })
 304       = do { itr <- stage work_item inerts
 305            ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
 306            ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
 307            ; run_pipeline stages itr' }
 308 \end{code}
 309
 310 Example 1:
 311   Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
 312   Reagent: a ~ [b] (given)
 313
 314 React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
 315 React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
 316 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []
 317
 318 Example 2:
 319   Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
 320   Reagent: a ~w [b]
 321
 322 React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
 323 React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
 324 etc.
 325
 326 Example 3:
 327   Inert:  {a ~ Int, F Int ~ b} (given)
 328   Reagent: F a ~ b (wanted)
 329
 330 React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
 331 React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing
 332
 333 \begin{code}
 334 -- Main interaction solver: we fully solve the worklist 'in one go',
 335 -- returning an extended inert set.
 336 --
 337 -- See Note [Touchables and givens].
 338 solveInteractGiven :: InertSet -> GivenLoc -> [EvVar] -> TcS InertSet
 339 solveInteractGiven inert gloc evs
 340   = do { (_, inert_ret) <- solveInteract inert $ listToBag $
 341                            map mk_given evs
 342        ; return inert_ret }
 343   where
 344     flav = Given gloc
 345     mk_given ev = mkEvVarX ev flav
 346
 347 solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet
 348 solveInteractWanted inert wvs
 349   = do { (_,inert_ret) <- solveInteract inert $ listToBag $
 350                           map wantedToFlavored wvs
 351        ; return inert_ret }
 352
 353 solveInteract :: InertSet -> Bag FlavoredEvVar -> TcS (Bool, InertSet)
 354 -- Post: (True,  inert_set) means we managed to discharge all constraints
 355 --                          without actually doing any interactions!
 356 --       (False, inert_set) means some interactions occurred
 357 solveInteract inert ws
 358   = do { dyn_flags <- getDynFlags
 359        ; sctx <- getTcSContext
 360
 361        ; traceTcS "solveInteract, before clever canonicalization:" $
 362          vcat [ text "ws = " <+>  ppr (mapBag (\(EvVarX ev ct)
 363                                                    -> (ct,evVarPred ev)) ws)
 364               , text "inert = " <+> ppr inert ]
 365
 366        ; (flag, inert_ret) <- foldlBagM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) ws
 367
 368        ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
 369          vcat [ text "No interaction happened = " <+> ppr flag
 370               , text "inert_ret = " <+> ppr inert_ret ]
 371
 372        ; return (flag, inert_ret) }
 373
 374
 375 tryPreSolveAndInteract :: SimplContext
 376                        -> DynFlags
 377                        -> (Bool, InertSet)
 378                        -> FlavoredEvVar
 379                        -> TcS (Bool, InertSet)
 380 -- Returns: True if it was able to discharge this constraint AND all previous ones
 381 tryPreSolveAndInteract sctx dyn_flags (all_previous_discharged, inert)
 382                        flavev@(EvVarX ev_var fl)
 383   = do { let inert_cts = get_inert_cts (evVarPred ev_var)
 384
 385        ; this_one_discharged <- dischargeFromCCans inert_cts flavev
 386
 387        ; if this_one_discharged
 388          then return (all_previous_discharged, inert)
 389
 390          else do
 391        { extra_cts <- mkCanonical fl ev_var
 392        ; inert_ret <- solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[])
 393                                              inert extra_cts
 394        ; return (False, inert_ret) } }
 395
 396   where
 397     get_inert_cts (ClassP clas _)
 398       | simplEqsOnly sctx = emptyCCan
 399       | otherwise         = fst (getRelevantCts clas (inert_dicts inert))
 400     get_inert_cts (IParam {})
 401       = emptyCCan -- We must not do the same thing for IParams, because (contrary
 402                   -- to dictionaries), work items /must/ override inert items.
 403                  -- See Note [Overriding implicit parameters] in TcInteract.
 404     get_inert_cts (EqPred {})
 405       = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
 406
 407 dischargeFromCCans :: CanonicalCts -> FlavoredEvVar -> TcS Bool
 408 dischargeFromCCans cans (EvVarX ev fl)
 409   = Bag.foldlBagM discharge_ct False cans
 410   where discharge_ct :: Bool -> CanonicalCt -> TcS Bool
 411         discharge_ct True _ct = return True
 412         discharge_ct False ct
 413           | evVarPred (cc_id ct) `tcEqPred` evVarPred ev
 414           , cc_flavor ct `canSolve` fl
 415           = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct)
 416                ; return True }
 417           where set_ev_bind x y
 418                     | EqPred {} <- evVarPred y
 419                     = setEvBind x (EvCoercion (mkCoVarCoercion y))
 420                     | otherwise = setEvBind x (EvId y)
 421         discharge_ct False _ct = return False
 422 \end{code}
 423
 424 Note [Avoiding the superclass explosion]
 425 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 426 This note now is not as significant as it used to be because we no
 427 longer add the superclasses of Wanted as Derived, except only if they
 428 have equality superclasses or superclasses with functional
 429 dependencies. The fear was that hundreds of identical wanteds would
 430 give rise each to the same superclass or equality Derived's which
 431 would lead to a blo-up in the number of interactions.
 432
 433 Instead, what we do with tryPreSolveAndCanon, is when we encounter a
 434 new constraint, we very quickly see if it can be immediately
 435 discharged by a class constraint in our inert set or the previous
 436 canonicals. If so, we add nothing to the returned canonical
 437 constraints.
 438
 439 \begin{code}
 440 solveOne :: InertSet -> WorkItem -> TcS InertSet
 441 solveOne inerts workItem
 442   = do { dyn_flags <- getDynFlags
 443        ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
 444        }
 445
 446 -----------------
 447 solveInteractWithDepth :: (Int, Int, [WorkItem])
 448                        -> InertSet -> WorkList -> TcS InertSet
 449 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
 450   | isEmptyWorkList ws
 451   = return inert
 452
 453   | n > max_depth
 454   = solverDepthErrorTcS n stack
 455
 456   | otherwise
 457   = do { traceTcS "solveInteractWithDepth" $
 458               vcat [ text "Current depth =" <+> ppr n
 459                    , text "Max depth =" <+> ppr max_depth ]
 460
 461               -- Solve equalities first
 462        ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
 463        ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
 464        ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
 465
 466 ------------------
 467 -- Fully interact the given work item with an inert set, and return a
 468 -- new inert set which has assimilated the new information.
 469 solveOneWithDepth :: (Int, Int, [WorkItem])
 470                   -> InertSet -> WorkItem -> TcS InertSet
 471 solveOneWithDepth (max_depth, n, stack) inert work
 472   = do { traceTcS0 (indent ++ "Solving {") (ppr work)
 473        ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
 474
 475        ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
 476
 477          -- Recursively solve the new work generated
 478          -- from workItem, with a greater depth
 479        ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
 480                                 new_inert new_work
 481
 482        ; traceTcS0 (indent ++ "Done }") (ppr work)
 483        ; return res_inert }
 484   where
 485     indent = replicate (2*n) ' '
 486
 487 thePipeline :: [(String,SimplifierStage)]
 488 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
 489               , ("interact with inerts",    interactWithInertsStage)
 490               , ("spontaneous solve",       spontaneousSolveStage)
 491               , ("top-level reactions",     topReactionsStage) ]
 492 \end{code}
 493
 494 *********************************************************************************
 495 *                                                                               *
 496                        The spontaneous-solve Stage
 497 *                                                                               *
 498 *********************************************************************************
 499
 500 Note [Efficient Orientation]
 501 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 502
 503 There are two cases where we have to be careful about
 504 orienting equalities to get better efficiency.
 505
 506 Case 1: In Rewriting Equalities (function rewriteEqLHS)
 507
 508     When rewriting two equalities with the same LHS:
 509           (a)  (tv ~ xi1)
 510           (b)  (tv ~ xi2)
 511     We have a choice of producing work (xi1 ~ xi2) (up-to the
 512     canonicalization invariants) However, to prevent the inert items
 513     from getting kicked out of the inerts first, we prefer to
 514     canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
 515     ~ xi1) if (a) comes from the inert set.
 516
 517     This choice is implemented using the WhichComesFromInert flag.
 518
 519 Case 2: Functional Dependencies
 520     Again, we should prefer, if possible, the inert variables on the RHS
 521
 522 Case 3: IP improvement work
 523     We must always rewrite so that the inert type is on the right.
 524
 525 \begin{code}
 526 spontaneousSolveStage :: SimplifierStage
 527 spontaneousSolveStage workItem inerts
 528   = do { mSolve <- trySpontaneousSolve workItem
 529
 530        ; case mSolve of
 531            SPCantSolve -> -- No spontaneous solution for him, keep going
 532                return $ SR { sr_new_work   = emptyWorkList
 533                            , sr_inerts     = inerts
 534                            , sr_stop       = ContinueWith workItem }
 535
 536            SPSolved workItem'
 537                | not (isGivenCt workItem)
 538                  -- Original was wanted or derived but we have now made him
 539                  -- given so we have to interact him with the inerts due to
 540                  -- its status change. This in turn may produce more work.
 541                  -- We do this *right now* (rather than just putting workItem'
 542                  -- back into the work-list) because we've solved
 543                -> do { (new_inert, new_work) <- runSolverPipeline
 544                              [ ("recursive interact with inert eqs", interactWithInertEqsStage)
 545                              , ("recursive interact with inerts", interactWithInertsStage)
 546                              ] inerts workItem'
 547                      ; return $ SR { sr_new_work = new_work
 548                                    , sr_inerts   = new_inert -- will include workItem'
 549                                    , sr_stop     = Stop }
 550                      }
 551                | otherwise
 552                    -> -- Original was given; he must then be inert all right, and
 553                       -- workList' are all givens from flattening
 554                       return $ SR { sr_new_work = emptyWorkList
 555                                   , sr_inerts   = inerts `updInertSet` workItem'
 556                                   , sr_stop     = Stop }
 557            SPError -> -- Return with no new work
 558                return $ SR { sr_new_work = emptyWorkList
 559                            , sr_inerts   = inerts
 560                            , sr_stop     = Stop }
 561        }
 562
 563 data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError
 564 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
 565 -- SPSolved workItem' gives us a new *given* to go on
 566 -- SPError means that it's completely impossible to solve this equality, eg due to a kind error
 567
 568
 569 -- @trySpontaneousSolve wi@ solves equalities where one side is a
 570 -- touchable unification variable.
 571 --          See Note [Touchables and givens]
 572 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
 573 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
 574   | isGiven gw
 575   = return SPCantSolve
 576   | Just tv2 <- tcGetTyVar_maybe xi
 577   = do { tch1 <- isTouchableMetaTyVar tv1
 578        ; tch2 <- isTouchableMetaTyVar tv2
 579        ; case (tch1, tch2) of
 580            (True,  True)  -> trySpontaneousEqTwoWay cv gw tv1 tv2
 581            (True,  False) -> trySpontaneousEqOneWay cv gw tv1 xi
 582            (False, True)  -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
 583            _ -> return SPCantSolve }
 584   | otherwise
 585   = do { tch1 <- isTouchableMetaTyVar tv1
 586        ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
 587                  else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
 588                          ; return SPCantSolve }
 589        }
 590
 591   -- No need for
 592   --      trySpontaneousSolve (CFunEqCan ...) = ...
 593   -- See Note [No touchables as FunEq RHS] in TcSMonad
 594 trySpontaneousSolve _ = return SPCantSolve
 595
 596 ----------------
 597 trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
 598 -- tv is a MetaTyVar, not untouchable
 599 trySpontaneousEqOneWay cv gw tv xi
 600   | not (isSigTyVar tv) || isTyVarTy xi
 601   = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts
 602                                -- so we have its more specific kind in our hands
 603        ; if kxi `isSubKind` tyVarKind tv then
 604              solveWithIdentity cv gw tv xi
 605          else return SPCantSolve
 606 {-
 607          else if tyVarKind tv `isSubKind` kxi then
 608              return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way
 609                                 -- This case covers the  a_touchable :: * ~ b_untouchable :: ??
 610                                 -- which has to be deferred or floated out for someone else to solve
 611                                 -- it in a scope where 'b' is no longer untouchable.
 612          else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors]
 613                  ; return SPError }
 614 -}
 615        }
 616   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
 617   = return SPCantSolve
 618
 619 ----------------
 620 trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
 621 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
 622 trySpontaneousEqTwoWay cv gw tv1 tv2
 623   | k1 `isSubKind` k2
 624   , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
 625   | k2 `isSubKind` k1
 626   = solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
 627   | otherwise -- None is a subkind of the other, but they are both touchable!
 628   = return SPCantSolve
 629     -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
 630     --   ; return SPError }
 631   where
 632     k1 = tyVarKind tv1
 633     k2 = tyVarKind tv2
 634     nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
 635 \end{code}
 636
 637 Note [Kind errors]
 638 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 639 Consider the wanted problem:
 640       alpha ~ (# Int, Int #)
 641 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
 642 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
 643 simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and
 644 get quantified over in inference mode. That's bad because we do know at this point that the
 645 constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
 646
 647 The same applies in canonicalization code in case of kind errors in the givens.
 648
 649 However, when we canonicalize givens we only check for compatibility (@compatKind@).
 650 If there were a kind error in the givens, this means some form of inconsistency or dead code.
 651
 652 You may think that when we spontaneously solve wanteds we may have to look through the
 653 bindings to determine the right kind of the RHS type. E.g one may be worried that xi is
 654 @alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
 655 But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
 656 so this situation can't happen.
 657
 658 Note [Spontaneous solving and kind compatibility]
 659 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 660 Note that our canonical constraints insist that *all* equalities (tv ~
 661 xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
 662 the same kinds.  ("compatible" means one is a subKind of the other.)
 663
 664   - It can't be *equal* kinds, because
 665      b) wanted constraints don't necessarily have identical kinds
 666                eg   alpha::? ~ Int
 667      b) a solved wanted constraint becomes a given
 668
 669   - SPJ thinks that *given* constraints (tv ~ tau) always have that
 670     tau has a sub-kind of tv; and when solving wanted constraints
 671     in trySpontaneousEqTwoWay we re-orient to achieve this.
 672
 673   - Note that the kind invariant is maintained by rewriting.
 674     Eg wanted1 rewrites wanted2; if both were compatible kinds before,
 675        wanted2 will be afterwards.  Similarly givens.
 676
 677 Caveat:
 678   - Givens from higher-rank, such as:
 679           type family T b :: * -> * -> *
 680           type instance T Bool = (->)
 681
 682           f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
 683           flop = f (...) True
 684      Whereas we would be able to apply the type instance, we would not be able to
 685      use the given (T Bool ~ (->)) in the body of 'flop'
 686
 687
 688 Note [Avoid double unifications]
 689 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 690 The spontaneous solver has to return a given which mentions the unified unification
 691 variable *on the left* of the equality. Here is what happens if not:
 692   Original wanted:  (a ~ alpha),  (alpha ~ Int)
 693 We spontaneously solve the first wanted, without changing the order!
 694       given : a ~ alpha      [having unified alpha := a]
 695 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
 696 At the end we spontaneously solve that guy, *reunifying*  [alpha := Int]
 697
 698 We avoid this problem by orienting the resulting given so that the unification
 699 variable is on the left.  [Note that alternatively we could attempt to
 700 enforce this at canonicalization]
 701
 702 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
 703 double unifications is the main reason we disallow touchable
 704 unification variables as RHS of type family equations: F xis ~ alpha.
 705
 706 \begin{code}
 707 ----------------
 708
 709 solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
 710 -- Solve with the identity coercion
 711 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 712 -- Precondition: CtFlavor is Wanted or Derived
 713 -- See [New Wanted Superclass Work] to see why solveWithIdentity
 714 --     must work for Derived as well as Wanted
 715 -- Returns: workItem where
 716 --        workItem = the new Given constraint
 717 solveWithIdentity cv wd tv xi
 718   = do { traceTcS "Sneaky unification:" $
 719                        vcat [text "Coercion variable:  " <+> ppr wd,
 720                              text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
 721                              text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
 722                              text "Right Kind is     : " <+> ppr (typeKind xi)
 723                   ]
 724
 725        ; setWantedTyBind tv xi
 726        ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi
 727
 728        ; when (isWanted wd) (setWantedCoBind cv xi)
 729            -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
 730
 731        ; return $ SPSolved (CTyEqCan { cc_id = cv_given
 732                                      , cc_flavor = mkGivenFlavor wd UnkSkol
 733                                      , cc_tyvar  = tv, cc_rhs = xi }) }
 734 \end{code}
 735
 736
 737
 738
 739 *********************************************************************************
 740 *                                                                               *
 741                        The interact-with-inert Stage
 742 *                                                                               *
 743 *********************************************************************************
 744
 745 \begin{code}
 746 -- Interaction result of  WorkItem <~> AtomicInert
 747 data InteractResult
 748    = IR { ir_stop         :: StopOrContinue
 749             -- Stop
 750             --   => Reagent (work item) consumed.
 751             -- ContinueWith new_reagent
 752             --   => Reagent transformed but keep gathering interactions.
 753             --      The transformed item remains inert with respect
 754             --      to any previously encountered inerts.
 755
 756         , ir_inert_action :: InertAction
 757             -- Whether the inert item should remain in the InertSet.
 758
 759         , ir_new_work     :: WorkList
 760             -- new work items to add to the WorkList
 761         }
 762
 763 -- What to do with the inert reactant.
 764 data InertAction = KeepInert
 765                  | DropInert
 766                  | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert
 767
 768 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
 769 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
 770
 771 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
 772 mkIRStop keep newWork = return $ IR Stop keep newWork
 773
 774 dischargeWorkItem :: Monad m => m InteractResult
 775 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
 776
 777 noInteraction :: Monad m => WorkItem -> m InteractResult
 778 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
 779
 780 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
 781      -- See Note [Efficient Orientation]
 782
 783
 784 ---------------------------------------------------
 785 -- Interact a single WorkItem with the equalities of an inert set as
 786 -- far as possible, i.e. until we get a Stop result from an individual
 787 -- reaction (i.e. when the WorkItem is consumed), or until we've
 788 -- interact the WorkItem with the entire equalities of the InertSet
 789
 790 interactWithInertEqsStage :: SimplifierStage
 791 interactWithInertEqsStage workItem inert
 792   = Bag.foldlBagM interactNext initITR (inert_eqs inert)
 793   where
 794     initITR = SR { sr_inerts   = inert { inert_eqs = emptyCCan }
 795                  , sr_new_work = emptyWorkList
 796                  , sr_stop     = ContinueWith workItem }
 797
 798 ---------------------------------------------------
 799 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
 800 -- Precondition: equality interactions must have already happened, hence we have
 801 -- to pick up some information from the incoming inert, before folding over the
 802 -- "Other" constraints it contains!
 803
 804 interactWithInertsStage :: SimplifierStage
 805 interactWithInertsStage workItem inert
 806   = let (relevant, inert_residual) = getISRelevant workItem inert
 807         initITR = SR { sr_inerts   = inert_residual
 808                      , sr_new_work = emptyWorkList
 809                      , sr_stop     = ContinueWith workItem }
 810     in Bag.foldlBagM interactNext initITR relevant
 811   where
 812     getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
 813     getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
 814                   -- Nothing s relevant; we have alread interacted
 815                   -- it with the equalities in the inert set
 816
 817     getISRelevant (CDictCan { cc_class = cls } ) is
 818       = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
 819         in (relevant, is { inert_dicts = residual_map })
 820     getISRelevant (CFunEqCan { cc_fun = tc } ) is
 821       = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
 822         in (relevant, is { inert_funeqs = residual_map })
 823     getISRelevant (CIPCan { cc_ip_nm = nm }) is
 824       = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
 825         in (relevant, is { inert_ips = residual_map })
 826     -- An equality, finally, may kick everything except equalities out
 827     -- because we have already interacted the equalities in interactWithInertEqsStage
 828     getISRelevant _eq_ct is  -- Equality, everything is relevant for this one
 829                              -- TODO: if we were caching variables, we'd know that only
 830                              --       some are relevant. Experiment with this for now.
 831       = let cts = cCanMapToBag (inert_ips is) `unionBags`
 832                     cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
 833         in (cts, is { inert_dicts  = emptyCCanMap
 834                     , inert_ips    = emptyCCanMap
 835                     , inert_funeqs = emptyCCanMap })
 836
 837 interactNext :: StageResult -> AtomicInert -> TcS StageResult
 838 interactNext it inert
 839   | ContinueWith workItem <- sr_stop it
 840   = do { let inerts      = sr_inerts it
 841
 842        ; ir <- interactWithInert inert workItem
 843
 844        -- New inerts depend on whether we KeepInert or not and must
 845        -- be updated with FD improvement information from the interaction result (ir)
 846        ; let inerts_new = case ir_inert_action ir of
 847                             KeepInert                   -> inerts `updInertSet` inert
 848                             DropInert                   -> inerts
 849                             KeepTransformedInert inert' -> inerts `updInertSet` inert'
 850
 851        ; return $ SR { sr_inerts   = inerts_new
 852                      , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
 853                      , sr_stop     = ir_stop ir } }
 854   | otherwise
 855   = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
 856
 857 -- Do a single interaction of two constraints.
 858 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
 859 interactWithInert inert workitem
 860   =  do { ctxt <- getTcSContext
 861         ; let is_allowed  = allowedInteraction (simplEqsOnly ctxt) inert workitem
 862
 863         ; if is_allowed then
 864               doInteractWithInert inert workitem
 865           else
 866               noInteraction workitem
 867         }
 868
 869 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
 870 -- Allowed interactions
 871 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
 872 allowedInteraction eqs_only (CIPCan {})   (CIPCan {})   = not eqs_only
 873 allowedInteraction _ _ _ = True
 874
 875 --------------------------------------------
 876 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
 877 -- Identical class constraints.
 878
 879 doInteractWithInert
 880            (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
 881   workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
 882   | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
 883   = solveOneFromTheOther (d1,fl1) workItem
 884
 885   | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
 886   =      -- See Note [When improvement happens]
 887     do { let pty1 = ClassP cls1 tys1
 888              pty2 = ClassP cls2 tys2
 889              work_item_pred_loc = (pty2, pprFlavorArising fl2)
 890              inert_pred_loc     = (pty1, pprFlavorArising fl1)
 891              loc                = combineCtLoc fl1 fl2
 892              eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
 893                              -- See Note [Efficient Orientation]
 894
 895        ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
 896        ; fd_work <- mapM mkCanonicalFEV derived_evs
 897                  -- See Note [Generating extra equalities]
 898
 899        ; mkIRContinue workItem KeepInert (unionManyBags fd_work)
 900        }
 901
 902 -- Class constraint and given equality: use the equality to rewrite
 903 -- the class constraint.
 904 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
 905                     (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
 906   | ifl `canRewrite` wfl
 907   , tv `elemVarSet` tyVarsOfTypes xis
 908   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
 909             -- Continue with rewritten Dictionary because we can only be in the
 910             -- interactWithEqsStage, so the dictionary is inert.
 911        ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
 912
 913 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
 914            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
 915   | wfl `canRewrite` ifl
 916   , tv `elemVarSet` tyVarsOfTypes xis
 917   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
 918        ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
 919
 920 -- Class constraint and given equality: use the equality to rewrite
 921 -- the class constraint.
 922 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
 923                     (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
 924   | ifl `canRewrite` wfl
 925   , tv `elemVarSet` tyVarsOfType ty
 926   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
 927        ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
 928
 929 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
 930            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
 931   | wfl `canRewrite` ifl
 932   , tv `elemVarSet` tyVarsOfType ty
 933   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
 934        ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
 935
 936 -- Two implicit parameter constraints.  If the names are the same,
 937 -- but their types are not, we generate a wanted type equality
 938 -- that equates the type (this is "improvement").
 939 -- However, we don't actually need the coercion evidence,
 940 -- so we just generate a fresh coercion variable that isn't used anywhere.
 941 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
 942            workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
 943   | nm1 == nm2 && isGiven wfl && isGiven ifl
 944   =     -- See Note [Overriding implicit parameters]
 945         -- Dump the inert item, override totally with the new one
 946         -- Do not require type equality
 947     mkIRContinue workItem DropInert emptyWorkList
 948
 949   | nm1 == nm2 && ty1 `tcEqType` ty2
 950   = solveOneFromTheOther (id1,ifl) workItem
 951
 952   | nm1 == nm2
 953   =     -- See Note [When improvement happens]
 954     do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
 955        ; let flav = Wanted (combineCtLoc ifl wfl)
 956        ; cans <- mkCanonical flav co_var
 957        ; mkIRContinue workItem KeepInert cans }
 958
 959
 960
 961 -- Never rewrite a given with a wanted equality, and a type function
 962 -- equality can never rewrite an equality. We rewrite LHS *and* RHS
 963 -- of function equalities so that our inert set exposes everything that
 964 -- we know about equalities.
 965
 966 -- Inert: equality, work item: function equality
 967 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
 968                     (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
 969                                , cc_tyargs = args, cc_rhs = xi2 })
 970   | ifl `canRewrite` wfl
 971   , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
 972   = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
 973        ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
 974          -- Must Stop here, because we may no longer be inert after the rewritting.
 975
 976 -- Inert: function equality, work item: equality
 977 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
 978                               , cc_tyargs = args, cc_rhs = xi1 })
 979            workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
 980   | wfl `canRewrite` ifl
 981   , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
 982   = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
 983        ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
 984          -- One may think that we could (KeepTransformedInert rewritten_funeq)
 985          -- but that is wrong, because it may end up not being inert with respect
 986          -- to future inerts. Example:
 987          -- Original inert = {    F xis ~  [a], b ~ Maybe Int }
 988          -- Work item comes along = a ~ [b]
 989          -- If we keep { F xis ~ [b] } in the inert set we will end up with:
 990          --      { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] }
 991          -- At the end, which is *not* inert. So we should unfortunately DropInert here.
 992
 993 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
 994                                , cc_tyargs = args1, cc_rhs = xi1 })
 995            workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
 996                                , cc_tyargs = args2, cc_rhs = xi2 })
 997   | fl1 `canSolve` fl2 && lhss_match
 998   = do { cans <- rewriteEqLHS LeftComesFromInert  (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
 999        ; mkIRStop KeepInert cans }
1000   | fl2 `canSolve` fl1 && lhss_match
1001   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1002        ; mkIRContinue workItem DropInert cans }
1003   where
1004     lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1005
1006 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1007            workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1008 -- Check for matching LHS
1009   | fl1 `canSolve` fl2 && tv1 == tv2
1010   = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1011        ; mkIRStop KeepInert cans }
1012
1013   | fl2 `canSolve` fl1 && tv1 == tv2
1014   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1015        ; mkIRContinue workItem DropInert cans }
1016 -- Check for rewriting RHS
1017   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1018   = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1019        ; mkIRStop KeepInert rewritten_eq }
1020   | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1021   = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1022        ; mkIRContinue workItem DropInert rewritten_eq }
1023
1024 doInteractWithInert (CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1025                     (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1026   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1027   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1028        ; mkIRStop KeepInert rewritten_frozen }
1029
1030 doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1031            workItem@(CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1032   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1033   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1034        ; mkIRContinue workItem DropInert rewritten_frozen }
1035
1036 -- Fall-through case for all other situations
1037 doInteractWithInert _ workItem = noInteraction workItem
1038
1039 -------------------------
1040 -- Equational Rewriting
1041 rewriteDict  :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1042 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1043   = do { let cos  = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1044              args = substTysWith [tv] [xi] xis
1045              con  = classTyCon cl
1046              dict_co = mkTyConCoercion con cos
1047        ; dv' <- newDictVar cl args
1048        ; case gw of
1049            Wanted {}         -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1050            Given {}          -> setDictBind dv' (EvCast dv dict_co)
1051            Derived {}        -> return () -- Derived dicts we don't set any evidence
1052
1053        ; return (CDictCan { cc_id = dv'
1054                           , cc_flavor = gw
1055                           , cc_class = cl
1056                           , cc_tyargs = args }) }
1057
1058 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1059 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1060   = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty     -- ty[tv] ~ t[xi]
1061              ty'   = substTyWith [tv] [xi] ty
1062        ; ipid' <- newIPVar nm ty'
1063        ; case gw of
1064            Wanted {}         -> setIPBind ipid  (EvCast ipid' (mkSymCoercion ip_co))
1065            Given {}          -> setIPBind ipid' (EvCast ipid ip_co)
1066            Derived {}        -> return () -- Derived ips: we don't set any evidence
1067
1068        ; return (CIPCan { cc_id = ipid'
1069                         , cc_flavor = gw
1070                         , cc_ip_nm = nm
1071                         , cc_ip_ty = ty' }) }
1072
1073 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1074 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)                   -- cv2 :: F args ~ xi2
1075   = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1076              args'   = substTysWith [tv] [xi1] args
1077              fun_co  = mkTyConCoercion tc arg_cos                 -- fun_co :: F args ~ F args'
1078
1079              xi2'    = substTyWith [tv] [xi1] xi2
1080              xi2_co  = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2'
1081        ; cv2' <- case gw of
1082                    Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2'
1083                                    ; setWantedCoBind cv2 $
1084                                      fun_co `mkTransCoercion`
1085                                             mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co
1086                                    ; return cv2' }
1087                    Given {}  -> newGivenCoVar (mkTyConApp tc args') xi2' $
1088                                   mkSymCoercion fun_co `mkTransCoercion`
1089                                                 mkCoVarCoercion cv2 `mkTransCoercion` xi2_co
1090                    Derived {} -> newDerivedId (EqPred (mkTyConApp tc args') xi2')
1091
1092        ; return (CFunEqCan { cc_id = cv2'
1093                            , cc_flavor = gw
1094                            , cc_tyargs = args'
1095                            , cc_fun = tc
1096                            , cc_rhs = xi2' }) }
1097
1098
1099 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1100 -- Use the first equality to rewrite the second, flavors already checked.
1101 -- E.g.          c1 : tv1 ~ xi1   c2 : tv2 ~ xi2
1102 -- rewrites c2 to give
1103 --               c2' : tv2 ~ xi2[xi1/tv1]
1104 -- We must do an occurs check to sure the new constraint is canonical
1105 -- So we might return an empty bag
1106 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1107   | Just tv2' <- tcGetTyVar_maybe xi2'
1108   , tv2 == tv2'  -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1109   = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1110        ; return emptyCCan }
1111   | otherwise
1112   = do { cv2' <-
1113            case gw of
1114              Wanted {}
1115                  -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1116                        ; setWantedCoBind cv2 $
1117                          mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1118                        ; return cv2' }
1119              Given {}
1120                  -> newGivenCoVar (mkTyVarTy tv2) xi2' $
1121                     mkCoVarCoercion cv2 `mkTransCoercion` co2'
1122              Derived {}
1123                  -> newDerivedId (EqPred (mkTyVarTy tv2) xi2')
1124
1125        ; canEq gw cv2' (mkTyVarTy tv2) xi2'
1126        }
1127   where
1128     xi2' = substTyWith [tv1] [xi1] xi2
1129     co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2  -- xi2 ~ xi2[xi1/tv1]
1130
1131
1132 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1133 -- Used to ineract two equalities of the following form:
1134 -- First Equality:   co1: (XXX ~ xi1)
1135 -- Second Equality:  cv2: (XXX ~ xi2)
1136 -- Where the cv1 `canSolve` cv2 equality
1137 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1138 --    See Note [Efficient Orientation] for that
1139 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1140   = do { cv2' <- case (isWanted gw, which) of
1141                    (True,LeftComesFromInert) ->
1142                        do { cv2' <- newWantedCoVar xi2 xi1
1143                           ; setWantedCoBind cv2 $
1144                             co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1145                           ; return cv2' }
1146                    (True,RightComesFromInert) ->
1147                        do { cv2' <- newWantedCoVar xi1 xi2
1148                           ; setWantedCoBind cv2 $
1149                             co1 `mkTransCoercion` mkCoVarCoercion cv2'
1150                           ; return cv2' }
1151                    (False,LeftComesFromInert) ->
1152                        if isGiven gw then
1153                            newGivenCoVar xi2 xi1 $
1154                            mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1155                        else newDerivedId (EqPred xi2 xi1)
1156                    (False,RightComesFromInert) ->
1157                        if isGiven gw then
1158                            newGivenCoVar xi1 xi2 $
1159                            mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1160                        else newDerivedId (EqPred xi1 xi2)
1161        ; mkCanonical gw cv2' }
1162
1163 rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList
1164 rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1165   = do { cv2' <-
1166            case fl2 of
1167              Wanted {} -> do { cv2' <- newWantedCoVar ty2a' ty2b'
1168                                     -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
1169                              ; setWantedCoBind cv2 $
1170                                  co2a'                `mkTransCoercion`
1171                                  mkCoVarCoercion cv2' `mkTransCoercion`
1172                                  mkSymCoercion co2b'
1173                              ; return cv2' }
1174
1175              Given {} -> newGivenCoVar ty2a' ty2b' $
1176                          mkSymCoercion co2a'  `mkTransCoercion`
1177                          mkCoVarCoercion cv2  `mkTransCoercion`
1178                          co2b'
1179
1180              Derived {} -> newDerivedId (EqPred ty2a' ty2b')
1181       ; return (singleCCan $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
1182   where
1183     (ty2a, ty2b) = coVarKind cv2          -- cv2 : ty2a ~ ty2b
1184     ty2a' = substTyWith [tv1] [xi1] ty2a
1185     ty2b' = substTyWith [tv1] [xi1] ty2b
1186
1187     co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a  -- ty2a ~ ty2a[xi1/tv1]
1188     co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b  -- ty2b ~ ty2b[xi1/tv1]
1189
1190 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1191 -- First argument inert, second argument workitem. They both represent
1192 -- wanted/given/derived evidence for the *same* predicate so we try here to
1193 -- discharge one directly from the other.
1194 --
1195 -- Precondition: value evidence only (implicit parameters, classes)
1196 --               not coercion
1197 solveOneFromTheOther (iid,ifl) workItem
1198   | ifl `canSolve` wfl
1199   = do { when (isWanted wfl) $ setEvBind wid (EvId iid)
1200            -- Overwrite the binding, if one exists
1201            -- For Givens, which are lambda-bound, nothing to overwrite,
1202        ; dischargeWorkItem }
1203   | wfl `canSolve` ifl
1204   = do { when (isWanted ifl) $ setEvBind iid (EvId wid)
1205        ; mkIRContinue workItem DropInert emptyWorkList }
1206
1207   | otherwise -- One of the two is Derived, we can just throw it away,
1208               -- preferrably the work item.
1209   = if isDerived wfl then dischargeWorkItem
1210     else mkIRContinue workItem DropInert emptyWorkList
1211
1212   where
1213      wfl = cc_flavor workItem
1214      wid = cc_id workItem
1215 \end{code}
1216
1217 Note [Superclasses and recursive dictionaries]
1218 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1219     Overlaps with Note [SUPERCLASS-LOOP 1]
1220                   Note [SUPERCLASS-LOOP 2]
1221                   Note [Recursive instances and superclases]
1222     ToDo: check overlap and delete redundant stuff
1223
1224 Right before adding a given into the inert set, we must
1225 produce some more work, that will bring the superclasses
1226 of the given into scope. The superclass constraints go into
1227 our worklist.
1228
1229 When we simplify a wanted constraint, if we first see a matching
1230 instance, we may produce new wanted work. To (1) avoid doing this work
1231 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1232 this item as given into our inert set WITHOUT adding its superclass constraints,
1233 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
1234 for doing the isGoodRecEv check in an older version of the type checker].
1235
1236 But now we have added partially solved constraints to the worklist which may
1237 interact with other wanteds. Consider the example:
1238
1239 Example 1:
1240
1241     class Eq b => Foo a b        --- 0-th selector
1242     instance Eq a => Foo [a] a   --- fooDFun
1243
1244 and wanted (Foo [t] t). We are first going to see that the instance matches
1245 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
1246        d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3
1247 Our work list is going to contain a new *wanted* goal
1248        d3 :_w Eq t
1249
1250 Ok, so how do we get recursive dictionaries, at all:
1251
1252 Example 2:
1253
1254     data D r = ZeroD | SuccD (r (D r));
1255
1256     instance (Eq (r (D r))) => Eq (D r) where
1257         ZeroD     == ZeroD     = True
1258         (SuccD a) == (SuccD b) = a == b
1259         _         == _         = False;
1260
1261     equalDC :: D [] -> D [] -> Bool;
1262     equalDC = (==);
1263
1264 We need to prove (Eq (D [])). Here's how we go:
1265
1266         d1 :_w Eq (D [])
1267
1268 by instance decl, holds if
1269         d2 :_w Eq [D []]
1270         where   d1 = dfEqD d2
1271
1272 *BUT* we have an inert set which gives us (no superclasses):
1273         d1 :_g Eq (D [])
1274 By the instance declaration of Eq we can show the 'd2' goal if
1275         d3 :_w Eq (D [])
1276         where   d2 = dfEqList d3
1277                 d1 = dfEqD d2
1278 Now, however this wanted can interact with our inert d1 to set:
1279         d3 := d1
1280 and solve the goal. Why was this interaction OK? Because, if we chase the
1281 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1282 are really setting
1283         d3 := dfEqD2 (dfEqList d3)
1284 which is FINE because the use of d3 is protected by the instance function
1285 applications.
1286
1287 So, our strategy is to try to put solved wanted dictionaries into the
1288 inert set along with their superclasses (when this is meaningful,
1289 i.e. when new wanted goals are generated) but solve a wanted dictionary
1290 from a given only in the case where the evidence variable of the
1291 wanted is mentioned in the evidence of the given (recursively through
1292 the evidence binds) in a protected way: more instance function applications
1293 than superclass selectors.
1294
1295 Here are some more examples from GHC's previous type checker
1296
1297
1298 Example 3:
1299 This code arises in the context of "Scrap Your Boilerplate with Class"
1300
1301     class Sat a
1302     class Data ctx a
1303     instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
1304     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
1305
1306     class Data Maybe a => Foo a
1307
1308     instance Foo t => Sat (Maybe t)                             -- dfunSat
1309
1310     instance Data Maybe a => Foo a                              -- dfunFoo1
1311     instance Foo a        => Foo [a]                            -- dfunFoo2
1312     instance                 Foo [Char]                         -- dfunFoo3
1313
1314 Consider generating the superclasses of the instance declaration
1315          instance Foo a => Foo [a]
1316
1317 So our problem is this
1318     d0 :_g Foo t
1319     d1 :_w Data Maybe [t]
1320
1321 We may add the given in the inert set, along with its superclasses
1322 [assuming we don't fail because there is a matching instance, see
1323  tryTopReact, given case ]
1324   Inert:
1325     d0 :_g Foo t
1326   WorkList
1327     d01 :_g Data Maybe t  -- d2 := EvDictSuperClass d0 0
1328     d1 :_w Data Maybe [t]
1329 Then d2 can readily enter the inert, and we also do solving of the wanted
1330   Inert:
1331     d0 :_g Foo t
1332     d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1333   WorkList
1334     d2 :_w Sat (Maybe [t])
1335     d3 :_w Data Maybe t
1336     d01 :_g Data Maybe t
1337 Now, we may simplify d2 more:
1338   Inert:
1339       d0 :_g Foo t
1340       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1341       d1 :_g Data Maybe [t]
1342       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1343   WorkList:
1344       d3 :_w Data Maybe t
1345       d4 :_w Foo [t]
1346       d01 :_g Data Maybe t
1347
1348 Now, we can just solve d3.
1349   Inert
1350       d0 :_g Foo t
1351       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1352       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1353   WorkList
1354       d4 :_w Foo [t]
1355       d01 :_g Data Maybe t
1356 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1357   Inert
1358       d0 :_g Foo t
1359       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1360       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1361       d4 :_g Foo [t]                  d4 := dfunFoo2 d5
1362   WorkList:
1363       d5 :_w Foo t
1364       d6 :_g Data Maybe [t]           d6 := EvDictSuperClass d4 0
1365       d01 :_g Data Maybe t
1366 Now, d5 can be solved! (and its superclass enter scope)
1367   Inert
1368       d0 :_g Foo t
1369       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1370       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1371       d4 :_g Foo [t]                  d4 := dfunFoo2 d5
1372       d5 :_g Foo t                    d5 := dfunFoo1 d7
1373   WorkList:
1374       d7 :_w Data Maybe t
1375       d6 :_g Data Maybe [t]
1376       d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
1377       d01 :_g Data Maybe t
1378
1379 Now, two problems:
1380    [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1381        we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1382        that must not be used (look at case interactInert where both inert and workitem
1383        are givens). So we have several options:
1384        - Drop the workitem always (this will drop d8)
1385               This feels very unsafe -- what if the work item was the "good" one
1386               that should be used later to solve another wanted?
1387        - Don't drop anyone: the inert set may contain multiple givens!
1388               [This is currently implemented]
1389
1390 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1391   [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1392       d7. Now the [isRecDictEv] function in the ineration solver
1393       [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1394       precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1395
1396       So, no interaction happens there. Then we meet d01 and there is no recursion
1397       problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1398
1399 Note [SUPERCLASS-LOOP 1]
1400 ~~~~~~~~~~~~~~~~~~~~~~~~
1401 We have to be very, very careful when generating superclasses, lest we
1402 accidentally build a loop. Here's an example:
1403
1404   class S a
1405
1406   class S a => C a where { opc :: a -> a }
1407   class S b => D b where { opd :: b -> b }
1408
1409   instance C Int where
1410      opc = opd
1411
1412   instance D Int where
1413      opd = opc
1414
1415 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1416 Simplifying, we may well get:
1417         $dfCInt = :C ds1 (opd dd)
1418         dd  = $dfDInt
1419         ds1 = $p1 dd
1420 Notice that we spot that we can extract ds1 from dd.
1421
1422 Alas!  Alack! We can do the same for (instance D Int):
1423
1424         $dfDInt = :D ds2 (opc dc)
1425         dc  = $dfCInt
1426         ds2 = $p1 dc
1427
1428 And now we've defined the superclass in terms of itself.
1429 Two more nasty cases are in
1430         tcrun021
1431         tcrun033
1432
1433 Solution:
1434   - Satisfy the superclass context *all by itself*
1435     (tcSimplifySuperClasses)
1436   - And do so completely; i.e. no left-over constraints
1437     to mix with the constraints arising from method declarations
1438
1439
1440 Note [SUPERCLASS-LOOP 2]
1441 ~~~~~~~~~~~~~~~~~~~~~~~~
1442 We need to be careful when adding "the constaint we are trying to prove".
1443 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1444
1445         class Ord a => C a where
1446         instance Ord [a] => C [a] where ...
1447
1448 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1449 superclasses of C [a] to avails.  But we must not overwrite the binding
1450 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1451 build a loop!
1452
1453 Here's another variant, immortalised in tcrun020
1454         class Monad m => C1 m
1455         class C1 m => C2 m x
1456         instance C2 Maybe Bool
1457 For the instance decl we need to build (C1 Maybe), and it's no good if
1458 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1459 before we search for C1 Maybe.
1460
1461 Here's another example
1462         class Eq b => Foo a b
1463         instance Eq a => Foo [a] a
1464 If we are reducing
1465         (Foo [t] t)
1466
1467 we'll first deduce that it holds (via the instance decl).  We must not
1468 then overwrite the Eq t constraint with a superclass selection!
1469
1470 At first I had a gross hack, whereby I simply did not add superclass constraints
1471 in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
1472 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1473 I found a very obscure program (now tcrun021) in which improvement meant the
1474 simplifier got two bites a the cherry... so something seemed to be an Stop
1475 first time, but reducible next time.
1476
1477 Now we implement the Right Solution, which is to check for loops directly
1478 when adding superclasses.  It's a bit like the occurs check in unification.
1479
1480 Note [Recursive instances and superclases]
1481 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1482 Consider this code, which arises in the context of "Scrap Your
1483 Boilerplate with Class".
1484
1485     class Sat a
1486     class Data ctx a
1487     instance  Sat (ctx Char)             => Data ctx Char
1488     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1489
1490     class Data Maybe a => Foo a
1491
1492     instance Foo t => Sat (Maybe t)
1493
1494     instance Data Maybe a => Foo a
1495     instance Foo a        => Foo [a]
1496     instance                 Foo [Char]
1497
1498 In the instance for Foo [a], when generating evidence for the superclasses
1499 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1500 Using the instance for Data, we therefore need
1501         (Sat (Maybe [a], Data Maybe a)
1502 But we are given (Foo a), and hence its superclass (Data Maybe a).
1503 So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
1504 we need (Foo [a]).  And that is the very dictionary we are bulding
1505 an instance for!  So we must put that in the "givens".  So in this
1506 case we have
1507         Given:  Foo a, Foo [a]
1508         Wanted: Data Maybe [a]
1509
1510 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1511 the givens, which is what 'addGiven' would normally do. Why? Because
1512 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1513 by selecting a superclass from Foo [a], which simply makes a loop.
1514
1515 On the other hand we *must* put the superclasses of (Foo a) in
1516 the givens, as you can see from the derivation described above.
1517
1518 Conclusion: in the very special case of tcSimplifySuperClasses
1519 we have one 'given' (namely the "this" dictionary) whose superclasses
1520 must not be added to 'givens' by addGiven.
1521
1522 There is a complication though.  Suppose there are equalities
1523       instance (Eq a, a~b) => Num (a,b)
1524 Then we normalise the 'givens' wrt the equalities, so the original
1525 given "this" dictionary is cast to one of a different type.  So it's a
1526 bit trickier than before to identify the "special" dictionary whose
1527 superclasses must not be added. See test
1528    indexed-types/should_run/EqInInstance
1529
1530 We need a persistent property of the dictionary to record this
1531 special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
1532 but cool), which is maintained by dictionary normalisation.
1533 Specifically, the InstLocOrigin is
1534              NoScOrigin
1535 then the no-superclass thing kicks in.  WATCH OUT if you fiddle
1536 with InstLocOrigin!
1537
1538 Note [MATCHING-SYNONYMS]
1539 ~~~~~~~~~~~~~~~~~~~~~~~~
1540 When trying to match a dictionary (D tau) to a top-level instance, or a
1541 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1542 we do *not* need to expand type synonyms because the matcher will do that for us.
1543
1544
1545 Note [RHS-FAMILY-SYNONYMS]
1546 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1547 The RHS of a family instance is represented as yet another constructor which is
1548 like a type synonym for the real RHS the programmer declared. Eg:
1549     type instance F (a,a) = [a]
1550 Becomes:
1551     :R32 a = [a]      -- internal type synonym introduced
1552     F (a,a) ~ :R32 a  -- instance
1553
1554 When we react a family instance with a type family equation in the work list
1555 we keep the synonym-using RHS without expansion.
1556
1557
1558 *********************************************************************************
1559 *                                                                               *
1560                        The top-reaction Stage
1561 *                                                                               *
1562 *********************************************************************************
1563
1564 \begin{code}
1565 -- If a work item has any form of interaction with top-level we get this
1566 data TopInteractResult
1567   = NoTopInt         -- No top-level interaction
1568                      -- Equivalent to (SomeTopInt emptyWorkList (ContinueWith work_item))
1569   | SomeTopInt
1570       { tir_new_work  :: WorkList       -- Sub-goals or new work (could be given,
1571                                         --                        for superclasses)
1572       , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1573       }                                 -- NB: in ``given'' (solved) form if the
1574                                         -- original was wanted or given and instance match
1575                                         -- was found, but may also be in wanted form if we
1576                                         -- only reacted with functional dependencies
1577                                         -- arising from top-level instances.
1578
1579 topReactionsStage :: SimplifierStage
1580 topReactionsStage workItem inerts
1581   = do { tir <- tryTopReact workItem
1582        ; case tir of
1583            NoTopInt ->
1584                return $ SR { sr_inerts   = inerts
1585                            , sr_new_work = emptyWorkList
1586                            , sr_stop     = ContinueWith workItem }
1587            SomeTopInt tir_new_work tir_new_inert ->
1588                return $ SR { sr_inerts   = inerts
1589                            , sr_new_work = tir_new_work
1590                            , sr_stop     = tir_new_inert
1591                            }
1592        }
1593
1594 tryTopReact :: WorkItem -> TcS TopInteractResult
1595 tryTopReact workitem
1596   = do {  -- A flag controls the amount of interaction allowed
1597           -- See Note [Simplifying RULE lhs constraints]
1598          ctxt <- getTcSContext
1599        ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1600          then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1601                  ; doTopReact workitem }
1602          else return NoTopInt
1603        }
1604
1605 allowedTopReaction :: Bool -> WorkItem -> Bool
1606 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1607 allowedTopReaction _        _             = True
1608
1609 doTopReact :: WorkItem -> TcS TopInteractResult
1610 -- The work item does not react with the inert set, so try interaction with top-level instances
1611 -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
1612 --     added in the worklist as part of the canonicalisation process.
1613 -- See Note [Adding superclasses] in TcCanonical.
1614
1615 -- Given dictionary
1616 -- See Note [Given constraint that matches an instance declaration]
1617 doTopReact (CDictCan { cc_flavor = Given {} })
1618   = return NoTopInt -- NB: Superclasses already added since it's canonical
1619
1620 -- Derived dictionary: just look for functional dependencies
1621 doTopReact workItem@(CDictCan { cc_flavor = Derived loc
1622                               , cc_class = cls, cc_tyargs = xis })
1623   = do { fd_work <- findClassFunDeps cls xis loc
1624        ; if isEmptyWorkList fd_work then
1625               return NoTopInt
1626          else return $ SomeTopInt { tir_new_work = fd_work
1627                                   , tir_new_inert = ContinueWith workItem } }
1628 -- Wanted dictionary
1629 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1630                               , cc_class = cls, cc_tyargs = xis })
1631   = do { -- See Note [MATCHING-SYNONYMS]
1632        ; lkp_inst_res <- matchClassInst cls xis loc
1633        ; case lkp_inst_res of
1634            NoInstance ->
1635              do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1636                 ; fd_work <- findClassFunDeps cls xis loc
1637                 ; return $ SomeTopInt
1638                               { tir_new_work  = fd_work
1639                               , tir_new_inert = ContinueWith workItem } }
1640
1641            GenInst wtvs ev_term ->  -- Solved
1642                    -- No need to do fundeps stuff here; the instance
1643                    -- matches already so we won't get any more info
1644                    -- from functional dependencies
1645                do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1646                   ; setDictBind dv ev_term
1647                   ; inst_work <- canWanteds wtvs
1648                   ; if null wtvs
1649                     -- Solved in one step and no new wanted work produced.
1650                     -- i.e we directly matched a top-level instance
1651                     -- No point in caching this in 'inert'; hence Stop
1652                     then return $ SomeTopInt { tir_new_work  = emptyWorkList
1653                                              , tir_new_inert = Stop }
1654
1655                     -- Solved and new wanted work produced, you may cache the
1656                     -- (tentatively solved) dictionary as Given! (used to be: Derived)
1657                     else do { let solved = makeSolvedByInst workItem
1658                             ; return $ SomeTopInt
1659                                   { tir_new_work  = inst_work
1660                                   , tir_new_inert = ContinueWith solved } }
1661        }          }
1662
1663 -- Type functions
1664 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1665                       , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1666   = ASSERT (isSynFamilyTyCon tc)   -- No associated data families have reached that far
1667     do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1668        ; case match_res of
1669            MatchInstNo
1670              -> return NoTopInt
1671            MatchInstSingle (rep_tc, rep_tys)
1672              -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1673                          Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1674                             -- Eagerly expand away the type synonym on the
1675                             -- RHS of a type function, so that it never
1676                             -- appears in an error message
1677                             -- See Note [Type synonym families] in TyCon
1678                          coe = mkTyConApp coe_tc rep_tys
1679                    ; cv' <- case fl of
1680                               Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1681                                               ; setWantedCoBind cv $
1682                                                     coe `mkTransCoercion`
1683                                                       mkCoVarCoercion cv'
1684                                               ; return cv' }
1685                               Given {}   -> newGivenCoVar xi rhs_ty $
1686                                             mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1687                               Derived {} -> newDerivedId (EqPred xi rhs_ty)
1688                    ; can_cts <- mkCanonical fl cv'
1689                    ; return $ SomeTopInt can_cts Stop }
1690            _
1691              -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1692        }
1693
1694
1695 -- Any other work item does not react with any top-level equations
1696 doTopReact _workItem = return NoTopInt
1697
1698 ----------------------
1699 findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList
1700 -- Look for a fundep reaction beween the wanted item
1701 -- and a top-level instance declaration
1702 findClassFunDeps cls xis loc
1703  = do { instEnvs <- getInstEnvs
1704       ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1705                                                (ClassP cls xis, pprArisingAt loc)
1706       ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
1707                       -- NB: fundeps generate some wanted equalities, but
1708                       --     we don't use their evidence for anything
1709       ; cts <- mapM mkCanonicalFEV derived_evs
1710       ; return $ unionManyBags cts }
1711 \end{code}
1712
1713
1714 Note [FunDep and implicit parameter reactions]
1715 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1716 Currently, our story of interacting two dictionaries (or a dictionary
1717 and top-level instances) for functional dependencies, and implicit
1718 paramters, is that we simply produce new wanted equalities.  So for example
1719
1720         class D a b | a -> b where ...
1721     Inert:
1722         d1 :g D Int Bool
1723     WorkItem:
1724         d2 :w D Int alpha
1725
1726     We generate the extra work item
1727         cv :w alpha ~ Bool
1728     where 'cv' is currently unused.  However, this new item reacts with d2,
1729     discharging it in favour of a new constraint d2' thus:
1730         d2' :w D Int Bool
1731         d2 := d2' |> D Int cv
1732     Now d2' can be discharged from d1
1733
1734 We could be more aggressive and try to *immediately* solve the dictionary
1735 using those extra equalities. With the same inert set and work item we
1736 might dischard d2 directly:
1737
1738         cv :w alpha ~ Bool
1739         d2 := d1 |> D Int cv
1740
1741 But in general it's a bit painful to figure out the necessary coercion,
1742 so we just take the first approach. Here is a better example. Consider:
1743     class C a b c | a -> b
1744 And:
1745      [Given]  d1 : C T Int Char
1746      [Wanted] d2 : C T beta Int
1747 In this case, it's *not even possible* to solve the wanted immediately.
1748 So we should simply output the functional dependency and add this guy
1749 [but NOT its superclasses] back in the worklist. Even worse:
1750      [Given] d1 : C T Int beta
1751      [Wanted] d2: C T beta Int
1752 Then it is solvable, but its very hard to detect this on the spot.
1753
1754 It's exactly the same with implicit parameters, except that the
1755 "aggressive" approach would be much easier to implement.
1756
1757 Note [When improvement happens]
1758 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1759 We fire an improvement rule when
1760
1761   * Two constraints match (modulo the fundep)
1762       e.g. C t1 t2, C t1 t3    where C a b | a->b
1763     The two match because the first arg is identical
1764
1765   * At least one is not Given.  If they are both given, we don't fire
1766     the reaction because we have no way of constructing evidence for a
1767     new equality nor does it seem right to create a new wanted goal
1768     (because the goal will most likely contain untouchables, which
1769     can't be solved anyway)!
1770
1771 Note that we *do* fire the improvement if one is Given and one is Derived.
1772 The latter can be a superclass of a wanted goal. Example (tcfail138)
1773     class L a b | a -> b
1774     class (G a, L a b) => C a b
1775
1776     instance C a b' => G (Maybe a)
1777     instance C a b  => C (Maybe a) a
1778     instance L (Maybe a) a
1779
1780 When solving the superclasses of the (C (Maybe a) a) instance, we get
1781   Given:  C a b  ... and hance by superclasses, (G a, L a b)
1782   Wanted: G (Maybe a)
1783 Use the instance decl to get
1784   Wanted: C a b'
1785 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1786 and now we need improvement between that derived superclass an the Given (L a b)
1787
1788 Note [Overriding implicit parameters]
1789 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1790 Consider
1791    f :: (?x::a) -> Bool -> a
1792
1793    g v = let ?x::Int = 3
1794          in (f v, let ?x::Bool = True in f v)
1795
1796 This should probably be well typed, with
1797    g :: Bool -> (Int, Bool)
1798
1799 So the inner binding for ?x::Bool *overrides* the outer one.
1800 Hence a work-item Given overrides an inert-item Given.
1801
1802 Note [Given constraint that matches an instance declaration]
1803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1804 What should we do when we discover that one (or more) top-level
1805 instances match a given (or solved) class constraint? We have
1806 two possibilities:
1807
1808   1. Reject the program. The reason is that there may not be a unique
1809      best strategy for the solver. Example, from the OutsideIn(X) paper:
1810        instance P x => Q [x]
1811        instance (x ~ y) => R [x] y
1812
1813        wob :: forall a b. (Q [b], R b a) => a -> Int
1814
1815        g :: forall a. Q [a] => [a] -> Int
1816        g x = wob x
1817
1818        will generate the impliation constraint:
1819             Q [a] => (Q [beta], R beta [a])
1820        If we react (Q [beta]) with its top-level axiom, we end up with a
1821        (P beta), which we have no way of discharging. On the other hand,
1822        if we react R beta [a] with the top-level we get  (beta ~ a), which
1823        is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1824        now solvable by the given Q [a].
1825
1826      However, this option is restrictive, for instance [Example 3] from
1827      Note [Recursive dictionaries] will fail to work.
1828
1829   2. Ignore the problem, hoping that the situations where there exist indeed
1830      such multiple strategies are rare: Indeed the cause of the previous
1831      problem is that (R [x] y) yields the new work (x ~ y) which can be
1832      *spontaneously* solved, not using the givens.
1833
1834 We are choosing option 2 below but we might consider having a flag as well.
1835
1836
1837 Note [New Wanted Superclass Work]
1838 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1839 Even in the case of wanted constraints, we may add some superclasses
1840 as new given work. The reason is:
1841
1842         To allow FD-like improvement for type families. Assume that
1843         we have a class
1844              class C a b | a -> b
1845         and we have to solve the implication constraint:
1846              C a b => C a beta
1847         Then, FD improvement can help us to produce a new wanted (beta ~ b)
1848
1849         We want to have the same effect with the type family encoding of
1850         functional dependencies. Namely, consider:
1851              class (F a ~ b) => C a b
1852         Now suppose that we have:
1853                given: C a b
1854                wanted: C a beta
1855         By interacting the given we will get given (F a ~ b) which is not
1856         enough by itself to make us discharge (C a beta). However, we
1857         may create a new derived equality from the super-class of the
1858         wanted constraint (C a beta), namely derived (F a ~ beta).
1859         Now we may interact this with given (F a ~ b) to get:
1860                   derived :  beta ~ b
1861         But 'beta' is a touchable unification variable, and hence OK to
1862         unify it with 'b', replacing the derived evidence with the identity.
1863
1864         This requires trySpontaneousSolve to solve *derived*
1865         equalities that have a touchable in their RHS, *in addition*
1866         to solving wanted equalities.
1867
1868 We also need to somehow use the superclasses to quantify over a minimal,
1869 constraint see note [Minimize by Superclasses] in TcSimplify.
1870
1871
1872 Finally, here is another example where this is useful.
1873
1874 Example 1:
1875 ----------
1876    class (F a ~ b) => C a b
1877 And we are given the wanteds:
1878       w1 : C a b
1879       w2 : C a c
1880       w3 : b ~ c
1881 We surely do *not* want to quantify over (b ~ c), since if someone provides
1882 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1883 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1884
1885      Step 1: We will get new *given* superclass work,
1886              provisionally to our solving of w1 and w2
1887
1888                g1: F a ~ b, g2 : F a ~ c,
1889                w1 : C a b, w2 : C a c, w3 : b ~ c
1890
1891              The evidence for g1 and g2 is a superclass evidence term:
1892
1893                g1 := sc w1, g2 := sc w2
1894
1895      Step 2: The givens will solve the wanted w3, so that
1896                w3 := sym (sc w1) ; sc w2
1897
1898      Step 3: Now, one may naively assume that then w2 can be solve from w1
1899              after rewriting with the (now solved equality) (b ~ c).
1900
1901              But this rewriting is ruled out by the isGoodRectDict!
1902
1903 Conclusion, we will (correctly) end up with the unsolved goals
1904     (C a b, C a c)
1905
1906 NB: The desugarer needs be more clever to deal with equalities
1907     that participate in recursive dictionary bindings.
1908
1909 \begin{code}
1910 data LookupInstResult
1911   = NoInstance
1912   | GenInst [WantedEvVar] EvTerm
1913
1914 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1915 matchClassInst clas tys loc
1916    = do { let pred = mkClassPred clas tys
1917         ; mb_result <- matchClass clas tys
1918         ; case mb_result of
1919             MatchInstNo   -> return NoInstance
1920             MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1921                                                -- we learn more about the reagent
1922             MatchInstSingle (dfun_id, mb_inst_tys) ->
1923               do { checkWellStagedDFun pred dfun_id loc
1924
1925         -- It's possible that not all the tyvars are in
1926         -- the substitution, tenv. For example:
1927         --      instance C X a => D X where ...
1928         -- (presumably there's a functional dependency in class C)
1929         -- Hence mb_inst_tys :: Either TyVar TcType
1930
1931                  ; tys <- instDFunTypes mb_inst_tys
1932                  ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1933                  ; if null theta then
1934                        return (GenInst [] (EvDFunApp dfun_id tys []))
1935                    else do
1936                      { ev_vars <- instDFunConstraints theta
1937                      ; let wevs = [EvVarX w loc | w <- ev_vars]
1938                      ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }
1939                  }
1940         }
1941 \end{code}