Comments and white space only
[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 as TcM
22 import TcType 
23 import TcSMonad as TcS
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            ; free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc_first_go) 
79            ; let meta_tvs = filterVarSet isMetaTyVar free_tvs
80                    -- zonkTyVarsAndFV: the wc_first_go is not yet zonked
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 (varSetElems 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 <- TcM.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 TcM.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   = do { traceTcS "solveImplication {" (ppr imp) 
803
804          -- Solve the nested constraints
805          -- NB: 'inerts' has empty inert_fsks
806        ; (new_fsks, residual_wanted) 
807             <- nestImplicTcS ev_binds untch inerts $
808                do { solveInteractGiven (mkGivenLoc info env) old_fsks givens 
809                   ; residual_wanted <- solve_wanteds wanteds
810                         -- solve_wanteds, *not* solve_wanteds_and_drop, because
811                         -- we want to retain derived equalities so we can float
812                         -- them out in floatEqualities
813                   ; more_fsks <- getFlattenSkols
814                   ; return (more_fsks ++ old_fsks, residual_wanted) }
815
816        ; (floated_eqs, final_wanted)
817              <- floatEqualities (skols ++ new_fsks) givens residual_wanted
818
819        ; let res_implic | isEmptyWC final_wanted 
820                         = emptyBag
821                         | otherwise
822                         = unitBag (imp { ic_fsks   = new_fsks
823                                        , ic_wanted = dropDerivedWC final_wanted
824                                        , ic_insol  = insolubleWC final_wanted })
825
826        ; evbinds <- getTcEvBindsMap
827        ; traceTcS "solveImplication end }" $ vcat
828              [ text "floated_eqs =" <+> ppr floated_eqs
829              , text "new_fsks =" <+> ppr new_fsks
830              , text "res_implic =" <+> ppr res_implic
831              , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
832
833        ; return (floated_eqs, res_implic) }
834 \end{code}
835
836
837 \begin{code}
838 floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints 
839                 -> TcS (Cts, WantedConstraints)
840 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
841 -- and come from the input wanted ev vars or deriveds 
842 -- Also performs some unifications, adding to monadically-carried ty_binds
843 -- These will be used when processing floated_eqs later
844 floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
845   | hasEqualities can_given 
846   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
847   | otherwise 
848   = do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
849        ; untch <- TcS.getUntouchables
850        ; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
851        ; ty_binds <- getTcSTyBindsMap
852        ; traceTcS "floatEqualities" (vcat [ text "Floated eqs =" <+> ppr float_eqs
853                                           , text "Ty binds =" <+> ppr ty_binds])
854        ; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
855   where 
856     skol_set = growSkols wanteds (mkVarSet skols)
857
858     is_floatable :: Ct -> Bool
859     is_floatable ct
860        = isEqPred pred && skol_set `disjointVarSet` tyVarsOfType pred
861        where
862          pred = ctPred ct
863
864 growSkols :: WantedConstraints -> VarSet -> VarSet
865 -- Find all the type variables that might possibly be unified
866 -- with a type that mentions a skolem.  This test is very conservative.
867 -- I don't *think* we need look inside the implications, because any 
868 -- relevant unification variables in there are untouchable.
869 growSkols (WC { wc_flat = flats }) skols
870   = growThetaTyVars theta skols
871   where
872     theta = foldrBag ((:) . ctPred) [] flats
873
874 promoteTyVar :: Untouchables -> TcTyVar  -> TcS ()
875 -- When we float a constraint out of an implication we must restore
876 -- invariant (MetaTvInv) in Note [Untouchable type variables] in TcType
877 promoteTyVar untch tv 
878   | isFloatedTouchableMetaTyVar untch tv
879   = do { cloned_tv <- TcS.cloneMetaTyVar tv
880        ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
881        ; setWantedTyBind tv (mkTyVarTy rhs_tv) }
882   | otherwise
883   = return ()
884
885 promoteAndDefaultTyVar :: Untouchables -> TcTyVarSet -> TyVar -> TcS ()
886 -- See Note [Promote _and_ default when inferring]
887 promoteAndDefaultTyVar untch gbl_tvs tv
888   = do { tv1 <- if tv `elemVarSet` gbl_tvs 
889                 then return tv
890                 else defaultTyVar tv
891        ; promoteTyVar untch tv1 }
892
893 defaultTyVar :: TcTyVar -> TcS TcTyVar
894 -- Precondition: MetaTyVars only
895 -- See Note [DefaultTyVar]
896 defaultTyVar the_tv
897   | not (k `eqKind` default_k)
898   = do { tv' <- TcS.cloneMetaTyVar the_tv
899        ; let new_tv = setTyVarKind tv' default_k
900        ; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv)
901        ; setWantedTyBind the_tv (mkTyVarTy new_tv)
902        ; return new_tv }
903              -- Why not directly derived_pred = mkTcEqPred k default_k?
904              -- See Note [DefaultTyVar]
905              -- We keep the same Untouchables on tv'
906
907   | otherwise = return the_tv    -- The common case
908   where
909     k = tyVarKind the_tv
910     default_k = defaultKind k
911
912 approximateWC :: WantedConstraints -> Cts
913 -- Postcondition: Wanted or Derived Cts 
914 approximateWC wc 
915   = float_wc emptyVarSet wc
916   where 
917     float_wc :: TcTyVarSet -> WantedConstraints -> Cts
918     float_wc skols (WC { wc_flat = flats, wc_impl = implics }) 
919       = do_bag (float_flat skols)   flats  `unionBags` 
920         do_bag (float_implic skols) implics
921                                  
922     float_implic :: TcTyVarSet -> Implication -> Cts
923     float_implic skols imp
924       | hasEqualities (ic_given imp)  -- Don't float out of equalities
925       = emptyCts                      -- cf floatEqualities
926       | otherwise                     -- See Note [approximateWC]
927       = float_wc skols' (ic_wanted imp)
928       where
929         skols' = skols `extendVarSetList` ic_skols imp `extendVarSetList` ic_fsks imp
930             
931     float_flat :: TcTyVarSet -> Ct -> Cts
932     float_flat skols ct
933       | tyVarsOfCt ct `disjointVarSet` skols 
934       = singleCt ct
935       | otherwise = emptyCts
936         
937     do_bag :: (a -> Bag c) -> Bag a -> Bag c
938     do_bag f = foldrBag (unionBags.f) emptyBag
939 \end{code}
940
941 Note [ApproximateWC]
942 ~~~~~~~~~~~~~~~~~~~~
943 approximateWC takes a constraint, typically arising from the RHS of a
944 let-binding whose type we are *inferring*, and extracts from it some
945 *flat* constraints that we might plausibly abstract over.  Of course
946 the top-level flat constraints are plausible, but we also float constraints
947 out from inside, if the are not captured by skolems.
948
949 However we do *not* float anything out if the implication binds equality
950 constriants, because that defeats the OutsideIn story.  Consider
951    data T a where
952      TInt :: T Int
953      MkT :: T a
954
955    f TInt = 3::Int
956
957 We get the implication (a ~ Int => res ~ Int), where so far we've decided 
958   f :: T a -> res
959 We don't want to float (res~Int) out because then we'll infer  
960   f :: T a -> Int
961 which is only on of the possible types. (GHC 7.6 accidentally *did*
962 float out of such implications, which meant it would happily infer
963 non-principal types.)
964
965 Note [DefaultTyVar]
966 ~~~~~~~~~~~~~~~~~~~
967 defaultTyVar is used on any un-instantiated meta type variables to
968 default the kind of OpenKind and ArgKind etc to *.  This is important 
969 to ensure that instance declarations match.  For example consider
970
971      instance Show (a->b)
972      foo x = show (\_ -> True)
973
974 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
975 and that won't match the typeKind (*) in the instance decl.  See tests
976 tc217 and tc175.
977
978 We look only at touchable type variables. No further constraints
979 are going to affect these type variables, so it's time to do it by
980 hand.  However we aren't ready to default them fully to () or
981 whatever, because the type-class defaulting rules have yet to run.
982
983 An important point is that if the type variable tv has kind k and the
984 default is default_k we do not simply generate [D] (k ~ default_k) because:
985
986    (1) k may be ArgKind and default_k may be * so we will fail
987
988    (2) We need to rewrite all occurrences of the tv to be a type
989        variable with the right kind and we choose to do this by rewriting 
990        the type variable /itself/ by a new variable which does have the 
991        right kind.
992
993 Note [Promote _and_ default when inferring]
994 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
995 When we are inferring a type, we simplify the constraint, and then use
996 approximateWC to produce a list of candidate constraints.  Then we MUST
997
998   a) Promote any meta-tyvars that have been floated out by 
999      approximateWC, to restore invariant (MetaTvInv) described in 
1000      Note [Untouchable type variables] in TcType.
1001
1002   b) Default the kind of any meta-tyyvars that are not mentioned in
1003      in the environment.
1004
1005 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
1006 have an instance (C ((x:*) -> Int)).  The instance doesn't match -- but it
1007 should!  If we don't solve the constraint, we'll stupidly quantify over 
1008 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
1009 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
1010
1011 Note [Float Equalities out of Implications]
1012 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1013 For ordinary pattern matches (including existentials) we float 
1014 equalities out of implications, for instance: 
1015      data T where 
1016        MkT :: Eq a => a -> T 
1017      f x y = case x of MkT _ -> (y::Int)
1018 We get the implication constraint (x::T) (y::alpha): 
1019      forall a. [untouchable=alpha] Eq a => alpha ~ Int
1020 We want to float out the equality into a scope where alpha is no
1021 longer untouchable, to solve the implication!  
1022
1023 But we cannot float equalities out of implications whose givens may
1024 yield or contain equalities:
1025
1026       data T a where 
1027         T1 :: T Int
1028         T2 :: T Bool
1029         T3 :: T a 
1030         
1031       h :: T a -> a -> Int
1032       
1033       f x y = case x of 
1034                 T1 -> y::Int
1035                 T2 -> y::Bool
1036                 T3 -> h x y
1037
1038 We generate constraint, for (x::T alpha) and (y :: beta): 
1039    [untouchables = beta] (alpha ~ Int => beta ~ Int)   -- From 1st branch
1040    [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1041    (alpha ~ beta)                                      -- From 3rd branch 
1042
1043 If we float the equality (beta ~ Int) outside of the first implication and 
1044 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1045 But if we just leave them inside the implications we unify alpha := beta and
1046 solve everything.
1047
1048 Principle: 
1049     We do not want to float equalities out which may need the given *evidence*
1050     to become soluble.
1051
1052 Consequence: classes with functional dependencies don't matter (since there is 
1053 no evidence for a fundep equality), but equality superclasses do matter (since 
1054 they carry evidence).
1055
1056 Note [Promoting unification variables]
1057 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1058 When we float an equality out of an implication we must "promote" free
1059 unification variables of the equality, in order to maintain Invariant
1060 (MetaTvInv) from Note [Untouchable type variables] in TcType.  for the
1061 leftover implication.
1062
1063 This is absolutely necessary. Consider the following example. We start
1064 with two implications and a class with a functional dependency.
1065
1066     class C x y | x -> y
1067     instance C [a] [a]
1068           
1069     (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
1070     (I2)      [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
1071
1072 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2. 
1073 They may react to yield that (beta := [alpha]) which can then be pushed inwards 
1074 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1075 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1076 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1077
1078     class C x y | x -> y where 
1079      op :: x -> y -> ()
1080
1081     instance C [a] [a]
1082
1083     type family F a :: *
1084
1085     h :: F Int -> ()
1086     h = undefined
1087
1088     data TEx where 
1089       TEx :: a -> TEx 
1090
1091
1092     f (x::beta) = 
1093         let g1 :: forall b. b -> ()
1094             g1 _ = h [x]
1095             g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1096         in (g1 '3', g2 undefined)
1097
1098
1099
1100 Note [Solving Family Equations] 
1101 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1102 After we are done with simplification we may be left with constraints of the form:
1103      [Wanted] F xis ~ beta 
1104 If 'beta' is a touchable unification variable not already bound in the TyBinds 
1105 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1106
1107 When is it ok to do so? 
1108     1) 'beta' must not already be defaulted to something. Example: 
1109
1110            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
1111            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
1112                                        have to report this as unsolved.
1113
1114     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
1115        set [beta := F xis] only if beta is not among the free variables of xis.
1116
1117     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
1118        of type family equations. See Inert Set invariants in TcInteract.
1119
1120 This solving is now happening during zonking, see Note [Unflattening while zonking]
1121 in TcMType.
1122
1123
1124 *********************************************************************************
1125 *                                                                               * 
1126 *                          Defaulting and disamgiguation                        *
1127 *                                                                               *
1128 *********************************************************************************
1129
1130 \begin{code}
1131 applyDefaultingRules :: Cts -> TcS Bool
1132   -- True <=> I did some defaulting, reflected in ty_binds
1133                  
1134 -- Return some extra derived equalities, which express the
1135 -- type-class default choice. 
1136 applyDefaultingRules wanteds
1137   | isEmptyBag wanteds 
1138   = return False
1139   | otherwise
1140   = do { traceTcS "applyDefaultingRules { " $ 
1141                   text "wanteds =" <+> ppr wanteds
1142                   
1143        ; info@(default_tys, _) <- getDefaultInfo
1144        ; let groups = findDefaultableGroups info wanteds
1145        ; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups
1146                                                  , text "info=" <+> ppr info ]
1147        ; something_happeneds <- mapM (disambigGroup default_tys) groups
1148
1149        ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
1150
1151        ; return (or something_happeneds) }
1152 \end{code}
1153
1154
1155
1156 \begin{code}
1157 findDefaultableGroups 
1158     :: ( [Type]
1159        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1160     -> Cts              -- Unsolved (wanted or derived)
1161     -> [[(Ct,Class,TcTyVar)]]
1162 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1163   | null default_tys             = []
1164   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1165   where 
1166     unaries     :: [(Ct, Class, TcTyVar)]  -- (C tv) constraints
1167     non_unaries :: [Ct]             -- and *other* constraints
1168     
1169     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1170         -- Finds unary type-class constraints
1171     find_unary cc 
1172         | Just (cls,[ty]) <- getClassPredTys_maybe (ctPred cc)
1173         , Just tv <- tcGetTyVar_maybe ty
1174         , isMetaTyVar tv  -- We might have runtime-skolems in GHCi, and 
1175                           -- we definitely don't want to try to assign to those!
1176         = Left (cc, cls, tv)
1177     find_unary cc = Right cc  -- Non unary or non dictionary 
1178
1179     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
1180     bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries 
1181
1182     cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
1183
1184     is_defaultable_group ds@((_,_,tv):_)
1185         = let b1 = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
1186               b2 = not (tv `elemVarSet` bad_tvs)
1187               b4 = defaultable_classes [cls | (_,cls,_) <- ds]
1188           in (b1 && b2 && b4)
1189     is_defaultable_group [] = panic "defaultable_group"
1190
1191     defaultable_classes clss 
1192         | extended_defaults = any isInteractiveClass clss
1193         | otherwise         = all is_std_class clss && (any is_num_class clss)
1194
1195     -- In interactive mode, or with -XExtendedDefaultRules,
1196     -- we default Show a to Show () to avoid graututious errors on "show []"
1197     isInteractiveClass cls 
1198         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1199
1200     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1201     -- is_num_class adds IsString to the standard numeric classes, 
1202     -- when -foverloaded-strings is enabled
1203
1204     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1205     -- Similarly is_std_class
1206
1207 ------------------------------
1208 disambigGroup :: [Type]                  -- The default types 
1209               -> [(Ct, Class, TcTyVar)]  -- All classes of the form (C a)
1210                                          --  sharing same type variable
1211               -> TcS Bool   -- True <=> something happened, reflected in ty_binds
1212
1213 disambigGroup []  _grp
1214   = return False
1215 disambigGroup (default_ty:default_tys) group
1216   = do { traceTcS "disambigGroup {" (ppr group $$ ppr default_ty)
1217        ; success <- tryTcS $ -- Why tryTcS? If this attempt fails, we want to 
1218                              -- discard all side effects from the attempt
1219                     do { setWantedTyBind the_tv default_ty
1220                        ; implics_from_defaulting <- solveInteract wanteds
1221                        ; MASSERT (isEmptyBag implics_from_defaulting)
1222                            -- I am not certain if any implications can be generated
1223                            -- but I am letting this fail aggressively if this ever happens.
1224                                      
1225                        ; checkAllSolved }
1226
1227        ; if success then
1228              -- Success: record the type variable binding, and return
1229              do { setWantedTyBind the_tv default_ty
1230                 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
1231                 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
1232                 ; return True }
1233          else
1234              -- Failure: try with the next type
1235              do { traceTcS "disambigGroup failed, will try other default types }"
1236                            (ppr default_ty)
1237                 ; disambigGroup default_tys group } }
1238   where
1239     ((_,_,the_tv):_) = group
1240     wanteds          = listToBag (map fstOf3 group)
1241 \end{code}
1242
1243 Note [Avoiding spurious errors]
1244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1245 When doing the unification for defaulting, we check for skolem
1246 type variables, and simply don't default them.  For example:
1247    f = (*)      -- Monomorphic
1248    g :: Num a => a -> a
1249    g x = f x x
1250 Here, we get a complaint when checking the type signature for g,
1251 that g isn't polymorphic enough; but then we get another one when
1252 dealing with the (Num a) context arising from f's definition;
1253 we try to unify a with Int (to default it), but find that it's
1254 already been unified with the rigid variable from g's type sig
1255
1256
1257
1258 *********************************************************************************
1259 *                                                                               * 
1260 *                   Utility functions
1261 *                                                                               *
1262 *********************************************************************************
1263
1264 \begin{code}
1265 newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
1266 newFlatWanteds orig theta
1267   = do { loc <- getCtLoc orig
1268        ; mapM (inst_to_wanted loc) theta }
1269   where 
1270     inst_to_wanted loc pty 
1271           = do { v <- TcM.newWantedEvVar pty 
1272                ; return $ mkNonCanonical loc $
1273                  CtWanted { ctev_evar = v
1274                           , ctev_pred = pty } }
1275 \end{code}