Simplify the implementation of Implicit Parameters
[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(..), isIPPred_maybe )
26 import Var
27 import Unique
28 import VarSet
29 import VarEnv 
30 import TcEvidence
31 import TypeRep
32 import Name
33 import Bag
34 import ListSetOps
35 import Util
36 import PrelInfo
37 import PrelNames
38 import Class            ( classKey )
39 import BasicTypes       ( RuleName )
40 import Control.Monad    ( when )
41 import Outputable
42 import FastString
43 import TrieMap () -- DV: for now
44 import DynFlags
45 import Data.Maybe ( mapMaybe )
46 \end{code}
47
48
49 *********************************************************************************
50 *                                                                               * 
51 *                           External interface                                  *
52 *                                                                               *
53 *********************************************************************************
54
55
56 \begin{code}
57
58
59 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
60 -- Simplify top-level constraints
61 -- Usually these will be implications,
62 -- but when there is nothing to quantify we don't wrap
63 -- in a degenerate implication, so we do that here instead
64 simplifyTop wanteds 
65   = do { ev_binds_var <- newTcEvBinds
66                          
67        ; zonked_wanteds <- zonkWC wanteds
68        ; wc_first_go <- runTcSWithEvBinds ev_binds_var $ solveWanteds zonked_wanteds
69        ; cts <- applyTyVarDefaulting wc_first_go 
70                 -- See Note [Top-level Defaulting Plan]
71                 
72        ; let wc_for_loop = wc_first_go { wc_flat = wc_flat wc_first_go `unionBags` cts }
73                            
74        ; traceTc "simpl_top_loop {" $ text "zonked_wc =" <+> ppr zonked_wanteds
75        ; simpl_top_loop ev_binds_var wc_for_loop }
76     
77   where simpl_top_loop ev_binds_var wc
78           | isEmptyWC wc 
79           = do { traceTc "simpl_top_loop }" empty
80                ; TcRnMonad.getTcEvBinds ev_binds_var }
81           | otherwise
82           = do { wc_residual <- runTcSWithEvBinds ev_binds_var $ solveWanteds wc
83                ; let wc_flat_approximate = approximateWC wc_residual
84                ; (dflt_eqs,_unused_bind) <- runTcS $
85                                             applyDefaultingRules wc_flat_approximate
86                                             -- See Note [Top-level Defaulting Plan]
87                ; if isEmptyBag dflt_eqs then 
88                    do { traceTc "simpl_top_loop }" empty
89                       ; report_and_finish ev_binds_var wc_residual }
90                  else
91                    simpl_top_loop ev_binds_var $ 
92                    wc_residual { wc_flat = wc_flat wc_residual `unionBags` dflt_eqs } }
93
94         report_and_finish ev_binds_var wc_residual 
95           = do { eb1 <- TcRnMonad.getTcEvBinds ev_binds_var
96                ; traceTc "reportUnsolved {" empty
97                    -- See Note [Deferring coercion errors to runtime]
98                ; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
99                ; eb2 <- reportUnsolved runtimeCoercionErrors wc_residual
100                ; traceTc "reportUnsolved }" empty
101                ; return (eb1 `unionBags` eb2) }
102 \end{code}
103
104 Note [Top-level Defaulting Plan]
105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
106
107 We have considered two design choices for where/when to apply defaulting.   
108    (i) Do it in SimplCheck mode only /whenever/ you try to solve some 
109        flat constraints, maybe deep inside the context of implications.
110        This used to be the case in GHC 7.4.1.
111    (ii) Do it in a tight loop at simplifyTop, once all other constraint has 
112         finished. This is the current story.
113
114 Option (i) had many disadvantages: 
115    a) First it was deep inside the actual solver, 
116    b) Second it was dependent on the context (Infer a type signature, 
117       or Check a type signature, or Interactive) since we did not want 
118       to always start defaulting when inferring (though there is an exception to  
119       this see Note [Default while Inferring])
120    c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
121           f :: Int -> Bool
122           f x = const True (\y -> let w :: a -> a
123                                       w a = const a (y+1)
124                                   in w y)
125       We will get an implication constraint (for beta the type of y):
126                [untch=beta] forall a. 0 => Num beta
127       which we really cannot default /while solving/ the implication, since beta is
128       untouchable.
129
130 Instead our new defaulting story is to pull defaulting out of the solver loop and
131 go with option (i), implemented at SimplifyTop. Namely:
132      - First have a go at solving the residual constraint of the whole program
133      - Try to approximate it with a flat constraint
134      - Figure out derived defaulting equations for that flat constraint
135      - Go round the loop again if you did manage to get some equations
136
137 Now, that has to do with class defaulting. However there exists type variable /kind/
138 defaulting. Again this is done at the top-level and the plan is:
139      - At the top-level, once you had a go at solving the constraint, do 
140        figure out /all/ the touchable unification variables of the wanted contraints.
141      - Apply defaulting to their kinds
142
143 More details in Note [DefaultTyVar].
144
145 \begin{code}
146
147 ------------------
148 simplifyAmbiguityCheck :: Name -> WantedConstraints -> TcM (Bag EvBind)
149 simplifyAmbiguityCheck name wanteds
150   = traceTc "simplifyAmbiguityCheck" (text "name =" <+> ppr name) >> 
151     simplifyCheck wanteds
152  
153 ------------------
154 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
155 simplifyInteractive wanteds 
156   = traceTc "simplifyInteractive" empty >>
157     simplifyTop wanteds 
158
159 ------------------
160 simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
161                 -> TcM ()       -- Succeeds iff the constraint is soluble
162 simplifyDefault theta
163   = do { traceTc "simplifyInteractive" empty
164        ; wanted <- newFlatWanteds DefaultOrigin theta
165        ; _ignored_ev_binds <- simplifyCheck (mkFlatWC wanted)
166        ; return () }
167 \end{code}
168
169
170 ***********************************************************************************
171 *                                                                                 * 
172 *                            Deriving                                             *
173 *                                                                                 *
174 ***********************************************************************************
175
176 \begin{code}
177 simplifyDeriv :: CtOrigin
178               -> PredType
179               -> [TyVar]        
180               -> ThetaType              -- Wanted
181               -> TcM ThetaType  -- Needed
182 -- Given  instance (wanted) => C inst_ty 
183 -- Simplify 'wanted' as much as possibles
184 -- Fail if not possible
185 simplifyDeriv orig pred tvs theta 
186   = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
187                 -- The constraint solving machinery 
188                 -- expects *TcTyVars* not TyVars.  
189                 -- We use *non-overlappable* (vanilla) skolems
190                 -- See Note [Overlap and deriving]
191
192        ; let subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
193              skol_set   = mkVarSet tvs_skols
194              doc = ptext (sLit "deriving") <+> parens (ppr pred)
195
196        ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
197
198        ; traceTc "simplifyDeriv" $ 
199          vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
200        ; (residual_wanted, _ev_binds1)
201              <- runTcS $ solveWanteds (mkFlatWC wanted)
202
203        ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
204                          -- See Note [Exotic derived instance contexts]
205              get_good :: Ct -> Either PredType Ct
206              get_good ct | validDerivPred skol_set p = Left p
207                          | otherwise                 = Right ct
208                          where p = ctPred ct
209
210        -- We never want to defer these errors because they are errors in the
211        -- compiler! Hence the `False` below
212        ; _ev_binds2 <- reportUnsolved False (residual_wanted { wc_flat = bad })
213
214        ; let min_theta = mkMinimalBySCs (bagToList good)
215        ; return (substTheta subst_skol min_theta) }
216 \end{code}
217
218 Note [Overlap and deriving]
219 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
220 Consider some overlapping instances:
221   data Show a => Show [a] where ..
222   data Show [Char] where ...
223
224 Now a data type with deriving:
225   data T a = MkT [a] deriving( Show )
226
227 We want to get the derived instance
228   instance Show [a] => Show (T a) where...
229 and NOT
230   instance Show a => Show (T a) where...
231 so that the (Show (T Char)) instance does the Right Thing
232
233 It's very like the situation when we're inferring the type
234 of a function
235    f x = show [x]
236 and we want to infer
237    f :: Show [a] => a -> String
238
239 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
240              the context for the derived instance. 
241              Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
242
243 Note [Exotic derived instance contexts]
244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
245 In a 'derived' instance declaration, we *infer* the context.  It's a
246 bit unclear what rules we should apply for this; the Haskell report is
247 silent.  Obviously, constraints like (Eq a) are fine, but what about
248         data T f a = MkT (f a) deriving( Eq )
249 where we'd get an Eq (f a) constraint.  That's probably fine too.
250
251 One could go further: consider
252         data T a b c = MkT (Foo a b c) deriving( Eq )
253         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
254
255 Notice that this instance (just) satisfies the Paterson termination 
256 conditions.  Then we *could* derive an instance decl like this:
257
258         instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
259 even though there is no instance for (C Int a), because there just
260 *might* be an instance for, say, (C Int Bool) at a site where we
261 need the equality instance for T's.  
262
263 However, this seems pretty exotic, and it's quite tricky to allow
264 this, and yet give sensible error messages in the (much more common)
265 case where we really want that instance decl for C.
266
267 So for now we simply require that the derived instance context
268 should have only type-variable constraints.
269
270 Here is another example:
271         data Fix f = In (f (Fix f)) deriving( Eq )
272 Here, if we are prepared to allow -XUndecidableInstances we
273 could derive the instance
274         instance Eq (f (Fix f)) => Eq (Fix f)
275 but this is so delicate that I don't think it should happen inside
276 'deriving'. If you want this, write it yourself!
277
278 NB: if you want to lift this condition, make sure you still meet the
279 termination conditions!  If not, the deriving mechanism generates
280 larger and larger constraints.  Example:
281   data Succ a = S a
282   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
283
284 Note the lack of a Show instance for Succ.  First we'll generate
285   instance (Show (Succ a), Show a) => Show (Seq a)
286 and then
287   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
288 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
289
290 The bottom line
291 ~~~~~~~~~~~~~~~
292 Allow constraints which consist only of type variables, with no repeats.
293
294 *********************************************************************************
295 *                                                                                 * 
296 *                            Inference
297 *                                                                                 *
298 ***********************************************************************************
299
300 Note [Which variables to quantify]
301 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
302 Suppose the inferred type of a function is
303    T kappa (alpha:kappa) -> Int
304 where alpha is a type unification variable and 
305       kappa is a kind unification variable
306 Then we want to quantify over *both* alpha and kappa.  But notice that
307 kappa appears "at top level" of the type, as well as inside the kind
308 of alpha.  So it should be fine to just look for the "top level"
309 kind/type variables of the type, without looking transitively into the
310 kinds of those type variables.
311
312 \begin{code}
313 simplifyInfer :: Bool
314               -> Bool                  -- Apply monomorphism restriction
315               -> [(Name, TcTauType)]   -- Variables to be generalised,
316                                        -- and their tau-types
317               -> (Untouchables, WantedConstraints)
318               -> TcM ([TcTyVar],    -- Quantify over these type variables
319                       [EvVar],      -- ... and these constraints
320                       Bool,         -- The monomorphism restriction did something
321                                     --   so the results type is not as general as
322                                     --   it could be
323                       TcEvBinds)    -- ... binding these evidence variables
324 simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
325   | isEmptyWC wanteds
326   = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
327        ; zonked_taus <- zonkTcTypes (map snd name_taus)
328        ; let tvs_to_quantify = varSetElems (tyVarsOfTypes zonked_taus `minusVarSet` gbl_tvs)
329                                -- tvs_to_quantify can contain both kind and type vars
330                                -- See Note [Which variables to quantify]
331        ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
332        ; return (qtvs, [], False, emptyTcEvBinds) }
333
334   | otherwise
335   = do { zonked_wanteds <- zonkWC wanteds
336        ; gbl_tvs        <- tcGetGlobalTyVars
337        ; zonked_tau_tvs <- zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
338        ; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
339
340        ; traceTc "simplifyInfer {"  $ vcat
341              [ ptext (sLit "names =") <+> ppr (map fst name_taus)
342              , ptext (sLit "taus =") <+> ppr (map snd name_taus)
343              , ptext (sLit "tau_tvs (zonked) =") <+> ppr zonked_tau_tvs
344              , ptext (sLit "gbl_tvs =") <+> ppr gbl_tvs
345              , ptext (sLit "closed =") <+> ppr _top_lvl
346              , ptext (sLit "apply_mr =") <+> ppr apply_mr
347              , ptext (sLit "untch =") <+> ppr untch
348              , ptext (sLit "wanted =") <+> ppr zonked_wanteds
349              ]
350
351              -- Step 1
352              -- Make a guess at the quantified type variables
353              -- Then split the constraints on the baisis of those tyvars
354              -- to avoid unnecessarily simplifying a class constraint
355              -- See Note [Avoid unecessary constraint simplification]
356        ; let proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
357                           zonked_tau_tvs `minusVarSet` gbl_tvs
358              (perhaps_bound, surely_free)
359                         = partitionBag (quantifyMe proto_qtvs ctPred) (wc_flat zonked_wanteds)
360
361        ; traceTc "simplifyInfer proto"  $ vcat
362              [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
363              , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
364              , ptext (sLit "surely_fref =") <+> ppr surely_free
365              ]
366
367        ; traceTc "sinf"  $ vcat
368              [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
369              , ptext (sLit "surely_free   =") <+> ppr surely_free
370              ]
371              
372        ; emitFlats surely_free      
373          
374             -- Step 2 
375             -- Now simplify the possibly-bound constraints
376        ; let wanteds_to_approximate = zonked_wanteds { wc_flat = perhaps_bound }
377              
378        ; traceTc "simplifyWithApprox" $
379          ptext (sLit "wanteds_to_approximate = ") <+> ppr wanteds_to_approximate
380               -- 2.1) First try full-blown solving
381        ; ev_binds_var <- newTcEvBinds
382        ; wanted_transformed 
383              <- runTcSWithEvBinds ev_binds_var $ solveWanteds wanteds_to_approximate
384               -- 2.2) Fail fast if there is an insoluble constraint,
385               -- unless we are deferring errors to runtime
386        ; when (not runtimeCoercionErrors && insolubleWC wanted_transformed) $ 
387          do { _ev_binds <- reportUnsolved False wanted_transformed; failM }
388               -- 2.3) Candidates for quantification are an approximation of wanted_transformed
389        ; let quant_candidates = approximateWC wanted_transformed               
390               -- NB: Already the fixpoint of any unifications that may have happened                                
391               -- NB: We do not do any defaulting when inferring a type, this can lead
392               -- to less polymorphic types, see Note [Default while Inferring]
393                                 
394               -- 2.4) Minimize the quantification candidates                             
395        ; (quant_candidates_transformed, _extra_binds)   
396              <- runTcS $ solveWanteds $ WC { wc_flat  = quant_candidates
397                                            , wc_impl  = emptyBag
398                                            , wc_insol = emptyBag }
399               -- 2.5) Final candidates for quantification                
400        ; let final_quant_candidates :: Bag PredType
401              final_quant_candidates = mapBag ctPred $ 
402                                       keepWanted (wc_flat quant_candidates_transformed)
403              -- NB: Already the fixpoint of any unifications that may have happened
404                   
405        ; gbl_tvs        <- tcGetGlobalTyVars -- TODO: can we just use untch instead of gbl_tvs?
406        ; zonked_tau_tvs <- zonkTyVarsAndFV zonked_tau_tvs
407        
408        ; traceTc "simplifyWithApprox" $
409          vcat [ ptext (sLit "final_quant_candidates =") <+> ppr final_quant_candidates
410               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
411               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs ]
412          
413        ; let init_tvs        = zonked_tau_tvs `minusVarSet` gbl_tvs
414              poly_qtvs       = growPreds gbl_tvs id final_quant_candidates init_tvs
415              
416              pbound          = filterBag (quantifyMe poly_qtvs id) final_quant_candidates
417              
418        ; traceTc "simplifyWithApprox" $
419          vcat [ ptext (sLit "pbound =") <+> ppr pbound ]
420          
421              -- Monomorphism restriction
422        ; let mr_qtvs         = init_tvs `minusVarSet` constrained_tvs
423              constrained_tvs = tyVarsOfBag tyVarsOfType final_quant_candidates
424              mr_bites        = apply_mr && not (isEmptyBag pbound)
425
426              (qtvs, bound)
427                 | mr_bites  = (mr_qtvs,   emptyBag)
428                 | otherwise = (poly_qtvs, pbound)
429              
430
431        ; if isEmptyVarSet qtvs && isEmptyBag bound
432          then ASSERT( isEmptyBag (wc_insol wanted_transformed) )
433               do { traceTc "} simplifyInfer/no quantification" empty                   
434                  ; emitWC wanted_transformed
435                  ; return ([], [], mr_bites, TcEvBinds ev_binds_var) }
436          else do
437
438        { traceTc "simplifyApprox" $ 
439          ptext (sLit "bound are =") <+> ppr bound 
440          
441             -- Step 4, zonk quantified variables 
442        ; let minimal_flat_preds = mkMinimalBySCs $ bagToList bound
443              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
444                                    | (name, ty) <- name_taus ]
445                         -- Don't add the quantified variables here, because
446                         -- they are also bound in ic_skols and we want them to be
447                         -- tidied uniformly
448
449        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
450
451             -- Step 5
452             -- Minimize `bound' and emit an implication
453        ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
454                                            
455        ; lcl_env <- getLclTypeEnv
456        ; gloc <- getCtLoc skol_info
457                  
458        ; let implic = Implic { ic_untch    = untch 
459                              , ic_env      = lcl_env
460                              , ic_skols    = qtvs_to_return
461                              , ic_given    = minimal_bound_ev_vars
462                              , ic_wanted   = wanted_transformed 
463                              , ic_insol    = False
464                              , ic_binds    = ev_binds_var
465                              , ic_loc      = gloc }
466                       
467        ; emitImplication implic
468          
469        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
470              vcat [ ptext (sLit "implic =") <+> ppr implic
471                        -- ic_skols, ic_given give rest of result
472                   , ptext (sLit "qtvs =") <+> ppr qtvs_to_return
473                   , ptext (sLit "spb =") <+> ppr final_quant_candidates
474                   , ptext (sLit "bound =") <+> ppr bound ]
475
476        ; return ( qtvs_to_return, minimal_bound_ev_vars
477                 , mr_bites,  TcEvBinds ev_binds_var) } }
478     where 
479 \end{code}
480
481
482 Note [Note [Default while Inferring]
483 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
484 Our current plan is that defaulting only happens at simplifyTop and
485 not simplifyInfer.  This may lead to some insoluble deferred constraints
486 Example:
487
488 instance D g => C g Int b 
489
490 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
491 type inferred       = gamma -> gamma 
492
493 Now, if we try to default (alpha := Int) we will be able to refine the implication to 
494   (forall b. 0 => C gamma Int b) 
495 which can then be simplified further to 
496   (forall b. 0 => D gamma)
497 Finally we /can/ approximate this implication with (D gamma) and infer the quantified
498 type:  forall g. D g => g -> g
499
500 Instead what will currently happen is that we will get a quantified type 
501 (forall g. g -> g) and an implication:
502        forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
503
504 which, even if the simplifyTop defaults (alpha := Int) we will still be left with an 
505 unsolvable implication:
506        forall g. 0 => (forall b. 0 => D g)
507
508 The concrete example would be: 
509        h :: C g a s => g -> a -> ST s a
510        f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
511
512 But it is quite tedious to do defaulting and resolve the implication constraints and
513 we have not observed code breaking because of the lack of defaulting in inference so 
514 we don't do it for now.
515
516
517
518 Note [Minimize by Superclasses]
519 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
520
521 When we quantify over a constraint, in simplifyInfer we need to
522 quantify over a constraint that is minimal in some sense: For
523 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
524 we'd like to quantify over Ord alpha, because we can just get Eq alpha
525 from superclass selection from Ord alpha. This minimization is what
526 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
527 to check the original wanted.
528
529
530 \begin{code}
531
532
533 approximateWC :: WantedConstraints -> Cts
534 approximateWC wc = float_wc emptyVarSet wc
535   where 
536     float_wc :: TcTyVarSet -> WantedConstraints -> Cts
537     float_wc skols (WC { wc_flat = flat, wc_impl = implic }) = floats1 `unionBags` floats2
538       where floats1 = do_bag (float_flat skols) flat
539             floats2 = do_bag (float_implic skols) implic
540                                  
541     float_implic :: TcTyVarSet -> Implication -> Cts
542     float_implic skols imp
543       = float_wc (skols `extendVarSetList` ic_skols imp) (ic_wanted imp)
544             
545     float_flat :: TcTyVarSet -> Ct -> Cts
546     float_flat skols ct
547       | tyVarsOfCt ct `disjointVarSet` skols 
548       , isWantedCt ct = singleCt ct
549       | otherwise = emptyCts
550         
551     do_bag :: (a -> Bag c) -> Bag a -> Bag c
552     do_bag f = foldrBag (unionBags.f) emptyBag
553
554
555 \end{code}
556
557 \begin{code}
558 -- (growX gbls wanted tvs) grows a seed 'tvs' against the 
559 -- X-constraint 'wanted', nuking the 'gbls' at each stage
560 -- It's conservative in that if the seed could *possibly*
561 -- grow to include a type variable, then it does
562
563
564 growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
565 growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
566
567
568 --------  Helper functions, do not do fixpoint ------------------------
569 growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
570 growWC gbl_tvs wc = growImplics gbl_tvs             (wc_impl wc) .
571                     growPreds   gbl_tvs ctPred (wc_flat wc) .
572                     growPreds   gbl_tvs ctPred (wc_insol wc)
573
574 growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
575 growImplics gbl_tvs implics tvs
576   = foldrBag grow_implic tvs implics
577   where
578     grow_implic implic tvs
579       = grow tvs `delVarSetList` ic_skols implic
580       where
581         grow = growWC gbl_tvs (ic_wanted implic) .
582                growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
583                -- We must grow from givens too; see test IPRun
584
585
586 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
587 growPreds gbl_tvs get_pred items tvs
588   = foldrBag extend tvs items
589   where
590     extend item tvs = tvs `unionVarSet`
591                       (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
592
593 --------------------
594 quantifyMe :: TyVarSet      -- Quantifying over these
595            -> (a -> PredType)
596            -> a -> Bool     -- True <=> quantify over this wanted
597 quantifyMe qtvs toPred ct
598   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
599   | otherwise     = tyVarsOfType pred `intersectsVarSet` qtvs
600   where
601     pred = toPred ct
602 \end{code}
603
604 Note [Avoid unecessary constraint simplification]
605 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
606 When inferring the type of a let-binding, with simplifyInfer,
607 try to avoid unnecessariliy simplifying class constraints.
608 Doing so aids sharing, but it also helps with delicate 
609 situations like
610
611    instance C t => C [t] where ..
612
613    f :: C [t] => ....
614    f x = let g y = ...(constraint C [t])... 
615          in ...
616 When inferring a type for 'g', we don't want to apply the
617 instance decl, because then we can't satisfy (C t).  So we
618 just notice that g isn't quantified over 't' and partition
619 the contraints before simplifying.
620
621 This only half-works, but then let-generalisation only half-works.
622 The example that needs this is:
623
624    typecheck/should_compile/T4361.hs
625
626
627 Note [Inheriting implicit parameters]
628 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
629 Consider this:
630
631         f x = (x::Int) + ?y
632
633 where f is *not* a top-level binding.
634 From the RHS of f we'll get the constraint (?y::Int).
635 There are two types we might infer for f:
636
637         f :: Int -> Int
638
639 (so we get ?y from the context of f's definition), or
640
641         f :: (?y::Int) => Int -> Int
642
643 At first you might think the first was better, becuase then
644 ?y behaves like a free variable of the definition, rather than
645 having to be passed at each call site.  But of course, the WHOLE
646 IDEA is that ?y should be passed at each call site (that's what
647 dynamic binding means) so we'd better infer the second.
648
649 BOTTOM LINE: when *inferring types* you *must* quantify 
650 over implicit parameters. See the predicate isFreeWhenInferring.
651
652
653 *********************************************************************************
654 *                                                                                 * 
655 *                             RULES                                               *
656 *                                                                                 *
657 ***********************************************************************************
658
659 See note [Simplifying RULE consraints] in TcRule
660
661 Note [RULE quanfification over equalities]
662 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
663 Decideing which equalities to quantify over is tricky:
664  * We do not want to quantify over insoluble equalities (Int ~ Bool)
665     (a) because we prefer to report a LHS type error
666     (b) because if such things end up in 'givens' we get a bogus
667         "inaccessible code" error
668
669  * But we do want to quantify over things like (a ~ F b), where
670    F is a type function.
671
672 The difficulty is that it's hard to tell what is insoluble!
673 So we see whether the simplificaiotn step yielded any type errors,
674 and if so refrain from quantifying over *any* equalites.
675
676 \begin{code}
677 simplifyRule :: RuleName 
678              -> WantedConstraints       -- Constraints from LHS
679              -> WantedConstraints       -- Constraints from RHS
680              -> TcM ([EvVar], WantedConstraints)   -- LHS evidence varaibles
681 -- See Note [Simplifying RULE constraints] in TcRule
682 simplifyRule name lhs_wanted rhs_wanted
683   = do { zonked_all <- zonkWC (lhs_wanted `andWC` rhs_wanted)
684        ; let doc = ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
685              
686                  -- We allow ourselves to unify environment 
687                  -- variables: runTcS runs with NoUntouchables
688        ; (resid_wanted, _) <- runTcS (solveWanteds zonked_all)
689
690        ; zonked_lhs <- zonkWC lhs_wanted
691
692        ; let (q_cts, non_q_cts) = partitionBag quantify_me (wc_flat zonked_lhs)
693              quantify_me  -- Note [RULE quantification over equalities]
694                | insolubleWC resid_wanted = quantify_insol
695                | otherwise                = quantify_normal
696
697              quantify_insol ct = not (isEqPred (ctPred ct))
698
699              quantify_normal ct
700                | EqPred t1 t2 <- classifyPredType (ctPred ct)
701                = not (t1 `eqType` t2)
702                | otherwise
703                = True
704              
705        ; traceTc "simplifyRule" $
706          vcat [ doc
707               , text "zonked_lhs" <+> ppr zonked_lhs 
708               , text "q_cts"      <+> ppr q_cts ]
709
710        ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
711                 , zonked_lhs { wc_flat = non_q_cts }) }
712 \end{code}
713
714
715 *********************************************************************************
716 *                                                                                 * 
717 *                                 Main Simplifier                                 *
718 *                                                                                 *
719 ***********************************************************************************
720
721 \begin{code}
722 simplifyCheck :: WantedConstraints      -- Wanted
723               -> TcM (Bag EvBind)
724 -- Solve a single, top-level implication constraint
725 -- e.g. typically one created from a top-level type signature
726 --          f :: forall a. [a] -> [a]
727 --          f x = rhs
728 -- We do this even if the function has no polymorphism:
729 --          g :: Int -> Int
730
731 --          g y = rhs
732 -- (whereas for *nested* bindings we would not create
733 --  an implication constraint for g at all.)
734 --
735 -- Fails if can't solve something in the input wanteds
736 simplifyCheck wanteds
737   = do { wanteds <- zonkWC wanteds
738
739        ; traceTc "simplifyCheck {" (vcat
740              [ ptext (sLit "wanted =") <+> ppr wanteds ])
741
742        ; (unsolved, eb1) <- runTcS (solveWanteds wanteds)
743
744        ; traceTc "simplifyCheck }" $ ptext (sLit "unsolved =") <+> ppr unsolved
745
746        ; traceTc "reportUnsolved {" empty
747        -- See Note [Deferring coercion errors to runtime]
748        ; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
749        ; eb2 <- reportUnsolved runtimeCoercionErrors unsolved 
750        ; traceTc "reportUnsolved }" empty
751
752        ; return (eb1 `unionBags` eb2) }
753 \end{code}
754
755 Note [Deferring coercion errors to runtime]
756 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
757
758 While developing, sometimes it is desirable to allow compilation to succeed even
759 if there are type errors in the code. Consider the following case:
760
761   module Main where
762
763   a :: Int
764   a = 'a'
765
766   main = print "b"
767
768 Even though `a` is ill-typed, it is not used in the end, so if all that we're
769 interested in is `main` it is handy to be able to ignore the problems in `a`.
770
771 Since we treat type equalities as evidence, this is relatively simple. Whenever
772 we run into a type mismatch in TcUnify, we normally just emit an error. But it
773 is always safe to defer the mismatch to the main constraint solver. If we do
774 that, `a` will get transformed into
775
776   co :: Int ~ Char
777   co = ...
778
779   a :: Int
780   a = 'a' `cast` co
781
782 The constraint solver would realize that `co` is an insoluble constraint, and
783 emit an error with `reportUnsolved`. But we can also replace the right-hand side
784 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
785 to compile, and it will run fine unless we evaluate `a`. This is what
786 `deferErrorsToRuntime` does.
787
788 It does this by keeping track of which errors correspond to which coercion
789 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
790 and does not fail if -fwarn-type-errors is on, so that we can continue
791 compilation. The errors are turned into warnings in `reportUnsolved`.
792
793 \begin{code}
794 solveWanteds :: WantedConstraints -> TcS WantedConstraints
795 -- Returns: residual constraints, plus evidence bindings 
796 -- NB: When we are called from TcM there are no inerts to pass down to TcS
797 solveWanteds wanted
798   = do { (_,wc_out) <- solve_wanteds wanted
799        ; let wc_ret = wc_out { wc_flat = keepWanted (wc_flat wc_out) } 
800                       -- Discard Derived
801        ; return wc_ret }
802
803 solve_wanteds :: WantedConstraints
804               -> TcS (TvSubst, WantedConstraints) 
805               -- NB: wc_flats may be wanted *or* derived now
806               -- Returns the flattening substitution as well in case we need to apply it
807 solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols }) 
808   = do { traceTcS "solveWanteds {" (ppr wanted)
809
810                  -- Try the flat bit
811                  -- Discard from insols all the derived/given constraints
812                  -- because they will show up again when we try to solve
813                  -- everything else.  Solving them a second time is a bit
814                  -- of a waste, but the code is simple, and the program is
815                  -- wrong anyway!
816
817                  -- DV: why only keepWanted? We make sure that we never float out
818                  -- whatever constraints can yield equalities, including class 
819                  -- constraints with functional dependencies and hence all the derived
820                  -- that were potentially insoluble will be re-generated.
821                  -- (It would not hurt though to just keep the wanted and the derived)
822                  -- See Note [The HasEqualities Predicate] in Inst.lhs
823          
824        ; let all_flats = flats `unionBags` keepWanted insols
825                          
826        ; impls_from_flats <- solveInteractCts $ bagToList all_flats
827
828        -- solve_wanteds iterates when it is able to float equalities 
829        -- out of one or more of the implications. 
830        ; unsolved_implics <- simpl_loop 1 (implics `unionBags` impls_from_flats)
831
832        ; (insoluble_flats,unsolved_flats) <- extractUnsolvedTcS 
833
834        ; bb <- getTcEvBindsMap
835        ; tb <- getTcSTyBindsMap
836
837        ; traceTcS "solveWanteds }" $
838                  vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
839                       , text "unsolved_implics =" <+> ppr unsolved_implics
840                       , text "current evbinds  =" <+> ppr (evBindMapBinds bb)
841                       , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
842                       ]
843
844        ; (subst, remaining_unsolved_flats) <- solveCTyFunEqs unsolved_flats
845                 -- See Note [Solving Family Equations]
846                 -- NB: remaining_flats has already had subst applied
847
848        ; traceTcS "solveWanteds finished with" $
849                  vcat [ text "remaining_unsolved_flats =" <+> ppr remaining_unsolved_flats
850                       , text "subst =" <+> ppr subst
851                       ]
852
853        ; return $ 
854          (subst, WC { wc_flat  = mapBag (substCt subst) remaining_unsolved_flats
855                     , wc_impl  = mapBag (substImplication subst) unsolved_implics
856                     , wc_insol = mapBag (substCt subst) insoluble_flats })
857        }
858
859 simpl_loop :: Int
860            -> Bag Implication
861            -> TcS (Bag Implication)
862 simpl_loop n implics
863   | n > 10 
864   = traceTcS "solveWanteds: loop!" empty >> return implics
865   | otherwise 
866   = do { (implic_eqs, unsolved_implics) <- solveNestedImplications implics
867
868        ; inerts <- getTcSInerts
869        ; let ((_,unsolved_flats),_) = extractUnsolved inerts
870                                       
871        ; let improve_eqs = implic_eqs
872              -- NB: improve_eqs used to contain defaulting equations HERE but 
873              -- defaulting now happens only at simplifyTop and not deep inside 
874              -- simpl_loop! See Note [Top-level Defaulting Plan]
875              
876        ; traceTcS "solveWanteds: simpl_loop end" $
877              vcat [ text "improve_eqs      =" <+> ppr improve_eqs
878                   , text "unsolved_flats   =" <+> ppr unsolved_flats
879                   , text "unsolved_implics =" <+> ppr unsolved_implics ]
880
881        ; if isEmptyBag improve_eqs then return unsolved_implics 
882          else do { impls_from_eqs <- solveInteractCts $ bagToList improve_eqs
883                  ; simpl_loop (n+1) (unsolved_implics `unionBags` 
884                                                  impls_from_eqs)} }
885
886 solveNestedImplications :: Bag Implication
887                         -> TcS (Cts, Bag Implication)
888 -- Precondition: the TcS inerts may contain unsolved flats which have 
889 -- to be converted to givens before we go inside a nested implication.
890 solveNestedImplications implics
891   | isEmptyBag implics
892   = return (emptyBag, emptyBag)
893   | otherwise 
894   = do { inerts <- getTcSInerts
895        ; traceTcS "solveNestedImplications starting, inerts are:" $ ppr inerts
896          
897        ; let ((_insoluble_flats, unsolved_flats),thinner_inerts) = extractUnsolved inerts 
898        ; traceTcS "solveNestedImplications starting, more info:" $ 
899          vcat [ text "inerts          = " <+> ppr inerts
900               , text "insoluble_flats = " <+> ppr _insoluble_flats
901               , text "unsolved_flats  = " <+> ppr unsolved_flats
902               , text "thinner_inerts  = " <+> ppr thinner_inerts ]
903          
904        ; (implic_eqs, unsolved_implics)
905            <- doWithInert thinner_inerts $ 
906               do { let pushed_givens = givens_from_wanteds unsolved_flats
907                        tcs_untouchables 
908                          = foldr (unionVarSet . tyVarsOfCt) emptyVarSet pushed_givens
909                                           -- Typically pushed_givens is very small, consists
910                                           -- only of unsolved equalities, so no inefficiency 
911                                           -- danger.
912                                                                                     
913                                           
914                  -- See Note [Preparing inert set for implications]
915                  -- Push the unsolved wanteds inwards, but as givens
916                  ; traceTcS "solveWanteds: preparing inerts for implications {" $ 
917                    vcat [ppr tcs_untouchables, ppr pushed_givens]
918                  ; impls_from_givens <- solveInteractCts pushed_givens
919                                         
920                  ; MASSERT (isEmptyBag impls_from_givens)
921                        -- impls_from_givens must be empty, since we are reacting givens
922                        -- with givens, and they can never generate extra implications 
923                        -- from decomposition of ForAll types. (Whereas wanteds can, see
924                        -- TcCanonical, canEq ForAll-ForAll case)
925                    
926                  ; traceTcS "solveWanteds: } now doing nested implications {" empty
927                  ; flatMapBagPairM (solveImplication tcs_untouchables) implics }
928
929        -- ... and we are back in the original TcS inerts 
930        -- Notice that the original includes the _insoluble_flats so it was safe to ignore
931        -- them in the beginning of this function.
932        ; traceTcS "solveWanteds: done nested implications }" $
933                   vcat [ text "implic_eqs ="       <+> ppr implic_eqs
934                        , text "unsolved_implics =" <+> ppr unsolved_implics ]
935
936        ; return (implic_eqs, unsolved_implics) }
937
938   where givens_from_wanteds = foldrBag get_wanted []
939         get_wanted cc rest_givens
940             | pushable_wanted cc
941             = let fl   = ctEvidence cc
942                   gfl  = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol
943                                , ctev_evtm = EvId (ctev_evar fl)
944                                , ctev_pred = ctev_pred fl }
945                   this_given = cc { cc_ev = gfl }
946               in this_given : rest_givens
947             | otherwise = rest_givens 
948
949         pushable_wanted :: Ct -> Bool 
950         pushable_wanted cc 
951          | isWantedCt cc 
952          = isEqPred (ctPred cc) -- see Note [Preparing inert set for implications]
953          | otherwise = False 
954
955 solveImplication :: TcTyVarSet     -- Untouchable TcS unification variables
956                  -> Implication    -- Wanted
957                  -> TcS (Cts,      -- All wanted or derived floated equalities: var = type
958                          Bag Implication) -- Unsolved rest (always empty or singleton)
959 -- Precondition: The TcS monad contains an empty worklist and given-only inerts 
960 -- which after trying to solve this implication we must restore to their original value
961 solveImplication tcs_untouchables
962      imp@(Implic { ic_untch  = untch
963                  , ic_binds  = ev_binds
964                  , ic_skols  = skols 
965                  , ic_given  = givens
966                  , ic_wanted = wanteds
967                  , ic_loc    = loc })
968   = shadowIPs givens $    -- See Note [Shadowing of Implicit Parameters]
969     nestImplicTcS ev_binds (untch, tcs_untouchables) $
970     recoverTcS (return (emptyBag, emptyBag)) $
971        -- Recover from nested failures.  Even the top level is
972        -- just a bunch of implications, so failing at the first one is bad
973     do { traceTcS "solveImplication {" (ppr imp) 
974
975          -- Solve flat givens
976        ; impls_from_givens <- solveInteractGiven loc givens 
977        ; MASSERT (isEmptyBag impls_from_givens)
978          
979          -- Simplify the wanteds
980        ; (_flat_subst, 
981            WC { wc_flat = unsolved_flats
982               , wc_impl = unsolved_implics
983               , wc_insol = insols }) <- solve_wanteds wanteds
984           -- NB: Not solveWanteds because we need the derived equalities,            
985           -- which may not be solvable (due to touchability) in this implication
986           -- but may become solvable by spontantenous unification outside. 
987
988        ; let (res_flat_free, res_flat_bound)
989                  = floatEqualities skols givens unsolved_flats
990              final_flat = keepWanted res_flat_bound
991
992        ; let res_wanted = WC { wc_flat  = final_flat
993                              , wc_impl  = unsolved_implics
994                              , wc_insol = insols }
995
996              res_implic = unitImplication $
997                           imp { ic_wanted = res_wanted
998                               , ic_insol  = insolubleWC res_wanted }
999
1000        ; evbinds <- getTcEvBindsMap
1001
1002        ; traceTcS "solveImplication end }" $ vcat
1003              [ text "res_flat_free =" <+> ppr res_flat_free
1004              , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds)
1005              , text "res_implic =" <+> ppr res_implic ]
1006
1007        ; return (res_flat_free, res_implic) }
1008     -- and we are back to the original inerts
1009
1010
1011 floatEqualities :: [TcTyVar] -> [EvVar] -> Cts -> (Cts, Cts)
1012 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
1013 -- and come from the input wanted ev vars or deriveds 
1014 floatEqualities skols can_given wantders
1015   | hasEqualities can_given = (emptyBag, wantders)
1016           -- Note [Float Equalities out of Implications]
1017   | otherwise = partitionBag is_floatable wantders
1018   where skol_set = mkVarSet skols
1019         is_floatable :: Ct -> Bool
1020         is_floatable ct
1021           | ct_predty <- ctPred ct
1022           , isEqPred ct_predty
1023           = skol_set `disjointVarSet` tvs_under_fsks ct_predty
1024         is_floatable _ct = False
1025
1026         tvs_under_fsks :: Type -> TyVarSet
1027         -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
1028         tvs_under_fsks (TyVarTy tv)     
1029           | not (isTcTyVar tv)               = unitVarSet tv
1030           | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
1031           | otherwise                        = unitVarSet tv
1032         tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
1033         tvs_under_fsks (LitTy {})       = emptyVarSet
1034         tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
1035         tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
1036         tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder 
1037                                         -- can mention type variables!
1038           | isTyVar tv                = inner_tvs `delVarSet` tv
1039           | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
1040                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
1041           where
1042             inner_tvs = tvs_under_fsks ty
1043
1044 shadowIPs :: [EvVar] -> TcS a -> TcS a
1045 shadowIPs gs m
1046   | null shadowed = m
1047   | otherwise     = do is <- getTcSInerts
1048                        doWithInert (purgeShadowed is) m
1049   where
1050   shadowed  = mapMaybe isIP gs
1051
1052   isIP g    = do p <- evVarPred_maybe g
1053                  (x,_) <- isIPPred_maybe p
1054                  return x
1055
1056   isShadowedCt ct = isShadowedEv (ctEvidence ct)
1057   isShadowedEv ev = case isIPPred_maybe (ctEvPred ev) of
1058                       Just (x,_) -> x `elem` shadowed
1059                       _          -> False
1060
1061   purgeShadowed is = is { inert_cans = purgeCans (inert_cans is)
1062                         , inert_solved = purgeSolved (inert_solved is)
1063                         }
1064
1065   purgeDicts    = snd . partitionCCanMap isShadowedCt
1066   purgeCans ics = ics { inert_dicts = purgeDicts (inert_dicts ics) }
1067   purgeSolved   = filterSolved (not . isShadowedEv)
1068 \end{code}
1069
1070 Note [Preparing inert set for implications]
1071 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1072 Before solving the nested implications, we convert any unsolved flat wanteds
1073 to givens, and add them to the inert set.  Reasons:
1074
1075   a) In checking mode, suppresses unnecessary errors.  We already have
1076      on unsolved-wanted error; adding it to the givens prevents any 
1077      consequential errors from showing up
1078
1079   b) More importantly, in inference mode, we are going to quantify over this
1080      constraint, and we *don't* want to quantify over any constraints that
1081      are deducible from it.
1082
1083   c) Flattened type-family equalities must be exposed to the nested
1084      constraints.  Consider
1085         F b ~ alpha, (forall c.  F b ~ alpha)
1086      Obviously this is soluble with [alpha := F b].  But the
1087      unification is only done by solveCTyFunEqs, right at the end of
1088      solveWanteds, and if we aren't careful we'll end up with an
1089      unsolved goal inside the implication.  We need to "push" the
1090      as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
1091      can be used to solve the inner (F b
1092      ~ alpha).  See Trac #4935.
1093
1094   d) There are other cases where interactions between wanteds that can help
1095      to solve a constraint. For example
1096
1097         class C a b | a -> b
1098
1099         (C Int alpha), (forall d. C d blah => C Int a)
1100
1101      If we push the (C Int alpha) inwards, as a given, it can produce
1102      a fundep (alpha~a) and this can float out again and be used to
1103      fix alpha.  (In general we can't float class constraints out just
1104      in case (C d blah) might help to solve (C Int a).)
1105
1106 The unsolved wanteds are *canonical* but they may not be *inert*,
1107 because when made into a given they might interact with other givens.
1108 Hence the call to solveInteract.  Example:
1109
1110  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta]) 
1111
1112 We were not able to solve (a ~w [beta]) but we can't just assume it as
1113 given because the resulting set is not inert. Hence we have to do a
1114 'solveInteract' step first. 
1115
1116 Finally, note that we convert them to [Given] and NOT [Given/Solved].
1117 The reason is that Given/Solved are weaker than Givens and may be discarded.
1118 As an example consider the inference case, where we may have, the following 
1119 original constraints: 
1120      [Wanted] F Int ~ Int
1121              (F Int ~ a => F Int ~ a)
1122 If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next 
1123 given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting 
1124 the (F Int ~ a) insoluble. Hence we should really convert the residual 
1125 wanteds to plain old Given. 
1126
1127 We need only push in unsolved equalities both in checking mode and inference mode: 
1128
1129   (1) In checking mode we should not push given dictionaries in because of
1130 example LongWayOverlapping.hs, where we might get strange overlap
1131 errors between far-away constraints in the program.  But even in
1132 checking mode, we must still push type family equations. Consider:
1133
1134    type instance F True a b = a 
1135    type instance F False a b = b
1136
1137    [w] F c a b ~ gamma 
1138    (c ~ True) => a ~ gamma 
1139    (c ~ False) => b ~ gamma
1140
1141 Since solveCTyFunEqs happens at the very end of solving, the only way to solve
1142 the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not 
1143 merely Given/Solved because it has to interact with the top-level instance 
1144 environment) and push it inside the implications. Now, when we come out again at
1145 the end, having solved the implications solveCTyFunEqs will solve this equality.
1146
1147   (2) In inference mode, we recheck the final constraint in checking mode and
1148 hence we will be able to solve inner implications from top-level quantified
1149 constraints nonetheless.
1150
1151
1152 Note [Extra TcsTv untouchables]
1153 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1154
1155 Whenever we are solving a bunch of flat constraints, they may contain 
1156 the following sorts of 'touchable' unification variables:
1157    
1158    (i)   Born-touchables in that scope
1159  
1160    (ii)  Simplifier-generated unification variables, such as unification 
1161          flatten variables
1162
1163    (iii) Touchables that have been floated out from some nested 
1164          implications, see Note [Float Equalities out of Implications]. 
1165
1166 Now, once we are done with solving these flats and have to move inwards to 
1167 the nested implications (perhaps for a second time), we must consider all the
1168 extra variables (categories (ii) and (iii) above) as untouchables for the 
1169 implication. Otherwise we have the danger or double unifications, as well
1170 as the danger of not ``seing'' some unification. Example (from Trac #4494):
1171
1172    (F Int ~ uf)  /\  [untch=beta](forall a. C a => F Int ~ beta) 
1173
1174 In this example, beta is touchable inside the implication. The 
1175 first solveInteract step leaves 'uf' ununified. Then we move inside 
1176 the implication where a new constraint
1177        uf  ~  beta  
1178 emerges. We may spontaneously solve it to get uf := beta, so the whole
1179 implication disappears but when we pop out again we are left with (F
1180 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
1181 uf will get unified *once more* to (F Int).
1182
1183 The solution is to record the unification variables of the flats, 
1184 and make them untouchables for the nested implication. In the 
1185 example above uf would become untouchable, so beta would be forced 
1186 to be unified as beta := uf.
1187
1188 Note [Float Equalities out of Implications]
1189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1190 For ordinary pattern matches (including existentials) we float 
1191 equalities out of implications, for instance: 
1192      data T where 
1193        MkT :: Eq a => a -> T 
1194      f x y = case x of MkT _ -> (y::Int)
1195 We get the implication constraint (x::T) (y::alpha): 
1196      forall a. [untouchable=alpha] Eq a => alpha ~ Int
1197 We want to float out the equality into a scope where alpha is no
1198 longer untouchable, to solve the implication!  
1199
1200 But we cannot float equalities out of implications whose givens may
1201 yield or contain equalities:
1202
1203       data T a where 
1204         T1 :: T Int
1205         T2 :: T Bool
1206         T3 :: T a 
1207         
1208       h :: T a -> a -> Int
1209       
1210       f x y = case x of 
1211                 T1 -> y::Int
1212                 T2 -> y::Bool
1213                 T3 -> h x y
1214
1215 We generate constraint, for (x::T alpha) and (y :: beta): 
1216    [untouchables = beta] (alpha ~ Int => beta ~ Int)   -- From 1st branch
1217    [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1218    (alpha ~ beta)                                      -- From 3rd branch 
1219
1220 If we float the equality (beta ~ Int) outside of the first implication and 
1221 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1222 But if we just leave them inside the implications we unify alpha := beta and
1223 solve everything.
1224
1225 Principle: 
1226     We do not want to float equalities out which may need the given *evidence*
1227     to become soluble.
1228
1229 Consequence: classes with functional dependencies don't matter (since there is 
1230 no evidence for a fundep equality), but equality superclasses do matter (since 
1231 they carry evidence).
1232
1233 Notice that, due to Note [Extra TcSTv Untouchables], the free unification variables 
1234 of an equality that is floated out of an implication become effectively untouchables
1235 for the leftover implication. This is absolutely necessary. Consider the following 
1236 example. We start with two implications and a class with a functional dependency. 
1237
1238 class C x y | x -> y
1239 instance C [a] [a]
1240       
1241 (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
1242 (I2)      [untch=beta]forall b. 0 => F Int ~ [[alpha]] /\ C beta [b]
1243
1244 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2. 
1245 They may react to yield that (beta := [alpha]) which can then be pushed inwards 
1246 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1247 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1248 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1249
1250 class C x y | x -> y where 
1251  op :: x -> y -> ()
1252
1253 instance C [a] [a]
1254
1255 type family F a :: *
1256
1257 h :: F Int -> ()
1258 h = undefined
1259
1260 data TEx where 
1261   TEx :: a -> TEx 
1262
1263
1264 f (x::beta) = 
1265     let g1 :: forall b. b -> ()
1266         g1 _ = h [x]
1267         g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1268     in (g1 '3', g2 undefined)
1269
1270 Note [Shadowing of Implicit Parameters]
1271 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1272 Consider the following example:
1273
1274 f :: (?x :: Char) => Char
1275 f = let ?x = 'a' in ?x
1276
1277 The "let ?x = ..." generates an implication constraint of the form:
1278
1279 ?x :: Char => ?x :: Char
1280
1281
1282 Furthermore, the signature for `f` also generates an implication
1283 constraint, so we end up with the following nested implication:
1284
1285 ?x :: Char => (?x :: Char => ?x :: Char)
1286
1287 Note that the wanted (?x :: Char) constraint may be solved in
1288 two incompatible ways:  either by using the parameter from the
1289 signature, or by using the local definition.  Our intention is
1290 that the local definition should "shadow" the parameter of the
1291 signature, and we implement this as follows: when we nest implications,
1292 we remove any implicit parameters in the outer implication, that
1293 have the same name as givens of the inner implication.
1294
1295 Here is another variation of the example:
1296
1297 f :: (?x :: Int) => Char
1298 f = let ?x = 'x' in ?x
1299
1300 This program should also be accepted: the two constraints `?x :: Int`
1301 and `?x :: Char` never exist in the same context, so they don't get to
1302 interact to cause failure.
1303 \begin{code}
1304
1305 solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)
1306 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
1307 -- See Note [Solving Family Equations]
1308 -- Returns: a bunch of unsolved constraints from the original Cts and implications
1309 --          where the newly generated equalities (alpha := F xi) have been substituted through.
1310 solveCTyFunEqs cts
1311  = do { untch   <- getUntouchables 
1312       ; let (unsolved_can_cts, (ni_subst, cv_binds))
1313                 = getSolvableCTyFunEqs untch cts
1314       ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
1315                                           , ppr ni_subst, ppr cv_binds
1316                                           ])
1317       ; mapM_ solve_one cv_binds
1318
1319       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
1320   where
1321     solve_one (Wanted { ctev_evar = cv }, tv, ty) 
1322       = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
1323     solve_one (Derived {}, tv, ty)
1324       = setWantedTyBind tv ty
1325     solve_one arg
1326       = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
1327 ------------
1328 type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
1329   -- The TvSubstEnv is not idempotent, but is loop-free
1330   -- See Note [Non-idempotent substitution] in Unify
1331 emptyFunEqBinds :: FunEqBinds
1332 emptyFunEqBinds = (emptyVarEnv, [])
1333
1334 extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
1335 extendFunEqBinds (tv_subst, cv_binds) fl tv ty
1336   = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
1337
1338 ------------
1339 getSolvableCTyFunEqs :: TcsUntouchables
1340                      -> Cts                -- Precondition: all Wanteds or Derived!
1341                      -> (Cts, FunEqBinds)  -- Postcondition: returns the unsolvables
1342 getSolvableCTyFunEqs untch cts
1343   = Bag.foldlBag dflt_funeq (emptyCts, emptyFunEqBinds) cts
1344   where
1345     dflt_funeq :: (Cts, FunEqBinds) -> Ct
1346                -> (Cts, FunEqBinds)
1347     dflt_funeq (cts_in, feb@(tv_subst, _))
1348                (CFunEqCan { cc_ev = fl
1349                           , cc_fun = tc
1350                           , cc_tyargs = xis
1351                           , cc_rhs = xi })
1352       | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
1353
1354       , isTouchableMetaTyVar_InRange untch tv
1355            -- And it's a *touchable* unification variable
1356
1357       , typeKind xi `tcIsSubKind` tyVarKind tv
1358          -- Must do a small kind check since TcCanonical invariants 
1359          -- on family equations only impose compatibility, not subkinding
1360
1361       , not (tv `elemVarEnv` tv_subst)
1362            -- Check not in extra_binds
1363            -- See Note [Solving Family Equations], Point 1
1364
1365       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1366            -- Occurs check: see Note [Solving Family Equations], Point 2
1367       = ASSERT ( not (isGiven fl) )
1368         (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
1369
1370     dflt_funeq (cts_in, fun_eq_binds) ct
1371       = (cts_in `extendCts` ct, fun_eq_binds)
1372 \end{code}
1373
1374 Note [Solving Family Equations] 
1375 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1376 After we are done with simplification we may be left with constraints of the form:
1377      [Wanted] F xis ~ beta 
1378 If 'beta' is a touchable unification variable not already bound in the TyBinds 
1379 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1380
1381 When is it ok to do so? 
1382     1) 'beta' must not already be defaulted to something. Example: 
1383
1384            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
1385            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
1386                                        have to report this as unsolved.
1387
1388     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
1389        set [beta := F xis] only if beta is not among the free variables of xis.
1390
1391     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
1392        of type family equations. See Inert Set invariants in TcInteract. 
1393
1394
1395 *********************************************************************************
1396 *                                                                               * 
1397 *                          Defaulting and disamgiguation                        *
1398 *                                                                               *
1399 *********************************************************************************
1400 \begin{code}
1401 applyDefaultingRules :: Cts      -- All wanteds
1402                      -> TcS Cts  -- All wanteds again!
1403 -- Return some *extra* givens, which express the 
1404 -- type-class-default choice
1405 applyDefaultingRules wanteds
1406   | isEmptyBag wanteds 
1407   = return emptyBag
1408   | otherwise
1409   = do { traceTcS "applyDefaultingRules { " $ 
1410                   text "wanteds =" <+> ppr wanteds
1411                   
1412        ; info@(default_tys, _) <- getDefaultInfo
1413        ; let groups = findDefaultableGroups info wanteds
1414        ; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups
1415                                                  , text "info=" <+> ppr info ]
1416        ; deflt_cts <- mapM (disambigGroup default_tys) groups
1417
1418        ; traceTcS "applyDefaultingRules }" $ 
1419                   vcat [ text "Type defaults =" <+> ppr deflt_cts]
1420
1421        ; return (unionManyBags deflt_cts) }
1422 \end{code}
1423
1424 Note [tryTcS in defaulting]
1425 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1426
1427 defaultTyVar and disambigGroup create new evidence variables for
1428 default equations, and hence update the EvVar cache. However, after
1429 applyDefaultingRules we will try to solve these default equations
1430 using solveInteractCts, which will consult the cache and solve those
1431 EvVars from themselves! That's wrong.
1432
1433 To avoid this problem we guard defaulting under a @tryTcS@ which leaves
1434 the original cache unmodified.
1435
1436 There is a second reason for @tryTcS@ in defaulting: disambGroup does
1437 some constraint solving to determine if a default equation is
1438 ``useful'' in solving some wanted constraints, but we want to
1439 discharge all evidence and unifications that may have happened during
1440 this constraint solving.
1441
1442 Finally, @tryTcS@ importantly does not inherit the original cache from
1443 the higher level but makes up a new cache, the reason is that disambigGroup
1444 will call solveInteractCts so the new derived and the wanteds must not be 
1445 in the cache!
1446
1447
1448 \begin{code}
1449 ------------------
1450 touchablesOfWC :: WantedConstraints -> TcTyVarSet
1451 -- See Note [Extra Tcs Untouchables] to see why we carry a TcsUntouchables 
1452 -- instead of just using the Untouchable range have in our hands.
1453 touchablesOfWC = go (NoUntouchables, emptyVarSet)
1454   where go :: TcsUntouchables -> WantedConstraints -> TcTyVarSet
1455         go untch (WC { wc_flat = flats, wc_impl = impls }) 
1456           = filterVarSet is_touchable flat_tvs `unionVarSet`
1457               foldrBag (unionVarSet . (go_impl $ untch_for_impls untch)) emptyVarSet impls 
1458           where is_touchable = isTouchableMetaTyVar_InRange untch
1459                 flat_tvs = tyVarsOfCts flats
1460                 untch_for_impls (r,uset) = (r, uset `unionVarSet` flat_tvs)
1461         go_impl (_rng,set) implic = go (ic_untch implic,set) (ic_wanted implic)
1462
1463 applyTyVarDefaulting :: WantedConstraints -> TcM Cts
1464 applyTyVarDefaulting wc = runTcS do_dflt >>= (return . fst)
1465   where do_dflt = do { tv_cts <- mapM defaultTyVar $ 
1466                                  varSetElems (touchablesOfWC wc)
1467                      ; return (unionManyBags tv_cts) }
1468
1469 defaultTyVar :: TcTyVar -> TcS Cts
1470 -- Precondition: a touchable meta-variable
1471 defaultTyVar the_tv
1472   | not (k `eqKind` default_k)
1473   -- Why tryTcS? See Note [tryTcS in defaulting]
1474   = tryTcS $
1475     do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1476        ; ty_k <- instFlexiTcSHelperTcS (tyVarName the_tv) default_k
1477        ; md <- newDerived loc (mkTcEqPred (mkTyVarTy the_tv) ty_k)
1478              -- Why not directly newDerived loc (mkTcEqPred k default_k)? 
1479              -- See Note [DefaultTyVar]
1480        ; let cts
1481               | Just der_ev <- md = [mkNonCanonical der_ev]
1482               | otherwise = []
1483        
1484        ; implics_from_defaulting <- solveInteractCts cts
1485        ; MASSERT (isEmptyBag implics_from_defaulting)
1486          
1487        ; (_,unsolved) <- extractUnsolvedTcS
1488        ; if isEmptyBag (keepWanted unsolved) then return (listToBag cts)
1489          else return emptyBag }
1490   | otherwise = return emptyBag  -- The common case
1491   where
1492     k = tyVarKind the_tv
1493     default_k = defaultKind k
1494 \end{code}
1495
1496 Note [DefaultTyVar]
1497 ~~~~~~~~~~~~~~~~~~~
1498 defaultTyVar is used on any un-instantiated meta type variables to
1499 default the kind of OpenKind and ArgKind etc to *.  This is important 
1500 to ensure that instance declarations match.  For example consider
1501
1502      instance Show (a->b)
1503      foo x = show (\_ -> True)
1504
1505 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
1506 and that won't match the typeKind (*) in the instance decl.  See tests
1507 tc217 and tc175.
1508
1509 We look only at touchable type variables. No further constraints
1510 are going to affect these type variables, so it's time to do it by
1511 hand.  However we aren't ready to default them fully to () or
1512 whatever, because the type-class defaulting rules have yet to run.
1513
1514 An important point is that if the type variable tv has kind k and the
1515 default is default_k we do not simply generate [D] (k ~ default_k) because:
1516
1517    (1) k may be ArgKind and default_k may be * so we will fail
1518
1519    (2) We need to rewrite all occurrences of the tv to be a type
1520        variable with the right kind and we choose to do this by rewriting 
1521        the type variable /itself/ by a new variable which does have the 
1522        right kind.
1523
1524 \begin{code}
1525
1526
1527 ----------------
1528 findDefaultableGroups 
1529     :: ( [Type]
1530        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1531     -> Cts      -- Unsolved
1532     -> [[(Ct,TcTyVar)]]
1533 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1534   | null default_tys             = []
1535   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1536   where 
1537     unaries     :: [(Ct, TcTyVar)]  -- (C tv) constraints
1538     non_unaries :: [Ct]             -- and *other* constraints
1539     
1540     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1541         -- Finds unary type-class constraints
1542     find_unary cc@(CDictCan { cc_tyargs = [ty] })
1543         | Just tv <- tcGetTyVar_maybe ty
1544         = Left (cc, tv)
1545     find_unary cc = Right cc  -- Non unary or non dictionary 
1546
1547     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
1548     bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries 
1549
1550     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1551
1552     is_defaultable_group ds@((_,tv):_)
1553         = let b1 = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
1554               b2 = not (tv `elemVarSet` bad_tvs)
1555               b4 = defaultable_classes [cc_class cc | (cc,_) <- ds]
1556           in (b1 && b2 && b4)
1557     is_defaultable_group [] = panic "defaultable_group"
1558
1559     defaultable_classes clss 
1560         | extended_defaults = any isInteractiveClass clss
1561         | otherwise         = all is_std_class clss && (any is_num_class clss)
1562
1563     -- In interactive mode, or with -XExtendedDefaultRules,
1564     -- we default Show a to Show () to avoid graututious errors on "show []"
1565     isInteractiveClass cls 
1566         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1567
1568     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1569     -- is_num_class adds IsString to the standard numeric classes, 
1570     -- when -foverloaded-strings is enabled
1571
1572     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1573     -- Similarly is_std_class
1574
1575 ------------------------------
1576 disambigGroup :: [Type]           -- The default types 
1577               -> [(Ct, TcTyVar)]  -- All classes of the form (C a)
1578                                   --  sharing same type variable
1579               -> TcS Cts
1580
1581 disambigGroup []  _grp
1582   = return emptyBag
1583 disambigGroup (default_ty:default_tys) group
1584   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1585        ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
1586                     do { derived_eq <- tryTcS $ 
1587                        -- I need a new tryTcS because we will call solveInteractCts below!
1588                             do { md <- newDerived (ctev_wloc the_fl) 
1589                                                   (mkTcEqPred (mkTyVarTy the_tv) default_ty)
1590                                                   -- ctev_wloc because constraint is not Given!
1591                                ; case md of 
1592                                     Nothing   -> return []
1593                                     Just ctev -> return [ mkNonCanonical ctev ] }
1594                             
1595                        ; traceTcS "disambigGroup (solving) {" $
1596                          text "trying to solve constraints along with default equations ..."
1597                        ; implics_from_defaulting <- 
1598                                     solveInteractCts (derived_eq ++ wanteds)
1599                        ; MASSERT (isEmptyBag implics_from_defaulting)
1600                            -- I am not certain if any implications can be generated
1601                            -- but I am letting this fail aggressively if this ever happens.
1602                                      
1603                        ; (_,unsolved) <- extractUnsolvedTcS 
1604                        ; traceTcS "disambigGroup (solving) }" $
1605                          text "disambigGroup unsolved =" <+> ppr (keepWanted unsolved)
1606                        ; if isEmptyBag (keepWanted unsolved) then -- Don't care about Derived's
1607                              return (Just $ listToBag derived_eq) 
1608                          else 
1609                              return Nothing 
1610                        }
1611        ; case success of
1612            Just cts -> -- Success: record the type variable binding, and return
1613                     do { wrapWarnTcS $ warnDefaulting wanteds default_ty
1614                        ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1615                        ; return cts }
1616            Nothing -> -- Failure: try with the next type
1617                     do { traceTcS "disambigGroup failed, will try other default types"
1618                                   (ppr default_ty)
1619                        ; disambigGroup default_tys group } }
1620   where
1621     ((the_ct,the_tv):_) = group
1622     the_fl              = cc_ev the_ct
1623     wanteds             = map fst group
1624 \end{code}
1625
1626 Note [Avoiding spurious errors]
1627 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1628 When doing the unification for defaulting, we check for skolem
1629 type variables, and simply don't default them.  For example:
1630    f = (*)      -- Monomorphic
1631    g :: Num a => a -> a
1632    g x = f x x
1633 Here, we get a complaint when checking the type signature for g,
1634 that g isn't polymorphic enough; but then we get another one when
1635 dealing with the (Num a) context arising from f's definition;
1636 we try to unify a with Int (to default it), but find that it's
1637 already been unified with the rigid variable from g's type sig
1638
1639
1640
1641 *********************************************************************************
1642 *                                                                               * 
1643 *                   Utility functions
1644 *                                                                               *
1645 *********************************************************************************
1646
1647 \begin{code}
1648 newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
1649 newFlatWanteds orig theta
1650   = do { loc <- getCtLoc orig
1651        ; mapM (inst_to_wanted loc) theta }
1652   where 
1653     inst_to_wanted loc pty 
1654           = do { v <- TcMType.newWantedEvVar pty 
1655                ; return $ 
1656                  CNonCanonical { cc_ev = Wanted { ctev_evar = v
1657                                                 , ctev_wloc = loc
1658                                                 , ctev_pred = pty }
1659                                , cc_depth = 0 } }
1660 \end{code}