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