Hurrah! This major commit adds support for scoped kind variables,
[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        ; let xi' = defaultKind xi      
637                -- We only instantiate kind unification variables
638                -- with simple kinds like *, not OpenKind or ArgKind
639                -- cf TcUnify.uUnboundKVar
640
641        ; setWantedTyBind tv xi'
642        ; let refl_xi = mkTcReflCo xi'
643
644        ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercion refl_xi) 
645        ; (_,eqv_given) <- newGivenEqVar solved_fl (mkTyVarTy tv) xi' refl_xi
646
647        ; when (isWanted wd) $ do { _ <- setEqBind eqv refl_xi wd; return () }
648            -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
649        ; return $ SPSolved (CTyEqCan { cc_id     = eqv_given
650                                      , cc_flavor = solved_fl
651                                      , cc_tyvar  = tv, cc_rhs = xi', cc_depth = d }) }
652 \end{code}
653
654
655 *********************************************************************************
656 *                                                                               * 
657                        The interact-with-inert Stage
658 *                                                                               *
659 *********************************************************************************
660
661 Note [The Solver Invariant]
662 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
663 We always add Givens first.  So you might think that the solver has
664 the invariant
665
666    If the work-item is Given, 
667    then the inert item must Given
668
669 But this isn't quite true.  Suppose we have, 
670     c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
671 After processing the first two, we get
672      c1: [G] beta ~ [alpha], c2 : [W] blah
673 Now, c3 does not interact with the the given c1, so when we spontaneously
674 solve c3, we must re-react it with the inert set.  So we can attempt a 
675 reaction between inert c2 [W] and work-item c3 [G].
676
677 It *is* true that [Solver Invariant]
678    If the work-item is Given, 
679    AND there is a reaction
680    then the inert item must Given
681 or, equivalently,
682    If the work-item is Given, 
683    and the inert item is Wanted/Derived
684    then there is no reaction
685
686 \begin{code}
687 -- Interaction result of  WorkItem <~> AtomicInert
688
689 data InteractResult 
690     = IRWorkItemConsumed { ir_fire :: String } 
691     | IRInertConsumed    { ir_fire :: String } 
692     | IRKeepGoing        { ir_fire :: String }
693
694 irWorkItemConsumed :: String -> TcS InteractResult
695 irWorkItemConsumed str = return (IRWorkItemConsumed str) 
696
697 irInertConsumed :: String -> TcS InteractResult
698 irInertConsumed str = return (IRInertConsumed str) 
699
700 irKeepGoing :: String -> TcS InteractResult 
701 irKeepGoing str = return (IRKeepGoing str) 
702 -- You can't discard neither workitem or inert, but you must keep 
703 -- going. It's possible that new work is waiting in the TcS worklist. 
704
705
706 interactWithInertsStage :: WorkItem -> TcS StopOrContinue 
707 -- Precondition: if the workitem is a CTyEqCan then it will not be able to 
708 -- react with anything at this stage. 
709 interactWithInertsStage wi 
710   = do { ctxt <- getTcSContext
711        ; if simplEqsOnly ctxt then 
712              return (ContinueWith wi)
713          else 
714              extractRelevantInerts wi >>= 
715                foldlBagM interact_next (ContinueWith wi) }
716
717   where interact_next Stop atomic_inert 
718           = updInertSetTcS atomic_inert >> return Stop
719         interact_next (ContinueWith wi) atomic_inert 
720           = do { ir <- doInteractWithInert atomic_inert wi
721                ; let mk_msg rule keep_doc 
722                        = text rule <+> keep_doc
723                          <+> vcat [ ptext (sLit "Inert =") <+> ppr atomic_inert
724                                   , ptext (sLit "Work =")  <+> ppr wi ]
725                ; case ir of 
726                    IRWorkItemConsumed { ir_fire = rule } 
727                        -> do { bumpStepCountTcS
728                              ; traceFireTcS (cc_depth wi) 
729                                             (mk_msg rule (text "WorkItemConsumed"))
730                              ; updInertSetTcS atomic_inert
731                              ; return Stop } 
732                    IRInertConsumed { ir_fire = rule }
733                        -> do { bumpStepCountTcS
734                              ; traceFireTcS (cc_depth atomic_inert) 
735                                             (mk_msg rule (text "InertItemConsumed"))
736                              ; return (ContinueWith wi) }
737                    IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
738                        -> do { updInertSetTcS atomic_inert
739                              ; return (ContinueWith wi) }
740                }
741    
742 --------------------------------------------
743 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
744
745 doInteractWithInert :: Ct -> Ct -> TcS InteractResult
746 -- Identical class constraints.
747 doInteractWithInert
748   inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
749    workItem@(CDictCan { cc_id = _d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
750
751   | cls1 == cls2  
752   = do { let pty1 = mkClassPred cls1 tys1
753              pty2 = mkClassPred cls2 tys2
754              inert_pred_loc     = (pty1, pprFlavorArising fl1)
755              work_item_pred_loc = (pty2, pprFlavorArising fl2)
756
757        ; traceTcS "doInteractWithInert" (vcat [ text "inertItem = " <+> ppr inertItem
758                                               , text "workItem  = " <+> ppr workItem ])
759
760        ; any_fundeps 
761            <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
762               -- NB: We don't create fds for given (and even solved), have not seen a useful
763               -- situation for these and even if we did we'd have to be very careful to only
764               -- create Derived's and not Wanteds. 
765
766               else do { let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
767                       ; wloc  <- get_workitem_wloc fl2 
768                       ; rewriteWithFunDeps fd_eqns tys2 wloc }
769                       -- See Note [Efficient Orientation], [When improvement happens]
770
771        ; case any_fundeps of
772            -- No Functional Dependencies 
773            Nothing             
774                | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
775                | otherwise         -> irKeepGoing "NOP"
776
777            -- Actual Functional Dependencies
778            Just (_rewritten_tys2,_cos2,fd_work)
779               -- Standard thing: create derived fds and keep on going. Importantly we don't
780                -- throw workitem back in the worklist because this can cause loops. See #5236.
781                -> do { emitFDWorkAsDerived fd_work (cc_depth workItem)
782                      ; irKeepGoing "Cls/Cls (new fundeps)" } -- Just keep going without droping the inert 
783        }
784   where get_workitem_wloc (Wanted wl)  = return wl 
785         get_workitem_wloc (Derived wl) = return wl 
786         get_workitem_wloc (Given {})   = pprPanic "Unexpected given workitem!" $
787                                          vcat [ text "Work item =" <+> ppr workItem
788                                               , text "Inert item=" <+> ppr inertItem
789                                               ]
790
791 -- Two pieces of irreducible evidence: if their types are *exactly identical* we can
792 -- rewrite them. We can never improve using this: if we want ty1 :: Constraint and have
793 -- ty2 :: Constraint it clearly does not mean that (ty1 ~ ty2)
794 doInteractWithInert (CIrredEvCan { cc_id = id1, cc_flavor = ifl, cc_ty = ty1 })
795            workItem@(CIrredEvCan { cc_ty = ty2 })
796   | ty1 `eqType` ty2
797   = solveOneFromTheOther "Irred/Irred" (EvId id1,ifl) workItem
798
799 -- Two implicit parameter constraints.  If the names are the same,
800 -- but their types are not, we generate a wanted type equality 
801 -- that equates the type (this is "improvement").  
802 -- However, we don't actually need the coercion evidence,
803 -- so we just generate a fresh coercion variable that isn't used anywhere.
804 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) 
805            workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
806   | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
807   =     -- See Note [Overriding implicit parameters]
808         -- Dump the inert item, override totally with the new one
809         -- Do not require type equality
810         -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
811         --              we must *override* the outer one with the inner one
812     irInertConsumed "IP/IP (override inert)"
813
814   | nm1 == nm2 && ty1 `eqType` ty2 
815   = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem 
816
817   | nm1 == nm2
818   =     -- See Note [When improvement happens]
819     do { let flav = Wanted (combineCtLoc ifl wfl)
820        ; eqv <- newEqVar flav ty2 ty1 -- See Note [Efficient Orientation]
821        ; when (isNewEvVar eqv) $
822               (let ct = CNonCanonical { cc_id     = evc_the_evvar eqv 
823                                       , cc_flavor = flav
824                                       , cc_depth  = cc_depth workItem }
825               in updWorkListTcS (extendWorkListEq ct))
826
827        ; case wfl of
828            Given   {} -> pprPanic "Unexpected given IP" (ppr workItem)
829            Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
830            Wanted  {} ->
831                do { _ <- setEvBind (cc_id workItem) 
832                             (mkEvCast id1 (mkTcSymCo (mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo (evc_the_evvar eqv)]))) wfl
833                   ; irWorkItemConsumed "IP/IP (solved by rewriting)" } }
834
835 doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1
836                                , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
837                     (CFunEqCan { cc_id = eqv2, cc_flavor = fl2, cc_fun = tc2
838                                , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
839   | lhss_match  
840   , Just (GivenSolved {}) <- isGiven_maybe fl1 -- Inert is solved and we can simply ignore it
841                                           -- when workitem is given/solved
842   , isGivenOrSolved fl2
843   = irInertConsumed "FunEq/FunEq"
844   | lhss_match 
845   , Just (GivenSolved {}) <- isGiven_maybe fl2 -- Workitem is solved and we can ignore it when
846                                                -- the inert is given/solved
847   , isGivenOrSolved fl1                 
848   = irWorkItemConsumed "FunEq/FunEq" 
849   | fl1 `canSolve` fl2 && lhss_match
850   = do { rewriteEqLHS LeftComesFromInert  (eqv1,xi1) (eqv2,d2,fl2,xi2) 
851        ; irWorkItemConsumed "FunEq/FunEq" }
852
853   | fl2 `canSolve` fl1 && lhss_match
854   = do { rewriteEqLHS RightComesFromInert (eqv2,xi2) (eqv1,d1,fl1,xi1) 
855        ; irInertConsumed "FunEq/FunEq"}
856   where
857     lhss_match = tc1 == tc2 && eqTypes args1 args2 
858
859
860 doInteractWithInert _ _ = irKeepGoing "NOP"
861
862
863 rewriteEqLHS :: WhichComesFromInert -> (EqVar,Xi) -> (EqVar,SubGoalDepth,CtFlavor,Xi) -> TcS ()
864 -- Used to ineract two equalities of the following form: 
865 -- First Equality:   co1: (XXX ~ xi1)  
866 -- Second Equality:  cv2: (XXX ~ xi2) 
867 -- Where the cv1 `canRewrite` cv2 equality 
868 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1), 
869 --    See Note [Efficient Orientation] for that 
870 rewriteEqLHS LeftComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) 
871   = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
872        ; evc <- newEqVar gw xi2 xi1
873        ; let eqv2' = evc_the_evvar evc
874        ; gw' <- case gw of 
875            Wanted {} 
876                -> setEqBind eqv2 
877                     (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcSymCo (mkTcCoVarCo eqv2')) gw
878            Given {}
879                -> setEqBind eqv2'
880                     (mkTcSymCo (mkTcCoVarCo eqv2) `mkTcTransCo` mkTcCoVarCo eqv1) gw
881            Derived {} 
882                -> return gw
883        ; when (isNewEvVar evc) $ 
884               updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id     = eqv2'
885                                                               , cc_flavor = gw'
886                                                               , cc_depth  = d } ) ) }
887
888 rewriteEqLHS RightComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) 
889   = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
890        ; evc <- newEqVar gw xi1 xi2
891        ; let eqv2' = evc_the_evvar evc
892        ; gw' <- case gw of
893            Wanted {} 
894                -> setEqBind eqv2
895                     (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcCoVarCo eqv2') gw
896            Given {}  
897                -> setEqBind eqv2'
898                     (mkTcSymCo (mkTcCoVarCo eqv1) `mkTcTransCo` mkTcCoVarCo eqv2) gw
899            Derived {} 
900                -> return gw
901
902        ; when (isNewEvVar evc) $
903               updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id = eqv2'
904                                                               , cc_flavor = gw'
905                                                               , cc_depth  = d } ) ) }
906
907 solveOneFromTheOther :: String             -- Info 
908                      -> (EvTerm, CtFlavor) -- Inert 
909                      -> Ct        -- WorkItem 
910                      -> TcS InteractResult
911 -- Preconditions: 
912 -- 1) inert and work item represent evidence for the /same/ predicate
913 -- 2) ip/class/irred evidence (no coercions) only
914 solveOneFromTheOther info (ev_term,ifl) workItem
915   | isDerived wfl
916   = irWorkItemConsumed ("Solved[DW] " ++ info)
917
918   | isDerived ifl -- The inert item is Derived, we can just throw it away, 
919                   -- The workItem is inert wrt earlier inert-set items, 
920                   -- so it's safe to continue on from this point
921   = irInertConsumed ("Solved[DI] " ++ info)
922   
923   | Just (GivenSolved {}) <- isGiven_maybe ifl, isGivenOrSolved wfl
924     -- Same if the inert is a GivenSolved -- just get rid of it
925   = irInertConsumed ("Solved[SI] " ++ info)
926
927   | otherwise
928   = ASSERT( ifl `canSolve` wfl )
929       -- Because of Note [The Solver Invariant], plus Derived dealt with
930     do { when (isWanted wfl) $ do { _ <- setEvBind wid ev_term wfl; return () }
931            -- Overwrite the binding, if one exists
932            -- If both are Given, we already have evidence; no need to duplicate
933        ; irWorkItemConsumed ("Solved " ++ info) }
934   where 
935      wfl = cc_flavor workItem
936      wid = cc_id workItem
937
938 \end{code}
939
940 Note [Superclasses and recursive dictionaries]
941 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
942     Overlaps with Note [SUPERCLASS-LOOP 1]
943                   Note [SUPERCLASS-LOOP 2]
944                   Note [Recursive instances and superclases]
945     ToDo: check overlap and delete redundant stuff
946
947 Right before adding a given into the inert set, we must
948 produce some more work, that will bring the superclasses 
949 of the given into scope. The superclass constraints go into 
950 our worklist. 
951
952 When we simplify a wanted constraint, if we first see a matching
953 instance, we may produce new wanted work. To (1) avoid doing this work 
954 twice in the future and (2) to handle recursive dictionaries we may ``cache'' 
955 this item as given into our inert set WITHOUT adding its superclass constraints, 
956 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
957 for doing the isGoodRecEv check in an older version of the type checker]. 
958
959 But now we have added partially solved constraints to the worklist which may 
960 interact with other wanteds. Consider the example: 
961
962 Example 1: 
963
964     class Eq b => Foo a b        --- 0-th selector
965     instance Eq a => Foo [a] a   --- fooDFun
966
967 and wanted (Foo [t] t). We are first going to see that the instance matches 
968 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
969        d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3 
970 Our work list is going to contain a new *wanted* goal
971        d3 :_w Eq t 
972
973 Ok, so how do we get recursive dictionaries, at all: 
974
975 Example 2:
976
977     data D r = ZeroD | SuccD (r (D r));
978     
979     instance (Eq (r (D r))) => Eq (D r) where
980         ZeroD     == ZeroD     = True
981         (SuccD a) == (SuccD b) = a == b
982         _         == _         = False;
983     
984     equalDC :: D [] -> D [] -> Bool;
985     equalDC = (==);
986
987 We need to prove (Eq (D [])). Here's how we go:
988
989         d1 :_w Eq (D [])
990
991 by instance decl, holds if
992         d2 :_w Eq [D []]
993         where   d1 = dfEqD d2
994
995 *BUT* we have an inert set which gives us (no superclasses): 
996         d1 :_g Eq (D []) 
997 By the instance declaration of Eq we can show the 'd2' goal if 
998         d3 :_w Eq (D [])
999         where   d2 = dfEqList d3
1000                 d1 = dfEqD d2
1001 Now, however this wanted can interact with our inert d1 to set: 
1002         d3 := d1 
1003 and solve the goal. Why was this interaction OK? Because, if we chase the 
1004 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we 
1005 are really setting
1006         d3 := dfEqD2 (dfEqList d3) 
1007 which is FINE because the use of d3 is protected by the instance function 
1008 applications. 
1009
1010 So, our strategy is to try to put solved wanted dictionaries into the
1011 inert set along with their superclasses (when this is meaningful,
1012 i.e. when new wanted goals are generated) but solve a wanted dictionary
1013 from a given only in the case where the evidence variable of the
1014 wanted is mentioned in the evidence of the given (recursively through
1015 the evidence binds) in a protected way: more instance function applications 
1016 than superclass selectors.
1017
1018 Here are some more examples from GHC's previous type checker
1019
1020
1021 Example 3: 
1022 This code arises in the context of "Scrap Your Boilerplate with Class"
1023
1024     class Sat a
1025     class Data ctx a
1026     instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
1027     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
1028
1029     class Data Maybe a => Foo a    
1030
1031     instance Foo t => Sat (Maybe t)                             -- dfunSat
1032
1033     instance Data Maybe a => Foo a                              -- dfunFoo1
1034     instance Foo a        => Foo [a]                            -- dfunFoo2
1035     instance                 Foo [Char]                         -- dfunFoo3
1036
1037 Consider generating the superclasses of the instance declaration
1038          instance Foo a => Foo [a]
1039
1040 So our problem is this
1041     d0 :_g Foo t
1042     d1 :_w Data Maybe [t] 
1043
1044 We may add the given in the inert set, along with its superclasses
1045 [assuming we don't fail because there is a matching instance, see 
1046  tryTopReact, given case ]
1047   Inert:
1048     d0 :_g Foo t 
1049   WorkList 
1050     d01 :_g Data Maybe t  -- d2 := EvDictSuperClass d0 0 
1051     d1 :_w Data Maybe [t] 
1052 Then d2 can readily enter the inert, and we also do solving of the wanted
1053   Inert: 
1054     d0 :_g Foo t 
1055     d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1056   WorkList
1057     d2 :_w Sat (Maybe [t])          
1058     d3 :_w Data Maybe t
1059     d01 :_g Data Maybe t 
1060 Now, we may simplify d2 more: 
1061   Inert:
1062       d0 :_g Foo t 
1063       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1064       d1 :_g Data Maybe [t] 
1065       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
1066   WorkList: 
1067       d3 :_w Data Maybe t 
1068       d4 :_w Foo [t] 
1069       d01 :_g Data Maybe t 
1070
1071 Now, we can just solve d3.
1072   Inert
1073       d0 :_g Foo t 
1074       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1075       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
1076   WorkList
1077       d4 :_w Foo [t] 
1078       d01 :_g Data Maybe t 
1079 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1080   Inert
1081       d0 :_g Foo t 
1082       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1083       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
1084       d4 :_g Foo [t]                  d4 := dfunFoo2 d5 
1085   WorkList:
1086       d5 :_w Foo t 
1087       d6 :_g Data Maybe [t]           d6 := EvDictSuperClass d4 0
1088       d01 :_g Data Maybe t 
1089 Now, d5 can be solved! (and its superclass enter scope) 
1090   Inert
1091       d0 :_g Foo t 
1092       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
1093       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
1094       d4 :_g Foo [t]                  d4 := dfunFoo2 d5 
1095       d5 :_g Foo t                    d5 := dfunFoo1 d7
1096   WorkList:
1097       d7 :_w Data Maybe t
1098       d6 :_g Data Maybe [t]
1099       d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
1100       d01 :_g Data Maybe t 
1101
1102 Now, two problems: 
1103    [1] Suppose we pick d8 and we react him with d01. Which of the two givens should 
1104        we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence 
1105        that must not be used (look at case interactInert where both inert and workitem
1106        are givens). So we have several options: 
1107        - Drop the workitem always (this will drop d8)
1108               This feels very unsafe -- what if the work item was the "good" one
1109               that should be used later to solve another wanted?
1110        - Don't drop anyone: the inert set may contain multiple givens! 
1111               [This is currently implemented] 
1112
1113 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2: 
1114   [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1115       d7. Now the [isRecDictEv] function in the ineration solver 
1116       [case inert-given workitem-wanted] will prevent us from interacting d7 := d8 
1117       precisely because chasing the evidence of d8 leads us to an unguarded use of d7. 
1118
1119       So, no interaction happens there. Then we meet d01 and there is no recursion 
1120       problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01! 
1121              
1122 Note [SUPERCLASS-LOOP 1]
1123 ~~~~~~~~~~~~~~~~~~~~~~~~
1124 We have to be very, very careful when generating superclasses, lest we
1125 accidentally build a loop. Here's an example:
1126
1127   class S a
1128
1129   class S a => C a where { opc :: a -> a }
1130   class S b => D b where { opd :: b -> b }
1131   
1132   instance C Int where
1133      opc = opd
1134   
1135   instance D Int where
1136      opd = opc
1137
1138 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1139 Simplifying, we may well get:
1140         $dfCInt = :C ds1 (opd dd)
1141         dd  = $dfDInt
1142         ds1 = $p1 dd
1143 Notice that we spot that we can extract ds1 from dd.  
1144
1145 Alas!  Alack! We can do the same for (instance D Int):
1146
1147         $dfDInt = :D ds2 (opc dc)
1148         dc  = $dfCInt
1149         ds2 = $p1 dc
1150
1151 And now we've defined the superclass in terms of itself.
1152 Two more nasty cases are in
1153         tcrun021
1154         tcrun033
1155
1156 Solution: 
1157   - Satisfy the superclass context *all by itself* 
1158     (tcSimplifySuperClasses)
1159   - And do so completely; i.e. no left-over constraints
1160     to mix with the constraints arising from method declarations
1161
1162
1163 Note [SUPERCLASS-LOOP 2]
1164 ~~~~~~~~~~~~~~~~~~~~~~~~
1165 We need to be careful when adding "the constaint we are trying to prove".
1166 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1167
1168         class Ord a => C a where
1169         instance Ord [a] => C [a] where ...
1170
1171 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1172 superclasses of C [a] to avails.  But we must not overwrite the binding
1173 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1174 build a loop! 
1175
1176 Here's another variant, immortalised in tcrun020
1177         class Monad m => C1 m
1178         class C1 m => C2 m x
1179         instance C2 Maybe Bool
1180 For the instance decl we need to build (C1 Maybe), and it's no good if
1181 we run around and add (C2 Maybe Bool) and its superclasses to the avails 
1182 before we search for C1 Maybe.
1183
1184 Here's another example 
1185         class Eq b => Foo a b
1186         instance Eq a => Foo [a] a
1187 If we are reducing
1188         (Foo [t] t)
1189
1190 we'll first deduce that it holds (via the instance decl).  We must not
1191 then overwrite the Eq t constraint with a superclass selection!
1192
1193 At first I had a gross hack, whereby I simply did not add superclass constraints
1194 in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
1195 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1196 I found a very obscure program (now tcrun021) in which improvement meant the
1197 simplifier got two bites a the cherry... so something seemed to be an Stop
1198 first time, but reducible next time.
1199
1200 Now we implement the Right Solution, which is to check for loops directly 
1201 when adding superclasses.  It's a bit like the occurs check in unification.
1202
1203 Note [Recursive instances and superclases]
1204 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1205 Consider this code, which arises in the context of "Scrap Your 
1206 Boilerplate with Class".  
1207
1208     class Sat a
1209     class Data ctx a
1210     instance  Sat (ctx Char)             => Data ctx Char
1211     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1212
1213     class Data Maybe a => Foo a
1214
1215     instance Foo t => Sat (Maybe t)
1216
1217     instance Data Maybe a => Foo a
1218     instance Foo a        => Foo [a]
1219     instance                 Foo [Char]
1220
1221 In the instance for Foo [a], when generating evidence for the superclasses
1222 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1223 Using the instance for Data, we therefore need
1224         (Sat (Maybe [a], Data Maybe a)
1225 But we are given (Foo a), and hence its superclass (Data Maybe a).
1226 So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
1227 we need (Foo [a]).  And that is the very dictionary we are bulding
1228 an instance for!  So we must put that in the "givens".  So in this
1229 case we have
1230         Given:  Foo a, Foo [a]
1231         Wanted: Data Maybe [a]
1232
1233 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1234 the givens, which is what 'addGiven' would normally do. Why? Because
1235 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted 
1236 by selecting a superclass from Foo [a], which simply makes a loop.
1237
1238 On the other hand we *must* put the superclasses of (Foo a) in
1239 the givens, as you can see from the derivation described above.
1240
1241 Conclusion: in the very special case of tcSimplifySuperClasses
1242 we have one 'given' (namely the "this" dictionary) whose superclasses
1243 must not be added to 'givens' by addGiven.  
1244
1245 There is a complication though.  Suppose there are equalities
1246       instance (Eq a, a~b) => Num (a,b)
1247 Then we normalise the 'givens' wrt the equalities, so the original
1248 given "this" dictionary is cast to one of a different type.  So it's a
1249 bit trickier than before to identify the "special" dictionary whose
1250 superclasses must not be added. See test
1251    indexed-types/should_run/EqInInstance
1252
1253 We need a persistent property of the dictionary to record this
1254 special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
1255 but cool), which is maintained by dictionary normalisation.
1256 Specifically, the InstLocOrigin is
1257              NoScOrigin
1258 then the no-superclass thing kicks in.  WATCH OUT if you fiddle
1259 with InstLocOrigin!
1260
1261 Note [MATCHING-SYNONYMS]
1262 ~~~~~~~~~~~~~~~~~~~~~~~~
1263 When trying to match a dictionary (D tau) to a top-level instance, or a 
1264 type family equation (F taus_1 ~ tau_2) to a top-level family instance, 
1265 we do *not* need to expand type synonyms because the matcher will do that for us.
1266
1267
1268 Note [RHS-FAMILY-SYNONYMS] 
1269 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1270 The RHS of a family instance is represented as yet another constructor which is 
1271 like a type synonym for the real RHS the programmer declared. Eg: 
1272     type instance F (a,a) = [a] 
1273 Becomes: 
1274     :R32 a = [a]      -- internal type synonym introduced
1275     F (a,a) ~ :R32 a  -- instance 
1276
1277 When we react a family instance with a type family equation in the work list 
1278 we keep the synonym-using RHS without expansion. 
1279
1280
1281 %************************************************************************
1282 %*                                                                      *
1283 %*          Functional dependencies, instantiation of equations
1284 %*                                                                      *
1285 %************************************************************************
1286
1287 When we spot an equality arising from a functional dependency,
1288 we now use that equality (a "wanted") to rewrite the work-item
1289 constraint right away.  This avoids two dangers
1290
1291  Danger 1: If we send the original constraint on down the pipeline
1292            it may react with an instance declaration, and in delicate
1293            situations (when a Given overlaps with an instance) that
1294            may produce new insoluble goals: see Trac #4952
1295
1296  Danger 2: If we don't rewrite the constraint, it may re-react
1297            with the same thing later, and produce the same equality
1298            again --> termination worries.
1299
1300 To achieve this required some refactoring of FunDeps.lhs (nicer
1301 now!).  
1302
1303 \begin{code}
1304 rewriteWithFunDeps :: [Equation]
1305                    -> [Xi] 
1306                    -> WantedLoc 
1307                    -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) 
1308                                            -- Not quite a WantedEvVar unfortunately
1309                                            -- Because our intention could be to make 
1310                                            -- it derived at the end of the day
1311 -- NB: The flavor of the returned EvVars will be decided by the caller
1312 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1313 rewriteWithFunDeps eqn_pred_locs xis wloc
1314  = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
1315       ; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
1316             fd_ev_pos = concat fd_ev_poss
1317             (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
1318       ; if null fd_ev_pos then return Nothing
1319         else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
1320
1321 instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
1322 -- Post: Returns the position index as well as the corresponding FunDep equality
1323 instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
1324                         , fd_pred1 = d1, fd_pred2 = d2 })
1325   = do { let tvs = varSetElems qtvs
1326        ; tvs' <- mapM instFlexiTcS tvs  -- IA0_TODO: we might need to do kind substitution
1327        ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
1328        ; foldM (do_one subst) [] eqs }
1329   where 
1330     do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
1331        = let sty1 = Type.substTy subst ty1 
1332              sty2 = Type.substTy subst ty2 
1333          in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
1334             else do { eqv <- newEqVar (Derived wl) sty1 sty2 -- Create derived or cached by deriveds
1335                     ; let wl' = push_ctx wl 
1336                     ; if isNewEvVar eqv then 
1337                           return $ (i,(evc_the_evvar eqv,wl')):ievs 
1338                       else -- We are eventually going to emit FD work back in the work list so 
1339                            -- it is important that we only return the /freshly created/ and not 
1340                            -- some existing equality!
1341                           return ievs }
1342
1343     push_ctx :: WantedLoc -> WantedLoc 
1344     push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1345
1346 mkEqnMsg :: (TcPredType, SDoc) 
1347          -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
1348 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1349   = do  { zpred1 <- zonkTcPredType pred1
1350         ; zpred2 <- zonkTcPredType pred2
1351         ; let { tpred1 = tidyType tidy_env zpred1
1352               ; tpred2 = tidyType tidy_env zpred2 }
1353         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1354                           nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
1355                           nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1356         ; return (tidy_env, msg) }
1357
1358 rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
1359                   -> [Type]                    -- A sequence of types: tys
1360                   -> [(Type, TcCoercion)]      -- Returns: [(ty', co : ty' ~ ty)]
1361 rewriteDictParams param_eqs tys
1362   = zipWith do_one tys [0..]
1363   where
1364     do_one :: Type -> Int -> (Type, TcCoercion)
1365     do_one ty n = case lookup n param_eqs of
1366                     Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
1367                     Nothing  -> (ty,             mkTcReflCo ty) -- Identity
1368
1369     get_fst_ty (wev,_wloc) 
1370       | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
1371       = ty1
1372       | otherwise 
1373       = panic "rewriteDictParams: non equality fundep!?"
1374
1375         
1376 emitFDWorkAsDerived :: [(EvVar,WantedLoc)] 
1377                     -> SubGoalDepth -> TcS () 
1378 emitFDWorkAsDerived evlocs d 
1379   = updWorkListTcS $ appendWorkListEqs fd_cts
1380   where fd_cts = map mk_fd_ct evlocs 
1381         mk_fd_ct (v,wl) = CNonCanonical { cc_id = v
1382                                         , cc_flavor = Derived wl 
1383                                         , cc_depth = d }
1384
1385
1386 \end{code}
1387
1388
1389
1390
1391 *********************************************************************************
1392 *                                                                               * 
1393                        The top-reaction Stage
1394 *                                                                               *
1395 *********************************************************************************
1396
1397 \begin{code}
1398
1399 topReactionsStage :: SimplifierStage 
1400 topReactionsStage workItem 
1401  = tryTopReact workItem 
1402    
1403
1404 tryTopReact :: WorkItem -> TcS StopOrContinue
1405 tryTopReact wi 
1406  = do { inerts <- getTcSInerts
1407       ; ctxt   <- getTcSContext
1408       ; if simplEqsOnly ctxt then return (ContinueWith wi) -- or Stop?
1409         else 
1410             do { tir <- doTopReact inerts wi
1411                ; case tir of 
1412                    NoTopInt 
1413                        -> return (ContinueWith wi)
1414                    SomeTopInt rule what_next 
1415                        -> do { bumpStepCountTcS 
1416                              ; traceFireTcS (cc_depth wi) $
1417                                ptext (sLit "Top react:") <+> text rule
1418                              ; return what_next }
1419                } }
1420
1421 data TopInteractResult 
1422  = NoTopInt
1423  | SomeTopInt { tir_rule :: String, tir_new_item :: StopOrContinue }
1424
1425
1426 doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1427
1428 -- The work item does not react with the inert set, so try interaction
1429 -- with top-level instances 
1430 -- NB: The place to add superclasses in *not*
1431 -- in doTopReact stage. Instead superclasses are added in the worklist
1432 -- as part of the canonicalisation process. See Note [Adding superclasses].
1433
1434
1435 -- Given dictionary
1436 -- See Note [Given constraint that matches an instance declaration]
1437 doTopReact _inerts (CDictCan { cc_flavor = Given {} })
1438   = return NoTopInt -- NB: Superclasses already added since it's canonical
1439
1440 -- Derived dictionary: just look for functional dependencies
1441 doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
1442                                       , cc_class = cls, cc_tyargs = xis })
1443   = do { instEnvs <- getInstEnvs
1444        ; let fd_eqns = improveFromInstEnv instEnvs
1445                            (mkClassPred cls xis, pprArisingAt loc)
1446        ; m <- rewriteWithFunDeps fd_eqns xis loc
1447        ; case m of
1448            Nothing -> return NoTopInt
1449            Just (xis',_,fd_work) ->
1450                let workItem' = workItem { cc_tyargs = xis' }
1451                    -- Deriveds are not supposed to have identity (cc_id is unused!)
1452                in do { emitFDWorkAsDerived fd_work (cc_depth workItem)
1453                      ; return $ 
1454                        SomeTopInt { tir_rule  = "Derived Cls fundeps" 
1455                                   , tir_new_item = ContinueWith workItem' } }
1456        }
1457
1458 -- Wanted dictionary
1459 doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
1460                                      , cc_id    = dict_id
1461                                      , cc_class = cls, cc_tyargs = xis
1462                                      , cc_depth = depth })
1463   -- See Note [MATCHING-SYNONYMS]
1464   = do { traceTcS "doTopReact" (ppr workItem)
1465        ; instEnvs <- getInstEnvs
1466        ; let fd_eqns = improveFromInstEnv instEnvs 
1467                             (mkClassPred cls xis, pprArisingAt loc)
1468
1469        ; any_fundeps <- rewriteWithFunDeps fd_eqns xis loc
1470        ; case any_fundeps of
1471            -- No Functional Dependencies
1472            Nothing ->
1473                do { lkup_inst_res  <- matchClassInst inerts cls xis loc
1474                   ; case lkup_inst_res of
1475                       GenInst wtvs ev_term
1476                           -> doSolveFromInstance wtvs ev_term 
1477                       NoInstance
1478                           -> return NoTopInt
1479                   }
1480            -- Actual Functional Dependencies
1481            Just (_xis',_cos,fd_work) ->
1482                do { emitFDWorkAsDerived fd_work (cc_depth workItem)
1483                   ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
1484                                       , tir_new_item = ContinueWith workItem } } }
1485
1486    where doSolveFromInstance :: [EvVar] -> EvTerm -> TcS TopInteractResult
1487          -- Precondition: evidence term matches the predicate of cc_id of workItem
1488          doSolveFromInstance evs ev_term 
1489             | null evs
1490             = do { traceTcS "doTopReact/found nullary instance for" (ppr dict_id)
1491                  ; _ <- setEvBind dict_id ev_term fl
1492                  ; return $ 
1493                    SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" 
1494                               , tir_new_item = Stop } } -- Don't put him in the inerts
1495             | otherwise 
1496             = do { traceTcS "doTopReact/found non-nullary instance for" (ppr dict_id)
1497                  ; _ <- setEvBind dict_id ev_term fl
1498                         -- Solved and new wanted work produced, you may cache the 
1499                         -- (tentatively solved) dictionary as Solved given.
1500 --                 ; let _solved = workItem { cc_flavor = solved_fl }
1501 --                       solved_fl = mkSolvedFlavor fl UnkSkol
1502                  ; let mk_new_wanted ev
1503                            = CNonCanonical { cc_id = ev, cc_flavor = fl
1504                                            , cc_depth  = depth + 1 }
1505                  ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
1506                  ; return $
1507                    SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
1508                               , tir_new_item = Stop }
1509                  }
1510 --                              , tir_new_item = ContinueWith solved } } -- Cache in inerts the Solved item
1511
1512 -- Type functions
1513 doTopReact _inerts (CFunEqCan { cc_flavor = fl })
1514   | Just (GivenSolved {}) <- isGiven_maybe fl
1515   = return NoTopInt -- If Solved, no more interactions should happen
1516
1517 -- Otherwise, it's a Given, Derived, or Wanted
1518 doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
1519                                        , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1520   = ASSERT (isSynFamilyTyCon tc)   -- No associated data families have reached that far 
1521     do { match_res <- matchFam tc args   -- See Note [MATCHING-SYNONYMS]
1522        ; case match_res of
1523            Nothing -> return NoTopInt 
1524            Just (famInst, rep_tys)
1525              -> do { let coe_ax = famInstAxiom famInst
1526                          rhs_ty = mkAxInstRHS coe_ax rep_tys
1527                          coe    = mkTcAxInstCo coe_ax rep_tys 
1528                    ; case fl of
1529                        Wanted {} -> do { evc <- newEqVar fl rhs_ty xi -- Wanted version
1530                                        ; let eqv' = evc_the_evvar evc
1531                                        ; let coercion = coe `mkTcTransCo` mkTcCoVarCo eqv'
1532                                        ; _ <- setEqBind eqv coercion fl
1533                                        ; when (isNewEvVar evc) $ 
1534                                             (let ct = CNonCanonical { cc_id = eqv'
1535                                                                     , cc_flavor = fl 
1536                                                                     , cc_depth = cc_depth workItem + 1} 
1537                                              in updWorkListTcS (extendWorkListEq ct))
1538
1539                                        ; let _solved   = workItem { cc_flavor = solved_fl }
1540                                              solved_fl = mkSolvedFlavor fl UnkSkol (EvCoercion coercion)
1541
1542                                        ; updateFlatCache eqv solved_fl tc args xi WhenSolved
1543
1544                                        ; return $ 
1545                                          SomeTopInt { tir_rule = "Fun/Top (solved, more work)"
1546                                                     , tir_new_item = Stop } }
1547                                                   --  , tir_new_item = ContinueWith solved } }
1548                                                      -- Cache in inerts the Solved item
1549
1550                        Given {} -> do { (fl',eqv') <- newGivenEqVar fl xi rhs_ty $ 
1551                                                          mkTcSymCo (mkTcCoVarCo eqv) `mkTcTransCo` coe
1552                                       ; let ct = CNonCanonical { cc_id = eqv'
1553                                                                , cc_flavor = fl'
1554                                                                , cc_depth = cc_depth workItem + 1}  
1555                                       ; updWorkListTcS (extendWorkListEq ct) 
1556                                       ; return $ 
1557                                         SomeTopInt { tir_rule = "Fun/Top (given)"
1558                                                    , tir_new_item = ContinueWith workItem } }
1559                        Derived {} -> do { evc <- newEvVar fl (mkTcEqPred xi rhs_ty)
1560                                         ; let eqv' = evc_the_evvar evc
1561                                         ; when (isNewEvVar evc) $ 
1562                                             (let ct = CNonCanonical { cc_id  = eqv'
1563                                                                  , cc_flavor = fl
1564                                                                  , cc_depth  = cc_depth workItem + 1 } 
1565                                              in updWorkListTcS (extendWorkListEq ct)) 
1566                                         ; return $ 
1567                                           SomeTopInt { tir_rule = "Fun/Top (derived)"
1568                                                      , tir_new_item = Stop } }
1569                    }
1570        }
1571
1572
1573 -- Any other work item does not react with any top-level equations
1574 doTopReact _inerts _workItem = return NoTopInt 
1575 \end{code}
1576
1577
1578 Note [FunDep and implicit parameter reactions] 
1579 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1580 Currently, our story of interacting two dictionaries (or a dictionary
1581 and top-level instances) for functional dependencies, and implicit
1582 paramters, is that we simply produce new wanted equalities.  So for example
1583
1584         class D a b | a -> b where ... 
1585     Inert: 
1586         d1 :g D Int Bool
1587     WorkItem: 
1588         d2 :w D Int alpha
1589
1590     We generate the extra work item
1591         cv :w alpha ~ Bool
1592     where 'cv' is currently unused.  However, this new item reacts with d2,
1593     discharging it in favour of a new constraint d2' thus:
1594         d2' :w D Int Bool
1595         d2 := d2' |> D Int cv
1596     Now d2' can be discharged from d1
1597
1598 We could be more aggressive and try to *immediately* solve the dictionary 
1599 using those extra equalities. With the same inert set and work item we
1600 might dischard d2 directly:
1601
1602         cv :w alpha ~ Bool
1603         d2 := d1 |> D Int cv
1604
1605 But in general it's a bit painful to figure out the necessary coercion,
1606 so we just take the first approach. Here is a better example. Consider:
1607     class C a b c | a -> b 
1608 And: 
1609      [Given]  d1 : C T Int Char 
1610      [Wanted] d2 : C T beta Int 
1611 In this case, it's *not even possible* to solve the wanted immediately. 
1612 So we should simply output the functional dependency and add this guy
1613 [but NOT its superclasses] back in the worklist. Even worse: 
1614      [Given] d1 : C T Int beta 
1615      [Wanted] d2: C T beta Int 
1616 Then it is solvable, but its very hard to detect this on the spot. 
1617
1618 It's exactly the same with implicit parameters, except that the
1619 "aggressive" approach would be much easier to implement.
1620
1621
1622 Note [When improvement happens]
1623 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1624 We fire an improvement rule when
1625
1626   * Two constraints match (modulo the fundep)
1627       e.g. C t1 t2, C t1 t3    where C a b | a->b
1628     The two match because the first arg is identical
1629
1630   * At least one is not Given.  If they are both given, we don't fire
1631     the reaction because we have no way of constructing evidence for a
1632     new equality nor does it seem right to create a new wanted goal
1633     (because the goal will most likely contain untouchables, which
1634     can't be solved anyway)!
1635    
1636 Note that we *do* fire the improvement if one is Given and one is Derived.
1637 The latter can be a superclass of a wanted goal. Example (tcfail138)
1638     class L a b | a -> b
1639     class (G a, L a b) => C a b
1640
1641     instance C a b' => G (Maybe a)
1642     instance C a b  => C (Maybe a) a
1643     instance L (Maybe a) a
1644
1645 When solving the superclasses of the (C (Maybe a) a) instance, we get
1646   Given:  C a b  ... and hance by superclasses, (G a, L a b)
1647   Wanted: G (Maybe a)
1648 Use the instance decl to get
1649   Wanted: C a b'
1650 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1651 and now we need improvement between that derived superclass an the Given (L a b)
1652
1653 Note [Overriding implicit parameters]
1654 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1655 Consider
1656    f :: (?x::a) -> Bool -> a
1657   
1658    g v = let ?x::Int = 3 
1659          in (f v, let ?x::Bool = True in f v)
1660
1661 This should probably be well typed, with
1662    g :: Bool -> (Int, Bool)
1663
1664 So the inner binding for ?x::Bool *overrides* the outer one.
1665 Hence a work-item Given overrides an inert-item Given.
1666
1667 Note [Given constraint that matches an instance declaration]
1668 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1669 What should we do when we discover that one (or more) top-level 
1670 instances match a given (or solved) class constraint? We have 
1671 two possibilities:
1672
1673   1. Reject the program. The reason is that there may not be a unique
1674      best strategy for the solver. Example, from the OutsideIn(X) paper:
1675        instance P x => Q [x] 
1676        instance (x ~ y) => R [x] y 
1677      
1678        wob :: forall a b. (Q [b], R b a) => a -> Int 
1679
1680        g :: forall a. Q [a] => [a] -> Int 
1681        g x = wob x 
1682
1683        will generate the impliation constraint: 
1684             Q [a] => (Q [beta], R beta [a]) 
1685        If we react (Q [beta]) with its top-level axiom, we end up with a 
1686        (P beta), which we have no way of discharging. On the other hand, 
1687        if we react R beta [a] with the top-level we get  (beta ~ a), which 
1688        is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is 
1689        now solvable by the given Q [a]. 
1690  
1691      However, this option is restrictive, for instance [Example 3] from 
1692      Note [Recursive instances and superclases] will fail to work. 
1693
1694   2. Ignore the problem, hoping that the situations where there exist indeed
1695      such multiple strategies are rare: Indeed the cause of the previous 
1696      problem is that (R [x] y) yields the new work (x ~ y) which can be 
1697      *spontaneously* solved, not using the givens. 
1698
1699 We are choosing option 2 below but we might consider having a flag as well.
1700
1701
1702 Note [New Wanted Superclass Work] 
1703 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1704 Even in the case of wanted constraints, we may add some superclasses 
1705 as new given work. The reason is: 
1706
1707         To allow FD-like improvement for type families. Assume that 
1708         we have a class 
1709              class C a b | a -> b 
1710         and we have to solve the implication constraint: 
1711              C a b => C a beta 
1712         Then, FD improvement can help us to produce a new wanted (beta ~ b) 
1713
1714         We want to have the same effect with the type family encoding of 
1715         functional dependencies. Namely, consider: 
1716              class (F a ~ b) => C a b 
1717         Now suppose that we have: 
1718                given: C a b 
1719                wanted: C a beta 
1720         By interacting the given we will get given (F a ~ b) which is not 
1721         enough by itself to make us discharge (C a beta). However, we 
1722         may create a new derived equality from the super-class of the
1723         wanted constraint (C a beta), namely derived (F a ~ beta). 
1724         Now we may interact this with given (F a ~ b) to get: 
1725                   derived :  beta ~ b 
1726         But 'beta' is a touchable unification variable, and hence OK to 
1727         unify it with 'b', replacing the derived evidence with the identity. 
1728
1729         This requires trySpontaneousSolve to solve *derived*
1730         equalities that have a touchable in their RHS, *in addition*
1731         to solving wanted equalities.
1732
1733 We also need to somehow use the superclasses to quantify over a minimal, 
1734 constraint see note [Minimize by Superclasses] in TcSimplify.
1735
1736
1737 Finally, here is another example where this is useful. 
1738
1739 Example 1:
1740 ----------
1741    class (F a ~ b) => C a b 
1742 And we are given the wanteds:
1743       w1 : C a b 
1744       w2 : C a c 
1745       w3 : b ~ c 
1746 We surely do *not* want to quantify over (b ~ c), since if someone provides
1747 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof 
1748 of (b ~ c), hence no extra evidence is necessary. Here is what will happen: 
1749
1750      Step 1: We will get new *given* superclass work, 
1751              provisionally to our solving of w1 and w2
1752              
1753                g1: F a ~ b, g2 : F a ~ c, 
1754                w1 : C a b, w2 : C a c, w3 : b ~ c
1755
1756              The evidence for g1 and g2 is a superclass evidence term: 
1757
1758                g1 := sc w1, g2 := sc w2
1759
1760      Step 2: The givens will solve the wanted w3, so that 
1761                w3 := sym (sc w1) ; sc w2 
1762                   
1763      Step 3: Now, one may naively assume that then w2 can be solve from w1
1764              after rewriting with the (now solved equality) (b ~ c). 
1765              
1766              But this rewriting is ruled out by the isGoodRectDict! 
1767
1768 Conclusion, we will (correctly) end up with the unsolved goals 
1769     (C a b, C a c)   
1770
1771 NB: The desugarer needs be more clever to deal with equalities 
1772     that participate in recursive dictionary bindings. 
1773
1774 \begin{code}
1775 data LookupInstResult
1776   = NoInstance
1777   | GenInst [EvVar] EvTerm 
1778
1779 matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1780 matchClassInst inerts clas tys loc
1781    = do { let pred = mkClassPred clas tys 
1782         ; mb_result <- matchClass clas tys
1783         ; untch <- getUntouchables
1784         ; case mb_result of
1785             MatchInstNo   -> return NoInstance
1786             MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1787                                                -- we learn more about the reagent 
1788             MatchInstSingle (_,_)
1789               | given_overlap untch -> 
1790                   do { traceTcS "Delaying instance application" $ 
1791                        vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
1792                             , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
1793                      ; return NoInstance -- see Note [Instance and Given overlap]
1794                      }
1795
1796             MatchInstSingle (dfun_id, mb_inst_tys) ->
1797               do { checkWellStagedDFun pred dfun_id loc
1798
1799         -- It's possible that not all the tyvars are in
1800         -- the substitution, tenv. For example:
1801         --      instance C X a => D X where ...
1802         -- (presumably there's a functional dependency in class C)
1803         -- Hence mb_inst_tys :: Either TyVar TcType 
1804
1805                  ; tys <- instDFunTypes mb_inst_tys
1806                  ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1807                  ; if null theta then
1808                        return (GenInst [] (EvDFunApp dfun_id tys []))
1809                    else do
1810                      { evc_vars <- instDFunConstraints theta (Wanted loc)
1811                      ; let ev_vars = map evc_the_evvar evc_vars
1812                            new_ev_vars = [evc_the_evvar evc | evc <- evc_vars, isNewEvVar evc]
1813                            -- new_ev_vars are only the real new variables that can be emitted 
1814                      ; return $ GenInst new_ev_vars (EvDFunApp dfun_id tys ev_vars) }
1815                  }
1816         }
1817    where 
1818      givens_for_this_clas :: Cts
1819      givens_for_this_clas 
1820          = lookupUFM (cts_given (inert_dicts inerts)) clas `orElse` emptyCts
1821
1822      given_overlap :: TcsUntouchables -> Bool
1823      given_overlap untch = anyBag (matchable untch) givens_for_this_clas
1824
1825      matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_flavor = fl })
1826        | Just GivenOrig <- isGiven_maybe fl
1827        = ASSERT( clas_g == clas )
1828          case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv && 
1829                                     tv `elemVarSet` tyVarsOfTypes tys
1830                                  then BindMe else Skolem) tys sys of
1831        -- We can't learn anything more about any variable at this point, so the only
1832        -- cause of overlap can be by an instantiation of a touchable unification
1833        -- variable. Hence we only bind touchable unification variables. In addition,
1834        -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
1835             Nothing -> False
1836             Just _  -> True
1837        | otherwise = False -- No overlap with a solved, already been taken care of 
1838                            -- by the overlap check with the instance environment.
1839      matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
1840 \end{code}
1841
1842 Note [Instance and Given overlap]
1843 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1844 Assume that we have an inert set that looks as follows:
1845        [Given] D [Int]
1846 And an instance declaration: 
1847        instance C a => D [a]
1848 A new wanted comes along of the form: 
1849        [Wanted] D [alpha]
1850
1851 One possibility is to apply the instance declaration which will leave us 
1852 with an unsolvable goal (C alpha). However, later on a new constraint may 
1853 arise (for instance due to a functional dependency between two later dictionaries), 
1854 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha]) 
1855 will be transformed to [Wanted] D [Int], which could have been discharged by the given. 
1856
1857 The solution is that in matchClassInst and eventually in topReact, we get back with 
1858 a matching instance, only when there is no Given in the inerts which is unifiable to
1859 this particular dictionary.
1860
1861 The end effect is that, much as we do for overlapping instances, we delay choosing a 
1862 class instance if there is a possibility of another instance OR a given to match our 
1863 constraint later on. This fixes bugs #4981 and #5002.
1864
1865 This is arguably not easy to appear in practice due to our aggressive prioritization 
1866 of equality solving over other constraints, but it is possible. I've added a test case 
1867 in typecheck/should-compile/GivenOverlapping.hs
1868
1869 Moreover notice that our goals here are different than the goals of the top-level 
1870 overlapping checks. There we are interested in validating the following principle:
1871  
1872     If we inline a function f at a site where the same global instance environment
1873     is available as the instance environment at the definition site of f then we 
1874     should get the same behaviour. 
1875
1876 But for the Given Overlap check our goal is just related to completeness of 
1877 constraint solving. 
1878
1879
1880
1881