compiler/typecheck/TcInteract.lhs

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