9b938156721e3b5e061ceb4f4a75673de4f8ec92
[ghc.git] / compiler / typecheck / TcCanonical.lhs
1 \begin{code}
2 {-# LANGUAGE CPP #-}
3
4 module TcCanonical( canonicalize ) where
5
6 #include "HsVersions.h"
7
8 import TcRnTypes
9 import TcType
10 import Type
11 import Kind
12 import TcFlatten
13 import TcSMonad
14 import TcEvidence
15 import Class
16 import TyCon
17 import TypeRep
18 import Var
19 import Name( isSystemName )
20 import OccName( OccName )
21 import Outputable
22 import Control.Monad    ( when )
23 import DynFlags( DynFlags )
24 import VarSet
25
26 import Util
27 import BasicTypes
28 \end{code}
29
30
31 %************************************************************************
32 %*                                                                      *
33 %*                      The Canonicaliser                               *
34 %*                                                                      *
35 %************************************************************************
36
37 Note [Canonicalization]
38 ~~~~~~~~~~~~~~~~~~~~~~~
39
40 Canonicalization converts a flat constraint to a canonical form. It is
41 unary (i.e. treats individual constraints one at a time), does not do
42 any zonking, but lives in TcS monad because it needs to create fresh
43 variables (for flattening) and consult the inerts (for efficiency).
44
45 The execution plan for canonicalization is the following:
46
47   1) Decomposition of equalities happens as necessary until we reach a
48      variable or type family in one side. There is no decomposition step
49      for other forms of constraints.
50
51   2) If, when we decompose, we discover a variable on the head then we
52      look at inert_eqs from the current inert for a substitution for this
53      variable and contine decomposing. Hence we lazily apply the inert
54      substitution if it is needed.
55
56   3) If no more decomposition is possible, we deeply apply the substitution
57      from the inert_eqs and continue with flattening.
58
59   4) During flattening, we examine whether we have already flattened some
60      function application by looking at all the CTyFunEqs with the same
61      function in the inert set. The reason for deeply applying the inert
62      substitution at step (3) is to maximise our chances of matching an
63      already flattened family application in the inert.
64
65 The net result is that a constraint coming out of the canonicalization
66 phase cannot be rewritten any further from the inerts (but maybe /it/ can
67 rewrite an inert or still interact with an inert in a further phase in the
68 simplifier.
69
70 Note [Caching for canonicals]
71 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
72 Our plan with pre-canonicalization is to be able to solve a constraint
73 really fast from existing bindings in TcEvBinds. So one may think that
74 the condition (isCNonCanonical) is not necessary.  However consider
75 the following setup:
76
77 InertSet = { [W] d1 : Num t }
78 WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
79
80 Now, we prioritize equalities, but in our concrete example
81 (should_run/mc17.hs) the first (d2) constraint is dealt with first,
82 because (t ~ Int) is an equality that only later appears in the
83 worklist since it is pulled out from a nested implication
84 constraint. So, let's examine what happens:
85
86    - We encounter work item (d2 : Num t)
87
88    - Nothing is yet in EvBinds, so we reach the interaction with inerts
89      and set:
90               d2 := d1
91     and we discard d2 from the worklist. The inert set remains unaffected.
92
93    - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
94      (d1 : Num t) from the inerts.  Then that equation gets
95      spontaneously solved, perhaps. We end up with:
96         InertSet : { [G] c : t ~ Int }
97         WorkList : { [W] d1 : Num t}
98
99    - Now we examine (d1), we observe that there is a binding for (Num
100      t) in the evidence binds and we set:
101              d1 := d2
102      and end up in a loop!
103
104 Now, the constraints that get kicked out from the inert set are always
105 Canonical, so by restricting the use of the pre-canonicalizer to
106 NonCanonical constraints we eliminate this danger. Moreover, for
107 canonical constraints we already have good caching mechanisms
108 (effectively the interaction solver) and we are interested in reducing
109 things like superclasses of the same non-canonical constraint being
110 generated hence I don't expect us to lose a lot by introducing the
111 (isCNonCanonical) restriction.
112
113 A similar situation can arise in TcSimplify, at the end of the
114 solve_wanteds function, where constraints from the inert set are
115 returned as new work -- our substCt ensures however that if they are
116 not rewritten by subst, they remain canonical and hence we will not
117 attempt to solve them from the EvBinds. If on the other hand they did
118 get rewritten and are now non-canonical they will still not match the
119 EvBinds, so we are again good.
120
121
122
123 \begin{code}
124
125 -- Top-level canonicalization
126 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
127
128 canonicalize :: Ct -> TcS (StopOrContinue Ct)
129 canonicalize ct@(CNonCanonical { cc_ev = ev })
130   = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
131        ; {-# SCC "canEvVar" #-}
132          canEvNC ev }
133
134 canonicalize (CDictCan { cc_ev = ev
135                        , cc_class  = cls
136                        , cc_tyargs = xis })
137   = {-# SCC "canClass" #-}
138     canClass ev cls xis -- Do not add any superclasses
139 canonicalize (CTyEqCan { cc_ev = ev
140                        , cc_tyvar  = tv
141                        , cc_rhs    = xi })
142   = {-# SCC "canEqLeafTyVarEq" #-}
143     canEqTyVar ev NotSwapped tv xi xi
144
145 canonicalize (CFunEqCan { cc_ev = ev
146                         , cc_fun    = fn
147                         , cc_tyargs = xis1
148                         , cc_fsk    = fsk })
149   = {-# SCC "canEqLeafFunEq" #-}
150     canCFunEqCan ev fn xis1 fsk
151
152 canonicalize (CIrredEvCan { cc_ev = ev })
153   = canIrred ev
154 canonicalize (CHoleCan { cc_ev = ev, cc_occ = occ })
155   = canHole ev occ
156
157 canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
158 -- Called only for non-canonical EvVars
159 canEvNC ev
160   = case classifyPredType (ctEvPred ev) of
161       ClassPred cls tys -> traceTcS "canEvNC:cls" (ppr cls <+> ppr tys) >> canClassNC ev cls tys
162       EqPred ty1 ty2    -> traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)   >> canEqNC    ev ty1 ty2
163       TuplePred tys     -> traceTcS "canEvNC:tup" (ppr tys)             >> canTuple   ev tys
164       IrredPred {}      -> traceTcS "canEvNC:irred" (ppr (ctEvPred ev)) >> canIrred   ev
165 \end{code}
166
167
168 %************************************************************************
169 %*                                                                      *
170 %*                      Tuple Canonicalization
171 %*                                                                      *
172 %************************************************************************
173
174 \begin{code}
175 canTuple :: CtEvidence -> [PredType] -> TcS (StopOrContinue Ct)
176 canTuple ev tys
177   = do { traceTcS "can_pred" (text "TuplePred!")
178        ; let xcomp = EvTupleMk
179              xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
180        ; xCtEvidence ev (XEvTerm tys xcomp xdecomp)
181        ; stopWith ev "Decomposed tuple constraint" }
182 \end{code}
183
184 %************************************************************************
185 %*                                                                      *
186 %*                      Class Canonicalization
187 %*                                                                      *
188 %************************************************************************
189
190 \begin{code}
191 canClass, canClassNC
192    :: CtEvidence
193    -> Class -> [Type] -> TcS (StopOrContinue Ct)
194 -- Precondition: EvVar is class evidence
195
196 -- The canClassNC version is used on non-canonical constraints
197 -- and adds superclasses.  The plain canClass version is used
198 -- for already-canonical class constraints (but which might have
199 -- been subsituted or somthing), and hence do not need superclasses
200
201 canClassNC ev cls tys
202   = canClass ev cls tys
203     `andWhenContinue` emitSuperclasses
204
205 canClass ev cls tys
206   = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
207        ; (xis, cos) <- flattenMany fmode tys
208        ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
209              xi = mkClassPred cls xis
210              mk_ct new_ev = CDictCan { cc_ev = new_ev
211                                      , cc_tyargs = xis, cc_class = cls }
212        ; mb <- rewriteEvidence ev xi co
213        ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
214                                    , ppr xi, ppr mb ])
215        ; return (fmap mk_ct mb) }
216
217 emitSuperclasses :: Ct -> TcS (StopOrContinue Ct)
218 emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls })
219             -- Add superclasses of this one here, See Note [Adding superclasses].
220             -- But only if we are not simplifying the LHS of a rule.
221  = do { newSCWorkFromFlavored ev cls xis_new
222       -- Arguably we should "seq" the coercions if they are derived,
223       -- as we do below for emit_kind_constraint, to allow errors in
224       -- superclasses to be executed if deferred to runtime!
225       ; continueWith ct }
226 emitSuperclasses _ = panic "emit_superclasses of non-class!"
227 \end{code}
228
229 Note [Adding superclasses]
230 ~~~~~~~~~~~~~~~~~~~~~~~~~~
231 Since dictionaries are canonicalized only once in their lifetime, the
232 place to add their superclasses is canonicalisation (The alternative
233 would be to do it during constraint solving, but we'd have to be
234 extremely careful to not repeatedly introduced the same superclass in
235 our worklist). Here is what we do:
236
237 For Givens:
238        We add all their superclasses as Givens.
239
240 For Wanteds:
241        Generally speaking we want to be able to add superclasses of
242        wanteds for two reasons:
243
244        (1) Oportunities for improvement. Example:
245                   class (a ~ b) => C a b
246            Wanted constraint is: C alpha beta
247            We'd like to simply have C alpha alpha. Similar
248            situations arise in relation to functional dependencies.
249
250        (2) To have minimal constraints to quantify over:
251            For instance, if our wanted constraint is (Eq a, Ord a)
252            we'd only like to quantify over Ord a.
253
254        To deal with (1) above we only add the superclasses of wanteds
255        which may lead to improvement, that is: equality superclasses or
256        superclasses with functional dependencies.
257
258        We deal with (2) completely independently in TcSimplify. See
259        Note [Minimize by SuperClasses] in TcSimplify.
260
261
262        Moreover, in all cases the extra improvement constraints are
263        Derived. Derived constraints have an identity (for now), but
264        we don't do anything with their evidence. For instance they
265        are never used to rewrite other constraints.
266
267        See also [New Wanted Superclass Work] in TcInteract.
268
269
270 For Deriveds:
271        We do nothing.
272
273 Here's an example that demonstrates why we chose to NOT add
274 superclasses during simplification: [Comes from ticket #4497]
275
276    class Num (RealOf t) => Normed t
277    type family RealOf x
278
279 Assume the generated wanted constraint is:
280    RealOf e ~ e, Normed e
281 If we were to be adding the superclasses during simplification we'd get:
282    Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
283 ==>
284    e ~ uf, Num uf, Normed e, RealOf e ~ e
285 ==> [Spontaneous solve]
286    Num uf, Normed uf, RealOf uf ~ uf
287
288 While looks exactly like our original constraint. If we add the superclass again we'd loop.
289 By adding superclasses definitely only once, during canonicalisation, this situation can't
290 happen.
291
292 \begin{code}
293 newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
294 -- Returns superclasses, see Note [Adding superclasses]
295 newSCWorkFromFlavored flavor cls xis
296   | isDerived flavor
297   = return ()  -- Deriveds don't yield more superclasses because we will
298                -- add them transitively in the case of wanteds.
299
300   | isGiven flavor
301   = do { let sc_theta = immSuperClasses cls xis
302              xev_decomp x = zipWith (\_ i -> EvSuperClass x i) sc_theta [0..]
303              xev = XEvTerm { ev_preds  =  sc_theta
304                            , ev_comp   = panic "Can't compose for given!"
305                            , ev_decomp = xev_decomp }
306        ; xCtEvidence flavor xev }
307
308   | isEmptyVarSet (tyVarsOfTypes xis)
309   = return () -- Wanteds with no variables yield no deriveds.
310               -- See Note [Improvement from Ground Wanteds]
311
312   | otherwise -- Wanted case, just add those SC that can lead to improvement.
313   = do { let sc_rec_theta = transSuperClasses cls xis
314              impr_theta   = filter is_improvement_pty sc_rec_theta
315              loc          = ctEvLoc flavor
316        ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
317        ; mapM_ (emitNewDerived loc) impr_theta }
318
319 is_improvement_pty :: PredType -> Bool
320 -- Either it's an equality, or has some functional dependency
321 is_improvement_pty ty = go (classifyPredType ty)
322   where
323     go (EqPred t1 t2)       = not (t1 `tcEqType` t2)
324     go (ClassPred cls _tys) = not $ null fundeps
325                             where (_,fundeps) = classTvsFds cls
326     go (TuplePred ts)       = any is_improvement_pty ts
327     go (IrredPred {})       = True -- Might have equalities after reduction?
328 \end{code}
329
330
331 %************************************************************************
332 %*                                                                      *
333 %*                      Irreducibles canonicalization
334 %*                                                                      *
335 %************************************************************************
336
337
338 \begin{code}
339 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
340 -- Precondition: ty not a tuple and no other evidence form
341 canIrred old_ev
342   = do { let old_ty = ctEvPred old_ev
343              fmode  = FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }
344                       -- Flatten (F [a]), say, so that it can reduce to Eq a
345        ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
346        ; (xi,co) <- flatten fmode old_ty -- co :: xi ~ old_ty
347        ; mb <- rewriteEvidence old_ev xi co
348        ; case mb of {
349              Stop ev s           -> return (Stop ev s) ;
350              ContinueWith new_ev ->
351
352     do { -- Re-classify, in case flattening has improved its shape
353        ; case classifyPredType (ctEvPred new_ev) of
354            ClassPred cls tys -> canClassNC new_ev cls tys
355            TuplePred tys     -> canTuple   new_ev tys
356            EqPred ty1 ty2    -> canEqNC new_ev ty1 ty2
357            _                 -> continueWith $
358                                 CIrredEvCan { cc_ev = new_ev } } } }
359
360 canHole :: CtEvidence -> OccName -> TcS (StopOrContinue Ct)
361 canHole ev occ
362   = do { let ty    = ctEvPred ev
363              fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly }
364        ; (xi,co) <- flatten fmode ty -- co :: xi ~ ty
365        ; mb <- rewriteEvidence ev xi co
366        ; case mb of
367            ContinueWith new_ev -> do { emitInsoluble (CHoleCan { cc_ev = new_ev, cc_occ = occ })
368                                      ; stopWith new_ev "Emit insoluble hole" }
369            Stop ev s -> return (Stop ev s) } -- Found a cached copy; won't happen
370 \end{code}
371
372 %************************************************************************
373 %*                                                                      *
374 %*        Equalities
375 %*                                                                      *
376 %************************************************************************
377
378 \begin{code}
379 canEqNC :: CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct)
380 canEqNC ev ty1 ty2 = can_eq_nc ev ty1 ty1 ty2 ty2
381
382 can_eq_nc, can_eq_nc' 
383    :: CtEvidence 
384    -> Type -> Type    -- LHS, after and before type-synonym expansion, resp 
385    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp 
386    -> TcS (StopOrContinue Ct)
387
388 can_eq_nc ev ty1 ps_ty1 ty2 ps_ty2
389   = do { traceTcS "can_eq_nc" $ 
390          vcat [ ppr ev, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
391        ; can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2 }
392
393 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
394 can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2
395   | Just ty1' <- tcView ty1 = can_eq_nc ev ty1' ps_ty1 ty2  ps_ty2
396   | Just ty2' <- tcView ty2 = can_eq_nc ev ty1  ps_ty1 ty2' ps_ty2
397
398 -- Type family on LHS or RHS take priority over tyvars,
399 -- so that  tv ~ F ty gets flattened
400 -- Otherwise  F a ~ F a  might not get solved!
401 can_eq_nc' ev (TyConApp fn1 tys1) _ ty2 ps_ty2
402   | isTypeFamilyTyCon fn1 = can_eq_fam_nc ev NotSwapped fn1 tys1 ty2 ps_ty2
403 can_eq_nc' ev ty1 ps_ty1 (TyConApp fn2 tys2) _
404   | isTypeFamilyTyCon fn2 = can_eq_fam_nc ev IsSwapped fn2 tys2 ty1 ps_ty1
405
406 -- Type variable on LHS or RHS are next
407 can_eq_nc' ev (TyVarTy tv1) _ ty2 ps_ty2
408   = canEqTyVar ev NotSwapped tv1 ty2 ps_ty2
409 can_eq_nc' ev ty1 ps_ty1 (TyVarTy tv2) _
410   = canEqTyVar ev IsSwapped tv2 ty1 ps_ty1
411
412 ----------------------
413 -- Otherwise try to decompose
414 ----------------------
415
416 -- Literals
417 can_eq_nc' ev ty1@(LitTy l1) _ (LitTy l2) _
418  | l1 == l2
419   = do { when (isWanted ev) $
420          setEvBind (ctev_evar ev) (EvCoercion (mkTcNomReflCo ty1))
421        ; stopWith ev "Equal LitTy" }
422
423 -- Decomposable type constructor applications 
424 -- Synonyms and type functions (which are not decomposable)
425 -- have already been dealt with 
426 can_eq_nc' ev (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
427   | isDecomposableTyCon tc1
428   , isDecomposableTyCon tc2
429   = canDecomposableTyConApp ev tc1 tys1 tc2 tys2
430
431 can_eq_nc' ev (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
432   | isDecomposableTyCon tc1 
433       -- The guard is important
434       -- e.g.  (x -> y) ~ (F x y) where F has arity 1
435       --       should not fail, but get the app/app case
436   = canEqFailure ev ps_ty1 ps_ty2
437
438 can_eq_nc' ev (FunTy s1 t1) _ (FunTy s2 t2) _
439   = canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2]
440
441 can_eq_nc' ev (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
442   | isDecomposableTyCon tc2 
443   = canEqFailure ev ps_ty1 ps_ty2
444
445 can_eq_nc' ev s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
446  | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
447  = do { let (tvs1,body1) = tcSplitForAllTys s1
448             (tvs2,body2) = tcSplitForAllTys s2
449       ; if not (equalLength tvs1 tvs2) then
450           canEqFailure ev s1 s2
451         else
452           do { traceTcS "Creating implication for polytype equality" $ ppr ev
453              ; ev_term <- deferTcSForAllEq Nominal loc (tvs1,body1) (tvs2,body2)
454              ; setEvBind orig_ev ev_term
455              ; stopWith ev "Deferred polytype equality" } }
456  | otherwise
457  = do { traceTcS "Ommitting decomposition of given polytype equality" $
458         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
459       ; stopWith ev "Discard given polytype equality" }
460
461 can_eq_nc' ev (AppTy s1 t1) ps_ty1 ty2 ps_ty2
462   = can_eq_app ev NotSwapped s1 t1 ps_ty1 ty2 ps_ty2
463 can_eq_nc' ev ty1 ps_ty1 (AppTy s2 t2) ps_ty2
464   = can_eq_app ev IsSwapped s2 t2 ps_ty2 ty1 ps_ty1
465
466 -- Everything else is a definite type error, eg LitTy ~ TyConApp
467 can_eq_nc' ev _ ps_ty1 _ ps_ty2
468   = canEqFailure ev ps_ty1 ps_ty2
469
470 ------------
471 can_eq_fam_nc :: CtEvidence -> SwapFlag
472               -> TyCon -> [TcType]
473               -> TcType -> TcType
474               -> TcS (StopOrContinue Ct)
475 -- Canonicalise a non-canonical equality of form (F tys ~ ty)
476 --   or the swapped version thereof
477 -- Flatten both sides and go round again
478 can_eq_fam_nc ev swapped fn tys rhs ps_rhs
479   = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
480        ; (xi_lhs, co_lhs) <- flattenFamApp fmode fn tys
481        ; mb_ct <- rewriteEqEvidence ev swapped xi_lhs rhs co_lhs (mkTcNomReflCo rhs)
482        ; case mb_ct of
483            Stop ev s           -> return (Stop ev s)
484            ContinueWith new_ev -> can_eq_nc new_ev xi_lhs xi_lhs rhs ps_rhs }
485
486 ------------
487 can_eq_app, can_eq_flat_app
488     :: CtEvidence -> SwapFlag
489     -> Type -> Type -> Type  -- LHS (s1 t2), after and before type-synonym expansion, resp
490     -> Type -> Type          -- RHS (ty2),   after and before type-synonym expansion, resp
491     -> TcS (StopOrContinue Ct)
492 -- See Note [Canonicalising type applications]
493 can_eq_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
494   =  do { traceTcS "can_eq_app 1" $
495           vcat [ ppr ev, ppr swapped, ppr s1, ppr t1, ppr ty2 ]
496         ; let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
497         ; (xi_s1, co_s1) <- flatten fmode s1
498         ; traceTcS "can_eq_app 2" $ vcat [ ppr ev, ppr xi_s1 ]
499         ; if s1 `tcEqType` xi_s1
500           then can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
501           else
502      do { (xi_t1, co_t1) <- flatten fmode t1
503              -- We flatten t1 as well so that (xi_s1 xi_t1) is well-kinded
504              -- If we form (xi_s1 t1) that might (appear) ill-kinded, 
505              -- and then crash in a call to typeKind
506         ; let xi1 = mkAppTy xi_s1 xi_t1
507               co1 = mkTcAppCo co_s1 co_t1
508         ; traceTcS "can_eq_app 3" $ vcat [ ppr ev, ppr xi1, ppr co1 ]
509         ; mb_ct <- rewriteEqEvidence ev swapped xi1 ps_ty2 
510                                      co1 (mkTcNomReflCo ps_ty2)
511         ; traceTcS "can_eq_app 4" $ vcat [ ppr ev, ppr xi1, ppr co1 ]
512         ; case mb_ct of
513             Stop ev s           -> return (Stop ev s)
514             ContinueWith new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }}
515
516 -- Preconditions: s1  is already flattened
517 --                ty2 is not a type variable, so flattening
518 --                    can't turn it into an application if it
519 --                    doesn't look like one already
520 -- See Note [Canonicalising type applications]
521 can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
522   | Just (s2,t2) <- tcSplitAppTy_maybe ty2
523   = unSwap swapped decompose_it (s1,t1) (s2,t2)
524   | otherwise
525   = unSwap swapped (canEqFailure ev) ps_ty1 ps_ty2
526   where
527     decompose_it (s1,t1) (s2,t2) 
528       = do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
529                  xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
530                  xevdecomp x = let xco = evTermCoercion x
531                                in [ EvCoercion (mkTcLRCo CLeft xco)
532                                   , EvCoercion (mkTcLRCo CRight xco)]
533            ; xCtEvidence ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp)
534            ; stopWith ev "Decomposed AppTy" }
535
536
537 ------------------------
538 canDecomposableTyConApp :: CtEvidence
539                         -> TyCon -> [TcType]
540                         -> TyCon -> [TcType]
541                         -> TcS (StopOrContinue Ct)
542 canDecomposableTyConApp ev tc1 tys1 tc2 tys2
543   | tc1 /= tc2 || length tys1 /= length tys2
544     -- Fail straight away for better error messages
545   = canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
546   | otherwise
547   = do { traceTcS "canDecomposableTyConApp" (ppr ev $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
548        ; canDecomposableTyConAppOK ev tc1 tys1 tys2 }
549
550 canDecomposableTyConAppOK :: CtEvidence
551                           -> TyCon -> [TcType] -> [TcType]
552                           -> TcS (StopOrContinue Ct)
553
554 canDecomposableTyConAppOK ev tc1 tys1 tys2
555   = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
556              xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
557              xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
558        ; xCtEvidence ev xev
559        ; stopWith ev "Decomposed TyConApp" }
560
561 canEqFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct)
562 -- See Note [Make sure that insolubles are fully rewritten]
563 canEqFailure ev ty1 ty2
564   = do { let fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly }
565        ; (s1, co1) <- flatten fmode ty1
566        ; (s2, co2) <- flatten fmode ty2
567        ; mb_ct <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
568        ; case mb_ct of
569            ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev)
570                                      ; stopWith new_ev "Definitely not equal" }
571            Stop ev s -> pprPanic "canEqFailure" (s $$ ppr ev $$ ppr ty1 $$ ppr ty2) }
572 \end{code}
573
574 Note [Canonicalising type applications]
575 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
576 Given (s1 t1) ~ ty2, how should we proceed?
577 The simple things is to see if ty2 is of form (s2 t2), and 
578 decompose.  By this time s1 and s2 can't be saturated type
579 function applications, because those have been dealt with 
580 by an earlier equation in can_eq_nc, so it is always sound to 
581 decompose.
582
583 However, over-eager decomposition gives bad error messages 
584 for things like
585    a b ~ Maybe c
586    e f ~ p -> q
587 Suppose (in the first example) we already know a~Array.  Then if we
588 decompose the application eagerly, yielding
589    a ~ Maybe
590    b ~ c
591 we get an error        "Can't match Array ~ Maybe", 
592 but we'd prefer to get "Can't match Array b ~ Maybe c".
593
594 So instead can_eq_app flattens s1.  If flattening does something, it
595 rewrites, and goes round can_eq_nc again.  If flattening 
596 does nothing, then (at least with our present state of knowledge)
597 we can only decompose, and that is what can_eq_flat_app attempts
598 to do. 
599
600 Note [Make sure that insolubles are fully rewritten]
601 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
602 When an equality fails, we still want to rewrite the equality
603 all the way down, so that it accurately reflects
604  (a) the mutable reference substitution in force at start of solving
605  (b) any ty-binds in force at this point in solving
606 See Note [Kick out insolubles] in TcInteract.
607 And if we don't do this there is a bad danger that
608 TcSimplify.applyTyVarDefaulting will find a variable
609 that has in fact been substituted.
610
611 Note [Do not decompose Given polytype equalities]
612 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
613 Consider [G] (forall a. t1 ~ forall a. t2).  Can we decompose this?
614 No -- what would the evidence look like?  So instead we simply discard
615 this given evidence.
616
617
618 Note [Combining insoluble constraints]
619 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
620 As this point we have an insoluble constraint, like Int~Bool.
621
622  * If it is Wanted, delete it from the cache, so that subsequent
623    Int~Bool constraints give rise to separate error messages
624
625  * But if it is Derived, DO NOT delete from cache.  A class constraint
626    may get kicked out of the inert set, and then have its functional
627    dependency Derived constraints generated a second time. In that
628    case we don't want to get two (or more) error messages by
629    generating two (or more) insoluble fundep constraints from the same
630    class constraint.
631
632
633 \begin{code}
634 canCFunEqCan :: CtEvidence 
635              -> TyCon -> [TcType]   -- LHS
636              -> TcTyVar             -- RHS
637              -> TcS (StopOrContinue Ct)
638 -- ^ Canonicalise a CFunEqCan.  We know that 
639 --     the arg types are already flat, 
640 -- and the RHS is a fsk, which we must *not* substitute.
641 -- So just substitute in the LHS
642 canCFunEqCan ev fn tys fsk
643   = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
644        ; (tys', cos) <- flattenMany fmode tys
645                         -- cos :: tys' ~ tys
646        ; let lhs_co  = mkTcTyConAppCo Nominal fn cos
647                         -- :: F tys' ~ F tys
648              new_lhs = mkTyConApp fn tys'
649              fsk_ty  = mkTyVarTy fsk
650        ; mb_ev <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
651                                     lhs_co (mkTcNomReflCo fsk_ty)
652        ; case mb_ev of {
653            Stop ev s        -> return (Stop ev s) ;
654            ContinueWith ev' ->
655
656     do { extendFlatCache fn tys' (ctEvCoercion ev', fsk)
657        ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
658                                  , cc_tyargs = tys', cc_fsk = fsk }) } } }
659
660 ---------------------
661 canEqTyVar :: CtEvidence -> SwapFlag
662            -> TcTyVar
663            -> TcType -> TcType
664            -> TcS (StopOrContinue Ct)
665 -- A TyVar on LHS, but so far un-zonked
666 canEqTyVar ev swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
667   = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
668        ; mb_yes <- flattenTyVarOuter ev tv1
669        ; case mb_yes of
670            Right (ty1, co1, _) -- co1 :: ty1 ~ tv1
671                      -> do { mb <- rewriteEqEvidence ev swapped  ty1 ps_ty2
672                                                      co1 (mkTcNomReflCo ps_ty2)
673                            ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1,
674                                                            ppUnless (isDerived ev) (ppr co1)])
675                            ; case mb of
676                                Stop ev s           -> return (Stop ev s)
677                                ContinueWith new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 }
678
679            Left tv1' -> do { -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
680                              -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
681                                  -- Flatten the RHS less vigorously, to avoid gratuitous flattening
682                                  -- True <=> xi2 should not itself be a type-function application
683                              let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
684                            ; (xi2, co2) <- flatten fmode ps_ty2 -- co2 :: xi2 ~ ps_ty2
685                                            -- Use ps_ty2 to preserve type synonyms if poss
686                            ; dflags <- getDynFlags
687                            ; canEqTyVar2 dflags ev swapped tv1' xi2 co2 } }
688
689 canEqTyVar2 :: DynFlags
690             -> CtEvidence   -- olhs ~ orhs (or, if swapped, orhs ~ olhs)
691             -> SwapFlag
692             -> TcTyVar      -- olhs
693             -> TcType       -- nrhs
694             -> TcCoercion   -- nrhs ~ orhs
695             -> TcS (StopOrContinue Ct)
696 -- LHS is an inert type variable, 
697 -- and RHS is fully rewritten, but with type synonyms
698 -- preserved as much as possible
699
700 canEqTyVar2 dflags ev swapped tv1 xi2 co2
701   | Just tv2 <- getTyVar_maybe xi2
702   = canEqTyVarTyVar ev swapped tv1 tv2 co2
703
704   | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2  -- No occurs check
705   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2' co1 co2
706                 -- Ensure that the new goal has enough type synonyms
707                 -- expanded by the occurCheckExpand; hence using xi2' here
708                 -- See Note [occurCheckExpand]
709
710        ; let k1 = tyVarKind tv1
711              k2 = typeKind xi2'
712        ; case mb of
713             Stop ev s -> return (Stop ev s)
714             ContinueWith new_ev 
715                 | k2 `isSubKind` k1
716                 -- Establish CTyEqCan kind invariant
717                 -- Reorientation has done its best, but the kinds might
718                 -- simply be incompatible
719                 -> continueWith (CTyEqCan { cc_ev = new_ev
720                                           , cc_tyvar  = tv1, cc_rhs = xi2' })
721                 | otherwise
722                 -> incompatibleKind new_ev xi1 k1 xi2' k2 }
723
724   | otherwise  -- Occurs check error
725   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2
726        ; case mb of
727            Stop ev s           -> return (Stop ev s)
728            ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev)
729               -- If we have a ~ [a], it is not canonical, and in particular
730               -- we don't want to rewrite existing inerts with it, otherwise
731               -- we'd risk divergence in the constraint solver
732                                      ; stopWith new_ev "Occurs check" } }
733   where
734     xi1 = mkTyVarTy tv1
735     co1 = mkTcNomReflCo xi1
736
737
738
739 canEqTyVarTyVar :: CtEvidence           -- tv1 ~ orhs (or orhs ~ tv1, if swapped)
740                 -> SwapFlag
741                 -> TcTyVar -> TcTyVar   -- tv2, tv2
742                 -> TcCoercion           -- tv2 ~ orhs
743                 -> TcS (StopOrContinue Ct)
744 -- Both LHS and RHS rewrote to a type variable,
745 -- If swapped = NotSwapped, then
746 --     rw_orhs = tv1, rw_olhs = orhs
747 --     rw_nlhs = tv2, rw_nrhs = xi1
748 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
749 canEqTyVarTyVar ev swapped tv1 tv2 co2
750   | tv1 == tv2
751   = do { when (isWanted ev) $
752          ASSERT( tcCoercionRole co2 == Nominal )
753          setEvBind (ctev_evar ev) (EvCoercion (maybeSym swapped co2))
754        ; stopWith ev "Equal tyvars" }
755
756   | incompat_kind   = incompat
757   | isFmvTyVar tv1  = do_fmv swapped            tv1 xi1 xi2 co1 co2
758   | isFmvTyVar tv2  = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
759   | same_kind       = if swap_over then do_swap else no_swap
760   | k1_sub_k2       = do_swap   -- Note [Kind orientation for CTyEqCan]
761   | otherwise       = no_swap   -- k2_sub_k1
762   where
763     xi1 = mkTyVarTy tv1
764     xi2 = mkTyVarTy tv2
765     k1  = tyVarKind tv1
766     k2  = tyVarKind tv2
767     co1 = mkTcNomReflCo xi1
768     k1_sub_k2     = k1 `isSubKind` k2
769     k2_sub_k1     = k2 `isSubKind` k1
770     same_kind     = k1_sub_k2 && k2_sub_k1
771     incompat_kind = not (k1_sub_k2 || k2_sub_k1)
772
773     no_swap = canon_eq swapped            tv1 xi1 xi2 co1 co2
774     do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
775
776     canon_eq swapped tv1 xi1 xi2 co1 co2
777         -- ev  : tv1 ~ orhs  (not swapped) or   orhs ~ tv1   (swapped)
778         -- co1 : xi1 ~ tv1
779         -- co2 : xi2 ~ tv2
780       = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2
781            ; let mk_ct ev' = CTyEqCan { cc_ev = ev', cc_tyvar = tv1, cc_rhs = xi2 }
782            ; return (fmap mk_ct mb) }
783
784     -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten
785     do_fmv swapped tv1 xi1 xi2 co1 co2
786       | same_kind
787       = canon_eq swapped tv1 xi1 xi2 co1 co2
788       | otherwise  -- Presumably tv1 `subKind` tv2, which is the wrong way round
789       = ASSERT2( k1_sub_k2, ppr tv1 $$ ppr tv2 )
790         ASSERT2( isWanted ev, ppr ev )  -- Only wanteds have flatten meta-vars
791         do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
792            ; new_ev <- newWantedEvVarNC (ctEvLoc ev) (mkTcEqPred tv_ty xi2)
793            ; emitWorkNC [new_ev]
794            ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev `mkTcTransCo` co2) }
795
796     incompat
797       = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 (mkTcNomReflCo xi1) co2
798            ; case mb of
799                Stop ev s        -> return (Stop ev s)
800                ContinueWith ev' -> incompatibleKind ev' xi1 k1 xi2 k2 }
801
802     swap_over
803       -- If tv1 is touchable, swap only if tv2 is also
804       -- touchable and it's strictly better to update the latter
805       -- But see Note [Avoid unnecessary swaps]
806       | Just lvl1 <- metaTyVarUntouchables_maybe tv1
807       = case metaTyVarUntouchables_maybe tv2 of
808           Nothing   -> False
809           Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
810                     | lvl1 `strictlyDeeperThan` lvl2 -> False
811                     | otherwise                      -> nicer_to_update_tv2
812
813       -- So tv1 is not a meta tyvar
814       -- If only one is a meta tyvar, put it on the left
815       -- This is not because it'll be solved; but becuase
816       -- the floating step looks for meta tyvars on the left
817       | isMetaTyVar tv2 = True
818
819       -- So neither is a meta tyvar
820
821       -- If only one is a flatten tyvar, put it on the left
822       -- See Note [Eliminate flat-skols]
823       | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
824
825       | otherwise = False
826
827     nicer_to_update_tv2
828       =  (isSigTyVar tv1                 && not (isSigTyVar tv2))
829       || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
830
831 incompatibleKind :: CtEvidence         -- t1~t2
832                  -> TcType -> TcKind
833                  -> TcType -> TcKind   -- s1~s2, flattened and zonked
834                  -> TcS (StopOrContinue Ct)
835 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
836 --       CIrredEvCan (NOT CTyEqCan or CFunEqCan)
837 -- for the type equality; and continue with the kind equality constraint.
838 -- When the latter is solved, it'll kick out the irreducible equality for
839 -- a second attempt at solving
840 --
841 -- See Note [Equalities with incompatible kinds]
842
843 incompatibleKind new_ev s1 k1 s2 k2   -- See Note [Equalities with incompatible kinds]
844   = ASSERT( isKind k1 && isKind k2 )
845     do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
846
847          -- Create a derived kind-equality, and solve it
848        ; emitNewDerived kind_co_loc (mkTcEqPred k1 k2)
849
850          -- Put the not-currently-soluble thing into the inert set
851        ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
852   where
853     loc = ctEvLoc new_ev
854     kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
855 \end{code}
856
857 Note [Canonical orientation for tyvar/tyvar equality constraints]
858 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
859 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
860 round should be oriented in the CTyEqCan?  The rules, implemented by
861 canEqTyVarTyVar, are these
862
863  * If either is a flatten-meta-variables, it goes on the left.
864
865  * If one is a strict sub-kind of the other e.g.
866        (alpha::?) ~ (beta::*)
867    orient them so RHS is a subkind of LHS.  That way we will replace
868    'a' with 'b', correctly narrowing the kind.
869    This establishes the subkind invariant of CTyEqCan.
870
871  * Put a meta-tyvar on the left if possible
872        alpha[3] ~ r
873
874  * If both are meta-tyvars, put the more touchable one (deepest level
875    number) on the left, so there is the best chance of unifying it
876         alpha[3] ~ beta[2]
877
878  * If both are meta-tyvars and both at the same level, put a SigTv
879    on the right if possible
880         alpha[2] ~ beta[2](sig-tv)
881    That way, when we unify alpha := beta, we don't lose the SigTv flag.
882
883  * Put a meta-tv with a System Name on the left if possible so it
884    gets eliminated (improves error messages)
885
886  * If one is a flatten-skolem, put it on the left so that it is
887    substituted out  Note [Elminate flat-skols]
888         fsk ~ a
889
890 Note [Avoid unnecessary swaps]
891 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
892 If we swap without actually improving matters, we can get an infnite loop.
893 Consider
894     work item:  a ~ b
895    inert item:  b ~ c
896 We canonicalise the work-time to (a ~ c).  If we then swap it before
897 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
898 inert guy, so we get
899    new work item:  b ~ c
900    inert item:     c ~ a
901 And now the cycle just repeats
902
903 Note [Eliminate flat-skols]
904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
905 Suppose we have  [G] Num (F [a])
906 then we flatten to
907      [G] Num fsk
908      [G] F [a] ~ fsk
909 where fsk is a flatten-skolem (FlatSkol). Suppose we have
910       type instance F [a] = a
911 then we'll reduce the second constraint to
912      [G] a ~ fsk
913 and then replace all uses of 'a' with fsk.  That's bad because
914 in error messages intead of saying 'a' we'll say (F [a]).  In all
915 places, including those where the programmer wrote 'a' in the first
916 place.  Very confusing!  See Trac #7862.
917
918 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
919 the fsk.
920
921 Note [Equalities with incompatible kinds]
922 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
923 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
924 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
925 CFunEqCan.  What if we try to unify two things with incompatible
926 kinds?
927
928 eg    a ~ b  where a::*, b::*->*
929 or    a ~ b  where a::*, b::k, k is a kind variable
930
931 The CTyEqCan compatKind invariant is important.  If we make a CTyEqCan
932 for a~b, then we might well *substitute* 'b' for 'a', and that might make
933 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
934 Trac #7696).
935
936 So instead for these ill-kinded equalities we generate a CIrredCan,
937 and put it in the inert set, which keeps it out of the way until a
938 subsequent substitution (on kind variables, say) re-activates it.
939
940 NB: it is important that the types s1,s2 are flattened and zonked
941     so that their kinds k1, k2 are inert wrt the substitution.  That
942     means that they can only become the same if we change the inert
943     set, which in turn will kick out the irreducible equality
944     E.g. it is WRONG to make an irred (a:k1)~(b:k2)
945          if we already have a substitution k1:=k2
946
947 NB: it's important that the new CIrredCan goes in the inert set rather
948 than back into the work list. We used to do the latter, but that led
949 to an infinite loop when we encountered it again, and put it back in
950 the work list again.
951
952 See also Note [Kind orientation for CTyEqCan] and
953          Note [Kind orientation for CFunEqCan] in TcRnTypes
954
955 Note [Type synonyms and canonicalization]
956 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
957 We treat type synonym applications as xi types, that is, they do not
958 count as type function applications.  However, we do need to be a bit
959 careful with type synonyms: like type functions they may not be
960 generative or injective.  However, unlike type functions, they are
961 parametric, so there is no problem in expanding them whenever we see
962 them, since we do not need to know anything about their arguments in
963 order to expand them; this is what justifies not having to treat them
964 as specially as type function applications.  The thing that causes
965 some subtleties is that we prefer to leave type synonym applications
966 *unexpanded* whenever possible, in order to generate better error
967 messages.
968
969 If we encounter an equality constraint with type synonym applications
970 on both sides, or a type synonym application on one side and some sort
971 of type application on the other, we simply must expand out the type
972 synonyms in order to continue decomposing the equality constraint into
973 primitive equality constraints.  For example, suppose we have
974
975   type F a = [Int]
976
977 and we encounter the equality
978
979   F a ~ [b]
980
981 In order to continue we must expand F a into [Int], giving us the
982 equality
983
984   [Int] ~ [b]
985
986 which we can then decompose into the more primitive equality
987 constraint
988
989   Int ~ b.
990
991 However, if we encounter an equality constraint with a type synonym
992 application on one side and a variable on the other side, we should
993 NOT (necessarily) expand the type synonym, since for the purpose of
994 good error messages we want to leave type synonyms unexpanded as much
995 as possible.  Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
996
997
998 Note [occurCheckExpand]
999 ~~~~~~~~~~~~~~~~~~~~~~~
1000 There is a subtle point with type synonyms and the occurs check that
1001 takes place for equality constraints of the form tv ~ xi.  As an
1002 example, suppose we have
1003
1004   type F a = Int
1005
1006 and we come across the equality constraint
1007
1008   a ~ F a
1009
1010 This should not actually fail the occurs check, since expanding out
1011 the type synonym results in the legitimate equality constraint a ~
1012 Int.  We must actually do this expansion, because unifying a with F a
1013 will lead the type checker into infinite loops later.  Put another
1014 way, canonical equality constraints should never *syntactically*
1015 contain the LHS variable in the RHS type.  However, we don't always
1016 need to expand type synonyms when doing an occurs check; for example,
1017 the constraint
1018
1019   a ~ F b
1020
1021 is obviously fine no matter what F expands to. And in this case we
1022 would rather unify a with F b (rather than F b's expansion) in order
1023 to get better error messages later.
1024
1025 So, when doing an occurs check with a type synonym application on the
1026 RHS, we use some heuristics to find an expansion of the RHS which does
1027 not contain the variable from the LHS.  In particular, given
1028
1029   a ~ F t1 ... tn
1030
1031 we first try expanding each of the ti to types which no longer contain
1032 a.  If this turns out to be impossible, we next try expanding F
1033 itself, and so on.  See Note [Occurs check expansion] in TcType
1034