compiler/typecheck/TcInteract.lhs

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