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