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