b87c5bda337f558d139c2452a383ee851d0dadba
[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://ghc.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 import BasicTypes ()
17 import TcCanonical
18 import VarSet
19 import Type
20 import Unify
21 import FamInst(TcBuiltInSynFamily(..))
22 import InstEnv( lookupInstEnv, instanceDFunId )
23
24 import Var
25 import TcType
26 import PrelNames (knownNatClassName, knownSymbolClassName, ipClassNameKey )
27 import TysWiredIn ( coercibleClass )
28 import Id( idType )
29 import Class
30 import TyCon
31 import DataCon
32 import Name
33 import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as,
34                  is_decl, Provenance(Imported), gre_prov )
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 Data.Maybe ( catMaybes, mapMaybe )
50
51 import VarEnv
52
53 import Control.Monad( when, unless )
54 import Pair (Pair(..))
55 import Unique( hasKey )
56 import UniqFM
57 import FastString ( sLit ) 
58 import DynFlags
59 import Util
60 \end{code}
61 **********************************************************************
62 *                                                                    * 
63 *                      Main Interaction Solver                       *
64 *                                                                    *
65 **********************************************************************
66
67 Note [Basic Simplifier Plan] 
68 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
69
70 1. Pick an element from the WorkList if there exists one with depth 
71    less thanour context-stack depth. 
72
73 2. Run it down the 'stage' pipeline. Stages are: 
74       - canonicalization
75       - inert reactions
76       - spontaneous reactions
77       - top-level intreactions
78    Each stage returns a StopOrContinue and may have sideffected 
79    the inerts or worklist.
80   
81    The threading of the stages is as follows: 
82       - If (Stop) is returned by a stage then we start again from Step 1. 
83       - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to 
84         the next stage in the pipeline. 
85 4. If the element has survived (i.e. ContinueWith x) the last stage 
86    then we add him in the inerts and jump back to Step 1.
87
88 If in Step 1 no such element exists, we have exceeded our context-stack 
89 depth and will simply fail.
90 \begin{code}
91 solveInteractGiven :: CtLoc -> [TcTyVar] -> [EvVar] -> TcS ()
92 -- In principle the givens can kick out some wanteds from the inert
93 -- resulting in solving some more wanted goals here which could emit
94 -- implications. That's why I return a bag of implications. Not sure
95 -- if this can happen in practice though.
96 solveInteractGiven loc fsks givens
97   = do { implics <- solveInteract (fsk_bag `unionBags` given_bag)
98        ; ASSERT( isEmptyBag implics )
99          return () }  -- We do not decompose *given* polymorphic equalities
100                       --    (forall a. t1 ~ forall a. t2)
101                       -- What would the evidence look like?!
102                       -- See Note [Do not decompose given polytype equalities]
103                       -- in TcCanonical
104   where 
105     given_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvId ev_id
106                                                          , ctev_pred = evVarPred ev_id }
107                           | ev_id <- givens ]
108
109     fsk_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvCoercion (mkTcReflCo tv_ty)
110                                                        , ctev_pred = pred  }
111                         | tv <- fsks
112                         , let FlatSkol fam_ty = tcTyVarDetails tv
113                               tv_ty = mkTyVarTy tv
114                               pred  = mkTcEqPred fam_ty tv_ty
115                         ]
116
117 -- The main solver loop implements Note [Basic Simplifier Plan]
118 ---------------------------------------------------------------
119 solveInteract :: Cts -> TcS (Bag Implication)
120 -- Returns the final InertSet in TcS
121 -- Has no effect on work-list or residual-iplications
122 solveInteract cts
123   = {-# SCC "solveInteract" #-}
124     withWorkList cts $
125     do { dyn_flags <- getDynFlags
126        ; solve_loop (ctxtStkDepth dyn_flags) }
127   where
128     solve_loop max_depth
129       = {-# SCC "solve_loop" #-}
130         do { sel <- selectNextWorkItem max_depth
131            ; case sel of 
132               NoWorkRemaining     -- Done, successfuly (modulo frozen)
133                 -> return ()
134               MaxDepthExceeded ct -- Failure, depth exceeded
135                 -> wrapErrTcS $ solverDepthErrorTcS ct
136               NextWorkItem ct     -- More work, loop around!
137                 -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
138
139 type WorkItem = Ct
140 type SimplifierStage = WorkItem -> TcS StopOrContinue
141
142 continueWith :: WorkItem -> TcS StopOrContinue
143 continueWith work_item = return (ContinueWith work_item) 
144
145 data SelectWorkItem 
146        = NoWorkRemaining      -- No more work left (effectively we're done!)
147        | MaxDepthExceeded Ct  -- More work left to do but this constraint has exceeded
148                               -- the max subgoal depth and we must stop 
149        | NextWorkItem Ct      -- More work left, here's the next item to look at 
150
151 selectNextWorkItem :: SubGoalDepth -- Max depth allowed
152                    -> TcS SelectWorkItem
153 selectNextWorkItem max_depth
154   = updWorkListTcS_return pick_next
155   where 
156     pick_next :: WorkList -> (SelectWorkItem, WorkList)
157     pick_next wl 
158       = case selectWorkItem wl of
159           (Nothing,_) 
160               -> (NoWorkRemaining,wl)           -- No more work
161           (Just ct, new_wl) 
162               | ctLocDepth (cc_loc ct) > max_depth  -- Depth exceeded
163               -> (MaxDepthExceeded ct,new_wl)
164           (Just ct, new_wl) 
165               -> (NextWorkItem ct, new_wl)      -- New workitem and worklist
166
167 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline 
168                   -> WorkItem                   -- The work item 
169                   -> TcS () 
170 -- Run this item down the pipeline, leaving behind new work and inerts
171 runSolverPipeline pipeline workItem 
172   = do { initial_is <- getTcSInerts 
173        ; traceTcS "Start solver pipeline {" $ 
174                   vcat [ ptext (sLit "work item = ") <+> ppr workItem 
175                        , ptext (sLit "inerts    = ") <+> ppr initial_is]
176
177        ; bumpStepCountTcS    -- One step for each constraint processed
178        ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
179
180        ; final_is <- getTcSInerts
181        ; case final_res of 
182            Stop            -> do { traceTcS "End solver pipeline (discharged) }" 
183                                        (ptext (sLit "inerts    = ") <+> ppr final_is)
184                                  ; return () }
185            ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert:") <+> ppr ct)
186                                  ; traceTcS "End solver pipeline (not discharged) }" $
187                                        vcat [ ptext (sLit "final_item = ") <+> ppr ct
188                                             , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
189                                             , ptext (sLit "inerts     = ") <+> ppr final_is]
190                                  ; insertInertItemTcS ct }
191        }
192   where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
193         run_pipeline [] res = return res 
194         run_pipeline _ Stop = return Stop 
195         run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
196           = do { traceTcS ("runStage " ++ stg_name ++ " {")
197                           (text "workitem   = " <+> ppr ct) 
198                ; res <- stg ct 
199                ; traceTcS ("end stage " ++ stg_name ++ " }") empty
200                ; run_pipeline stgs res 
201                }
202 \end{code}
203
204 Example 1:
205   Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
206   Reagent: a ~ [b] (given)
207
208 React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
209 React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
210 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []
211
212 Example 2:
213   Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
214   Reagent: a ~w [b]
215
216 React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
217 React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
218 etc.
219
220 Example 3:
221   Inert:  {a ~ Int, F Int ~ b} (given)
222   Reagent: F a ~ b (wanted)
223
224 React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
225 React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing
226
227 \begin{code}
228 thePipeline :: [(String,SimplifierStage)]
229 thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
230               , ("spontaneous solve",       spontaneousSolveStage)
231               , ("interact with inerts",    interactWithInertsStage)
232               , ("top-level reactions",     topReactionsStage) ]
233 \end{code}
234
235
236 *********************************************************************************
237 *                                                                               * 
238                        The spontaneous-solve Stage
239 *                                                                               *
240 *********************************************************************************
241
242 \begin{code}
243 spontaneousSolveStage :: SimplifierStage 
244 -- CTyEqCans are always consumed, returning Stop
245 spontaneousSolveStage workItem
246   = do { mb_solved <- trySpontaneousSolve workItem
247        ; case mb_solved of
248            SPCantSolve
249               | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = fl } <- workItem
250               -- Unsolved equality
251               -> do { untch <- getUntouchables
252                     ; traceTcS "Can't solve tyvar equality" 
253                           (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
254                                 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
255                                 , text "Untouchables =" <+> ppr untch ])
256                     ; n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
257                     ; traceFireTcS workItem $
258                       ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon 
259                       <+> ppr workItem
260                     ; insertInertItemTcS workItem
261                     ; return Stop }
262               | otherwise
263               -> continueWith workItem
264
265            SPSolved new_tv
266               -- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
267               -- see Note [Spontaneously solved in TyBinds]
268               -> do { n_kicked <- kickOutRewritable Given new_tv
269                     ; traceFireTcS workItem $
270                       ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked <> colon 
271                       <+> ppr workItem
272                     ; return Stop } }
273
274 ppr_kicked :: Int -> SDoc
275 ppr_kicked 0 = empty
276 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out")) 
277 \end{code}
278 Note [Spontaneously solved in TyBinds]
279 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
280 When we encounter a constraint ([W] alpha ~ tau) which can be spontaneously solved,
281 we record the equality on the TyBinds of the TcSMonad. In the past, we used to also
282 add a /given/ version of the constraint ([G] alpha ~ tau) to the inert
283 canonicals -- and potentially kick out other equalities that mention alpha.
284
285 Then, the flattener only had to look in the inert equalities during flattening of a
286 type (TcCanonical.flattenTyVar).
287
288 However it is a bit silly to record these equalities /both/ in the inerts AND the
289 TyBinds, so we have now eliminated spontaneously solved equalities from the inerts,
290 and only record them in the TyBinds of the TcS monad. The flattener is now consulting
291 these binds /and/ the inerts for potentially unsolved or other given equalities.
292
293 \begin{code}
294 kickOutRewritable :: CtFlavour    -- Flavour of the equality that is 
295                                   -- being added to the inert set
296                   -> TcTyVar      -- The new equality is tv ~ ty
297                   -> TcS Int
298 kickOutRewritable new_flav new_tv
299   = do { wl <- modifyInertTcS kick_out
300        ; traceTcS "kickOutRewritable" $ 
301             vcat [ text "tv = " <+> ppr new_tv  
302                  , ptext (sLit "Kicked out =") <+> ppr wl]
303        ; updWorkListTcS (appendWorkList wl)
304        ; return (workListSize wl)  }
305   where
306     kick_out :: InertSet -> (WorkList, InertSet)
307     kick_out (is@(IS { inert_cans = IC { inert_eqs = tv_eqs
308                      , inert_dicts  = dictmap
309                      , inert_funeqs = funeqmap
310                      , inert_irreds = irreds
311                      , inert_insols = insols } }))
312        = (kicked_out, is { inert_cans = inert_cans_in })
313                 -- NB: Notice that don't rewrite 
314                 -- inert_solved_dicts, and inert_solved_funeqs
315                 -- optimistically. But when we lookup we have to take the 
316                 -- subsitution into account
317        where
318          inert_cans_in = IC { inert_eqs = tv_eqs_in
319                             , inert_dicts = dicts_in
320                             , inert_funeqs = feqs_in
321                             , inert_irreds = irs_in
322                             , inert_insols = insols_in }
323
324          kicked_out = WorkList { wl_eqs    = varEnvElts tv_eqs_out
325                                , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
326                                , wl_rest   = bagToList (dicts_out `andCts` irs_out 
327                                                         `andCts` insols_out) }
328   
329          (tv_eqs_out,  tv_eqs_in) = partitionVarEnv  kick_out_eq tv_eqs
330          (feqs_out,   feqs_in)    = partCtFamHeadMap kick_out_ct funeqmap
331          (dicts_out,  dicts_in)   = partitionCCanMap kick_out_ct dictmap
332          (irs_out,    irs_in)     = partitionBag     kick_out_ct irreds
333          (insols_out, insols_in)  = partitionBag     kick_out_ct insols
334            -- Kick out even insolubles; see Note [Kick out insolubles]
335
336     kick_out_ct inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
337                           (new_tv `elemVarSet` tyVarsOfCt inert_ct) 
338                     -- NB: tyVarsOfCt will return the type 
339                     --     variables /and the kind variables/ that are 
340                     --     directly visible in the type. Hence we will
341                     --     have exposed all the rewriting we care about
342                     --     to make the most precise kinds visible for 
343                     --     matching classes etc. No need to kick out 
344                     --     constraints that mention type variables whose
345                     --     kinds could contain this variable!
346
347     kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = ev })
348       =  (new_flav `canRewrite` inert_flav)  -- See Note [Delicate equality kick-out]
349       && (new_tv `elemVarSet` kind_vars ||              -- (1)
350           (not (inert_flav `canRewrite` new_flav) &&    -- (2)
351            new_tv `elemVarSet` (extendVarSet (tyVarsOfType rhs) tv)))
352       where
353         inert_flav = ctEvFlavour ev
354         kind_vars = tyVarsOfType (tyVarKind tv) `unionVarSet`
355                     tyVarsOfType (typeKind rhs)
356
357     kick_out_eq other_ct = pprPanic "kick_out_eq" (ppr other_ct)
358 \end{code}
359
360 Note [Kick out insolubles]
361 ~~~~~~~~~~~~~~~~~~~~~~~~~~
362 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
363 because an occurs check.  And then we unify alpha := [Int].  
364 Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
365 Now it can be decomposed.  Otherwise we end up with a "Can't match
366 [Int] ~ [[Int]]" which is true, but a bit confusing because the
367 outer type constructors match. 
368
369 Note [Delicate equality kick-out]
370 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
371 When adding an equality (a ~ xi), we kick out an inert type-variable 
372 equality (b ~ phi) in two cases
373
374 (1) If the new tyvar can rewrite the kind LHS or RHS of the inert
375     equality.  Example:
376     Work item: [W] k ~ *
377     Inert:     [W] (a:k) ~ ty        
378                [W] (b:*) ~ c :: k
379     We must kick out those blocked inerts so that we rewrite them
380     and can subsequently unify.
381
382 (2) If the new tyvar can 
383           Work item:  [G] a ~ b
384           Inert:      [W] b ~ [a]
385     Now at this point the work item cannot be further rewritten by the
386     inert (due to the weaker inert flavor). But we can't add the work item
387     as-is because the inert set would then have a cyclic substitution, 
388     when rewriting a wanted type mentioning 'a'. So we must kick the inert out. 
389
390     We have to do this only if the inert *cannot* rewrite the work item;
391     it it can, then the work item will have been fully rewritten by the 
392     inert during canonicalisation.  So for example:
393          Work item: [W] a ~ Int
394          Inert:     [W] b ~ [a]
395     No need to kick out the inert, beause the inert substitution is not
396     necessarily idemopotent.  See Note [Non-idempotent inert substitution].
397
398 See also point (8) of Note [Detailed InertCans Invariants] 
399
400 \begin{code}
401 data SPSolveResult = SPCantSolve
402                    | SPSolved TcTyVar
403                      -- We solved this /unification/ variable to some type using reflexivity
404
405 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
406 -- SPSolved workItem' gives us a new *given* to go on 
407
408 -- @trySpontaneousSolve wi@ solves equalities where one side is a
409 -- touchable unification variable.
410 --          See Note [Touchables and givens] 
411 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
412 trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
413                                        , cc_tyvar = tv1, cc_rhs = xi, cc_loc = d })
414   | isGiven gw
415   = do { traceTcS "No spontaneous solve for given" (ppr workItem)
416        ; return SPCantSolve }
417   | Just tv2 <- tcGetTyVar_maybe xi
418   = do { tch1 <- isTouchableMetaTyVarTcS tv1
419        ; tch2 <- isTouchableMetaTyVarTcS tv2
420        ; case (tch1, tch2) of
421            (True,  True)  -> trySpontaneousEqTwoWay d gw tv1 tv2
422            (True,  False) -> trySpontaneousEqOneWay d gw tv1 xi
423            (False, True)  -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
424            _              -> return SPCantSolve }
425   | otherwise
426   = do { tch1 <- isTouchableMetaTyVarTcS tv1
427        ; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
428                  else return SPCantSolve }
429
430   -- No need for 
431   --      trySpontaneousSolve (CFunEqCan ...) = ...
432   -- See Note [No touchables as FunEq RHS] in TcSMonad
433 trySpontaneousSolve item = do { traceTcS "Spont: no tyvar on lhs" (ppr item)
434                               ; return SPCantSolve }
435
436 ----------------
437 trySpontaneousEqOneWay :: CtLoc -> CtEvidence 
438                        -> TcTyVar -> Xi -> TcS SPSolveResult
439 -- tv is a MetaTyVar, not untouchable
440 trySpontaneousEqOneWay d gw tv xi
441   | not (isSigTyVar tv) || isTyVarTy xi
442   , typeKind xi `tcIsSubKind` tyVarKind tv
443   = solveWithIdentity d gw tv xi
444   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
445   = return SPCantSolve
446
447 ----------------
448 trySpontaneousEqTwoWay :: CtLoc -> CtEvidence 
449                        -> TcTyVar -> TcTyVar -> TcS SPSolveResult
450 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
451
452 trySpontaneousEqTwoWay d gw tv1 tv2
453   | k1 `tcIsSubKind` k2 && nicer_to_update_tv2
454   = solveWithIdentity d gw tv2 (mkTyVarTy tv1)
455   | k2 `tcIsSubKind` k1
456   = solveWithIdentity d gw tv1 (mkTyVarTy tv2)
457   | otherwise
458   = return SPCantSolve
459   where
460     k1 = tyVarKind tv1
461     k2 = tyVarKind tv2
462     nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
463 \end{code}
464
465 Note [Avoid double unifications] 
466 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
467 The spontaneous solver has to return a given which mentions the unified unification
468 variable *on the left* of the equality. Here is what happens if not: 
469   Original wanted:  (a ~ alpha),  (alpha ~ Int) 
470 We spontaneously solve the first wanted, without changing the order! 
471       given : a ~ alpha      [having unified alpha := a] 
472 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
473 At the end we spontaneously solve that guy, *reunifying*  [alpha := Int] 
474
475 We avoid this problem by orienting the resulting given so that the unification
476 variable is on the left.  [Note that alternatively we could attempt to
477 enforce this at canonicalization]
478
479 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
480 double unifications is the main reason we disallow touchable
481 unification variables as RHS of type family equations: F xis ~ alpha.
482
483 \begin{code}
484 solveWithIdentity :: CtLoc -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
485 -- Solve with the identity coercion 
486 -- Precondition: kind(xi) is a sub-kind of kind(tv)
487 -- Precondition: CtEvidence is Wanted or Derived
488 -- See [New Wanted Superclass Work] to see why solveWithIdentity 
489 --     must work for Derived as well as Wanted
490 -- Returns: workItem where 
491 --        workItem = the new Given constraint
492 --
493 -- NB: No need for an occurs check here, because solveWithIdentity always 
494 --     arises from a CTyEqCan, a *canonical* constraint.  Its invariants
495 --     say that in (a ~ xi), the type variable a does not appear in xi.
496 --     See TcRnTypes.Ct invariants.
497 solveWithIdentity _d wd tv xi 
498   = do { let tv_ty = mkTyVarTy tv
499        ; traceTcS "Sneaky unification:" $ 
500                        vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
501                              text "Coercion:" <+> pprEq tv_ty xi,
502                              text "Left Kind is:" <+> ppr (typeKind tv_ty),
503                              text "Right Kind is:" <+> ppr (typeKind xi) ]
504
505        ; let xi' = defaultKind xi      
506                -- We only instantiate kind unification variables
507                -- with simple kinds like *, not OpenKind or ArgKind
508                -- cf TcUnify.uUnboundKVar
509
510        ; setWantedTyBind tv xi'
511        ; let refl_evtm = EvCoercion (mkTcReflCo xi')
512
513        ; when (isWanted wd) $ 
514               setEvBind (ctev_evar wd) refl_evtm
515
516        ; return (SPSolved tv) }
517 \end{code}
518
519
520 *********************************************************************************
521 *                                                                               * 
522                        The interact-with-inert Stage
523 *                                                                               *
524 *********************************************************************************
525
526 Note [
527
528 Note [The Solver Invariant]
529 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
530 We always add Givens first.  So you might think that the solver has
531 the invariant
532
533    If the work-item is Given, 
534    then the inert item must Given
535
536 But this isn't quite true.  Suppose we have, 
537     c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
538 After processing the first two, we get
539      c1: [G] beta ~ [alpha], c2 : [W] blah
540 Now, c3 does not interact with the the given c1, so when we spontaneously
541 solve c3, we must re-react it with the inert set.  So we can attempt a 
542 reaction between inert c2 [W] and work-item c3 [G].
543
544 It *is* true that [Solver Invariant]
545    If the work-item is Given, 
546    AND there is a reaction
547    then the inert item must Given
548 or, equivalently,
549    If the work-item is Given, 
550    and the inert item is Wanted/Derived
551    then there is no reaction
552
553 \begin{code}
554 -- Interaction result of  WorkItem <~> Ct
555
556 data InteractResult 
557     = IRWorkItemConsumed { ir_fire :: String }    -- Work item discharged by interaction; stop
558     | IRReplace          { ir_fire :: String }    -- Inert item replaced by work item; stop
559     | IRInertConsumed    { ir_fire :: String }    -- Inert item consumed, keep going with work item 
560     | IRKeepGoing        { ir_fire :: String }    -- Inert item remains, keep going with work item
561
562 interactWithInertsStage :: WorkItem -> TcS StopOrContinue 
563 -- Precondition: if the workitem is a CTyEqCan then it will not be able to 
564 -- react with anything at this stage. 
565 interactWithInertsStage wi 
566   = do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
567        ; rels <- extractRelevantInerts wi 
568        ; traceTcS "relevant inerts are:" $ ppr rels
569        ; builtInInteractions
570        ; foldlBagM interact_next (ContinueWith wi) rels }
571
572   where interact_next Stop atomic_inert 
573           = do { insertInertItemTcS atomic_inert; return Stop }
574         interact_next (ContinueWith wi) atomic_inert 
575           = do { ir <- doInteractWithInert atomic_inert wi
576                ; let mk_msg rule keep_doc 
577                        = vcat [ text rule <+> keep_doc
578                               , ptext (sLit "InertItem =") <+> ppr atomic_inert
579                               , ptext (sLit "WorkItem  =") <+> ppr wi ]
580                ; case ir of 
581                    IRWorkItemConsumed { ir_fire = rule } 
582                        -> do { traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
583                              ; insertInertItemTcS atomic_inert
584                              ; return Stop } 
585                    IRReplace { ir_fire = rule }
586                        -> do { traceFireTcS atomic_inert 
587                                             (mk_msg rule (text "InertReplace"))
588                              ; insertInertItemTcS wi
589                              ; return Stop } 
590                    IRInertConsumed { ir_fire = rule }
591                        -> do { traceFireTcS atomic_inert 
592                                             (mk_msg rule (text "InertItemConsumed"))
593                              ; return (ContinueWith wi) }
594                    IRKeepGoing {}
595                        -> do { insertInertItemTcS atomic_inert
596                              ; return (ContinueWith wi) }
597                }
598
599         -- See if we can compute some new derived work for built-ins.
600         builtInInteractions
601           | CFunEqCan { cc_fun = tc, cc_tyargs = args, cc_rhs = xi } <- wi
602           , Just ops <- isBuiltInSynFamTyCon_maybe tc =
603             do is <- getInertsFunEqTyCon tc
604                traceTcS "builtInCandidates: " $ ppr is
605                let interact = sfInteractInert ops args xi
606                impMbs <- sequence
607                  [ do mb <- newDerived (mkTcEqPred lhs rhs)
608                       case mb of
609                         Just x -> return $ Just $ mkNonCanonical d x
610                         Nothing -> return Nothing
611                  | CFunEqCan { cc_tyargs = iargs
612                              , cc_rhs = ixi
613                              , cc_loc = d } <- is
614                  , Pair lhs rhs <- interact iargs ixi
615                  ]
616                let imps = catMaybes impMbs
617                unless (null imps) $ updWorkListTcS (extendWorkListEqs imps)
618           | otherwise = return ()
619
620
621
622
623 \end{code}
624
625 \begin{code}
626 --------------------------------------------
627
628 doInteractWithInert :: Ct -> Ct -> TcS InteractResult
629 -- Identical class constraints.
630 doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1, cc_loc = loc1 })
631                      workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2, cc_loc = loc2 })
632   | cls1 == cls2  
633   = do { let pty1 = mkClassPred cls1 tys1
634              pty2 = mkClassPred cls2 tys2
635              inert_pred_loc     = (pty1, pprArisingAt loc1)
636              work_item_pred_loc = (pty2, pprArisingAt loc2)
637
638        ; let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
639        ; fd_work <- rewriteWithFunDeps fd_eqns loc2
640                 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
641                 -- NB: We do create FDs for given to report insoluble equations that arise
642                 -- from pairs of Givens, and also because of floating when we approximate
643                 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
644                 -- Also see Note [When improvement happens]
645        
646        ; traceTcS "doInteractWithInert:dict" 
647                   (vcat [ text "inertItem =" <+> ppr inertItem
648                         , text "workItem  =" <+> ppr workItem
649                         , text "fundeps =" <+> ppr fd_work ])
650  
651        ; case fd_work of
652            -- No Functional Dependencies 
653            []  | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
654                | otherwise         -> return (IRKeepGoing "NOP")
655
656            -- Actual Functional Dependencies
657            _   | cls1 `hasKey` ipClassNameKey
658                , isGiven fl1, isGiven fl2  -- See Note [Shadowing of Implicit Parameters]
659                -> return (IRReplace ("Replace IP"))
660
661                -- Standard thing: create derived fds and keep on going. Importantly we don't
662                -- throw workitem back in the worklist because this can cause loops. See #5236.
663                | otherwise 
664                -> do { updWorkListTcS (extendWorkListEqs fd_work)
665                      ; return (IRKeepGoing "Cls/Cls (new fundeps)") } -- Just keep going without droping the inert 
666        }
667  
668 -- Two pieces of irreducible evidence: if their types are *exactly identical* 
669 -- we can rewrite them. We can never improve using this: 
670 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not 
671 -- mean that (ty1 ~ ty2)
672 doInteractWithInert (CIrredEvCan { cc_ev = ifl })
673            workItem@(CIrredEvCan { cc_ev = wfl })
674   | ctEvPred ifl `eqType` ctEvPred wfl
675   = solveOneFromTheOther "Irred/Irred" ifl workItem
676
677 doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
678                                   , cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 }) 
679                     wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
680                                   , cc_tyargs = args2, cc_rhs = xi2, cc_loc = d2 })
681   | i_solves_w && (not (w_solves_i && isMetaTyVarTy xi1))
682                -- See Note [Carefully solve the right CFunEqCan]
683   = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
684     do { traceTcS "interact with inerts: FunEq/FunEq" $ 
685          vcat [ text "workItem =" <+> ppr wi
686               , text "inertItem=" <+> ppr ii ]
687
688        ; let xev = XEvTerm xcomp xdecomp
689              -- xcomp : [(xi2 ~ xi1)] -> (F args ~ xi2) 
690              xcomp [x] = EvCoercion (co1 `mkTcTransCo` mk_sym_co x)
691              xcomp _   = panic "No more goals!"
692              -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]                 
693              xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
694
695        ; ctevs <- xCtFlavor ev2 [mkTcEqPred xi2 xi1] xev
696              -- No caching!  See Note [Cache-caused loops]
697              -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
698        ; emitWorkNC d2 ctevs 
699        ; return (IRWorkItemConsumed "FunEq/FunEq") }
700
701   | fl2 `canSolve` fl1
702   = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
703     do { traceTcS "interact with inerts: FunEq/FunEq" $ 
704          vcat [ text "workItem =" <+> ppr wi
705               , text "inertItem=" <+> ppr ii ]
706
707        ; let xev = XEvTerm xcomp xdecomp
708               -- xcomp : [(xi2 ~ xi1)] -> [(F args ~ xi1)]
709              xcomp [x] = EvCoercion (co2 `mkTcTransCo` evTermCoercion x)
710              xcomp _ = panic "No more goals!"
711              -- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
712              xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
713
714        ; ctevs <- xCtFlavor ev1 [mkTcEqPred xi2 xi1] xev 
715              -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
716
717        ; emitWorkNC d1 ctevs 
718        ; return (IRInertConsumed "FunEq/FunEq") }
719   where
720     lhss_match = tc1 == tc2 && eqTypes args1 args2 
721     co1 = evTermCoercion $ ctEvTerm ev1
722     co2 = evTermCoercion $ ctEvTerm ev2
723     mk_sym_co x = mkTcSymCo (evTermCoercion x)
724     fl1 = ctEvFlavour ev1
725     fl2 = ctEvFlavour ev2
726
727     i_solves_w = fl1 `canSolve` fl2 
728     w_solves_i = fl2 `canSolve` fl1 
729     
730
731 doInteractWithInert _ _ = return (IRKeepGoing "NOP")
732 \end{code}
733
734 Note [Efficient Orientation] 
735 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
736 Suppose we are interacting two FunEqCans with the same LHS:
737           (inert)  ci :: (F ty ~ xi_i) 
738           (work)   cw :: (F ty ~ xi_w) 
739 We prefer to keep the inert (else we pass the work item on down
740 the pipeline, which is a bit silly).  If we keep the inert, we
741 will (a) discharge 'cw' 
742      (b) produce a new equality work-item (xi_w ~ xi_i)
743 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
744     new_work :: xi_w ~ xi_i
745     cw := ci ; sym new_work
746 Why?  Consider the simplest case when xi1 is a type variable.  If
747 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
748 If we generate xi2~xi1, there is less chance of that happening.
749 Of course it can and should still happen if xi1=a, xi1=Int, say.
750 But we want to avoid it happening needlessly.
751
752 Similarly, if we *can't* keep the inert item (because inert is Wanted,
753 and work is Given, say), we prefer to orient the new equality (xi_i ~
754 xi_w).
755
756 Note [Carefully solve the right CFunEqCan]
757 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
758 Consider the constraints
759   c1 :: F Int ~ a      -- Arising from an application line 5
760   c2 :: F Int ~ Bool   -- Arising from an application line 10
761 Suppose that 'a' is a unification variable, arising only from 
762 flattening.  So there is no error on line 5; it's just a flattening
763 variable.  But there is (or might be) an error on line 10.
764
765 Two ways to combine them, leaving either (Plan A)
766   c1 :: F Int ~ a      -- Arising from an application line 5
767   c3 :: a ~ Bool       -- Arising from an application line 10
768 or (Plan B)
769   c2 :: F Int ~ Bool   -- Arising from an application line 10
770   c4 :: a ~ Bool       -- Arising from an application line 5
771
772 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
773 on the *totally innocent* line 5.  An example is test SimpleFail16
774 where the expected/actual message comes out backwards if we use
775 the wrong plan.
776
777 The second is the right thing to do.  Hence the isMetaTyVarTy
778 test when solving pairwise CFunEqCan.
779
780 Note [Shadowing of Implicit Parameters]
781 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
782
783 Consider the following example:
784
785 f :: (?x :: Char) => Char
786 f = let ?x = 'a' in ?x
787
788 The "let ?x = ..." generates an implication constraint of the form:
789
790 ?x :: Char => ?x :: Char
791
792 Furthermore, the signature for `f` also generates an implication
793 constraint, so we end up with the following nested implication:
794
795 ?x :: Char => (?x :: Char => ?x :: Char)
796
797 Note that the wanted (?x :: Char) constraint may be solved in
798 two incompatible ways:  either by using the parameter from the
799 signature, or by using the local definition.  Our intention is
800 that the local definition should "shadow" the parameter of the
801 signature, and we implement this as follows: when we add a new
802 given implicit parameter to the inert set, it replaces any existing
803 givens for the same implicit parameter.
804
805 This works for the normal cases but it has an odd side effect
806 in some pathological programs like this:
807
808 -- This is accepted, the second parameter shadows
809 f1 :: (?x :: Int, ?x :: Char) => Char
810 f1 = ?x
811
812 -- This is rejected, the second parameter shadows
813 f2 :: (?x :: Int, ?x :: Char) => Int
814 f2 = ?x
815
816 Both of these are actually wrong:  when we try to use either one,
817 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
818 which would lead to an error.
819
820 I can think of two ways to fix this:
821
822   1. Simply disallow multiple constratits for the same implicit
823     parameter---this is never useful, and it can be detected completely
824     syntactically.
825
826   2. Move the shadowing machinery to the location where we nest
827      implications, and add some code here that will produce an
828      error if we get multiple givens for the same implicit parameter.
829
830
831 Note [Cache-caused loops]
832 ~~~~~~~~~~~~~~~~~~~~~~~~~
833 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our 
834 solved cache (which is the default behaviour or xCtFlavor), because the interaction 
835 may not be contributing towards a solution. Here is an example:
836
837 Initial inert set:
838   [W] g1 : F a ~ beta1
839 Work item:
840   [W] g2 : F a ~ beta2
841 The work item will react with the inert yielding the _same_ inert set plus:
842     i)   Will set g2 := g1 `cast` g3   
843     ii)  Will add to our solved cache that [S] g2 : F a ~ beta2
844     iii) Will emit [W] g3 : beta1 ~ beta2 
845 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
846 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it 
847 will set 
848       g1 := g ; sym g3 
849 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
850 remember that we have this in our solved cache, and it is ... g2! In short we 
851 created the evidence loop:
852
853         g2 := g1 ; g3 
854         g3 := refl
855         g1 := g2 ; sym g3 
856
857 To avoid this situation we do not cache as solved any workitems (or inert) 
858 which did not really made a 'step' towards proving some goal. Solved's are 
859 just an optimization so we don't lose anything in terms of completeness of 
860 solving.
861
862 \begin{code}
863 solveOneFromTheOther :: String    -- Info 
864                      -> CtEvidence  -- Inert 
865                      -> Ct        -- WorkItem 
866                      -> TcS InteractResult
867 -- Preconditions: 
868 -- 1) inert and work item represent evidence for the /same/ predicate
869 -- 2) ip/class/irred evidence (no coercions) only
870 solveOneFromTheOther info ifl workItem
871   | isDerived wfl
872   = return (IRWorkItemConsumed ("Solved[DW] " ++ info))
873
874   | isDerived ifl -- The inert item is Derived, we can just throw it away, 
875                   -- The workItem is inert wrt earlier inert-set items, 
876                   -- so it's safe to continue on from this point
877   = return (IRInertConsumed ("Solved[DI] " ++ info))
878   
879   | CtWanted { ctev_evar = ev_id } <- wfl
880   = do { setEvBind ev_id (ctEvTerm ifl); return (IRWorkItemConsumed ("Solved(w) " ++ info)) }
881
882   | CtWanted { ctev_evar = ev_id } <- ifl
883   = do { setEvBind ev_id (ctEvTerm wfl); return (IRInertConsumed ("Solved(g) " ++ info)) }
884
885   | otherwise      -- If both are Given, we already have evidence; no need to duplicate
886                    -- But the work item *overrides* the inert item (hence IRReplace)
887                    -- See Note [Shadowing of Implicit Parameters]
888   = return (IRReplace ("Replace(gg) " ++ info))
889   where 
890      wfl = cc_ev workItem
891 \end{code}
892
893 Note [Shadowing of Implicit Parameters]
894 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
895 Consider the following example:
896
897 f :: (?x :: Char) => Char
898 f = let ?x = 'a' in ?x
899
900 The "let ?x = ..." generates an implication constraint of the form:
901
902 ?x :: Char => ?x :: Char
903
904
905 Furthermore, the signature for `f` also generates an implication
906 constraint, so we end up with the following nested implication:
907
908 ?x :: Char => (?x :: Char => ?x :: Char)
909
910 Note that the wanted (?x :: Char) constraint may be solved in
911 two incompatible ways:  either by using the parameter from the
912 signature, or by using the local definition.  Our intention is
913 that the local definition should "shadow" the parameter of the
914 signature, and we implement this as follows: when we nest implications,
915 we remove any implicit parameters in the outer implication, that
916 have the same name as givens of the inner implication.
917
918 Here is another variation of the example:
919
920 f :: (?x :: Int) => Char
921 f = let ?x = 'x' in ?x
922
923 This program should also be accepted: the two constraints `?x :: Int`
924 and `?x :: Char` never exist in the same context, so they don't get to
925 interact to cause failure.
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  topReactionsStage, 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 because 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] -> CtLoc -> TcS [Ct] 
1292 -- NB: The returned constraints are all Derived
1293 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1294 rewriteWithFunDeps eqn_pred_locs loc
1295  = do { fd_cts <- mapM (instFunDepEqn loc) eqn_pred_locs
1296       ; return (concat fd_cts) }
1297
1298 instFunDepEqn :: CtLoc -> Equation -> TcS [Ct]
1299 -- Post: Returns the position index as well as the corresponding FunDep equality
1300 instFunDepEqn loc (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
1301                          , fd_pred1 = d1, fd_pred2 = d2 })
1302   = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
1303        ; foldM (do_one subst) [] eqs }
1304   where 
1305     der_loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1306
1307     do_one subst ievs (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
1308        | eqType sty1 sty2 
1309        = return ievs -- Return no trivial equalities
1310        | otherwise
1311        = do { mb_eqv <- newDerived (mkTcEqPred sty1 sty2)
1312             ; case mb_eqv of
1313                  Just ev -> return (mkNonCanonical der_loc ev : ievs)
1314                  Nothing -> return ievs }
1315                    -- We are eventually going to emit FD work back in the work list so 
1316                    -- it is important that we only return the /freshly created/ and not 
1317                    -- some existing equality!
1318        where
1319          sty1 = Type.substTy subst ty1 
1320          sty2 = Type.substTy subst ty2 
1321
1322 mkEqnMsg :: (TcPredType, SDoc) 
1323          -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
1324 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1325   = do  { zpred1 <- zonkTcPredType pred1
1326         ; zpred2 <- zonkTcPredType pred2
1327         ; let { tpred1 = tidyType tidy_env zpred1
1328               ; tpred2 = tidyType tidy_env zpred2 }
1329         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1330                           nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
1331                           nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1332         ; return (tidy_env, msg) }
1333 \end{code}
1334
1335
1336
1337
1338 *********************************************************************************
1339 *                                                                               * 
1340                        The top-reaction Stage
1341 *                                                                               *
1342 *********************************************************************************
1343
1344 \begin{code}
1345 topReactionsStage :: WorkItem -> TcS StopOrContinue
1346 topReactionsStage wi 
1347  = do { inerts <- getTcSInerts
1348       ; tir <- doTopReact inerts wi
1349       ; case tir of 
1350           NoTopInt -> return (ContinueWith wi)
1351           SomeTopInt rule what_next 
1352                    -> do { traceFireTcS wi $
1353                            vcat [ ptext (sLit "Top react:") <+> text rule
1354                                 , text "WorkItem =" <+> ppr wi ]
1355                          ; return what_next } }
1356
1357 data TopInteractResult 
1358  = NoTopInt
1359  | SomeTopInt { tir_rule :: String, tir_new_item :: StopOrContinue }
1360
1361
1362 doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1363 -- The work item does not react with the inert set, so try interaction with top-level 
1364 -- instances. Note:
1365 --
1366 --   (a) The place to add superclasses in not here in doTopReact stage. 
1367 --       Instead superclasses are added in the worklist as part of the
1368 --       canonicalization process. See Note [Adding superclasses].
1369 --
1370 --   (b) See Note [Given constraint that matches an instance declaration] 
1371 --       for some design decisions for given dictionaries. 
1372
1373 doTopReact inerts workItem
1374   = do { traceTcS "doTopReact" (ppr workItem)
1375        ; case workItem of
1376            CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
1377                     , cc_loc = d }
1378               -> doTopReactDict inerts fl cls xis d
1379
1380            CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
1381                      , cc_rhs = xi, cc_loc = d }
1382               -> doTopReactFunEq workItem fl tc args xi d
1383
1384            _  -> -- Any other work item does not react with any top-level equations
1385                  return NoTopInt  }
1386
1387 --------------------
1388 doTopReactDict :: InertSet -> CtEvidence -> Class -> [Xi]
1389                -> CtLoc -> TcS TopInteractResult
1390 doTopReactDict inerts fl cls xis loc
1391   | not (isWanted fl)
1392   = try_fundeps_and_return
1393
1394   | Just ev <- lookupSolvedDict inerts pred   -- Cached
1395   = do { setEvBind dict_id (ctEvTerm ev); 
1396        ; return $ SomeTopInt { tir_rule = "Dict/Top (cached)" 
1397                              , tir_new_item = Stop } } 
1398
1399   | otherwise  -- Not cached
1400    = do { lkup_inst_res <- matchClassInst inerts cls xis loc
1401          ; case lkup_inst_res of
1402                GenInst wtvs ev_term -> do { addSolvedDict fl 
1403                                           ; solve_from_instance wtvs ev_term }
1404                NoInstance -> try_fundeps_and_return }
1405    where 
1406      arising_sdoc = pprArisingAt loc
1407      dict_id = ctEvId fl
1408      pred = mkClassPred cls xis
1409                        
1410      solve_from_instance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
1411       -- Precondition: evidence term matches the predicate workItem
1412      solve_from_instance evs ev_term 
1413         | null evs
1414         = do { traceTcS "doTopReact/found nullary instance for" $
1415                ppr dict_id
1416              ; setEvBind dict_id ev_term
1417              ; return $ 
1418                SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" 
1419                           , tir_new_item = Stop } }
1420         | otherwise 
1421         = do { traceTcS "doTopReact/found non-nullary instance for" $ 
1422                ppr dict_id
1423              ; setEvBind dict_id ev_term
1424              ; let mk_new_wanted ev
1425                        = CNonCanonical { cc_ev  = ev
1426                                        , cc_loc = bumpCtLocDepth loc }
1427              ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
1428              ; return $
1429                SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
1430                           , tir_new_item = Stop } }
1431
1432      -- We didn't solve it; so try functional dependencies with 
1433      -- the instance environment, and return
1434      -- NB: even if there *are* some functional dependencies against the
1435      -- instance environment, there might be a unique match, and if 
1436      -- so we make sure we get on and solve it first. See Note [Weird fundeps]
1437      try_fundeps_and_return
1438        = do { instEnvs <- getInstEnvs 
1439             ; let fd_eqns = improveFromInstEnv instEnvs (pred, arising_sdoc)
1440             ; fd_work <- rewriteWithFunDeps fd_eqns loc
1441             ; unless (null fd_work) (updWorkListTcS (extendWorkListEqs fd_work))
1442             ; return NoTopInt }
1443        
1444 --------------------
1445 doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
1446                 -> CtLoc -> TcS TopInteractResult
1447 doTopReactFunEq _ct fl fun_tc args xi loc
1448   = ASSERT(isSynFamilyTyCon fun_tc) -- No associated data families have
1449                                      -- reached this far 
1450     -- Look in the cache of solved funeqs
1451     do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
1452        ; case lookupFamHead fun_eq_cache fam_ty of {
1453            Just (ctev, rhs_ty)
1454              | ctEvFlavour ctev `canRewrite` ctEvFlavour fl
1455              -> ASSERT( not (isDerived ctev) )
1456                 succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
1457            _other -> 
1458
1459     -- Look up in top-level instances, or built-in axiom
1460     do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
1461        ; case match_res of {
1462            Nothing -> try_improve_and_return ;
1463            Just (co, ty) ->
1464
1465     -- Found a top-level instance
1466     do {    -- Add it to the solved goals
1467          unless (isDerived fl) (addSolvedFunEq fam_ty fl xi)
1468
1469        ; succeed_with "Fun/Top" co ty } } } } }
1470   where
1471     fam_ty = mkTyConApp fun_tc args
1472
1473     try_improve_and_return =
1474       do { case isBuiltInSynFamTyCon_maybe fun_tc of
1475              Just ops ->
1476                do { let eqns = sfInteractTop ops args xi
1477                   ; impsMb <- mapM (\(Pair x y) -> newDerived (mkTcEqPred x y))
1478                                    eqns
1479                   ; let work = map (mkNonCanonical loc) (catMaybes impsMb)
1480                   ; unless (null work) (updWorkListTcS (extendWorkListEqs work))
1481                   }
1482              _ -> return ()
1483          ; return NoTopInt
1484          }
1485
1486     succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
1487     succeed_with str co rhs_ty    -- co :: fun_tc args ~ rhs_ty
1488       = do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
1489            ; traceTcS ("doTopReactFunEq " ++ str) (ppr ctevs)
1490            ; case ctevs of
1491                [ctev] -> updWorkListTcS $ extendWorkListEq $
1492                          CNonCanonical { cc_ev = ctev
1493                                        , cc_loc  = bumpCtLocDepth loc }
1494                ctevs -> -- No subgoal (because it's cached)
1495                         ASSERT( null ctevs) return () 
1496            ; return $ SomeTopInt { tir_rule = str
1497                                  , tir_new_item = Stop } }
1498       where
1499         xdecomp x = [EvCoercion (mkTcSymCo co `mkTcTransCo` evTermCoercion x)]
1500         xcomp [x] = EvCoercion (co `mkTcTransCo` evTermCoercion x)
1501         xcomp _   = panic "No more goals!"
1502         xev = XEvTerm xcomp xdecomp
1503 \end{code}
1504
1505
1506 Note [FunDep and implicit parameter reactions] 
1507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1508 Currently, our story of interacting two dictionaries (or a dictionary
1509 and top-level instances) for functional dependencies, and implicit
1510 paramters, is that we simply produce new Derived equalities.  So for example
1511
1512         class D a b | a -> b where ... 
1513     Inert: 
1514         d1 :g D Int Bool
1515     WorkItem: 
1516         d2 :w D Int alpha
1517
1518     We generate the extra work item
1519         cv :d alpha ~ Bool
1520     where 'cv' is currently unused.  However, this new item can perhaps be 
1521     spontaneously solved to become given and react with d2,
1522     discharging it in favour of a new constraint d2' thus:
1523         d2' :w D Int Bool
1524         d2 := d2' |> D Int cv
1525     Now d2' can be discharged from d1
1526
1527 We could be more aggressive and try to *immediately* solve the dictionary 
1528 using those extra equalities, but that requires those equalities to carry 
1529 evidence and derived do not carry evidence.
1530
1531 If that were the case with the same inert set and work item we might dischard 
1532 d2 directly:
1533
1534         cv :w alpha ~ Bool
1535         d2 := d1 |> D Int cv
1536
1537 But in general it's a bit painful to figure out the necessary coercion,
1538 so we just take the first approach. Here is a better example. Consider:
1539     class C a b c | a -> b 
1540 And: 
1541      [Given]  d1 : C T Int Char 
1542      [Wanted] d2 : C T beta Int 
1543 In this case, it's *not even possible* to solve the wanted immediately. 
1544 So we should simply output the functional dependency and add this guy
1545 [but NOT its superclasses] back in the worklist. Even worse: 
1546      [Given] d1 : C T Int beta 
1547      [Wanted] d2: C T beta Int 
1548 Then it is solvable, but its very hard to detect this on the spot. 
1549
1550 It's exactly the same with implicit parameters, except that the
1551 "aggressive" approach would be much easier to implement.
1552
1553 Note [When improvement happens]
1554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1555 We fire an improvement rule when
1556
1557   * Two constraints match (modulo the fundep)
1558       e.g. C t1 t2, C t1 t3    where C a b | a->b
1559     The two match because the first arg is identical
1560    
1561 Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a 
1562 superclass of a Wanted goal) or if both are Given.
1563
1564 Example (tcfail138)
1565     class L a b | a -> b
1566     class (G a, L a b) => C a b
1567
1568     instance C a b' => G (Maybe a)
1569     instance C a b  => C (Maybe a) a
1570     instance L (Maybe a) a
1571
1572 When solving the superclasses of the (C (Maybe a) a) instance, we get
1573   Given:  C a b  ... and hance by superclasses, (G a, L a b)
1574   Wanted: G (Maybe a)
1575 Use the instance decl to get
1576   Wanted: C a b'
1577 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1578 and now we need improvement between that derived superclass an the Given (L a b)
1579
1580 Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to 
1581 emit Derived FDs for givens as well. 
1582
1583 Note [Weird fundeps]
1584 ~~~~~~~~~~~~~~~~~~~~
1585 Consider   class Het a b | a -> b where
1586               het :: m (f c) -> a -> m b
1587
1588            class GHet (a :: * -> *) (b :: * -> *) | a -> b
1589            instance            GHet (K a) (K [a])
1590            instance Het a b => GHet (K a) (K b)
1591
1592 The two instances don't actually conflict on their fundeps,
1593 although it's pretty strange.  So they are both accepted. Now
1594 try   [W] GHet (K Int) (K Bool)
1595 This triggers fudeps from both instance decls; but it also 
1596 matches a *unique* instance decl, and we should go ahead and
1597 pick that one right now.  Otherwise, if we don't, it ends up 
1598 unsolved in the inert set and is reported as an error.
1599
1600 Trac #7875 is a case in point.
1601
1602 Note [Overriding implicit parameters]
1603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1604 Consider
1605    f :: (?x::a) -> Bool -> a
1606   
1607    g v = let ?x::Int = 3 
1608          in (f v, let ?x::Bool = True in f v)
1609
1610 This should probably be well typed, with
1611    g :: Bool -> (Int, Bool)
1612
1613 So the inner binding for ?x::Bool *overrides* the outer one.
1614 Hence a work-item Given overrides an inert-item Given.
1615
1616 Note [Given constraint that matches an instance declaration]
1617 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1618 What should we do when we discover that one (or more) top-level 
1619 instances match a given (or solved) class constraint? We have 
1620 two possibilities:
1621
1622   1. Reject the program. The reason is that there may not be a unique
1623      best strategy for the solver. Example, from the OutsideIn(X) paper:
1624        instance P x => Q [x] 
1625        instance (x ~ y) => R [x] y 
1626      
1627        wob :: forall a b. (Q [b], R b a) => a -> Int 
1628
1629        g :: forall a. Q [a] => [a] -> Int 
1630        g x = wob x 
1631
1632        will generate the impliation constraint: 
1633             Q [a] => (Q [beta], R beta [a]) 
1634        If we react (Q [beta]) with its top-level axiom, we end up with a 
1635        (P beta), which we have no way of discharging. On the other hand, 
1636        if we react R beta [a] with the top-level we get  (beta ~ a), which 
1637        is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is 
1638        now solvable by the given Q [a]. 
1639  
1640      However, this option is restrictive, for instance [Example 3] from 
1641      Note [Recursive instances and superclases] will fail to work. 
1642
1643   2. Ignore the problem, hoping that the situations where there exist indeed
1644      such multiple strategies are rare: Indeed the cause of the previous 
1645      problem is that (R [x] y) yields the new work (x ~ y) which can be 
1646      *spontaneously* solved, not using the givens. 
1647
1648 We are choosing option 2 below but we might consider having a flag as well.
1649
1650
1651 Note [New Wanted Superclass Work] 
1652 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1653 Even in the case of wanted constraints, we may add some superclasses 
1654 as new given work. The reason is: 
1655
1656         To allow FD-like improvement for type families. Assume that 
1657         we have a class 
1658              class C a b | a -> b 
1659         and we have to solve the implication constraint: 
1660              C a b => C a beta 
1661         Then, FD improvement can help us to produce a new wanted (beta ~ b) 
1662
1663         We want to have the same effect with the type family encoding of 
1664         functional dependencies. Namely, consider: 
1665              class (F a ~ b) => C a b 
1666         Now suppose that we have: 
1667                given: C a b 
1668                wanted: C a beta 
1669         By interacting the given we will get given (F a ~ b) which is not 
1670         enough by itself to make us discharge (C a beta). However, we 
1671         may create a new derived equality from the super-class of the
1672         wanted constraint (C a beta), namely derived (F a ~ beta). 
1673         Now we may interact this with given (F a ~ b) to get: 
1674                   derived :  beta ~ b 
1675         But 'beta' is a touchable unification variable, and hence OK to 
1676         unify it with 'b', replacing the derived evidence with the identity. 
1677
1678         This requires trySpontaneousSolve to solve *derived*
1679         equalities that have a touchable in their RHS, *in addition*
1680         to solving wanted equalities.
1681
1682 We also need to somehow use the superclasses to quantify over a minimal, 
1683 constraint see note [Minimize by Superclasses] in TcSimplify.
1684
1685
1686 Finally, here is another example where this is useful. 
1687
1688 Example 1:
1689 ----------
1690    class (F a ~ b) => C a b 
1691 And we are given the wanteds:
1692       w1 : C a b 
1693       w2 : C a c 
1694       w3 : b ~ c 
1695 We surely do *not* want to quantify over (b ~ c), since if someone provides
1696 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof 
1697 of (b ~ c), hence no extra evidence is necessary. Here is what will happen: 
1698
1699      Step 1: We will get new *given* superclass work, 
1700              provisionally to our solving of w1 and w2
1701              
1702                g1: F a ~ b, g2 : F a ~ c, 
1703                w1 : C a b, w2 : C a c, w3 : b ~ c
1704
1705              The evidence for g1 and g2 is a superclass evidence term: 
1706
1707                g1 := sc w1, g2 := sc w2
1708
1709      Step 2: The givens will solve the wanted w3, so that 
1710                w3 := sym (sc w1) ; sc w2 
1711                   
1712      Step 3: Now, one may naively assume that then w2 can be solve from w1
1713              after rewriting with the (now solved equality) (b ~ c). 
1714              
1715              But this rewriting is ruled out by the isGoodRectDict! 
1716
1717 Conclusion, we will (correctly) end up with the unsolved goals 
1718     (C a b, C a c)   
1719
1720 NB: The desugarer needs be more clever to deal with equalities 
1721     that participate in recursive dictionary bindings. 
1722
1723 \begin{code}
1724 data LookupInstResult
1725   = NoInstance
1726   | GenInst [CtEvidence] EvTerm 
1727
1728 instance Outputable LookupInstResult where
1729   ppr NoInstance = text "NoInstance"
1730   ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
1731
1732
1733 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1734
1735 matchClassInst _ clas [ ty ] _
1736   | className clas == knownNatClassName
1737   , Just n <- isNumLitTy ty = makeDict (EvNum n)
1738
1739   | className clas == knownSymbolClassName
1740   , Just s <- isStrLitTy ty = makeDict (EvStr s)
1741
1742   where
1743   {- This adds a coercion that will convert the literal into a dictionary
1744      of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
1745      in TcEvidence.  The coercion happens in 2 steps:
1746
1747      Integer -> SNat n     -- representation of literal to singleton
1748      SNat n  -> KnownNat n -- singleton to dictionary
1749
1750      The process is mirrored for Symbols:
1751      String    -> SSymbol n
1752      SSymbol n -> KnownSymbol n
1753   -}
1754   makeDict evLit =
1755     case unwrapNewTyCon_maybe (classTyCon clas) of
1756       Just (_,_, axDict)
1757         | [ meth ]   <- classMethods clas
1758         , Just tcRep <- tyConAppTyCon_maybe -- SNat
1759                       $ funResultTy         -- SNat n
1760                       $ dropForAlls         -- KnownNat n => SNat n
1761                       $ idType meth         -- forall n. KnownNat n => SNat n
1762         , Just (_,_,axRep) <- unwrapNewTyCon_maybe tcRep
1763         -> return $
1764            let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axRep  [ty]
1765                co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [ty]
1766            in GenInst [] $ EvCast (EvLit evLit) (mkTcTransCo co1 co2)
1767
1768       _ -> panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1769                      $$ vcat (map (ppr . idType) (classMethods clas)))
1770
1771 matchClassInst _ clas [ ty1, ty2 ] _
1772   | clas == coercibleClass =  do
1773       traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2
1774       rdr_env <- getGlobalRdrEnvTcS
1775       safeMode <- safeLanguageOn `fmap` getDynFlags
1776       ev <- getCoericbleInst safeMode rdr_env ty1 ty2
1777       traceTcS "matchClassInst returned" $ ppr ev
1778       return ev
1779
1780 matchClassInst inerts clas tys loc
1781    = do { dflags <- getDynFlags
1782         ; untch <- getUntouchables
1783         ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
1784                                            , text "inerts=" <+> ppr inerts
1785                                            , text "untouchables=" <+> ppr untch ]
1786         ; instEnvs <- getInstEnvs
1787         ; case lookupInstEnv instEnvs clas tys of
1788             ([], _, _)               -- Nothing matches  
1789                 -> do { traceTcS "matchClass not matching" $ 
1790                         vcat [ text "dict" <+> ppr pred ]
1791                       ; return NoInstance }
1792
1793             ([(ispec, inst_tys)], [], _) -- A single match 
1794                 | not (xopt Opt_IncoherentInstances dflags)
1795                 , given_overlap untch 
1796                 -> -- See Note [Instance and Given overlap]
1797                    do { traceTcS "Delaying instance application" $ 
1798                           vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
1799                                , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
1800                       ; return NoInstance  }
1801
1802                 | otherwise
1803                 -> do   { let dfun_id = instanceDFunId ispec
1804                         ; traceTcS "matchClass success" $
1805                           vcat [text "dict" <+> ppr pred, 
1806                                 text "witness" <+> ppr dfun_id
1807                                                <+> ppr (idType dfun_id) ]
1808                                   -- Record that this dfun is needed
1809                         ; match_one dfun_id inst_tys }
1810
1811             (matches, _, _)    -- More than one matches 
1812                                -- Defer any reactions of a multitude
1813                                -- until we learn more about the reagent 
1814                 -> do   { traceTcS "matchClass multiple matches, deferring choice" $
1815                           vcat [text "dict" <+> ppr pred,
1816                                 text "matches" <+> ppr matches]
1817                         ; return NoInstance } }
1818    where 
1819      pred = mkClassPred clas tys 
1820
1821      match_one :: DFunId -> [Maybe TcType] -> TcS LookupInstResult
1822                   -- See Note [DFunInstType: instantiating types] in InstEnv
1823      match_one dfun_id mb_inst_tys
1824        = do { checkWellStagedDFun pred dfun_id loc
1825             ; (tys, dfun_phi) <- instDFunType dfun_id mb_inst_tys
1826             ; let (theta, _) = tcSplitPhiTy dfun_phi
1827             ; if null theta then
1828                   return (GenInst [] (EvDFunApp dfun_id tys []))
1829               else do
1830             { evc_vars <- instDFunConstraints theta
1831             ; let new_ev_vars = freshGoals evc_vars
1832                       -- new_ev_vars are only the real new variables that can be emitted 
1833                   dfun_app = EvDFunApp dfun_id tys (getEvTerms evc_vars)
1834             ; return $ GenInst new_ev_vars dfun_app } }
1835
1836      givens_for_this_clas :: Cts
1837      givens_for_this_clas 
1838          = lookupUFM (cts_given (inert_dicts $ inert_cans inerts)) clas 
1839              `orElse` emptyCts
1840
1841      given_overlap :: Untouchables -> Bool
1842      given_overlap untch = anyBag (matchable untch) givens_for_this_clas
1843
1844      matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys
1845                                , cc_ev = fl })
1846        | isGiven fl
1847        = ASSERT( clas_g == clas )
1848          case tcUnifyTys (\tv -> if isTouchableMetaTyVar untch tv && 
1849                                     tv `elemVarSet` tyVarsOfTypes tys
1850                                  then BindMe else Skolem) tys sys of
1851        -- We can't learn anything more about any variable at this point, so the only
1852        -- cause of overlap can be by an instantiation of a touchable unification
1853        -- variable. Hence we only bind touchable unification variables. In addition,
1854        -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
1855             Nothing -> False
1856             Just _  -> True
1857        | otherwise = False -- No overlap with a solved, already been taken care of 
1858                            -- by the overlap check with the instance environment.
1859      matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
1860
1861 -- See Note [Coercible Instances]
1862 -- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
1863 getCoericbleInst :: Bool -> GlobalRdrEnv -> TcType -> TcType -> TcS LookupInstResult
1864 getCoericbleInst safeMode rdr_env ty1 ty2
1865   | ty1 `eqType` ty2
1866   = do return $ GenInst []
1867               $ EvCoercible (EvCoercibleRefl ty1)
1868
1869   | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
1870     Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
1871     tc1 == tc2,
1872     nominalArgsAgree tc1 tyArgs1 tyArgs2,
1873     not safeMode || all (dataConsInScope rdr_env) (tyConsOfTyCon tc1)
1874   = do -- Mark all used data constructors as used
1875        when safeMode $ mapM_ (markDataConsAsUsed rdr_env) (tyConsOfTyCon tc1)
1876        -- We want evidence for all type arguments of role R
1877        arg_evs <- flip mapM (zip3 (tyConRoles tc1) tyArgs1 tyArgs2) $ \(r,ta1,ta2) ->
1878          case r of Nominal -> return (Nothing, EvCoercibleArgN ta1 {- == ta2, due to nominalArgsAgree -})
1879                    Representational -> do
1880                         ct_ev <- requestCoercible ta1 ta2
1881                         return (freshGoal ct_ev, EvCoercibleArgR (getEvTerm ct_ev))
1882                    Phantom -> do
1883                         return (Nothing, EvCoercibleArgP ta1 ta2)
1884        return $ GenInst (mapMaybe fst arg_evs)
1885               $ EvCoercible (EvCoercibleTyCon tc1 (map snd arg_evs))
1886
1887   | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
1888     Just (_, _, _) <- unwrapNewTyCon_maybe tc,
1889     not (isRecursiveTyCon tc),
1890     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
1891   = do markDataConsAsUsed rdr_env tc
1892        let concTy = newTyConInstRhs tc tyArgs 
1893        ct_ev <- requestCoercible concTy ty2
1894        return $ GenInst (freshGoals [ct_ev])
1895               $ EvCoercible (EvCoercibleNewType CLeft tc tyArgs (getEvTerm ct_ev))
1896
1897   | Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
1898     Just (_, _, _) <- unwrapNewTyCon_maybe tc,
1899     not (isRecursiveTyCon tc),
1900     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
1901   = do markDataConsAsUsed rdr_env tc
1902        let concTy = newTyConInstRhs tc tyArgs 
1903        ct_ev <- requestCoercible ty1 concTy
1904        return $ GenInst (freshGoals [ct_ev])
1905               $ EvCoercible (EvCoercibleNewType CRight tc tyArgs (getEvTerm ct_ev))
1906
1907   | otherwise
1908   = return NoInstance
1909
1910
1911 nominalArgsAgree :: TyCon -> [Type] -> [Type] -> Bool
1912 nominalArgsAgree tc tys1 tys2 = all ok $ zip3 (tyConRoles tc) tys1 tys2
1913   where ok (r,t1,t2) = r /= Nominal || t1 `eqType` t2
1914
1915 dataConsInScope :: GlobalRdrEnv -> TyCon -> Bool
1916 dataConsInScope rdr_env tc = not hidden_data_cons
1917   where
1918     data_con_names = map dataConName (tyConDataCons tc)
1919     hidden_data_cons = not (isWiredInName (tyConName tc)) &&
1920                        (isAbstractTyCon tc || any not_in_scope data_con_names)
1921     not_in_scope dc  = null (lookupGRE_Name rdr_env dc)
1922
1923 markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
1924 markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
1925   [ mkRdrQual (is_as (is_decl imp_spec)) occ
1926   | dc <- tyConDataCons tc
1927   , let dc_name = dataConName dc
1928         occ  = nameOccName dc_name
1929         gres = lookupGRE_Name rdr_env dc_name
1930   , not (null gres)
1931   , Imported (imp_spec:_) <- [gre_prov (head gres)] ]
1932
1933 requestCoercible :: TcType -> TcType -> TcS MaybeNew
1934 requestCoercible ty1 ty2 = newWantedEvVar (coercibleClass `mkClassPred` [ty1, ty2]) 
1935
1936 \end{code}
1937
1938 Note [Coercible Instances]
1939 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1940 The class Coercible is special: There are no regular instances, and the user
1941 cannot even define them. Instead, the type checker will create instances and
1942 their evidence out of thin air, in getCoericbleInst. The following “instances”
1943 are present:
1944
1945  1. instance Coercible a a
1946     for any type a.
1947  2. instance (Coercible t1_r t1'_r, Coercible t2_r t2_r',...) =>
1948        Coercible (C t1_r  t2_r  ... t1_p  t2_p  ... t1_n t2_n ...)
1949                  (C t1_r' t2_r' ... t1_p' t2_p' ... t1_n t2_n ...)
1950     for a type constructor C where
1951      * the nominal type arguments are not changed,
1952      * the phantom type arguments may change arbitrarily
1953      * the representational type arguments are again Coercible
1954     Furthermore in Safe Haskell code, we check that
1955      * the data constructors of C are in scope and
1956      * the data constructors of all type constructors used in the definition of C are in scope.
1957        This is required as otherwise the previous check can be circumvented by
1958        just adding a local data type around C.
1959  3. instance Coercible r b => Coercible (NT t1 t2 ...) b
1960     instance Coercible a r => Coercible a (NT t1 t2 ...)
1961     for a newtype constructor NT where
1962      * NT is not recursive
1963      * r is the concrete type of NT, instantiated with the arguments t1 t2 ... 
1964      * the data constructors of NT are in scope.
1965      
1966 These three shapes of instances correspond to the three constructors of
1967 EvCoercible (defined in EvEvidence). They are assembled here and turned to Core
1968 by dsEvTerm in DsBinds.
1969
1970
1971 Note [Instance and Given overlap]
1972 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1973 Assume that we have an inert set that looks as follows:
1974        [Given] D [Int]
1975 And an instance declaration: 
1976        instance C a => D [a]
1977 A new wanted comes along of the form: 
1978        [Wanted] D [alpha]
1979
1980 One possibility is to apply the instance declaration which will leave us 
1981 with an unsolvable goal (C alpha). However, later on a new constraint may 
1982 arise (for instance due to a functional dependency between two later dictionaries), 
1983 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha]) 
1984 will be transformed to [Wanted] D [Int], which could have been discharged by the given. 
1985
1986 The solution is that in matchClassInst and eventually in topReact, we get back with 
1987 a matching instance, only when there is no Given in the inerts which is unifiable to
1988 this particular dictionary.
1989
1990 The end effect is that, much as we do for overlapping instances, we delay choosing a 
1991 class instance if there is a possibility of another instance OR a given to match our 
1992 constraint later on. This fixes bugs #4981 and #5002.
1993
1994 This is arguably not easy to appear in practice due to our aggressive prioritization 
1995 of equality solving over other constraints, but it is possible. I've added a test case 
1996 in typecheck/should-compile/GivenOverlapping.hs
1997
1998 We ignore the overlap problem if -XIncoherentInstances is in force: see
1999 Trac #6002 for a worked-out example where this makes a difference.
2000
2001 Moreover notice that our goals here are different than the goals of the top-level 
2002 overlapping checks. There we are interested in validating the following principle:
2003  
2004     If we inline a function f at a site where the same global instance environment
2005     is available as the instance environment at the definition site of f then we 
2006     should get the same behaviour. 
2007
2008 But for the Given Overlap check our goal is just related to completeness of 
2009 constraint solving.