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