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