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