Flattener preserves synonyms, rewriteEvidence can drop buggy "optimisation"
[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 _ _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
479
480 flatten f ctxt (TyVarTy tv)
481   = flattenTyVar f ctxt tv
482
483 flatten f ctxt (AppTy ty1 ty2)
484   = do { (xi1,co1) <- flatten f ctxt ty1
485        ; (xi2,co2) <- flatten f ctxt ty2
486        ; traceTcS "flatten/appty" (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$ ppr co1 $$ ppr xi2 $$ ppr co2)
487        ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
488
489 flatten f ctxt (FunTy ty1 ty2)
490   = do { (xi1,co1) <- flatten f ctxt ty1
491        ; (xi2,co2) <- flatten f ctxt ty2
492        ; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
493
494 flatten f ctxt (TyConApp tc tys)
495   -- For * a normal data type application
496   --     * type synonym application  See Note [Flattening synonyms]
497   --     * data family application
498   -- we just recursively flatten the arguments.
499   | not (isSynFamilyTyCon tc)
500     = do { (xis,cos) <- flattenMany f ctxt tys
501          ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
502
503   -- Otherwise, it's a type function application, and we have to
504   -- flatten it away as well, and generate a new given equality constraint
505   -- between the application and a newly generated flattening skolem variable.
506   | otherwise
507   = ASSERT( tyConArity tc <= length tys )       -- Type functions are saturated
508       do { (xis, cos) <- flattenMany f ctxt tys
509          ; let (xi_args,  xi_rest)  = splitAt (tyConArity tc) xis
510                (cos_args, cos_rest) = splitAt (tyConArity tc) cos
511                  -- The type function might be *over* saturated
512                  -- in which case the remaining arguments should
513                  -- be dealt with by AppTys
514
515          ; (rhs_xi, ret_co) <- flattenNestedFamApp f ctxt tc xi_args
516
517                   -- Emit the flat constraints
518          ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
519                                             --    cf Trac #5655
520                   , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo Nominal tc cos_args) $
521                     cos_rest
522                   )
523          }
524
525 flatten _f ctxt ty@(ForAllTy {})
526 -- We allow for-alls when, but only when, no type function
527 -- applications inside the forall involve the bound type variables.
528   = do { let (tvs, rho) = splitForAllTys ty
529        ; (rho', co) <- flatten FMSubstOnly ctxt rho
530                          -- Substitute only under a forall
531                          -- See Note [Flattening under a forall]
532        ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
533 \end{code}
534
535 Note [Flattening synonyms]
536 ~~~~~~~~~~~~~~~~~~~~~~~~~~
537 Suppose
538    type T a = a -> a
539 and we want to flatten the type (T (F a)).  Then we can safely flatten
540 the (F a) to a skolem, and return (T fsk).  We don't need to expand the
541 synonym.  This works because TcTyConAppCo can deal with synonyms
542 (unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
543
544 Not expanding synonyms aggressively improves error messages.
545
546 Note [Flattening under a forall]
547 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
548 Under a forall, we
549   (a) MUST apply the inert subsitution
550   (b) MUST NOT flatten type family applications
551 Hence FMSubstOnly.
552
553 For (a) consider   c ~ a, a ~ T (forall b. (b, [c])
554 If we don't apply the c~a substitution to the second constraint
555 we won't see the occurs-check error.
556
557 For (b) consider  (a ~ forall b. F a b), we don't want to flatten
558 to     (a ~ forall b.fsk, F a b ~ fsk)
559 because now the 'b' has escaped its scope.  We'd have to flatten to
560        (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
561 and we have not begun to think about how to make that work!
562
563 \begin{code}
564 flattenNestedFamApp :: FlattenMode -> CtEvidence
565                     -> TyCon -> [TcType]   -- Exactly-saturated type function application
566                     -> TcS (Xi, TcCoercion)
567 flattenNestedFamApp FMSubstOnly _ tc xi_args
568   = do { let fam_ty = mkTyConApp tc xi_args
569        ; return (fam_ty, mkTcNomReflCo fam_ty) }
570
571 flattenNestedFamApp FMFullFlatten ctxt tc xi_args  -- Eactly saturated
572   = do { let fam_ty = mkTyConApp tc xi_args
573        ; mb_ct <- lookupFlatEqn tc xi_args
574        ; case mb_ct of
575            Just (ctev, rhs_ty)
576              | ctev `canRewriteOrSame `ctxt    -- Must allow [W]/[W]
577              -> -- You may think that we can just return (cc_rhs ct) but not so.
578                 --            return (mkTcCoVarCo (ctId ct), cc_rhs ct, [])
579                 -- The cached constraint resides in the cache so we have to flatten
580                 -- the rhs to make sure we have applied any inert substitution to it.
581                 -- Alternatively we could be applying the inert substitution to the
582                 -- cache as well when we interact an equality with the inert.
583                 -- The design choice is: do we keep the flat cache rewritten or not?
584                 -- For now I say we don't keep it fully rewritten.
585                do { (rhs_xi,co) <- flatten FMFullFlatten ctev rhs_ty
586                   ; let final_co = evTermCoercion (ctEvTerm ctev)
587                                    `mkTcTransCo` mkTcSymCo co
588                   ; traceTcS "flatten/flat-cache hit" $ (ppr ctev $$ ppr rhs_xi $$ ppr final_co)
589                   ; return (rhs_xi, final_co) }
590
591            _ -> do { (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty
592                    ; extendFlatCache tc xi_args ctev rhs_xi
593
594                    -- The new constraint (F xi_args ~ rhs_xi) is not necessarily inert
595                    -- (e.g. the LHS may be a redex) so we must put it in the work list
596                    ; let ct = CFunEqCan { cc_ev     = ctev
597                                         , cc_fun    = tc
598                                         , cc_tyargs = xi_args
599                                         , cc_rhs    = rhs_xi }
600                    ; updWorkListTcS $ extendWorkListFunEq ct
601
602                    ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr rhs_xi $$ ppr ctev)
603                    ; return (rhs_xi, evTermCoercion (ctEvTerm ctev)) }
604        }
605 \end{code}
606
607 \begin{code}
608 flattenTyVar :: FlattenMode -> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
609 -- "Flattening" a type variable means to apply the substitution to it
610 -- The substitution is actually the union of the substitution in the TyBinds
611 -- for the unification variables that have been unified already with the inert
612 -- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract.
613 --
614 -- Postcondition: co : xi ~ tv
615 flattenTyVar f ctxt tv
616   = do { mb_yes <- flattenTyVarOuter f ctxt tv
617        ; case mb_yes of
618            Left tv'         -> -- Done 
619                                do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv'))
620                                   ; return (ty', mkTcNomReflCo ty') }
621                             where
622                                ty' = mkTyVarTy tv'
623
624            Right (ty1, co1) -> -- Recurse
625                                do { (ty2, co2) <- flatten f ctxt ty1
626                                   ; traceTcS "flattenTyVar2" (ppr tv $$ ppr ty2)
627                                   ; return (ty2, co2 `mkTcTransCo` co1) }
628        }
629
630 flattenTyVarOuter, flattenTyVarFinal 
631    :: FlattenMode -> CtEvidence
632    -> TcTyVar 
633    -> TcS (Either TyVar (TcType, TcCoercion))
634 -- Look up the tyvar in 
635 --   a) the internal MetaTyVar box
636 --   b) the tyvar binds 
637 --   c) the inerts
638 -- Return (Left tv')       if it is not found, tv' has a properly zonked kind
639 --        (Right (ty, co)) if found, with co :: ty ~ tv
640 --                         NB: in the latter case ty is not necessarily flattened
641
642 flattenTyVarOuter f ctxt tv
643   | not (isTcTyVar tv)            -- Happens when flatten under a (forall a. ty)
644   = flattenTyVarFinal f ctxt tv   -- So ty contains refernces to the non-TcTyVar a
645   | otherwise
646   = do { mb_ty <- isFilledMetaTyVar_maybe tv
647        ; case mb_ty of {
648            Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
649                          ; return (Right (ty, mkTcNomReflCo ty)) } ;
650            Nothing ->
651
652     -- Try in ty_binds
653     do { ty_binds <- getTcSTyBindsMap
654        ; case lookupVarEnv ty_binds tv of {
655            Just (_tv,ty) -> do { traceTcS "Following bound tyvar" (ppr tv <+> equals <+> ppr ty)
656                                ; return (Right (ty, mkTcNomReflCo ty)) } ;
657                                  -- NB: ty_binds coercions are all ReflCo,
658            Nothing ->
659
660     -- Try in the inert equalities
661     do { ieqs <- getInertEqs
662        ; case lookupVarEnv ieqs tv of
663            Just (ct:_)                      -- If the first doesn't work,
664              | let ctev   = ctEvidence ct   -- the subsequent ones won't either
665                    rhs_ty = cc_rhs ct
666              , ctev `canRewrite` ctxt 
667              ->  do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
668                     ; return (Right (rhs_ty, mkTcSymCo (evTermCoercion (ctEvTerm ctev)))) }
669                     -- NB: even if ct is Derived we are not going to
670                     -- touch the actual coercion so we are fine.
671
672            _other -> flattenTyVarFinal f ctxt tv
673     } } } } }
674
675 flattenTyVarFinal f ctxt tv
676   = -- Done, but make sure the kind is zonked
677     do { let knd = tyVarKind tv
678        ; (new_knd, _kind_co) <- flatten f ctxt knd
679        ; return (Left (setVarType tv new_knd)) }
680 \end{code}
681
682 Note [Non-idempotent inert substitution]
683 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
684
685 The inert substitution is not idempotent in the broad sense. It is only idempotent in
686 that it cannot rewrite the RHS of other inert equalities any further. An example of such
687 an inert substitution is:
688
689  [G] g1 : ta8 ~ ta4
690  [W] g2 : ta4 ~ a5Fj
691
692 Observe that the wanted cannot rewrite the solved goal, despite the fact that ta4 appears on
693 an RHS of an equality. Now, imagine a constraint:
694
695  [W] g3: ta8 ~ Int
696
697 coming in. If we simply apply once the inert substitution we will get:
698
699  [W] g3_1: ta4 ~ Int
700
701 and because potentially ta4 is untouchable we will try to insert g3_1 in the inert set,
702 getting a panic since the inert only allows ONE equation per LHS type variable (as it
703 should).
704
705 For this reason, when we reach to flatten a type variable, we flatten it recursively,
706 so that we can make sure that the inert substitution /is/ fully applied.
707
708 Insufficient (non-recursive) rewriting was the reason for #5668.
709
710
711 %************************************************************************
712 %*                                                                      *
713 %*        Equalities
714 %*                                                                      *
715 %************************************************************************
716
717 \begin{code}
718 canEvVarsCreated :: [CtEvidence] -> TcS StopOrContinue
719 canEvVarsCreated [] = return Stop
720     -- Add all but one to the work list
721     -- and return the first (if any) for futher processing
722 canEvVarsCreated (ev : evs)
723   = do { emitWorkNC evs; canEvNC ev }
724           -- Note the "NC": these are fresh goals, not necessarily canonical
725
726 emitWorkNC :: [CtEvidence] -> TcS ()
727 emitWorkNC evs
728   | null evs  = return ()
729   | otherwise = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
730                    ; updWorkListTcS (extendWorkListCts (map mk_nc evs)) }
731   where
732     mk_nc ev = mkNonCanonical ev
733
734 -------------------------
735 canEqNC :: CtEvidence -> Type -> Type -> TcS StopOrContinue
736 canEqNC ev ty1 ty2 = can_eq_nc ev ty1 ty1 ty2 ty2
737
738
739 can_eq_nc, can_eq_nc' 
740    :: CtEvidence 
741    -> Type -> Type    -- LHS, after and before type-synonym expansion, resp 
742    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp 
743    -> TcS StopOrContinue
744
745 can_eq_nc ev ty1 ps_ty1 ty2 ps_ty2
746   = do { traceTcS "can_eq_nc" $ 
747          vcat [ ppr ev, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
748        ; can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2 }
749
750 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
751 can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2
752   | Just ty1' <- tcView ty1 = can_eq_nc ev ty1' ps_ty1 ty2  ps_ty2
753   | Just ty2' <- tcView ty2 = can_eq_nc ev ty1  ps_ty1 ty2' ps_ty2
754
755 -- Type family on LHS or RHS take priority
756 can_eq_nc' ev (TyConApp fn tys) _ ty2 ps_ty2
757   | isSynFamilyTyCon fn
758   = canEqLeafFun ev NotSwapped fn tys ty2 ps_ty2
759 can_eq_nc' ev ty1 ps_ty1 (TyConApp fn tys) _
760   | isSynFamilyTyCon fn
761   = canEqLeafFun ev IsSwapped fn tys ty1 ps_ty1
762
763 -- Type variable on LHS or RHS are next
764 can_eq_nc' ev (TyVarTy tv1) _ ty2 ps_ty2
765   = canEqTyVar ev NotSwapped tv1 ty2 ps_ty2
766 can_eq_nc' ev ty1 ps_ty1 (TyVarTy tv2) _
767   = canEqTyVar ev IsSwapped tv2 ty1 ps_ty1
768
769 ----------------------
770 -- Otherwise try to decompose
771 ----------------------
772
773 -- Literals
774 can_eq_nc' ev ty1@(LitTy l1) _ (LitTy l2) _
775  | l1 == l2
776   = do { when (isWanted ev) $
777          setEvBind (ctev_evar ev) (EvCoercion (mkTcNomReflCo ty1))
778        ; return Stop }
779
780 -- Decomposable type constructor applications 
781 -- Synonyms and type functions (which are not decomposable)
782 -- have already been dealt with 
783 can_eq_nc' ev (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
784   | isDecomposableTyCon tc1
785   , isDecomposableTyCon tc2
786   = canDecomposableTyConApp ev tc1 tys1 tc2 tys2
787
788 can_eq_nc' ev (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
789   | isDecomposableTyCon tc1 
790       -- The guard is important
791       -- e.g.  (x -> y) ~ (F x y) where F has arity 1
792       --       should not fail, but get the app/app case
793   = canEqFailure ev ps_ty1 ps_ty2
794
795 can_eq_nc' ev (FunTy s1 t1) _ (FunTy s2 t2) _
796   = canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2]
797
798 can_eq_nc' ev (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
799   | isDecomposableTyCon tc2 
800   = canEqFailure ev ps_ty1 ps_ty2
801
802 can_eq_nc' ev s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
803  | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
804  = do { let (tvs1,body1) = tcSplitForAllTys s1
805             (tvs2,body2) = tcSplitForAllTys s2
806       ; if not (equalLength tvs1 tvs2) then
807           canEqFailure ev s1 s2
808         else
809           do { traceTcS "Creating implication for polytype equality" $ ppr ev
810              ; ev_term <- deferTcSForAllEq Nominal loc (tvs1,body1) (tvs2,body2)
811              ; setEvBind orig_ev ev_term
812              ; return Stop } }
813  | otherwise
814  = do { traceTcS "Ommitting decomposition of given polytype equality" $
815         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
816       ; return Stop }
817
818 can_eq_nc' ev (AppTy s1 t1) ps_ty1 ty2 ps_ty2
819   = can_eq_app ev NotSwapped s1 t1 ps_ty1 ty2 ps_ty2
820 can_eq_nc' ev ty1 ps_ty1 (AppTy s2 t2) ps_ty2
821   = can_eq_app ev IsSwapped s2 t2 ps_ty2 ty1 ps_ty1
822
823 -- Everything else is a definite type error, eg LitTy ~ TyConApp
824 can_eq_nc' ev _ ps_ty1 _ ps_ty2
825   = canEqFailure ev ps_ty1 ps_ty2
826
827 ------------
828 can_eq_app, can_eq_flat_app
829     :: CtEvidence -> SwapFlag
830     -> Type -> Type -> Type  -- LHS (s1 t2), after and before type-synonym expansion, resp 
831     -> Type -> Type          -- RHS (ty2),   after and before type-synonym expansion, resp 
832     -> TcS StopOrContinue
833 -- See Note [Canonicalising type applications]
834 can_eq_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
835   =  do { traceTcS "can_eq_app 1" $
836           vcat [ ppr ev, ppr swapped, ppr s1, ppr t1, ppr ty2 ]
837         ; (xi_s1, co_s1) <- flatten FMSubstOnly ev s1
838         ; traceTcS "can_eq_app 2" $ vcat [ ppr ev, ppr xi_s1 ]
839         ; if s1 `tcEqType` xi_s1
840           then can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
841           else
842      do { (xi_t1, co_t1) <- flatten FMSubstOnly ev t1
843              -- We flatten t1 as well so that (xi_s1 xi_t1) is well-kinded
844              -- If we form (xi_s1 t1) that might (appear) ill-kinded, 
845              -- and then crash in a call to typeKind
846         ; let xi1 = mkAppTy xi_s1 xi_t1
847               co1 = mkTcAppCo co_s1 co_t1
848         ; traceTcS "can_eq_app 3" $ vcat [ ppr ev, ppr xi1, ppr co1 ]
849         ; mb_ct <- rewriteEqEvidence ev swapped xi1 ps_ty2 
850                                      co1 (mkTcNomReflCo ps_ty2)
851         ; traceTcS "can_eq_app 4" $ vcat [ ppr ev, ppr xi1, ppr co1 ]
852         ; case mb_ct of
853            Nothing     -> return Stop
854            Just new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }}
855
856 -- Preconditions: s1  is already flattened
857 --                ty2 is not a type variable, so flattening
858 --                    can't turn it into an application if it
859 --                    doesn't look like one already
860 -- See Note [Canonicalising type applications]
861 can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
862   | Just (s2,t2) <- tcSplitAppTy_maybe ty2
863   = unSwap swapped decompose_it (s1,t1) (s2,t2)
864   | otherwise
865   = unSwap swapped (canEqFailure ev) ps_ty1 ps_ty2
866   where
867     decompose_it (s1,t1) (s2,t2) 
868       = do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
869                  xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
870                  xevdecomp x = let xco = evTermCoercion x
871                                in [ EvCoercion (mkTcLRCo CLeft xco)
872                                   , EvCoercion (mkTcLRCo CRight xco)]
873            ; ctevs <- xCtEvidence ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp)
874            ; canEvVarsCreated ctevs }
875
876
877 ------------------------
878 canDecomposableTyConApp :: CtEvidence
879                         -> TyCon -> [TcType]
880                         -> TyCon -> [TcType]
881                         -> TcS StopOrContinue
882 canDecomposableTyConApp ev tc1 tys1 tc2 tys2
883   | tc1 /= tc2 || length tys1 /= length tys2
884     -- Fail straight away for better error messages
885   = canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
886   | otherwise
887   = do { traceTcS "canDecomposableTyConApp" (ppr ev $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
888        ; canDecomposableTyConAppOK ev tc1 tys1 tys2 }
889
890 canDecomposableTyConAppOK :: CtEvidence
891                           -> TyCon -> [TcType] -> [TcType]
892                           -> TcS StopOrContinue
893
894 canDecomposableTyConAppOK ev tc1 tys1 tys2
895   = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
896              xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
897              xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
898        ; ctevs <- xCtEvidence ev xev
899        ; canEvVarsCreated ctevs }
900
901 canEqFailure :: CtEvidence -> TcType -> TcType -> TcS StopOrContinue
902 -- See Note [Make sure that insolubles are fully rewritten]
903 canEqFailure ev ty1 ty2
904   = do { (s1, co1) <- flatten FMSubstOnly ev ty1
905        ; (s2, co2) <- flatten FMSubstOnly ev ty2
906        ; mb_ct <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
907        ; case mb_ct of
908            Just new_ev -> emitInsoluble (mkNonCanonical new_ev)
909            Nothing -> pprPanic "canEqFailure" (ppr ev $$ ppr ty1 $$ ppr ty2)
910        ; return Stop }
911 \end{code}
912
913 Note [Canonicalising type applications]
914 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
915 Given (s1 t1) ~ ty2, how should we proceed?
916 The simple things is to see if ty2 is of form (s2 t2), and 
917 decompose.  By this time s1 and s2 can't be saturated type
918 function applications, because those have been dealt with 
919 by an earlier equation in can_eq_nc, so it is always sound to 
920 decompose.
921
922 However, over-eager decomposition gives bad error messages 
923 for things like
924    a b ~ Maybe c
925    e f ~ p -> q
926 Suppose (in the first example) we already know a~Array.  Then if we
927 decompose the application eagerly, yielding
928    a ~ Maybe
929    b ~ c
930 we get an error        "Can't match Array ~ Maybe", 
931 but we'd prefer to get "Can't match Array b ~ Maybe c".
932
933 So instead can_eq_app flattens s1.  If flattening does something, it
934 rewrites, and goes round can_eq_nc again.  If flattening 
935 does nothing, then (at least with our present state of knowledge)
936 we can only decompose, and that is what can_eq_flat_app attempts
937 to do. 
938
939 Note [Make sure that insolubles are fully rewritten]
940 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
941 When an equality fails, we still want to rewrite the equality
942 all the way down, so that it accurately reflects
943  (a) the mutable reference substitution in force at start of solving
944  (b) any ty-binds in force at this point in solving
945 See Note [Kick out insolubles] in TcInteract.
946 And if we don't do this there is a bad danger that
947 TcSimplify.applyTyVarDefaulting will find a variable
948 that has in fact been substituted.
949
950 Note [Do not decompose Given polytype equalities]
951 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
952 Consider [G] (forall a. t1 ~ forall a. t2).  Can we decompose this?
953 No -- what would the evidence look like?  So instead we simply discard
954 this given evidence.
955
956
957 Note [Combining insoluble constraints]
958 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
959 As this point we have an insoluble constraint, like Int~Bool.
960
961  * If it is Wanted, delete it from the cache, so that subsequent
962    Int~Bool constraints give rise to separate error messages
963
964  * But if it is Derived, DO NOT delete from cache.  A class constraint
965    may get kicked out of the inert set, and then have its functional
966    dependency Derived constraints generated a second time. In that
967    case we don't want to get two (or more) error messages by
968    generating two (or more) insoluble fundep constraints from the same
969    class constraint.
970
971
972 Note [Canonical ordering for equality constraints]
973 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
974 Implemented as (<+=) below:
975
976   - Type function applications always come before anything else.
977   - Variables always come before non-variables (other than type
978       function applications).
979
980 Note that we don't need to unfold type synonyms on the RHS to check
981 the ordering; that is, in the rules above it's OK to consider only
982 whether something is *syntactically* a type function application or
983 not.  To illustrate why this is OK, suppose we have an equality of the
984 form 'tv ~ S a b c', where S is a type synonym which expands to a
985 top-level application of the type function F, something like
986
987   type S a b c = F d e
988
989 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
990 expansion contains type function applications the flattener will do
991 the expansion and then generate a skolem variable for the type
992 function application, so we end up with something like this:
993
994   tv ~ x
995   F d e ~ x
996
997 where x is the skolem variable.  This is one extra equation than
998 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
999 if we had noticed that S expanded to a top-level type function
1000 application and flipped it around in the first place) but this way
1001 keeps the code simpler.
1002
1003 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
1004 ordering of tv ~ tv constraints.  There are several reasons why we
1005 might:
1006
1007   (1) In order to be able to extract a substitution that doesn't
1008       mention untouchable variables after we are done solving, we might
1009       prefer to put touchable variables on the left. However, in and
1010       of itself this isn't necessary; we can always re-orient equality
1011       constraints at the end if necessary when extracting a substitution.
1012
1013   (2) To ensure termination we might think it necessary to put
1014       variables in lexicographic order. However, this isn't actually
1015       necessary as outlined below.
1016
1017 While building up an inert set of canonical constraints, we maintain
1018 the invariant that the equality constraints in the inert set form an
1019 acyclic rewrite system when viewed as L-R rewrite rules.  Moreover,
1020 the given constraints form an idempotent substitution (i.e. none of
1021 the variables on the LHS occur in any of the RHS's, and type functions
1022 never show up in the RHS at all), the wanted constraints also form an
1023 idempotent substitution, and finally the LHS of a given constraint
1024 never shows up on the RHS of a wanted constraint.  There may, however,
1025 be a wanted LHS that shows up in a given RHS, since we do not rewrite
1026 given constraints with wanted constraints.
1027
1028 Suppose we have an inert constraint set
1029
1030
1031   tg_1 ~ xig_1         -- givens
1032   tg_2 ~ xig_2
1033   ...
1034   tw_1 ~ xiw_1         -- wanteds
1035   tw_2 ~ xiw_2
1036   ...
1037
1038 where each t_i can be either a type variable or a type function
1039 application. Now suppose we take a new canonical equality constraint,
1040 t' ~ xi' (note among other things this means t' does not occur in xi')
1041 and try to react it with the existing inert set.  We show by induction
1042 on the number of t_i which occur in t' ~ xi' that this process will
1043 terminate.
1044
1045 There are several ways t' ~ xi' could react with an existing constraint:
1046
1047 TODO: finish this proof.  The below was for the case where the entire
1048 inert set is an idempotent subustitution...
1049
1050 (b) We could have t' = t_j for some j.  Then we obtain the new
1051     equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j.  We
1052     now canonicalize the new equality, which may involve decomposing it
1053     into several canonical equalities, and recurse on these.  However,
1054     none of the new equalities will contain t_j, so they have fewer
1055     occurrences of the t_i than the original equation.
1056
1057 (a) We could have t_j occurring in xi' for some j, with t' /=
1058     t_j. Then we substitute xi_j for t_j in xi' and continue.  However,
1059     since none of the t_i occur in xi_j, we have decreased the
1060     number of t_i that occur in xi', since we eliminated t_j and did not
1061     introduce any new ones.
1062
1063 \begin{code}
1064 canEqLeafFun :: CtEvidence 
1065              -> SwapFlag
1066              -> TyCon -> [TcType]   -- LHS
1067              -> TcType -> TcType    -- RHS
1068              -> TcS StopOrContinue
1069 canEqLeafFun ev swapped fn tys1 ty2 ps_ty2
1070   | length tys1 > tyConArity fn
1071   = -- Over-saturated type function on LHS: 
1072     -- flatten LHS, leaving an AppTy, and go around again
1073     do { (xi1, co1) <- flatten FMFullFlatten ev (mkTyConApp fn tys1)
1074        ; mb <- rewriteEqEvidence ev swapped xi1 ps_ty2 
1075                                  co1 (mkTcNomReflCo ps_ty2)
1076        ; case mb of
1077             Nothing     -> return Stop
1078             Just new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }
1079
1080   | otherwise
1081   = -- ev :: F tys1 ~ ty2,   if not swapped
1082     -- ev :: ty2 ~ F tys1,   if swapped                                    
1083     ASSERT( length tys1 == tyConArity fn )  
1084         -- Type functions are never under-saturated
1085         -- Previous equation checks for over-saturation
1086     do { traceTcS "canEqLeafFun" $ pprEq (mkTyConApp fn tys1) ps_ty2
1087
1088             -- Flatten type function arguments
1089             -- cos1 :: xis1 ~ tys1
1090             -- co2  :: xi2 ~ ty2
1091       ; (xis1,cos1) <- flattenMany FMFullFlatten ev tys1
1092       ; (xi2, co2)  <- flatten     FMFullFlatten ev ps_ty2
1093
1094        ; let fam_head = mkTyConApp fn xis1
1095              co1      = mkTcTyConAppCo Nominal fn cos1
1096        ; mb <- rewriteEqEvidence ev swapped fam_head xi2 co1 co2
1097
1098        ; let k1 = typeKind fam_head
1099              k2 = typeKind xi2
1100        ; case mb of
1101             Nothing     -> return Stop
1102             Just new_ev | k1 `isSubKind` k2
1103                         -- Establish CFunEqCan kind invariant
1104                         -> continueWith (CFunEqCan { cc_ev = new_ev, cc_fun = fn
1105                                                    , cc_tyargs = xis1, cc_rhs = xi2 })
1106                         | otherwise
1107                         -> checkKind new_ev fam_head k1 xi2 k2 }
1108
1109 ---------------------
1110 canEqTyVar :: CtEvidence -> SwapFlag
1111            -> TcTyVar 
1112            -> TcType -> TcType
1113            -> TcS StopOrContinue
1114 -- A TyVar on LHS, but so far un-zonked
1115 canEqTyVar ev swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
1116   = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
1117        ; mb_yes <- flattenTyVarOuter FMFullFlatten ev tv1 
1118        ; case mb_yes of
1119            Right (ty1, co1) -> -- co1 :: ty1 ~ tv1
1120                                do { mb <- rewriteEqEvidence ev swapped  ty1 ps_ty2
1121                                                             co1 (mkTcNomReflCo ps_ty2)
1122                                   ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1,
1123                                                                   ppUnless (isDerived ev) (ppr co1)])
1124                                   ; case mb of
1125                                       Nothing     -> return Stop
1126                                       Just new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 }
1127
1128            Left tv1' -> do { (xi2, co2) <- flatten FMFullFlatten ev ps_ty2 -- co2 :: xi2 ~ ps_ty2
1129                                            -- Use ps_ty2 to preserve type synonyms if poss
1130                            ; dflags <- getDynFlags
1131                            ; canEqTyVar2 dflags ev swapped tv1' xi2 co2 } }
1132
1133 canEqTyVar2 :: DynFlags
1134             -> CtEvidence   -- olhs ~ orhs (or, if swapped, orhs ~ olhs)
1135             -> SwapFlag
1136             -> TcTyVar      -- olhs
1137             -> TcType       -- nrhs
1138             -> TcCoercion   -- nrhs ~ orhs
1139             -> TcS StopOrContinue
1140 -- LHS is an inert type variable, 
1141 -- and RHS is fully rewritten, but with type synonyms
1142 -- preserved as much as possible
1143
1144 canEqTyVar2 dflags ev swapped tv1 xi2 co2
1145   | Just tv2 <- getTyVar_maybe xi2
1146   = canEqTyVarTyVar ev swapped tv1 tv2 co2
1147
1148   | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2  -- No occurs check
1149   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2' co1 co2
1150                 -- Ensure that the new goal has enough type synonyms
1151                 -- expanded by the occurCheckExpand; hence using xi2' here
1152                 -- See Note [occurCheckExpand]
1153
1154        ; let k1 = tyVarKind tv1
1155              k2 = typeKind xi2'
1156        ; case mb of
1157             Nothing     -> return Stop
1158             Just new_ev | k2 `isSubKind` k1
1159                         -- Establish CTyEqCan kind invariant
1160                         -- Reorientation has done its best, but the kinds might
1161                         -- simply be incompatible
1162                         -> continueWith (CTyEqCan { cc_ev = new_ev
1163                                                   , cc_tyvar  = tv1, cc_rhs = xi2' })
1164                         | otherwise
1165                         -> checkKind new_ev xi1 k1 xi2' k2 }
1166
1167   | otherwise  -- Occurs check error
1168   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2
1169        ; case mb of
1170            Nothing     -> return ()
1171            Just new_ev -> emitInsoluble (mkNonCanonical new_ev)
1172        ; return Stop }
1173   where
1174     xi1 = mkTyVarTy tv1
1175     co1 = mkTcNomReflCo xi1
1176
1177
1178 canEqTyVarTyVar :: CtEvidence       -- tv1 ~ orhs (or orhs ~ tv1, if swapped)
1179                 -> SwapFlag
1180                 -> TyVar -> TyVar   -- tv2, tv2
1181                 -> TcCoercion       -- tv2 ~ orhs
1182                 -> TcS StopOrContinue
1183 -- Both LHS and RHS rewrote to a type variable,
1184 canEqTyVarTyVar ev swapped tv1 tv2 co2
1185   | tv1 == tv2
1186   = do { when (isWanted ev) $
1187          ASSERT( tcCoercionRole co2 == Nominal )
1188          setEvBind (ctev_evar ev) (EvCoercion (maybeSym swapped co2))
1189        ; return Stop }  
1190
1191   | reorient_me  -- See note [Canonical ordering for equality constraints].
1192                  -- True => the kinds are compatible, 
1193                  --         so no need for further sub-kind check
1194                  -- If swapped = NotSwapped, then
1195                  --     rw_orhs = tv1, rw_olhs = orhs
1196                  --     rw_nlhs = tv2, rw_nrhs = xi1
1197   = do { mb <- rewriteEqEvidence ev (flipSwap swapped)  xi2 xi1
1198                                  co2 (mkTcNomReflCo xi1)
1199        ; case mb of
1200            Nothing     -> return Stop
1201            Just new_ev -> continueWith (CTyEqCan { cc_ev = new_ev
1202                                                  , cc_tyvar  = tv2, cc_rhs = xi1 }) }
1203
1204   | otherwise
1205   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 
1206                                  (mkTcNomReflCo xi1) co2
1207        ; case mb of
1208            Nothing     -> return Stop
1209            Just new_ev | k2 `isSubKind` k1
1210                        -> continueWith (CTyEqCan { cc_ev = new_ev
1211                                                  , cc_tyvar = tv1, cc_rhs = xi2 })
1212                        | otherwise
1213                        -> checkKind new_ev xi1 k1 xi2 k2 } 
1214   where
1215     reorient_me 
1216       | k1 `tcEqKind` k2    = tv2 `better_than` tv1
1217       | k1 `isSubKind` k2   = True  -- Note [Kind orientation for CTyEqCan]
1218       | otherwise           = False -- in TcRnTypes
1219
1220     xi1 = mkTyVarTy tv1
1221     xi2 = mkTyVarTy tv2
1222     k1  = tyVarKind tv1
1223     k2  = tyVarKind tv2
1224
1225     tv2 `better_than` tv1
1226       | isMetaTyVar tv1     = False   -- Never swap a meta-tyvar
1227       | isFlatSkolTyVar tv1 = isMetaTyVar tv2
1228       | otherwise           = isMetaTyVar tv2 || isFlatSkolTyVar tv2
1229                             -- Note [Eliminate flat-skols]
1230
1231 checkKind :: CtEvidence         -- t1~t2
1232           -> TcType -> TcKind
1233           -> TcType -> TcKind   -- s1~s2, flattened and zonked
1234           -> TcS StopOrContinue
1235 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
1236 --       CIrredEvCan (NOT CTyEqCan or CFunEqCan)
1237 -- for the type equality; and continue with the kind equality constraint.
1238 -- When the latter is solved, it'll kick out the irreducible equality for
1239 -- a second attempt at solving
1240 --
1241 -- See Note [Equalities with incompatible kinds]
1242
1243 checkKind new_ev s1 k1 s2 k2   -- See Note [Equalities with incompatible kinds]
1244   = ASSERT( isKind k1 && isKind k2 )
1245     do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
1246
1247          -- Create a derived kind-equality, and solve it
1248        ; mw <- newDerived kind_co_loc (mkEqPred k1 k2)
1249        ; case mw of
1250            Nothing  -> return ()
1251            Just kev -> emitWorkNC [kev]
1252
1253          -- Put the not-currently-soluble thing into the inert set
1254        ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1255   where
1256     loc = ctev_loc new_ev
1257     kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
1258 \end{code}
1259
1260 Note [Eliminate flat-skols]
1261 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1262 Suppose we have  [G] Num (F [a])
1263 then we flatten to
1264      [G] Num fsk
1265      [G] F [a] ~ fsk
1266 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1267       type instance F [a] = a
1268 then we'll reduce the second constraint to
1269      [G] a ~ fsk
1270 and then replace all uses of 'a' with fsk.  That's bad because
1271 in error messages intead of saying 'a' we'll say (F [a]).  In all
1272 places, including those where the programmer wrote 'a' in the first
1273 place.  Very confusing!  See Trac #7862.
1274
1275 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1276 the fsk.
1277
1278 Note [Equalities with incompatible kinds]
1279 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1280 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1281 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1282 CFunEqCan.  What if we try to unify two things with incompatible
1283 kinds?
1284
1285 eg    a ~ b  where a::*, b::*->*
1286 or    a ~ b  where a::*, b::k, k is a kind variable
1287
1288 The CTyEqCan compatKind invariant is important.  If we make a CTyEqCan
1289 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1290 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1291 Trac #7696).
1292
1293 So instead for these ill-kinded equalities we generate a CIrredCan,
1294 and put it in the inert set, which keeps it out of the way until a
1295 subsequent substitution (on kind variables, say) re-activates it.
1296
1297 NB: it is important that the types s1,s2 are flattened and zonked
1298     so that their kinds k1, k2 are inert wrt the substitution.  That
1299     means that they can only become the same if we change the inert
1300     set, which in turn will kick out the irreducible equality
1301     E.g. it is WRONG to make an irred (a:k1)~(b:k2)
1302          if we already have a substitution k1:=k2
1303
1304 NB: it's important that the new CIrredCan goes in the inert set rather
1305 than back into the work list. We used to do the latter, but that led
1306 to an infinite loop when we encountered it again, and put it back it
1307 the work list again.
1308
1309 See also Note [Kind orientation for CTyEqCan] and
1310          Note [Kind orientation for CFunEqCan] in TcRnTypes
1311
1312 Note [Type synonyms and canonicalization]
1313 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1314 We treat type synonym applications as xi types, that is, they do not
1315 count as type function applications.  However, we do need to be a bit
1316 careful with type synonyms: like type functions they may not be
1317 generative or injective.  However, unlike type functions, they are
1318 parametric, so there is no problem in expanding them whenever we see
1319 them, since we do not need to know anything about their arguments in
1320 order to expand them; this is what justifies not having to treat them
1321 as specially as type function applications.  The thing that causes
1322 some subtleties is that we prefer to leave type synonym applications
1323 *unexpanded* whenever possible, in order to generate better error
1324 messages.
1325
1326 If we encounter an equality constraint with type synonym applications
1327 on both sides, or a type synonym application on one side and some sort
1328 of type application on the other, we simply must expand out the type
1329 synonyms in order to continue decomposing the equality constraint into
1330 primitive equality constraints.  For example, suppose we have
1331
1332   type F a = [Int]
1333
1334 and we encounter the equality
1335
1336   F a ~ [b]
1337
1338 In order to continue we must expand F a into [Int], giving us the
1339 equality
1340
1341   [Int] ~ [b]
1342
1343 which we can then decompose into the more primitive equality
1344 constraint
1345
1346   Int ~ b.
1347
1348 However, if we encounter an equality constraint with a type synonym
1349 application on one side and a variable on the other side, we should
1350 NOT (necessarily) expand the type synonym, since for the purpose of
1351 good error messages we want to leave type synonyms unexpanded as much
1352 as possible.  Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1353
1354
1355 Note [occurCheckExpand]
1356 ~~~~~~~~~~~~~~~~~~~~~~~
1357 There is a subtle point with type synonyms and the occurs check that
1358 takes place for equality constraints of the form tv ~ xi.  As an
1359 example, suppose we have
1360
1361   type F a = Int
1362
1363 and we come across the equality constraint
1364
1365   a ~ F a
1366
1367 This should not actually fail the occurs check, since expanding out
1368 the type synonym results in the legitimate equality constraint a ~
1369 Int.  We must actually do this expansion, because unifying a with F a
1370 will lead the type checker into infinite loops later.  Put another
1371 way, canonical equality constraints should never *syntactically*
1372 contain the LHS variable in the RHS type.  However, we don't always
1373 need to expand type synonyms when doing an occurs check; for example,
1374 the constraint
1375
1376   a ~ F b
1377
1378 is obviously fine no matter what F expands to. And in this case we
1379 would rather unify a with F b (rather than F b's expansion) in order
1380 to get better error messages later.
1381
1382 So, when doing an occurs check with a type synonym application on the
1383 RHS, we use some heuristics to find an expansion of the RHS which does
1384 not contain the variable from the LHS.  In particular, given
1385
1386   a ~ F t1 ... tn
1387
1388 we first try expanding each of the ti to types which no longer contain
1389 a.  If this turns out to be impossible, we next try expanding F
1390 itself, and so on.  See Note [Occurs check expansion] in TcType
1391