fix haddock submodule pointer
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
1 \begin{code}
2 module TcSimplify( 
3        simplifyInfer,
4        simplifyDefault, simplifyDeriv, 
5        simplifyRule, simplifyTop, simplifyInteractive
6   ) where
7
8 #include "HsVersions.h"
9
10 import HsSyn           
11 import TcRnMonad
12 import TcErrors
13 import TcMType
14 import TcType 
15 import TcSMonad 
16 import TcInteract
17 import Inst
18 import Id       ( evVarPred )
19 import Unify    ( niFixTvSubst, niSubstTvSet )
20 import Var
21 import VarSet
22 import VarEnv 
23 import Coercion
24 import TypeRep
25
26 import Name
27 import NameEnv  ( emptyNameEnv )
28 import Bag
29 import ListSetOps
30 import Util
31 import PrelInfo
32 import PrelNames
33 import Class            ( classKey )
34 import BasicTypes       ( RuleName, TopLevelFlag, isTopLevel )
35 import Control.Monad    ( when )
36 import Outputable
37 import FastString
38 \end{code}
39
40
41 *********************************************************************************
42 *                                                                               * 
43 *                           External interface                                  *
44 *                                                                               *
45 *********************************************************************************
46
47 \begin{code}
48 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
49 -- Simplify top-level constraints
50 -- Usually these will be implications,
51 -- but when there is nothing to quantify we don't wrap
52 -- in a degenerate implication, so we do that here instead
53 simplifyTop wanteds 
54   = simplifyCheck (SimplCheck (ptext (sLit "top level"))) wanteds
55
56 ------------------
57 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
58 simplifyInteractive wanteds 
59   = simplifyCheck SimplInteractive wanteds
60
61 ------------------
62 simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
63                 -> TcM ()       -- Succeeds iff the constraint is soluble
64 simplifyDefault theta
65   = do { wanted <- newFlatWanteds DefaultOrigin theta
66        ; _ignored_ev_binds <- simplifyCheck (SimplCheck (ptext (sLit "defaults"))) 
67                                             (mkFlatWC wanted)
68        ; return () }
69 \end{code}
70
71
72
73 *********************************************************************************
74 *                                                                                 * 
75 *                            Deriving
76 *                                                                                 *
77 ***********************************************************************************
78
79 \begin{code}
80 simplifyDeriv :: CtOrigin
81               -> PredType
82               -> [TyVar]        
83               -> ThetaType              -- Wanted
84               -> TcM ThetaType  -- Needed
85 -- Given  instance (wanted) => C inst_ty 
86 -- Simplify 'wanted' as much as possibles
87 -- Fail if not possible
88 simplifyDeriv orig pred tvs theta 
89   = do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize
90                 -- The constraint solving machinery 
91                 -- expects *TcTyVars* not TyVars.  
92                 -- We use *non-overlappable* (vanilla) skolems
93                 -- See Note [Overlap and deriving]
94
95        ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
96              subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
97              doc = parens $ ptext (sLit "deriving") <+> parens (ppr pred)
98
99        ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
100
101        ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
102        ; (residual_wanted, _binds)
103              <- runTcS (SimplInfer doc) NoUntouchables $
104                 solveWanteds emptyInert (mkFlatWC wanted)
105
106        ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
107                          -- See Note [Exotic derived instance contexts]
108              get_good :: WantedEvVar -> Either PredType WantedEvVar
109              get_good wev | validDerivPred p = Left p
110                           | otherwise        = Right wev
111                           where p = evVarOfPred wev
112
113        ; reportUnsolved (residual_wanted { wc_flat = bad })
114
115        ; let min_theta = mkMinimalBySCs (bagToList good)
116        ; return (substTheta subst_skol min_theta) }
117 \end{code}
118
119 Note [Overlap and deriving]
120 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
121 Consider some overlapping instances:
122   data Show a => Show [a] where ..
123   data Show [Char] where ...
124
125 Now a data type with deriving:
126   data T a = MkT [a] deriving( Show )
127
128 We want to get the derived instance
129   instance Show [a] => Show (T a) where...
130 and NOT
131   instance Show a => Show (T a) where...
132 so that the (Show (T Char)) instance does the Right Thing
133
134 It's very like the situation when we're inferring the type
135 of a function
136    f x = show [x]
137 and we want to infer
138    f :: Show [a] => a -> String
139
140 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
141              the context for the derived instance. 
142              Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
143
144 Note [Exotic derived instance contexts]
145 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
146 In a 'derived' instance declaration, we *infer* the context.  It's a
147 bit unclear what rules we should apply for this; the Haskell report is
148 silent.  Obviously, constraints like (Eq a) are fine, but what about
149         data T f a = MkT (f a) deriving( Eq )
150 where we'd get an Eq (f a) constraint.  That's probably fine too.
151
152 One could go further: consider
153         data T a b c = MkT (Foo a b c) deriving( Eq )
154         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
155
156 Notice that this instance (just) satisfies the Paterson termination 
157 conditions.  Then we *could* derive an instance decl like this:
158
159         instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
160 even though there is no instance for (C Int a), because there just
161 *might* be an instance for, say, (C Int Bool) at a site where we
162 need the equality instance for T's.  
163
164 However, this seems pretty exotic, and it's quite tricky to allow
165 this, and yet give sensible error messages in the (much more common)
166 case where we really want that instance decl for C.
167
168 So for now we simply require that the derived instance context
169 should have only type-variable constraints.
170
171 Here is another example:
172         data Fix f = In (f (Fix f)) deriving( Eq )
173 Here, if we are prepared to allow -XUndecidableInstances we
174 could derive the instance
175         instance Eq (f (Fix f)) => Eq (Fix f)
176 but this is so delicate that I don't think it should happen inside
177 'deriving'. If you want this, write it yourself!
178
179 NB: if you want to lift this condition, make sure you still meet the
180 termination conditions!  If not, the deriving mechanism generates
181 larger and larger constraints.  Example:
182   data Succ a = S a
183   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
184
185 Note the lack of a Show instance for Succ.  First we'll generate
186   instance (Show (Succ a), Show a) => Show (Seq a)
187 and then
188   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
189 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
190
191 The bottom line
192 ~~~~~~~~~~~~~~~
193 Allow constraints which consist only of type variables, with no repeats.
194
195 *********************************************************************************
196 *                                                                                 * 
197 *                            Inference
198 *                                                                                 *
199 ***********************************************************************************
200
201 \begin{code}
202 simplifyInfer :: TopLevelFlag
203               -> Bool                  -- Apply monomorphism restriction
204               -> [(Name, TcTauType)]   -- Variables to be generalised,
205                                        -- and their tau-types
206               -> WantedConstraints
207               -> TcM ([TcTyVar],    -- Quantify over these type variables
208                       [EvVar],      -- ... and these constraints
209                       TcEvBinds)    -- ... binding these evidence variables
210 simplifyInfer top_lvl apply_mr name_taus wanteds
211   | isEmptyWC wanteds
212   = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
213        ; zonked_taus <- zonkTcTypes (map snd name_taus)
214        ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
215        ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
216        ; return (qtvs, [], emptyTcEvBinds) }
217
218   | otherwise
219   = do { zonked_wanteds <- zonkWC wanteds
220        ; zonked_taus    <- zonkTcTypes (map snd name_taus)
221        ; gbl_tvs        <- tcGetGlobalTyVars
222
223        ; traceTc "simplifyInfer {"  $ vcat
224              [ ptext (sLit "apply_mr =") <+> ppr apply_mr
225              , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
226              , ptext (sLit "wanted =") <+> ppr zonked_wanteds
227              ]
228
229              -- Step 1
230              -- Make a guess at the quantified type variables
231              -- Then split the constraints on the baisis of those tyvars
232              -- to avoid unnecessarily simplifying a class constraint
233              -- See Note [Avoid unecessary constraint simplification]
234        ; let zonked_tau_tvs = get_tau_tvs zonked_taus
235              proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
236                           zonked_tau_tvs `minusVarSet` gbl_tvs
237              (perhaps_bound, surely_free)
238                         = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds)
239
240        ; traceTc "simplifyInfer proto"  $ vcat
241              [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
242              , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
243              , ptext (sLit "surely_fref =") <+> ppr surely_free
244              ]
245
246        ; emitFlats surely_free
247        ; traceTc "sinf"  $ vcat
248              [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
249              , ptext (sLit "surely_free   =") <+> ppr surely_free
250              ]
251
252             -- Step 2 
253             -- Now simplify the possibly-bound constraints
254        ; (simpl_results, tc_binds0)
255            <- runTcS (SimplInfer (ppr (map fst name_taus))) NoUntouchables $
256               simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
257
258        ; when (insolubleWC simpl_results)  -- Fail fast if there is an insoluble constraint
259               (do { reportUnsolved simpl_results; failM })
260
261             -- Step 3 
262             -- Split again simplified_perhaps_bound, because some unifications 
263             -- may have happened, and emit the free constraints. 
264        ; gbl_tvs        <- tcGetGlobalTyVars
265        ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
266        ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
267        ; let init_tvs        = zonked_tau_tvs `minusVarSet` gbl_tvs
268              mr_qtvs         = init_tvs `minusVarSet` constrained_tvs
269              constrained_tvs = tyVarsOfEvVarXs zonked_simples
270              qtvs            = growWantedEVs gbl_tvs zonked_simples init_tvs
271              (final_qtvs, (bound, free))
272                 | apply_mr  = (mr_qtvs, (emptyBag, zonked_simples))
273                 | otherwise = (qtvs,    partitionBag (quantifyMe qtvs) zonked_simples)
274        ; emitFlats free
275
276        ; if isEmptyVarSet final_qtvs && isEmptyBag bound
277          then ASSERT( isEmptyBag (wc_insol simpl_results) )
278               do { traceTc "} simplifyInfer/no quantification" empty
279                  ; emitImplications (wc_impl simpl_results)
280                  ; return ([], [], EvBinds tc_binds0) }
281          else do
282
283             -- Step 4, zonk quantified variables 
284        { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
285        ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
286                         | (name, ty) <- name_taus ]
287                         -- Don't add the quantified variables here, because
288                         -- they are also bound in ic_skols and we want them to be
289                         -- tidied uniformly
290              skol_info = InferSkol poly_ids
291
292        ; gloc <- getCtLoc skol_info
293        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
294
295             -- Step 5
296             -- Minimize `bound' and emit an implication
297        ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
298        ; ev_binds_var <- newTcEvBinds
299        ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0
300        ; lcl_env <- getLclTypeEnv
301        ; let implic = Implic { ic_untch    = NoUntouchables
302                              , ic_env      = lcl_env
303                              , ic_skols    = mkVarSet qtvs_to_return
304                              , ic_given    = minimal_bound_ev_vars
305                              , ic_wanted   = simpl_results { wc_flat = bound }
306                              , ic_insol    = False
307                              , ic_binds    = ev_binds_var
308                              , ic_loc      = gloc }
309        ; emitImplication implic
310        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
311              vcat [ ptext (sLit "implic =") <+> ppr implic
312                        -- ic_skols, ic_given give rest of result
313                   , ptext (sLit "qtvs =") <+> ppr final_qtvs
314                   , ptext (sLit "spb =") <+> ppr zonked_simples
315                   , ptext (sLit "bound =") <+> ppr bound ]
316
317
318
319        ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
320   where
321     get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
322                 | otherwise          = exactTyVarsOfTypes
323      -- See Note [Silly type synonym] in TcType
324 \end{code}
325
326
327 Note [Minimize by Superclasses]
328 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
329
330 When we quantify over a constraint, in simplifyInfer we need to
331 quantify over a constraint that is minimal in some sense: For
332 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
333 we'd like to quantify over Ord alpha, because we can just get Eq alpha
334 from superclass selection from Ord alpha. This minimization is what
335 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
336 to check the original wanted.
337
338 \begin{code}
339 simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints
340 simplifyWithApprox wanted
341  = do { traceTcS "simplifyApproxLoop" (ppr wanted)
342
343       ; results <- solveWanteds emptyInert wanted
344
345       ; let (residual_implics, floats) = approximateImplications (wc_impl results)
346
347         -- If no new work was produced then we are done with simplifyApproxLoop
348       ; if insolubleWC results || isEmptyBag floats
349         then return results
350
351         else solveWanteds emptyInert
352                 (WC { wc_flat = floats `unionBags` wc_flat results
353                     , wc_impl = residual_implics
354                     , wc_insol = emptyBag }) }
355
356 approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar)
357 -- Extracts any nested constraints that don't mention the skolems
358 approximateImplications impls
359   = do_bag (float_implic emptyVarSet) impls
360   where 
361     do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
362     do_bag f = foldrBag (plus . f) (emptyBag, emptyBag)
363     plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c)
364     plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2)
365
366     float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar)
367     float_implic skols imp
368       = (unitBag (imp { ic_wanted = wanted' }), floats)
369       where
370         (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp)
371
372     float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic })
373       = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2)
374       where
375         (flat',   floats1) = do_bag (float_flat   skols) flat
376         (implic', floats2) = do_bag (float_implic skols) implic
377
378     float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
379     float_flat skols wev
380       | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev)
381       | otherwise                                 = (unitBag wev, emptyBag)
382 \end{code}
383
384 \begin{code}
385 -- (growX gbls wanted tvs) grows a seed 'tvs' against the 
386 -- X-constraint 'wanted', nuking the 'gbls' at each stage
387 -- It's conservative in that if the seed could *possibly*
388 -- grow to include a type variable, then it does
389
390 growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
391 growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
392
393 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
394 growWantedEVs gbl_tvs ws tvs
395   | isEmptyBag ws = tvs
396   | otherwise     = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
397
398 --------  Helper functions, do not do fixpoint ------------------------
399 growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
400 growWC gbl_tvs wc = growImplics gbl_tvs             (wc_impl wc) .
401                     growPreds   gbl_tvs evVarOfPred (wc_flat wc) .
402                     growPreds   gbl_tvs evVarOfPred (wc_insol wc)
403
404 growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
405 growImplics gbl_tvs implics tvs
406   = foldrBag grow_implic tvs implics
407   where
408     grow_implic implic tvs
409       = grow tvs `minusVarSet` ic_skols implic
410       where
411         grow = growWC gbl_tvs (ic_wanted implic) .
412                growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
413                -- We must grow from givens too; see test IPRun
414
415 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
416 growPreds gbl_tvs get_pred items tvs
417   = foldrBag extend tvs items
418   where
419     extend item tvs = tvs `unionVarSet`
420                       (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
421
422 --------------------
423 quantifyMe :: TyVarSet      -- Quantifying over these
424            -> WantedEvVar
425            -> Bool          -- True <=> quantify over this wanted
426 quantifyMe qtvs wev
427   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
428   | otherwise     = tyVarsOfPred pred `intersectsVarSet` qtvs
429   where
430     pred = evVarOfPred wev
431 \end{code}
432
433 Note [Avoid unecessary constraint simplification]
434 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
435 When inferring the type of a let-binding, with simplifyInfer,
436 try to avoid unnecessariliy simplifying class constraints.
437 Doing so aids sharing, but it also helps with delicate 
438 situations like
439    instance C t => C [t] where ..
440    f :: C [t] => ....
441    f x = let g y = ...(constraint C [t])... 
442          in ...
443 When inferring a type for 'g', we don't want to apply the
444 instance decl, because then we can't satisfy (C t).  So we
445 just notice that g isn't quantified over 't' and partition
446 the contraints before simplifying.
447
448 This only half-works, but then let-generalisation only half-works.
449
450
451 Note [Inheriting implicit parameters]
452 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
453 Consider this:
454
455         f x = (x::Int) + ?y
456
457 where f is *not* a top-level binding.
458 From the RHS of f we'll get the constraint (?y::Int).
459 There are two types we might infer for f:
460
461         f :: Int -> Int
462
463 (so we get ?y from the context of f's definition), or
464
465         f :: (?y::Int) => Int -> Int
466
467 At first you might think the first was better, becuase then
468 ?y behaves like a free variable of the definition, rather than
469 having to be passed at each call site.  But of course, the WHOLE
470 IDEA is that ?y should be passed at each call site (that's what
471 dynamic binding means) so we'd better infer the second.
472
473 BOTTOM LINE: when *inferring types* you *must* quantify 
474 over implicit parameters. See the predicate isFreeWhenInferring.
475
476
477 *********************************************************************************
478 *                                                                                 * 
479 *                             RULES                                               *
480 *                                                                                 *
481 ***********************************************************************************
482
483 Note [Simplifying RULE lhs constraints]
484 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
485 On the LHS of transformation rules we only simplify only equalities,
486 but not dictionaries.  We want to keep dictionaries unsimplified, to
487 serve as the available stuff for the RHS of the rule.  We *do* want to
488 simplify equalities, however, to detect ill-typed rules that cannot be
489 applied.
490
491 Implementation: the TcSFlags carried by the TcSMonad controls the
492 amount of simplification, so simplifyRuleLhs just sets the flag
493 appropriately.
494
495 Example.  Consider the following left-hand side of a rule
496         f (x == y) (y > z) = ...
497 If we typecheck this expression we get constraints
498         d1 :: Ord a, d2 :: Eq a
499 We do NOT want to "simplify" to the LHS
500         forall x::a, y::a, z::a, d1::Ord a.
501           f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
502 Instead we want 
503         forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
504           f ((==) d2 x y) ((>) d1 y z) = ...
505
506 Here is another example:
507         fromIntegral :: (Integral a, Num b) => a -> b
508         {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
509 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
510 we *dont* want to get
511         forall dIntegralInt.
512            fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
513 because the scsel will mess up RULE matching.  Instead we want
514         forall dIntegralInt, dNumInt.
515           fromIntegral Int Int dIntegralInt dNumInt = id Int
516
517 Even if we have 
518         g (x == y) (y == z) = ..
519 where the two dictionaries are *identical*, we do NOT WANT
520         forall x::a, y::a, z::a, d1::Eq a
521           f ((==) d1 x y) ((>) d1 y z) = ...
522 because that will only match if the dict args are (visibly) equal.
523 Instead we want to quantify over the dictionaries separately.
524
525 In short, simplifyRuleLhs must *only* squash equalities, leaving
526 all dicts unchanged, with absolutely no sharing.  
527
528 HOWEVER, under a nested implication things are different
529 Consider
530   f :: (forall a. Eq a => a->a) -> Bool -> ...
531   {-# RULES "foo" forall (v::forall b. Eq b => b->b).
532        f b True = ...
533     #=}
534 Here we *must* solve the wanted (Eq a) from the given (Eq a)
535 resulting from skolemising the agument type of g.  So we 
536 revert to SimplCheck when going under an implication.  
537
538 \begin{code}
539 simplifyRule :: RuleName 
540              -> [TcTyVar]               -- Explicit skolems
541              -> WantedConstraints       -- Constraints from LHS
542              -> WantedConstraints       -- Constraints from RHS
543              -> TcM ([EvVar],           -- LHS dicts
544                      TcEvBinds,         -- Evidence for LHS
545                      TcEvBinds)         -- Evidence for RHS
546 -- See Note [Simplifying RULE lhs constraints]
547 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
548   = do { loc        <- getCtLoc (RuleSkol name)
549        ; zonked_lhs <- zonkWC lhs_wanted
550        ; let untch = NoUntouchables
551                  -- We allow ourselves to unify environment 
552                  -- variables; hence *no untouchables*
553
554        ; (lhs_results, lhs_binds)
555               <- runTcS (SimplRuleLhs name) untch $
556                  solveWanteds emptyInert zonked_lhs
557
558        ; traceTc "simplifyRule" $
559          vcat [ text "zonked_lhs"   <+> ppr zonked_lhs 
560               , text "lhs_results" <+> ppr lhs_results
561               , text "lhs_binds"    <+> ppr lhs_binds 
562               , text "rhs_wanted"   <+> ppr rhs_wanted ]
563
564
565        -- Don't quantify over equalities (judgement call here)
566        ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred)
567                                          (wc_flat lhs_results)
568              lhs_dicts    = map evVarOf (bagToList dicts)
569                                  -- Dicts and implicit parameters
570
571            -- Fail if we have not got down to unsolved flats
572        ; ev_binds_var <- newTcEvBinds
573        ; emitImplication $ Implic { ic_untch  = untch
574                                   , ic_env    = emptyNameEnv
575                                   , ic_skols  = mkVarSet tv_bndrs
576                                   , ic_given  = lhs_dicts
577                                   , ic_wanted = lhs_results { wc_flat = eqs }
578                                   , ic_insol  = insolubleWC lhs_results
579                                   , ic_binds  = ev_binds_var
580                                   , ic_loc    = loc }
581
582              -- Notice that we simplify the RHS with only the explicitly
583              -- introduced skolems, allowing the RHS to constrain any 
584              -- unification variables.
585              -- Then, and only then, we call zonkQuantifiedTypeVariables
586              -- Example   foo :: Ord a => a -> a
587              --           foo_spec :: Int -> Int
588              --           {-# RULE "foo"  foo = foo_spec #-}
589              --     Here, it's the RHS that fixes the type variable
590
591              -- So we don't want to make untouchable the type
592              -- variables in the envt of the RHS, because they include
593              -- the template variables of the RULE
594
595              -- Hence the rather painful ad-hoc treatement here
596        ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
597        ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
598        ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $
599             WC { wc_flat = emptyBag
600                , wc_insol = emptyBag
601                , wc_impl = unitBag $
602                     Implic { ic_untch   = NoUntouchables
603                             , ic_env    = emptyNameEnv
604                             , ic_skols  = mkVarSet tv_bndrs
605                             , ic_given  = lhs_dicts
606                             , ic_wanted = rhs_wanted
607                             , ic_insol  = insolubleWC rhs_wanted
608                             , ic_binds  = rhs_binds_var
609                             , ic_loc    = loc } }
610        ; rhs_binds2 <- readTcRef evb_ref
611
612        ; return ( lhs_dicts
613                 , EvBinds lhs_binds 
614                 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
615 \end{code}
616
617
618 *********************************************************************************
619 *                                                                                 * 
620 *                                 Main Simplifier                                 *
621 *                                                                                 *
622 ***********************************************************************************
623
624 \begin{code}
625 simplifyCheck :: SimplContext
626               -> WantedConstraints      -- Wanted
627               -> TcM (Bag EvBind)
628 -- Solve a single, top-level implication constraint
629 -- e.g. typically one created from a top-level type signature
630 --          f :: forall a. [a] -> [a]
631 --          f x = rhs
632 -- We do this even if the function has no polymorphism:
633 --          g :: Int -> Int
634
635 --          g y = rhs
636 -- (whereas for *nested* bindings we would not create
637 --  an implication constraint for g at all.)
638 --
639 -- Fails if can't solve something in the input wanteds
640 simplifyCheck ctxt wanteds
641   = do { wanteds <- zonkWC wanteds
642
643        ; traceTc "simplifyCheck {" (vcat
644              [ ptext (sLit "wanted =") <+> ppr wanteds ])
645
646        ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
647                                  solveWanteds emptyInert wanteds
648
649        ; traceTc "simplifyCheck }" $
650          ptext (sLit "unsolved =") <+> ppr unsolved
651
652        ; reportUnsolved unsolved
653
654        ; return ev_binds }
655
656 ----------------
657 solveWanteds :: InertSet                            -- Given
658              -> WantedConstraints
659              -> TcS WantedConstraints
660 solveWanteds inert wanted
661   = do { (unsolved_flats, unsolved_implics, insols)
662              <- solve_wanteds inert wanted
663        ; return (WC { wc_flat = keepWanted unsolved_flats   -- Discard Derived
664                     , wc_impl = unsolved_implics
665                     , wc_insol = insols }) }
666
667 solve_wanteds :: InertSet                            -- Given
668               -> WantedConstraints
669               -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar)
670 -- solve_wanteds iterates when it is able to float equalities
671 -- out of one or more of the implications
672 solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
673   = do { traceTcS "solveWanteds {" (ppr wanted)
674
675                  -- Try the flat bit
676                  -- Discard from insols all the derived/given constraints
677                  -- because they will show up again when we try to solve
678                  -- everything else.  Solving them a second time is a bit
679                  -- of a waste, but the code is simple, and the program is
680                  -- wrong anyway!
681        ; let all_flats = flats `unionBags` keepWanted insols
682        ; inert1 <- solveInteractWanted inert (bagToList all_flats)
683
684        ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics
685
686        ; bb <- getTcEvBindsBag
687        ; tb <- getTcSTyBindsMap
688        ; traceTcS "solveWanteds }" $
689                  vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
690                       , text "unsolved_implics =" <+> ppr unsolved_implics
691                       , text "current evbinds  =" <+> vcat (map ppr (varEnvElts bb))
692                       , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
693                       ]
694
695        ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats
696                 -- See Note [Solving Family Equations]
697                 -- NB: remaining_flats has already had subst applied
698
699        ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats
700
701        ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats
702                 , mapBag (substImplication subst) unsolved_implics
703                 , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) }
704
705   where
706     simpl_loop :: Int
707                -> InertSet
708                -> Bag Implication
709                -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
710     simpl_loop n inert implics
711       | n>10
712       = trace "solveWanteds: loop" $                    -- Always bleat
713         do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
714            ; let (_, unsolved_cans) = extractUnsolved inert
715            ; return (unsolved_cans, implics) }
716
717       | otherwise
718       = do { traceTcS "solveWanteds: simpl_loop start {" $
719                  vcat [ text "n =" <+> ppr n
720                       , text "implics =" <+> ppr implics
721                       , text "inert   =" <+> ppr inert ]
722            
723            ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
724                      -- unsolved_cans contains either Wanted or Derived!
725
726            ; (implic_eqs, unsolved_implics) 
727                   <- solveNestedImplications just_given_inert unsolved_cans implics
728
729                 -- Apply defaulting rules if and only if there
730                 -- no floated equalities.  If there are, they may
731                 -- solve the remaining wanteds, so don't do defaulting.
732            ; improve_eqs <- if not (isEmptyBag implic_eqs)
733                             then return implic_eqs
734                             else applyDefaultingRules just_given_inert unsolved_cans
735
736            ; traceTcS "solveWanteds: simpl_loop end }" $
737                  vcat [ text "improve_eqs      =" <+> ppr improve_eqs
738                       , text "unsolved_flats   =" <+> ppr unsolved_cans
739                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
740
741            ; (improve_eqs_already_in_inert, inert_with_improvement)
742                <- solveInteract inert improve_eqs 
743
744            ; if improve_eqs_already_in_inert then
745                  return (unsolved_cans, unsolved_implics)
746              else 
747                  simpl_loop (n+1) inert_with_improvement 
748                                          -- Contain unsolved_cans and the improve_eqs
749                                   unsolved_implics
750            }
751
752 givensFromWanteds :: SimplContext -> CanonicalCts -> Bag FlavoredEvVar
753 -- Extract the Wanted ones from CanonicalCts and conver to
754 -- Givens; not Given/Solved, see Note [Preparing inert set for implications]
755 givensFromWanteds _ctxt = foldrBag getWanted emptyBag
756   where
757     getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
758     getWanted cc givens
759       | pushable_wanted cc
760       = let given = mkEvVarX (cc_id cc) (mkGivenFlavor (cc_flavor cc) UnkSkol)
761         in given `consBag` givens     -- and not mkSolvedFlavor,
762                                       -- see Note [Preparing inert set for implications]
763       | otherwise = givens
764
765     pushable_wanted :: CanonicalCt -> Bool 
766     pushable_wanted cc 
767       | not (isCFrozenErr cc) 
768       , isWantedCt cc 
769       = isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications]
770       | otherwise = False 
771  
772 solveNestedImplications :: InertSet -> CanonicalCts
773                         -> Bag Implication
774                         -> TcS (Bag FlavoredEvVar, Bag Implication)
775 solveNestedImplications just_given_inert unsolved_cans implics
776   | isEmptyBag implics
777   = return (emptyBag, emptyBag)
778   | otherwise 
779   = do {  -- See Note [Preparing inert set for implications]
780           -- Push the unsolved wanteds inwards, but as givens
781              
782        ; simpl_ctx <- getTcSContext 
783
784        ; let pushed_givens    = givensFromWanteds simpl_ctx unsolved_cans
785              tcs_untouchables = filterVarSet isFlexiTcsTv $
786                                 tyVarsOfEvVarXs pushed_givens
787              -- See Note [Extra TcsTv untouchables]
788
789        ; traceTcS "solveWanteds: preparing inerts for implications {"  
790                   (vcat [ppr tcs_untouchables, ppr pushed_givens])
791
792        ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens 
793
794        ; traceTcS "solveWanteds: } now doing nested implications {" $
795          vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
796               , text "implics =" <+> ppr implics ]
797
798        ; (implic_eqs, unsolved_implics)
799            <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
800
801        ; traceTcS "solveWanteds: done nested implications }" $
802                   vcat [ text "implic_eqs ="       <+> ppr implic_eqs
803                        , text "unsolved_implics =" <+> ppr unsolved_implics ]
804
805        ; return (implic_eqs, unsolved_implics) }
806
807 solveImplication :: TcTyVarSet                -- Untouchable TcS unification variables
808                  -> InertSet                  -- Given
809                  -> Implication               -- Wanted
810                  -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type
811                          Bag Implication)     -- Unsolved rest (always empty or singleton)
812 -- Returns: 
813 --  1. A bag of floatable wanted constraints, not mentioning any skolems, 
814 --     that are of the form unification var = type
815 -- 
816 --  2. Maybe a unsolved implication, empty if entirely solved! 
817 -- 
818 -- Precondition: everything is zonked by now
819 solveImplication tcs_untouchables inert
820      imp@(Implic { ic_untch  = untch 
821                  , ic_binds  = ev_binds
822                  , ic_skols  = skols 
823                  , ic_given  = givens
824                  , ic_wanted = wanteds
825                  , ic_loc    = loc })
826   = nestImplicTcS ev_binds (untch, tcs_untouchables) $
827     recoverTcS (return (emptyBag, emptyBag)) $
828        -- Recover from nested failures.  Even the top level is
829        -- just a bunch of implications, so failing at the first
830        -- one is bad
831     do { traceTcS "solveImplication {" (ppr imp) 
832
833          -- Solve flat givens
834        ; given_inert <- solveInteractGiven inert loc givens 
835
836          -- Simplify the wanteds
837        ; (unsolved_flats, unsolved_implics, insols)
838              <- solve_wanteds given_inert wanteds
839
840        ; let (res_flat_free, res_flat_bound)
841                  = floatEqualities skols givens unsolved_flats
842              final_flat = keepWanted res_flat_bound
843
844        ; let res_wanted = WC { wc_flat = final_flat
845                              , wc_impl = unsolved_implics
846                              , wc_insol = insols }
847              res_implic = unitImplication $
848                           imp { ic_wanted = res_wanted
849                               , ic_insol  = insolubleWC res_wanted }
850
851        ; traceTcS "solveImplication end }" $ vcat
852              [ text "res_flat_free =" <+> ppr res_flat_free
853              , text "res_implic =" <+> ppr res_implic ]
854
855        ; return (res_flat_free, res_implic) }
856
857
858 floatEqualities :: TcTyVarSet -> [EvVar]
859                 -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
860 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
861 -- and come from the input wanted ev vars or deriveds 
862 floatEqualities skols can_given wantders
863   | hasEqualities can_given = (emptyBag, wantders)
864           -- Note [Float Equalities out of Implications]
865   | otherwise = partitionBag is_floatable wantders
866   
867
868   where is_floatable :: FlavoredEvVar -> Bool
869         is_floatable (EvVarX cv _fl)
870           | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
871         is_floatable _flev = False
872
873         tvs_under_fsks :: Type -> TyVarSet
874         -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
875         tvs_under_fsks (TyVarTy tv)     
876           | not (isTcTyVar tv)               = unitVarSet tv
877           | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
878           | otherwise                        = unitVarSet tv
879         tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
880         tvs_under_fsks (PredTy sty)     = predTvs_under_fsks sty
881         tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
882         tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
883         tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder 
884                                       -- can mention type variables!
885           | isTyVar tv                = inner_tvs `delVarSet` tv
886           | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
887                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
888           where
889             inner_tvs = tvs_under_fsks ty
890
891         predTvs_under_fsks :: PredType -> TyVarSet
892         predTvs_under_fsks (IParam _ ty)    = tvs_under_fsks ty
893         predTvs_under_fsks (ClassP _ tys)   = unionVarSets (map tvs_under_fsks tys)
894         predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
895 \end{code}
896
897 Note [Preparing inert set for implications]
898 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
899 Before solving the nested implications, we convert any unsolved flat wanteds
900 to givens, and add them to the inert set.  Reasons:
901
902   a) In checking mode, suppresses unnecessary errors.  We already have
903      on unsolved-wanted error; adding it to the givens prevents any 
904      consequential errors from showing up
905
906   b) More importantly, in inference mode, we are going to quantify over this
907      constraint, and we *don't* want to quantify over any constraints that
908      are deducible from it.
909
910   c) Flattened type-family equalities must be exposed to the nested
911      constraints.  Consider
912         F b ~ alpha, (forall c.  F b ~ alpha)
913      Obviously this is soluble with [alpha := F b].  But the
914      unification is only done by solveCTyFunEqs, right at the end of
915      solveWanteds, and if we aren't careful we'll end up with an
916      unsolved goal inside the implication.  We need to "push" the
917      as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
918      can be used to solve the inner (F b
919      ~ alpha).  See Trac #4935.
920
921   d) There are other cases where interactions between wanteds that can help
922      to solve a constraint. For example
923
924         class C a b | a -> b
925
926         (C Int alpha), (forall d. C d blah => C Int a)
927
928      If we push the (C Int alpha) inwards, as a given, it can produce
929      a fundep (alpha~a) and this can float out again and be used to
930      fix alpha.  (In general we can't float class constraints out just
931      in case (C d blah) might help to solve (C Int a).)
932
933 The unsolved wanteds are *canonical* but they may not be *inert*,
934 because when made into a given they might interact with other givens.
935 Hence the call to solveInteract.  Example:
936
937  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta]) 
938
939 We were not able to solve (a ~w [beta]) but we can't just assume it as
940 given because the resulting set is not inert. Hence we have to do a
941 'solveInteract' step first. 
942
943 Finally, note that we convert them to [Given] and NOT [Given/Solved].
944 The reason is that Given/Solved are weaker than Givens and may be discarded.
945 As an example consider the inference case, where we may have, the following 
946 original constraints: 
947      [Wanted] F Int ~ Int
948              (F Int ~ a => F Int ~ a)
949 If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next 
950 given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting 
951 the (F Int ~ a) insoluble. Hence we should really convert the residual 
952 wanteds to plain old Given. 
953
954 We need only push in unsolved equalities both in checking mode and inference mode: 
955
956   (1) In checking mode we should not push given dictionaries in because of
957 example LongWayOverlapping.hs, where we might get strange overlap
958 errors between far-away constraints in the program.  But even in
959 checking mode, we must still push type family equations. Consider:
960
961    type instance F True a b = a 
962    type instance F False a b = b
963
964    [w] F c a b ~ gamma 
965    (c ~ True) => a ~ gamma 
966    (c ~ False) => b ~ gamma
967
968 Since solveCTyFunEqs happens at the very end of solving, the only way to solve
969 the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not 
970 merely Given/Solved because it has to interact with the top-level instance 
971 environment) and push it inside the implications. Now, when we come out again at
972 the end, having solved the implications solveCTyFunEqs will solve this equality.
973
974   (2) In inference mode, we recheck the final constraint in checking mode and
975 hence we will be able to solve inner implications from top-level quantified
976 constraints nonetheless.
977
978
979 Note [Extra TcsTv untouchables]
980 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
981 Furthemore, we record the inert set simplifier-generated unification
982 variables of the TcsTv kind (such as variables from instance that have
983 been applied, or unification flattens). These variables must be passed
984 to the implications as extra untouchable variables. Otherwise we have
985 the danger of double unifications. Example (from trac ticket #4494):
986
987    (F Int ~ uf)  /\  (forall a. C a => F Int ~ beta) 
988
989 In this example, beta is touchable inside the implication. The first
990 solveInteract step leaves 'uf' ununified. Then we move inside the
991 implication where a new constraint
992        uf  ~  beta  
993 emerges. We may spontaneously solve it to get uf := beta, so the whole
994 implication disappears but when we pop out again we are left with (F
995 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
996 uf will get unified *once more* to (F Int).
997
998 The solution is to record the TcsTvs (i.e. the simplifier-generated
999 unification variables) that are generated when solving the flats, and
1000 make them untouchables for the nested implication. In the example
1001 above uf would become untouchable, so beta would be forced to be
1002 unified as beta := uf.
1003
1004 NB: A consequence is that every simplifier-generated TcsTv variable
1005     that gets floated out of an implication becomes now untouchable
1006     next time we go inside that implication to solve any residual
1007     constraints. In effect, by floating an equality out of the
1008     implication we are committing to have it solved in the outside.
1009
1010 Note [Float Equalities out of Implications]
1011 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1012 We want to float equalities out of vanilla existentials, but *not* out 
1013 of GADT pattern matches. 
1014
1015
1016 \begin{code}
1017
1018 solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
1019 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
1020 -- See Note [Solving Family Equations]
1021 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
1022 --          where the newly generated equalities (alpha := F xi) have been substituted through.
1023 solveCTyFunEqs cts
1024  = do { untch   <- getUntouchables 
1025       ; let (unsolved_can_cts, (ni_subst, cv_binds))
1026                 = getSolvableCTyFunEqs untch cts
1027       ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
1028                                           , ppr ni_subst, ppr cv_binds
1029                                           ])
1030       ; mapM_ solve_one cv_binds
1031
1032       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
1033   where
1034     solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
1035                               ; setCoBind cv (mkReflCo ty) }
1036
1037 ------------
1038 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
1039   -- The TvSubstEnv is not idempotent, but is loop-free
1040   -- See Note [Non-idempotent substitution] in Unify
1041 emptyFunEqBinds :: FunEqBinds
1042 emptyFunEqBinds = (emptyVarEnv, [])
1043
1044 extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
1045 extendFunEqBinds (tv_subst, cv_binds) cv tv ty
1046   = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
1047
1048 ------------
1049 getSolvableCTyFunEqs :: TcsUntouchables
1050                      -> CanonicalCts                -- Precondition: all Wanteds or Derived!
1051                      -> (CanonicalCts, FunEqBinds)  -- Postcondition: returns the unsolvables
1052 getSolvableCTyFunEqs untch cts
1053   = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
1054   where
1055     dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
1056                -> (CanonicalCts, FunEqBinds)
1057     dflt_funeq (cts_in, feb@(tv_subst, _))
1058                (CFunEqCan { cc_id = cv
1059                           , cc_flavor = fl
1060                           , cc_fun = tc
1061                           , cc_tyargs = xis
1062                           , cc_rhs = xi })
1063       | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
1064
1065       , isTouchableMetaTyVar_InRange untch tv
1066            -- And it's a *touchable* unification variable
1067
1068       , typeKind xi `isSubKind` tyVarKind tv
1069          -- Must do a small kind check since TcCanonical invariants 
1070          -- on family equations only impose compatibility, not subkinding
1071
1072       , not (tv `elemVarEnv` tv_subst)
1073            -- Check not in extra_binds
1074            -- See Note [Solving Family Equations], Point 1
1075
1076       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1077            -- Occurs check: see Note [Solving Family Equations], Point 2
1078       = ASSERT ( not (isGivenOrSolved fl) )
1079         (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
1080
1081     dflt_funeq (cts_in, fun_eq_binds) ct
1082       = (cts_in `extendCCans` ct, fun_eq_binds)
1083 \end{code}
1084
1085 Note [Solving Family Equations] 
1086 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1087 After we are done with simplification we may be left with constraints of the form:
1088      [Wanted] F xis ~ beta 
1089 If 'beta' is a touchable unification variable not already bound in the TyBinds 
1090 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1091
1092 When is it ok to do so? 
1093     1) 'beta' must not already be defaulted to something. Example: 
1094
1095            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
1096            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
1097                                        have to report this as unsolved.
1098
1099     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
1100        set [beta := F xis] only if beta is not among the free variables of xis.
1101
1102     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
1103        of type family equations. See Inert Set invariants in TcInteract. 
1104
1105
1106 *********************************************************************************
1107 *                                                                               * 
1108 *                          Defaulting and disamgiguation                        *
1109 *                                                                               *
1110 *********************************************************************************
1111
1112 Basic plan behind applyDefaulting rules: 
1113  
1114  Step 1:  
1115     Split wanteds into defaultable groups, `groups' and the rest `rest_wanted' 
1116     For each defaultable group, do: 
1117       For each possible substitution for [alpha |-> tau] where `alpha' is the 
1118       group's variable, do: 
1119         1) Make up new TcEvBinds
1120         2) Extend TcS with (groupVariable 
1121         3) given_inert <- solveOne inert (given : a ~ tau) 
1122         4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1123         5) if unsolved == empty then 
1124                  sneakyUnify a |-> tau 
1125                  write the evidence bins
1126                  return (final_inert ++ group_constraints,[]) 
1127                       -- will contain the info (alpha |-> tau)!!
1128                  goto next defaultable group 
1129            if unsolved <> empty then 
1130                  throw away evidence binds
1131                  try next substitution 
1132      If you've run out of substitutions for this group, too bad, you failed 
1133                  return (inert,group) 
1134                  goto next defaultable group
1135  
1136  Step 2: 
1137    Collect all the (canonical-cts, wanteds) gathered this way. 
1138    - Do a solveGiven over the canonical-cts to make sure they are inert 
1139 ------------------------------------------------------------------------------------------
1140
1141
1142 \begin{code}
1143 applyDefaultingRules :: InertSet
1144                      -> CanonicalCts             -- All wanteds
1145                      -> TcS (Bag FlavoredEvVar)  -- All wanteds again!
1146 -- Return some *extra* givens, which express the 
1147 -- type-class-default choice
1148
1149 applyDefaultingRules inert wanteds
1150   | isEmptyBag wanteds 
1151   = return emptyBag
1152   | otherwise
1153   = do { untch <- getUntouchables
1154        ; tv_cts <- mapM (defaultTyVar untch) $
1155                    varSetElems (tyVarsOfCDicts wanteds) 
1156
1157        ; info@(_, default_tys, _) <- getDefaultInfo
1158        ; let groups = findDefaultableGroups info untch wanteds
1159        ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1160
1161        ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1162                                  , text "Type defaults =" <+> ppr deflt_cts])
1163
1164        ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1165
1166 ------------------
1167 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
1168 -- defaultTyVar is used on any un-instantiated meta type variables to
1169 -- default the kind of ? and ?? etc to *.  This is important to ensure
1170 -- that instance declarations match.  For example consider
1171 --      instance Show (a->b)
1172 --      foo x = show (\_ -> True)
1173 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), 
1174 -- and that won't match the typeKind (*) in the instance decl.  
1175 -- See test tc217.
1176 --
1177 -- We look only at touchable type variables. No further constraints
1178 -- are going to affect these type variables, so it's time to do it by
1179 -- hand.  However we aren't ready to default them fully to () or
1180 -- whatever, because the type-class defaulting rules have yet to run.
1181
1182 defaultTyVar untch the_tv 
1183   | isTouchableMetaTyVar_InRange untch the_tv
1184   , not (k `eqKind` default_k)
1185   = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1186        ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1187        ; return (unitBag (mkEvVarX ev (Wanted loc))) }
1188   | otherwise            
1189   = return emptyBag      -- The common case
1190   where
1191     k = tyVarKind the_tv
1192     default_k = defaultKind k
1193
1194
1195 ----------------
1196 findDefaultableGroups 
1197     :: ( SimplContext 
1198        , [Type]
1199        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1200     -> TcsUntouchables  -- Untouchable
1201     -> CanonicalCts     -- Unsolved
1202     -> [[(CanonicalCt,TcTyVar)]]
1203 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) 
1204                       untch wanteds
1205   | not (performDefaulting ctxt) = []
1206   | null default_tys             = []
1207   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1208   where 
1209     unaries     :: [(CanonicalCt, TcTyVar)]  -- (C tv) constraints
1210     non_unaries :: [CanonicalCt]             -- and *other* constraints
1211     
1212     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1213         -- Finds unary type-class constraints
1214     find_unary cc@(CDictCan { cc_tyargs = [ty] })
1215         | Just tv <- tcGetTyVar_maybe ty
1216         = Left (cc, tv)
1217     find_unary cc = Right cc  -- Non unary or non dictionary 
1218
1219     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
1220     bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries 
1221
1222     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1223
1224     is_defaultable_group ds@((_,tv):_)
1225         = isTyConableTyVar tv   -- Note [Avoiding spurious errors]
1226         && not (tv `elemVarSet` bad_tvs)
1227         && isTouchableMetaTyVar_InRange untch tv 
1228         && defaultable_classes [cc_class cc | (cc,_) <- ds]
1229     is_defaultable_group [] = panic "defaultable_group"
1230
1231     defaultable_classes clss 
1232         | extended_defaults = any isInteractiveClass clss
1233         | otherwise         = all is_std_class clss && (any is_num_class clss)
1234
1235     -- In interactive mode, or with -XExtendedDefaultRules,
1236     -- we default Show a to Show () to avoid graututious errors on "show []"
1237     isInteractiveClass cls 
1238         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1239
1240     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1241     -- is_num_class adds IsString to the standard numeric classes, 
1242     -- when -foverloaded-strings is enabled
1243
1244     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1245     -- Similarly is_std_class
1246
1247 ------------------------------
1248 disambigGroup :: [Type]                    -- The default types 
1249               -> InertSet                  -- Given inert 
1250               -> [(CanonicalCt, TcTyVar)]  -- All classes of the form (C a)
1251                                            --  sharing same type variable
1252               -> TcS (Bag FlavoredEvVar)
1253
1254 disambigGroup [] _inert _grp 
1255   = return emptyBag
1256 disambigGroup (default_ty:default_tys) inert group
1257   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1258        ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
1259        ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
1260              derived_eq = mkEvVarX ev der_flav
1261
1262        ; success <- tryTcS $
1263                     do { (_,final_inert) <- solveInteract inert $ listToBag $
1264                                             derived_eq : wanted_ev_vars
1265                        ; let (_, unsolved) = extractUnsolved final_inert                         
1266                        ; let wanted_unsolved = filterBag isWantedCt unsolved 
1267                                             -- Don't care about Derived's
1268                        ; return (isEmptyBag wanted_unsolved) }
1269        ; case success of
1270            True  ->  -- Success: record the type variable binding, and return
1271                     do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1272                        ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1273                        ; return (unitBag derived_eq) }
1274            False ->    -- Failure: try with the next type
1275                     do { traceTcS "disambigGroup failed, will try other default types"
1276                                   (ppr default_ty)
1277                        ; disambigGroup default_tys inert group } }
1278   where
1279     ((the_ct,the_tv):_) = group
1280     wanteds             = map fst group
1281     wanted_ev_vars :: [FlavoredEvVar]
1282     wanted_ev_vars      = map deCanonicalise wanteds
1283
1284     mk_derived_flavor :: CtFlavor -> CtFlavor
1285     mk_derived_flavor (Wanted loc) = Derived loc
1286     mk_derived_flavor _ = panic "Asked  to disambiguate given or derived!"
1287 \end{code}
1288
1289 Note [Avoiding spurious errors]
1290 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1291 When doing the unification for defaulting, we check for skolem
1292 type variables, and simply don't default them.  For example:
1293    f = (*)      -- Monomorphic
1294    g :: Num a => a -> a
1295    g x = f x x
1296 Here, we get a complaint when checking the type signature for g,
1297 that g isn't polymorphic enough; but then we get another one when
1298 dealing with the (Num a) context arising from f's definition;
1299 we try to unify a with Int (to default it), but find that it's
1300 already been unified with the rigid variable from g's type sig
1301
1302
1303
1304 *********************************************************************************
1305 *                                                                               * 
1306 *                   Utility functions
1307 *                                                                               *
1308 *********************************************************************************
1309
1310 \begin{code}
1311 newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
1312 newFlatWanteds orig theta
1313   = do { loc <- getCtLoc orig
1314        ; evs <- newWantedEvVars theta
1315        ; return (listToBag [EvVarX w loc | w <- evs]) }
1316 \end{code}