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