Merge branch 'master' of http://darcs.haskell.org/ghc
[ghc.git] / compiler / typecheck / TcSimplify.lhs
1 \begin{code}
2 {-# OPTIONS -fno-warn-tabs #-}
3 -- The above warning supression flag is a temporary kludge.
4 -- While working on this module you are encouraged to remove it and
5 -- detab the module (please do the detabbing in a separate patch). See
6 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
7 -- for details
8
9 module TcSimplify( 
10        simplifyInfer, quantifyPred,
11        simplifyAmbiguityCheck,
12        simplifyDefault, 
13        simplifyRule, simplifyTop, simplifyInteractive,
14        solveWantedsTcM
15   ) where
16
17 #include "HsVersions.h"
18
19 import TcRnTypes
20 import TcRnMonad
21 import TcErrors
22 import TcMType as TcM
23 import TcType 
24 import TcSMonad as TcS
25 import TcInteract 
26 import Inst
27 import FunDeps  ( growThetaTyVars )
28 import Type     ( classifyPredType, PredTree(..), getClassPredTys_maybe )
29 import Class    ( Class )
30 import Var
31 import Unique
32 import VarSet
33 import VarEnv 
34 import TcEvidence
35 import Name
36 import Bag
37 import ListSetOps
38 import Util
39 import PrelInfo
40 import PrelNames
41 import Class            ( classKey )
42 import BasicTypes       ( RuleName )
43 import Outputable
44 import FastString
45 import TrieMap () -- DV: for now
46 \end{code}
47
48
49 *********************************************************************************
50 *                                                                               * 
51 *                           External interface                                  *
52 *                                                                               *
53 *********************************************************************************
54
55 \begin{code}
56 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
57 -- Simplify top-level constraints
58 -- Usually these will be implications,
59 -- but when there is nothing to quantify we don't wrap
60 -- in a degenerate implication, so we do that here instead
61 simplifyTop wanteds
62   = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds 
63        ; ev_binds_var <- newTcEvBinds
64        ; zonked_final_wc <- solveWantedsTcMWithEvBinds ev_binds_var wanteds simpl_top
65        ; binds1 <- TcRnMonad.getTcEvBinds ev_binds_var
66        ; traceTc "End simplifyTop }" empty
67
68        ; traceTc "reportUnsolved {" empty
69        ; binds2 <- reportUnsolved zonked_final_wc
70        ; traceTc "reportUnsolved }" empty
71          
72        ; return (binds1 `unionBags` binds2) }
73
74   where
75     -- See Note [Top-level Defaulting Plan]
76     simpl_top :: WantedConstraints -> TcS WantedConstraints
77     simpl_top wanteds
78       = do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds)
79            ; free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc_first_go) 
80            ; let meta_tvs = filterVarSet isMetaTyVar free_tvs
81                    -- zonkTyVarsAndFV: the wc_first_go is not yet zonked
82                    -- filter isMetaTyVar: we might have runtime-skolems in GHCi, 
83                    -- and we definitely don't want to try to assign to those!
84
85            ; mapM_ defaultTyVar (varSetElems meta_tvs)   -- Has unification side effects
86            ; simpl_top_loop wc_first_go }
87     
88     simpl_top_loop wc
89       | isEmptyWC wc || insolubleWC wc
90              -- Don't do type-class defaulting if there are insolubles
91              -- Doing so is not going to solve the insolubles
92       = return wc
93       | otherwise
94       = do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
95            ; let wc_flat_approximate = approximateWC wc_residual
96            ; something_happened <- applyDefaultingRules wc_flat_approximate
97                                         -- See Note [Top-level Defaulting Plan]
98            ; if something_happened then 
99                simpl_top_loop wc_residual 
100              else 
101                return wc_residual }
102 \end{code}
103
104 Note [Top-level Defaulting Plan]
105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
106
107 We have considered two design choices for where/when to apply defaulting.   
108    (i) Do it in SimplCheck mode only /whenever/ you try to solve some 
109        flat constraints, maybe deep inside the context of implications.
110        This used to be the case in GHC 7.4.1.
111    (ii) Do it in a tight loop at simplifyTop, once all other constraint has 
112         finished. This is the current story.
113
114 Option (i) had many disadvantages: 
115    a) First it was deep inside the actual solver, 
116    b) Second it was dependent on the context (Infer a type signature, 
117       or Check a type signature, or Interactive) since we did not want 
118       to always start defaulting when inferring (though there is an exception to  
119       this see Note [Default while Inferring])
120    c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
121           f :: Int -> Bool
122           f x = const True (\y -> let w :: a -> a
123                                       w a = const a (y+1)
124                                   in w y)
125       We will get an implication constraint (for beta the type of y):
126                [untch=beta] forall a. 0 => Num beta
127       which we really cannot default /while solving/ the implication, since beta is
128       untouchable.
129
130 Instead our new defaulting story is to pull defaulting out of the solver loop and
131 go with option (i), implemented at SimplifyTop. Namely:
132      - First have a go at solving the residual constraint of the whole program
133      - Try to approximate it with a flat constraint
134      - Figure out derived defaulting equations for that flat constraint
135      - Go round the loop again if you did manage to get some equations
136
137 Now, that has to do with class defaulting. However there exists type variable /kind/
138 defaulting. Again this is done at the top-level and the plan is:
139      - At the top-level, once you had a go at solving the constraint, do 
140        figure out /all/ the touchable unification variables of the wanted contraints.
141      - Apply defaulting to their kinds
142
143 More details in Note [DefaultTyVar].
144
145 \begin{code}
146
147 ------------------
148 simplifyAmbiguityCheck :: Name -> WantedConstraints -> TcM (Bag EvBind)
149 simplifyAmbiguityCheck name wanteds
150   = traceTc "simplifyAmbiguityCheck" (text "name =" <+> ppr name) >> 
151     simplifyTop wanteds  -- NB: must be simplifyTop so that we
152                          --     do ambiguity resolution.  
153                          -- See Note [Impedence matching] in TcBinds.
154  
155 ------------------
156 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
157 simplifyInteractive wanteds 
158   = traceTc "simplifyInteractive" empty >>
159     simplifyTop wanteds 
160
161 ------------------
162 simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
163                 -> TcM ()       -- Succeeds iff the constraint is soluble
164 simplifyDefault theta
165   = do { traceTc "simplifyInteractive" empty
166        ; wanted <- newFlatWanteds DefaultOrigin theta
167        ; (unsolved, _binds) <- solveWantedsTcM (mkFlatWC wanted)
168
169        ; traceTc "reportUnsolved {" empty
170        -- See Note [Deferring coercion errors to runtime]
171        ; reportAllUnsolved unsolved 
172          -- Postcondition of solveWantedsTcM is that returned
173          -- constraints are zonked. So Precondition of reportUnsolved
174          -- is true.
175        ; traceTc "reportUnsolved }" empty
176
177        ; return () }
178 \end{code}
179
180
181 *********************************************************************************
182 *                                                                                 * 
183 *                            Inference
184 *                                                                                 *
185 ***********************************************************************************
186
187 Note [Which variables to quantify]
188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
189 Suppose the inferred type of a function is
190    T kappa (alpha:kappa) -> Int
191 where alpha is a type unification variable and 
192       kappa is a kind unification variable
193 Then we want to quantify over *both* alpha and kappa.  But notice that
194 kappa appears "at top level" of the type, as well as inside the kind
195 of alpha.  So it should be fine to just look for the "top level"
196 kind/type variables of the type, without looking transitively into the
197 kinds of those type variables.
198
199 \begin{code}
200 simplifyInfer :: Bool
201               -> Bool                  -- Apply monomorphism restriction
202               -> [(Name, TcTauType)]   -- Variables to be generalised,
203                                        -- and their tau-types
204               -> WantedConstraints
205               -> TcM ([TcTyVar],    -- Quantify over these type variables
206                       [EvVar],      -- ... and these constraints
207                       Bool,         -- The monomorphism restriction did something
208                                     --   so the results type is not as general as
209                                     --   it could be
210                       TcEvBinds)    -- ... binding these evidence variables
211 simplifyInfer _top_lvl apply_mr name_taus wanteds
212   | isEmptyWC wanteds
213   = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
214        ; zonked_taus <- zonkTcTypes (map snd name_taus)
215        ; let tvs_to_quantify = varSetElems (tyVarsOfTypes zonked_taus `minusVarSet` gbl_tvs)
216                                -- tvs_to_quantify can contain both kind and type vars
217                                -- See Note [Which variables to quantify]
218        ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
219        ; return (qtvs, [], False, emptyTcEvBinds) }
220
221   | otherwise
222   = do { traceTc "simplifyInfer {"  $ vcat
223              [ ptext (sLit "binds =") <+> ppr name_taus
224              , ptext (sLit "closed =") <+> ppr _top_lvl
225              , ptext (sLit "apply_mr =") <+> ppr apply_mr
226              , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds
227              ]
228
229               -- Historical note: Before step 2 we used to have a
230               -- HORRIBLE HACK described in Note [Avoid unecessary
231               -- constraint simplification] but, as described in Trac
232               -- #4361, we have taken in out now.  That's why we start
233               -- with step 2!
234
235               -- Step 2) First try full-blown solving 
236
237               -- NB: we must gather up all the bindings from doing
238               -- this solving; hence (runTcSWithEvBinds ev_binds_var).
239               -- And note that since there are nested implications,
240               -- calling solveWanteds will side-effect their evidence
241               -- bindings, so we can't just revert to the input
242               -- constraint.
243
244        ; ev_binds_var <- newTcEvBinds
245        ; wanted_transformed <- solveWantedsTcMWithEvBinds ev_binds_var wanteds $
246                                solve_wanteds_and_drop
247                                -- Post: wanted_transformed are zonked
248
249               -- Step 4) Candidates for quantification are an approximation of wanted_transformed
250               -- NB: Already the fixpoint of any unifications that may have happened                                
251               -- NB: We do not do any defaulting when inferring a type, this can lead
252               -- to less polymorphic types, see Note [Default while Inferring]
253  
254               -- Step 5) Minimize the quantification candidates                             
255               -- Step 6) Final candidates for quantification                
256               -- We discard bindings, insolubles etc, because all we are
257               -- care aout it
258
259        ; tc_lcl_env <- TcRnMonad.getLclEnv
260        ; let untch = tcl_untch tc_lcl_env
261        ; quant_pred_candidates   
262            <- if insolubleWC wanted_transformed 
263               then return []   -- See Note [Quantification with errors]
264               else do { gbl_tvs <- tcGetGlobalTyVars
265                       ; let quant_cand = approximateWC wanted_transformed
266                             meta_tvs   = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand)) 
267                       ; ((flats, _insols), _extra_binds) <- runTcS $ 
268                         do { mapM_ (promoteAndDefaultTyVar untch gbl_tvs) meta_tvs
269                                  -- See Note [Promote _and_ default when inferring]
270                            ; _implics <- solveInteract quant_cand
271                            ; getInertUnsolved }
272                       ; return (map ctPred $ filter isWantedCt (bagToList flats)) }
273                    -- NB: Dimitrios is slightly worried that we will get
274                    -- family equalities (F Int ~ alpha) in the quantification
275                    -- candidates, as we have performed no further unflattening
276                    -- at this point. Nothing bad, but inferred contexts might
277                    -- look complicated.
278
279        -- NB: quant_pred_candidates is already the fixpoint of any 
280        --     unifications that may have happened
281        ; gbl_tvs        <- tcGetGlobalTyVars
282        ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
283        ; let init_tvs  = zonked_tau_tvs `minusVarSet` gbl_tvs
284              poly_qtvs = growThetaTyVars quant_pred_candidates init_tvs 
285                          `minusVarSet` gbl_tvs
286              pbound    = filter (quantifyPred poly_qtvs) quant_pred_candidates
287              
288              -- Monomorphism restriction
289              mr_qtvs         = init_tvs `minusVarSet` constrained_tvs
290              constrained_tvs = tyVarsOfTypes quant_pred_candidates
291              mr_bites        = apply_mr && not (null pbound)
292
293              (qtvs, bound) | mr_bites  = (mr_qtvs,   [])
294                            | otherwise = (poly_qtvs, pbound)
295              
296        ; traceTc "simplifyWithApprox" $
297          vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
298               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
299               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
300               , ptext (sLit "pbound =") <+> ppr pbound
301               , ptext (sLit "init_qtvs =") <+> ppr init_tvs 
302               , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs ]
303
304        ; if isEmptyVarSet qtvs && null bound
305          then do { traceTc "} simplifyInfer/no quantification" empty                   
306                  ; emitConstraints wanted_transformed
307                     -- Includes insolubles (if -fdefer-type-errors)
308                     -- as well as flats and implications
309                  ; return ([], [], mr_bites, TcEvBinds ev_binds_var) }
310          else do
311
312        { traceTc "simplifyApprox" $ 
313          ptext (sLit "bound are =") <+> ppr bound 
314          
315             -- Step 4, zonk quantified variables 
316        ; let minimal_flat_preds = mkMinimalBySCs bound
317              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
318                                    | (name, ty) <- name_taus ]
319                         -- Don't add the quantified variables here, because
320                         -- they are also bound in ic_skols and we want them to be
321                         -- tidied uniformly
322
323        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
324
325             -- Step 7) Emit an implication
326        ; minimal_bound_ev_vars <- mapM TcM.newEvVar minimal_flat_preds
327        ; let implic = Implic { ic_untch    = pushUntouchables untch
328                              , ic_skols    = qtvs_to_return
329                              , ic_fsks     = []  -- wanted_tansformed arose only from solveWanteds
330                                                  -- hence no flatten-skolems (which come from givens)
331                              , ic_given    = minimal_bound_ev_vars
332                              , ic_wanted   = wanted_transformed 
333                              , ic_insol    = False
334                              , ic_binds    = ev_binds_var
335                              , ic_info     = skol_info
336                              , ic_env      = tc_lcl_env }
337        ; emitImplication implic
338          
339        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
340              vcat [ ptext (sLit "implic =") <+> ppr implic
341                        -- ic_skols, ic_given give rest of result
342                   , ptext (sLit "qtvs =") <+> ppr qtvs_to_return
343                   , ptext (sLit "spb =") <+> ppr quant_pred_candidates
344                   , ptext (sLit "bound =") <+> ppr bound ]
345
346        ; return ( qtvs_to_return, minimal_bound_ev_vars
347                 , mr_bites,  TcEvBinds ev_binds_var) } }
348
349 quantifyPred :: TyVarSet           -- Quantifying over these
350              -> PredType -> Bool   -- True <=> quantify over this wanted
351 quantifyPred qtvs pred
352   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
353   | otherwise     = tyVarsOfType pred `intersectsVarSet` qtvs
354 \end{code}
355
356 Note [Inheriting implicit parameters]
357 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
358 Consider this:
359
360         f x = (x::Int) + ?y
361
362 where f is *not* a top-level binding.
363 From the RHS of f we'll get the constraint (?y::Int).
364 There are two types we might infer for f:
365
366         f :: Int -> Int
367
368 (so we get ?y from the context of f's definition), or
369
370         f :: (?y::Int) => Int -> Int
371
372 At first you might think the first was better, because then
373 ?y behaves like a free variable of the definition, rather than
374 having to be passed at each call site.  But of course, the WHOLE
375 IDEA is that ?y should be passed at each call site (that's what
376 dynamic binding means) so we'd better infer the second.
377
378 BOTTOM LINE: when *inferring types* you *must* quantify 
379 over implicit parameters. See the predicate isFreeWhenInferring.
380
381 Note [Quantification with errors]
382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
383 If we find that the RHS of the definition has some absolutely-insoluble
384 constraints, we abandon all attempts to find a context to quantify
385 over, and instead make the function fully-polymorphic in whatever
386 type we have found.  For two reasons
387   a) Minimise downstream errors
388   b) Avoid spurious errors from this function
389    
390
391 Note [Default while Inferring]
392 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
393 Our current plan is that defaulting only happens at simplifyTop and
394 not simplifyInfer.  This may lead to some insoluble deferred constraints
395 Example:
396
397 instance D g => C g Int b 
398
399 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
400 type inferred       = gamma -> gamma 
401
402 Now, if we try to default (alpha := Int) we will be able to refine the implication to 
403   (forall b. 0 => C gamma Int b) 
404 which can then be simplified further to 
405   (forall b. 0 => D gamma)
406 Finally we /can/ approximate this implication with (D gamma) and infer the quantified
407 type:  forall g. D g => g -> g
408
409 Instead what will currently happen is that we will get a quantified type 
410 (forall g. g -> g) and an implication:
411        forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
412
413 which, even if the simplifyTop defaults (alpha := Int) we will still be left with an 
414 unsolvable implication:
415        forall g. 0 => (forall b. 0 => D g)
416
417 The concrete example would be: 
418        h :: C g a s => g -> a -> ST s a
419        f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
420
421 But it is quite tedious to do defaulting and resolve the implication constraints and
422 we have not observed code breaking because of the lack of defaulting in inference so 
423 we don't do it for now.
424
425
426
427 Note [Minimize by Superclasses]
428 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
429 When we quantify over a constraint, in simplifyInfer we need to
430 quantify over a constraint that is minimal in some sense: For
431 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
432 we'd like to quantify over Ord alpha, because we can just get Eq alpha
433 from superclass selection from Ord alpha. This minimization is what
434 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
435 to check the original wanted.
436
437
438 Note [Avoid unecessary constraint simplification]
439 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
440     -------- NB NB NB (Jun 12) ------------- 
441     This note not longer applies; see the notes with Trac #4361.
442     But I'm leaving it in here so we remember the issue.)
443     ----------------------------------------
444 When inferring the type of a let-binding, with simplifyInfer,
445 try to avoid unnecessarily simplifying class constraints.
446 Doing so aids sharing, but it also helps with delicate 
447 situations like
448
449    instance C t => C [t] where ..
450
451    f :: C [t] => ....
452    f x = let g y = ...(constraint C [t])... 
453          in ...
454 When inferring a type for 'g', we don't want to apply the
455 instance decl, because then we can't satisfy (C t).  So we
456 just notice that g isn't quantified over 't' and partition
457 the contraints before simplifying.
458
459 This only half-works, but then let-generalisation only half-works.
460
461
462 *********************************************************************************
463 *                                                                                 * 
464 *                             RULES                                               *
465 *                                                                                 *
466 ***********************************************************************************
467
468 See note [Simplifying RULE consraints] in TcRule
469
470 Note [RULE quanfification over equalities]
471 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
472 Decideing which equalities to quantify over is tricky:
473  * We do not want to quantify over insoluble equalities (Int ~ Bool)
474     (a) because we prefer to report a LHS type error
475     (b) because if such things end up in 'givens' we get a bogus
476         "inaccessible code" error
477
478  * But we do want to quantify over things like (a ~ F b), where
479    F is a type function.
480
481 The difficulty is that it's hard to tell what is insoluble!
482 So we see whether the simplificaiotn step yielded any type errors,
483 and if so refrain from quantifying over *any* equalites.
484
485 \begin{code}
486 simplifyRule :: RuleName 
487              -> WantedConstraints       -- Constraints from LHS
488              -> WantedConstraints       -- Constraints from RHS
489              -> TcM ([EvVar], WantedConstraints)   -- LHS evidence varaibles
490 -- See Note [Simplifying RULE constraints] in TcRule
491 simplifyRule name lhs_wanted rhs_wanted
492   = do {         -- We allow ourselves to unify environment 
493                  -- variables: runTcS runs with NoUntouchables
494          (resid_wanted, _) <- solveWantedsTcM (lhs_wanted `andWC` rhs_wanted)
495                               -- Post: these are zonked and unflattened
496
497        ; zonked_lhs_flats <- zonkCts (wc_flat lhs_wanted)
498        ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs_flats
499              quantify_me  -- Note [RULE quantification over equalities]
500                | insolubleWC resid_wanted = quantify_insol
501                | otherwise                = quantify_normal
502
503              quantify_insol ct = not (isEqPred (ctPred ct))
504
505              quantify_normal ct
506                | EqPred t1 t2 <- classifyPredType (ctPred ct)
507                = not (t1 `eqType` t2)
508                | otherwise
509                = True
510              
511        ; traceTc "simplifyRule" $
512          vcat [ ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
513               , text "zonked_lhs_flats" <+> ppr zonked_lhs_flats 
514               , text "q_cts"      <+> ppr q_cts ]
515
516        ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
517                 , lhs_wanted { wc_flat = non_q_cts }) }
518 \end{code}
519
520
521 *********************************************************************************
522 *                                                                                 * 
523 *                                 Main Simplifier                                 *
524 *                                                                                 *
525 ***********************************************************************************
526
527 Note [Deferring coercion errors to runtime]
528 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
529 While developing, sometimes it is desirable to allow compilation to succeed even
530 if there are type errors in the code. Consider the following case:
531
532   module Main where
533
534   a :: Int
535   a = 'a'
536
537   main = print "b"
538
539 Even though `a` is ill-typed, it is not used in the end, so if all that we're
540 interested in is `main` it is handy to be able to ignore the problems in `a`.
541
542 Since we treat type equalities as evidence, this is relatively simple. Whenever
543 we run into a type mismatch in TcUnify, we normally just emit an error. But it
544 is always safe to defer the mismatch to the main constraint solver. If we do
545 that, `a` will get transformed into
546
547   co :: Int ~ Char
548   co = ...
549
550   a :: Int
551   a = 'a' `cast` co
552
553 The constraint solver would realize that `co` is an insoluble constraint, and
554 emit an error with `reportUnsolved`. But we can also replace the right-hand side
555 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
556 to compile, and it will run fine unless we evaluate `a`. This is what
557 `deferErrorsToRuntime` does.
558
559 It does this by keeping track of which errors correspond to which coercion
560 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
561 and does not fail if -fdefer-type-errors is on, so that we can continue
562 compilation. The errors are turned into warnings in `reportUnsolved`.
563
564 Note [Zonk after solving]
565 ~~~~~~~~~~~~~~~~~~~~~~~~~
566 We zonk the result immediately after constraint solving, for two reasons:
567
568 a) because zonkWC generates evidence, and this is the moment when we
569    have a suitable evidence variable to hand.
570
571 Note that *after* solving the constraints are typically small, so the
572 overhead is not great.
573
574 \begin{code}
575 solveWantedsTcMWithEvBinds :: EvBindsVar
576                            -> WantedConstraints
577                            -> (WantedConstraints -> TcS WantedConstraints)
578                            -> TcM WantedConstraints
579 -- Returns a *zonked* result
580 -- We zonk when we finish primarily to un-flatten out any
581 -- flatten-skolems etc introduced by canonicalisation of
582 -- types involving type funuctions.  Happily the result 
583 -- is typically much smaller than the input, indeed it is 
584 -- often empty.
585 solveWantedsTcMWithEvBinds ev_binds_var wc tcs_action
586   = do { traceTc "solveWantedsTcMWithEvBinds" $ text "wanted=" <+> ppr wc
587        ; wc2 <- runTcSWithEvBinds ev_binds_var (tcs_action wc)
588        ; zonkWC ev_binds_var wc2 }
589          -- See Note [Zonk after solving]
590
591 solveWantedsTcM :: WantedConstraints -> TcM (WantedConstraints, Bag EvBind)
592 -- Zonk the input constraints, and simplify them
593 -- Return the evidence binds in the BagEvBinds result
594 -- Discards all Derived stuff in result
595 -- Postcondition: fully zonked and unflattened constraints
596 solveWantedsTcM wanted 
597   = do { ev_binds_var <- newTcEvBinds
598        ; wanteds' <- solveWantedsTcMWithEvBinds ev_binds_var wanted solve_wanteds_and_drop
599        ; binds <- TcRnMonad.getTcEvBinds ev_binds_var
600        ; return (wanteds', binds) }
601
602 solve_wanteds_and_drop :: WantedConstraints -> TcS (WantedConstraints)
603 -- Since solve_wanteds returns the residual WantedConstraints,
604 -- it should alway be called within a runTcS or something similar,
605 solve_wanteds_and_drop wanted = do { wc <- solve_wanteds wanted 
606                                    ; return (dropDerivedWC wc) }
607
608 solve_wanteds :: WantedConstraints -> TcS WantedConstraints 
609 -- so that the inert set doesn't mindlessly propagate.
610 -- NB: wc_flats may be wanted /or/ derived now
611 solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols }) 
612   = do { traceTcS "solveWanteds {" (ppr wanted)
613
614          -- Try the flat bit, including insolubles. Solving insolubles a 
615          -- second time round is a bit of a waste; but the code is simple 
616          -- and the program is wrong anyway, and we don't run the danger 
617          -- of adding Derived insolubles twice; see 
618          -- TcSMonad Note [Do not add duplicate derived insolubles] 
619        ; traceTcS "solveFlats {" empty
620        ; let all_flats = flats `unionBags` insols
621        ; impls_from_flats <- solveInteract all_flats
622        ; traceTcS "solveFlats end }" (ppr impls_from_flats)
623
624        -- solve_wanteds iterates when it is able to float equalities 
625        -- out of one or more of the implications. 
626        ; unsolved_implics <- simpl_loop 1 (implics `unionBags` impls_from_flats)
627
628        ; (unsolved_flats, insoluble_flats) <- getInertUnsolved
629
630         -- We used to unflatten here but now we only do it once at top-level
631         -- during zonking -- see Note [Unflattening while zonking] in TcMType
632        ; let wc = WC { wc_flat  = unsolved_flats   
633                      , wc_impl  = unsolved_implics 
634                      , wc_insol = insoluble_flats }
635                   
636        ; bb <- getTcEvBindsMap
637        ; tb <- getTcSTyBindsMap
638        ; traceTcS "solveWanteds }" $
639                  vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
640                       , text "unsolved_implics =" <+> ppr unsolved_implics
641                       , text "current evbinds  =" <+> ppr (evBindMapBinds bb)
642                       , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
643                       , text "final wc =" <+> ppr wc ]
644
645        ; return wc }
646
647 simpl_loop :: Int
648            -> Bag Implication
649            -> TcS (Bag Implication)
650 simpl_loop n implics
651   | n > 10 
652   = traceTcS "solveWanteds: loop!" empty >> return implics
653   | otherwise 
654   = do { (floated_eqs, unsolved_implics) <- solveNestedImplications implics
655        ; if isEmptyBag floated_eqs 
656          then return unsolved_implics 
657          else 
658     do {   -- Put floated_eqs into the current inert set before looping
659          impls_from_eqs <- solveInteract floated_eqs
660        ; simpl_loop (n+1) (unsolved_implics `unionBags` impls_from_eqs)} }
661
662
663 solveNestedImplications :: Bag Implication
664                         -> TcS (Cts, Bag Implication)
665 -- Precondition: the TcS inerts may contain unsolved flats which have 
666 -- to be converted to givens before we go inside a nested implication.
667 solveNestedImplications implics
668   | isEmptyBag implics
669   = return (emptyBag, emptyBag)
670   | otherwise 
671   = do { inerts <- getTcSInerts
672        ; let thinner_inerts = prepareInertsForImplications inerts
673                  -- See Note [Preparing inert set for implications]
674   
675        ; traceTcS "solveNestedImplications starting {" $ 
676          vcat [ text "original inerts = " <+> ppr inerts
677               , text "thinner_inerts  = " <+> ppr thinner_inerts ]
678          
679        ; (floated_eqs, unsolved_implics)
680            <- flatMapBagPairM (solveImplication thinner_inerts) implics
681
682        -- ... and we are back in the original TcS inerts 
683        -- Notice that the original includes the _insoluble_flats so it was safe to ignore
684        -- them in the beginning of this function.
685        ; traceTcS "solveNestedImplications end }" $
686                   vcat [ text "all floated_eqs ="  <+> ppr floated_eqs
687                        , text "unsolved_implics =" <+> ppr unsolved_implics ]
688
689        ; return (floated_eqs, unsolved_implics) }
690
691 solveImplication :: InertSet
692                  -> Implication    -- Wanted
693                  -> TcS (Cts,      -- All wanted or derived floated equalities: var = type
694                          Bag Implication) -- Unsolved rest (always empty or singleton)
695 -- Precondition: The TcS monad contains an empty worklist and given-only inerts 
696 -- which after trying to solve this implication we must restore to their original value
697 solveImplication inerts
698      imp@(Implic { ic_untch  = untch
699                  , ic_binds  = ev_binds
700                  , ic_skols  = skols 
701                  , ic_fsks   = old_fsks
702                  , ic_given  = givens
703                  , ic_wanted = wanteds
704                  , ic_info   = info
705                  , ic_env    = env })
706   = do { traceTcS "solveImplication {" (ppr imp) 
707
708          -- Solve the nested constraints
709          -- NB: 'inerts' has empty inert_fsks
710        ; (new_fsks, residual_wanted) 
711             <- nestImplicTcS ev_binds untch inerts $
712                do { solveInteractGiven (mkGivenLoc info env) old_fsks givens 
713                   ; residual_wanted <- solve_wanteds wanteds
714                         -- solve_wanteds, *not* solve_wanteds_and_drop, because
715                         -- we want to retain derived equalities so we can float
716                         -- them out in floatEqualities
717                   ; more_fsks <- getFlattenSkols
718                   ; return (more_fsks ++ old_fsks, residual_wanted) }
719
720        ; (floated_eqs, final_wanted)
721              <- floatEqualities (skols ++ new_fsks) givens residual_wanted
722
723        ; let res_implic | isEmptyWC final_wanted 
724                         = emptyBag
725                         | otherwise
726                         = unitBag (imp { ic_fsks   = new_fsks
727                                        , ic_wanted = dropDerivedWC final_wanted
728                                        , ic_insol  = insolubleWC final_wanted })
729
730        ; evbinds <- getTcEvBindsMap
731        ; traceTcS "solveImplication end }" $ vcat
732              [ text "floated_eqs =" <+> ppr floated_eqs
733              , text "new_fsks =" <+> ppr new_fsks
734              , text "res_implic =" <+> ppr res_implic
735              , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
736
737        ; return (floated_eqs, res_implic) }
738 \end{code}
739
740
741 \begin{code}
742 floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints 
743                 -> TcS (Cts, WantedConstraints)
744 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
745 -- and come from the input wanted ev vars or deriveds 
746 -- Also performs some unifications, adding to monadically-carried ty_binds
747 -- These will be used when processing floated_eqs later
748 floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
749   | hasEqualities can_given 
750   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
751   | otherwise 
752   = do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
753        ; untch <- TcS.getUntouchables
754        ; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
755        ; ty_binds <- getTcSTyBindsMap
756        ; traceTcS "floatEqualities" (vcat [ text "Floated eqs =" <+> ppr float_eqs
757                                           , text "Ty binds =" <+> ppr ty_binds])
758        ; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
759   where 
760     skol_set = growSkols wanteds (mkVarSet skols)
761
762     is_floatable :: Ct -> Bool
763     is_floatable ct
764        = isEqPred pred && skol_set `disjointVarSet` tyVarsOfType pred
765        where
766          pred = ctPred ct
767
768 growSkols :: WantedConstraints -> VarSet -> VarSet
769 -- Find all the type variables that might possibly be unified
770 -- with a type that mentions a skolem.  This test is very conservative.
771 -- I don't *think* we need look inside the implications, because any 
772 -- relevant unification variables in there are untouchable.
773 growSkols (WC { wc_flat = flats }) skols
774   = growThetaTyVars theta skols
775   where
776     theta = foldrBag ((:) . ctPred) [] flats
777
778 promoteTyVar :: Untouchables -> TcTyVar  -> TcS ()
779 -- When we float a constraint out of an implication we must restore
780 -- invariant (MetaTvInv) in Note [Untouchable type variables] in TcType
781 promoteTyVar untch tv 
782   | isFloatedTouchableMetaTyVar untch tv
783   = do { cloned_tv <- TcS.cloneMetaTyVar tv
784        ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
785        ; setWantedTyBind tv (mkTyVarTy rhs_tv) }
786   | otherwise
787   = return ()
788
789 promoteAndDefaultTyVar :: Untouchables -> TcTyVarSet -> TyVar -> TcS ()
790 -- See Note [Promote _and_ default when inferring]
791 promoteAndDefaultTyVar untch gbl_tvs tv
792   = do { tv1 <- if tv `elemVarSet` gbl_tvs 
793                 then return tv
794                 else defaultTyVar tv
795        ; promoteTyVar untch tv1 }
796
797 defaultTyVar :: TcTyVar -> TcS TcTyVar
798 -- Precondition: MetaTyVars only
799 -- See Note [DefaultTyVar]
800 defaultTyVar the_tv
801   | not (k `eqKind` default_k)
802   = do { tv' <- TcS.cloneMetaTyVar the_tv
803        ; let new_tv = setTyVarKind tv' default_k
804        ; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv)
805        ; setWantedTyBind the_tv (mkTyVarTy new_tv)
806        ; return new_tv }
807              -- Why not directly derived_pred = mkTcEqPred k default_k?
808              -- See Note [DefaultTyVar]
809              -- We keep the same Untouchables on tv'
810
811   | otherwise = return the_tv    -- The common case
812   where
813     k = tyVarKind the_tv
814     default_k = defaultKind k
815
816 approximateWC :: WantedConstraints -> Cts
817 -- Postcondition: Wanted or Derived Cts 
818 approximateWC wc 
819   = float_wc emptyVarSet wc
820   where 
821     float_wc :: TcTyVarSet -> WantedConstraints -> Cts
822     float_wc skols (WC { wc_flat = flats, wc_impl = implics }) 
823       = do_bag (float_flat skols)   flats  `unionBags` 
824         do_bag (float_implic skols) implics
825                                  
826     float_implic :: TcTyVarSet -> Implication -> Cts
827     float_implic skols imp
828       | hasEqualities (ic_given imp)  -- Don't float out of equalities
829       = emptyCts                      -- cf floatEqualities
830       | otherwise                     -- See Note [approximateWC]
831       = float_wc skols' (ic_wanted imp)
832       where
833         skols' = skols `extendVarSetList` ic_skols imp `extendVarSetList` ic_fsks imp
834             
835     float_flat :: TcTyVarSet -> Ct -> Cts
836     float_flat skols ct
837       | tyVarsOfCt ct `disjointVarSet` skols 
838       = singleCt ct
839       | otherwise = emptyCts
840         
841     do_bag :: (a -> Bag c) -> Bag a -> Bag c
842     do_bag f = foldrBag (unionBags.f) emptyBag
843 \end{code}
844
845 Note [ApproximateWC]
846 ~~~~~~~~~~~~~~~~~~~~
847 approximateWC takes a constraint, typically arising from the RHS of a
848 let-binding whose type we are *inferring*, and extracts from it some
849 *flat* constraints that we might plausibly abstract over.  Of course
850 the top-level flat constraints are plausible, but we also float constraints
851 out from inside, if the are not captured by skolems.
852
853 However we do *not* float anything out if the implication binds equality
854 constriants, because that defeats the OutsideIn story.  Consider
855    data T a where
856      TInt :: T Int
857      MkT :: T a
858
859    f TInt = 3::Int
860
861 We get the implication (a ~ Int => res ~ Int), where so far we've decided 
862   f :: T a -> res
863 We don't want to float (res~Int) out because then we'll infer  
864   f :: T a -> Int
865 which is only on of the possible types. (GHC 7.6 accidentally *did*
866 float out of such implications, which meant it would happily infer
867 non-principal types.)
868
869 Note [DefaultTyVar]
870 ~~~~~~~~~~~~~~~~~~~
871 defaultTyVar is used on any un-instantiated meta type variables to
872 default the kind of OpenKind and ArgKind etc to *.  This is important 
873 to ensure that instance declarations match.  For example consider
874
875      instance Show (a->b)
876      foo x = show (\_ -> True)
877
878 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
879 and that won't match the typeKind (*) in the instance decl.  See tests
880 tc217 and tc175.
881
882 We look only at touchable type variables. No further constraints
883 are going to affect these type variables, so it's time to do it by
884 hand.  However we aren't ready to default them fully to () or
885 whatever, because the type-class defaulting rules have yet to run.
886
887 An important point is that if the type variable tv has kind k and the
888 default is default_k we do not simply generate [D] (k ~ default_k) because:
889
890    (1) k may be ArgKind and default_k may be * so we will fail
891
892    (2) We need to rewrite all occurrences of the tv to be a type
893        variable with the right kind and we choose to do this by rewriting 
894        the type variable /itself/ by a new variable which does have the 
895        right kind.
896
897 Note [Promote _and_ default when inferring]
898 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
899 When we are inferring a type, we simplify the constraint, and then use
900 approximateWC to produce a list of candidate constraints.  Then we MUST
901
902   a) Promote any meta-tyvars that have been floated out by 
903      approximateWC, to restore invariant (MetaTvInv) described in 
904      Note [Untouchable type variables] in TcType.
905
906   b) Default the kind of any meta-tyyvars that are not mentioned in
907      in the environment.
908
909 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
910 have an instance (C ((x:*) -> Int)).  The instance doesn't match -- but it
911 should!  If we don't solve the constraint, we'll stupidly quantify over 
912 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
913 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
914 Trac #7641 is a simpler example.
915
916 Note [Float Equalities out of Implications]
917 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
918 For ordinary pattern matches (including existentials) we float 
919 equalities out of implications, for instance: 
920      data T where 
921        MkT :: Eq a => a -> T 
922      f x y = case x of MkT _ -> (y::Int)
923 We get the implication constraint (x::T) (y::alpha): 
924      forall a. [untouchable=alpha] Eq a => alpha ~ Int
925 We want to float out the equality into a scope where alpha is no
926 longer untouchable, to solve the implication!  
927
928 But we cannot float equalities out of implications whose givens may
929 yield or contain equalities:
930
931       data T a where 
932         T1 :: T Int
933         T2 :: T Bool
934         T3 :: T a 
935         
936       h :: T a -> a -> Int
937       
938       f x y = case x of 
939                 T1 -> y::Int
940                 T2 -> y::Bool
941                 T3 -> h x y
942
943 We generate constraint, for (x::T alpha) and (y :: beta): 
944    [untouchables = beta] (alpha ~ Int => beta ~ Int)   -- From 1st branch
945    [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
946    (alpha ~ beta)                                      -- From 3rd branch 
947
948 If we float the equality (beta ~ Int) outside of the first implication and 
949 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
950 But if we just leave them inside the implications we unify alpha := beta and
951 solve everything.
952
953 Principle: 
954     We do not want to float equalities out which may need the given *evidence*
955     to become soluble.
956
957 Consequence: classes with functional dependencies don't matter (since there is 
958 no evidence for a fundep equality), but equality superclasses do matter (since 
959 they carry evidence).
960
961 Note [Promoting unification variables]
962 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
963 When we float an equality out of an implication we must "promote" free
964 unification variables of the equality, in order to maintain Invariant
965 (MetaTvInv) from Note [Untouchable type variables] in TcType.  for the
966 leftover implication.
967
968 This is absolutely necessary. Consider the following example. We start
969 with two implications and a class with a functional dependency.
970
971     class C x y | x -> y
972     instance C [a] [a]
973           
974     (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
975     (I2)      [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
976
977 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2. 
978 They may react to yield that (beta := [alpha]) which can then be pushed inwards 
979 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
980 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
981 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
982
983     class C x y | x -> y where 
984      op :: x -> y -> ()
985
986     instance C [a] [a]
987
988     type family F a :: *
989
990     h :: F Int -> ()
991     h = undefined
992
993     data TEx where 
994       TEx :: a -> TEx 
995
996
997     f (x::beta) = 
998         let g1 :: forall b. b -> ()
999             g1 _ = h [x]
1000             g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1001         in (g1 '3', g2 undefined)
1002
1003
1004
1005 Note [Solving Family Equations] 
1006 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1007 After we are done with simplification we may be left with constraints of the form:
1008      [Wanted] F xis ~ beta 
1009 If 'beta' is a touchable unification variable not already bound in the TyBinds 
1010 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1011
1012 When is it ok to do so? 
1013     1) 'beta' must not already be defaulted to something. Example: 
1014
1015            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
1016            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
1017                                        have to report this as unsolved.
1018
1019     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
1020        set [beta := F xis] only if beta is not among the free variables of xis.
1021
1022     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
1023        of type family equations. See Inert Set invariants in TcInteract.
1024
1025 This solving is now happening during zonking, see Note [Unflattening while zonking]
1026 in TcMType.
1027
1028
1029 *********************************************************************************
1030 *                                                                               * 
1031 *                          Defaulting and disamgiguation                        *
1032 *                                                                               *
1033 *********************************************************************************
1034
1035 \begin{code}
1036 applyDefaultingRules :: Cts -> TcS Bool
1037   -- True <=> I did some defaulting, reflected in ty_binds
1038                  
1039 -- Return some extra derived equalities, which express the
1040 -- type-class default choice. 
1041 applyDefaultingRules wanteds
1042   | isEmptyBag wanteds 
1043   = return False
1044   | otherwise
1045   = do { traceTcS "applyDefaultingRules { " $ 
1046                   text "wanteds =" <+> ppr wanteds
1047                   
1048        ; info@(default_tys, _) <- getDefaultInfo
1049        ; let groups = findDefaultableGroups info wanteds
1050        ; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups
1051                                                  , text "info=" <+> ppr info ]
1052        ; something_happeneds <- mapM (disambigGroup default_tys) groups
1053
1054        ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
1055
1056        ; return (or something_happeneds) }
1057 \end{code}
1058
1059
1060
1061 \begin{code}
1062 findDefaultableGroups 
1063     :: ( [Type]
1064        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1065     -> Cts              -- Unsolved (wanted or derived)
1066     -> [[(Ct,Class,TcTyVar)]]
1067 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1068   | null default_tys             = []
1069   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1070   where 
1071     unaries     :: [(Ct, Class, TcTyVar)]  -- (C tv) constraints
1072     non_unaries :: [Ct]             -- and *other* constraints
1073     
1074     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1075         -- Finds unary type-class constraints
1076     find_unary cc 
1077         | Just (cls,[ty]) <- getClassPredTys_maybe (ctPred cc)
1078         , Just tv <- tcGetTyVar_maybe ty
1079         , isMetaTyVar tv  -- We might have runtime-skolems in GHCi, and 
1080                           -- we definitely don't want to try to assign to those!
1081         = Left (cc, cls, tv)
1082     find_unary cc = Right cc  -- Non unary or non dictionary 
1083
1084     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
1085     bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries 
1086
1087     cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
1088
1089     is_defaultable_group ds@((_,_,tv):_)
1090         = let b1 = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
1091               b2 = not (tv `elemVarSet` bad_tvs)
1092               b4 = defaultable_classes [cls | (_,cls,_) <- ds]
1093           in (b1 && b2 && b4)
1094     is_defaultable_group [] = panic "defaultable_group"
1095
1096     defaultable_classes clss 
1097         | extended_defaults = any isInteractiveClass clss
1098         | otherwise         = all is_std_class clss && (any is_num_class clss)
1099
1100     -- In interactive mode, or with -XExtendedDefaultRules,
1101     -- we default Show a to Show () to avoid graututious errors on "show []"
1102     isInteractiveClass cls 
1103         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1104
1105     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1106     -- is_num_class adds IsString to the standard numeric classes, 
1107     -- when -foverloaded-strings is enabled
1108
1109     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1110     -- Similarly is_std_class
1111
1112 ------------------------------
1113 disambigGroup :: [Type]                  -- The default types 
1114               -> [(Ct, Class, TcTyVar)]  -- All classes of the form (C a)
1115                                          --  sharing same type variable
1116               -> TcS Bool   -- True <=> something happened, reflected in ty_binds
1117
1118 disambigGroup []  _grp
1119   = return False
1120 disambigGroup (default_ty:default_tys) group
1121   = do { traceTcS "disambigGroup {" (ppr group $$ ppr default_ty)
1122        ; success <- tryTcS $ -- Why tryTcS? If this attempt fails, we want to 
1123                              -- discard all side effects from the attempt
1124                     do { setWantedTyBind the_tv default_ty
1125                        ; implics_from_defaulting <- solveInteract wanteds
1126                        ; MASSERT (isEmptyBag implics_from_defaulting)
1127                            -- I am not certain if any implications can be generated
1128                            -- but I am letting this fail aggressively if this ever happens.
1129                                      
1130                        ; checkAllSolved }
1131
1132        ; if success then
1133              -- Success: record the type variable binding, and return
1134              do { setWantedTyBind the_tv default_ty
1135                 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
1136                 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
1137                 ; return True }
1138          else
1139              -- Failure: try with the next type
1140              do { traceTcS "disambigGroup failed, will try other default types }"
1141                            (ppr default_ty)
1142                 ; disambigGroup default_tys group } }
1143   where
1144     ((_,_,the_tv):_) = group
1145     wanteds          = listToBag (map fstOf3 group)
1146 \end{code}
1147
1148 Note [Avoiding spurious errors]
1149 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1150 When doing the unification for defaulting, we check for skolem
1151 type variables, and simply don't default them.  For example:
1152    f = (*)      -- Monomorphic
1153    g :: Num a => a -> a
1154    g x = f x x
1155 Here, we get a complaint when checking the type signature for g,
1156 that g isn't polymorphic enough; but then we get another one when
1157 dealing with the (Num a) context arising from f's definition;
1158 we try to unify a with Int (to default it), but find that it's
1159 already been unified with the rigid variable from g's type sig
1160