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