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