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