3e580133c243581a4921353383b962d7b8856032
[ghc.git] / compiler / typecheck / TcInteract.lhs
1 \begin{code}
2 {-# OPTIONS -fno-warn-tabs #-}
3 -- The above warning supression flag is a temporary kludge.
4 -- While working on this module you are encouraged to remove it and
5 -- detab the module (please do the detabbing in a separate patch). See
6 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
7 -- for details
8
9 module TcInteract ( 
10      solveInteractGiven,  -- Solves [EvVar],GivenLoc
11      solveInteractCts,    -- Solves [Cts]
12   ) where  
13
14 #include "HsVersions.h"
15
16
17 import BasicTypes ()
18 import TcCanonical
19 import VarSet
20 import Type
21 import Unify
22 import FamInstEnv
23 import Coercion( mkAxInstRHS )
24
25 import Id 
26 import Var
27
28 import TcType
29
30 import Class
31 import TyCon
32 import Name
33 import IParam
34
35 import FunDeps
36
37 import TcEvidence
38 import Outputable
39
40 import TcMType ( zonkTcPredType )
41
42 import TcRnTypes
43 import TcErrors
44 import TcSMonad
45 import Maybes( orElse )
46 import Bag
47
48 import Control.Monad ( foldM )
49 import TrieMap
50
51 import VarEnv
52 import qualified Data.Traversable as Traversable
53
54 import Control.Monad( when )
55 import Pair ( pSnd )
56 import UniqFM
57 import FastString ( sLit ) 
58 import DynFlags
59 \end{code}
60 **********************************************************************
61 *                                                                    * 
62 *                      Main Interaction Solver                       *
63 *                                                                    *
64 **********************************************************************
65
66 Note [Basic Simplifier Plan] 
67 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
68
69 1. Pick an element from the WorkList if there exists one with depth 
70    less thanour context-stack depth. 
71
72 2. Run it down the 'stage' pipeline. Stages are: 
73       - canonicalization
74       - inert reactions
75       - spontaneous reactions
76       - top-level intreactions
77    Each stage returns a StopOrContinue and may have sideffected 
78    the inerts or worklist.
79   
80    The threading of the stages is as follows: 
81       - If (Stop) is returned by a stage then we start again from Step 1. 
82       - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to 
83         the next stage in the pipeline. 
84 4. If the element has survived (i.e. ContinueWith x) the last stage 
85    then we add him in the inerts and jump back to Step 1.
86
87 If in Step 1 no such element exists, we have exceeded our context-stack 
88 depth and will simply fail.
89 \begin{code}
90
91 solveInteractCts :: [Ct] -> TcS ()
92 solveInteractCts cts 
93   = do { evvar_cache <- getTcSEvVarCacheMap
94        ; (cts_thinner, new_evvar_cache) <- add_cts_in_cache evvar_cache cts
95        ; traceTcS "solveInteractCts" (vcat [ text "cts_original =" <+> ppr cts, 
96                                              text "cts_thinner  =" <+> ppr cts_thinner
97                                            ])
98        ; setTcSEvVarCacheMap new_evvar_cache 
99        ; updWorkListTcS (appendWorkListCt cts_thinner) >> solveInteract }
100  
101   where 
102     add_cts_in_cache evvar_cache cts
103       = do { ctxt <- getTcSContext
104            ; foldM (solve_or_cache (simplEqsOnly ctxt)) ([],evvar_cache) cts }
105
106     solve_or_cache :: Bool    -- Solve equalities only, not classes etc
107                    -> ([Ct],TypeMap (EvVar,CtFlavor)) 
108                    -> Ct
109                    -> TcS ([Ct],TypeMap (EvVar,CtFlavor))
110     solve_or_cache eqs_only (acc_cts,acc_cache) ct
111       | dont_cache eqs_only (classifyPredType pred_ty)
112       = return (ct:acc_cts,acc_cache) 
113
114       | Just (ev',fl') <- lookupTM pred_ty acc_cache
115       , fl' `canSolve` fl
116       , isWanted fl
117       = do { _ <- setEvBind ev (EvId ev') fl
118            ; return (acc_cts,acc_cache) }
119
120       | otherwise -- If it's a given keep it in the work list, even if it exists in the cache!
121       = return (ct:acc_cts, alterTM pred_ty (\_ -> Just (ev,fl)) acc_cache)
122       where fl = cc_flavor ct
123             ev = cc_id ct
124             pred_ty = ctPred ct
125
126     dont_cache :: Bool -> PredTree -> Bool
127     -- Do not use the cache, not update it, if this is true
128     dont_cache _ (IPPred {}) = True    -- IPPreds have subtle shadowing
129     dont_cache _ (EqPred ty1 ty2)      -- Report Int ~ Bool errors separately
130       | Just tc1 <- tyConAppTyCon_maybe ty1
131       , Just tc2 <- tyConAppTyCon_maybe ty2
132       , tc1 /= tc2
133       = isDecomposableTyCon tc1 && isDecomposableTyCon tc2
134       | otherwise = False
135     dont_cache eqs_only _ = eqs_only
136             -- If we are simplifying equalities only, 
137             -- do not cache non-equalities
138             -- See Note [Simplifying RULE lhs constraints] in TcSimplify
139
140 solveInteractGiven :: GivenLoc -> [EvVar] -> TcS () 
141 solveInteractGiven gloc evs
142   = solveInteractCts (map mk_noncan evs)
143   where mk_noncan ev = CNonCanonical { cc_id = ev
144                                      , cc_flavor = Given gloc GivenOrig 
145                                      , cc_depth = 0 }
146
147 -- The main solver loop implements Note [Basic Simplifier Plan]
148 ---------------------------------------------------------------
149 solveInteract :: TcS ()
150 -- Returns the final InertSet in TcS, WorkList will be eventually empty.
151 solveInteract
152   = {-# SCC "solveInteract" #-}
153     do { dyn_flags <- getDynFlags
154        ; let max_depth = ctxtStkDepth dyn_flags
155              solve_loop
156               = {-# SCC "solve_loop" #-}
157                 do { sel <- selectNextWorkItem max_depth
158                    ; case sel of 
159                       NoWorkRemaining     -- Done, successfuly (modulo frozen)
160                         -> return ()
161                       MaxDepthExceeded ct -- Failure, depth exceeded
162                         -> wrapErrTcS $ solverDepthErrorTcS (cc_depth ct) [ct]
163                       NextWorkItem ct     -- More work, loop around!
164                         -> runSolverPipeline thePipeline ct >> solve_loop }
165        ; solve_loop }
166
167 type WorkItem = Ct
168 type SimplifierStage = WorkItem -> TcS StopOrContinue
169
170 continueWith :: WorkItem -> TcS StopOrContinue
171 continueWith work_item = return (ContinueWith work_item) 
172
173 data SelectWorkItem 
174        = NoWorkRemaining      -- No more work left (effectively we're done!)
175        | MaxDepthExceeded Ct  -- More work left to do but this constraint has exceeded
176                               -- the max subgoal depth and we must stop 
177        | NextWorkItem Ct      -- More work left, here's the next item to look at 
178
179 selectNextWorkItem :: SubGoalDepth -- Max depth allowed
180                    -> TcS SelectWorkItem
181 selectNextWorkItem max_depth
182   = updWorkListTcS_return pick_next
183   where 
184     pick_next :: WorkList -> (SelectWorkItem, WorkList)
185     pick_next wl = case selectWorkItem wl of
186                      (Nothing,_) 
187                          -> (NoWorkRemaining,wl)           -- No more work
188                      (Just ct, new_wl) 
189                          | cc_depth ct > max_depth         -- Depth exceeded
190                          -> (MaxDepthExceeded ct,new_wl)
191                      (Just ct, new_wl) 
192                          -> (NextWorkItem ct, new_wl)      -- New workitem and worklist
193
194 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline 
195                   -> WorkItem                   -- The work item 
196                   -> TcS () 
197 -- Run this item down the pipeline, leaving behind new work and inerts
198 runSolverPipeline pipeline workItem 
199   = do { initial_is <- getTcSInerts 
200        ; traceTcS "Start solver pipeline {" $ 
201                   vcat [ ptext (sLit "work item = ") <+> ppr workItem 
202                        , ptext (sLit "inerts    = ") <+> ppr initial_is]
203
204        ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
205
206        ; final_is <- getTcSInerts
207        ; case final_res of 
208            Stop            -> do { traceTcS "End solver pipeline (discharged) }" 
209                                        (ptext (sLit "inerts    = ") <+> ppr final_is)
210                                  ; return () }
211            ContinueWith ct -> do { traceTcS "End solver pipeline (not discharged) }" $
212                                        vcat [ ptext (sLit "final_item = ") <+> ppr ct
213                                             , ptext (sLit "inerts     = ") <+> ppr final_is]
214                                  ; updInertSetTcS ct }
215        }
216   where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
217         run_pipeline [] res = return res 
218         run_pipeline _ Stop = return Stop 
219         run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
220           = do { traceTcS ("runStage " ++ stg_name ++ " {")
221                           (text "workitem   = " <+> ppr ct) 
222                ; res <- stg ct 
223                ; traceTcS ("end stage " ++ stg_name ++ " }") empty
224                ; run_pipeline stgs res 
225                }
226 \end{code}
227
228 Example 1:
229   Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
230   Reagent: a ~ [b] (given)
231
232 React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
233 React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
234 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []
235
236 Example 2:
237   Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
238   Reagent: a ~w [b]
239
240 React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
241 React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
242 etc.
243
244 Example 3:
245   Inert:  {a ~ Int, F Int ~ b} (given)
246   Reagent: F a ~ b (wanted)
247
248 React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
249 React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing
250
251 \begin{code}
252 thePipeline :: [(String,SimplifierStage)]
253 thePipeline = [ ("canonicalization",        canonicalizationStage)
254               , ("spontaneous solve",       spontaneousSolveStage)
255               , ("interact with inerts",    interactWithInertsStage)
256               , ("top-level reactions",     topReactionsStage) ]
257 \end{code}
258
259
260 \begin{code}
261
262 -- The canonicalization stage, see TcCanonical for details
263 ----------------------------------------------------------
264 canonicalizationStage :: SimplifierStage
265 canonicalizationStage = TcCanonical.canonicalize 
266
267 \end{code}
268
269 *********************************************************************************
270 *                                                                               * 
271                        The spontaneous-solve Stage
272 *                                                                               *
273 *********************************************************************************
274
275 Note [Efficient Orientation] 
276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
277
278 There are two cases where we have to be careful about 
279 orienting equalities to get better efficiency. 
280
281 Case 1: In Rewriting Equalities (function rewriteEqLHS) 
282
283     When rewriting two equalities with the same LHS:
284           (a)  (tv ~ xi1) 
285           (b)  (tv ~ xi2) 
286     We have a choice of producing work (xi1 ~ xi2) (up-to the
287     canonicalization invariants) However, to prevent the inert items
288     from getting kicked out of the inerts first, we prefer to
289     canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
290     ~ xi1) if (a) comes from the inert set.
291     
292     This choice is implemented using the WhichComesFromInert flag. 
293
294 Case 2: Functional Dependencies 
295     Again, we should prefer, if possible, the inert variables on the RHS
296
297 Case 3: IP improvement work
298     We must always rewrite so that the inert type is on the right. 
299
300 \begin{code}
301 spontaneousSolveStage :: SimplifierStage 
302 spontaneousSolveStage workItem
303   = do { mSolve <- trySpontaneousSolve workItem
304        ; spont_solve mSolve } 
305   where spont_solve SPCantSolve 
306           | isCTyEqCan workItem                    -- Unsolved equality
307           = do { kickOutRewritableInerts workItem  -- NB: will add workItem in inerts
308                ; return Stop }
309           | otherwise
310           = continueWith workItem
311         spont_solve (SPSolved workItem')           -- Post: workItem' must be equality
312           = do { bumpStepCountTcS
313                ; traceFireTcS (cc_depth workItem) $
314                  ptext (sLit "Spontaneous") 
315                            <+> parens (ppr (cc_flavor workItem)) <+> ppr workItem
316
317                  -- NB: will add the item in the inerts
318                ; kickOutRewritableInerts workItem'
319                -- .. and Stop
320                ; return Stop }
321
322 kickOutRewritableInerts :: Ct -> TcS () 
323 -- Pre:  ct is a CTyEqCan 
324 -- Post: The TcS monad is left with the thinner non-rewritable inerts; but which
325 --       contains the new constraint.
326 --       The rewritable end up in the worklist
327 kickOutRewritableInerts ct
328   = {-# SCC "kickOutRewritableInerts" #-}
329     do { (wl,ieqs) <- {-# SCC "kick_out_rewritable" #-}
330                       modifyInertTcS (kick_out_rewritable ct)
331
332        -- Step 1: Rewrite as many of the inert_eqs on the spot! 
333        -- NB: if it is a solved constraint just use the cached evidence
334        
335        ; let ct_coercion = getCtCoercion ct 
336
337        ; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
338                      rewriteInertEqsFromInertEq (cc_tyvar ct,ct_coercion, cc_flavor ct) ieqs
339        ; modifyInertTcS (\is -> ((), is { inert_eqs = new_ieqs }))
340
341        -- Step 2: Add the new guy in
342        ; updInertSetTcS ct
343
344        ; traceTcS "Kick out" (ppr ct $$ ppr wl)
345        ; updWorkListTcS (unionWorkList wl) }
346
347 rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution
348                            -> TyVarEnv (Ct, TcCoercion)       -- All inert equalities
349                            -> TcS (TyVarEnv (Ct,TcCoercion)) -- The new inert equalities
350 rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs
351 -- The goal: traverse the inert equalities and rewrite some of them, dropping some others
352 -- back to the worklist. This is delicate, see Note [Delicate equality kick-out]
353  = do { mieqs <- Traversable.mapM do_one ieqs 
354       ; traceTcS "Original inert equalities:" (ppr ieqs)
355       ; let flatten_justs elem venv
356               | Just (act,aco) <- elem = extendVarEnv venv (cc_tyvar act) (act,aco)
357               | otherwise = venv                                     
358             final_ieqs = foldVarEnv flatten_justs emptyVarEnv mieqs
359       ; traceTcS "Remaining inert equalities:" (ppr final_ieqs)
360       ; return final_ieqs }
361
362  where do_one (ct,inert_co)
363          | subst_fl `canRewrite` fl && (subst_tv `elemVarSet` tyVarsOfCt ct) 
364                                       -- Annoyingly inefficient, but we can't simply check 
365                                       -- that isReflCo co because of cached solved ReflCo evidence.
366          = if fl `canRewrite` subst_fl then 
367                -- If also the inert can rewrite the subst it's totally safe 
368                -- to rewrite on the spot
369                do { (ct',inert_co') <- rewrite_on_the_spot (ct,inert_co)
370                   ; return $ Just (ct',inert_co') }
371            else -- We have to throw inert back to worklist for occurs checks 
372               do { updWorkListTcS (extendWorkListEq ct)
373                  ; return Nothing }
374          | otherwise -- Just keep it there
375          = return $ Just (ct,inert_co)
376          where 
377            -- We have new guy         co : tv ~ something
378            -- and old inert  {wanted} cv : tv' ~ rhs[tv]
379            -- We want to rewrite to
380            --                {wanted} cv' : tv' ~ rhs[something] 
381            --                cv = cv' ; rhs[Sym co]
382            --                  
383            rewrite_on_the_spot (ct,_inert_co)
384              = do { let rhs' = pSnd (tcCoercionKind co)
385                   ; delCachedEvVar ev fl
386                   ; evc <- newEqVar fl (mkTyVarTy tv) rhs'
387                   ; let ev'   = evc_the_evvar evc
388                   ; let evco' = mkTcCoVarCo ev' 
389                   ; fl' <- if isNewEvVar evc then
390                                do { case fl of 
391                                       Wanted {} 
392                                         -> setEqBind ev (evco' `mkTcTransCo` mkTcSymCo co) fl
393                                       Given {} 
394                                         -> setEqBind ev' (mkTcCoVarCo ev `mkTcTransCo` co) fl
395                                       Derived {}
396                                         -> return fl }
397                            else
398                                if isWanted fl then 
399                                    setEqBind ev (evco' `mkTcTransCo` mkTcSymCo co) fl
400                                else return fl
401                   ; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' }
402                   ; return (ct',evco') }
403            ev  = cc_id ct
404            fl  = cc_flavor ct
405            tv  = cc_tyvar ct
406            rhs = cc_rhs ct
407            co  = liftTcCoSubstWith [subst_tv] [subst_co] rhs
408
409 kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,TcCoercion)), InertSet)
410 -- Returns ALL equalities, to be dealt with later
411 kick_out_rewritable ct (IS { inert_eqs    = eqmap
412                            , inert_eq_tvs = inscope
413                            , inert_dicts  = dictmap
414                            , inert_ips    = ipmap
415                            , inert_funeqs = funeqmap
416                            , inert_irreds = irreds
417                            , inert_frozen = frozen
418                            } )
419   = ((kicked_out, eqmap), remaining)
420   where
421     kicked_out = WorkList { wl_eqs    = []
422                           , wl_funeqs = bagToList feqs_out
423                           , wl_rest   = bagToList (fro_out `andCts` dicts_out 
424                                           `andCts` ips_out `andCts` irs_out) }
425   
426     remaining = IS { inert_eqs = emptyVarEnv
427                    , inert_eq_tvs = inscope -- keep the same, safe and cheap
428                    , inert_dicts = dicts_in
429                    , inert_ips = ips_in
430                    , inert_funeqs = feqs_in
431                    , inert_irreds = irs_in
432                    , inert_frozen = fro_in 
433                    }
434
435     fl = cc_flavor ct
436     tv = cc_tyvar ct
437                                
438     (ips_out,   ips_in)     = partitionCCanMap rewritable ipmap
439
440     (feqs_out,  feqs_in)    = partitionCtTypeMap rewritable funeqmap
441     (dicts_out, dicts_in)   = partitionCCanMap rewritable dictmap
442
443     (irs_out,   irs_in)   = partitionBag rewritable irreds
444     (fro_out,   fro_in)   = partitionBag rewritable frozen
445
446     rewritable ct = (fl `canRewrite` cc_flavor ct)  &&
447                     (tv `elemVarSet` tyVarsOfCt ct) 
448                     -- NB: tyVarsOfCt will return the type 
449                     --     variables /and the kind variables/ that are 
450                     --     directly visible in the type. Hence we will
451                     --     have exposed all the rewriting we care about
452                     --     to make the most precise kinds visible for 
453                     --     matching classes etc. No need to kick out 
454                     --     constraints that mention type variables whose
455                     --     kinds could contain this variable!
456
457 \end{code}
458
459 Note [Delicate equality kick-out]
460 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
461
462 Delicate:
463 When kicking out rewritable constraints, it would be safe to simply
464 kick out all rewritable equalities, but instead we only kick out those
465 that, when rewritten, may result in occur-check errors. We rewrite the
466 rest on the spot. Example:
467
468           WorkItem =   [S] a ~ b
469           Inerts   = { [W] b ~ [a] }
470 Now at this point the work item cannot be further rewritten by the
471 inert (due to the weaker inert flavor), so we are examining if we can
472 instead rewrite the inert from the workitem. But if we rewrite it on
473 the spot we have to recanonicalize because of the danger of occurs
474 errors.  On the other hand if the inert flavor was just as powerful or
475 more powerful than the workitem flavor, the work-item could not have
476 reached this stage (because it would have already been rewritten by
477 the inert).
478
479 The coclusion is: we kick out the 'dangerous' equalities that may
480 require recanonicalization (occurs checks) and the rest we rewrite
481 unconditionally without further checks, on-the-spot with function
482 rewriteInertEqsFromInertEq.
483
484
485 \begin{code}
486 data SPSolveResult = SPCantSolve
487                    | SPSolved WorkItem 
488
489 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
490 -- SPSolved workItem' gives us a new *given* to go on 
491
492 -- @trySpontaneousSolve wi@ solves equalities where one side is a
493 -- touchable unification variable.
494 --          See Note [Touchables and givens] 
495 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
496 trySpontaneousSolve workItem@(CTyEqCan { cc_id = eqv, cc_flavor = gw
497                                        , cc_tyvar = tv1, cc_rhs = xi, cc_depth = d })
498   | isGivenOrSolved gw
499   = return SPCantSolve
500   | Just tv2 <- tcGetTyVar_maybe xi
501   = do { tch1 <- isTouchableMetaTyVar tv1
502        ; tch2 <- isTouchableMetaTyVar tv2
503        ; case (tch1, tch2) of
504            (True,  True)  -> trySpontaneousEqTwoWay d eqv gw tv1 tv2
505            (True,  False) -> trySpontaneousEqOneWay d eqv gw tv1 xi
506            (False, True)  -> trySpontaneousEqOneWay d eqv gw tv2 (mkTyVarTy tv1)
507            _ -> return SPCantSolve }
508   | otherwise
509   = do { tch1 <- isTouchableMetaTyVar tv1
510        ; if tch1 then trySpontaneousEqOneWay d eqv gw tv1 xi
511                  else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" $
512                            ppr workItem 
513                          ; return SPCantSolve }
514        }
515
516   -- No need for 
517   --      trySpontaneousSolve (CFunEqCan ...) = ...
518   -- See Note [No touchables as FunEq RHS] in TcSMonad
519 trySpontaneousSolve _ = return SPCantSolve
520
521 ----------------
522 trySpontaneousEqOneWay :: SubGoalDepth 
523                        -> EqVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
524 -- tv is a MetaTyVar, not untouchable
525 trySpontaneousEqOneWay d eqv gw tv xi
526   | not (isSigTyVar tv) || isTyVarTy xi
527   = solveWithIdentity d eqv gw tv xi
528   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
529   = return SPCantSolve
530
531 ----------------
532 trySpontaneousEqTwoWay :: SubGoalDepth 
533                        -> EqVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
534 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
535
536 trySpontaneousEqTwoWay d eqv gw tv1 tv2
537   = do { let k1_sub_k2 = k1 `tcIsSubKind` k2
538        ; if k1_sub_k2 && nicer_to_update_tv2
539          then solveWithIdentity d eqv gw tv2 (mkTyVarTy tv1)
540          else solveWithIdentity d eqv gw tv1 (mkTyVarTy tv2) }
541   where
542     k1 = tyVarKind tv1
543     k2 = tyVarKind tv2
544     nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
545 \end{code}
546
547 Note [Kind errors] 
548 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
549 Consider the wanted problem: 
550       alpha ~ (# Int, Int #) 
551 where alpha :: ArgKind and (# Int, Int #) :: (#). We can't spontaneously solve this constraint, 
552 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay' 
553 simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and 
554 get quantified over in inference mode. That's bad because we do know at this point that the 
555 constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
556
557 The same applies in canonicalization code in case of kind errors in the givens. 
558
559 However, when we canonicalize givens we only check for compatibility (@compatKind@). 
560 If there were a kind error in the givens, this means some form of inconsistency or dead code.
561
562 You may think that when we spontaneously solve wanteds we may have to look through the 
563 bindings to determine the right kind of the RHS type. E.g one may be worried that xi is 
564 @alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
565 But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
566 so this situation can't happen. 
567
568 Note [Spontaneous solving and kind compatibility] 
569 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
570 Note that our canonical constraints insist that *all* equalities (tv ~
571 xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
572 the same kinds.  ("compatible" means one is a subKind of the other.)
573
574   - It can't be *equal* kinds, because
575      b) wanted constraints don't necessarily have identical kinds
576                eg   alpha::? ~ Int
577      b) a solved wanted constraint becomes a given
578
579   - SPJ thinks that *given* constraints (tv ~ tau) always have that
580     tau has a sub-kind of tv; and when solving wanted constraints
581     in trySpontaneousEqTwoWay we re-orient to achieve this.
582
583   - Note that the kind invariant is maintained by rewriting.
584     Eg wanted1 rewrites wanted2; if both were compatible kinds before,
585        wanted2 will be afterwards.  Similarly givens.
586
587 Caveat:
588   - Givens from higher-rank, such as: 
589           type family T b :: * -> * -> * 
590           type instance T Bool = (->) 
591
592           f :: forall a. ((T a ~ (->)) => ...) -> a -> ... 
593           flop = f (...) True 
594      Whereas we would be able to apply the type instance, we would not be able to 
595      use the given (T Bool ~ (->)) in the body of 'flop' 
596
597
598 Note [Avoid double unifications] 
599 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
600 The spontaneous solver has to return a given which mentions the unified unification
601 variable *on the left* of the equality. Here is what happens if not: 
602   Original wanted:  (a ~ alpha),  (alpha ~ Int) 
603 We spontaneously solve the first wanted, without changing the order! 
604       given : a ~ alpha      [having unified alpha := a] 
605 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
606 At the end we spontaneously solve that guy, *reunifying*  [alpha := Int] 
607
608 We avoid this problem by orienting the resulting given so that the unification
609 variable is on the left.  [Note that alternatively we could attempt to
610 enforce this at canonicalization]
611
612 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
613 double unifications is the main reason we disallow touchable
614 unification variables as RHS of type family equations: F xis ~ alpha.
615
616 \begin{code}
617 ----------------
618
619 solveWithIdentity :: SubGoalDepth 
620                   -> EqVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
621 -- Solve with the identity coercion 
622 -- Precondition: kind(xi) is a sub-kind of kind(tv)
623 -- Precondition: CtFlavor is Wanted or Derived
624 -- See [New Wanted Superclass Work] to see why solveWithIdentity 
625 --     must work for Derived as well as Wanted
626 -- Returns: workItem where 
627 --        workItem = the new Given constraint
628 solveWithIdentity d eqv wd tv xi 
629   = do { traceTcS "Sneaky unification:" $ 
630                        vcat [text "Coercion variable:  " <+> ppr eqv <+> ppr wd, 
631                              text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
632                              text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
633                              text "Right Kind is     : " <+> ppr (typeKind xi)
634                             ]
635
636        ; setWantedTyBind tv xi
637        ; let refl_xi = mkTcReflCo xi
638
639        ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercion refl_xi) 
640        ; (_,eqv_given) <- newGivenEqVar solved_fl (mkTyVarTy tv) xi refl_xi
641
642        ; when (isWanted wd) $ do { _ <- setEqBind eqv refl_xi wd; return () }
643            -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
644        ; return $ SPSolved (CTyEqCan { cc_id     = eqv_given
645                                      , cc_flavor = solved_fl
646                                      , cc_tyvar  = tv, cc_rhs = xi, cc_depth = d }) }
647 \end{code}
648
649
650 *********************************************************************************
651 *                                                                               * 
652                        The interact-with-inert Stage
653 *                                                                               *
654 *********************************************************************************
655
656 Note [The Solver Invariant]
657 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
658 We always add Givens first.  So you might think that the solver has
659 the invariant
660
661    If the work-item is Given, 
662    then the inert item must Given
663
664 But this isn't quite true.  Suppose we have, 
665     c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
666 After processing the first two, we get
667      c1: [G] beta ~ [alpha], c2 : [W] blah
668 Now, c3 does not interact with the the given c1, so when we spontaneously
669 solve c3, we must re-react it with the inert set.  So we can attempt a 
670 reaction between inert c2 [W] and work-item c3 [G].
671
672 It *is* true that [Solver Invariant]
673    If the work-item is Given, 
674    AND there is a reaction
675    then the inert item must Given
676 or, equivalently,
677    If the work-item is Given, 
678    and the inert item is Wanted/Derived
679    then there is no reaction
680
681 \begin{code}
682 -- Interaction result of  WorkItem <~> AtomicInert
683
684 data InteractResult 
685     = IRWorkItemConsumed { ir_fire :: String } 
686     | IRInertConsumed    { ir_fire :: String } 
687     | IRKeepGoing        { ir_fire :: String }
688
689 irWorkItemConsumed :: String -> TcS InteractResult
690 irWorkItemConsumed str = return (IRWorkItemConsumed str) 
691
692 irInertConsumed :: String -> TcS InteractResult
693 irInertConsumed str = return (IRInertConsumed str) 
694
695 irKeepGoing :: String -> TcS InteractResult 
696 irKeepGoing str = return (IRKeepGoing str) 
697 -- You can't discard neither workitem or inert, but you must keep 
698 -- going. It's possible that new work is waiting in the TcS worklist. 
699
700
701 interactWithInertsStage :: WorkItem -> TcS StopOrContinue 
702 -- Precondition: if the workitem is a CTyEqCan then it will not be able to 
703 -- react with anything at this stage. 
704 interactWithInertsStage wi 
705   = do { ctxt <- getTcSContext
706        ; if simplEqsOnly ctxt then 
707              return (ContinueWith wi)
708          else 
709              extractRelevantInerts wi >>= 
710                foldlBagM interact_next (ContinueWith wi) }
711
712   where interact_next Stop atomic_inert 
713           = updInertSetTcS atomic_inert >> return Stop
714         interact_next (ContinueWith wi) atomic_inert 
715           = do { ir <- doInteractWithInert atomic_inert wi
716                ; let mk_msg rule keep_doc 
717                        = text rule <+> keep_doc
718                          <+> vcat [ ptext (sLit "Inert =") <+> ppr atomic_inert
719                                   , ptext (sLit "Work =")  <+> ppr wi ]
720                ; case ir of 
721                    IRWorkItemConsumed { ir_fire = rule } 
722                        -> do { bumpStepCountTcS
723                              ; traceFireTcS (cc_depth wi) 
724                                             (mk_msg rule (text "WorkItemConsumed"))
725                              ; updInertSetTcS atomic_inert
726                              ; return Stop } 
727                    IRInertConsumed { ir_fire = rule }
728                        -> do { bumpStepCountTcS
729                              ; traceFireTcS (cc_depth atomic_inert) 
730                                             (mk_msg rule (text "InertItemConsumed"))
731                              ; return (ContinueWith wi) }
732                    IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
733                        -> do { updInertSetTcS atomic_inert
734                              ; return (ContinueWith wi) }
735                }
736    
737 --------------------------------------------
738 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
739
740 doInteractWithInert :: Ct -> Ct -> TcS InteractResult
741 -- Identical class constraints.
742 doInteractWithInert
743   inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
744    workItem@(CDictCan { cc_id = _d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
745
746   | cls1 == cls2  
747   = do { let pty1 = mkClassPred cls1 tys1
748              pty2 = mkClassPred cls2 tys2
749              inert_pred_loc     = (pty1, pprFlavorArising fl1)
750              work_item_pred_loc = (pty2, pprFlavorArising fl2)
751
752        ; traceTcS "doInteractWithInert" (vcat [ text "inertItem = " <+> ppr inertItem
753                                               , text "workItem  = " <+> ppr workItem ])
754
755        ; any_fundeps 
756            <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
757               -- NB: We don't create fds for given (and even solved), have not seen a useful
758               -- situation for these and even if we did we'd have to be very careful to only
759               -- create Derived's and not Wanteds. 
760
761               else do { let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
762                       ; wloc  <- get_workitem_wloc fl2 
763                       ; rewriteWithFunDeps fd_eqns tys2 wloc }
764                       -- See Note [Efficient Orientation], [When improvement happens]
765
766        ; case any_fundeps of
767            -- No Functional Dependencies 
768            Nothing             
769                | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
770                | otherwise         -> irKeepGoing "NOP"
771
772            -- Actual Functional Dependencies
773            Just (_rewritten_tys2,_cos2,fd_work)
774               -- Standard thing: create derived fds and keep on going. Importantly we don't
775                -- throw workitem back in the worklist because this can cause loops. See #5236.
776                -> do { emitFDWorkAsDerived fd_work (cc_depth workItem)
777                      ; irKeepGoing "Cls/Cls (new fundeps)" } -- Just keep going without droping the inert 
778        }
779   where get_workitem_wloc (Wanted wl)  = return wl 
780         get_workitem_wloc (Derived wl) = return wl 
781         get_workitem_wloc (Given {})   = pprPanic "Unexpected given workitem!" $
782                                          vcat [ text "Work item =" <+> ppr workItem
783                                               , text "Inert item=" <+> ppr inertItem
784                                               ]
785
786 -- Two pieces of irreducible evidence: if their types are *exactly identical* we can
787 -- rewrite them. We can never improve using this: if we want ty1 :: Constraint and have
788 -- ty2 :: Constraint it clearly does not mean that (ty1 ~ ty2)
789 doInteractWithInert (CIrredEvCan { cc_id = id1, cc_flavor = ifl, cc_ty = ty1 })
790            workItem@(CIrredEvCan { cc_ty = ty2 })
791   | ty1 `eqType` ty2
792   = solveOneFromTheOther "Irred/Irred" (EvId id1,ifl) workItem
793
794 -- Two implicit parameter constraints.  If the names are the same,
795 -- but their types are not, we generate a wanted type equality 
796 -- that equates the type (this is "improvement").  
797 -- However, we don't actually need the coercion evidence,
798 -- so we just generate a fresh coercion variable that isn't used anywhere.
799 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) 
800            workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
801   | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
802   =     -- See Note [Overriding implicit parameters]
803         -- Dump the inert item, override totally with the new one
804         -- Do not require type equality
805         -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
806         --              we must *override* the outer one with the inner one
807     irInertConsumed "IP/IP (override inert)"
808
809   | nm1 == nm2 && ty1 `eqType` ty2 
810   = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem 
811
812   | nm1 == nm2
813   =     -- See Note [When improvement happens]
814     do { let flav = Wanted (combineCtLoc ifl wfl)
815        ; eqv <- newEqVar flav ty2 ty1 -- See Note [Efficient Orientation]
816        ; when (isNewEvVar eqv) $
817               (let ct = CNonCanonical { cc_id     = evc_the_evvar eqv 
818                                       , cc_flavor = flav
819                                       , cc_depth  = cc_depth workItem }
820               in updWorkListTcS (extendWorkListEq ct))
821
822        ; case wfl of
823            Given   {} -> pprPanic "Unexpected given IP" (ppr workItem)
824            Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
825            Wanted  {} ->
826                do { _ <- setEvBind (cc_id workItem) 
827                             (mkEvCast id1 (mkTcSymCo (mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo (evc_the_evvar eqv)]))) wfl
828                   ; irWorkItemConsumed "IP/IP (solved by rewriting)" } }
829
830 doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1
831                                , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
832                     (CFunEqCan { cc_id = eqv2, cc_flavor = fl2, cc_fun = tc2
833                                , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
834   | lhss_match  
835   , Just (GivenSolved {}) <- isGiven_maybe fl1 -- Inert is solved and we can simply ignore it
836                                           -- when workitem is given/solved
837   , isGivenOrSolved fl2
838   = irInertConsumed "FunEq/FunEq"
839   | lhss_match 
840   , Just (GivenSolved {}) <- isGiven_maybe fl2 -- Workitem is solved and we can ignore it when
841                                                -- the inert is given/solved
842   , isGivenOrSolved fl1                 
843   = irWorkItemConsumed "FunEq/FunEq" 
844   | fl1 `canSolve` fl2 && lhss_match
845   = do { rewriteEqLHS LeftComesFromInert  (eqv1,xi1) (eqv2,d2,fl2,xi2) 
846        ; irWorkItemConsumed "FunEq/FunEq" }
847
848   | fl2 `canSolve` fl1 && lhss_match
849   = do { rewriteEqLHS RightComesFromInert (eqv2,xi2) (eqv1,d1,fl1,xi1) 
850        ; irInertConsumed "FunEq/FunEq"}
851   where
852     lhss_match = tc1 == tc2 && eqTypes args1 args2 
853
854
855 doInteractWithInert _ _ = irKeepGoing "NOP"
856
857
858 rewriteEqLHS :: WhichComesFromInert -> (EqVar,Xi) -> (EqVar,SubGoalDepth,CtFlavor,Xi) -> TcS ()
859 -- Used to ineract two equalities of the following form: 
860 -- First Equality:   co1: (XXX ~ xi1)  
861 -- Second Equality:  cv2: (XXX ~ xi2) 
862 -- Where the cv1 `canRewrite` cv2 equality 
863 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1), 
864 --    See Note [Efficient Orientation] for that 
865 rewriteEqLHS LeftComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) 
866   = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
867        ; evc <- newEqVar gw xi2 xi1
868        ; let eqv2' = evc_the_evvar evc
869        ; gw' <- case gw of 
870            Wanted {} 
871                -> setEqBind eqv2 
872                     (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcSymCo (mkTcCoVarCo eqv2')) gw
873            Given {}
874                -> setEqBind eqv2'
875                     (mkTcSymCo (mkTcCoVarCo eqv2) `mkTcTransCo` mkTcCoVarCo eqv1) gw
876            Derived {} 
877                -> return gw
878        ; when (isNewEvVar evc) $ 
879               updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id     = eqv2'
880                                                               , cc_flavor = gw'
881                                                               , cc_depth  = d } ) ) }
882
883 rewriteEqLHS RightComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) 
884   = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
885        ; evc <- newEqVar gw xi1 xi2
886        ; let eqv2' = evc_the_evvar evc
887        ; gw' <- case gw of
888            Wanted {} 
889                -> setEqBind eqv2
890                     (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcCoVarCo eqv2') gw
891            Given {}  
892                -> setEqBind eqv2'
893                     (mkTcSymCo (mkTcCoVarCo eqv1) `mkTcTransCo` mkTcCoVarCo eqv2) gw
894            Derived {} 
895                -> return gw
896
897        ; when (isNewEvVar evc) $
898               updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id = eqv2'
899                                                               , cc_flavor = gw'
900                                                               , cc_depth  = d } ) ) }
901
902 solveOneFromTheOther :: String             -- Info 
903                      -> (EvTerm, CtFlavor) -- Inert 
904                      -> Ct        -- WorkItem 
905                      -> TcS InteractResult
906 -- Preconditions: 
907 -- 1) inert and work item represent evidence for the /same/ predicate
908 -- 2) ip/class/irred evidence (no coercions) only
909 solveOneFromTheOther info (ev_term,ifl) workItem
910   | isDerived wfl
911   = irWorkItemConsumed ("Solved[DW] " ++ info)
912
913   | isDerived ifl -- The inert item is Derived, we can just throw it away, 
914                   -- The workItem is inert wrt earlier inert-set items, 
915                   -- so it's safe to continue on from this point
916   = irInertConsumed ("Solved[DI] " ++ info)
917   
918   | Just (GivenSolved {}) <- isGiven_maybe ifl, isGivenOrSolved wfl
919     -- Same if the inert is a GivenSolved -- just get rid of it
920   = irInertConsumed ("Solved[SI] " ++ info)
921
922   | otherwise
923   = ASSERT( ifl `canSolve` wfl )
924       -- Because of Note [The Solver Invariant], plus Derived dealt with
925     do { when (isWanted wfl) $ do { _ <- setEvBind wid ev_term wfl; return () }
926            -- Overwrite the binding, if one exists
927            -- If both are Given, we already have evidence; no need to duplicate
928        ; irWorkItemConsumed ("Solved " ++ info) }
929   where 
930      wfl = cc_flavor workItem
931      wid = cc_id workItem
932
933 \end{code}
934
935 Note [Superclasses and recursive dictionaries]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937     Overlaps with Note [SUPERCLASS-LOOP 1]
938                   Note [SUPERCLASS-LOOP 2]
939                   Note [Recursive instances and superclases]
940     ToDo: check overlap and delete redundant stuff
941
942 Right before adding a given into the inert set, we must
943 produce some more work, that will bring the superclasses 
944 of the given into scope. The superclass constraints go into 
945 our worklist. 
946
947 When we simplify a wanted constraint, if we first see a matching
948 instance, we may produce new wanted work. To (1) avoid doing this work 
949 twice in the future and (2) to handle recursive dictionaries we may ``cache'' 
950 this item as given into our inert set WITHOUT adding its superclass constraints, 
951 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
952 for doing the isGoodRecEv check in an older version of the type checker]. 
953
954 But now we have added partially solved constraints to the worklist which may 
955 interact with other wanteds. Consider the example: 
956
957 Example 1: 
958
959     class Eq b => Foo a b        --- 0-th selector
960     instance Eq a => Foo [a] a   --- fooDFun
961
962 and wanted (Foo [t] t). We are first going to see that the instance matches 
963 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
964        d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3 
965 Our work list is going to contain a new *wanted* goal
966        d3 :_w Eq t 
967
968 Ok, so how do we get recursive dictionaries, at all: 
969
970 Example 2:
971
972     data D r = ZeroD | SuccD (r (D r));
973     
974     instance (Eq (r (D r))) => Eq (D r) where
975         ZeroD     == ZeroD     = True
976         (SuccD a) == (SuccD b) = a == b
977         _         == _         = False;
978     
979     equalDC :: D [] -> D [] -> Bool;
980     equalDC = (==);
981
982 We need to prove (Eq (D [])). Here's how we go:
983
984         d1 :_w Eq (D [])
985
986 by instance decl, holds if
987         d2 :_w Eq [D []]
988         where   d1 = dfEqD d2
989
990 *BUT* we have an inert set which gives us (no superclasses): 
991         d1 :_g Eq (D []) 
992 By the instance declaration of Eq we can show the 'd2' goal if 
993         d3 :_w Eq (D [])
994         where   d2 = dfEqList d3
995                 d1 = dfEqD d2
996 Now, however this wanted can interact with our inert d1 to set: 
997         d3 := d1 
998 and solve the goal. Why was this interaction OK? Because, if we chase the 
999 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we 
1000 are really setting
1001         d3 := dfEqD2 (dfEqList d3) 
1002 which is FINE because the use of d3 is protected by the instance function 
1003 applications. 
1004
1005 So, our strategy is to try to put solved wanted dictionaries into the
1006 inert set along with their superclasses (when this is meaningful,
1007 i.e. when new wanted goals are generated) but solve a wanted dictionary
1008 from a given only in the case where the evidence variable of the
1009 wanted is mentioned in the evidence of the given (recursively through
1010 the evidence binds) in a protected way: more instance function applications 
1011 than superclass selectors.
1012
1013 Here are some more examples from GHC's previous type checker
1014
1015
1016 Example 3: 
1017 This code arises in the context of "Scrap Your Boilerplate with Class"
1018
1019     class Sat a
1020     class Data ctx a
1021     instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
1022     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
1023
1024     class Data Maybe a => Foo a    
1025
1026     instance Foo t => Sat (Maybe t)                             -- dfunSat
1027
1028     instance Data Maybe a => Foo a                              -- dfunFoo1
1029     instance Foo a        => Foo [a]                            -- dfunFoo2
1030     instance                 Foo [Char]                         -- dfunFoo3
1031
1032 Consider generating the superclasses of the instance declaration
1033          instance Foo a => Foo [a]
1034
1035 So our problem is this
1036     d0 :_g Foo t
1037     d1 :_w Data Maybe [t] 
1038
1039 We may add the given in the inert set, along with its superclasses
1040 [assuming we don't fail because there is a matching instance, see 
1041  tryTopReact, given case ]
1042   Inert:
1043     d0 :_g Foo t 
1044   WorkList 
1045     d01 :_g Data Maybe t  -- d2 := EvDictSuperClass d0 0 
1046     d1 :_w Data Maybe [t] 
1047 Then d2 can readily enter the inert, and we also do solving of the wanted
1048   Inert: 
1049     d0 :_g Foo t 
1050     d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1051   WorkList
1052     d2 :_w Sat (Maybe [t])          
1053     d3 :_w Data Maybe t
1054     d01 :_g Data Maybe t 
1055 Now, we may simplify d2 more: 
1056   Inert:
1057       d0 :_g Foo t 
1058       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1059       d1 :_g Data Maybe [t] 
1060       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
1061   WorkList: 
1062       d3 :_w Data Maybe t 
1063       d4 :_w Foo [t] 
1064       d01 :_g Data Maybe t 
1065
1066 Now, we can just solve d3.
1067   Inert
1068       d0 :_g Foo t 
1069       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1070       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
1071   WorkList
1072       d4 :_w Foo [t] 
1073       d01 :_g Data Maybe t 
1074 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1075   Inert
1076       d0 :_g Foo t 
1077       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1078       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
1079       d4 :_g Foo [t]                  d4 := dfunFoo2 d5 
1080   WorkList:
1081       d5 :_w Foo t 
1082       d6 :_g Data Maybe [t]           d6 := EvDictSuperClass d4 0
1083       d01 :_g Data Maybe t 
1084 Now, d5 can be solved! (and its superclass enter scope) 
1085   Inert
1086       d0 :_g Foo t 
1087       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1088       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
1089       d4 :_g Foo [t]                  d4 := dfunFoo2 d5 
1090       d5 :_g Foo t                    d5 := dfunFoo1 d7
1091   WorkList:
1092       d7 :_w Data Maybe t
1093       d6 :_g Data Maybe [t]
1094       d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
1095       d01 :_g Data Maybe t 
1096
1097 Now, two problems: 
1098    [1] Suppose we pick d8 and we react him with d01. Which of the two givens should 
1099        we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence 
1100        that must not be used (look at case interactInert where both inert and workitem
1101        are givens). So we have several options: 
1102        - Drop the workitem always (this will drop d8)
1103               This feels very unsafe -- what if the work item was the "good" one
1104               that should be used later to solve another wanted?
1105        - Don't drop anyone: the inert set may contain multiple givens! 
1106               [This is currently implemented] 
1107
1108 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2: 
1109   [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1110       d7. Now the [isRecDictEv] function in the ineration solver 
1111       [case inert-given workitem-wanted] will prevent us from interacting d7 := d8 
1112       precisely because chasing the evidence of d8 leads us to an unguarded use of d7. 
1113
1114       So, no interaction happens there. Then we meet d01 and there is no recursion 
1115       problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01! 
1116              
1117 Note [SUPERCLASS-LOOP 1]
1118 ~~~~~~~~~~~~~~~~~~~~~~~~
1119 We have to be very, very careful when generating superclasses, lest we
1120 accidentally build a loop. Here's an example:
1121
1122   class S a
1123
1124   class S a => C a where { opc :: a -> a }
1125   class S b => D b where { opd :: b -> b }
1126   
1127   instance C Int where
1128      opc = opd
1129   
1130   instance D Int where
1131      opd = opc
1132
1133 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1134 Simplifying, we may well get:
1135         $dfCInt = :C ds1 (opd dd)
1136         dd  = $dfDInt
1137         ds1 = $p1 dd
1138 Notice that we spot that we can extract ds1 from dd.  
1139
1140 Alas!  Alack! We can do the same for (instance D Int):
1141
1142         $dfDInt = :D ds2 (opc dc)
1143         dc  = $dfCInt
1144         ds2 = $p1 dc
1145
1146 And now we've defined the superclass in terms of itself.
1147 Two more nasty cases are in
1148         tcrun021
1149         tcrun033
1150
1151 Solution: 
1152   - Satisfy the superclass context *all by itself* 
1153     (tcSimplifySuperClasses)
1154   - And do so completely; i.e. no left-over constraints
1155     to mix with the constraints arising from method declarations
1156
1157
1158 Note [SUPERCLASS-LOOP 2]
1159 ~~~~~~~~~~~~~~~~~~~~~~~~
1160 We need to be careful when adding "the constaint we are trying to prove".
1161 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1162
1163         class Ord a => C a where
1164         instance Ord [a] => C [a] where ...
1165
1166 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1167 superclasses of C [a] to avails.  But we must not overwrite the binding
1168 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1169 build a loop! 
1170
1171 Here's another variant, immortalised in tcrun020
1172         class Monad m => C1 m
1173         class C1 m => C2 m x
1174         instance C2 Maybe Bool
1175 For the instance decl we need to build (C1 Maybe), and it's no good if
1176 we run around and add (C2 Maybe Bool) and its superclasses to the avails 
1177 before we search for C1 Maybe.
1178
1179 Here's another example 
1180         class Eq b => Foo a b
1181         instance Eq a => Foo [a] a
1182 If we are reducing
1183         (Foo [t] t)
1184
1185 we'll first deduce that it holds (via the instance decl).  We must not
1186 then overwrite the Eq t constraint with a superclass selection!
1187
1188 At first I had a gross hack, whereby I simply did not add superclass constraints
1189 in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
1190 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1191 I found a very obscure program (now tcrun021) in which improvement meant the
1192 simplifier got two bites a the cherry... so something seemed to be an Stop
1193 first time, but reducible next time.
1194
1195 Now we implement the Right Solution, which is to check for loops directly 
1196 when adding superclasses.  It's a bit like the occurs check in unification.
1197
1198 Note [Recursive instances and superclases]
1199 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1200 Consider this code, which arises in the context of "Scrap Your 
1201 Boilerplate with Class".  
1202
1203     class Sat a
1204     class Data ctx a
1205     instance  Sat (ctx Char)             => Data ctx Char
1206     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1207
1208     class Data Maybe a => Foo a
1209
1210     instance Foo t => Sat (Maybe t)
1211
1212     instance Data Maybe a => Foo a
1213     instance Foo a        => Foo [a]
1214     instance                 Foo [Char]
1215
1216 In the instance for Foo [a], when generating evidence for the superclasses
1217 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1218 Using the instance for Data, we therefore need
1219         (Sat (Maybe [a], Data Maybe a)
1220 But we are given (Foo a), and hence its superclass (Data Maybe a).
1221 So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
1222 we need (Foo [a]).  And that is the very dictionary we are bulding
1223 an instance for!  So we must put that in the "givens".  So in this
1224 case we have
1225         Given:  Foo a, Foo [a]
1226         Wanted: Data Maybe [a]
1227
1228 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1229 the givens, which is what 'addGiven' would normally do. Why? Because
1230 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted 
1231 by selecting a superclass from Foo [a], which simply makes a loop.
1232
1233 On the other hand we *must* put the superclasses of (Foo a) in
1234 the givens, as you can see from the derivation described above.
1235
1236 Conclusion: in the very special case of tcSimplifySuperClasses
1237 we have one 'given' (namely the "this" dictionary) whose superclasses
1238 must not be added to 'givens' by addGiven.  
1239
1240 There is a complication though.  Suppose there are equalities
1241       instance (Eq a, a~b) => Num (a,b)
1242 Then we normalise the 'givens' wrt the equalities, so the original
1243 given "this" dictionary is cast to one of a different type.  So it's a
1244 bit trickier than before to identify the "special" dictionary whose
1245 superclasses must not be added. See test
1246    indexed-types/should_run/EqInInstance
1247
1248 We need a persistent property of the dictionary to record this
1249 special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
1250 but cool), which is maintained by dictionary normalisation.
1251 Specifically, the InstLocOrigin is
1252              NoScOrigin
1253 then the no-superclass thing kicks in.  WATCH OUT if you fiddle
1254 with InstLocOrigin!
1255
1256 Note [MATCHING-SYNONYMS]
1257 ~~~~~~~~~~~~~~~~~~~~~~~~
1258 When trying to match a dictionary (D tau) to a top-level instance, or a 
1259 type family equation (F taus_1 ~ tau_2) to a top-level family instance, 
1260 we do *not* need to expand type synonyms because the matcher will do that for us.
1261
1262
1263 Note [RHS-FAMILY-SYNONYMS] 
1264 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1265 The RHS of a family instance is represented as yet another constructor which is 
1266 like a type synonym for the real RHS the programmer declared. Eg: 
1267     type instance F (a,a) = [a] 
1268 Becomes: 
1269     :R32 a = [a]      -- internal type synonym introduced
1270     F (a,a) ~ :R32 a  -- instance 
1271
1272 When we react a family instance with a type family equation in the work list 
1273 we keep the synonym-using RHS without expansion. 
1274
1275
1276 %************************************************************************
1277 %*                                                                      *
1278 %*          Functional dependencies, instantiation of equations
1279 %*                                                                      *
1280 %************************************************************************
1281
1282 When we spot an equality arising from a functional dependency,
1283 we now use that equality (a "wanted") to rewrite the work-item
1284 constraint right away.  This avoids two dangers
1285
1286  Danger 1: If we send the original constraint on down the pipeline
1287            it may react with an instance declaration, and in delicate
1288            situations (when a Given overlaps with an instance) that
1289            may produce new insoluble goals: see Trac #4952
1290
1291  Danger 2: If we don't rewrite the constraint, it may re-react
1292            with the same thing later, and produce the same equality
1293            again --> termination worries.
1294
1295 To achieve this required some refactoring of FunDeps.lhs (nicer
1296 now!).  
1297
1298 \begin{code}
1299 rewriteWithFunDeps :: [Equation]
1300                    -> [Xi] 
1301                    -> WantedLoc 
1302                    -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) 
1303                                            -- Not quite a WantedEvVar unfortunately
1304                                            -- Because our intention could be to make 
1305                                            -- it derived at the end of the day
1306 -- NB: The flavor of the returned EvVars will be decided by the caller
1307 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1308 rewriteWithFunDeps eqn_pred_locs xis wloc
1309  = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
1310       ; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
1311             fd_ev_pos = concat fd_ev_poss
1312             (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
1313       ; if null fd_ev_pos then return Nothing
1314         else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
1315
1316 instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
1317 -- Post: Returns the position index as well as the corresponding FunDep equality
1318 instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
1319                         , fd_pred1 = d1, fd_pred2 = d2 })
1320   = do { let tvs = varSetElems qtvs
1321        ; tvs' <- mapM instFlexiTcS tvs  -- IA0_TODO: we might need to do kind substitution
1322        ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
1323        ; foldM (do_one subst) [] eqs }
1324   where 
1325     do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
1326        = let sty1 = Type.substTy subst ty1 
1327              sty2 = Type.substTy subst ty2 
1328          in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
1329             else do { eqv <- newEqVar (Derived wl) sty1 sty2 -- Create derived or cached by deriveds
1330                     ; let wl' = push_ctx wl 
1331                     ; if isNewEvVar eqv then 
1332                           return $ (i,(evc_the_evvar eqv,wl')):ievs 
1333                       else -- We are eventually going to emit FD work back in the work list so 
1334                            -- it is important that we only return the /freshly created/ and not 
1335                            -- some existing equality!
1336                           return ievs }
1337
1338     push_ctx :: WantedLoc -> WantedLoc 
1339     push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1340
1341 mkEqnMsg :: (TcPredType, SDoc) 
1342          -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
1343 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1344   = do  { zpred1 <- zonkTcPredType pred1
1345         ; zpred2 <- zonkTcPredType pred2
1346         ; let { tpred1 = tidyType tidy_env zpred1
1347               ; tpred2 = tidyType tidy_env zpred2 }
1348         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1349                           nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
1350                           nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1351         ; return (tidy_env, msg) }
1352
1353 rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
1354                   -> [Type]                    -- A sequence of types: tys
1355                   -> [(Type, TcCoercion)]      -- Returns: [(ty', co : ty' ~ ty)]
1356 rewriteDictParams param_eqs tys
1357   = zipWith do_one tys [0..]
1358   where
1359     do_one :: Type -> Int -> (Type, TcCoercion)
1360     do_one ty n = case lookup n param_eqs of
1361                     Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
1362                     Nothing  -> (ty,             mkTcReflCo ty) -- Identity
1363
1364     get_fst_ty (wev,_wloc) 
1365       | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
1366       = ty1
1367       | otherwise 
1368       = panic "rewriteDictParams: non equality fundep!?"
1369
1370         
1371 emitFDWorkAsDerived :: [(EvVar,WantedLoc)] 
1372                     -> SubGoalDepth -> TcS () 
1373 emitFDWorkAsDerived evlocs d 
1374   = updWorkListTcS $ appendWorkListEqs fd_cts
1375   where fd_cts = map mk_fd_ct evlocs 
1376         mk_fd_ct (v,wl) = CNonCanonical { cc_id = v
1377                                         , cc_flavor = Derived wl 
1378                                         , cc_depth = d }
1379
1380
1381 \end{code}
1382
1383
1384
1385
1386 *********************************************************************************
1387 *                                                                               * 
1388                        The top-reaction Stage
1389 *                                                                               *
1390 *********************************************************************************
1391
1392 \begin{code}
1393
1394 topReactionsStage :: SimplifierStage 
1395 topReactionsStage workItem 
1396  = tryTopReact workItem 
1397    
1398
1399 tryTopReact :: WorkItem -> TcS StopOrContinue
1400 tryTopReact wi 
1401  = do { inerts <- getTcSInerts
1402       ; ctxt   <- getTcSContext
1403       ; if simplEqsOnly ctxt then return (ContinueWith wi) -- or Stop?
1404         else 
1405             do { tir <- doTopReact inerts wi
1406                ; case tir of 
1407                    NoTopInt 
1408                        -> return (ContinueWith wi)
1409                    SomeTopInt rule what_next 
1410                        -> do { bumpStepCountTcS 
1411                              ; traceFireTcS (cc_depth wi) $
1412                                ptext (sLit "Top react:") <+> text rule
1413                              ; return what_next }
1414                } }
1415
1416 data TopInteractResult 
1417  = NoTopInt
1418  | SomeTopInt { tir_rule :: String, tir_new_item :: StopOrContinue }
1419
1420
1421 doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1422
1423 -- The work item does not react with the inert set, so try interaction
1424 -- with top-level instances 
1425 -- NB: The place to add superclasses in *not*
1426 -- in doTopReact stage. Instead superclasses are added in the worklist
1427 -- as part of the canonicalisation process. See Note [Adding superclasses].
1428
1429
1430 -- Given dictionary
1431 -- See Note [Given constraint that matches an instance declaration]
1432 doTopReact _inerts (CDictCan { cc_flavor = Given {} })
1433   = return NoTopInt -- NB: Superclasses already added since it's canonical
1434
1435 -- Derived dictionary: just look for functional dependencies
1436 doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
1437                                       , cc_class = cls, cc_tyargs = xis })
1438   = do { instEnvs <- getInstEnvs
1439        ; let fd_eqns = improveFromInstEnv instEnvs
1440                            (mkClassPred cls xis, pprArisingAt loc)
1441        ; m <- rewriteWithFunDeps fd_eqns xis loc
1442        ; case m of
1443            Nothing -> return NoTopInt
1444            Just (xis',_,fd_work) ->
1445                let workItem' = workItem { cc_tyargs = xis' }
1446                    -- Deriveds are not supposed to have identity (cc_id is unused!)
1447                in do { emitFDWorkAsDerived fd_work (cc_depth workItem)
1448                      ; return $ 
1449                        SomeTopInt { tir_rule  = "Derived Cls fundeps" 
1450                                   , tir_new_item = ContinueWith workItem' } }
1451        }
1452
1453 -- Wanted dictionary
1454 doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
1455                                      , cc_id    = dict_id
1456                                      , cc_class = cls, cc_tyargs = xis
1457                                      , cc_depth = depth })
1458   -- See Note [MATCHING-SYNONYMS]
1459   = do { traceTcS "doTopReact" (ppr workItem)
1460        ; instEnvs <- getInstEnvs
1461        ; let fd_eqns = improveFromInstEnv instEnvs 
1462                             (mkClassPred cls xis, pprArisingAt loc)
1463
1464        ; any_fundeps <- rewriteWithFunDeps fd_eqns xis loc
1465        ; case any_fundeps of
1466            -- No Functional Dependencies
1467            Nothing ->
1468                do { lkup_inst_res  <- matchClassInst inerts cls xis loc
1469                   ; case lkup_inst_res of
1470                       GenInst wtvs ev_term
1471                           -> doSolveFromInstance wtvs ev_term 
1472                       NoInstance
1473                           -> return NoTopInt
1474                   }
1475            -- Actual Functional Dependencies
1476            Just (_xis',_cos,fd_work) ->
1477                do { emitFDWorkAsDerived fd_work (cc_depth workItem)
1478                   ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
1479                                       , tir_new_item = ContinueWith workItem } } }
1480
1481    where doSolveFromInstance :: [EvVar] -> EvTerm -> TcS TopInteractResult
1482          -- Precondition: evidence term matches the predicate of cc_id of workItem
1483          doSolveFromInstance evs ev_term 
1484             | null evs
1485             = do { traceTcS "doTopReact/found nullary instance for" (ppr dict_id)
1486                  ; _ <- setEvBind dict_id ev_term fl
1487                  ; return $ 
1488                    SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" 
1489                               , tir_new_item = Stop } } -- Don't put him in the inerts
1490             | otherwise 
1491             = do { traceTcS "doTopReact/found non-nullary instance for" (ppr dict_id)
1492                  ; _ <- setEvBind dict_id ev_term fl
1493                         -- Solved and new wanted work produced, you may cache the 
1494                         -- (tentatively solved) dictionary as Solved given.
1495 --                 ; let _solved = workItem { cc_flavor = solved_fl }
1496 --                       solved_fl = mkSolvedFlavor fl UnkSkol
1497                  ; let mk_new_wanted ev
1498                            = CNonCanonical { cc_id = ev, cc_flavor = fl
1499                                            , cc_depth  = depth + 1 }
1500                  ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
1501                  ; return $
1502                    SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
1503                               , tir_new_item = Stop }
1504                  }
1505 --                              , tir_new_item = ContinueWith solved } } -- Cache in inerts the Solved item
1506
1507 -- Type functions
1508 doTopReact _inerts (CFunEqCan { cc_flavor = fl })
1509   | Just (GivenSolved {}) <- isGiven_maybe fl
1510   = return NoTopInt -- If Solved, no more interactions should happen
1511
1512 -- Otherwise, it's a Given, Derived, or Wanted
1513 doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
1514                                        , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1515   = ASSERT (isSynFamilyTyCon tc)   -- No associated data families have reached that far 
1516     do { match_res <- matchFam tc args   -- See Note [MATCHING-SYNONYMS]
1517        ; case match_res of
1518            Nothing -> return NoTopInt 
1519            Just (famInst, rep_tys)
1520              -> do { let coe_ax = famInstAxiom famInst
1521                          rhs_ty = mkAxInstRHS coe_ax rep_tys
1522                          coe    = mkTcAxInstCo coe_ax rep_tys 
1523                    ; case fl of
1524                        Wanted {} -> do { evc <- newEqVar fl rhs_ty xi -- Wanted version
1525                                        ; let eqv' = evc_the_evvar evc
1526                                        ; let coercion = coe `mkTcTransCo` mkTcCoVarCo eqv'
1527                                        ; _ <- setEqBind eqv coercion fl
1528                                        ; when (isNewEvVar evc) $ 
1529                                             (let ct = CNonCanonical { cc_id = eqv'
1530                                                                     , cc_flavor = fl 
1531                                                                     , cc_depth = cc_depth workItem + 1} 
1532                                              in updWorkListTcS (extendWorkListEq ct))
1533
1534                                        ; let _solved   = workItem { cc_flavor = solved_fl }
1535                                              solved_fl = mkSolvedFlavor fl UnkSkol (EvCoercion coercion)
1536
1537                                        ; updateFlatCache eqv solved_fl tc args xi WhenSolved
1538
1539                                        ; return $ 
1540                                          SomeTopInt { tir_rule = "Fun/Top (solved, more work)"
1541                                                     , tir_new_item = Stop } }
1542                                                   --  , tir_new_item = ContinueWith solved } }
1543                                                      -- Cache in inerts the Solved item
1544
1545                        Given {} -> do { (fl',eqv') <- newGivenEqVar fl xi rhs_ty $ 
1546                                                          mkTcSymCo (mkTcCoVarCo eqv) `mkTcTransCo` coe
1547                                       ; let ct = CNonCanonical { cc_id = eqv'
1548                                                                , cc_flavor = fl'
1549                                                                , cc_depth = cc_depth workItem + 1}  
1550                                       ; updWorkListTcS (extendWorkListEq ct) 
1551                                       ; return $ 
1552                                         SomeTopInt { tir_rule = "Fun/Top (given)"
1553                                                    , tir_new_item = ContinueWith workItem } }
1554                        Derived {} -> do { evc <- newEvVar fl (mkEqPred (xi, rhs_ty))
1555                                         ; let eqv' = evc_the_evvar evc
1556                                         ; when (isNewEvVar evc) $ 
1557                                             (let ct = CNonCanonical { cc_id  = eqv'
1558                                                                  , cc_flavor = fl
1559                                                                  , cc_depth  = cc_depth workItem + 1 } 
1560                                              in updWorkListTcS (extendWorkListEq ct)) 
1561                                         ; return $ 
1562                                           SomeTopInt { tir_rule = "Fun/Top (derived)"
1563                                                      , tir_new_item = Stop } }
1564                    }
1565        }
1566
1567
1568 -- Any other work item does not react with any top-level equations
1569 doTopReact _inerts _workItem = return NoTopInt 
1570 \end{code}
1571
1572
1573 Note [FunDep and implicit parameter reactions] 
1574 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1575 Currently, our story of interacting two dictionaries (or a dictionary
1576 and top-level instances) for functional dependencies, and implicit
1577 paramters, is that we simply produce new wanted equalities.  So for example
1578
1579         class D a b | a -> b where ... 
1580     Inert: 
1581         d1 :g D Int Bool
1582     WorkItem: 
1583         d2 :w D Int alpha
1584
1585     We generate the extra work item
1586         cv :w alpha ~ Bool
1587     where 'cv' is currently unused.  However, this new item reacts with d2,
1588     discharging it in favour of a new constraint d2' thus:
1589         d2' :w D Int Bool
1590         d2 := d2' |> D Int cv
1591     Now d2' can be discharged from d1
1592
1593 We could be more aggressive and try to *immediately* solve the dictionary 
1594 using those extra equalities. With the same inert set and work item we
1595 might dischard d2 directly:
1596
1597         cv :w alpha ~ Bool
1598         d2 := d1 |> D Int cv
1599
1600 But in general it's a bit painful to figure out the necessary coercion,
1601 so we just take the first approach. Here is a better example. Consider:
1602     class C a b c | a -> b 
1603 And: 
1604      [Given]  d1 : C T Int Char 
1605      [Wanted] d2 : C T beta Int 
1606 In this case, it's *not even possible* to solve the wanted immediately. 
1607 So we should simply output the functional dependency and add this guy
1608 [but NOT its superclasses] back in the worklist. Even worse: 
1609      [Given] d1 : C T Int beta 
1610      [Wanted] d2: C T beta Int 
1611 Then it is solvable, but its very hard to detect this on the spot. 
1612
1613 It's exactly the same with implicit parameters, except that the
1614 "aggressive" approach would be much easier to implement.
1615
1616
1617 Note [When improvement happens]
1618 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1619 We fire an improvement rule when
1620
1621   * Two constraints match (modulo the fundep)
1622       e.g. C t1 t2, C t1 t3    where C a b | a->b
1623     The two match because the first arg is identical
1624
1625   * At least one is not Given.  If they are both given, we don't fire
1626     the reaction because we have no way of constructing evidence for a
1627     new equality nor does it seem right to create a new wanted goal
1628     (because the goal will most likely contain untouchables, which
1629     can't be solved anyway)!
1630    
1631 Note that we *do* fire the improvement if one is Given and one is Derived.
1632 The latter can be a superclass of a wanted goal. Example (tcfail138)
1633     class L a b | a -> b
1634     class (G a, L a b) => C a b
1635
1636     instance C a b' => G (Maybe a)
1637     instance C a b  => C (Maybe a) a
1638     instance L (Maybe a) a
1639
1640 When solving the superclasses of the (C (Maybe a) a) instance, we get
1641   Given:  C a b  ... and hance by superclasses, (G a, L a b)
1642   Wanted: G (Maybe a)
1643 Use the instance decl to get
1644   Wanted: C a b'
1645 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1646 and now we need improvement between that derived superclass an the Given (L a b)
1647
1648 Note [Overriding implicit parameters]
1649 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1650 Consider
1651    f :: (?x::a) -> Bool -> a
1652   
1653    g v = let ?x::Int = 3 
1654          in (f v, let ?x::Bool = True in f v)
1655
1656 This should probably be well typed, with
1657    g :: Bool -> (Int, Bool)
1658
1659 So the inner binding for ?x::Bool *overrides* the outer one.
1660 Hence a work-item Given overrides an inert-item Given.
1661
1662 Note [Given constraint that matches an instance declaration]
1663 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1664 What should we do when we discover that one (or more) top-level 
1665 instances match a given (or solved) class constraint? We have 
1666 two possibilities:
1667
1668   1. Reject the program. The reason is that there may not be a unique
1669      best strategy for the solver. Example, from the OutsideIn(X) paper:
1670        instance P x => Q [x] 
1671        instance (x ~ y) => R [x] y 
1672      
1673        wob :: forall a b. (Q [b], R b a) => a -> Int 
1674
1675        g :: forall a. Q [a] => [a] -> Int 
1676        g x = wob x 
1677
1678        will generate the impliation constraint: 
1679             Q [a] => (Q [beta], R beta [a]) 
1680        If we react (Q [beta]) with its top-level axiom, we end up with a 
1681        (P beta), which we have no way of discharging. On the other hand, 
1682        if we react R beta [a] with the top-level we get  (beta ~ a), which 
1683        is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is 
1684        now solvable by the given Q [a]. 
1685  
1686      However, this option is restrictive, for instance [Example 3] from 
1687      Note [Recursive instances and superclases] will fail to work. 
1688
1689   2. Ignore the problem, hoping that the situations where there exist indeed
1690      such multiple strategies are rare: Indeed the cause of the previous 
1691      problem is that (R [x] y) yields the new work (x ~ y) which can be 
1692      *spontaneously* solved, not using the givens. 
1693
1694 We are choosing option 2 below but we might consider having a flag as well.
1695
1696
1697 Note [New Wanted Superclass Work] 
1698 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1699 Even in the case of wanted constraints, we may add some superclasses 
1700 as new given work. The reason is: 
1701
1702         To allow FD-like improvement for type families. Assume that 
1703         we have a class 
1704              class C a b | a -> b 
1705         and we have to solve the implication constraint: 
1706              C a b => C a beta 
1707         Then, FD improvement can help us to produce a new wanted (beta ~ b) 
1708
1709         We want to have the same effect with the type family encoding of 
1710         functional dependencies. Namely, consider: 
1711              class (F a ~ b) => C a b 
1712         Now suppose that we have: 
1713                given: C a b 
1714                wanted: C a beta 
1715         By interacting the given we will get given (F a ~ b) which is not 
1716         enough by itself to make us discharge (C a beta). However, we 
1717         may create a new derived equality from the super-class of the
1718         wanted constraint (C a beta), namely derived (F a ~ beta). 
1719         Now we may interact this with given (F a ~ b) to get: 
1720                   derived :  beta ~ b 
1721         But 'beta' is a touchable unification variable, and hence OK to 
1722         unify it with 'b', replacing the derived evidence with the identity. 
1723
1724         This requires trySpontaneousSolve to solve *derived*
1725         equalities that have a touchable in their RHS, *in addition*
1726         to solving wanted equalities.
1727
1728 We also need to somehow use the superclasses to quantify over a minimal, 
1729 constraint see note [Minimize by Superclasses] in TcSimplify.
1730
1731
1732 Finally, here is another example where this is useful. 
1733
1734 Example 1:
1735 ----------
1736    class (F a ~ b) => C a b 
1737 And we are given the wanteds:
1738       w1 : C a b 
1739       w2 : C a c 
1740       w3 : b ~ c 
1741 We surely do *not* want to quantify over (b ~ c), since if someone provides
1742 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof 
1743 of (b ~ c), hence no extra evidence is necessary. Here is what will happen: 
1744
1745      Step 1: We will get new *given* superclass work, 
1746              provisionally to our solving of w1 and w2
1747              
1748                g1: F a ~ b, g2 : F a ~ c, 
1749                w1 : C a b, w2 : C a c, w3 : b ~ c
1750
1751              The evidence for g1 and g2 is a superclass evidence term: 
1752
1753                g1 := sc w1, g2 := sc w2
1754
1755      Step 2: The givens will solve the wanted w3, so that 
1756                w3 := sym (sc w1) ; sc w2 
1757                   
1758      Step 3: Now, one may naively assume that then w2 can be solve from w1
1759              after rewriting with the (now solved equality) (b ~ c). 
1760              
1761              But this rewriting is ruled out by the isGoodRectDict! 
1762
1763 Conclusion, we will (correctly) end up with the unsolved goals 
1764     (C a b, C a c)   
1765
1766 NB: The desugarer needs be more clever to deal with equalities 
1767     that participate in recursive dictionary bindings. 
1768
1769 \begin{code}
1770 data LookupInstResult
1771   = NoInstance
1772   | GenInst [EvVar] EvTerm 
1773
1774 matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1775 matchClassInst inerts clas tys loc
1776    = do { let pred = mkClassPred clas tys 
1777         ; mb_result <- matchClass clas tys
1778         ; untch <- getUntouchables
1779         ; case mb_result of
1780             MatchInstNo   -> return NoInstance
1781             MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1782                                                -- we learn more about the reagent 
1783             MatchInstSingle (_,_)
1784               | given_overlap untch -> 
1785                   do { traceTcS "Delaying instance application" $ 
1786                        vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
1787                             , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
1788                      ; return NoInstance -- see Note [Instance and Given overlap]
1789                      }
1790
1791             MatchInstSingle (dfun_id, mb_inst_tys) ->
1792               do { checkWellStagedDFun pred dfun_id loc
1793
1794         -- It's possible that not all the tyvars are in
1795         -- the substitution, tenv. For example:
1796         --      instance C X a => D X where ...
1797         -- (presumably there's a functional dependency in class C)
1798         -- Hence mb_inst_tys :: Either TyVar TcType 
1799
1800                  ; tys <- instDFunTypes mb_inst_tys
1801                  ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1802                  ; if null theta then
1803                        return (GenInst [] (EvDFunApp dfun_id tys []))
1804                    else do
1805                      { evc_vars <- instDFunConstraints theta (Wanted loc)
1806                      ; let ev_vars = map evc_the_evvar evc_vars
1807                            new_ev_vars = [evc_the_evvar evc | evc <- evc_vars, isNewEvVar evc]
1808                            -- new_ev_vars are only the real new variables that can be emitted 
1809                      ; return $ GenInst new_ev_vars (EvDFunApp dfun_id tys ev_vars) }
1810                  }
1811         }
1812    where 
1813      givens_for_this_clas :: Cts
1814      givens_for_this_clas 
1815          = lookupUFM (cts_given (inert_dicts inerts)) clas `orElse` emptyCts
1816
1817      given_overlap :: TcsUntouchables -> Bool
1818      given_overlap untch = anyBag (matchable untch) givens_for_this_clas
1819
1820      matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_flavor = fl })
1821        | Just GivenOrig <- isGiven_maybe fl
1822        = ASSERT( clas_g == clas )
1823          case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv && 
1824                                     tv `elemVarSet` tyVarsOfTypes tys
1825                                  then BindMe else Skolem) tys sys of
1826        -- We can't learn anything more about any variable at this point, so the only
1827        -- cause of overlap can be by an instantiation of a touchable unification
1828        -- variable. Hence we only bind touchable unification variables. In addition,
1829        -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
1830             Nothing -> False
1831             Just _  -> True
1832        | otherwise = False -- No overlap with a solved, already been taken care of 
1833                            -- by the overlap check with the instance environment.
1834      matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
1835 \end{code}
1836
1837 Note [Instance and Given overlap]
1838 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1839 Assume that we have an inert set that looks as follows:
1840        [Given] D [Int]
1841 And an instance declaration: 
1842        instance C a => D [a]
1843 A new wanted comes along of the form: 
1844        [Wanted] D [alpha]
1845
1846 One possibility is to apply the instance declaration which will leave us 
1847 with an unsolvable goal (C alpha). However, later on a new constraint may 
1848 arise (for instance due to a functional dependency between two later dictionaries), 
1849 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha]) 
1850 will be transformed to [Wanted] D [Int], which could have been discharged by the given. 
1851
1852 The solution is that in matchClassInst and eventually in topReact, we get back with 
1853 a matching instance, only when there is no Given in the inerts which is unifiable to
1854 this particular dictionary.
1855
1856 The end effect is that, much as we do for overlapping instances, we delay choosing a 
1857 class instance if there is a possibility of another instance OR a given to match our 
1858 constraint later on. This fixes bugs #4981 and #5002.
1859
1860 This is arguably not easy to appear in practice due to our aggressive prioritization 
1861 of equality solving over other constraints, but it is possible. I've added a test case 
1862 in typecheck/should-compile/GivenOverlapping.hs
1863
1864 Moreover notice that our goals here are different than the goals of the top-level 
1865 overlapping checks. There we are interested in validating the following principle:
1866  
1867     If we inline a function f at a site where the same global instance environment
1868     is available as the instance environment at the definition site of f then we 
1869     should get the same behaviour. 
1870
1871 But for the Given Overlap check our goal is just related to completeness of 
1872 constraint solving. 
1873
1874
1875
1876