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