afd9093c527ee4f91de39166fa41e7963b9887c4
[ghc.git] / compiler / typecheck / TcCanonical.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 TcCanonical(
10     canonicalize,
11     canOccursCheck, canEq, canEvVar,
12     rewriteWithFunDeps,
13     emitFDWorkAsWanted, emitFDWorkAsDerived,
14     StopOrContinue (..)
15  ) where
16
17 #include "HsVersions.h"
18
19 import BasicTypes ( IPName )
20 import TcErrors
21 import TcRnTypes
22 import FunDeps
23 import qualified TcMType as TcM
24 import TcType
25 import Type
26 import Kind
27 import TcEvidence
28 import Class
29 import TyCon
30 import TypeRep
31 import Name ( Name )
32 import Var
33 import VarEnv
34 import Outputable
35 import Control.Monad    ( when, unless, zipWithM, foldM )
36 import MonadUtils
37 import Control.Applicative ( (<|>) )
38
39 import TrieMap
40 import VarSet
41 import TcSMonad
42 import FastString
43
44 import Data.Maybe ( isNothing )
45 import Pair ( pSnd )
46
47 \end{code}
48
49
50 %************************************************************************
51 %*                                                                      *
52 %*                      The Canonicaliser                               *
53 %*                                                                      *
54 %************************************************************************
55
56 Note [Canonicalization]
57 ~~~~~~~~~~~~~~~~~~~~~~~
58
59 Canonicalization converts a flat constraint to a canonical form. It is
60 unary (i.e. treats individual constraints one at a time), does not do
61 any zonking, but lives in TcS monad because it needs to create fresh
62 variables (for flattening) and consult the inerts (for efficiency).
63
64 The execution plan for canonicalization is the following:
65  
66   1) Decomposition of equalities happens as necessary until we reach a 
67      variable or type family in one side. There is no decomposition step
68      for other forms of constraints. 
69
70   2) If, when we decompose, we discover a variable on the head then we 
71      look at inert_eqs from the current inert for a substitution for this 
72      variable and contine decomposing. Hence we lazily apply the inert 
73      substitution if it is needed. 
74
75   3) If no more decomposition is possible, we deeply apply the substitution
76      from the inert_eqs and continue with flattening.
77
78   4) During flattening, we examine whether we have already flattened some 
79      function application by looking at all the CTyFunEqs with the same 
80      function in the inert set. The reason for deeply applying the inert 
81      substitution at step (3) is to maximise our chances of matching an 
82      already flattened family application in the inert. 
83
84 The net result is that a constraint coming out of the canonicalization 
85 phase cannot be rewritten any further from the inerts (but maybe /it/ can 
86 rewrite an inert or still interact with an inert in a further phase in the
87 simplifier.
88
89 \begin{code}
90
91 -- Informative results of canonicalization
92 data StopOrContinue 
93   = ContinueWith Ct   -- Either no canonicalization happened, or if some did 
94                       -- happen, it is still safe to just keep going with this 
95                       -- work item. 
96   | Stop              -- Some canonicalization happened, extra work is now in 
97                       -- the TcS WorkList. 
98
99 instance Outputable StopOrContinue where
100   ppr Stop             = ptext (sLit "Stop")
101   ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
102
103
104 continueWith :: Ct -> TcS StopOrContinue
105 continueWith = return . ContinueWith
106
107 andWhenContinue :: TcS StopOrContinue 
108                 -> (Ct -> TcS StopOrContinue) 
109                 -> TcS StopOrContinue
110 andWhenContinue tcs1 tcs2
111   = do { r <- tcs1
112        ; case r of
113            Stop            -> return Stop
114            ContinueWith ct -> tcs2 ct }
115
116 \end{code}
117
118 Note [Caching for canonicals]
119 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
120 Our plan with pre-canonicalization is to be able to solve a constraint really fast from existing
121 bindings in TcEvBinds. So one may think that the condition (isCNonCanonical) is not necessary. 
122 However consider the following setup:
123
124 InertSet = { [W] d1 : Num t } 
125 WorkList = { [W] d2 : Num t, [W] c : t ~ Int} 
126
127 Now, we prioritize equalities, but in our concrete example (should_run/mc17.hs) the first (d2) constraint 
128 is dealt with first, because (t ~ Int) is an equality that only later appears in the worklist since it is
129 pulled out from a nested implication constraint. So, let's examine what happens:
130  
131    - We encounter work item (d2 : Num t)
132
133    - Nothing is yet in EvBinds, so we reach the interaction with inerts 
134      and set:
135               d2 := d1 
136     and we discard d2 from the worklist. The inert set remains unaffected.
137
138    - Now the equation ([W] c : t ~ Int) is encountered and kicks-out (d1 : Num t) from the inerts.
139      Then that equation gets spontaneously solved, perhaps. We end up with:
140         InertSet : { [G] c : t ~ Int }
141         WorkList : { [W] d1 : Num t} 
142
143    - Now we examine (d1), we observe that there is a binding for (Num t) in the evidence binds and 
144      we set: 
145              d1 := d2 
146      and end up in a loop!
147
148 Now, the constraints that get kicked out from the inert set are always Canonical, so by restricting
149 the use of the pre-canonicalizer to NonCanonical constraints we eliminate this danger. Moreover, for 
150 canonical constraints we already have good caching mechanisms (effectively the interaction solver) 
151 and we are interested in reducing things like superclasses of the same non-canonical constraint being 
152 generated hence I don't expect us to lose a lot by introducing the (isCNonCanonical) restriction.
153
154 A similar situation can arise in TcSimplify, at the end of the solve_wanteds function, where constraints
155 from the inert set are returned as new work -- our substCt ensures however that if they are not rewritten
156 by subst, they remain canonical and hence we will not attempt to solve them from the EvBinds. If on the 
157 other hand they did get rewritten and are now non-canonical they will still not match the EvBinds, so we 
158 are again good.
159
160
161
162 \begin{code}
163
164 -- Top-level canonicalization
165 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
166
167 canonicalize :: Ct -> TcS StopOrContinue
168 canonicalize ct@(CNonCanonical { cc_id = ev, cc_flavor = fl, cc_depth  = d })
169   = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
170        ; {-# SCC "canEvVar" #-}
171          canEvVar ev (classifyPredType (evVarPred ev)) d fl }
172
173 canonicalize (CDictCan { cc_id = ev, cc_depth = d
174                        , cc_flavor = fl
175                        , cc_class  = cls
176                        , cc_tyargs = xis })
177   = {-# SCC "canClass" #-}
178     canClass d fl ev cls xis -- Do not add any superclasses
179 canonicalize (CTyEqCan { cc_id = ev, cc_depth = d
180                        , cc_flavor = fl
181                        , cc_tyvar  = tv
182                        , cc_rhs    = xi })
183   = {-# SCC "canEqLeafTyVarLeftRec" #-}
184     canEqLeafTyVarLeftRec d fl ev tv xi
185
186 canonicalize (CFunEqCan { cc_id = ev, cc_depth = d
187                         , cc_flavor = fl
188                         , cc_fun    = fn
189                         , cc_tyargs = xis1
190                         , cc_rhs    = xi2 })
191   = {-# SCC "canEqLeafFunEqLeftRec" #-}
192     canEqLeafFunEqLeftRec d fl ev (fn,xis1) xi2
193
194 canonicalize (CIPCan { cc_id = ev, cc_depth = d
195                      , cc_flavor = fl
196                      , cc_ip_nm  = nm
197                      , cc_ip_ty  = xi })
198   = canIP d fl ev nm xi
199 canonicalize (CIrredEvCan { cc_id = ev, cc_flavor = fl
200                           , cc_depth = d
201                           , cc_ty = xi })
202   = canIrred d fl ev xi
203
204
205 canEvVar :: EvVar -> PredTree 
206          -> SubGoalDepth -> CtFlavor -> TcS StopOrContinue
207 canEvVar ev pred_classifier d fl 
208   = case pred_classifier of
209       ClassPred cls tys -> canClass d fl ev cls tys 
210                                         `andWhenContinue` emit_superclasses
211       EqPred ty1 ty2    -> canEq    d fl ev ty1 ty2
212       IPPred nm ty      -> canIP    d fl ev nm ty
213       IrredPred ev_ty   -> canIrred d fl ev ev_ty
214       TuplePred tys     -> canTuple d fl ev tys
215   where emit_superclasses ct@(CDictCan {cc_id = v_new
216                                        , cc_tyargs = xis_new, cc_class = cls })
217             -- Add superclasses of this one here, See Note [Adding superclasses]. 
218             -- But only if we are not simplifying the LHS of a rule. 
219           = do { sctxt <- getTcSContext
220                ; unless (simplEqsOnly sctxt) $ 
221                         newSCWorkFromFlavored d v_new fl cls xis_new
222                ; continueWith ct }
223         emit_superclasses _ = panic "emit_superclasses of non-class!"
224
225
226 -- Tuple canonicalisation
227 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
228 canTuple :: SubGoalDepth -- Depth 
229          -> CtFlavor -> EvVar -> [PredType] -> TcS StopOrContinue
230 canTuple d fl ev tys
231   = do { traceTcS "can_pred" (text "TuplePred!") 
232        ; evs <- zipWithM can_pred_tup_one tys [0..]
233        ; if (isWanted fl) then 
234              do {_unused_fl <- setEvBind ev (EvTupleMk evs) fl
235                 ; return Stop }
236          else return Stop }
237   where 
238      can_pred_tup_one ty n
239           = do { evc <- newEvVar fl ty
240                ; let ev' = evc_the_evvar evc
241                ; fl' <- if isGivenOrSolved fl then 
242                             setEvBind ev' (EvTupleSel ev n) fl
243                         else return fl
244                ; when (isNewEvVar evc) $
245                       addToWork (canEvVar ev' (classifyPredType (evVarPred ev')) d fl')
246                ; return ev' }
247
248 -- Implicit Parameter Canonicalization
249 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
250 canIP :: SubGoalDepth -- Depth 
251       -> CtFlavor -> EvVar 
252       -> IPName Name -> Type -> TcS StopOrContinue
253 -- Precondition: EvVar is implicit parameter evidence
254 canIP d fl v nm ty
255   =    -- Note [Canonical implicit parameter constraints] explains why it's 
256        -- possible in principle to not flatten, but since flattening applies 
257        -- the inert substitution we choose to flatten anyway.
258     do { (xi,co) <- flatten d fl (mkIPPred nm ty)
259        ; let no_flattening = isTcReflCo co 
260        ; if no_flattening then
261             let IPPred _ xi_in = classifyPredType xi 
262             in continueWith $ CIPCan { cc_id = v, cc_flavor = fl
263                                      , cc_ip_nm = nm, cc_ip_ty = xi_in
264                                      , cc_depth = d }
265          else do { evc <- newEvVar fl xi
266                  ; let v_new          = evc_the_evvar evc
267                        IPPred _ ip_xi = classifyPredType xi
268                  ; fl_new <- case fl of 
269                                Wanted {}  -> setEvBind v (EvCast v_new co) fl 
270                                Given {}   -> setEvBind v_new (EvCast v (mkTcSymCo co)) fl
271                                Derived {} -> return fl
272                  ; if isNewEvVar evc then
273                        continueWith $ CIPCan { cc_id     = v_new
274                                              , cc_flavor = fl_new, cc_ip_nm = nm
275                                              , cc_ip_ty  = ip_xi
276                                              , cc_depth  = d }
277                    else return Stop } }
278 \end{code}
279
280 Note [Canonical implicit parameter constraints]
281 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
282 The type in a canonical implicit parameter constraint doesn't need to
283 be a xi (type-function-free type) since we can defer the flattening
284 until checking this type for equality with another type.  If we
285 encounter two IP constraints with the same name, they MUST have the
286 same type, and at that point we can generate a flattened equality
287 constraint between the types.  (On the other hand, the types in two
288 class constraints for the same class MAY be equal, so they need to be
289 flattened in the first place to facilitate comparing them.)
290 \begin{code}
291
292 -- Class Canonicalization
293 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
294
295 canClass :: SubGoalDepth -- Depth
296          -> CtFlavor -> EvVar  
297          -> Class -> [Type] -> TcS StopOrContinue
298 -- Precondition: EvVar is class evidence 
299 -- Note: Does NOT add superclasses, but the /caller/ is responsible for adding them!
300 canClass d fl v cls tys
301   = do { -- sctx <- getTcSContext
302        ; (xis, cos) <- flattenMany d fl tys
303        ; let co = mkTcTyConAppCo (classTyCon cls) cos 
304              xi = mkClassPred cls xis
305
306        ; let no_flattening = all isTcReflCo cos
307                   -- No flattening, continue with canonical
308        ; if no_flattening then 
309              continueWith $ CDictCan { cc_id = v, cc_flavor = fl
310                                      , cc_tyargs = xis, cc_class = cls
311                                      , cc_depth = d }
312                    -- Flattening happened
313          else do { evc <- newEvVar fl xi
314                  ; let v_new = evc_the_evvar evc
315                  ; fl_new <- case fl of
316                      Wanted  {} -> setEvBind v (EvCast v_new co) fl
317                      Given   {} -> setEvBind v_new (EvCast v (mkTcSymCo co)) fl
318                      Derived {} -> return fl
319                     -- Continue only if flat constraint is new
320                  ; if isNewEvVar evc then
321                         continueWith $ CDictCan { cc_id = v_new, cc_flavor = fl_new
322                                                 , cc_tyargs = xis, cc_class = cls
323                                                 , cc_depth  = d }
324                    else return Stop } }
325 \end{code}
326
327 Note [Adding superclasses]
328 ~~~~~~~~~~~~~~~~~~~~~~~~~~ 
329 Since dictionaries are canonicalized only once in their lifetime, the
330 place to add their superclasses is canonicalisation (The alternative
331 would be to do it during constraint solving, but we'd have to be
332 extremely careful to not repeatedly introduced the same superclass in
333 our worklist). Here is what we do:
334
335 For Givens: 
336        We add all their superclasses as Givens. 
337
338 For Wanteds: 
339        Generally speaking we want to be able to add superclasses of 
340        wanteds for two reasons:
341
342        (1) Oportunities for improvement. Example: 
343                   class (a ~ b) => C a b 
344            Wanted constraint is: C alpha beta 
345            We'd like to simply have C alpha alpha. Similar 
346            situations arise in relation to functional dependencies. 
347            
348        (2) To have minimal constraints to quantify over: 
349            For instance, if our wanted constraint is (Eq a, Ord a) 
350            we'd only like to quantify over Ord a. 
351
352        To deal with (1) above we only add the superclasses of wanteds
353        which may lead to improvement, that is: equality superclasses or 
354        superclasses with functional dependencies. 
355
356        We deal with (2) completely independently in TcSimplify. See 
357        Note [Minimize by SuperClasses] in TcSimplify. 
358
359
360        Moreover, in all cases the extra improvement constraints are 
361        Derived. Derived constraints have an identity (for now), but 
362        we don't do anything with their evidence. For instance they 
363        are never used to rewrite other constraints. 
364
365        See also [New Wanted Superclass Work] in TcInteract. 
366
367
368 For Deriveds: 
369        We do nothing.
370
371 Here's an example that demonstrates why we chose to NOT add
372 superclasses during simplification: [Comes from ticket #4497]
373  
374    class Num (RealOf t) => Normed t
375    type family RealOf x
376
377 Assume the generated wanted constraint is: 
378    RealOf e ~ e, Normed e 
379 If we were to be adding the superclasses during simplification we'd get: 
380    Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf 
381 ==> 
382    e ~ uf, Num uf, Normed e, RealOf e ~ e 
383 ==> [Spontaneous solve] 
384    Num uf, Normed uf, RealOf uf ~ uf 
385
386 While looks exactly like our original constraint. If we add the superclass again we'd loop. 
387 By adding superclasses definitely only once, during canonicalisation, this situation can't 
388 happen.
389
390 \begin{code}
391
392 newSCWorkFromFlavored :: SubGoalDepth -- Depth
393                       -> EvVar -> CtFlavor -> Class -> [Xi] -> TcS ()
394 -- Returns superclasses, see Note [Adding superclasses]
395 newSCWorkFromFlavored d ev flavor cls xis 
396   | isDerived flavor 
397   = return ()  -- Deriveds don't yield more superclasses because we will
398                -- add them transitively in the case of wanteds. 
399
400   | Just gk <- isGiven_maybe flavor 
401   = case gk of 
402       GivenOrig -> do { let sc_theta = immSuperClasses cls xis 
403                       ; sc_vars <- mapM (newEvVar flavor) sc_theta
404                       ; sc_cts <- zipWithM (\scv ev_trm -> 
405                                                 do { let sc_evvar = evc_the_evvar scv
406                                                    ; _unused_fl <- setEvBind sc_evvar ev_trm flavor
407                                                       -- unused because it's the same
408                                                    ; return $ 
409                                                      CNonCanonical { cc_id = sc_evvar
410                                                                    , cc_flavor = flavor
411                                                                    , cc_depth = d }}) 
412                                            sc_vars [EvSuperClass ev n | n <- [0..]]
413                         -- Emit now, canonicalize later in a lazier fashion
414                       ; traceTcS "newSCWorkFromFlavored" $
415                                  text "Emitting superclass work:" <+> ppr sc_cts
416                       ; updWorkListTcS $ appendWorkListCt sc_cts }
417       GivenSolved {} -> return ()
418       -- Seems very dangerous to add the superclasses for dictionaries that may be 
419       -- partially solved because we may end up with evidence loops.
420
421   | isEmptyVarSet (tyVarsOfTypes xis)
422   = return () -- Wanteds with no variables yield no deriveds.
423               -- See Note [Improvement from Ground Wanteds]
424
425   | otherwise -- Wanted case, just add those SC that can lead to improvement. 
426   = do { let sc_rec_theta = transSuperClasses cls xis 
427              impr_theta   = filter is_improvement_pty sc_rec_theta 
428              Wanted wloc  = flavor
429        ; sc_cts <- mapM (\pty -> do { scv <- newEvVar (Derived wloc) pty
430                                     ; if isNewEvVar scv then 
431                                           return [ CNonCanonical { cc_id = evc_the_evvar scv
432                                                                  , cc_flavor = Derived wloc
433                                                                  , cc_depth = d } ]  
434                                       else return [] }
435                         ) impr_theta
436        ; let sc_cts_flat = concat sc_cts
437        ; traceTcS "newSCWorkFromFlavored" (text "Emitting superclass work:" <+> ppr sc_cts_flat)
438        ; updWorkListTcS $ appendWorkListCt sc_cts_flat }
439
440 is_improvement_pty :: PredType -> Bool 
441 -- Either it's an equality, or has some functional dependency
442 is_improvement_pty ty = go (classifyPredType ty)
443   where
444     go (EqPred {})         = True 
445     go (ClassPred cls _tys) = not $ null fundeps
446       where (_,fundeps) = classTvsFds cls
447     go (IPPred {})         = False
448     go (TuplePred ts)      = any is_improvement_pty ts
449     go (IrredPred {})      = True -- Might have equalities after reduction?
450 \end{code}
451
452
453
454 \begin{code}
455 -- Irreducibles canonicalization
456 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
457 canIrred :: SubGoalDepth -- Depth
458          -> CtFlavor -> EvVar -> TcType -> TcS StopOrContinue
459 -- Precondition: ty not a tuple and no other evidence form
460 canIrred d fl v ty 
461   = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty) 
462        ; (xi,co) <- flatten d fl ty -- co :: xi ~ ty
463        ; let no_flattening = xi `eqType` ty 
464                              -- In this particular case it is not safe to 
465                              -- say 'isTcReflCo' because the new constraint may
466                              -- be reducible!
467        ; if no_flattening then
468             continueWith $ CIrredEvCan { cc_id = v, cc_flavor = fl
469                                        , cc_ty = xi, cc_depth  = d }
470          else do
471       {   -- Flattening consults and applies family equations from the
472           -- inerts, so 'xi' may become reducible. So just recursively
473           -- canonicalise the resulting evidence variable
474         evc <- newEvVar fl xi
475       ; let v' = evc_the_evvar evc
476       ; fl' <- case fl of 
477           Wanted  {} -> setEvBind v (EvCast v' co) fl
478           Given   {} -> setEvBind v' (EvCast v (mkTcSymCo co)) fl
479           Derived {} -> return fl
480       
481       ; if isNewEvVar evc then 
482             canEvVar v' (classifyPredType (evVarPred v')) d fl'
483         else
484             return Stop }
485       }
486
487 \end{code}
488
489 %************************************************************************
490 %*                                                                      *
491 %*        Flattening (eliminating all function symbols)                 *
492 %*                                                                      *
493 %************************************************************************
494
495 Note [Flattening]
496 ~~~~~~~~~~~~~~~~~~~~
497   flatten ty  ==>   (xi, cc)
498     where
499       xi has no type functions
500       cc = Auxiliary given (equality) constraints constraining
501            the fresh type variables in xi.  Evidence for these 
502            is always the identity coercion, because internally the
503            fresh flattening skolem variables are actually identified
504            with the types they have been generated to stand in for.
505
506 Note that it is flatten's job to flatten *every type function it sees*.
507 flatten is only called on *arguments* to type functions, by canEqGiven.
508
509 Recall that in comments we use alpha[flat = ty] to represent a
510 flattening skolem variable alpha which has been generated to stand in
511 for ty.
512
513 ----- Example of flattening a constraint: ------
514   flatten (List (F (G Int)))  ==>  (xi, cc)
515     where
516       xi  = List alpha
517       cc  = { G Int ~ beta[flat = G Int],
518               F beta ~ alpha[flat = F beta] }
519 Here
520   * alpha and beta are 'flattening skolem variables'.
521   * All the constraints in cc are 'given', and all their coercion terms 
522     are the identity.
523
524 NB: Flattening Skolems only occur in canonical constraints, which
525 are never zonked, so we don't need to worry about zonking doing
526 accidental unflattening.
527
528 Note that we prefer to leave type synonyms unexpanded when possible,
529 so when the flattener encounters one, it first asks whether its
530 transitive expansion contains any type function applications.  If so,
531 it expands the synonym and proceeds; if not, it simply returns the
532 unexpanded synonym.
533
534 \begin{code}
535
536 -- Flatten a bunch of types all at once.
537 flattenMany :: SubGoalDepth -- Depth
538             -> CtFlavor -> [Type] -> TcS ([Xi], [TcCoercion])
539 -- Coercions :: Xi ~ Type 
540 -- Returns True iff (no flattening happened)
541 flattenMany d ctxt tys 
542   = -- pprTrace "flattenMany" empty $
543     go tys 
544   where go []       = return ([],[])
545         go (ty:tys) = do { (xi,co)    <- flatten d ctxt ty
546                          ; (xis,cos)  <- go tys
547                          ; return (xi:xis,co:cos) }
548
549 -- Flatten a type to get rid of type function applications, returning
550 -- the new type-function-free type, and a collection of new equality
551 -- constraints.  See Note [Flattening] for more detail.
552 flatten :: SubGoalDepth -- Depth
553         -> CtFlavor -> TcType -> TcS (Xi, TcCoercion)
554 -- Postcondition: Coercion :: Xi ~ TcType
555 flatten d ctxt ty 
556   | Just ty' <- tcView ty
557   = do { (xi, co) <- flatten d ctxt ty'
558        ; return (xi,co) }
559         
560        -- DV: The following is tedious to do but maybe we should return to this
561        -- Preserve type synonyms if possible
562        -- ; if no_flattening
563        --   then return (xi, mkTcReflCo xi,no_flattening) -- Importantly, not xi!
564        --   else return (xi,co,no_flattening) 
565        -- }
566
567 flatten d ctxt v@(TyVarTy _)
568   = do { ieqs <- getInertEqs
569        ; let co = liftInertEqsTy ieqs ctxt v           -- co : v ~ ty
570              ty = pSnd (tcCoercionKind co)
571        ; if v `eqType` ty then
572              return (ty,mkTcReflCo ty)
573          else -- NB recursive call. Why? See Note [Non-idempotent inert substitution]
574               -- Actually I believe that applying the substition only *twice* will suffice
575          
576              do { (ty_final,co') <- flatten d ctxt ty  -- co' : ty_final ~ ty
577                 ; return (ty_final,co' `mkTcTransCo` mkTcSymCo co) } }
578
579 \end{code}
580
581 Note [Non-idempotent inert substitution]
582 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
583
584 The inert substitution is not idempotent in the broad sense. It is only idempotent in 
585 that it cannot rewrite the RHS of other inert equalities any further. An example of such 
586 an inert substitution is:
587
588  [Ś] g1 : ta8 ~ ta4
589  [W] g2 : ta4 ~ a5Fj
590
591 Observe that the wanted cannot rewrite the solved goal, despite the fact that ta4 appears on
592 an RHS of an equality. Now, imagine a constraint:
593
594  [W] g3: ta8 ~ Int 
595
596 coming in. If we simply apply once the inert substitution we will get: 
597
598  [W] g3_1: ta4 ~ Int 
599
600 and because potentially ta4 is untouchable we will try to insert g3_1 in the inert set, 
601 getting a panic since the inert only allows ONE equation per LHS type variable (as it 
602 should).
603
604 For this reason, when we reach to flatten a type variable, we flatten it recursively, 
605 so that we can make sure that the inert substitution /is/ fully applied.
606
607 This insufficient rewriting was the reason for #5668.
608
609 \begin{code}
610
611
612 flatten d ctxt (AppTy ty1 ty2)
613   = do { (xi1,co1) <- flatten d ctxt ty1
614        ; (xi2,co2) <- flatten d ctxt ty2
615        ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
616
617 flatten d ctxt (FunTy ty1 ty2)
618   = do { (xi1,co1) <- flatten d ctxt ty1
619        ; (xi2,co2) <- flatten d ctxt ty2
620        ; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
621
622 flatten d fl (TyConApp tc tys)
623   -- For a normal type constructor or data family application, we just
624   -- recursively flatten the arguments.
625   | not (isSynFamilyTyCon tc)
626     = do { (xis,cos) <- flattenMany d fl tys
627          ; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
628
629   -- Otherwise, it's a type function application, and we have to
630   -- flatten it away as well, and generate a new given equality constraint
631   -- between the application and a newly generated flattening skolem variable.
632   | otherwise
633   = ASSERT( tyConArity tc <= length tys )       -- Type functions are saturated
634       do { (xis, cos) <- flattenMany d fl tys
635          ; let (xi_args, xi_rest)  = splitAt (tyConArity tc) xis
636                  -- The type function might be *over* saturated
637                  -- in which case the remaining arguments should
638                  -- be dealt with by AppTys
639                fam_ty = mkTyConApp tc xi_args
640          ; (ret_co, rhs_xi, ct) <-
641              do { is_cached <- getCachedFlatEq tc xi_args fl Any
642                 ; case is_cached of
643                     Just (rhs_xi,ret_eq) -> 
644                         do { traceTcS "is_cached!" $ ppr ret_eq
645                            ; return (ret_eq, rhs_xi, []) }
646                     Nothing
647                         | isGivenOrSolved fl ->
648                             do { rhs_xi_var <- newFlattenSkolemTy fam_ty
649                                ; (fl',eqv) 
650                                    <- newGivenEqVar fl fam_ty rhs_xi_var (mkTcReflCo fam_ty)
651                                ; let ct  = CFunEqCan { cc_id     = eqv
652                                                      , cc_flavor = fl' -- Given
653                                                      , cc_fun    = tc 
654                                                      , cc_tyargs = xi_args 
655                                                      , cc_rhs    = rhs_xi_var 
656                                                      , cc_depth  = d }
657                                            -- Update the flat cache: just an optimisation!
658                                ; updateFlatCache eqv fl' tc xi_args rhs_xi_var WhileFlattening
659                                ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
660                         | otherwise ->
661                     -- Derived or Wanted: make a new /unification/ flatten variable
662                             do { rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
663                                ; let wanted_flavor = mkWantedFlavor fl
664                                ; evc <- newEqVar wanted_flavor fam_ty rhs_xi_var
665                                ; let eqv = evc_the_evvar evc -- Not going to be cached
666                                      ct = CFunEqCan { cc_id = eqv
667                                                     , cc_flavor = wanted_flavor
668                                                     -- Always Wanted, not Derived
669                                                     , cc_fun = tc
670                                                     , cc_tyargs = xi_args
671                                                     , cc_rhs    = rhs_xi_var 
672                                                     , cc_depth  = d }
673                                           -- Update the flat cache: just an optimisation!
674                                ; updateFlatCache eqv fl tc xi_args rhs_xi_var WhileFlattening
675                                ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) } }
676
677            -- Emit the flat constraints
678          ; updWorkListTcS $ appendWorkListEqs ct
679
680          ; let (cos_args, cos_rest) = splitAt (tyConArity tc) cos
681          ; return ( mkAppTys rhs_xi xi_rest    -- NB mkAppTys: rhs_xi might not be a type variable
682                                                --    cf Trac #5655
683                   , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args)
684                                cos_rest
685                   ) }
686
687
688 flatten d ctxt ty@(ForAllTy {})
689 -- We allow for-alls when, but only when, no type function
690 -- applications inside the forall involve the bound type variables.
691   = do { let (tvs, rho) = splitForAllTys ty
692        ; when (under_families tvs rho) $ flattenForAllErrorTcS ctxt ty
693        ; (rho', co) <- flatten d ctxt rho
694        ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
695
696   where under_families tvs rho 
697             = go (mkVarSet tvs) rho 
698             where go _bound (TyVarTy _tv) = False
699                   go bound (TyConApp tc tys)
700                       | isSynFamilyTyCon tc
701                       , (args,rest) <- splitAt (tyConArity tc) tys
702                       = (tyVarsOfTypes args `intersectsVarSet` bound) || any (go bound) rest
703                       | otherwise = any (go bound) tys
704                   go bound (FunTy arg res)  = go bound arg || go bound res
705                   go bound (AppTy fun arg)  = go bound fun || go bound arg
706                   go bound (ForAllTy tv ty) = go (bound `extendVarSet` tv) ty
707
708
709 getCachedFlatEq :: TyCon -> [Xi] -> CtFlavor 
710                 -> FlatEqOrigin
711                 -> TcS (Maybe (Xi, TcCoercion))
712 -- Returns a coercion between (TyConApp tc xi_args ~ xi) if such an inert item exists
713 -- But also applies the substitution to the item via calling flatten recursively
714 getCachedFlatEq tc xi_args fl feq_origin
715   = do { let pty = mkTyConApp tc xi_args
716        ; traceTcS "getCachedFlatEq" $ ppr (mkTyConApp tc xi_args)
717        ; flat_cache <- getTcSEvVarFlatCache
718        ; inerts <- getTcSInerts
719        ; case lookupFunEq pty fl (inert_funeqs inerts) of
720            Nothing 
721                -> lookup_in_flat_cache pty flat_cache
722            res -> return res }
723   where lookup_in_flat_cache pty flat_cache 
724           = case lookupTM pty flat_cache of
725               Just (co',(xi',fl',when_generated)) -- ev' :: (TyConApp tc xi_args) ~ xi'
726                | fl' `canRewrite` fl
727                , feq_origin `origin_matches` when_generated
728                -> do { traceTcS "getCachedFlatEq" $ text "success!"
729                      ; (xi'',co) <- flatten 0 fl' xi' -- co :: xi'' ~ xi'
730                                     -- The only purpose of this flattening is to apply the
731                                     -- inert substitution (since everything in the flat cache
732                                     -- by construction will have a family-free RHS.
733                      ; return $ Just (xi'', co' `mkTcTransCo` (mkTcSymCo co)) }
734               _ -> do { traceTcS "getCachedFlatEq" $ text "failure!" <+> pprEvVarCache flat_cache
735                       ; return Nothing }
736
737 -----------------
738 addToWork :: TcS StopOrContinue -> TcS ()
739 addToWork tcs_action = tcs_action >>= stop_or_emit
740   where stop_or_emit Stop              = return ()
741         stop_or_emit (ContinueWith ct) = updWorkListTcS $ 
742                                          extendWorkListCt ct
743
744 canEqEvVarsCreated :: SubGoalDepth 
745                    -> [CtFlavor] -> [EvVarCreated] -> [Type] -> [Type]
746                    -> TcS StopOrContinue
747 canEqEvVarsCreated _d _fl [] _ _    = return Stop
748 canEqEvVarsCreated d (fl:fls) (evc:evcs) (ty1:tys1) (ty2:tys2) 
749   | isNewEvVar evc 
750   = let do_one evc0 sy1 sy2
751           | isNewEvVar evc0 
752           = canEq_ d fl (evc_the_evvar evc0) sy1 sy2
753           | otherwise = return ()
754     in do { _unused <- zipWith3M do_one evcs tys1 tys2 
755           ; canEq d fl (evc_the_evvar evc) ty1 ty2 }
756   | otherwise 
757   = canEqEvVarsCreated d fls evcs tys1 tys2
758 canEqEvVarsCreated _ _ _ _ _ = return Stop
759
760
761 canEq_ :: SubGoalDepth 
762        -> CtFlavor -> EqVar -> Type -> Type -> TcS ()
763 canEq_ d fl eqv ty1 ty2 = addToWork (canEq d fl eqv ty1 ty2)
764
765 canEq :: SubGoalDepth 
766       -> CtFlavor -> EqVar -> Type -> Type -> TcS StopOrContinue
767 canEq _d fl eqv ty1 ty2
768   | eqType ty1 ty2      -- Dealing with equality here avoids
769                         -- later spurious occurs checks for a~a
770   = do { when (isWanted fl) $ 
771               do { _ <- setEqBind eqv (mkTcReflCo ty1) fl; return () }
772        ; return Stop }
773
774 -- Split up an equality between function types into two equalities.
775 canEq d fl eqv (FunTy s1 t1) (FunTy s2 t2)
776   = do { argeqv <- newEqVar fl s1 s2
777        ; reseqv <- newEqVar fl t1 t2
778        ; let argeqv_v = evc_the_evvar argeqv
779              reseqv_v = evc_the_evvar reseqv
780        ; (fl1,fl2) <- case fl of
781            Wanted {} ->
782                do { _ <- setEqBind eqv (mkTcFunCo (mkTcCoVarCo argeqv_v) (mkTcCoVarCo reseqv_v)) fl
783                   ; return (fl,fl) }
784            Given {} ->
785                do { fl1 <- setEqBind argeqv_v (mkTcNthCo 0 (mkTcCoVarCo eqv)) fl
786                   ; fl2 <- setEqBind reseqv_v (mkTcNthCo 1 (mkTcCoVarCo eqv)) fl 
787                   ; return (fl1,fl2)
788                   }
789            Derived {} ->
790                return (fl,fl)
791
792        ; canEqEvVarsCreated d [fl2,fl1] [reseqv,argeqv] [t1,s1] [t2,s2] }
793
794 -- If one side is a variable, orient and flatten,
795 -- WITHOUT expanding type synonyms, so that we tend to 
796 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@
797 canEq d fl eqv ty1@(TyVarTy {}) ty2 
798   = canEqLeaf d fl eqv ty1 ty2
799 canEq d fl eqv ty1 ty2@(TyVarTy {})
800   = canEqLeaf d fl eqv ty1 ty2
801
802 canEq d fl eqv ty1@(TyConApp fn tys) ty2 
803   | isSynFamilyTyCon fn, length tys == tyConArity fn
804   = canEqLeaf d fl eqv ty1 ty2
805 canEq d fl eqv ty1 ty2@(TyConApp fn tys)
806   | isSynFamilyTyCon fn, length tys == tyConArity fn
807   = canEqLeaf d fl eqv ty1 ty2
808
809 canEq d fl eqv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
810   | isDecomposableTyCon tc1 && isDecomposableTyCon tc2
811   , tc1 == tc2
812   , length tys1 == length tys2
813   = -- Generate equalities for each of the corresponding arguments
814     do { let (kis1,  tys1') = span isKind tys1
815              (_kis2, tys2') = span isKind tys2
816        ; let kicos = map mkTcReflCo kis1
817
818        ; argeqvs <- zipWithM (newEqVar fl) tys1' tys2'
819        ; fls <- case fl of 
820            Wanted {} -> 
821              do { _ <- setEqBind eqv
822                          (mkTcTyConAppCo tc1 (kicos ++ map (mkTcCoVarCo . evc_the_evvar) argeqvs)) fl
823                 ; return (map (\_ -> fl) argeqvs) }
824            Given {} ->
825              let do_one argeqv n = setEqBind (evc_the_evvar argeqv) 
826                                              (mkTcNthCo n (mkTcCoVarCo eqv)) fl
827              in zipWithM do_one argeqvs [(length kicos)..]
828            Derived {} -> return (map (\_ -> fl) argeqvs)
829
830        ; canEqEvVarsCreated d fls argeqvs tys1' tys2' }
831
832 -- See Note [Equality between type applications]
833 --     Note [Care with type applications] in TcUnify
834 canEq d fl eqv ty1 ty2
835   | Nothing <- tcView ty1  -- Naked applications ONLY
836   , Nothing <- tcView ty2  -- See Note [Naked given applications]
837   , Just (s1,t1) <- tcSplitAppTy_maybe ty1
838   , Just (s2,t2) <- tcSplitAppTy_maybe ty2
839   = ASSERT( not (isKind t1) && not (isKind t2) )
840     if isGivenOrSolved fl then 
841         do { traceTcS "canEq/(app case)" $
842                 text "Ommitting decomposition of given equality between: " 
843                     <+> ppr ty1 <+> text "and" <+> ppr ty2
844                    -- We cannot decompose given applications
845                    -- because we no longer have 'left' and 'right'
846            ; return Stop }
847     else
848         do { evc1 <- newEqVar fl s1 s2
849            ; evc2 <- newEqVar fl t1 t2
850            ; let eqv1 = evc_the_evvar evc1
851                  eqv2 = evc_the_evvar evc2
852  
853            ; when (isWanted fl) $
854                   do { _ <- setEqBind eqv (mkTcAppCo (mkTcCoVarCo eqv1) (mkTcCoVarCo eqv2)) fl
855                      ; return () }
856            
857            ; canEqEvVarsCreated d [fl,fl] [evc1,evc2] [s1,t1] [s2,t2] }
858
859
860 canEq d fl eqv s1@(ForAllTy {}) s2@(ForAllTy {})
861  | tcIsForAllTy s1, tcIsForAllTy s2, 
862    Wanted {} <- fl 
863  = canEqFailure d fl eqv
864  | otherwise
865  = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
866       ; return Stop }
867
868 -- Finally expand any type synonym applications.
869 canEq d fl eqv ty1 ty2 | Just ty1' <- tcView ty1 = canEq d fl eqv ty1' ty2
870 canEq d fl eqv ty1 ty2 | Just ty2' <- tcView ty2 = canEq d fl eqv ty1 ty2'
871 canEq d fl eqv _ _                               = canEqFailure d fl eqv
872
873 canEqFailure :: SubGoalDepth 
874              -> CtFlavor -> EvVar -> TcS StopOrContinue
875 canEqFailure d fl eqv = do { emitFrozenError fl eqv d; return Stop }
876 \end{code}
877
878 Note [Naked given applications]
879 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
880 Consider: 
881    data A a 
882    type T a = A a 
883 and the given equality:  
884    [G] A a ~ T Int 
885 We will reach the case canEq where we do a tcSplitAppTy_maybe, but if
886 we dont have the guards (Nothing <- tcView ty1) (Nothing <- tcView
887 ty2) then the given equation is going to fall through and get
888 completely forgotten!
889
890 What we want instead is this clause to apply only when there is no
891 immediate top-level synonym; if there is one it will be later on
892 unfolded by the later stages of canEq.
893
894 Test-case is in typecheck/should_compile/GivenTypeSynonym.hs
895
896
897 Note [Equality between type applications]
898 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
899 If we see an equality of the form s1 t1 ~ s2 t2 we can always split
900 it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
901 functions (type functions use the TyConApp constructor, which never
902 shows up as the LHS of an AppTy).  Other than type functions, types
903 in Haskell are always 
904
905   (1) generative: a b ~ c d implies a ~ c, since different type
906       constructors always generate distinct types
907
908   (2) injective: a b ~ a d implies b ~ d; we never generate the
909       same type from different type arguments.
910
911
912 Note [Canonical ordering for equality constraints]
913 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
914 Implemented as (<+=) below:
915
916   - Type function applications always come before anything else.  
917   - Variables always come before non-variables (other than type
918       function applications).
919
920 Note that we don't need to unfold type synonyms on the RHS to check
921 the ordering; that is, in the rules above it's OK to consider only
922 whether something is *syntactically* a type function application or
923 not.  To illustrate why this is OK, suppose we have an equality of the
924 form 'tv ~ S a b c', where S is a type synonym which expands to a
925 top-level application of the type function F, something like
926
927   type S a b c = F d e
928
929 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
930 expansion contains type function applications the flattener will do
931 the expansion and then generate a skolem variable for the type
932 function application, so we end up with something like this:
933
934   tv ~ x
935   F d e ~ x
936
937 where x is the skolem variable.  This is one extra equation than
938 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
939 if we had noticed that S expanded to a top-level type function
940 application and flipped it around in the first place) but this way
941 keeps the code simpler.
942
943 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
944 ordering of tv ~ tv constraints.  There are several reasons why we
945 might:
946
947   (1) In order to be able to extract a substitution that doesn't
948       mention untouchable variables after we are done solving, we might
949       prefer to put touchable variables on the left. However, in and
950       of itself this isn't necessary; we can always re-orient equality
951       constraints at the end if necessary when extracting a substitution.
952
953   (2) To ensure termination we might think it necessary to put
954       variables in lexicographic order. However, this isn't actually 
955       necessary as outlined below.
956
957 While building up an inert set of canonical constraints, we maintain
958 the invariant that the equality constraints in the inert set form an
959 acyclic rewrite system when viewed as L-R rewrite rules.  Moreover,
960 the given constraints form an idempotent substitution (i.e. none of
961 the variables on the LHS occur in any of the RHS's, and type functions
962 never show up in the RHS at all), the wanted constraints also form an
963 idempotent substitution, and finally the LHS of a given constraint
964 never shows up on the RHS of a wanted constraint.  There may, however,
965 be a wanted LHS that shows up in a given RHS, since we do not rewrite
966 given constraints with wanted constraints.
967
968 Suppose we have an inert constraint set
969
970
971   tg_1 ~ xig_1         -- givens
972   tg_2 ~ xig_2
973   ...
974   tw_1 ~ xiw_1         -- wanteds
975   tw_2 ~ xiw_2
976   ...
977
978 where each t_i can be either a type variable or a type function
979 application. Now suppose we take a new canonical equality constraint,
980 t' ~ xi' (note among other things this means t' does not occur in xi')
981 and try to react it with the existing inert set.  We show by induction
982 on the number of t_i which occur in t' ~ xi' that this process will
983 terminate.
984
985 There are several ways t' ~ xi' could react with an existing constraint:
986
987 TODO: finish this proof.  The below was for the case where the entire
988 inert set is an idempotent subustitution...
989
990 (b) We could have t' = t_j for some j.  Then we obtain the new
991     equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j.  We
992     now canonicalize the new equality, which may involve decomposing it
993     into several canonical equalities, and recurse on these.  However,
994     none of the new equalities will contain t_j, so they have fewer
995     occurrences of the t_i than the original equation.
996
997 (a) We could have t_j occurring in xi' for some j, with t' /=
998     t_j. Then we substitute xi_j for t_j in xi' and continue.  However,
999     since none of the t_i occur in xi_j, we have decreased the
1000     number of t_i that occur in xi', since we eliminated t_j and did not
1001     introduce any new ones.
1002
1003 \begin{code}
1004 data TypeClassifier 
1005   = FskCls TcTyVar      -- ^ Flatten skolem 
1006   | VarCls TcTyVar      -- ^ Non-flatten-skolem variable 
1007   | FunCls TyCon [Type] -- ^ Type function, exactly saturated
1008   | OtherCls TcType     -- ^ Neither of the above
1009
1010 {- Useless these days! 
1011 unClassify :: TypeClassifier -> TcType
1012 unClassify (VarCls tv)      = TyVarTy tv
1013 unClassify (FskCls tv) = TyVarTy tv 
1014 unClassify (FunCls fn tys)  = TyConApp fn tys
1015 unClassify (OtherCls ty)    = ty
1016 -} 
1017
1018 classify :: TcType -> TypeClassifier
1019
1020 classify (TyVarTy tv) 
1021   | isTcTyVar tv, 
1022     FlatSkol {} <- tcTyVarDetails tv = FskCls tv
1023   | otherwise                        = VarCls tv
1024 classify (TyConApp tc tys) | isSynFamilyTyCon tc
1025                            , tyConArity tc == length tys
1026                            = FunCls tc tys
1027 classify ty                | Just ty' <- tcView ty
1028                            = case classify ty' of
1029                                OtherCls {} -> OtherCls ty
1030                                var_or_fn   -> var_or_fn
1031                            | otherwise 
1032                            = OtherCls ty
1033
1034 -- See note [Canonical ordering for equality constraints].
1035 reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool        
1036 -- (t1 `reOrient` t2) responds True 
1037 --   iff we should flip to (t2~t1)
1038 -- We try to say False if possible, to minimise evidence generation
1039 --
1040 -- Postcondition: After re-orienting, first arg is not OTherCls
1041 reOrient _fl (OtherCls {}) (FunCls {})   = True
1042 reOrient _fl (OtherCls {}) (FskCls {})   = True
1043 reOrient _fl (OtherCls {}) (VarCls {})   = True
1044 reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient"  -- One must be Var/Fun
1045
1046 reOrient _fl (FunCls {})   (VarCls _tv)  = False  
1047   -- But consider the following variation: isGiven fl && isMetaTyVar tv
1048
1049   -- See Note [No touchables as FunEq RHS] in TcSMonad
1050 reOrient _fl (FunCls {}) _                = False             -- Fun/Other on rhs
1051
1052 reOrient _fl (VarCls {}) (FunCls {})      = True 
1053
1054 reOrient _fl (VarCls {}) (FskCls {})      = False
1055
1056 reOrient _fl (VarCls {})  (OtherCls {})   = False
1057 reOrient _fl (VarCls tv1)  (VarCls tv2)  
1058   | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True 
1059   | otherwise                                = False 
1060   -- Just for efficiency, see CTyEqCan invariants 
1061
1062 reOrient _fl (FskCls {}) (VarCls tv2)     = isMetaTyVar tv2 
1063   -- Just for efficiency, see CTyEqCan invariants
1064
1065 reOrient _fl (FskCls {}) (FskCls {})     = False
1066 reOrient _fl (FskCls {}) (FunCls {})     = True 
1067 reOrient _fl (FskCls {}) (OtherCls {})   = False 
1068
1069 ------------------
1070
1071 canEqLeaf :: SubGoalDepth -- Depth
1072           -> CtFlavor -> EqVar 
1073           -> Type -> Type 
1074           -> TcS StopOrContinue
1075 -- Canonicalizing "leaf" equality constraints which cannot be
1076 -- decomposed further (ie one of the types is a variable or
1077 -- saturated type function application).  
1078
1079 -- Preconditions: 
1080 --    * one of the two arguments is variable or family applications
1081 --    * the two types are not equal (looking through synonyms)
1082 canEqLeaf d fl eqv s1 s2 
1083   | cls1 `re_orient` cls2
1084   = do { traceTcS "canEqLeaf (reorienting)" $ ppr eqv <+> dcolon <+> pprEq s1 s2
1085        ; delCachedEvVar eqv fl
1086        ; evc <- newEqVar fl s2 s1
1087        ; let eqv' = evc_the_evvar evc
1088        ; fl' <- case fl of 
1089            Wanted {}  -> setEqBind eqv (mkTcSymCo (mkTcCoVarCo eqv')) fl 
1090            Given {}   -> setEqBind eqv' (mkTcSymCo (mkTcCoVarCo eqv)) fl 
1091            Derived {} -> return fl 
1092        ; if isNewEvVar evc then 
1093              do { canEqLeafOriented d fl' eqv' s2 s1 }
1094          else return Stop 
1095        }
1096   | otherwise
1097   = do { traceTcS "canEqLeaf" $ ppr (mkEqPred (s1,s2))
1098        ; canEqLeafOriented d fl eqv s1 s2 }
1099   where
1100     re_orient = reOrient fl 
1101     cls1 = classify s1
1102     cls2 = classify s2
1103
1104 canEqLeafOriented :: SubGoalDepth -- Depth
1105                   -> CtFlavor -> EqVar 
1106                   -> TcType -> TcType -> TcS StopOrContinue
1107 -- By now s1 will either be a variable or a type family application
1108 canEqLeafOriented d fl eqv s1 s2
1109   | let k1 = typeKind s1
1110   , let k2 = typeKind s2
1111   -- Establish kind invariants for CFunEqCan and CTyEqCan
1112   = do { are_compat <- compatKindTcS k1 k2
1113        ; can_unify <- if not are_compat
1114                       then unifyKindTcS s1 s2 k1 k2
1115                       else return False
1116          -- If the kinds cannot be unified or are not compatible, don't fail
1117          -- right away; instead, emit a frozen error
1118        ; if (not are_compat && not can_unify) then
1119              canEqFailure d fl eqv
1120          else can_eq_kinds_ok d fl eqv s1 s2 }
1121
1122   where can_eq_kinds_ok d fl eqv s1 s2
1123           | Just (fn,tys1) <- splitTyConApp_maybe s1
1124           = canEqLeafFunEqLeftRec d fl eqv (fn,tys1) s2
1125           | Just tv <- getTyVar_maybe s1
1126           = canEqLeafTyVarLeftRec d fl eqv tv s2
1127           | otherwise
1128           = pprPanic "canEqLeafOriented" $
1129             text "Non-variable or non-family equality LHS" <+> ppr eqv <+> 
1130                                                        dcolon <+> ppr (evVarPred eqv)
1131 canEqLeafFunEqLeftRec :: SubGoalDepth
1132                       -> CtFlavor 
1133                       -> EqVar 
1134                       -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
1135 canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2  -- eqv :: F tys1 ~ ty2
1136   = do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
1137        ; (xis1,cos1) <- 
1138            {-# SCC "flattenMany" #-}
1139            flattenMany d fl tys1 -- Flatten type function arguments
1140                                  -- cos1 :: xis1 ~ tys1
1141
1142 --       ; inerts <- getTcSInerts
1143 --        ; let fam_eqs   = inert_funeqs inerts
1144
1145        ; let flat_ty = mkTyConApp fn xis1
1146
1147        ; is_cached <- getCachedFlatEq fn xis1 fl WhenSolved
1148                       -- Lookup if we have solved this goal already
1149 {-
1150        ; let is_cached = {-# SCC "lookupFunEq" #-} 
1151                          lookupFunEq flat_ty fl fam_eqs
1152 -}
1153        ; let no_flattening = all isTcReflCo cos1
1154                       
1155        ; if no_flattening && isNothing is_cached then 
1156              canEqLeafFunEqLeft d fl eqv (fn,xis1) ty2
1157          else do
1158        { let (final_co, final_ty)
1159                  | no_flattening        -- Just in inerts
1160                  , Just (rhs_ty, ret_eq) <- is_cached
1161                  = (mkTcSymCo ret_eq, rhs_ty)
1162                  | Nothing <- is_cached -- Just flattening
1163                  = (mkTcTyConAppCo fn cos1, flat_ty)
1164                  | Just (rhs_ty, ret_eq) <- is_cached  -- Both
1165                  = (mkTcSymCo ret_eq `mkTcTransCo` mkTcTyConAppCo fn cos1, rhs_ty)
1166                  | otherwise = panic "No flattening and not cached!"
1167        ; delCachedEvVar eqv fl
1168        ; evc <- newEqVar fl final_ty ty2
1169        ; let new_eqv = evc_the_evvar evc
1170        ; fl' <- case fl of
1171            Wanted {}  -> setEqBind eqv 
1172                            (mkTcSymCo final_co `mkTcTransCo` (mkTcCoVarCo new_eqv)) fl
1173            Given {}   -> setEqBind new_eqv (final_co `mkTcTransCo` (mkTcCoVarCo eqv)) fl
1174            Derived {} -> return fl
1175        ; if isNewEvVar evc then
1176              if isNothing is_cached then
1177                  {-# SCC "canEqLeafFunEqLeft" #-}
1178                  canEqLeafFunEqLeft d fl' new_eqv (fn,xis1) ty2
1179              else
1180                  canEq (d+1) fl' new_eqv final_ty ty2
1181          else return Stop
1182        }
1183        }
1184
1185 lookupFunEq :: PredType -> CtFlavor -> TypeMap Ct -> Maybe (TcType, TcCoercion)
1186 lookupFunEq pty fl fam_eqs = lookup_funeq pty fam_eqs
1187   where lookup_funeq pty fam_eqs
1188           | Just ct <- lookupTM pty fam_eqs
1189           , cc_flavor ct `canRewrite` fl 
1190           = Just (cc_rhs ct, mkTcCoVarCo (cc_id ct))
1191           | otherwise 
1192           = Nothing
1193
1194 canEqLeafFunEqLeft :: SubGoalDepth -- Depth
1195                    -> CtFlavor -> EqVar -> (TyCon,[Xi]) 
1196                    -> TcType -> TcS StopOrContinue
1197 -- Precondition: No more flattening is needed for the LHS
1198 canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
1199  = {-# SCC "canEqLeafFunEqLeft" #-}
1200    do { traceTcS "canEqLeafFunEqLeft" $ pprEq (mkTyConApp fn xis1) s2
1201       ; (xi2,co2) <- 
1202           {-# SCC "flatten" #-} 
1203           flatten d fl s2 -- co2 :: xi2 ~ s2
1204       ; let no_flattening_happened = isTcReflCo co2
1205       ; if no_flattening_happened then 
1206             continueWith $ CFunEqCan { cc_id     = eqv
1207                                      , cc_flavor = fl
1208                                      , cc_fun    = fn
1209                                      , cc_tyargs = xis1 
1210                                      , cc_rhs    = xi2 
1211                                      , cc_depth  = d }
1212         else do { delCachedEvVar eqv fl
1213                 ; evc <- 
1214                     {-# SCC "newEqVar" #-}
1215                     newEqVar fl (mkTyConApp fn xis1) xi2
1216                 ; let new_eqv = evc_the_evvar evc -- F xis1 ~ xi2 
1217                       new_cv  = mkTcCoVarCo new_eqv
1218                       cv      = mkTcCoVarCo eqv    -- F xis1 ~ s2
1219                 ; fl' <- case fl of
1220                     Wanted {} -> setEqBind eqv (new_cv `mkTcTransCo` co2) fl 
1221                     Given {}  -> setEqBind new_eqv (cv `mkTcTransCo` mkTcSymCo co2) fl
1222                     Derived {} -> return fl
1223                 ; if isNewEvVar evc then 
1224                       do { continueWith $
1225                            CFunEqCan { cc_id = new_eqv
1226                                      , cc_flavor = fl'
1227                                      , cc_fun    = fn
1228                                      , cc_tyargs = xis1 
1229                                      , cc_rhs    = xi2 
1230                                      , cc_depth  = d } }
1231                   else return Stop }  }
1232
1233
1234 canEqLeafTyVarLeftRec :: SubGoalDepth
1235                       -> CtFlavor -> EqVar
1236                       -> TcTyVar -> TcType -> TcS StopOrContinue
1237 canEqLeafTyVarLeftRec d fl eqv tv s2              -- eqv :: tv ~ s2
1238   = do {  traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
1239        ; (xi1,co1) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv
1240        ; case isTcReflCo co1 of 
1241              True -- If reflco and variable, just go on
1242                | Just tv' <- getTyVar_maybe xi1 
1243                  -> canEqLeafTyVarLeft d fl eqv tv' s2
1244              _ -> -- If not a variable or not refl co, must rewrite and go on
1245                do { delCachedEvVar eqv fl
1246                   ; evc <- newEqVar fl xi1 s2  -- new_ev :: xi1 ~ s2
1247                   ; let new_ev = evc_the_evvar evc
1248                   ; fl' <- case fl of 
1249                     Wanted  {} -> setEqBind eqv 
1250                                     (mkTcSymCo co1 `mkTcTransCo` mkTcCoVarCo new_ev) fl
1251                     Given   {} -> setEqBind new_ev
1252                                     (co1 `mkTcTransCo` mkTcCoVarCo eqv) fl
1253                     Derived {} -> return fl
1254                   ; if isNewEvVar evc then
1255                       do { canEq d fl' new_ev xi1 s2 }
1256                     else return Stop
1257                   }
1258        }
1259
1260 canEqLeafTyVarLeft :: SubGoalDepth -- Depth
1261                    -> CtFlavor -> EqVar
1262                    -> TcTyVar -> TcType -> TcS StopOrContinue
1263 -- Precondition LHS is fully rewritten from inerts (but not RHS)
1264 canEqLeafTyVarLeft d fl eqv tv s2       -- eqv : tv ~ s2
1265   = do { traceTcS "canEqLeafTyVarLeft" (pprEq (mkTyVarTy tv) s2)
1266        ; (xi2, co) <- flatten d fl s2   -- Flatten RHS   co : xi2 ~ s2
1267                                                
1268        ; let no_flattening_happened = isTcReflCo co
1269              
1270        ; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv  =" <+> ppr tv
1271                                                      , text "s2  =" <+> ppr s2
1272                                                      , text "xi2 =" <+> ppr xi2]))
1273
1274                       -- Flattening the RHS may reveal an identity coercion, which should
1275                       -- not be reported as occurs check error! 
1276        ; let is_same_tv
1277                | Just tv' <- getTyVar_maybe xi2, tv' == tv
1278                = True
1279                | otherwise = False
1280        ; if is_same_tv then
1281              do { delCachedEvVar eqv fl
1282                 ; when (isWanted fl) $ 
1283                        do { _ <- setEqBind eqv co fl; return () }
1284                 ; return Stop }
1285          else
1286     do { -- Do an occurs check, and return a possibly
1287          -- unfolded version of the RHS, if we had to 
1288          -- unfold any type synonyms to get rid of tv.
1289          occ_check_result <- canOccursCheck fl tv xi2
1290
1291        ; let xi2'
1292               | Just xi2_unfolded <- occ_check_result
1293               = xi2_unfolded
1294               | otherwise = xi2
1295
1296
1297        ; if no_flattening_happened then
1298              if isNothing occ_check_result then 
1299                  canEqFailure d fl (setVarType eqv $ mkEqPred (mkTyVarTy tv, xi2'))
1300              else 
1301                  continueWith $ CTyEqCan { cc_id     = eqv
1302                                          , cc_flavor = fl
1303                                          , cc_tyvar  = tv
1304                                          , cc_rhs    = xi2'
1305                                          , cc_depth  = d }
1306          else -- Flattening happened, in any case we have to create new variable 
1307               -- even if we report an occurs check error
1308              do { delCachedEvVar eqv fl
1309                 ; evc <- newEqVar fl (mkTyVarTy tv) xi2' 
1310                 ; let eqv' = evc_the_evvar evc -- eqv' : tv ~ xi2'
1311                       cv   = mkTcCoVarCo eqv    -- cv : tv ~ s2
1312                       cv'  = mkTcCoVarCo eqv'   -- cv': tv ~ xi2'
1313                  ; fl' <- case fl of 
1314                      Wanted {}  -> setEqBind eqv (cv' `mkTcTransCo` co) fl         -- tv ~ xi2' ~ s2
1315                      Given {}   -> setEqBind eqv' (cv `mkTcTransCo` mkTcSymCo co) fl -- tv ~ s2 ~ xi2'
1316                      Derived {} -> return fl
1317
1318                  ; if isNewEvVar evc then 
1319                        if isNothing occ_check_result then 
1320                            canEqFailure d fl eqv'
1321                        else continueWith CTyEqCan { cc_id     = eqv'
1322                                                   , cc_flavor = fl'
1323                                                   , cc_tyvar  = tv
1324                                                   , cc_rhs    = xi2' 
1325                                                   , cc_depth  = d }
1326                    else 
1327                        return Stop } } }
1328
1329
1330 -- See Note [Type synonyms and canonicalization].
1331 -- Check whether the given variable occurs in the given type.  We may
1332 -- have needed to do some type synonym unfolding in order to get rid
1333 -- of the variable, so we also return the unfolded version of the
1334 -- type, which is guaranteed to be syntactically free of the given
1335 -- type variable.  If the type is already syntactically free of the
1336 -- variable, then the same type is returned.
1337 --
1338 -- Precondition: the two types are not equal (looking though synonyms)
1339 canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
1340 canOccursCheck _gw tv xi = return (expandAway tv xi)
1341 \end{code}
1342
1343 @expandAway tv xi@ expands synonyms in xi just enough to get rid of
1344 occurrences of tv, if that is possible; otherwise, it returns Nothing.
1345 For example, suppose we have
1346   type F a b = [a]
1347 Then
1348   expandAway b (F Int b) = Just [Int]
1349 but
1350   expandAway a (F a Int) = Nothing
1351
1352 We don't promise to do the absolute minimum amount of expanding
1353 necessary, but we try not to do expansions we don't need to.  We
1354 prefer doing inner expansions first.  For example,
1355   type F a b = (a, Int, a, [a])
1356   type G b   = Char
1357 We have
1358   expandAway b (F (G b)) = F Char
1359 even though we could also expand F to get rid of b.
1360
1361 \begin{code}
1362 expandAway :: TcTyVar -> Xi -> Maybe Xi
1363 expandAway tv t@(TyVarTy tv')
1364   | tv == tv' = Nothing
1365   | otherwise = Just t
1366 expandAway tv xi
1367   | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
1368 expandAway tv (AppTy ty1 ty2) 
1369   = do { ty1' <- expandAway tv ty1
1370        ; ty2' <- expandAway tv ty2 
1371        ; return (mkAppTy ty1' ty2') }
1372 -- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
1373 expandAway tv (FunTy ty1 ty2)
1374   = do { ty1' <- expandAway tv ty1 
1375        ; ty2' <- expandAway tv ty2 
1376        ; return (mkFunTy ty1' ty2') } 
1377 -- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
1378 expandAway tv ty@(ForAllTy {}) 
1379   = let (tvs,rho) = splitForAllTys ty
1380         tvs_knds  = map tyVarKind tvs 
1381     in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
1382        -- Can't expand away the kinds unless we create 
1383        -- fresh variables which we don't want to do at this point.
1384            Nothing 
1385        else do { rho' <- expandAway tv rho
1386                ; return (mkForAllTys tvs rho') }
1387 -- For a type constructor application, first try expanding away the
1388 -- offending variable from the arguments.  If that doesn't work, next
1389 -- see if the type constructor is a type synonym, and if so, expand
1390 -- it and try again.
1391 expandAway tv ty@(TyConApp tc tys)
1392   = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
1393
1394 \end{code}
1395
1396 Note [Type synonyms and canonicalization]
1397 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1398
1399 We treat type synonym applications as xi types, that is, they do not
1400 count as type function applications.  However, we do need to be a bit
1401 careful with type synonyms: like type functions they may not be
1402 generative or injective.  However, unlike type functions, they are
1403 parametric, so there is no problem in expanding them whenever we see
1404 them, since we do not need to know anything about their arguments in
1405 order to expand them; this is what justifies not having to treat them
1406 as specially as type function applications.  The thing that causes
1407 some subtleties is that we prefer to leave type synonym applications
1408 *unexpanded* whenever possible, in order to generate better error
1409 messages.
1410
1411 If we encounter an equality constraint with type synonym applications
1412 on both sides, or a type synonym application on one side and some sort
1413 of type application on the other, we simply must expand out the type
1414 synonyms in order to continue decomposing the equality constraint into
1415 primitive equality constraints.  For example, suppose we have
1416
1417   type F a = [Int]
1418
1419 and we encounter the equality
1420
1421   F a ~ [b]
1422
1423 In order to continue we must expand F a into [Int], giving us the
1424 equality
1425
1426   [Int] ~ [b]
1427
1428 which we can then decompose into the more primitive equality
1429 constraint
1430
1431   Int ~ b.
1432
1433 However, if we encounter an equality constraint with a type synonym
1434 application on one side and a variable on the other side, we should
1435 NOT (necessarily) expand the type synonym, since for the purpose of
1436 good error messages we want to leave type synonyms unexpanded as much
1437 as possible.
1438
1439 However, there is a subtle point with type synonyms and the occurs
1440 check that takes place for equality constraints of the form tv ~ xi.
1441 As an example, suppose we have
1442
1443   type F a = Int
1444
1445 and we come across the equality constraint
1446
1447   a ~ F a
1448
1449 This should not actually fail the occurs check, since expanding out
1450 the type synonym results in the legitimate equality constraint a ~
1451 Int.  We must actually do this expansion, because unifying a with F a
1452 will lead the type checker into infinite loops later.  Put another
1453 way, canonical equality constraints should never *syntactically*
1454 contain the LHS variable in the RHS type.  However, we don't always
1455 need to expand type synonyms when doing an occurs check; for example,
1456 the constraint
1457
1458   a ~ F b
1459
1460 is obviously fine no matter what F expands to. And in this case we
1461 would rather unify a with F b (rather than F b's expansion) in order
1462 to get better error messages later.
1463
1464 So, when doing an occurs check with a type synonym application on the
1465 RHS, we use some heuristics to find an expansion of the RHS which does
1466 not contain the variable from the LHS.  In particular, given
1467
1468   a ~ F t1 ... tn
1469
1470 we first try expanding each of the ti to types which no longer contain
1471 a.  If this turns out to be impossible, we next try expanding F
1472 itself, and so on.
1473
1474
1475 %************************************************************************
1476 %*                                                                      *
1477 %*          Functional dependencies, instantiation of equations
1478 %*                                                                      *
1479 %************************************************************************
1480
1481 When we spot an equality arising from a functional dependency,
1482 we now use that equality (a "wanted") to rewrite the work-item
1483 constraint right away.  This avoids two dangers
1484
1485  Danger 1: If we send the original constraint on down the pipeline
1486            it may react with an instance declaration, and in delicate
1487            situations (when a Given overlaps with an instance) that
1488            may produce new insoluble goals: see Trac #4952
1489
1490  Danger 2: If we don't rewrite the constraint, it may re-react
1491            with the same thing later, and produce the same equality
1492            again --> termination worries.
1493
1494 To achieve this required some refactoring of FunDeps.lhs (nicer
1495 now!).  
1496
1497 \begin{code}
1498 rewriteWithFunDeps :: [Equation]
1499                    -> [Xi] 
1500                    -> WantedLoc 
1501                    -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) 
1502                                            -- Not quite a WantedEvVar unfortunately
1503                                            -- Because our intention could be to make 
1504                                            -- it derived at the end of the day
1505 -- NB: The flavor of the returned EvVars will be decided by the caller
1506 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1507 rewriteWithFunDeps eqn_pred_locs xis wloc
1508  = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
1509       ; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
1510             fd_ev_pos = concat fd_ev_poss
1511             (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
1512       ; if null fd_ev_pos then return Nothing
1513         else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
1514
1515 instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
1516 -- Post: Returns the position index as well as the corresponding FunDep equality
1517 instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
1518                         , fd_pred1 = d1, fd_pred2 = d2 })
1519   = do { let tvs = varSetElems qtvs
1520        ; tvs' <- mapM instFlexiTcS tvs  -- IA0_TODO: we might need to do kind substitution
1521        ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
1522        ; foldM (do_one subst) [] eqs }
1523   where 
1524     do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
1525        = let sty1 = Type.substTy subst ty1 
1526              sty2 = Type.substTy subst ty2 
1527          in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
1528             else do { eqv <- newEqVar (Derived wl) sty1 sty2 -- Create derived or cached by deriveds
1529                     ; let wl' = push_ctx wl 
1530                     ; if isNewEvVar eqv then 
1531                           return $ (i,(evc_the_evvar eqv,wl')):ievs 
1532                       else -- We are eventually going to emit FD work back in the work list so 
1533                            -- it is important that we only return the /freshly created/ and not 
1534                            -- some existing equality!
1535                           return ievs }
1536
1537     push_ctx :: WantedLoc -> WantedLoc 
1538     push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1539
1540 mkEqnMsg :: (TcPredType, SDoc) 
1541          -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
1542 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1543   = do  { zpred1 <- TcM.zonkTcPredType pred1
1544         ; zpred2 <- TcM.zonkTcPredType pred2
1545         ; let { tpred1 = tidyType tidy_env zpred1
1546               ; tpred2 = tidyType tidy_env zpred2 }
1547         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1548                           nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
1549                           nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1550         ; return (tidy_env, msg) }
1551
1552 rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
1553                   -> [Type]                    -- A sequence of types: tys
1554                   -> [(Type, TcCoercion)]      -- Returns: [(ty', co : ty' ~ ty)]
1555 rewriteDictParams param_eqs tys
1556   = zipWith do_one tys [0..]
1557   where
1558     do_one :: Type -> Int -> (Type, TcCoercion)
1559     do_one ty n = case lookup n param_eqs of
1560                     Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
1561                     Nothing  -> (ty,             mkTcReflCo ty) -- Identity
1562
1563     get_fst_ty (wev,_wloc) 
1564       | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
1565       = ty1
1566       | otherwise 
1567       = panic "rewriteDictParams: non equality fundep!?"
1568
1569         
1570 emitFDWork :: Bool
1571            -> [(EvVar,WantedLoc)] 
1572            -> SubGoalDepth -> TcS () 
1573 emitFDWork as_wanted evlocs d 
1574   = updWorkListTcS $ appendWorkListEqs fd_cts
1575   where fd_cts = map mk_fd_ct evlocs 
1576         mk_fl wl = if as_wanted then (Wanted wl) else (Derived wl)
1577         mk_fd_ct (v,wl) = CNonCanonical { cc_id = v
1578                                         , cc_flavor = mk_fl wl 
1579                                         , cc_depth = d }
1580
1581 emitFDWorkAsDerived, emitFDWorkAsWanted :: [(EvVar,WantedLoc)] 
1582                                         -> SubGoalDepth 
1583                                         -> TcS () 
1584 emitFDWorkAsDerived = emitFDWork False
1585 emitFDWorkAsWanted  = emitFDWork True 
1586
1587 \end{code}