a90627091f43e5909824a98139993a88f7c08218
[ghc.git] / compiler / typecheck / TcCanonical.lhs
1 \begin{code}
2 module TcCanonical(
3     canonicalize, emitWorkNC,
4     StopOrContinue (..)
5  ) where
6
7 #include "HsVersions.h"
8
9 import TcRnTypes
10 import TcType
11 import Type
12 import Kind
13 import TcEvidence
14 import Class
15 import TyCon
16 import TypeRep
17 import Var
18 import VarEnv
19 import OccName( OccName )
20 import Outputable
21 import Control.Monad    ( when )
22 import DynFlags( DynFlags )
23 import VarSet
24 import TcSMonad
25 import FastString
26
27 import Util
28 import BasicTypes
29 import Maybes( catMaybes )
30 \end{code}
31
32
33 %************************************************************************
34 %*                                                                      *
35 %*                      The Canonicaliser                               *
36 %*                                                                      *
37 %************************************************************************
38
39 Note [Canonicalization]
40 ~~~~~~~~~~~~~~~~~~~~~~~
41
42 Canonicalization converts a flat constraint to a canonical form. It is
43 unary (i.e. treats individual constraints one at a time), does not do
44 any zonking, but lives in TcS monad because it needs to create fresh
45 variables (for flattening) and consult the inerts (for efficiency).
46
47 The execution plan for canonicalization is the following:
48
49   1) Decomposition of equalities happens as necessary until we reach a
50      variable or type family in one side. There is no decomposition step
51      for other forms of constraints.
52
53   2) If, when we decompose, we discover a variable on the head then we
54      look at inert_eqs from the current inert for a substitution for this
55      variable and contine decomposing. Hence we lazily apply the inert
56      substitution if it is needed.
57
58   3) If no more decomposition is possible, we deeply apply the substitution
59      from the inert_eqs and continue with flattening.
60
61   4) During flattening, we examine whether we have already flattened some
62      function application by looking at all the CTyFunEqs with the same
63      function in the inert set. The reason for deeply applying the inert
64      substitution at step (3) is to maximise our chances of matching an
65      already flattened family application in the inert.
66
67 The net result is that a constraint coming out of the canonicalization
68 phase cannot be rewritten any further from the inerts (but maybe /it/ can
69 rewrite an inert or still interact with an inert in a further phase in the
70 simplifier.
71
72 \begin{code}
73
74 -- Informative results of canonicalization
75 data StopOrContinue
76   = ContinueWith Ct   -- Either no canonicalization happened, or if some did
77                       -- happen, it is still safe to just keep going with this
78                       -- work item.
79   | Stop              -- Some canonicalization happened, extra work is now in
80                       -- the TcS WorkList.
81
82 instance Outputable StopOrContinue where
83   ppr Stop             = ptext (sLit "Stop")
84   ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
85
86
87 continueWith :: Ct -> TcS StopOrContinue
88 continueWith = return . ContinueWith
89
90 andWhenContinue :: TcS StopOrContinue
91                 -> (Ct -> TcS StopOrContinue)
92                 -> TcS StopOrContinue
93 andWhenContinue tcs1 tcs2
94   = do { r <- tcs1
95        ; case r of
96            Stop            -> return Stop
97            ContinueWith ct -> tcs2 ct }
98
99 \end{code}
100
101 Note [Caching for canonicals]
102 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
103 Our plan with pre-canonicalization is to be able to solve a constraint
104 really fast from existing bindings in TcEvBinds. So one may think that
105 the condition (isCNonCanonical) is not necessary.  However consider
106 the following setup:
107
108 InertSet = { [W] d1 : Num t }
109 WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
110
111 Now, we prioritize equalities, but in our concrete example
112 (should_run/mc17.hs) the first (d2) constraint is dealt with first,
113 because (t ~ Int) is an equality that only later appears in the
114 worklist since it is pulled out from a nested implication
115 constraint. So, let's examine what happens:
116
117    - We encounter work item (d2 : Num t)
118
119    - Nothing is yet in EvBinds, so we reach the interaction with inerts
120      and set:
121               d2 := d1
122     and we discard d2 from the worklist. The inert set remains unaffected.
123
124    - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
125      (d1 : Num t) from the inerts.  Then that equation gets
126      spontaneously solved, perhaps. We end up with:
127         InertSet : { [G] c : t ~ Int }
128         WorkList : { [W] d1 : Num t}
129
130    - Now we examine (d1), we observe that there is a binding for (Num
131      t) in the evidence binds and we set:
132              d1 := d2
133      and end up in a loop!
134
135 Now, the constraints that get kicked out from the inert set are always
136 Canonical, so by restricting the use of the pre-canonicalizer to
137 NonCanonical constraints we eliminate this danger. Moreover, for
138 canonical constraints we already have good caching mechanisms
139 (effectively the interaction solver) and we are interested in reducing
140 things like superclasses of the same non-canonical constraint being
141 generated hence I don't expect us to lose a lot by introducing the
142 (isCNonCanonical) restriction.
143
144 A similar situation can arise in TcSimplify, at the end of the
145 solve_wanteds function, where constraints from the inert set are
146 returned as new work -- our substCt ensures however that if they are
147 not rewritten by subst, they remain canonical and hence we will not
148 attempt to solve them from the EvBinds. If on the other hand they did
149 get rewritten and are now non-canonical they will still not match the
150 EvBinds, so we are again good.
151
152
153
154 \begin{code}
155
156 -- Top-level canonicalization
157 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
158
159 canonicalize :: Ct -> TcS StopOrContinue
160 canonicalize ct@(CNonCanonical { cc_ev = ev })
161   = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
162        ; {-# SCC "canEvVar" #-}
163          canEvNC ev }
164
165 canonicalize (CDictCan { cc_ev = ev
166                        , cc_class  = cls
167                        , cc_tyargs = xis })
168   = {-# SCC "canClass" #-}
169     canClass ev cls xis -- Do not add any superclasses
170 canonicalize (CTyEqCan { cc_ev = ev
171                        , cc_tyvar  = tv
172                        , cc_rhs    = xi })
173   = {-# SCC "canEqLeafTyVarEq" #-}
174     canEqTyVar ev NotSwapped tv xi xi
175
176 canonicalize (CFunEqCan { cc_ev = ev
177                         , cc_fun    = fn
178                         , cc_tyargs = xis1
179                         , cc_rhs    = xi2 })
180   = {-# SCC "canEqLeafFunEq" #-}
181     canEqLeafFun ev NotSwapped fn xis1 xi2 xi2
182
183 canonicalize (CIrredEvCan { cc_ev = ev })
184   = canIrred ev
185 canonicalize (CHoleCan { cc_ev = ev, cc_occ = occ })
186   = canHole ev occ
187
188 canEvNC :: CtEvidence -> TcS StopOrContinue
189 -- Called only for non-canonical EvVars
190 canEvNC ev
191   = case classifyPredType (ctEvPred ev) of
192       ClassPred cls tys -> traceTcS "canEvNC:cls" (ppr cls <+> ppr tys) >> canClassNC ev cls tys
193       EqPred ty1 ty2    -> traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)   >> canEqNC    ev ty1 ty2
194       TuplePred tys     -> traceTcS "canEvNC:tup" (ppr tys)             >> canTuple   ev tys
195       IrredPred {}      -> traceTcS "canEvNC:irred" (ppr (ctEvPred ev)) >> canIrred   ev
196 \end{code}
197
198
199 %************************************************************************
200 %*                                                                      *
201 %*                      Tuple Canonicalization
202 %*                                                                      *
203 %************************************************************************
204
205 \begin{code}
206 canTuple :: CtEvidence -> [PredType] -> TcS StopOrContinue
207 canTuple ev tys
208   = do { traceTcS "can_pred" (text "TuplePred!")
209        ; let xcomp = EvTupleMk
210              xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
211        ; ctevs <- xCtEvidence ev (XEvTerm tys xcomp xdecomp)
212        ; canEvVarsCreated ctevs }
213 \end{code}
214
215 %************************************************************************
216 %*                                                                      *
217 %*                      Class Canonicalization
218 %*                                                                      *
219 %************************************************************************
220
221 \begin{code}
222 canClass, canClassNC
223    :: CtEvidence
224    -> Class -> [Type] -> TcS StopOrContinue
225 -- Precondition: EvVar is class evidence
226
227 -- The canClassNC version is used on non-canonical constraints
228 -- and adds superclasses.  The plain canClass version is used
229 -- for already-canonical class constraints (but which might have
230 -- been subsituted or somthing), and hence do not need superclasses
231
232 canClassNC ev cls tys
233   = canClass ev cls tys
234     `andWhenContinue` emitSuperclasses
235
236 canClass ev cls tys
237   = do { (xis, cos) <- flattenMany FMFullFlatten ev tys
238        ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
239              xi = mkClassPred cls xis
240        ; mb <- rewriteEvidence ev xi co
241        ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
242                                    , ppr xi, ppr mb ])
243        ; case mb of
244            Nothing -> return Stop
245            Just new_ev -> continueWith $
246                           CDictCan { cc_ev = new_ev
247                                    , cc_tyargs = xis, cc_class = cls } }
248
249 emitSuperclasses :: Ct -> TcS StopOrContinue
250 emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls })
251             -- Add superclasses of this one here, See Note [Adding superclasses].
252             -- But only if we are not simplifying the LHS of a rule.
253  = do { newSCWorkFromFlavored ev cls xis_new
254       -- Arguably we should "seq" the coercions if they are derived,
255       -- as we do below for emit_kind_constraint, to allow errors in
256       -- superclasses to be executed if deferred to runtime!
257       ; continueWith ct }
258 emitSuperclasses _ = panic "emit_superclasses of non-class!"
259 \end{code}
260
261 Note [Adding superclasses]
262 ~~~~~~~~~~~~~~~~~~~~~~~~~~
263 Since dictionaries are canonicalized only once in their lifetime, the
264 place to add their superclasses is canonicalisation (The alternative
265 would be to do it during constraint solving, but we'd have to be
266 extremely careful to not repeatedly introduced the same superclass in
267 our worklist). Here is what we do:
268
269 For Givens:
270        We add all their superclasses as Givens.
271
272 For Wanteds:
273        Generally speaking we want to be able to add superclasses of
274        wanteds for two reasons:
275
276        (1) Oportunities for improvement. Example:
277                   class (a ~ b) => C a b
278            Wanted constraint is: C alpha beta
279            We'd like to simply have C alpha alpha. Similar
280            situations arise in relation to functional dependencies.
281
282        (2) To have minimal constraints to quantify over:
283            For instance, if our wanted constraint is (Eq a, Ord a)
284            we'd only like to quantify over Ord a.
285
286        To deal with (1) above we only add the superclasses of wanteds
287        which may lead to improvement, that is: equality superclasses or
288        superclasses with functional dependencies.
289
290        We deal with (2) completely independently in TcSimplify. See
291        Note [Minimize by SuperClasses] in TcSimplify.
292
293
294        Moreover, in all cases the extra improvement constraints are
295        Derived. Derived constraints have an identity (for now), but
296        we don't do anything with their evidence. For instance they
297        are never used to rewrite other constraints.
298
299        See also [New Wanted Superclass Work] in TcInteract.
300
301
302 For Deriveds:
303        We do nothing.
304
305 Here's an example that demonstrates why we chose to NOT add
306 superclasses during simplification: [Comes from ticket #4497]
307
308    class Num (RealOf t) => Normed t
309    type family RealOf x
310
311 Assume the generated wanted constraint is:
312    RealOf e ~ e, Normed e
313 If we were to be adding the superclasses during simplification we'd get:
314    Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
315 ==>
316    e ~ uf, Num uf, Normed e, RealOf e ~ e
317 ==> [Spontaneous solve]
318    Num uf, Normed uf, RealOf uf ~ uf
319
320 While looks exactly like our original constraint. If we add the superclass again we'd loop.
321 By adding superclasses definitely only once, during canonicalisation, this situation can't
322 happen.
323
324 \begin{code}
325 newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
326 -- Returns superclasses, see Note [Adding superclasses]
327 newSCWorkFromFlavored flavor cls xis
328   | isDerived flavor
329   = return ()  -- Deriveds don't yield more superclasses because we will
330                -- add them transitively in the case of wanteds.
331
332   | isGiven flavor
333   = do { let sc_theta = immSuperClasses cls xis
334              xev_decomp x = zipWith (\_ i -> EvSuperClass x i) sc_theta [0..]
335              xev = XEvTerm { ev_preds  =  sc_theta
336                            , ev_comp   = panic "Can't compose for given!"
337                            , ev_decomp = xev_decomp }
338        ; ctevs <- xCtEvidence flavor xev
339        ; emitWorkNC ctevs }
340
341   | isEmptyVarSet (tyVarsOfTypes xis)
342   = return () -- Wanteds with no variables yield no deriveds.
343               -- See Note [Improvement from Ground Wanteds]
344
345   | otherwise -- Wanted case, just add those SC that can lead to improvement.
346   = do { let sc_rec_theta = transSuperClasses cls xis
347              impr_theta   = filter is_improvement_pty sc_rec_theta
348              loc          = ctev_loc flavor
349        ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
350        ; mb_der_evs <- mapM (newDerived loc) impr_theta
351        ; emitWorkNC (catMaybes mb_der_evs) }
352
353 is_improvement_pty :: PredType -> Bool
354 -- Either it's an equality, or has some functional dependency
355 is_improvement_pty ty = go (classifyPredType ty)
356   where
357     go (EqPred {})         = True
358     go (ClassPred cls _tys) = not $ null fundeps
359       where (_,fundeps) = classTvsFds cls
360     go (TuplePred ts)      = any is_improvement_pty ts
361     go (IrredPred {})      = True -- Might have equalities after reduction?
362 \end{code}
363
364
365 %************************************************************************
366 %*                                                                      *
367 %*                      Irreducibles canonicalization
368 %*                                                                      *
369 %************************************************************************
370
371
372 \begin{code}
373 canIrred :: CtEvidence -> TcS StopOrContinue
374 -- Precondition: ty not a tuple and no other evidence form
375 canIrred old_ev
376   = do { let old_ty = ctEvPred old_ev
377        ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
378        ; (xi,co) <- flatten FMFullFlatten old_ev old_ty -- co :: xi ~ old_ty
379        ; mb <- rewriteEvidence old_ev xi co
380        ; case mb of {
381              Nothing     -> return Stop ;
382              Just new_ev ->
383
384     do { -- Re-classify, in case flattening has improved its shape
385        ; case classifyPredType (ctEvPred new_ev) of
386            ClassPred cls tys -> canClassNC new_ev cls tys
387            TuplePred tys     -> canTuple   new_ev tys
388            EqPred ty1 ty2    -> canEqNC new_ev ty1 ty2
389            _                 -> continueWith $
390                                 CIrredEvCan { cc_ev = new_ev } } } }
391
392 canHole :: CtEvidence -> OccName -> TcS StopOrContinue
393 canHole ev occ
394   = do { let ty = ctEvPred ev
395        ; (xi,co) <- flatten FMFullFlatten ev ty -- co :: xi ~ ty
396        ; mb <- rewriteEvidence ev xi co
397        ; case mb of
398              Just new_ev -> emitInsoluble (CHoleCan { cc_ev = new_ev, cc_occ = occ })
399              Nothing     -> return ()   -- Found a cached copy; won't happen
400        ; return Stop }
401 \end{code}
402
403 %************************************************************************
404 %*                                                                      *
405 %*        Flattening (eliminating all function symbols)                 *
406 %*                                                                      *
407 %************************************************************************
408
409 Note [Flattening]
410 ~~~~~~~~~~~~~~~~~~~~
411   flatten ty  ==>   (xi, cc)
412     where
413       xi has no type functions, unless they appear under ForAlls
414
415       cc = Auxiliary given (equality) constraints constraining
416            the fresh type variables in xi.  Evidence for these
417            is always the identity coercion, because internally the
418            fresh flattening skolem variables are actually identified
419            with the types they have been generated to stand in for.
420
421 Note that it is flatten's job to flatten *every type function it sees*.
422 flatten is only called on *arguments* to type functions, by canEqGiven.
423
424 Recall that in comments we use alpha[flat = ty] to represent a
425 flattening skolem variable alpha which has been generated to stand in
426 for ty.
427
428 ----- Example of flattening a constraint: ------
429   flatten (List (F (G Int)))  ==>  (xi, cc)
430     where
431       xi  = List alpha
432       cc  = { G Int ~ beta[flat = G Int],
433               F beta ~ alpha[flat = F beta] }
434 Here
435   * alpha and beta are 'flattening skolem variables'.
436   * All the constraints in cc are 'given', and all their coercion terms
437     are the identity.
438
439 NB: Flattening Skolems only occur in canonical constraints, which
440 are never zonked, so we don't need to worry about zonking doing
441 accidental unflattening.
442
443 Note that we prefer to leave type synonyms unexpanded when possible,
444 so when the flattener encounters one, it first asks whether its
445 transitive expansion contains any type function applications.  If so,
446 it expands the synonym and proceeds; if not, it simply returns the
447 unexpanded synonym.
448
449 \begin{code}
450 data FlattenMode = FMSubstOnly | FMFullFlatten
451                    -- See Note [Flattening under a forall]
452
453 -- Flatten a bunch of types all at once.
454 flattenMany ::  FlattenMode
455             -> CtEvidence
456             -> [Type] -> TcS ([Xi], [TcCoercion])
457 -- Coercions :: Xi ~ Type
458 -- Returns True iff (no flattening happened)
459 -- NB: The EvVar inside the 'ctxt :: CtEvidence' is unused,
460 --     we merely want (a) Given/Solved/Derived/Wanted info
461 --                    (b) the GivenLoc/WantedLoc for when we create new evidence
462 flattenMany f ctxt tys
463   = -- pprTrace "flattenMany" empty $
464     go tys
465   where go []       = return ([],[])
466         go (ty:tys) = do { (xi,co)    <- flatten f ctxt ty
467                          ; (xis,cos)  <- go tys
468                          ; return (xi:xis,co:cos) }
469
470 flatten :: FlattenMode
471         -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
472 -- Flatten a type to get rid of type function applications, returning
473 -- the new type-function-free type, and a collection of new equality
474 -- constraints.  See Note [Flattening] for more detail.
475 --
476 -- Postcondition: Coercion :: Xi ~ TcType
477
478 flatten f ctxt ty
479   | Just ty' <- tcView ty
480   = do { (xi, co) <- flatten f ctxt ty'
481        ; if xi `tcEqType` ty' then return (ty,co) 
482                               else return (xi,co) }
483        -- Small tweak for better error messages
484        -- by preserving type synonyms where possible
485
486 flatten _ _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
487
488 flatten f ctxt (TyVarTy tv)
489   = flattenTyVar f ctxt tv
490
491 flatten f ctxt (AppTy ty1 ty2)
492   = do { (xi1,co1) <- flatten f ctxt ty1
493        ; (xi2,co2) <- flatten f ctxt ty2
494        ; traceTcS "flatten/appty" (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$ ppr co1 $$ ppr xi2 $$ ppr co2)
495        ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
496
497 flatten f ctxt (FunTy ty1 ty2)
498   = do { (xi1,co1) <- flatten f ctxt ty1
499        ; (xi2,co2) <- flatten f ctxt ty2
500        ; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
501
502 flatten f ctxt (TyConApp tc tys)
503   -- For a normal type constructor or data family application,
504   -- we just recursively flatten the arguments.
505   | not (isSynFamilyTyCon tc)
506     = do { (xis,cos) <- flattenMany f ctxt tys
507          ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
508
509   -- Otherwise, it's a type function application, and we have to
510   -- flatten it away as well, and generate a new given equality constraint
511   -- between the application and a newly generated flattening skolem variable.
512   | otherwise
513   = ASSERT( tyConArity tc <= length tys )       -- Type functions are saturated
514       do { (xis, cos) <- flattenMany f ctxt tys
515          ; let (xi_args,  xi_rest)  = splitAt (tyConArity tc) xis
516                (cos_args, cos_rest) = splitAt (tyConArity tc) cos
517                  -- The type function might be *over* saturated
518                  -- in which case the remaining arguments should
519                  -- be dealt with by AppTys
520
521          ; (rhs_xi, ret_co) <- flattenNestedFamApp f ctxt tc xi_args
522
523                   -- Emit the flat constraints
524          ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
525                                             --    cf Trac #5655
526                   , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo Nominal tc cos_args) $
527                     cos_rest
528                   )
529          }
530
531 flatten _f ctxt ty@(ForAllTy {})
532 -- We allow for-alls when, but only when, no type function
533 -- applications inside the forall involve the bound type variables.
534   = do { let (tvs, rho) = splitForAllTys ty
535        ; (rho', co) <- flatten FMSubstOnly ctxt rho
536                          -- Substitute only under a forall
537                          -- See Note [Flattening under a forall]
538        ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
539 \end{code}
540
541 Note [Flattening under a forall]
542 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
543 Under a forall, we
544   (a) MUST apply the inert subsitution
545   (b) MUST NOT flatten type family applications
546 Hence FMSubstOnly.
547
548 For (a) consider   c ~ a, a ~ T (forall b. (b, [c])
549 If we don't apply the c~a substitution to the second constraint
550 we won't see the occurs-check error.
551
552 For (b) consider  (a ~ forall b. F a b), we don't want to flatten
553 to     (a ~ forall b.fsk, F a b ~ fsk)
554 because now the 'b' has escaped its scope.  We'd have to flatten to
555        (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
556 and we have not begun to think about how to make that work!
557
558 \begin{code}
559 flattenNestedFamApp :: FlattenMode -> CtEvidence
560                     -> TyCon -> [TcType]   -- Exactly-saturated type function application
561                     -> TcS (Xi, TcCoercion)
562 flattenNestedFamApp FMSubstOnly _ tc xi_args
563   = do { let fam_ty = mkTyConApp tc xi_args
564        ; return (fam_ty, mkTcNomReflCo fam_ty) }
565
566 flattenNestedFamApp FMFullFlatten ctxt tc xi_args  -- Eactly saturated
567   = do { let fam_ty = mkTyConApp tc xi_args
568        ; mb_ct <- lookupFlatEqn tc xi_args
569        ; case mb_ct of
570            Just (ctev, rhs_ty)
571              | ctev `canRewriteOrSame `ctxt    -- Must allow [W]/[W]
572              -> -- You may think that we can just return (cc_rhs ct) but not so.
573                 --            return (mkTcCoVarCo (ctId ct), cc_rhs ct, [])
574                 -- The cached constraint resides in the cache so we have to flatten
575                 -- the rhs to make sure we have applied any inert substitution to it.
576                 -- Alternatively we could be applying the inert substitution to the
577                 -- cache as well when we interact an equality with the inert.
578                 -- The design choice is: do we keep the flat cache rewritten or not?
579                 -- For now I say we don't keep it fully rewritten.
580                do { (rhs_xi,co) <- flatten FMFullFlatten ctev rhs_ty
581                   ; let final_co = evTermCoercion (ctEvTerm ctev)
582                                    `mkTcTransCo` mkTcSymCo co
583                   ; traceTcS "flatten/flat-cache hit" $ (ppr ctev $$ ppr rhs_xi $$ ppr final_co)
584                   ; return (rhs_xi, final_co) }
585
586            _ -> do { (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty
587                    ; extendFlatCache tc xi_args ctev rhs_xi
588
589                    -- The new constraint (F xi_args ~ rhs_xi) is not necessarily inert
590                    -- (e.g. the LHS may be a redex) so we must put it in the work list
591                    ; let ct = CFunEqCan { cc_ev     = ctev
592                                         , cc_fun    = tc
593                                         , cc_tyargs = xi_args
594                                         , cc_rhs    = rhs_xi }
595                    ; updWorkListTcS $ extendWorkListFunEq ct
596
597                    ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr rhs_xi $$ ppr ctev)
598                    ; return (rhs_xi, evTermCoercion (ctEvTerm ctev)) }
599        }
600 \end{code}
601
602 \begin{code}
603 flattenTyVar :: FlattenMode -> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
604 -- "Flattening" a type variable means to apply the substitution to it
605 -- The substitution is actually the union of the substitution in the TyBinds
606 -- for the unification variables that have been unified already with the inert
607 -- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract.
608 --
609 -- Postcondition: co : xi ~ tv
610 flattenTyVar f ctxt tv
611   = do { mb_yes <- flattenTyVarOuter f ctxt tv
612        ; case mb_yes of
613            Left tv'         -> -- Done 
614                                do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv'))
615                                   ; return (ty', mkTcNomReflCo ty') }
616                             where
617                                ty' = mkTyVarTy tv'
618
619            Right (ty1, co1) -> -- Recurse
620                                do { (ty2, co2) <- flatten f ctxt ty1
621                                   ; traceTcS "flattenTyVar2" (ppr tv $$ ppr ty2)
622                                   ; return (ty2, co2 `mkTcTransCo` co1) }
623        }
624
625 flattenTyVarOuter, flattenTyVarFinal 
626    :: FlattenMode -> CtEvidence
627    -> TcTyVar 
628    -> TcS (Either TyVar (TcType, TcCoercion))
629 -- Look up the tyvar in 
630 --   a) the internal MetaTyVar box
631 --   b) the tyvar binds 
632 --   c) the inerts
633 -- Return (Left tv')       if it is not found, tv' has a properly zonked kind
634 --        (Right (ty, co)) if found, with co :: ty ~ tv
635 --                         NB: in the latter case ty is not necessarily flattened
636
637 flattenTyVarOuter f ctxt tv
638   | not (isTcTyVar tv)            -- Happens when flatten under a (forall a. ty)
639   = flattenTyVarFinal f ctxt tv   -- So ty contains refernces to the non-TcTyVar a
640   | otherwise
641   = do { mb_ty <- isFilledMetaTyVar_maybe tv
642        ; case mb_ty of {
643            Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
644                          ; return (Right (ty, mkTcNomReflCo ty)) } ;
645            Nothing ->
646
647     -- Try in ty_binds
648     do { ty_binds <- getTcSTyBindsMap
649        ; case lookupVarEnv ty_binds tv of {
650            Just (_tv,ty) -> do { traceTcS "Following bound tyvar" (ppr tv <+> equals <+> ppr ty)
651                                ; return (Right (ty, mkTcNomReflCo ty)) } ;
652                                  -- NB: ty_binds coercions are all ReflCo,
653            Nothing ->
654
655     -- Try in the inert equalities
656     do { ieqs <- getInertEqs
657        ; case lookupVarEnv ieqs tv of
658            Just (ct:_)                      -- If the first doesn't work,
659              | let ctev   = ctEvidence ct   -- the subsequent ones won't either
660                    rhs_ty = cc_rhs ct
661              , ctev `canRewrite` ctxt 
662              ->  do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
663                     ; return (Right (rhs_ty, mkTcSymCo (evTermCoercion (ctEvTerm ctev)))) }
664                     -- NB: even if ct is Derived we are not going to
665                     -- touch the actual coercion so we are fine.
666
667            _other -> flattenTyVarFinal f ctxt tv
668     } } } } }
669
670 flattenTyVarFinal f ctxt tv
671   = -- Done, but make sure the kind is zonked
672     do { let knd = tyVarKind tv
673        ; (new_knd, _kind_co) <- flatten f ctxt knd
674        ; return (Left (setVarType tv new_knd)) }
675 \end{code}
676
677 Note [Non-idempotent inert substitution]
678 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
679
680 The inert substitution is not idempotent in the broad sense. It is only idempotent in
681 that it cannot rewrite the RHS of other inert equalities any further. An example of such
682 an inert substitution is:
683
684  [G] g1 : ta8 ~ ta4
685  [W] g2 : ta4 ~ a5Fj
686
687 Observe that the wanted cannot rewrite the solved goal, despite the fact that ta4 appears on
688 an RHS of an equality. Now, imagine a constraint:
689
690  [W] g3: ta8 ~ Int
691
692 coming in. If we simply apply once the inert substitution we will get:
693
694  [W] g3_1: ta4 ~ Int
695
696 and because potentially ta4 is untouchable we will try to insert g3_1 in the inert set,
697 getting a panic since the inert only allows ONE equation per LHS type variable (as it
698 should).
699
700 For this reason, when we reach to flatten a type variable, we flatten it recursively,
701 so that we can make sure that the inert substitution /is/ fully applied.
702
703 Insufficient (non-recursive) rewriting was the reason for #5668.
704
705
706 %************************************************************************
707 %*                                                                      *
708 %*        Equalities
709 %*                                                                      *
710 %************************************************************************
711
712 \begin{code}
713 canEvVarsCreated :: [CtEvidence] -> TcS StopOrContinue
714 canEvVarsCreated [] = return Stop
715     -- Add all but one to the work list
716     -- and return the first (if any) for futher processing
717 canEvVarsCreated (ev : evs)
718   = do { emitWorkNC evs; canEvNC ev }
719           -- Note the "NC": these are fresh goals, not necessarily canonical
720
721 emitWorkNC :: [CtEvidence] -> TcS ()
722 emitWorkNC evs
723   | null evs  = return ()
724   | otherwise = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
725                    ; updWorkListTcS (extendWorkListCts (map mk_nc evs)) }
726   where
727     mk_nc ev = mkNonCanonical ev
728
729 -------------------------
730 canEqNC :: CtEvidence -> Type -> Type -> TcS StopOrContinue
731 canEqNC ev ty1 ty2 = can_eq_nc ev ty1 ty1 ty2 ty2
732
733
734 can_eq_nc, can_eq_nc' 
735    :: CtEvidence 
736    -> Type -> Type    -- LHS, after and before type-synonym expansion, resp 
737    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp 
738    -> TcS StopOrContinue
739
740 can_eq_nc ev ty1 ps_ty1 ty2 ps_ty2
741   = do { traceTcS "can_eq_nc" $ 
742          vcat [ ppr ev, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
743        ; can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2 }
744
745 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
746 can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2
747   | Just ty1' <- tcView ty1 = can_eq_nc ev ty1' ps_ty1 ty2  ps_ty2
748   | Just ty2' <- tcView ty2 = can_eq_nc ev ty1  ps_ty1 ty2' ps_ty2
749
750 -- Type family on LHS or RHS take priority
751 can_eq_nc' ev (TyConApp fn tys) _ ty2 ps_ty2
752   | isSynFamilyTyCon fn
753   = canEqLeafFun ev NotSwapped fn tys ty2 ps_ty2
754 can_eq_nc' ev ty1 ps_ty1 (TyConApp fn tys) _
755   | isSynFamilyTyCon fn
756   = canEqLeafFun ev IsSwapped fn tys ty1 ps_ty1
757
758 -- Type variable on LHS or RHS are next
759 can_eq_nc' ev (TyVarTy tv1) _ ty2 ps_ty2
760   = canEqTyVar ev NotSwapped tv1 ty2 ps_ty2
761 can_eq_nc' ev ty1 ps_ty1 (TyVarTy tv2) _
762   = canEqTyVar ev IsSwapped tv2 ty1 ps_ty1
763
764 ----------------------
765 -- Otherwise try to decompose
766 ----------------------
767
768 -- Literals
769 can_eq_nc' ev ty1@(LitTy l1) _ (LitTy l2) _
770  | l1 == l2
771   = do { when (isWanted ev) $
772          setEvBind (ctev_evar ev) (EvCoercion (mkTcNomReflCo ty1))
773        ; return Stop }
774
775 -- Decomposable type constructor applications 
776 -- Synonyms and type functions (which are not decomposable)
777 -- have already been dealt with 
778 can_eq_nc' ev (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
779   | isDecomposableTyCon tc1
780   , isDecomposableTyCon tc2
781   = canDecomposableTyConApp ev tc1 tys1 tc2 tys2
782
783 can_eq_nc' ev (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
784   | isDecomposableTyCon tc1 
785       -- The guard is important
786       -- e.g.  (x -> y) ~ (F x y) where F has arity 1
787       --       should not fail, but get the app/app case
788   = canEqFailure ev ps_ty1 ps_ty2
789
790 can_eq_nc' ev (FunTy s1 t1) _ (FunTy s2 t2) _
791   = canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2]
792
793 can_eq_nc' ev (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
794   | isDecomposableTyCon tc2 
795   = canEqFailure ev ps_ty1 ps_ty2
796
797 can_eq_nc' ev s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
798  | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
799  = do { let (tvs1,body1) = tcSplitForAllTys s1
800             (tvs2,body2) = tcSplitForAllTys s2
801       ; if not (equalLength tvs1 tvs2) then
802           canEqFailure ev s1 s2
803         else
804           do { traceTcS "Creating implication for polytype equality" $ ppr ev
805              ; ev_term <- deferTcSForAllEq Nominal loc (tvs1,body1) (tvs2,body2)
806              ; setEvBind orig_ev ev_term
807              ; return Stop } }
808  | otherwise
809  = do { traceTcS "Ommitting decomposition of given polytype equality" $
810         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
811       ; return Stop }
812
813 can_eq_nc' ev (AppTy s1 t1) ps_ty1 ty2 ps_ty2
814   = can_eq_app ev NotSwapped s1 t1 ps_ty1 ty2 ps_ty2
815 can_eq_nc' ev ty1 ps_ty1 (AppTy s2 t2) ps_ty2
816   = can_eq_app ev IsSwapped s2 t2 ps_ty2 ty1 ps_ty1
817
818 -- Everything else is a definite type error, eg LitTy ~ TyConApp
819 can_eq_nc' ev _ ps_ty1 _ ps_ty2
820   = canEqFailure ev ps_ty1 ps_ty2
821
822 ------------
823 can_eq_app, can_eq_flat_app
824     :: CtEvidence -> SwapFlag
825     -> Type -> Type -> Type  -- LHS (s1 t2), after and before type-synonym expansion, resp 
826     -> Type -> Type          -- RHS (ty2),   after and before type-synonym expansion, resp 
827     -> TcS StopOrContinue
828 -- See Note [Canonicalising type applications]
829 can_eq_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
830   =  do { traceTcS "can_eq_app 1" $
831           vcat [ ppr ev, ppr swapped, ppr s1, ppr t1, ppr ty2 ]
832         ; (xi_s1, co_s1) <- flatten FMSubstOnly ev s1
833         ; traceTcS "can_eq_app 2" $ vcat [ ppr ev, ppr xi_s1 ]
834         ; if s1 `tcEqType` xi_s1
835           then can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
836           else
837      do { (xi_t1, co_t1) <- flatten FMSubstOnly ev t1
838              -- We flatten t1 as well so that (xi_s1 xi_t1) is well-kinded
839              -- If we form (xi_s1 t1) that might (appear) ill-kinded, 
840              -- and then crash in a call to typeKind
841         ; let xi1 = mkAppTy xi_s1 xi_t1
842               co1 = mkTcAppCo co_s1 co_t1
843         ; traceTcS "can_eq_app 3" $ vcat [ ppr ev, ppr xi1, ppr co1 ]
844         ; mb_ct <- rewriteEqEvidence ev swapped xi1 ps_ty2 
845                                      co1 (mkTcNomReflCo ps_ty2)
846         ; traceTcS "can_eq_app 4" $ vcat [ ppr ev, ppr xi1, ppr co1 ]
847         ; case mb_ct of
848            Nothing     -> return Stop
849            Just new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }}
850
851 -- Preconditions: s1  is already flattened
852 --                ty2 is not a type variable, so flattening
853 --                    can't turn it into an application if it
854 --                    doesn't look like one already
855 -- See Note [Canonicalising type applications]
856 can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
857   | Just (s2,t2) <- tcSplitAppTy_maybe ty2
858   = unSwap swapped decompose_it (s1,t1) (s2,t2)
859   | otherwise
860   = unSwap swapped (canEqFailure ev) ps_ty1 ps_ty2
861   where
862     decompose_it (s1,t1) (s2,t2) 
863       = do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
864                  xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
865                  xevdecomp x = let xco = evTermCoercion x
866                                in [ EvCoercion (mkTcLRCo CLeft xco)
867                                   , EvCoercion (mkTcLRCo CRight xco)]
868            ; ctevs <- xCtEvidence ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp)
869            ; canEvVarsCreated ctevs }
870
871
872 ------------------------
873 canDecomposableTyConApp :: CtEvidence
874                         -> TyCon -> [TcType]
875                         -> TyCon -> [TcType]
876                         -> TcS StopOrContinue
877 canDecomposableTyConApp ev tc1 tys1 tc2 tys2
878   | tc1 /= tc2 || length tys1 /= length tys2
879     -- Fail straight away for better error messages
880   = canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
881   | otherwise
882   = do { traceTcS "canDecomposableTyConApp" (ppr ev $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
883        ; canDecomposableTyConAppOK ev tc1 tys1 tys2 }
884
885 canDecomposableTyConAppOK :: CtEvidence
886                           -> TyCon -> [TcType] -> [TcType]
887                           -> TcS StopOrContinue
888
889 canDecomposableTyConAppOK ev tc1 tys1 tys2
890   = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
891              xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
892              xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
893        ; ctevs <- xCtEvidence ev xev
894        ; canEvVarsCreated ctevs }
895
896 canEqFailure :: CtEvidence -> TcType -> TcType -> TcS StopOrContinue
897 -- See Note [Make sure that insolubles are fully rewritten]
898 canEqFailure ev ty1 ty2
899   = do { (s1, co1) <- flatten FMSubstOnly ev ty1
900        ; (s2, co2) <- flatten FMSubstOnly ev ty2
901        ; mb_ct <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
902        ; case mb_ct of
903            Just new_ev -> emitInsoluble (mkNonCanonical new_ev)
904            Nothing -> pprPanic "canEqFailure" (ppr ev $$ ppr ty1 $$ ppr ty2)
905        ; return Stop }
906 \end{code}
907
908 Note [Canonicalising type applications]
909 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
910 Given (s1 t1) ~ ty2, how should we proceed?
911 The simple things is to see if ty2 is of form (s2 t2), and 
912 decompose.  By this time s1 and s2 can't be saturated type
913 function applications, because those have been dealt with 
914 by an earlier equation in can_eq_nc, so it is always sound to 
915 decompose.
916
917 However, over-eager decomposition gives bad error messages 
918 for things like
919    a b ~ Maybe c
920    e f ~ p -> q
921 Suppose (in the first example) we already know a~Array.  Then if we
922 decompose the application eagerly, yielding
923    a ~ Maybe
924    b ~ c
925 we get an error        "Can't match Array ~ Maybe", 
926 but we'd prefer to get "Can't match Array b ~ Maybe c".
927
928 So instead can_eq_app flattens s1.  If flattening does something, it
929 rewrites, and goes round can_eq_nc again.  If flattening 
930 does nothing, then (at least with our present state of knowledge)
931 we can only decompose, and that is what can_eq_flat_app attempts
932 to do. 
933
934 Note [Make sure that insolubles are fully rewritten]
935 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
936 When an equality fails, we still want to rewrite the equality
937 all the way down, so that it accurately reflects
938  (a) the mutable reference substitution in force at start of solving
939  (b) any ty-binds in force at this point in solving
940 See Note [Kick out insolubles] in TcInteract.
941 And if we don't do this there is a bad danger that
942 TcSimplify.applyTyVarDefaulting will find a variable
943 that has in fact been substituted.
944
945 Note [Do not decompose Given polytype equalities]
946 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
947 Consider [G] (forall a. t1 ~ forall a. t2).  Can we decompose this?
948 No -- what would the evidence look like?  So instead we simply discard
949 this given evidence.
950
951
952 Note [Combining insoluble constraints]
953 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
954 As this point we have an insoluble constraint, like Int~Bool.
955
956  * If it is Wanted, delete it from the cache, so that subsequent
957    Int~Bool constraints give rise to separate error messages
958
959  * But if it is Derived, DO NOT delete from cache.  A class constraint
960    may get kicked out of the inert set, and then have its functional
961    dependency Derived constraints generated a second time. In that
962    case we don't want to get two (or more) error messages by
963    generating two (or more) insoluble fundep constraints from the same
964    class constraint.
965
966
967 Note [Canonical ordering for equality constraints]
968 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
969 Implemented as (<+=) below:
970
971   - Type function applications always come before anything else.
972   - Variables always come before non-variables (other than type
973       function applications).
974
975 Note that we don't need to unfold type synonyms on the RHS to check
976 the ordering; that is, in the rules above it's OK to consider only
977 whether something is *syntactically* a type function application or
978 not.  To illustrate why this is OK, suppose we have an equality of the
979 form 'tv ~ S a b c', where S is a type synonym which expands to a
980 top-level application of the type function F, something like
981
982   type S a b c = F d e
983
984 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
985 expansion contains type function applications the flattener will do
986 the expansion and then generate a skolem variable for the type
987 function application, so we end up with something like this:
988
989   tv ~ x
990   F d e ~ x
991
992 where x is the skolem variable.  This is one extra equation than
993 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
994 if we had noticed that S expanded to a top-level type function
995 application and flipped it around in the first place) but this way
996 keeps the code simpler.
997
998 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
999 ordering of tv ~ tv constraints.  There are several reasons why we
1000 might:
1001
1002   (1) In order to be able to extract a substitution that doesn't
1003       mention untouchable variables after we are done solving, we might
1004       prefer to put touchable variables on the left. However, in and
1005       of itself this isn't necessary; we can always re-orient equality
1006       constraints at the end if necessary when extracting a substitution.
1007
1008   (2) To ensure termination we might think it necessary to put
1009       variables in lexicographic order. However, this isn't actually
1010       necessary as outlined below.
1011
1012 While building up an inert set of canonical constraints, we maintain
1013 the invariant that the equality constraints in the inert set form an
1014 acyclic rewrite system when viewed as L-R rewrite rules.  Moreover,
1015 the given constraints form an idempotent substitution (i.e. none of
1016 the variables on the LHS occur in any of the RHS's, and type functions
1017 never show up in the RHS at all), the wanted constraints also form an
1018 idempotent substitution, and finally the LHS of a given constraint
1019 never shows up on the RHS of a wanted constraint.  There may, however,
1020 be a wanted LHS that shows up in a given RHS, since we do not rewrite
1021 given constraints with wanted constraints.
1022
1023 Suppose we have an inert constraint set
1024
1025
1026   tg_1 ~ xig_1         -- givens
1027   tg_2 ~ xig_2
1028   ...
1029   tw_1 ~ xiw_1         -- wanteds
1030   tw_2 ~ xiw_2
1031   ...
1032
1033 where each t_i can be either a type variable or a type function
1034 application. Now suppose we take a new canonical equality constraint,
1035 t' ~ xi' (note among other things this means t' does not occur in xi')
1036 and try to react it with the existing inert set.  We show by induction
1037 on the number of t_i which occur in t' ~ xi' that this process will
1038 terminate.
1039
1040 There are several ways t' ~ xi' could react with an existing constraint:
1041
1042 TODO: finish this proof.  The below was for the case where the entire
1043 inert set is an idempotent subustitution...
1044
1045 (b) We could have t' = t_j for some j.  Then we obtain the new
1046     equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j.  We
1047     now canonicalize the new equality, which may involve decomposing it
1048     into several canonical equalities, and recurse on these.  However,
1049     none of the new equalities will contain t_j, so they have fewer
1050     occurrences of the t_i than the original equation.
1051
1052 (a) We could have t_j occurring in xi' for some j, with t' /=
1053     t_j. Then we substitute xi_j for t_j in xi' and continue.  However,
1054     since none of the t_i occur in xi_j, we have decreased the
1055     number of t_i that occur in xi', since we eliminated t_j and did not
1056     introduce any new ones.
1057
1058 \begin{code}
1059 canEqLeafFun :: CtEvidence 
1060              -> SwapFlag
1061              -> TyCon -> [TcType]   -- LHS
1062              -> TcType -> TcType    -- RHS
1063              -> TcS StopOrContinue
1064 canEqLeafFun ev swapped fn tys1 ty2 ps_ty2
1065   | length tys1 > tyConArity fn
1066   = -- Over-saturated type function on LHS: 
1067     -- flatten LHS, leaving an AppTy, and go around again
1068     do { (xi1, co1) <- flatten FMFullFlatten ev (mkTyConApp fn tys1)
1069        ; mb <- rewriteEqEvidence ev swapped xi1 ps_ty2 
1070                                  co1 (mkTcNomReflCo ps_ty2)
1071        ; case mb of
1072             Nothing     -> return Stop
1073             Just new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }
1074
1075   | otherwise
1076   = -- ev :: F tys1 ~ ty2,   if not swapped
1077     -- ev :: ty2 ~ F tys1,   if swapped                                    
1078     ASSERT( length tys1 == tyConArity fn )  
1079         -- Type functions are never under-saturated
1080         -- Previous equation checks for over-saturation
1081     do { traceTcS "canEqLeafFun" $ pprEq (mkTyConApp fn tys1) ps_ty2
1082
1083             -- Flatten type function arguments
1084             -- cos1 :: xis1 ~ tys1
1085             -- co2  :: xi2 ~ ty2
1086       ; (xis1,cos1) <- flattenMany FMFullFlatten ev tys1
1087       ; (xi2, co2)  <- flatten     FMFullFlatten ev ps_ty2
1088
1089        ; let fam_head = mkTyConApp fn xis1
1090              co1      = mkTcTyConAppCo Nominal fn cos1
1091        ; mb <- rewriteEqEvidence ev swapped fam_head xi2 co1 co2
1092
1093        ; let k1 = typeKind fam_head
1094              k2 = typeKind xi2
1095        ; case mb of
1096             Nothing     -> return Stop
1097             Just new_ev | k1 `isSubKind` k2
1098                         -- Establish CFunEqCan kind invariant
1099                         -> continueWith (CFunEqCan { cc_ev = new_ev, cc_fun = fn
1100                                                    , cc_tyargs = xis1, cc_rhs = xi2 })
1101                         | otherwise
1102                         -> checkKind new_ev fam_head k1 xi2 k2 }
1103
1104 ---------------------
1105 canEqTyVar :: CtEvidence -> SwapFlag
1106            -> TcTyVar 
1107            -> TcType -> TcType
1108            -> TcS StopOrContinue
1109 -- A TyVar on LHS, but so far un-zonked
1110 canEqTyVar ev swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
1111   = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
1112        ; mb_yes <- flattenTyVarOuter FMFullFlatten ev tv1 
1113        ; case mb_yes of
1114            Right (ty1, co1) -> -- co1 :: ty1 ~ tv1
1115                                do { mb <- rewriteEqEvidence ev swapped  ty1 ps_ty2
1116                                                             co1 (mkTcNomReflCo ps_ty2)
1117                                   ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1,
1118                                                                   ppUnless (isDerived ev) (ppr co1)])
1119                                   ; case mb of
1120                                       Nothing     -> return Stop
1121                                       Just new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 }
1122
1123            Left tv1' -> do { (xi2, co2) <- flatten FMFullFlatten ev ps_ty2 -- co2 :: xi2 ~ ps_ty2
1124                                            -- Use ps_ty2 to preserve type synonyms if poss
1125                            ; dflags <- getDynFlags
1126                            ; canEqTyVar2 dflags ev swapped tv1' xi2 co2 } }
1127
1128 canEqTyVar2 :: DynFlags
1129             -> CtEvidence   -- olhs ~ orhs (or, if swapped, orhs ~ olhs)
1130             -> SwapFlag
1131             -> TcTyVar      -- olhs
1132             -> TcType       -- nrhs
1133             -> TcCoercion   -- nrhs ~ orhs
1134             -> TcS StopOrContinue
1135 -- LHS is an inert type variable, 
1136 -- and RHS is fully rewritten, but with type synonyms
1137 -- preserved as much as possible
1138
1139 canEqTyVar2 dflags ev swapped tv1 xi2 co2
1140   | Just tv2 <- getTyVar_maybe xi2
1141   = canEqTyVarTyVar ev swapped tv1 tv2 co2
1142
1143   | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2  -- No occurs check
1144   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2' co1 co2
1145                 -- Ensure that the new goal has enough type synonyms
1146                 -- expanded by the occurCheckExpand; hence using xi2' here
1147                 -- See Note [occurCheckExpand]
1148
1149        ; let k1 = tyVarKind tv1
1150              k2 = typeKind xi2'
1151        ; case mb of
1152             Nothing     -> return Stop
1153             Just new_ev | k2 `isSubKind` k1
1154                         -- Establish CTyEqCan kind invariant
1155                         -- Reorientation has done its best, but the kinds might
1156                         -- simply be incompatible
1157                         -> continueWith (CTyEqCan { cc_ev = new_ev
1158                                                   , cc_tyvar  = tv1, cc_rhs = xi2' })
1159                         | otherwise
1160                         -> checkKind new_ev xi1 k1 xi2' k2 }
1161
1162   | otherwise  -- Occurs check error
1163   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2
1164        ; case mb of
1165            Nothing     -> return ()
1166            Just new_ev -> emitInsoluble (mkNonCanonical new_ev)
1167        ; return Stop }
1168   where
1169     xi1 = mkTyVarTy tv1
1170     co1 = mkTcNomReflCo xi1
1171
1172
1173 canEqTyVarTyVar :: CtEvidence       -- tv1 ~ orhs (or orhs ~ tv1, if swapped)
1174                 -> SwapFlag
1175                 -> TyVar -> TyVar   -- tv2, tv2
1176                 -> TcCoercion       -- tv2 ~ orhs
1177                 -> TcS StopOrContinue
1178 -- Both LHS and RHS rewrote to a type variable,
1179 canEqTyVarTyVar ev swapped tv1 tv2 co2
1180   | tv1 == tv2
1181   = do { when (isWanted ev) $
1182          ASSERT( tcCoercionRole co2 == Nominal )
1183          setEvBind (ctev_evar ev) (EvCoercion (maybeSym swapped co2))
1184        ; return Stop }  
1185
1186   | reorient_me  -- See note [Canonical ordering for equality constraints].
1187                  -- True => the kinds are compatible, 
1188                  --         so no need for further sub-kind check
1189                  -- If swapped = NotSwapped, then
1190                  --     rw_orhs = tv1, rw_olhs = orhs
1191                  --     rw_nlhs = tv2, rw_nrhs = xi1
1192   = do { mb <- rewriteEqEvidence ev (flipSwap swapped)  xi2 xi1
1193                                  co2 (mkTcNomReflCo xi1)
1194        ; case mb of
1195            Nothing     -> return Stop
1196            Just new_ev -> continueWith (CTyEqCan { cc_ev = new_ev
1197                                                  , cc_tyvar  = tv2, cc_rhs = xi1 }) }
1198
1199   | otherwise
1200   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 
1201                                  (mkTcNomReflCo xi1) co2
1202        ; case mb of
1203            Nothing     -> return Stop
1204            Just new_ev | k2 `isSubKind` k1
1205                        -> continueWith (CTyEqCan { cc_ev = new_ev
1206                                                  , cc_tyvar = tv1, cc_rhs = xi2 })
1207                        | otherwise
1208                        -> checkKind new_ev xi1 k1 xi2 k2 } 
1209   where
1210     reorient_me 
1211       | k1 `tcEqKind` k2    = tv2 `better_than` tv1
1212       | k1 `isSubKind` k2   = True  -- Note [Kind orientation for CTyEqCan]
1213       | otherwise           = False -- in TcRnTypes
1214
1215     xi1 = mkTyVarTy tv1
1216     xi2 = mkTyVarTy tv2
1217     k1  = tyVarKind tv1
1218     k2  = tyVarKind tv2
1219
1220     tv2 `better_than` tv1
1221       | isMetaTyVar tv1     = False   -- Never swap a meta-tyvar
1222       | isFlatSkolTyVar tv1 = isMetaTyVar tv2
1223       | otherwise           = isMetaTyVar tv2 || isFlatSkolTyVar tv2
1224                             -- Note [Eliminate flat-skols]
1225
1226 checkKind :: CtEvidence         -- t1~t2
1227           -> TcType -> TcKind
1228           -> TcType -> TcKind   -- s1~s2, flattened and zonked
1229           -> TcS StopOrContinue
1230 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
1231 --       CIrredEvCan (NOT CTyEqCan or CFunEqCan)
1232 -- for the type equality; and continue with the kind equality constraint.
1233 -- When the latter is solved, it'll kick out the irreducible equality for
1234 -- a second attempt at solving
1235 --
1236 -- See Note [Equalities with incompatible kinds]
1237
1238 checkKind new_ev s1 k1 s2 k2   -- See Note [Equalities with incompatible kinds]
1239   = ASSERT( isKind k1 && isKind k2 )
1240     do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
1241
1242          -- Create a derived kind-equality, and solve it
1243        ; mw <- newDerived kind_co_loc (mkEqPred k1 k2)
1244        ; case mw of
1245            Nothing  -> return ()
1246            Just kev -> emitWorkNC [kev]
1247
1248          -- Put the not-currently-soluble thing into the inert set
1249        ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1250   where
1251     loc = ctev_loc new_ev
1252     kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
1253 \end{code}
1254
1255 Note [Eliminate flat-skols]
1256 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1257 Suppose we have  [G] Num (F [a])
1258 then we flatten to
1259      [G] Num fsk
1260      [G] F [a] ~ fsk
1261 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1262       type instance F [a] = a
1263 then we'll reduce the second constraint to
1264      [G] a ~ fsk
1265 and then replace all uses of 'a' with fsk.  That's bad because
1266 in error messages intead of saying 'a' we'll say (F [a]).  In all
1267 places, including those where the programmer wrote 'a' in the first
1268 place.  Very confusing!  See Trac #7862.
1269
1270 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1271 the fsk.
1272
1273 Note [Equalities with incompatible kinds]
1274 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1275 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1276 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1277 CFunEqCan.  What if we try to unify two things with incompatible
1278 kinds?
1279
1280 eg    a ~ b  where a::*, b::*->*
1281 or    a ~ b  where a::*, b::k, k is a kind variable
1282
1283 The CTyEqCan compatKind invariant is important.  If we make a CTyEqCan
1284 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1285 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1286 Trac #7696).
1287
1288 So instead for these ill-kinded equalities we generate a CIrredCan,
1289 and put it in the inert set, which keeps it out of the way until a
1290 subsequent substitution (on kind variables, say) re-activates it.
1291
1292 NB: it is important that the types s1,s2 are flattened and zonked
1293     so that their kinds k1, k2 are inert wrt the substitution.  That
1294     means that they can only become the same if we change the inert
1295     set, which in turn will kick out the irreducible equality
1296     E.g. it is WRONG to make an irred (a:k1)~(b:k2)
1297          if we already have a substitution k1:=k2
1298
1299 NB: it's important that the new CIrredCan goes in the inert set rather
1300 than back into the work list. We used to do the latter, but that led
1301 to an infinite loop when we encountered it again, and put it back it
1302 the work list again.
1303
1304 See also Note [Kind orientation for CTyEqCan] and
1305          Note [Kind orientation for CFunEqCan] in TcRnTypes
1306
1307 Note [Type synonyms and canonicalization]
1308 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1309 We treat type synonym applications as xi types, that is, they do not
1310 count as type function applications.  However, we do need to be a bit
1311 careful with type synonyms: like type functions they may not be
1312 generative or injective.  However, unlike type functions, they are
1313 parametric, so there is no problem in expanding them whenever we see
1314 them, since we do not need to know anything about their arguments in
1315 order to expand them; this is what justifies not having to treat them
1316 as specially as type function applications.  The thing that causes
1317 some subtleties is that we prefer to leave type synonym applications
1318 *unexpanded* whenever possible, in order to generate better error
1319 messages.
1320
1321 If we encounter an equality constraint with type synonym applications
1322 on both sides, or a type synonym application on one side and some sort
1323 of type application on the other, we simply must expand out the type
1324 synonyms in order to continue decomposing the equality constraint into
1325 primitive equality constraints.  For example, suppose we have
1326
1327   type F a = [Int]
1328
1329 and we encounter the equality
1330
1331   F a ~ [b]
1332
1333 In order to continue we must expand F a into [Int], giving us the
1334 equality
1335
1336   [Int] ~ [b]
1337
1338 which we can then decompose into the more primitive equality
1339 constraint
1340
1341   Int ~ b.
1342
1343 However, if we encounter an equality constraint with a type synonym
1344 application on one side and a variable on the other side, we should
1345 NOT (necessarily) expand the type synonym, since for the purpose of
1346 good error messages we want to leave type synonyms unexpanded as much
1347 as possible.  Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1348
1349
1350 Note [occurCheckExpand]
1351 ~~~~~~~~~~~~~~~~~~~~~~~
1352 There is a subtle point with type synonyms and the occurs check that
1353 takes place for equality constraints of the form tv ~ xi.  As an
1354 example, suppose we have
1355
1356   type F a = Int
1357
1358 and we come across the equality constraint
1359
1360   a ~ F a
1361
1362 This should not actually fail the occurs check, since expanding out
1363 the type synonym results in the legitimate equality constraint a ~
1364 Int.  We must actually do this expansion, because unifying a with F a
1365 will lead the type checker into infinite loops later.  Put another
1366 way, canonical equality constraints should never *syntactically*
1367 contain the LHS variable in the RHS type.  However, we don't always
1368 need to expand type synonyms when doing an occurs check; for example,
1369 the constraint
1370
1371   a ~ F b
1372
1373 is obviously fine no matter what F expands to. And in this case we
1374 would rather unify a with F b (rather than F b's expansion) in order
1375 to get better error messages later.
1376
1377 So, when doing an occurs check with a type synonym application on the
1378 RHS, we use some heuristics to find an expansion of the RHS which does
1379 not contain the variable from the LHS.  In particular, given
1380
1381   a ~ F t1 ... tn
1382
1383 we first try expanding each of the ti to types which no longer contain
1384 a.  If this turns out to be impossible, we next try expanding F
1385 itself, and so on.  See Note [Occurs check expansion] in TcType
1386