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