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