Merge branch 'master' of http://darcs.haskell.org//ghc
[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 Type     ( classifyPredType, PredTree(..) )
26 import Var
27 import VarSet
28 import VarEnv 
29 import TcEvidence
30 import TypeRep
31 import Name
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 () -- DV: for now
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       ; implics_from_flats <- solveInteractCts $ bagToList all_flats
388       ; unsolved_implics <- simpl_loop 1 (wc_impl wanted `unionBags` 
389                                                implics_from_flats)
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 See note [Simplifying RULE consraints] in TcRule
531
532 Note [RULE quanfification over equalities]
533 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
534 Decideing which equalities to quantify over is tricky:
535  * We do not want to quantify over insoluble equalities (Int ~ Bool)
536     (a) because we prefer to report a LHS type error
537     (b) because if such things end up in 'givens' we get a bogus
538         "inaccessible code" error
539
540  * But we do want to quantify over things like (a ~ F b), where
541    F is a type function.
542
543 The difficulty is that it's hard to tell what is insoluble!
544 So we see whether the simplificaiotn step yielded any type errors,
545 and if so refrain from quantifying over *any* equalites.
546
547 \begin{code}
548 simplifyRule :: RuleName 
549              -> WantedConstraints       -- Constraints from LHS
550              -> WantedConstraints       -- Constraints from RHS
551              -> TcM ([EvVar], WantedConstraints)   -- LHS evidence varaibles
552 -- See Note [Simplifying RULE constraints] in TcRule
553 simplifyRule name lhs_wanted rhs_wanted
554   = do { zonked_all <- zonkWC (lhs_wanted `andWC` rhs_wanted)
555        ; let doc = ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
556              untch = NoUntouchables
557                  -- We allow ourselves to unify environment 
558                  -- variables; hence NoUntouchables
559
560        ; (resid_wanted, _) <- runTcS (SimplInfer doc) untch emptyInert emptyWorkList $
561                               solveWanteds zonked_all
562
563        ; zonked_lhs <- zonkWC lhs_wanted
564
565        ; let (q_cts, non_q_cts) = partitionBag quantify_me (wc_flat zonked_lhs)
566              quantify_me  -- Note [RULE quantification over equalities]
567                | insolubleWC resid_wanted = quantify_insol
568                | otherwise                = quantify_normal
569
570              quantify_insol ct = not (isEqPred (ctPred ct))
571
572              quantify_normal ct
573                | EqPred t1 t2 <- classifyPredType (ctPred ct)
574                = not (t1 `eqType` t2)
575                | otherwise
576                = True
577              
578        ; traceTc "simplifyRule" $
579          vcat [ text "zonked_lhs" <+> ppr zonked_lhs 
580               , text "q_cts"      <+> ppr q_cts ]
581
582        ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
583                 , zonked_lhs { wc_flat = non_q_cts }) }
584 \end{code}
585
586
587 *********************************************************************************
588 *                                                                                 * 
589 *                                 Main Simplifier                                 *
590 *                                                                                 *
591 ***********************************************************************************
592
593 \begin{code}
594 simplifyCheck :: SimplContext
595               -> WantedConstraints      -- Wanted
596               -> TcM (Bag EvBind)
597 -- Solve a single, top-level implication constraint
598 -- e.g. typically one created from a top-level type signature
599 --          f :: forall a. [a] -> [a]
600 --          f x = rhs
601 -- We do this even if the function has no polymorphism:
602 --          g :: Int -> Int
603
604 --          g y = rhs
605 -- (whereas for *nested* bindings we would not create
606 --  an implication constraint for g at all.)
607 --
608 -- Fails if can't solve something in the input wanteds
609 simplifyCheck ctxt wanteds
610   = do { wanteds <- zonkWC wanteds
611
612        ; traceTc "simplifyCheck {" (vcat
613              [ ptext (sLit "wanted =") <+> ppr wanteds ])
614
615        ; (unsolved, eb1)
616            <- runTcS ctxt NoUntouchables emptyInert emptyWorkList $ 
617               solveWanteds wanteds
618
619        ; traceTc "simplifyCheck }" $ ptext (sLit "unsolved =") <+> ppr unsolved
620
621        ; traceTc "reportUnsolved {" empty
622        -- See Note [Deferring coercion errors to runtime]
623        ; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
624        ; eb2 <- reportUnsolved runtimeCoercionErrors unsolved 
625        ; traceTc "reportUnsolved }" empty
626
627        ; return (eb1 `unionBags` eb2) }
628 \end{code}
629
630 Note [Deferring coercion errors to runtime]
631 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
632
633 While developing, sometimes it is desirable to allow compilation to succeed even
634 if there are type errors in the code. Consider the following case:
635
636   module Main where
637
638   a :: Int
639   a = 'a'
640
641   main = print "b"
642
643 Even though `a` is ill-typed, it is not used in the end, so if all that we're
644 interested in is `main` it is handy to be able to ignore the problems in `a`.
645
646 Since we treat type equalities as evidence, this is relatively simple. Whenever
647 we run into a type mismatch in TcUnify, we normally just emit an error. But it
648 is always safe to defer the mismatch to the main constraint solver. If we do
649 that, `a` will get transformed into
650
651   co :: Int ~ Char
652   co = ...
653
654   a :: Int
655   a = 'a' `cast` co
656
657 The constraint solver would realize that `co` is an insoluble constraint, and
658 emit an error with `reportUnsolved`. But we can also replace the right-hand side
659 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
660 to compile, and it will run fine unless we evaluate `a`. This is what
661 `deferErrorsToRuntime` does.
662
663 It does this by keeping track of which errors correspond to which coercion
664 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
665 and does not fail if -fwarn-type-errors is on, so that we can continue
666 compilation. The errors are turned into warnings in `reportUnsolved`.
667
668 \begin{code}
669 solveWanteds :: WantedConstraints -> TcS WantedConstraints
670 -- Returns: residual constraints, plus evidence bindings 
671 -- NB: When we are called from TcM there are no inerts to pass down to TcS
672 solveWanteds wanted
673   = do { wc_out <- solve_wanteds wanted
674        ; let wc_ret = wc_out { wc_flat = keepWanted (wc_flat wc_out) } 
675                       -- Discard Derived
676        ; return wc_ret }
677
678 solve_wanteds :: WantedConstraints
679               -> TcS WantedConstraints  -- NB: wc_flats may be wanted *or* derived now
680 solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols }) 
681   = do { traceTcS "solveWanteds {" (ppr wanted)
682
683                  -- Try the flat bit
684                  -- Discard from insols all the derived/given constraints
685                  -- because they will show up again when we try to solve
686                  -- everything else.  Solving them a second time is a bit
687                  -- of a waste, but the code is simple, and the program is
688                  -- wrong anyway!
689
690        ; let all_flats = flats `unionBags` keepWanted insols
691        ; impls_from_flats <- solveInteractCts $ bagToList all_flats
692
693        -- solve_wanteds iterates when it is able to float equalities 
694        -- out of one or more of the implications. 
695        ; unsolved_implics <- simpl_loop 1 (implics `unionBags` impls_from_flats)
696
697        ; (insoluble_flats,unsolved_flats) <- extractUnsolvedTcS 
698
699        ; bb <- getTcEvBindsMap
700        ; tb <- getTcSTyBindsMap
701
702        ; traceTcS "solveWanteds }" $
703                  vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
704                       , text "unsolved_implics =" <+> ppr unsolved_implics
705                       , text "current evbinds  =" <+> ppr (evBindMapBinds bb)
706                       , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
707                       ]
708
709        ; (subst, remaining_unsolved_flats) <- solveCTyFunEqs unsolved_flats
710                 -- See Note [Solving Family Equations]
711                 -- NB: remaining_flats has already had subst applied
712
713        ; traceTcS "solveWanteds finished with" $
714                  vcat [ text "remaining_unsolved_flats =" <+> ppr remaining_unsolved_flats
715                       , text "subst =" <+> ppr subst
716                       ]
717
718        ; return $ 
719          WC { wc_flat  = mapBag (substCt subst) remaining_unsolved_flats
720             , wc_impl  = mapBag (substImplication subst) unsolved_implics
721             , wc_insol = mapBag (substCt subst) insoluble_flats }
722        }
723
724 simpl_loop :: Int
725            -> Bag Implication
726            -> TcS (Bag Implication)
727 simpl_loop n implics
728   | n > 10 
729   = traceTcS "solveWanteds: loop!" empty >> return implics
730   | otherwise 
731   = do { (implic_eqs, unsolved_implics) <- solveNestedImplications implics
732
733        ; inerts <- getTcSInerts
734        ; let ((_,unsolved_flats),_) = extractUnsolved inerts
735                                       
736        ; improve_eqs <- if not (isEmptyBag implic_eqs)
737                         then return implic_eqs
738                         else applyDefaultingRules unsolved_flats
739
740        ; traceTcS "solveWanteds: simpl_loop end" $
741              vcat [ text "improve_eqs      =" <+> ppr improve_eqs
742                   , text "unsolved_flats   =" <+> ppr unsolved_flats
743                   , text "unsolved_implics =" <+> ppr unsolved_implics ]
744
745        ; if isEmptyBag improve_eqs then return unsolved_implics 
746          else do { impls_from_eqs <- solveInteractCts $ bagToList improve_eqs
747                  ; simpl_loop (n+1) (unsolved_implics `unionBags` 
748                                                  impls_from_eqs)} }
749
750 solveNestedImplications :: Bag Implication
751                         -> TcS (Cts, Bag Implication)
752 -- Precondition: the TcS inerts may contain unsolved flats which have 
753 -- to be converted to givens before we go inside a nested implication.
754 solveNestedImplications implics
755   | isEmptyBag implics
756   = return (emptyBag, emptyBag)
757   | otherwise 
758   = do { inerts <- getTcSInerts
759        ; let ((_insoluble_flats, unsolved_flats),thinner_inerts) = extractUnsolved inerts 
760
761        ; (implic_eqs, unsolved_implics)
762            <- doWithInert thinner_inerts $ 
763               do { let pushed_givens = givens_from_wanteds unsolved_flats
764                        tcs_untouchables = filterVarSet isFlexiTcsTv $ 
765                                           tyVarsOfCts unsolved_flats
766                  -- See Note [Preparing inert set for implications]
767                  -- Push the unsolved wanteds inwards, but as givens
768                  ; traceTcS "solveWanteds: preparing inerts for implications {" $ 
769                    vcat [ppr tcs_untouchables, ppr pushed_givens]
770                  ; impls_from_givens <- solveInteractCts pushed_givens 
771                  ; MASSERT (isEmptyBag impls_from_givens)
772                    
773                  ; traceTcS "solveWanteds: } now doing nested implications {" empty
774                  ; flatMapBagPairM (solveImplication tcs_untouchables) implics }
775
776        -- ... and we are back in the original TcS inerts 
777        -- Notice that the original includes the _insoluble_flats so it was safe to ignore
778        -- them in the beginning of this function.
779        ; traceTcS "solveWanteds: done nested implications }" $
780                   vcat [ text "implic_eqs ="       <+> ppr implic_eqs
781                        , text "unsolved_implics =" <+> ppr unsolved_implics ]
782
783        ; return (implic_eqs, unsolved_implics) }
784
785   where givens_from_wanteds = foldrBag get_wanted []
786         get_wanted cc rest_givens
787             | pushable_wanted cc
788             = let fl   = ctEvidence cc
789                   gfl  = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol
790                                , ctev_evtm = EvId (ctev_evar fl)
791                                , ctev_pred = ctev_pred fl }
792                   this_given = cc { cc_ev = gfl }
793               in this_given : rest_givens
794             | otherwise = rest_givens 
795
796         pushable_wanted :: Ct -> Bool 
797         pushable_wanted cc 
798          | isWantedCt cc 
799          = isEqPred (ctPred cc) -- see Note [Preparing inert set for implications]
800          | otherwise = False 
801
802 solveImplication :: TcTyVarSet     -- Untouchable TcS unification variables
803                  -> Implication    -- Wanted
804                  -> TcS (Cts,      -- All wanted or derived floated equalities: var = type
805                          Bag Implication) -- Unsolved rest (always empty or singleton)
806 -- Precondition: The TcS monad contains an empty worklist and given-only inerts 
807 -- which after trying to solve this implication we must restore to their original value
808 solveImplication tcs_untouchables
809      imp@(Implic { ic_untch  = untch
810                  , ic_binds  = ev_binds
811                  , ic_skols  = skols 
812                  , ic_given  = givens
813                  , ic_wanted = wanteds
814                  , ic_loc    = loc })
815   = nestImplicTcS ev_binds (untch, tcs_untouchables) $
816     recoverTcS (return (emptyBag, emptyBag)) $
817        -- Recover from nested failures.  Even the top level is
818        -- just a bunch of implications, so failing at the first one is bad
819     do { traceTcS "solveImplication {" (ppr imp) 
820
821          -- Solve flat givens
822        ; impls_from_givens <- solveInteractGiven loc givens 
823        ; MASSERT (isEmptyBag impls_from_givens)
824          
825          -- Simplify the wanteds
826        ; WC { wc_flat = unsolved_flats
827             , wc_impl = unsolved_implics
828             , wc_insol = insols } <- solve_wanteds wanteds
829
830        ; let (res_flat_free, res_flat_bound)
831                  = floatEqualities skols givens unsolved_flats
832              final_flat = keepWanted res_flat_bound
833
834        ; let res_wanted = WC { wc_flat  = final_flat
835                              , wc_impl  = unsolved_implics
836                              , wc_insol = insols }
837
838              res_implic = unitImplication $
839                           imp { ic_wanted = res_wanted
840                               , ic_insol  = insolubleWC res_wanted }
841
842        ; evbinds <- getTcEvBindsMap
843
844        ; traceTcS "solveImplication end }" $ vcat
845              [ text "res_flat_free =" <+> ppr res_flat_free
846              , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds)
847              , text "res_implic =" <+> ppr res_implic ]
848
849        ; return (res_flat_free, res_implic) }
850     -- and we are back to the original inerts
851
852
853 floatEqualities :: [TcTyVar] -> [EvVar] -> Cts -> (Cts, Cts)
854 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
855 -- and come from the input wanted ev vars or deriveds 
856 floatEqualities skols can_given wantders
857   | hasEqualities can_given = (emptyBag, wantders)
858           -- Note [Float Equalities out of Implications]
859   | otherwise = partitionBag is_floatable wantders
860
861 -- TODO: Maybe we should try out /not/ floating constraints that contain touchables only, 
862 -- since they are inert and not going to interact with anything more in a more global scope.
863
864   where skol_set = mkVarSet skols
865         is_floatable :: Ct -> Bool
866         is_floatable ct
867           | ct_predty <- ctPred ct
868           , isEqPred ct_predty
869           = skol_set `disjointVarSet` tvs_under_fsks ct_predty
870         is_floatable _ct = False
871
872         tvs_under_fsks :: Type -> TyVarSet
873         -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
874         tvs_under_fsks (TyVarTy tv)     
875           | not (isTcTyVar tv)               = unitVarSet tv
876           | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
877           | otherwise                        = unitVarSet tv
878         tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
879         tvs_under_fsks (LitTy {})       = emptyVarSet
880         tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
881         tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
882         tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder 
883                                         -- can mention type variables!
884           | isTyVar tv                = inner_tvs `delVarSet` tv
885           | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
886                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
887           where
888             inner_tvs = tvs_under_fsks ty
889 \end{code}
890
891 Note [Preparing inert set for implications]
892 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
893 Before solving the nested implications, we convert any unsolved flat wanteds
894 to givens, and add them to the inert set.  Reasons:
895
896   a) In checking mode, suppresses unnecessary errors.  We already have
897      on unsolved-wanted error; adding it to the givens prevents any 
898      consequential errors from showing up
899
900   b) More importantly, in inference mode, we are going to quantify over this
901      constraint, and we *don't* want to quantify over any constraints that
902      are deducible from it.
903
904   c) Flattened type-family equalities must be exposed to the nested
905      constraints.  Consider
906         F b ~ alpha, (forall c.  F b ~ alpha)
907      Obviously this is soluble with [alpha := F b].  But the
908      unification is only done by solveCTyFunEqs, right at the end of
909      solveWanteds, and if we aren't careful we'll end up with an
910      unsolved goal inside the implication.  We need to "push" the
911      as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
912      can be used to solve the inner (F b
913      ~ alpha).  See Trac #4935.
914
915   d) There are other cases where interactions between wanteds that can help
916      to solve a constraint. For example
917
918         class C a b | a -> b
919
920         (C Int alpha), (forall d. C d blah => C Int a)
921
922      If we push the (C Int alpha) inwards, as a given, it can produce
923      a fundep (alpha~a) and this can float out again and be used to
924      fix alpha.  (In general we can't float class constraints out just
925      in case (C d blah) might help to solve (C Int a).)
926
927 The unsolved wanteds are *canonical* but they may not be *inert*,
928 because when made into a given they might interact with other givens.
929 Hence the call to solveInteract.  Example:
930
931  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta]) 
932
933 We were not able to solve (a ~w [beta]) but we can't just assume it as
934 given because the resulting set is not inert. Hence we have to do a
935 'solveInteract' step first. 
936
937 Finally, note that we convert them to [Given] and NOT [Given/Solved].
938 The reason is that Given/Solved are weaker than Givens and may be discarded.
939 As an example consider the inference case, where we may have, the following 
940 original constraints: 
941      [Wanted] F Int ~ Int
942              (F Int ~ a => F Int ~ a)
943 If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next 
944 given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting 
945 the (F Int ~ a) insoluble. Hence we should really convert the residual 
946 wanteds to plain old Given. 
947
948 We need only push in unsolved equalities both in checking mode and inference mode: 
949
950   (1) In checking mode we should not push given dictionaries in because of
951 example LongWayOverlapping.hs, where we might get strange overlap
952 errors between far-away constraints in the program.  But even in
953 checking mode, we must still push type family equations. Consider:
954
955    type instance F True a b = a 
956    type instance F False a b = b
957
958    [w] F c a b ~ gamma 
959    (c ~ True) => a ~ gamma 
960    (c ~ False) => b ~ gamma
961
962 Since solveCTyFunEqs happens at the very end of solving, the only way to solve
963 the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not 
964 merely Given/Solved because it has to interact with the top-level instance 
965 environment) and push it inside the implications. Now, when we come out again at
966 the end, having solved the implications solveCTyFunEqs will solve this equality.
967
968   (2) In inference mode, we recheck the final constraint in checking mode and
969 hence we will be able to solve inner implications from top-level quantified
970 constraints nonetheless.
971
972
973 Note [Extra TcsTv untouchables]
974 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
975 Furthemore, we record the inert set simplifier-generated unification
976 variables of the TcsTv kind (such as variables from instance that have
977 been applied, or unification flattens). These variables must be passed
978 to the implications as extra untouchable variables. Otherwise we have
979 the danger of double unifications. Example (from trac ticket #4494):
980
981    (F Int ~ uf)  /\  (forall a. C a => F Int ~ beta) 
982
983 In this example, beta is touchable inside the implication. The first
984 solveInteract step leaves 'uf' ununified. Then we move inside the
985 implication where a new constraint
986        uf  ~  beta  
987 emerges. We may spontaneously solve it to get uf := beta, so the whole
988 implication disappears but when we pop out again we are left with (F
989 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
990 uf will get unified *once more* to (F Int).
991
992 The solution is to record the TcsTvs (i.e. the simplifier-generated
993 unification variables) that are generated when solving the flats, and
994 make them untouchables for the nested implication. In the example
995 above uf would become untouchable, so beta would be forced to be
996 unified as beta := uf.
997
998 NB: A consequence is that every simplifier-generated TcsTv variable
999     that gets floated out of an implication becomes now untouchable
1000     next time we go inside that implication to solve any residual
1001     constraints. In effect, by floating an equality out of the
1002     implication we are committing to have it solved in the outside.
1003
1004 Note [Float Equalities out of Implications]
1005 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1006 We want to float equalities out of vanilla existentials, but *not* out 
1007 of GADT pattern matches. 
1008
1009 ---> TODO Expand in accordance to our discussion
1010
1011
1012 \begin{code}
1013
1014 solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)
1015 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
1016 -- See Note [Solving Family Equations]
1017 -- Returns: a bunch of unsolved constraints from the original Cts and implications
1018 --          where the newly generated equalities (alpha := F xi) have been substituted through.
1019 solveCTyFunEqs cts
1020  = do { untch   <- getUntouchables 
1021       ; let (unsolved_can_cts, (ni_subst, cv_binds))
1022                 = getSolvableCTyFunEqs untch cts
1023       ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
1024                                           , ppr ni_subst, ppr cv_binds
1025                                           ])
1026       ; mapM_ solve_one cv_binds
1027
1028       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
1029   where
1030     solve_one (Wanted { ctev_evar = cv }, tv, ty) 
1031       = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
1032     solve_one (Derived {}, tv, ty)
1033       = setWantedTyBind tv ty
1034     solve_one arg
1035       = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
1036 ------------
1037 type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
1038   -- The TvSubstEnv is not idempotent, but is loop-free
1039   -- See Note [Non-idempotent substitution] in Unify
1040 emptyFunEqBinds :: FunEqBinds
1041 emptyFunEqBinds = (emptyVarEnv, [])
1042
1043 extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
1044 extendFunEqBinds (tv_subst, cv_binds) fl tv ty
1045   = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
1046
1047 ------------
1048 getSolvableCTyFunEqs :: TcsUntouchables
1049                      -> Cts                -- Precondition: all Wanteds or Derived!
1050                      -> (Cts, FunEqBinds)  -- Postcondition: returns the unsolvables
1051 getSolvableCTyFunEqs untch cts
1052   = Bag.foldlBag dflt_funeq (emptyCts, emptyFunEqBinds) cts
1053   where
1054     dflt_funeq :: (Cts, FunEqBinds) -> Ct
1055                -> (Cts, FunEqBinds)
1056     dflt_funeq (cts_in, feb@(tv_subst, _))
1057                (CFunEqCan { cc_ev = fl
1058                           , cc_fun = tc
1059                           , cc_tyargs = xis
1060                           , cc_rhs = xi })
1061       | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
1062
1063       , isTouchableMetaTyVar_InRange untch tv
1064            -- And it's a *touchable* unification variable
1065
1066       , typeKind xi `tcIsSubKind` tyVarKind tv
1067          -- Must do a small kind check since TcCanonical invariants 
1068          -- on family equations only impose compatibility, not subkinding
1069
1070       , not (tv `elemVarEnv` tv_subst)
1071            -- Check not in extra_binds
1072            -- See Note [Solving Family Equations], Point 1
1073
1074       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1075            -- Occurs check: see Note [Solving Family Equations], Point 2
1076       = ASSERT ( not (isGiven fl) )
1077         (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
1078
1079     dflt_funeq (cts_in, fun_eq_binds) ct
1080       = (cts_in `extendCts` ct, fun_eq_binds)
1081 \end{code}
1082
1083 Note [Solving Family Equations] 
1084 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1085 After we are done with simplification we may be left with constraints of the form:
1086      [Wanted] F xis ~ beta 
1087 If 'beta' is a touchable unification variable not already bound in the TyBinds 
1088 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1089
1090 When is it ok to do so? 
1091     1) 'beta' must not already be defaulted to something. Example: 
1092
1093            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
1094            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
1095                                        have to report this as unsolved.
1096
1097     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
1098        set [beta := F xis] only if beta is not among the free variables of xis.
1099
1100     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
1101        of type family equations. See Inert Set invariants in TcInteract. 
1102
1103
1104 *********************************************************************************
1105 *                                                                               * 
1106 *                          Defaulting and disamgiguation                        *
1107 *                                                                               *
1108 *********************************************************************************
1109
1110 Basic plan behind applyDefaulting rules: 
1111  
1112  Step 1:  
1113     Split wanteds into defaultable groups, `groups' and the rest `rest_wanted' 
1114     For each defaultable group, do: 
1115       For each possible substitution for [alpha |-> tau] where `alpha' is the 
1116       group's variable, do: 
1117         1) Make up new TcEvBinds
1118         2) Extend TcS with (groupVariable 
1119         3) given_inert <- solveOne inert (given : a ~ tau) 
1120         4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1121         5) if unsolved == empty then 
1122                  sneakyUnify a |-> tau 
1123                  write the evidence bins
1124                  return (final_inert ++ group_constraints,[]) 
1125                       -- will contain the info (alpha |-> tau)!!
1126                  goto next defaultable group 
1127            if unsolved <> empty then 
1128                  throw away evidence binds
1129                  try next substitution 
1130      If you've run out of substitutions for this group, too bad, you failed 
1131                  return (inert,group) 
1132                  goto next defaultable group
1133  
1134  Step 2: 
1135    Collect all the (canonical-cts, wanteds) gathered this way. 
1136    - Do a solveGiven over the canonical-cts to make sure they are inert 
1137 ------------------------------------------------------------------------------------------
1138
1139
1140 \begin{code}
1141 applyDefaultingRules :: Cts      -- All wanteds
1142                      -> TcS Cts  -- All wanteds again!
1143 -- Return some *extra* givens, which express the 
1144 -- type-class-default choice
1145 applyDefaultingRules wanteds
1146   | isEmptyBag wanteds 
1147   = return emptyBag
1148   | otherwise
1149   = do { traceTcS "applyDefaultingRules { " $ 
1150                   text "wanteds =" <+> ppr wanteds
1151        ; untch <- getUntouchables
1152        ; tv_cts <- mapM (defaultTyVar untch) $
1153                    varSetElems (tyVarsOfCDicts wanteds)
1154
1155        ; info@(_, default_tys, _) <- getDefaultInfo
1156        ; let groups = findDefaultableGroups info untch wanteds
1157        ; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups
1158                                                  , text "untouchables=" <+> ppr  untch 
1159                                                  , text "info=" <+> ppr info ]
1160        ; deflt_cts <- mapM (disambigGroup default_tys) groups
1161
1162        ; traceTcS "applyDefaultingRules }" $ 
1163                   vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1164                        , text "Type defaults =" <+> ppr deflt_cts]
1165
1166        ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1167 \end{code}
1168
1169 Note [tryTcS in defaulting]
1170 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1171
1172 defaultTyVar and disambigGroup create new evidence variables for
1173 default equations, and hence update the EvVar cache. However, after
1174 applyDefaultingRules we will try to solve these default equations
1175 using solveInteractCts, which will consult the cache and solve those
1176 EvVars from themselves! That's wrong.
1177
1178 To avoid this problem we guard defaulting under a @tryTcS@ which leaves
1179 the original cache unmodified.
1180
1181 There is a second reason for @tryTcS@ in defaulting: disambGroup does
1182 some constraint solving to determine if a default equation is
1183 ``useful'' in solving some wanted constraints, but we want to
1184 discharge all evidence and unifications that may have happened during
1185 this constraint solving.
1186
1187 Finally, @tryTcS@ importantly does not inherit the original cache from
1188 the higher level but makes up a new cache, the reason is that disambigGroup
1189 will call solveInteractCts so the new derived and the wanteds must not be 
1190 in the cache!
1191
1192
1193 \begin{code}
1194 ------------------
1195 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS Cts
1196 -- defaultTyVar is used on any un-instantiated meta type variables to
1197 -- default the kind of OpenKind and ArgKind etc to *.  This is important to
1198 -- ensure that instance declarations match.  For example consider
1199 --      instance Show (a->b)
1200 --      foo x = show (\_ -> True)
1201 -- Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind, 
1202 -- and that won't match the typeKind (*) in the instance decl.  
1203 -- See test tc217.
1204 --
1205 -- We look only at touchable type variables. No further constraints
1206 -- are going to affect these type variables, so it's time to do it by
1207 -- hand.  However we aren't ready to default them fully to () or
1208 -- whatever, because the type-class defaulting rules have yet to run.
1209
1210 defaultTyVar untch the_tv 
1211   | isTouchableMetaTyVar_InRange untch the_tv
1212   , not (k `eqKind` default_k)
1213   = tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
1214     do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1215        ; eqv <- TcSMonad.newKindConstraint loc the_tv default_k
1216        ; case eqv of
1217            Fresh x -> 
1218              return $ unitBag $
1219              CNonCanonical { cc_ev = x, cc_depth = 0 }
1220            Cached _ -> return emptyBag }
1221 {- DELETEME
1222          if isNewEvVar eqv then 
1223              return $ unitBag (CNonCanonical { cc_id = evc_the_evvar eqv
1224                                              , cc_ev = fl, cc_depth = 0 })
1225          else return emptyBag }
1226 -}
1227
1228   | otherwise            
1229   = return emptyBag      -- The common case
1230   where
1231     k = tyVarKind the_tv
1232     default_k = defaultKind k
1233
1234
1235 ----------------
1236 findDefaultableGroups 
1237     :: ( SimplContext 
1238        , [Type]
1239        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1240     -> TcsUntouchables  -- Untouchable
1241     -> Cts      -- Unsolved
1242     -> [[(Ct,TcTyVar)]]
1243 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) 
1244                       untch wanteds
1245   | not (performDefaulting ctxt) = []
1246   | null default_tys             = []
1247   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1248   where 
1249     unaries     :: [(Ct, TcTyVar)]  -- (C tv) constraints
1250     non_unaries :: [Ct]             -- and *other* constraints
1251     
1252     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1253         -- Finds unary type-class constraints
1254     find_unary cc@(CDictCan { cc_tyargs = [ty] })
1255         | Just tv <- tcGetTyVar_maybe ty
1256         = Left (cc, tv)
1257     find_unary cc = Right cc  -- Non unary or non dictionary 
1258
1259     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
1260     bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries 
1261
1262     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1263
1264     is_defaultable_group ds@((_,tv):_)
1265         = let b1 = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
1266               b2 = not (tv `elemVarSet` bad_tvs)
1267               b3 = isTouchableMetaTyVar_InRange untch tv 
1268               b4 = defaultable_classes [cc_class cc | (cc,_) <- ds]
1269           in (b1 && b2 && b3 && b4)
1270           {- pprTrace "is_defaultable_group" (vcat [ text "isTyConable   " <+> ppr tv <+> ppr b1 
1271                                                    , text "is not in bad " <+> ppr tv <+> ppr b2 
1272                                                    , text "is touchable  " <+> ppr tv <+> ppr b3
1273                                                    , text "is defaultable" <+> ppr tv <+> ppr b4 ]) -}
1274     is_defaultable_group [] = panic "defaultable_group"
1275
1276     defaultable_classes clss 
1277         | extended_defaults = any isInteractiveClass clss
1278         | otherwise         = all is_std_class clss && (any is_num_class clss)
1279
1280     -- In interactive mode, or with -XExtendedDefaultRules,
1281     -- we default Show a to Show () to avoid graututious errors on "show []"
1282     isInteractiveClass cls 
1283         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1284
1285     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1286     -- is_num_class adds IsString to the standard numeric classes, 
1287     -- when -foverloaded-strings is enabled
1288
1289     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1290     -- Similarly is_std_class
1291
1292 ------------------------------
1293 disambigGroup :: [Type]           -- The default types 
1294               -> [(Ct, TcTyVar)]  -- All classes of the form (C a)
1295                                   --  sharing same type variable
1296               -> TcS Cts
1297
1298 disambigGroup []  _grp
1299   = return emptyBag
1300 disambigGroup (default_ty:default_tys) group
1301   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1302        ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
1303                     do { derived_eq <- tryTcS $
1304                                        -- I need a new tryTcS because we will call solveInteractCts below!
1305                             do { md <- newDerived (ctev_wloc the_fl) 
1306                                                   (mkTcEqPred (mkTyVarTy the_tv) default_ty)
1307                                                   -- ctev_wloc because constraint is not Given!
1308                                ; case md of 
1309                                     Nothing   -> return []
1310                                     Just ctev -> return [ mkNonCanonical ctev ] }
1311                             
1312                        ; traceTcS "disambigGroup (solving) {" 
1313                                   (text "trying to solve constraints along with default equations ...")
1314                        ; implics_from_defaulting <- 
1315                                     solveInteractCts (derived_eq ++ wanteds)
1316                        ; MASSERT (isEmptyBag implics_from_defaulting)
1317                                      -- Ignore implics: I don't think that a defaulting equation can cause
1318                                      -- new implications to be emitted. Maybe we have to revisit this.
1319                                      
1320                        ; (_,unsolved) <- extractUnsolvedTcS 
1321                        ; traceTcS "disambigGroup (solving) }"
1322                                   (text "disambigGroup unsolved =" <+> ppr (keepWanted unsolved))
1323                        ; if isEmptyBag (keepWanted unsolved) then -- Don't care about Derived's
1324                              return (Just $ listToBag derived_eq) 
1325                          else 
1326                              return Nothing 
1327                        }
1328        ; case success of
1329            Just cts -> -- Success: record the type variable binding, and return
1330                     do { wrapWarnTcS $ warnDefaulting wanteds default_ty
1331                        ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1332                        ; return cts }
1333            Nothing -> -- Failure: try with the next type
1334                     do { traceTcS "disambigGroup failed, will try other default types"
1335                                   (ppr default_ty)
1336                        ; disambigGroup default_tys group } }
1337   where
1338     ((the_ct,the_tv):_) = group
1339     the_fl              = cc_ev the_ct
1340     wanteds             = map fst group
1341 \end{code}
1342
1343 Note [Avoiding spurious errors]
1344 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1345 When doing the unification for defaulting, we check for skolem
1346 type variables, and simply don't default them.  For example:
1347    f = (*)      -- Monomorphic
1348    g :: Num a => a -> a
1349    g x = f x x
1350 Here, we get a complaint when checking the type signature for g,
1351 that g isn't polymorphic enough; but then we get another one when
1352 dealing with the (Num a) context arising from f's definition;
1353 we try to unify a with Int (to default it), but find that it's
1354 already been unified with the rigid variable from g's type sig
1355
1356
1357
1358 *********************************************************************************
1359 *                                                                               * 
1360 *                   Utility functions
1361 *                                                                               *
1362 *********************************************************************************
1363
1364 \begin{code}
1365 newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
1366 newFlatWanteds orig theta
1367   = do { loc <- getCtLoc orig
1368        ; mapM (inst_to_wanted loc) theta }
1369   where 
1370     inst_to_wanted loc pty 
1371           = do { v <- TcMType.newWantedEvVar pty 
1372                ; return $ 
1373                  CNonCanonical { cc_ev = Wanted { ctev_evar = v
1374                                                 , ctev_wloc = loc
1375                                                 , ctev_pred = pty }
1376                                , cc_depth = 0 } }
1377 \end{code}