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