Keeping Derived constraints in the unsolved
[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, simplifyAmbiguityCheck,
11        simplifyDefault, simplifyDeriv, 
12        simplifyRule, simplifyTop, simplifyInteractive
13   ) where
14
15 #include "HsVersions.h"
16
17 import TcRnMonad
18 import TcErrors
19 import TcMType
20 import TcType 
21 import TcSMonad 
22 import TcInteract 
23 import Inst
24 import Unify    ( niFixTvSubst, niSubstTvSet )
25 import Type     ( classifyPredType, PredTree(..), isIPPred_maybe )
26 import Var
27 import Unique
28 import VarSet
29 import VarEnv 
30 import TcEvidence
31 import TypeRep
32 import Name
33 import Bag
34 import ListSetOps
35 import Util
36 import PrelInfo
37 import PrelNames
38 import Class            ( classKey )
39 import BasicTypes       ( RuleName )
40 import Control.Monad    ( when )
41 import Outputable
42 import FastString
43 import TrieMap () -- DV: for now
44 import DynFlags
45 import Data.Maybe ( mapMaybe )
46 \end{code}
47
48
49 *********************************************************************************
50 *                                                                               * 
51 *                           External interface                                  *
52 *                                                                               *
53 *********************************************************************************
54
55
56 \begin{code}
57
58
59 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
60 -- Simplify top-level constraints
61 -- Usually these will be implications,
62 -- but when there is nothing to quantify we don't wrap
63 -- in a degenerate implication, so we do that here instead
64 simplifyTop wanteds 
65   = do { ev_binds_var <- newTcEvBinds
66                          
67        ; zonked_wanteds <- zonkWC wanteds
68        ; wc_first_go <- solveWantedsWithEvBinds ev_binds_var zonked_wanteds
69        ; cts <- applyTyVarDefaulting wc_first_go 
70                 -- See Note [Top-level Defaulting Plan]
71                 
72        ; let wc_for_loop = wc_first_go { wc_flat = wc_flat wc_first_go `unionBags` cts }
73                            
74        ; traceTc "simpl_top_loop {" $ text "zonked_wc =" <+> ppr zonked_wanteds
75        ; simpl_top_loop ev_binds_var wc_for_loop }
76     
77   where simpl_top_loop ev_binds_var wc
78           | isEmptyWC wc 
79           = do { traceTc "simpl_top_loop }" empty
80                ; TcRnMonad.getTcEvBinds ev_binds_var }
81           | otherwise
82           = do { wc_residual <- solveWantedsWithEvBinds ev_binds_var wc
83                ; let wc_flat_approximate = approximateWC wc_residual
84                ; (dflt_eqs,_unused_bind) <- runTcS $
85                                             applyDefaultingRules wc_flat_approximate
86                                             -- See Note [Top-level Defaulting Plan]
87                ; if isEmptyBag dflt_eqs then 
88                    do { traceTc "simpl_top_loop }" empty
89                       ; report_and_finish ev_binds_var wc_residual }
90                  else
91                    simpl_top_loop ev_binds_var $ 
92                    wc_residual { wc_flat = wc_flat wc_residual `unionBags` dflt_eqs } }
93
94         report_and_finish ev_binds_var wc_residual 
95           = do { eb1 <- TcRnMonad.getTcEvBinds ev_binds_var
96                ; traceTc "reportUnsolved {" empty
97                    -- See Note [Deferring coercion errors to runtime]
98                ; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
99                ; eb2 <- reportUnsolved runtimeCoercionErrors wc_residual
100                ; traceTc "reportUnsolved }" empty
101                ; return (eb1 `unionBags` eb2) }
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     simplifyCheck wanteds
152  
153 ------------------
154 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
155 simplifyInteractive wanteds 
156   = traceTc "simplifyInteractive" empty >>
157     simplifyTop wanteds 
158
159 ------------------
160 simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
161                 -> TcM ()       -- Succeeds iff the constraint is soluble
162 simplifyDefault theta
163   = do { traceTc "simplifyInteractive" empty
164        ; wanted <- newFlatWanteds DefaultOrigin theta
165        ; _ignored_ev_binds <- simplifyCheck (mkFlatWC wanted)
166        ; return () }
167 \end{code}
168
169
170 ***********************************************************************************
171 *                                                                                 * 
172 *                            Deriving                                             *
173 *                                                                                 *
174 ***********************************************************************************
175
176 \begin{code}
177 simplifyDeriv :: CtOrigin
178               -> PredType
179               -> [TyVar]        
180               -> ThetaType              -- Wanted
181               -> TcM ThetaType  -- Needed
182 -- Given  instance (wanted) => C inst_ty 
183 -- Simplify 'wanted' as much as possibles
184 -- Fail if not possible
185 simplifyDeriv orig pred tvs theta 
186   = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
187                 -- The constraint solving machinery 
188                 -- expects *TcTyVars* not TyVars.  
189                 -- We use *non-overlappable* (vanilla) skolems
190                 -- See Note [Overlap and deriving]
191
192        ; let subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
193              skol_set   = mkVarSet tvs_skols
194              doc = ptext (sLit "deriving") <+> parens (ppr pred)
195
196        ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
197
198        ; traceTc "simplifyDeriv" $ 
199          vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
200        ; (residual_wanted, _ev_binds1)
201              <- solveWanteds (mkFlatWC wanted)
202
203        ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
204                          -- See Note [Exotic derived instance contexts]
205              get_good :: Ct -> Either PredType Ct
206              get_good ct | validDerivPred skol_set p 
207                          , isWantedCt ct  = Left p 
208                          -- NB: residual_wanted may contain unsolved
209                          -- Derived and we stick them into the bad set
210                          -- so that reportUnsolved may decide what to do with them
211                          | otherwise = Right ct
212                          where p = ctPred ct
213
214        -- We never want to defer these errors because they are errors in the
215        -- compiler! Hence the `False` below
216        ; _ev_binds2 <- reportUnsolved False (residual_wanted { wc_flat = bad })
217
218        ; let min_theta = mkMinimalBySCs (bagToList good)
219        ; return (substTheta subst_skol min_theta) }
220 \end{code}
221
222 Note [Overlap and deriving]
223 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
224 Consider some overlapping instances:
225   data Show a => Show [a] where ..
226   data Show [Char] where ...
227
228 Now a data type with deriving:
229   data T a = MkT [a] deriving( Show )
230
231 We want to get the derived instance
232   instance Show [a] => Show (T a) where...
233 and NOT
234   instance Show a => Show (T a) where...
235 so that the (Show (T Char)) instance does the Right Thing
236
237 It's very like the situation when we're inferring the type
238 of a function
239    f x = show [x]
240 and we want to infer
241    f :: Show [a] => a -> String
242
243 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
244              the context for the derived instance. 
245              Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
246
247 Note [Exotic derived instance contexts]
248 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
249 In a 'derived' instance declaration, we *infer* the context.  It's a
250 bit unclear what rules we should apply for this; the Haskell report is
251 silent.  Obviously, constraints like (Eq a) are fine, but what about
252         data T f a = MkT (f a) deriving( Eq )
253 where we'd get an Eq (f a) constraint.  That's probably fine too.
254
255 One could go further: consider
256         data T a b c = MkT (Foo a b c) deriving( Eq )
257         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
258
259 Notice that this instance (just) satisfies the Paterson termination 
260 conditions.  Then we *could* derive an instance decl like this:
261
262         instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
263 even though there is no instance for (C Int a), because there just
264 *might* be an instance for, say, (C Int Bool) at a site where we
265 need the equality instance for T's.  
266
267 However, this seems pretty exotic, and it's quite tricky to allow
268 this, and yet give sensible error messages in the (much more common)
269 case where we really want that instance decl for C.
270
271 So for now we simply require that the derived instance context
272 should have only type-variable constraints.
273
274 Here is another example:
275         data Fix f = In (f (Fix f)) deriving( Eq )
276 Here, if we are prepared to allow -XUndecidableInstances we
277 could derive the instance
278         instance Eq (f (Fix f)) => Eq (Fix f)
279 but this is so delicate that I don't think it should happen inside
280 'deriving'. If you want this, write it yourself!
281
282 NB: if you want to lift this condition, make sure you still meet the
283 termination conditions!  If not, the deriving mechanism generates
284 larger and larger constraints.  Example:
285   data Succ a = S a
286   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
287
288 Note the lack of a Show instance for Succ.  First we'll generate
289   instance (Show (Succ a), Show a) => Show (Seq a)
290 and then
291   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
292 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
293
294 The bottom line
295 ~~~~~~~~~~~~~~~
296 Allow constraints which consist only of type variables, with no repeats.
297
298 *********************************************************************************
299 *                                                                                 * 
300 *                            Inference
301 *                                                                                 *
302 ***********************************************************************************
303
304 Note [Which variables to quantify]
305 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
306 Suppose the inferred type of a function is
307    T kappa (alpha:kappa) -> Int
308 where alpha is a type unification variable and 
309       kappa is a kind unification variable
310 Then we want to quantify over *both* alpha and kappa.  But notice that
311 kappa appears "at top level" of the type, as well as inside the kind
312 of alpha.  So it should be fine to just look for the "top level"
313 kind/type variables of the type, without looking transitively into the
314 kinds of those type variables.
315
316 \begin{code}
317 simplifyInfer :: Bool
318               -> Bool                  -- Apply monomorphism restriction
319               -> [(Name, TcTauType)]   -- Variables to be generalised,
320                                        -- and their tau-types
321               -> (Untouchables, WantedConstraints)
322               -> TcM ([TcTyVar],    -- Quantify over these type variables
323                       [EvVar],      -- ... and these constraints
324                       Bool,         -- The monomorphism restriction did something
325                                     --   so the results type is not as general as
326                                     --   it could be
327                       TcEvBinds)    -- ... binding these evidence variables
328 simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
329   | isEmptyWC wanteds
330   = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
331        ; zonked_taus <- zonkTcTypes (map snd name_taus)
332        ; let tvs_to_quantify = varSetElems (tyVarsOfTypes zonked_taus `minusVarSet` gbl_tvs)
333                                -- tvs_to_quantify can contain both kind and type vars
334                                -- See Note [Which variables to quantify]
335        ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
336        ; return (qtvs, [], False, emptyTcEvBinds) }
337
338   | otherwise
339   = do { runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
340        ; gbl_tvs        <- tcGetGlobalTyVars
341        ; zonked_tau_tvs <- zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
342        ; zonked_wanteds <- zonkWC wanteds
343
344        ; traceTc "simplifyInfer {"  $ vcat
345              [ ptext (sLit "names =") <+> ppr (map fst name_taus)
346              , ptext (sLit "taus =") <+> ppr (map snd name_taus)
347              , ptext (sLit "tau_tvs (zonked) =") <+> ppr zonked_tau_tvs
348              , ptext (sLit "gbl_tvs =") <+> ppr gbl_tvs
349              , ptext (sLit "closed =") <+> ppr _top_lvl
350              , ptext (sLit "apply_mr =") <+> ppr apply_mr
351              , ptext (sLit "untch =") <+> ppr untch
352              , ptext (sLit "wanted =") <+> ppr zonked_wanteds
353              ]
354
355               -- Historical note: Before step 2 we used to have a
356               -- HORRIBLE HACK described in Note [Avoid unecessary
357               -- constraint simplification] but, as described in Trac
358               -- #4361, we have taken in out now.  That's why we start
359               -- with step 2!
360
361               -- Step 2) First try full-blown solving 
362
363               -- NB: we must gather up all the bindings from doing
364               -- this solving; hence (runTcSWithEvBinds ev_binds_var).
365               -- And note that since there are nested implications,
366               -- calling solveWanteds will side-effect their evidence
367               -- bindings, so we can't just revert to the input
368               -- constraint.
369        ; ev_binds_var <- newTcEvBinds
370        ; wanted_transformed <- solveWantedsWithEvBinds ev_binds_var zonked_wanteds
371
372               -- Step 3) Fail fast if there is an insoluble constraint,
373               -- unless we are deferring errors to runtime
374        ; when (not runtimeCoercionErrors && insolubleWC wanted_transformed) $ 
375          do { _ev_binds <- reportUnsolved False wanted_transformed; failM }
376
377               -- Step 4) Candidates for quantification are an approximation of wanted_transformed
378        ; let quant_candidates = approximateWC wanted_transformed               
379               -- NB: Already the fixpoint of any unifications that may have happened                                
380               -- NB: We do not do any defaulting when inferring a type, this can lead
381               -- to less polymorphic types, see Note [Default while Inferring]
382               -- NB: quant_candidates here are wanted or derived, we filter the wanteds later, anyway
383  
384               -- Step 5) Minimize the quantification candidates                             
385        ; (quant_candidates_transformed, _extra_binds)   
386              <- solveWanteds $ WC { wc_flat  = quant_candidates
387                                   , wc_impl  = emptyBag
388                                   , wc_insol = emptyBag }
389
390               -- Step 6) Final candidates for quantification                
391        ; let final_quant_candidates :: Bag PredType
392              final_quant_candidates = mapBag ctPred $ 
393                                       keepWanted (wc_flat quant_candidates_transformed)
394              -- NB: Already the fixpoint of any unifications that may have happened
395                   
396        ; gbl_tvs        <- tcGetGlobalTyVars -- TODO: can we just use untch instead of gbl_tvs?
397        ; zonked_tau_tvs <- zonkTyVarsAndFV zonked_tau_tvs
398        
399        ; traceTc "simplifyWithApprox" $
400          vcat [ ptext (sLit "final_quant_candidates =") <+> ppr final_quant_candidates
401               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
402               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs ]
403          
404        ; let init_tvs        = zonked_tau_tvs `minusVarSet` gbl_tvs
405              poly_qtvs       = growPreds gbl_tvs id final_quant_candidates init_tvs
406              
407              pbound          = filterBag (quantifyMe poly_qtvs id) final_quant_candidates
408              
409        ; traceTc "simplifyWithApprox" $
410          vcat [ ptext (sLit "pbound =") <+> ppr pbound ]
411          
412              -- Monomorphism restriction
413        ; let mr_qtvs         = init_tvs `minusVarSet` constrained_tvs
414              constrained_tvs = tyVarsOfBag tyVarsOfType final_quant_candidates
415              mr_bites        = apply_mr && not (isEmptyBag pbound)
416
417              (qtvs, bound)
418                 | mr_bites  = (mr_qtvs,   emptyBag)
419                 | otherwise = (poly_qtvs, pbound)
420              
421
422        ; if isEmptyVarSet qtvs && isEmptyBag bound
423          then do { traceTc "} simplifyInfer/no quantification" empty                   
424                  ; emitConstraints wanted_transformed
425                     -- Includes insolubles (if -fdefer-type-errors)
426                     -- as well as flats and implications
427                  ; return ([], [], mr_bites, TcEvBinds ev_binds_var) }
428          else do
429
430        { traceTc "simplifyApprox" $ 
431          ptext (sLit "bound are =") <+> ppr bound 
432          
433             -- Step 4, zonk quantified variables 
434        ; let minimal_flat_preds = mkMinimalBySCs $ bagToList bound
435              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
436                                    | (name, ty) <- name_taus ]
437                         -- Don't add the quantified variables here, because
438                         -- they are also bound in ic_skols and we want them to be
439                         -- tidied uniformly
440
441        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
442
443             -- Step 7) Emit an implication
444        ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
445        ; lcl_env <- getLclTypeEnv
446        ; gloc <- getCtLoc skol_info
447        ; let implic = Implic { ic_untch    = untch 
448                              , ic_env      = lcl_env
449                              , ic_skols    = qtvs_to_return
450                              , ic_given    = minimal_bound_ev_vars
451                              , ic_wanted   = wanted_transformed 
452                              , ic_insol    = False
453                              , ic_binds    = ev_binds_var
454                              , ic_loc      = gloc }
455        ; emitImplication implic
456          
457        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
458              vcat [ ptext (sLit "implic =") <+> ppr implic
459                        -- ic_skols, ic_given give rest of result
460                   , ptext (sLit "qtvs =") <+> ppr qtvs_to_return
461                   , ptext (sLit "spb =") <+> ppr final_quant_candidates
462                   , ptext (sLit "bound =") <+> ppr bound ]
463
464        ; return ( qtvs_to_return, minimal_bound_ev_vars
465                 , mr_bites,  TcEvBinds ev_binds_var) } }
466     where 
467 \end{code}
468
469
470 Note [Note [Default while Inferring]
471 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
472 Our current plan is that defaulting only happens at simplifyTop and
473 not simplifyInfer.  This may lead to some insoluble deferred constraints
474 Example:
475
476 instance D g => C g Int b 
477
478 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
479 type inferred       = gamma -> gamma 
480
481 Now, if we try to default (alpha := Int) we will be able to refine the implication to 
482   (forall b. 0 => C gamma Int b) 
483 which can then be simplified further to 
484   (forall b. 0 => D gamma)
485 Finally we /can/ approximate this implication with (D gamma) and infer the quantified
486 type:  forall g. D g => g -> g
487
488 Instead what will currently happen is that we will get a quantified type 
489 (forall g. g -> g) and an implication:
490        forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
491
492 which, even if the simplifyTop defaults (alpha := Int) we will still be left with an 
493 unsolvable implication:
494        forall g. 0 => (forall b. 0 => D g)
495
496 The concrete example would be: 
497        h :: C g a s => g -> a -> ST s a
498        f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
499
500 But it is quite tedious to do defaulting and resolve the implication constraints and
501 we have not observed code breaking because of the lack of defaulting in inference so 
502 we don't do it for now.
503
504
505
506 Note [Minimize by Superclasses]
507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
508
509 When we quantify over a constraint, in simplifyInfer we need to
510 quantify over a constraint that is minimal in some sense: For
511 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
512 we'd like to quantify over Ord alpha, because we can just get Eq alpha
513 from superclass selection from Ord alpha. This minimization is what
514 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
515 to check the original wanted.
516
517
518 \begin{code}
519
520
521 approximateWC :: WantedConstraints -> Cts
522 -- Postcondition: Wanted or Derived Cts 
523 approximateWC wc = float_wc emptyVarSet wc
524   where 
525     float_wc :: TcTyVarSet -> WantedConstraints -> Cts
526     float_wc skols (WC { wc_flat = flat, wc_impl = implic }) = floats1 `unionBags` floats2
527       where floats1 = do_bag (float_flat skols) flat
528             floats2 = do_bag (float_implic skols) implic
529                                  
530     float_implic :: TcTyVarSet -> Implication -> Cts
531     float_implic skols imp
532       = float_wc (skols `extendVarSetList` ic_skols imp) (ic_wanted imp)
533             
534     float_flat :: TcTyVarSet -> Ct -> Cts
535     float_flat skols ct
536       | tyVarsOfCt ct `disjointVarSet` skols 
537       = singleCt ct
538       | otherwise = emptyCts
539         
540     do_bag :: (a -> Bag c) -> Bag a -> Bag c
541     do_bag f = foldrBag (unionBags.f) emptyBag
542
543
544 \end{code}
545
546 \begin{code}
547 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
548 growPreds gbl_tvs get_pred items tvs
549   = foldrBag extend tvs items
550   where
551     extend item tvs = tvs `unionVarSet`
552                       (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
553
554 --------------------
555 quantifyMe :: TyVarSet      -- Quantifying over these
556            -> (a -> PredType)
557            -> a -> Bool     -- True <=> quantify over this wanted
558 quantifyMe qtvs toPred ct
559   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
560   | otherwise     = tyVarsOfType pred `intersectsVarSet` qtvs
561   where
562     pred = toPred ct
563 \end{code}
564
565 Note [Avoid unecessary constraint simplification]
566 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
567     -------- NB NB NB (Jun 12) ------------- 
568     This note not longer applies; see the notes with Trac #4361.
569     But I'm leaving it in here so we remember the issue.)
570     ----------------------------------------
571 When inferring the type of a let-binding, with simplifyInfer,
572 try to avoid unnecessarily simplifying class constraints.
573 Doing so aids sharing, but it also helps with delicate 
574 situations like
575
576    instance C t => C [t] where ..
577
578    f :: C [t] => ....
579    f x = let g y = ...(constraint C [t])... 
580          in ...
581 When inferring a type for 'g', we don't want to apply the
582 instance decl, because then we can't satisfy (C t).  So we
583 just notice that g isn't quantified over 't' and partition
584 the contraints before simplifying.
585
586 This only half-works, but then let-generalisation only half-works.
587
588
589 Note [Inheriting implicit parameters]
590 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
591 Consider this:
592
593         f x = (x::Int) + ?y
594
595 where f is *not* a top-level binding.
596 From the RHS of f we'll get the constraint (?y::Int).
597 There are two types we might infer for f:
598
599         f :: Int -> Int
600
601 (so we get ?y from the context of f's definition), or
602
603         f :: (?y::Int) => Int -> Int
604
605 At first you might think the first was better, becuase then
606 ?y behaves like a free variable of the definition, rather than
607 having to be passed at each call site.  But of course, the WHOLE
608 IDEA is that ?y should be passed at each call site (that's what
609 dynamic binding means) so we'd better infer the second.
610
611 BOTTOM LINE: when *inferring types* you *must* quantify 
612 over implicit parameters. See the predicate isFreeWhenInferring.
613
614
615 *********************************************************************************
616 *                                                                                 * 
617 *                             RULES                                               *
618 *                                                                                 *
619 ***********************************************************************************
620
621 See note [Simplifying RULE consraints] in TcRule
622
623 Note [RULE quanfification over equalities]
624 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
625 Decideing which equalities to quantify over is tricky:
626  * We do not want to quantify over insoluble equalities (Int ~ Bool)
627     (a) because we prefer to report a LHS type error
628     (b) because if such things end up in 'givens' we get a bogus
629         "inaccessible code" error
630
631  * But we do want to quantify over things like (a ~ F b), where
632    F is a type function.
633
634 The difficulty is that it's hard to tell what is insoluble!
635 So we see whether the simplificaiotn step yielded any type errors,
636 and if so refrain from quantifying over *any* equalites.
637
638 \begin{code}
639 simplifyRule :: RuleName 
640              -> WantedConstraints       -- Constraints from LHS
641              -> WantedConstraints       -- Constraints from RHS
642              -> TcM ([EvVar], WantedConstraints)   -- LHS evidence varaibles
643 -- See Note [Simplifying RULE constraints] in TcRule
644 simplifyRule name lhs_wanted rhs_wanted
645   = do { zonked_all <- zonkWC (lhs_wanted `andWC` rhs_wanted)
646        ; let doc = ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
647              
648                  -- We allow ourselves to unify environment 
649                  -- variables: runTcS runs with NoUntouchables
650        ; (resid_wanted, _) <- solveWanteds zonked_all
651
652        ; zonked_lhs <- zonkWC lhs_wanted
653
654        ; let (q_cts, non_q_cts) = partitionBag quantify_me (wc_flat zonked_lhs)
655              quantify_me  -- Note [RULE quantification over equalities]
656                | insolubleWC resid_wanted = quantify_insol
657                | otherwise                = quantify_normal
658
659              quantify_insol ct = not (isEqPred (ctPred ct))
660
661              quantify_normal ct
662                | EqPred t1 t2 <- classifyPredType (ctPred ct)
663                = not (t1 `eqType` t2)
664                | otherwise
665                = True
666              
667        ; traceTc "simplifyRule" $
668          vcat [ doc
669               , text "zonked_lhs" <+> ppr zonked_lhs 
670               , text "q_cts"      <+> ppr q_cts ]
671
672        ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
673                 , zonked_lhs { wc_flat = non_q_cts }) }
674 \end{code}
675
676
677 *********************************************************************************
678 *                                                                                 * 
679 *                                 Main Simplifier                                 *
680 *                                                                                 *
681 ***********************************************************************************
682
683 \begin{code}
684 simplifyCheck :: WantedConstraints      -- Wanted
685               -> TcM (Bag EvBind)
686 -- Solve a single, top-level implication constraint
687 -- e.g. typically one created from a top-level type signature
688 --          f :: forall a. [a] -> [a]
689 --          f x = rhs
690 -- We do this even if the function has no polymorphism:
691 --          g :: Int -> Int
692
693 --          g y = rhs
694 -- (whereas for *nested* bindings we would not create
695 --  an implication constraint for g at all.)
696 --
697 -- Fails if can't solve something in the input wanteds
698 simplifyCheck wanteds
699   = do { wanteds <- zonkWC wanteds
700
701        ; traceTc "simplifyCheck {" (vcat
702              [ ptext (sLit "wanted =") <+> ppr wanteds ])
703
704        ; (unsolved, eb1) <- solveWanteds wanteds
705
706        ; traceTc "simplifyCheck }" $ ptext (sLit "unsolved =") <+> ppr unsolved
707
708        ; traceTc "reportUnsolved {" empty
709        -- See Note [Deferring coercion errors to runtime]
710        ; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
711        ; eb2 <- reportUnsolved runtimeCoercionErrors unsolved 
712        ; traceTc "reportUnsolved }" empty
713
714        ; return (eb1 `unionBags` eb2) }
715 \end{code}
716
717 Note [Deferring coercion errors to runtime]
718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
719
720 While developing, sometimes it is desirable to allow compilation to succeed even
721 if there are type errors in the code. Consider the following case:
722
723   module Main where
724
725   a :: Int
726   a = 'a'
727
728   main = print "b"
729
730 Even though `a` is ill-typed, it is not used in the end, so if all that we're
731 interested in is `main` it is handy to be able to ignore the problems in `a`.
732
733 Since we treat type equalities as evidence, this is relatively simple. Whenever
734 we run into a type mismatch in TcUnify, we normally just emit an error. But it
735 is always safe to defer the mismatch to the main constraint solver. If we do
736 that, `a` will get transformed into
737
738   co :: Int ~ Char
739   co = ...
740
741   a :: Int
742   a = 'a' `cast` co
743
744 The constraint solver would realize that `co` is an insoluble constraint, and
745 emit an error with `reportUnsolved`. But we can also replace the right-hand side
746 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
747 to compile, and it will run fine unless we evaluate `a`. This is what
748 `deferErrorsToRuntime` does.
749
750 It does this by keeping track of which errors correspond to which coercion
751 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
752 and does not fail if -fwarn-type-errors is on, so that we can continue
753 compilation. The errors are turned into warnings in `reportUnsolved`.
754
755 \begin{code}
756
757 solveWanteds :: WantedConstraints -> TcM (WantedConstraints, Bag EvBind)
758 -- Return the evidence binds in the BagEvBinds result
759 solveWanteds wanted = runTcS $ solve_wanteds wanted 
760
761 solveWantedsWithEvBinds :: EvBindsVar -> WantedConstraints -> TcM WantedConstraints
762 -- Side-effect the EvBindsVar argument to add new bindings from solving
763 solveWantedsWithEvBinds ev_binds_var wanted
764   = runTcSWithEvBinds ev_binds_var $ solve_wanteds wanted
765
766
767 solve_wanteds :: WantedConstraints -> TcS WantedConstraints 
768 -- NB: wc_flats may be wanted /or/ derived now
769 solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols }) 
770   = do { traceTcS "solveWanteds {" (ppr wanted)
771
772          -- Try the flat bit, including insolubles. Solving insolubles a 
773          -- second time round is a bit of a waste but the code is simple 
774          -- and the program is wrong anyway. 
775          -- Why keepWanted insols? See Note [KeepWanted in SolveWanteds] 
776        ; let all_flats = flats `unionBags` keepWanted insols
777              -- DV: Used to be 'keepWanted insols' but just insols is
778                          
779        ; impls_from_flats <- solveInteractCts $ bagToList all_flats
780
781        -- solve_wanteds iterates when it is able to float equalities 
782        -- out of one or more of the implications. 
783        ; unsolved_implics <- simpl_loop 1 (implics `unionBags` impls_from_flats)
784
785        ; (insoluble_flats,unsolved_flats) <- extractUnsolvedTcS 
786
787        ; bb <- getTcEvBindsMap
788        ; tb <- getTcSTyBindsMap
789
790        ; traceTcS "solveWanteds }" $
791                  vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
792                       , text "unsolved_implics =" <+> ppr unsolved_implics
793                       , text "current evbinds  =" <+> ppr (evBindMapBinds bb)
794                       , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
795                       ]
796
797        ; let wc =  WC { wc_flat  = unsolved_flats
798                       , wc_impl  = unsolved_implics
799                       , wc_insol = insoluble_flats }
800
801
802        ; traceTcS "solveWanteds finished with" $
803                  vcat [ text "wc (unflattened) =" <+> ppr wc ]
804
805        ; unFlattenWC wc }
806
807
808
809 simpl_loop :: Int
810            -> Bag Implication
811            -> TcS (Bag Implication)
812 simpl_loop n implics
813   | n > 10 
814   = traceTcS "solveWanteds: loop!" empty >> return implics
815   | otherwise 
816   = do { (implic_eqs, unsolved_implics) <- solveNestedImplications implics
817
818        ; inerts <- getTcSInerts
819        ; let ((_,unsolved_flats),_) = extractUnsolved inerts
820                                       
821        ; let improve_eqs = implic_eqs
822              -- NB: improve_eqs used to contain defaulting equations HERE but 
823              -- defaulting now happens only at simplifyTop and not deep inside 
824              -- simpl_loop! See Note [Top-level Defaulting Plan]
825              
826        ; traceTcS "solveWanteds: simpl_loop end" $
827              vcat [ text "improve_eqs      =" <+> ppr improve_eqs
828                   , text "unsolved_flats   =" <+> ppr unsolved_flats
829                   , text "unsolved_implics =" <+> ppr unsolved_implics ]
830
831        ; if isEmptyBag improve_eqs then return unsolved_implics 
832          else do { impls_from_eqs <- solveInteractCts $ bagToList improve_eqs
833                  ; simpl_loop (n+1) (unsolved_implics `unionBags` 
834                                                  impls_from_eqs)} }
835
836 solveNestedImplications :: Bag Implication
837                         -> TcS (Cts, Bag Implication)
838 -- Precondition: the TcS inerts may contain unsolved flats which have 
839 -- to be converted to givens before we go inside a nested implication.
840 solveNestedImplications implics
841   | isEmptyBag implics
842   = return (emptyBag, emptyBag)
843   | otherwise 
844   = do { inerts <- getTcSInerts
845        ; traceTcS "solveNestedImplications starting, inerts are:" $ ppr inerts
846          
847        ; let ((_insoluble_flats, unsolved_flats),thinner_inerts) = extractUnsolved inerts 
848        ; traceTcS "solveNestedImplications starting, more info:" $ 
849          vcat [ text "inerts          = " <+> ppr inerts
850               , text "insoluble_flats = " <+> ppr _insoluble_flats
851               , text "unsolved_flats  = " <+> ppr unsolved_flats
852               , text "thinner_inerts  = " <+> ppr thinner_inerts ]
853          
854        ; (implic_eqs, unsolved_implics)
855            <- doWithInert thinner_inerts $ 
856               do { let pushed_givens = givens_from_wanteds unsolved_flats
857                        tcs_untouchables 
858                          = foldr (unionVarSet . tyVarsOfCt) emptyVarSet pushed_givens
859                                           -- Typically pushed_givens is very small, consists
860                                           -- only of unsolved equalities, so no inefficiency 
861                                           -- danger.
862                                                                                     
863                                           
864                  -- See Note [Preparing inert set for implications]
865                  -- Push the unsolved wanteds inwards, but as givens
866                  ; traceTcS "solveWanteds: preparing inerts for implications {" $ 
867                    vcat [ppr tcs_untouchables, ppr pushed_givens]
868                  ; impls_from_givens <- solveInteractCts pushed_givens
869                                         
870                  ; MASSERT (isEmptyBag impls_from_givens)
871                        -- impls_from_givens must be empty, since we are reacting givens
872                        -- with givens, and they can never generate extra implications 
873                        -- from decomposition of ForAll types. (Whereas wanteds can, see
874                        -- TcCanonical, canEq ForAll-ForAll case)
875                    
876                  ; traceTcS "solveWanteds: } now doing nested implications {" empty
877                  ; flatMapBagPairM (solveImplication tcs_untouchables) implics }
878
879        -- ... and we are back in the original TcS inerts 
880        -- Notice that the original includes the _insoluble_flats so it was safe to ignore
881        -- them in the beginning of this function.
882        ; traceTcS "solveWanteds: done nested implications }" $
883                   vcat [ text "implic_eqs ="       <+> ppr implic_eqs
884                        , text "unsolved_implics =" <+> ppr unsolved_implics ]
885
886        ; return (implic_eqs, unsolved_implics) }
887
888   where givens_from_wanteds = foldrBag get_wanted []
889         get_wanted cc rest_givens
890             | pushable_wanted cc
891             = let fl   = ctEvidence cc
892                   gfl  = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol
893                                , ctev_evtm = EvId (ctev_evar fl)
894                                , ctev_pred = ctev_pred fl }
895                   this_given = cc { cc_ev = gfl }
896               in this_given : rest_givens
897             | otherwise = rest_givens 
898
899         pushable_wanted :: Ct -> Bool 
900         pushable_wanted cc 
901          | isWantedCt cc 
902          = isEqPred (ctPred cc) -- see Note [Preparing inert set for implications]
903          | otherwise = False 
904
905 solveImplication :: TcTyVarSet     -- Untouchable TcS unification variables
906                  -> Implication    -- Wanted
907                  -> TcS (Cts,      -- All wanted or derived floated equalities: var = type
908                          Bag Implication) -- Unsolved rest (always empty or singleton)
909 -- Precondition: The TcS monad contains an empty worklist and given-only inerts 
910 -- which after trying to solve this implication we must restore to their original value
911 solveImplication tcs_untouchables
912      imp@(Implic { ic_untch  = untch
913                  , ic_binds  = ev_binds
914                  , ic_skols  = skols 
915                  , ic_given  = givens
916                  , ic_wanted = wanteds
917                  , ic_loc    = loc })
918   = shadowIPs givens $    -- See Note [Shadowing of Implicit Parameters]
919     nestImplicTcS ev_binds (untch, tcs_untouchables) $
920     recoverTcS (return (emptyBag, emptyBag)) $
921        -- Recover from nested failures.  Even the top level is
922        -- just a bunch of implications, so failing at the first one is bad
923     do { traceTcS "solveImplication {" (ppr imp) 
924
925          -- Solve flat givens
926        ; impls_from_givens <- solveInteractGiven loc givens 
927        ; MASSERT (isEmptyBag impls_from_givens)
928          
929          -- Simplify the wanteds
930        ; WC { wc_flat = unsolved_flats
931             , wc_impl = unsolved_implics
932             , wc_insol = insols } <- solve_wanteds wanteds
933
934        ; let (res_flat_free, res_flat_bound)
935                  = floatEqualities skols givens unsolved_flats
936
937        ; let res_wanted = WC { wc_flat  = keepWanted $ res_flat_bound
938                                -- I think this keepWanted must eventually go away, but it is
939                                -- a real code-breaking change. 
940                                -- See Note [KeepWanted in SolveImplication]
941                              , wc_impl  = unsolved_implics
942                              , wc_insol = insols }
943
944              res_implic = unitImplication $
945                           imp { ic_wanted = res_wanted
946                               , ic_insol  = insolubleWC res_wanted }
947
948        ; evbinds <- getTcEvBindsMap
949
950        ; traceTcS "solveImplication end }" $ vcat
951              [ text "res_flat_free =" <+> ppr res_flat_free
952              , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds)
953              , text "res_implic =" <+> ppr res_implic ]
954
955        ; return (res_flat_free, res_implic) }
956     -- and we are back to the original inerts
957
958 \end{code}
959
960 Note [KeepWanted in SolveWanteds]
961 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
962 Why do we have:
963    let all_flats = flats `unionBags` keepWanted insols
964 instead of the simpler:
965    let all_flats = flats `unionBags` insols
966 in solve_wanteds?
967
968 Assume a top-level class and instance declaration:
969
970   class D a b | a -> b 
971   instance D [a] [a] 
972
973 Assume we have started with an implication:
974
975   forall c. Eq c => { wc_flat = D [c] c [W] }
976
977 which we have simplified to:
978
979   forall c. Eq c => { wc_flat = D [c] c [W]
980                     , wc_insols = (c ~ [c]) [D] }
981
982 For some reason, e.g. because we floated an equality somewhere else,
983 we might try to re-solve this implication. If we do not do a
984 keepWanted, then we will end up trying to solve the following
985 constraints the second time:
986
987   (D [c] c) [W]
988   (c ~ [c]) [D]
989
990 which will result in two Deriveds to end up in the insoluble set:
991
992   wc_flat   = D [c] c [W]
993   wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
994
995 which can result in reporting the same error twice.  
996
997 So, do we /lose/ some potentially useful information by doing this? 
998
999 No, because the insoluble Derived/Given are going to be equalities, 
1000 which are going to be derivable anyway from the rest of the flat 
1001 constraints. 
1002
1003
1004 Note [KeepWanted in SolveImplication]
1005 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1006
1007 Here is a real example, 
1008 stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
1009
1010   class C a b | a -> b
1011   g :: C a b => a -> b -> () 
1012   f :: C a b => a -> b -> () 
1013   f xa xb = 
1014       let loop = g xa 
1015       in loop xb
1016
1017 We will first try to infer a type for loop, and we will succeed:
1018     C a b' => b' -> ()
1019 Subsequently, we will type check (loop xb) and all is good. But, 
1020 recall that we have to solve a final implication constraint: 
1021     C a b => (C a b' => .... cts from body of loop .... )) 
1022 And now we have a problem as we will generate an equality b ~ b' and fail to 
1023 solve it. 
1024
1025 I actually think this is a legitimate behaviour (to fail). After all, if we had 
1026 given the inferred signature to foo we would have failed as well, but we have to 
1027 find a workaround because library code breaks.
1028
1029 For now I keep the 'keepWanted' though it seems problematic e.g. we might discard 
1030 a useful Derived!
1031
1032 \begin{code}
1033
1034
1035 floatEqualities :: [TcTyVar] -> [EvVar] -> Cts -> (Cts, Cts)
1036 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
1037 -- and come from the input wanted ev vars or deriveds 
1038 floatEqualities skols can_given wantders
1039   | hasEqualities can_given = (emptyBag, wantders)
1040           -- Note [Float Equalities out of Implications]
1041   | otherwise = partitionBag is_floatable wantders
1042   where skol_set = mkVarSet skols
1043         is_floatable :: Ct -> Bool
1044         is_floatable ct
1045           | ct_predty <- ctPred ct
1046           , isEqPred ct_predty
1047           = skol_set `disjointVarSet` tvs_under_fsks ct_predty
1048         is_floatable _ct = False
1049
1050         tvs_under_fsks :: Type -> TyVarSet
1051         -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
1052         tvs_under_fsks (TyVarTy tv)     
1053           | not (isTcTyVar tv)               = unitVarSet tv
1054           | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
1055           | otherwise                        = unitVarSet tv
1056         tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
1057         tvs_under_fsks (LitTy {})       = emptyVarSet
1058         tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
1059         tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
1060         tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder 
1061                                         -- can mention type variables!
1062           | isTyVar tv                = inner_tvs `delVarSet` tv
1063           | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
1064                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
1065           where
1066             inner_tvs = tvs_under_fsks ty
1067
1068 shadowIPs :: [EvVar] -> TcS a -> TcS a
1069 shadowIPs gs m
1070   | null shadowed = m
1071   | otherwise     = do is <- getTcSInerts
1072                        doWithInert (purgeShadowed is) m
1073   where
1074   shadowed  = mapMaybe isIP gs
1075
1076   isIP g    = do p <- evVarPred_maybe g
1077                  (x,_) <- isIPPred_maybe p
1078                  return x
1079
1080   isShadowedCt ct = isShadowedEv (ctEvidence ct)
1081   isShadowedEv ev = case isIPPred_maybe (ctEvPred ev) of
1082                       Just (x,_) -> x `elem` shadowed
1083                       _          -> False
1084
1085   purgeShadowed is = is { inert_cans = purgeCans (inert_cans is)
1086                         , inert_solved = purgeSolved (inert_solved is)
1087                         }
1088
1089   purgeDicts    = snd . partitionCCanMap isShadowedCt
1090   purgeCans ics = ics { inert_dicts = purgeDicts (inert_dicts ics) }
1091   purgeSolved   = filterSolved (not . isShadowedEv)
1092 \end{code}
1093
1094 Note [Preparing inert set for implications]
1095 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1096 Before solving the nested implications, we convert any unsolved flat wanteds
1097 to givens, and add them to the inert set.  Reasons:
1098
1099   a) In checking mode, suppresses unnecessary errors.  We already have
1100      on unsolved-wanted error; adding it to the givens prevents any 
1101      consequential errors from showing up
1102
1103   b) More importantly, in inference mode, we are going to quantify over this
1104      constraint, and we *don't* want to quantify over any constraints that
1105      are deducible from it.
1106
1107   c) Flattened type-family equalities must be exposed to the nested
1108      constraints.  Consider
1109         F b ~ alpha, (forall c.  F b ~ alpha)
1110      Obviously this is soluble with [alpha := F b].  But the
1111      unification is only done by solveCTyFunEqs, right at the end of
1112      solveWanteds, and if we aren't careful we'll end up with an
1113      unsolved goal inside the implication.  We need to "push" the
1114      as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
1115      can be used to solve the inner (F b
1116      ~ alpha).  See Trac #4935.
1117
1118   d) There are other cases where interactions between wanteds that can help
1119      to solve a constraint. For example
1120
1121         class C a b | a -> b
1122
1123         (C Int alpha), (forall d. C d blah => C Int a)
1124
1125      If we push the (C Int alpha) inwards, as a given, it can produce
1126      a fundep (alpha~a) and this can float out again and be used to
1127      fix alpha.  (In general we can't float class constraints out just
1128      in case (C d blah) might help to solve (C Int a).)
1129
1130 The unsolved wanteds are *canonical* but they may not be *inert*,
1131 because when made into a given they might interact with other givens.
1132 Hence the call to solveInteract.  Example:
1133
1134  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta]) 
1135
1136 We were not able to solve (a ~w [beta]) but we can't just assume it as
1137 given because the resulting set is not inert. Hence we have to do a
1138 'solveInteract' step first. 
1139
1140 Finally, note that we convert them to [Given] and NOT [Given/Solved].
1141 The reason is that Given/Solved are weaker than Givens and may be discarded.
1142 As an example consider the inference case, where we may have, the following 
1143 original constraints: 
1144      [Wanted] F Int ~ Int
1145              (F Int ~ a => F Int ~ a)
1146 If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next 
1147 given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting 
1148 the (F Int ~ a) insoluble. Hence we should really convert the residual 
1149 wanteds to plain old Given. 
1150
1151 We need only push in unsolved equalities both in checking mode and inference mode: 
1152
1153   (1) In checking mode we should not push given dictionaries in because of
1154 example LongWayOverlapping.hs, where we might get strange overlap
1155 errors between far-away constraints in the program.  But even in
1156 checking mode, we must still push type family equations. Consider:
1157
1158    type instance F True a b = a 
1159    type instance F False a b = b
1160
1161    [w] F c a b ~ gamma 
1162    (c ~ True) => a ~ gamma 
1163    (c ~ False) => b ~ gamma
1164
1165 Since solveCTyFunEqs happens at the very end of solving, the only way to solve
1166 the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not 
1167 merely Given/Solved because it has to interact with the top-level instance 
1168 environment) and push it inside the implications. Now, when we come out again at
1169 the end, having solved the implications solveCTyFunEqs will solve this equality.
1170
1171   (2) In inference mode, we recheck the final constraint in checking mode and
1172 hence we will be able to solve inner implications from top-level quantified
1173 constraints nonetheless.
1174
1175
1176 Note [Extra TcsTv untouchables]
1177 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1178
1179 Whenever we are solving a bunch of flat constraints, they may contain 
1180 the following sorts of 'touchable' unification variables:
1181    
1182    (i)   Born-touchables in that scope
1183  
1184    (ii)  Simplifier-generated unification variables, such as unification 
1185          flatten variables
1186
1187    (iii) Touchables that have been floated out from some nested 
1188          implications, see Note [Float Equalities out of Implications]. 
1189
1190 Now, once we are done with solving these flats and have to move inwards to 
1191 the nested implications (perhaps for a second time), we must consider all the
1192 extra variables (categories (ii) and (iii) above) as untouchables for the 
1193 implication. Otherwise we have the danger or double unifications, as well
1194 as the danger of not ``seing'' some unification. Example (from Trac #4494):
1195
1196    (F Int ~ uf)  /\  [untch=beta](forall a. C a => F Int ~ beta) 
1197
1198 In this example, beta is touchable inside the implication. The 
1199 first solveInteract step leaves 'uf' ununified. Then we move inside 
1200 the implication where a new constraint
1201        uf  ~  beta  
1202 emerges. We may spontaneously solve it to get uf := beta, so the whole
1203 implication disappears but when we pop out again we are left with (F
1204 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
1205 uf will get unified *once more* to (F Int).
1206
1207 The solution is to record the unification variables of the flats, 
1208 and make them untouchables for the nested implication. In the 
1209 example above uf would become untouchable, so beta would be forced 
1210 to be unified as beta := uf.
1211
1212 Note [Float Equalities out of Implications]
1213 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1214 For ordinary pattern matches (including existentials) we float 
1215 equalities out of implications, for instance: 
1216      data T where 
1217        MkT :: Eq a => a -> T 
1218      f x y = case x of MkT _ -> (y::Int)
1219 We get the implication constraint (x::T) (y::alpha): 
1220      forall a. [untouchable=alpha] Eq a => alpha ~ Int
1221 We want to float out the equality into a scope where alpha is no
1222 longer untouchable, to solve the implication!  
1223
1224 But we cannot float equalities out of implications whose givens may
1225 yield or contain equalities:
1226
1227       data T a where 
1228         T1 :: T Int
1229         T2 :: T Bool
1230         T3 :: T a 
1231         
1232       h :: T a -> a -> Int
1233       
1234       f x y = case x of 
1235                 T1 -> y::Int
1236                 T2 -> y::Bool
1237                 T3 -> h x y
1238
1239 We generate constraint, for (x::T alpha) and (y :: beta): 
1240    [untouchables = beta] (alpha ~ Int => beta ~ Int)   -- From 1st branch
1241    [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1242    (alpha ~ beta)                                      -- From 3rd branch 
1243
1244 If we float the equality (beta ~ Int) outside of the first implication and 
1245 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1246 But if we just leave them inside the implications we unify alpha := beta and
1247 solve everything.
1248
1249 Principle: 
1250     We do not want to float equalities out which may need the given *evidence*
1251     to become soluble.
1252
1253 Consequence: classes with functional dependencies don't matter (since there is 
1254 no evidence for a fundep equality), but equality superclasses do matter (since 
1255 they carry evidence).
1256
1257 Notice that, due to Note [Extra TcSTv Untouchables], the free unification variables 
1258 of an equality that is floated out of an implication become effectively untouchables
1259 for the leftover implication. This is absolutely necessary. Consider the following 
1260 example. We start with two implications and a class with a functional dependency. 
1261
1262 class C x y | x -> y
1263 instance C [a] [a]
1264       
1265 (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
1266 (I2)      [untch=beta]forall b. 0 => F Int ~ [[alpha]] /\ C beta [b]
1267
1268 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2. 
1269 They may react to yield that (beta := [alpha]) which can then be pushed inwards 
1270 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1271 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1272 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1273
1274 class C x y | x -> y where 
1275  op :: x -> y -> ()
1276
1277 instance C [a] [a]
1278
1279 type family F a :: *
1280
1281 h :: F Int -> ()
1282 h = undefined
1283
1284 data TEx where 
1285   TEx :: a -> TEx 
1286
1287
1288 f (x::beta) = 
1289     let g1 :: forall b. b -> ()
1290         g1 _ = h [x]
1291         g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1292     in (g1 '3', g2 undefined)
1293
1294 Note [Shadowing of Implicit Parameters]
1295 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1296 Consider the following example:
1297
1298 f :: (?x :: Char) => Char
1299 f = let ?x = 'a' in ?x
1300
1301 The "let ?x = ..." generates an implication constraint of the form:
1302
1303 ?x :: Char => ?x :: Char
1304
1305
1306 Furthermore, the signature for `f` also generates an implication
1307 constraint, so we end up with the following nested implication:
1308
1309 ?x :: Char => (?x :: Char => ?x :: Char)
1310
1311 Note that the wanted (?x :: Char) constraint may be solved in
1312 two incompatible ways:  either by using the parameter from the
1313 signature, or by using the local definition.  Our intention is
1314 that the local definition should "shadow" the parameter of the
1315 signature, and we implement this as follows: when we nest implications,
1316 we remove any implicit parameters in the outer implication, that
1317 have the same name as givens of the inner implication.
1318
1319 Here is another variation of the example:
1320
1321 f :: (?x :: Int) => Char
1322 f = let ?x = 'x' in ?x
1323
1324 This program should also be accepted: the two constraints `?x :: Int`
1325 and `?x :: Char` never exist in the same context, so they don't get to
1326 interact to cause failure.
1327 \begin{code}
1328
1329
1330
1331 unFlattenWC :: WantedConstraints -> TcS WantedConstraints
1332 unFlattenWC wc 
1333   = do { (subst, remaining_unsolved_flats) <- solveCTyFunEqs (wc_flat wc)
1334                 -- See Note [Solving Family Equations]
1335                 -- NB: remaining_flats has already had subst applied
1336        ; return $ 
1337          WC { wc_flat  = mapBag (substCt subst) remaining_unsolved_flats
1338             , wc_impl  = mapBag (substImplication subst) (wc_impl wc) 
1339             , wc_insol = mapBag (substCt subst) (wc_insol wc) }
1340        }
1341   where 
1342     solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)
1343     -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
1344     -- See Note [Solving Family Equations]
1345     -- Returns: a bunch of unsolved constraints from the original Cts and implications
1346     --          where the newly generated equalities (alpha := F xi) have been substituted through.
1347     solveCTyFunEqs cts
1348      = do { untch   <- getUntouchables 
1349           ; let (unsolved_can_cts, (ni_subst, cv_binds))
1350                     = getSolvableCTyFunEqs untch cts
1351           ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
1352                                               , ppr ni_subst, ppr cv_binds
1353                                               ])
1354           ; mapM_ solve_one cv_binds
1355
1356           ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
1357       where
1358         solve_one (Wanted { ctev_evar = cv }, tv, ty) 
1359           = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
1360         solve_one (Derived {}, tv, ty)
1361           = setWantedTyBind tv ty
1362         solve_one arg
1363           = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
1364
1365 ------------
1366 type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
1367   -- The TvSubstEnv is not idempotent, but is loop-free
1368   -- See Note [Non-idempotent substitution] in Unify
1369 emptyFunEqBinds :: FunEqBinds
1370 emptyFunEqBinds = (emptyVarEnv, [])
1371
1372 extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
1373 extendFunEqBinds (tv_subst, cv_binds) fl tv ty
1374   = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
1375
1376 ------------
1377 getSolvableCTyFunEqs :: TcsUntouchables
1378                      -> Cts                -- Precondition: all Wanteds or Derived!
1379                      -> (Cts, FunEqBinds)  -- Postcondition: returns the unsolvables
1380 getSolvableCTyFunEqs untch cts
1381   = Bag.foldlBag dflt_funeq (emptyCts, emptyFunEqBinds) cts
1382   where
1383     dflt_funeq :: (Cts, FunEqBinds) -> Ct
1384                -> (Cts, FunEqBinds)
1385     dflt_funeq (cts_in, feb@(tv_subst, _))
1386                (CFunEqCan { cc_ev = fl
1387                           , cc_fun = tc
1388                           , cc_tyargs = xis
1389                           , cc_rhs = xi })
1390       | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
1391
1392       , isTouchableMetaTyVar_InRange untch tv
1393            -- And it's a *touchable* unification variable
1394
1395       , typeKind xi `tcIsSubKind` tyVarKind tv
1396          -- Must do a small kind check since TcCanonical invariants 
1397          -- on family equations only impose compatibility, not subkinding
1398
1399       , not (tv `elemVarEnv` tv_subst)
1400            -- Check not in extra_binds
1401            -- See Note [Solving Family Equations], Point 1
1402
1403       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1404            -- Occurs check: see Note [Solving Family Equations], Point 2
1405       = ASSERT ( not (isGiven fl) )
1406         (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
1407
1408     dflt_funeq (cts_in, fun_eq_binds) ct
1409       = (cts_in `extendCts` ct, fun_eq_binds)
1410 \end{code}
1411
1412 Note [Solving Family Equations] 
1413 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1414 After we are done with simplification we may be left with constraints of the form:
1415      [Wanted] F xis ~ beta 
1416 If 'beta' is a touchable unification variable not already bound in the TyBinds 
1417 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1418
1419 When is it ok to do so? 
1420     1) 'beta' must not already be defaulted to something. Example: 
1421
1422            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
1423            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
1424                                        have to report this as unsolved.
1425
1426     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
1427        set [beta := F xis] only if beta is not among the free variables of xis.
1428
1429     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
1430        of type family equations. See Inert Set invariants in TcInteract. 
1431
1432
1433 *********************************************************************************
1434 *                                                                               * 
1435 *                          Defaulting and disamgiguation                        *
1436 *                                                                               *
1437 *********************************************************************************
1438 \begin{code}
1439 applyDefaultingRules :: Cts      -- Wanteds or Deriveds
1440                      -> TcS Cts  -- Derived equalities 
1441 -- Return some extra derived equalities, which express the
1442 -- type-class default choice. 
1443 applyDefaultingRules wanteds
1444   | isEmptyBag wanteds 
1445   = return emptyBag
1446   | otherwise
1447   = do { traceTcS "applyDefaultingRules { " $ 
1448                   text "wanteds =" <+> ppr wanteds
1449                   
1450        ; info@(default_tys, _) <- getDefaultInfo
1451        ; let groups = findDefaultableGroups info wanteds
1452        ; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups
1453                                                  , text "info=" <+> ppr info ]
1454        ; deflt_cts <- mapM (disambigGroup default_tys) groups
1455
1456        ; traceTcS "applyDefaultingRules }" $ 
1457                   vcat [ text "Type defaults =" <+> ppr deflt_cts]
1458
1459        ; return (unionManyBags deflt_cts) }
1460 \end{code}
1461
1462 Note [tryTcS in defaulting]
1463 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1464
1465 defaultTyVar and disambigGroup create new evidence variables for
1466 default equations, and hence update the EvVar cache. However, after
1467 applyDefaultingRules we will try to solve these default equations
1468 using solveInteractCts, which will consult the cache and solve those
1469 EvVars from themselves! That's wrong.
1470
1471 To avoid this problem we guard defaulting under a @tryTcS@ which leaves
1472 the original cache unmodified.
1473
1474 There is a second reason for @tryTcS@ in defaulting: disambGroup does
1475 some constraint solving to determine if a default equation is
1476 ``useful'' in solving some wanted constraints, but we want to
1477 discharge all evidence and unifications that may have happened during
1478 this constraint solving.
1479
1480 Finally, @tryTcS@ importantly does not inherit the original cache from
1481 the higher level but makes up a new cache, the reason is that disambigGroup
1482 will call solveInteractCts so the new derived and the wanteds must not be 
1483 in the cache!
1484
1485
1486 \begin{code}
1487 ------------------
1488 touchablesOfWC :: WantedConstraints -> TcTyVarSet
1489 -- See Note [Extra Tcs Untouchables] to see why we carry a TcsUntouchables 
1490 -- instead of just using the Untouchable range have in our hands.
1491 touchablesOfWC = go (NoUntouchables, emptyVarSet)
1492   where go :: TcsUntouchables -> WantedConstraints -> TcTyVarSet
1493         go untch (WC { wc_flat = flats, wc_impl = impls }) 
1494           = filterVarSet is_touchable flat_tvs `unionVarSet`
1495               foldrBag (unionVarSet . (go_impl $ untch_for_impls untch)) emptyVarSet impls 
1496           where is_touchable = isTouchableMetaTyVar_InRange untch
1497                 flat_tvs = tyVarsOfCts flats
1498                 untch_for_impls (r,uset) = (r, uset `unionVarSet` flat_tvs)
1499         go_impl (_rng,set) implic = go (ic_untch implic,set) (ic_wanted implic)
1500
1501 applyTyVarDefaulting :: WantedConstraints -> TcM Cts
1502 applyTyVarDefaulting wc = runTcS do_dflt >>= (return . fst)
1503   where do_dflt = do { tv_cts <- mapM defaultTyVar $ 
1504                                  varSetElems (touchablesOfWC wc)
1505                      ; return (unionManyBags tv_cts) }
1506
1507 defaultTyVar :: TcTyVar -> TcS Cts
1508 -- Precondition: a touchable meta-variable
1509 defaultTyVar the_tv
1510   | not (k `eqKind` default_k)
1511   -- Why tryTcS? See Note [tryTcS in defaulting]
1512   = tryTcS $
1513     do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1514        ; ty_k <- instFlexiTcSHelperTcS (tyVarName the_tv) default_k
1515        ; md <- newDerived loc (mkTcEqPred (mkTyVarTy the_tv) ty_k)
1516              -- Why not directly newDerived loc (mkTcEqPred k default_k)? 
1517              -- See Note [DefaultTyVar]
1518        ; let cts
1519               | Just der_ev <- md = [mkNonCanonical der_ev]
1520               | otherwise = []
1521        
1522        ; implics_from_defaulting <- solveInteractCts cts
1523        ; MASSERT (isEmptyBag implics_from_defaulting)
1524          
1525        ; (_,unsolved) <- extractUnsolvedTcS
1526        ; if isEmptyBag (keepWanted unsolved) then return (listToBag cts)
1527          else return emptyBag }
1528   | otherwise = return emptyBag  -- The common case
1529   where
1530     k = tyVarKind the_tv
1531     default_k = defaultKind k
1532 \end{code}
1533
1534 Note [DefaultTyVar]
1535 ~~~~~~~~~~~~~~~~~~~
1536 defaultTyVar is used on any un-instantiated meta type variables to
1537 default the kind of OpenKind and ArgKind etc to *.  This is important 
1538 to ensure that instance declarations match.  For example consider
1539
1540      instance Show (a->b)
1541      foo x = show (\_ -> True)
1542
1543 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
1544 and that won't match the typeKind (*) in the instance decl.  See tests
1545 tc217 and tc175.
1546
1547 We look only at touchable type variables. No further constraints
1548 are going to affect these type variables, so it's time to do it by
1549 hand.  However we aren't ready to default them fully to () or
1550 whatever, because the type-class defaulting rules have yet to run.
1551
1552 An important point is that if the type variable tv has kind k and the
1553 default is default_k we do not simply generate [D] (k ~ default_k) because:
1554
1555    (1) k may be ArgKind and default_k may be * so we will fail
1556
1557    (2) We need to rewrite all occurrences of the tv to be a type
1558        variable with the right kind and we choose to do this by rewriting 
1559        the type variable /itself/ by a new variable which does have the 
1560        right kind.
1561
1562 \begin{code}
1563
1564
1565 ----------------
1566 findDefaultableGroups 
1567     :: ( [Type]
1568        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1569     -> Cts              -- Unsolved (wanted or derived)
1570     -> [[(Ct,TcTyVar)]]
1571 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1572   | null default_tys             = []
1573   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1574   where 
1575     unaries     :: [(Ct, TcTyVar)]  -- (C tv) constraints
1576     non_unaries :: [Ct]             -- and *other* constraints
1577     
1578     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1579         -- Finds unary type-class constraints
1580     find_unary cc@(CDictCan { cc_tyargs = [ty] })
1581         | Just tv <- tcGetTyVar_maybe ty
1582         = Left (cc, tv)
1583     find_unary cc = Right cc  -- Non unary or non dictionary 
1584
1585     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
1586     bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries 
1587
1588     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1589
1590     is_defaultable_group ds@((_,tv):_)
1591         = let b1 = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
1592               b2 = not (tv `elemVarSet` bad_tvs)
1593               b4 = defaultable_classes [cc_class cc | (cc,_) <- ds]
1594           in (b1 && b2 && b4)
1595     is_defaultable_group [] = panic "defaultable_group"
1596
1597     defaultable_classes clss 
1598         | extended_defaults = any isInteractiveClass clss
1599         | otherwise         = all is_std_class clss && (any is_num_class clss)
1600
1601     -- In interactive mode, or with -XExtendedDefaultRules,
1602     -- we default Show a to Show () to avoid graututious errors on "show []"
1603     isInteractiveClass cls 
1604         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1605
1606     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1607     -- is_num_class adds IsString to the standard numeric classes, 
1608     -- when -foverloaded-strings is enabled
1609
1610     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1611     -- Similarly is_std_class
1612
1613 ------------------------------
1614 disambigGroup :: [Type]           -- The default types 
1615               -> [(Ct, TcTyVar)]  -- All classes of the form (C a)
1616                                   --  sharing same type variable
1617               -> TcS Cts
1618
1619 disambigGroup []  _grp
1620   = return emptyBag
1621 disambigGroup (default_ty:default_tys) group
1622   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1623        ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
1624                     do { derived_eq <- tryTcS $ 
1625                        -- I need a new tryTcS because we will call solveInteractCts below!
1626                             do { md <- newDerived (ctev_wloc the_fl) 
1627                                                   (mkTcEqPred (mkTyVarTy the_tv) default_ty)
1628                                                   -- ctev_wloc because constraint is not Given!
1629                                ; case md of 
1630                                     Nothing   -> return []
1631                                     Just ctev -> return [ mkNonCanonical ctev ] }
1632                             
1633                        ; traceTcS "disambigGroup (solving) {" $
1634                          text "trying to solve constraints along with default equations ..."
1635                        ; implics_from_defaulting <- 
1636                                     solveInteractCts (derived_eq ++ wanteds)
1637                        ; MASSERT (isEmptyBag implics_from_defaulting)
1638                            -- I am not certain if any implications can be generated
1639                            -- but I am letting this fail aggressively if this ever happens.
1640                                      
1641                        ; (_,unsolved) <- extractUnsolvedTcS 
1642                        ; traceTcS "disambigGroup (solving) }" $
1643                          text "disambigGroup unsolved =" <+> ppr (keepWanted unsolved)
1644                        ; if isEmptyBag (keepWanted unsolved) then -- Don't care about Derived's
1645                              return (Just $ listToBag derived_eq) 
1646                          else 
1647                              return Nothing 
1648                        }
1649        ; case success of
1650            Just cts -> -- Success: record the type variable binding, and return
1651                     do { wrapWarnTcS $ warnDefaulting wanteds default_ty
1652                        ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1653                        ; return cts }
1654            Nothing -> -- Failure: try with the next type
1655                     do { traceTcS "disambigGroup failed, will try other default types"
1656                                   (ppr default_ty)
1657                        ; disambigGroup default_tys group } }
1658   where
1659     ((the_ct,the_tv):_) = group
1660     the_fl              = cc_ev the_ct
1661     wanteds             = map fst group
1662 \end{code}
1663
1664 Note [Avoiding spurious errors]
1665 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1666 When doing the unification for defaulting, we check for skolem
1667 type variables, and simply don't default them.  For example:
1668    f = (*)      -- Monomorphic
1669    g :: Num a => a -> a
1670    g x = f x x
1671 Here, we get a complaint when checking the type signature for g,
1672 that g isn't polymorphic enough; but then we get another one when
1673 dealing with the (Num a) context arising from f's definition;
1674 we try to unify a with Int (to default it), but find that it's
1675 already been unified with the rigid variable from g's type sig
1676
1677
1678
1679 *********************************************************************************
1680 *                                                                               * 
1681 *                   Utility functions
1682 *                                                                               *
1683 *********************************************************************************
1684
1685 \begin{code}
1686 newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
1687 newFlatWanteds orig theta
1688   = do { loc <- getCtLoc orig
1689        ; mapM (inst_to_wanted loc) theta }
1690   where 
1691     inst_to_wanted loc pty 
1692           = do { v <- TcMType.newWantedEvVar pty 
1693                ; return $ 
1694                  CNonCanonical { cc_ev = Wanted { ctev_evar = v
1695                                                 , ctev_wloc = loc
1696                                                 , ctev_pred = pty }
1697                                , cc_depth = 0 } }
1698 \end{code}