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