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