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