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