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