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