Implememt -fdefer-type-errors (Trac #5624)
[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) $ wrapErrTcS $ 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 -- If one side is a variable, orient and flatten,
822 -- WITHOUT expanding type synonyms, so that we tend to 
823 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@
824 canEq d fl eqv ty1@(TyVarTy {}) ty2 
825   = canEqLeaf d fl eqv ty1 ty2
826 canEq d fl eqv ty1 ty2@(TyVarTy {})
827   = canEqLeaf d fl eqv ty1 ty2
828
829 -- See Note [Naked given applications]
830 canEq d fl eqv ty1 ty2
831   | Just ty1' <- tcView ty1 = canEq d fl eqv ty1' ty2
832   | Just ty2' <- tcView ty2 = canEq d fl eqv ty1  ty2'
833
834 canEq d fl eqv ty1@(TyConApp fn tys) ty2 
835   | isSynFamilyTyCon fn, length tys == tyConArity fn
836   = canEqLeaf d fl eqv ty1 ty2
837 canEq d fl eqv ty1 ty2@(TyConApp fn tys)
838   | isSynFamilyTyCon fn, length tys == tyConArity fn
839   = canEqLeaf d fl eqv ty1 ty2
840
841 canEq d fl eqv ty1 ty2
842   | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
843   , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
844   , isDecomposableTyCon tc1 && isDecomposableTyCon tc2
845   = -- Generate equalities for each of the corresponding arguments
846     if (tc1 /= tc2 || length tys1 /= length tys2)
847     -- Fail straight away for better error messages
848     then canEqFailure d fl eqv
849     else do {
850          let (kis1,  tys1') = span isKind tys1
851              (_kis2, tys2') = span isKind tys2
852              kicos          = map mkTcReflCo kis1
853
854        ; argeqvs <- zipWithM (newEqVar fl) tys1' tys2'
855        ; fls <- case fl of 
856            Wanted {} -> 
857              do { _ <- setEqBind eqv
858                          (mkTcTyConAppCo tc1 (kicos ++ map (mkTcCoVarCo . evc_the_evvar) argeqvs)) fl
859                 ; return (map (\_ -> fl) argeqvs) }
860            Given {} ->
861              let do_one argeqv n = setEqBind (evc_the_evvar argeqv) 
862                                              (mkTcNthCo n (mkTcCoVarCo eqv)) fl
863              in zipWithM do_one argeqvs [(length kicos)..]
864            Derived {} -> return (map (\_ -> fl) argeqvs)
865
866        ; canEqEvVarsCreated d fls argeqvs tys1' tys2' }
867
868 -- See Note [Equality between type applications]
869 --     Note [Care with type applications] in TcUnify
870 canEq d fl eqv ty1 ty2    -- e.g.  F a b ~ Maybe c
871                           -- where F has arity 1
872   | Just (s1,t1) <- tcSplitAppTy_maybe ty1
873   , Just (s2,t2) <- tcSplitAppTy_maybe ty2
874   = canEqAppTy d fl eqv s1 t1 s2 t2
875
876 canEq d fl eqv s1@(ForAllTy {}) s2@(ForAllTy {})
877  | tcIsForAllTy s1, tcIsForAllTy s2, 
878    Wanted {} <- fl 
879  = canEqFailure d fl eqv
880  | otherwise
881  = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
882       ; return Stop }
883
884 canEq d fl eqv _ _                               = canEqFailure d fl eqv
885
886 -- Type application
887 canEqAppTy :: SubGoalDepth 
888            -> CtFlavor -> EqVar -> Type -> Type -> Type -> Type
889            -> TcS StopOrContinue
890 canEqAppTy d fl eqv s1 t1 s2 t2
891   = ASSERT( not (isKind t1) && not (isKind t2) )
892     if isGivenOrSolved fl then 
893         do { traceTcS "canEq (app case)" $
894                 text "Ommitting decomposition of given equality between: " 
895                     <+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2)
896                    -- We cannot decompose given applications
897                    -- because we no longer have 'left' and 'right'
898            ; return Stop }
899     else
900         do { evc1 <- newEqVar fl s1 s2
901            ; evc2 <- newEqVar fl t1 t2
902            ; let eqv1 = evc_the_evvar evc1
903                  eqv2 = evc_the_evvar evc2
904  
905            ; when (isWanted fl) $
906                   do { _ <- setEqBind eqv (mkTcAppCo (mkTcCoVarCo eqv1) (mkTcCoVarCo eqv2)) fl
907                      ; return () }
908            
909            ; canEqEvVarsCreated d [fl,fl] [evc1,evc2] [s1,t1] [s2,t2] }
910
911 canEqFailure :: SubGoalDepth 
912              -> CtFlavor -> EvVar -> TcS StopOrContinue
913 canEqFailure d fl eqv 
914   = do { when (isWanted fl) (delCachedEvVar eqv fl) 
915           -- See Note [Combining insoluble constraints]
916        ; emitFrozenError fl eqv d
917        ; return Stop }
918 \end{code}
919
920 Note [Combining insoluble constraints]
921 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
922 As this point we have an insoluble constraint, like Int~Bool.
923
924  * If it is Wanted, delete it from the cache, so that subsequent
925    Int~Bool constraints give rise to separate error messages
926
927  * But if it is Derived, DO NOT delete from cache.  A class constraint
928    may get kicked out of the inert set, and then have its functional
929    dependency Derived constraints generated a second time. In that
930    case we don't want to get two (or more) error messages by
931    generating two (or more) insoluble fundep constraints from the same
932    class constraint.
933    
934
935 Note [Naked given applications]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 Consider: 
938    data A a 
939    type T a = A a 
940 and the given equality:  
941    [G] A a ~ T Int 
942 We will reach the case canEq where we do a tcSplitAppTy_maybe, but if
943 we dont have the guards (Nothing <- tcView ty1) (Nothing <- tcView
944 ty2) then the given equation is going to fall through and get
945 completely forgotten!
946
947 What we want instead is this clause to apply only when there is no
948 immediate top-level synonym; if there is one it will be later on
949 unfolded by the later stages of canEq.
950
951 Test-case is in typecheck/should_compile/GivenTypeSynonym.hs
952
953
954 Note [Equality between type applications]
955 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
956 If we see an equality of the form s1 t1 ~ s2 t2 we can always split
957 it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
958 functions (type functions use the TyConApp constructor, which never
959 shows up as the LHS of an AppTy).  Other than type functions, types
960 in Haskell are always 
961
962   (1) generative: a b ~ c d implies a ~ c, since different type
963       constructors always generate distinct types
964
965   (2) injective: a b ~ a d implies b ~ d; we never generate the
966       same type from different type arguments.
967
968
969 Note [Canonical ordering for equality constraints]
970 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
971 Implemented as (<+=) below:
972
973   - Type function applications always come before anything else.  
974   - Variables always come before non-variables (other than type
975       function applications).
976
977 Note that we don't need to unfold type synonyms on the RHS to check
978 the ordering; that is, in the rules above it's OK to consider only
979 whether something is *syntactically* a type function application or
980 not.  To illustrate why this is OK, suppose we have an equality of the
981 form 'tv ~ S a b c', where S is a type synonym which expands to a
982 top-level application of the type function F, something like
983
984   type S a b c = F d e
985
986 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
987 expansion contains type function applications the flattener will do
988 the expansion and then generate a skolem variable for the type
989 function application, so we end up with something like this:
990
991   tv ~ x
992   F d e ~ x
993
994 where x is the skolem variable.  This is one extra equation than
995 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
996 if we had noticed that S expanded to a top-level type function
997 application and flipped it around in the first place) but this way
998 keeps the code simpler.
999
1000 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
1001 ordering of tv ~ tv constraints.  There are several reasons why we
1002 might:
1003
1004   (1) In order to be able to extract a substitution that doesn't
1005       mention untouchable variables after we are done solving, we might
1006       prefer to put touchable variables on the left. However, in and
1007       of itself this isn't necessary; we can always re-orient equality
1008       constraints at the end if necessary when extracting a substitution.
1009
1010   (2) To ensure termination we might think it necessary to put
1011       variables in lexicographic order. However, this isn't actually 
1012       necessary as outlined below.
1013
1014 While building up an inert set of canonical constraints, we maintain
1015 the invariant that the equality constraints in the inert set form an
1016 acyclic rewrite system when viewed as L-R rewrite rules.  Moreover,
1017 the given constraints form an idempotent substitution (i.e. none of
1018 the variables on the LHS occur in any of the RHS's, and type functions
1019 never show up in the RHS at all), the wanted constraints also form an
1020 idempotent substitution, and finally the LHS of a given constraint
1021 never shows up on the RHS of a wanted constraint.  There may, however,
1022 be a wanted LHS that shows up in a given RHS, since we do not rewrite
1023 given constraints with wanted constraints.
1024
1025 Suppose we have an inert constraint set
1026
1027
1028   tg_1 ~ xig_1         -- givens
1029   tg_2 ~ xig_2
1030   ...
1031   tw_1 ~ xiw_1         -- wanteds
1032   tw_2 ~ xiw_2
1033   ...
1034
1035 where each t_i can be either a type variable or a type function
1036 application. Now suppose we take a new canonical equality constraint,
1037 t' ~ xi' (note among other things this means t' does not occur in xi')
1038 and try to react it with the existing inert set.  We show by induction
1039 on the number of t_i which occur in t' ~ xi' that this process will
1040 terminate.
1041
1042 There are several ways t' ~ xi' could react with an existing constraint:
1043
1044 TODO: finish this proof.  The below was for the case where the entire
1045 inert set is an idempotent subustitution...
1046
1047 (b) We could have t' = t_j for some j.  Then we obtain the new
1048     equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j.  We
1049     now canonicalize the new equality, which may involve decomposing it
1050     into several canonical equalities, and recurse on these.  However,
1051     none of the new equalities will contain t_j, so they have fewer
1052     occurrences of the t_i than the original equation.
1053
1054 (a) We could have t_j occurring in xi' for some j, with t' /=
1055     t_j. Then we substitute xi_j for t_j in xi' and continue.  However,
1056     since none of the t_i occur in xi_j, we have decreased the
1057     number of t_i that occur in xi', since we eliminated t_j and did not
1058     introduce any new ones.
1059
1060 \begin{code}
1061 data TypeClassifier 
1062   = FskCls TcTyVar      -- ^ Flatten skolem 
1063   | VarCls TcTyVar      -- ^ Non-flatten-skolem variable 
1064   | FunCls TyCon [Type] -- ^ Type function, exactly saturated
1065   | OtherCls TcType     -- ^ Neither of the above
1066
1067 {- Useless these days! 
1068 unClassify :: TypeClassifier -> TcType
1069 unClassify (VarCls tv)      = TyVarTy tv
1070 unClassify (FskCls tv) = TyVarTy tv 
1071 unClassify (FunCls fn tys)  = TyConApp fn tys
1072 unClassify (OtherCls ty)    = ty
1073 -} 
1074
1075 classify :: TcType -> TypeClassifier
1076
1077 classify (TyVarTy tv) 
1078   | isTcTyVar tv, 
1079     FlatSkol {} <- tcTyVarDetails tv = FskCls tv
1080   | otherwise                        = VarCls tv
1081 classify (TyConApp tc tys) | isSynFamilyTyCon tc
1082                            , tyConArity tc == length tys
1083                            = FunCls tc tys
1084 classify ty                | Just ty' <- tcView ty
1085                            = case classify ty' of
1086                                OtherCls {} -> OtherCls ty
1087                                var_or_fn   -> var_or_fn
1088                            | otherwise 
1089                            = OtherCls ty
1090
1091 -- See note [Canonical ordering for equality constraints].
1092 reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool        
1093 -- (t1 `reOrient` t2) responds True 
1094 --   iff we should flip to (t2~t1)
1095 -- We try to say False if possible, to minimise evidence generation
1096 --
1097 -- Postcondition: After re-orienting, first arg is not OTherCls
1098 reOrient _fl (OtherCls {}) (FunCls {})   = True
1099 reOrient _fl (OtherCls {}) (FskCls {})   = True
1100 reOrient _fl (OtherCls {}) (VarCls {})   = True
1101 reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient"  -- One must be Var/Fun
1102
1103 reOrient _fl (FunCls {})   (VarCls _tv)  = False  
1104   -- But consider the following variation: isGiven fl && isMetaTyVar tv
1105
1106   -- See Note [No touchables as FunEq RHS] in TcSMonad
1107 reOrient _fl (FunCls {}) _                = False             -- Fun/Other on rhs
1108
1109 reOrient _fl (VarCls {}) (FunCls {})      = True 
1110
1111 reOrient _fl (VarCls {}) (FskCls {})      = False
1112
1113 reOrient _fl (VarCls {})  (OtherCls {})   = False
1114 reOrient _fl (VarCls tv1)  (VarCls tv2)  
1115   | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True 
1116   | otherwise                                = False 
1117   -- Just for efficiency, see CTyEqCan invariants 
1118
1119 reOrient _fl (FskCls {}) (VarCls tv2)     = isMetaTyVar tv2 
1120   -- Just for efficiency, see CTyEqCan invariants
1121
1122 reOrient _fl (FskCls {}) (FskCls {})     = False
1123 reOrient _fl (FskCls {}) (FunCls {})     = True 
1124 reOrient _fl (FskCls {}) (OtherCls {})   = False 
1125
1126 ------------------
1127
1128 canEqLeaf :: SubGoalDepth -- Depth
1129           -> CtFlavor -> EqVar 
1130           -> Type -> Type 
1131           -> TcS StopOrContinue
1132 -- Canonicalizing "leaf" equality constraints which cannot be
1133 -- decomposed further (ie one of the types is a variable or
1134 -- saturated type function application).  
1135
1136 -- Preconditions: 
1137 --    * one of the two arguments is variable or family applications
1138 --    * the two types are not equal (looking through synonyms)
1139 canEqLeaf d fl eqv s1 s2 
1140   | cls1 `re_orient` cls2
1141   = do { traceTcS "canEqLeaf (reorienting)" $ ppr eqv <+> dcolon <+> pprEq s1 s2
1142        ; delCachedEvVar eqv fl
1143        ; evc <- newEqVar fl s2 s1
1144        ; let eqv' = evc_the_evvar evc
1145        ; fl' <- case fl of 
1146            Wanted {}  -> setEqBind eqv (mkTcSymCo (mkTcCoVarCo eqv')) fl 
1147            Given {}   -> setEqBind eqv' (mkTcSymCo (mkTcCoVarCo eqv)) fl 
1148            Derived {} -> return fl 
1149        ; if isNewEvVar evc then 
1150              do { canEqLeafOriented d fl' eqv' s2 s1 }
1151          else return Stop 
1152        }
1153   | otherwise
1154   = do { traceTcS "canEqLeaf" $ ppr (mkEqPred (s1,s2))
1155        ; canEqLeafOriented d fl eqv s1 s2 }
1156   where
1157     re_orient = reOrient fl 
1158     cls1 = classify s1
1159     cls2 = classify s2
1160
1161 canEqLeafOriented :: SubGoalDepth -- Depth
1162                   -> CtFlavor -> EqVar 
1163                   -> TcType -> TcType -> TcS StopOrContinue
1164 -- By now s1 will either be a variable or a type family application
1165 canEqLeafOriented d fl eqv s1 s2
1166   = can_eq_split_lhs d fl eqv s1 s2
1167   where can_eq_split_lhs d fl eqv s1 s2
1168           | Just (fn,tys1) <- splitTyConApp_maybe s1
1169           = canEqLeafFunEqLeftRec d fl eqv (fn,tys1) s2
1170           | Just tv <- getTyVar_maybe s1
1171           = canEqLeafTyVarLeftRec d fl eqv tv s2
1172           | otherwise
1173           = pprPanic "canEqLeafOriented" $
1174             text "Non-variable or non-family equality LHS" <+> 
1175                  ppr eqv <+> dcolon <+> ppr (evVarPred eqv)
1176
1177 canEqLeafFunEqLeftRec :: SubGoalDepth
1178                       -> CtFlavor 
1179                       -> EqVar 
1180                       -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
1181 canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2  -- eqv :: F tys1 ~ ty2
1182   = do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
1183        ; (xis1,cos1) <- 
1184            {-# SCC "flattenMany" #-}
1185            flattenMany d fl tys1 -- Flatten type function arguments
1186                                  -- cos1 :: xis1 ~ tys1
1187
1188 --       ; inerts <- getTcSInerts
1189 --        ; let fam_eqs   = inert_funeqs inerts
1190
1191        ; let flat_ty = mkTyConApp fn xis1
1192
1193        ; is_cached <- getCachedFlatEq fn xis1 fl WhenSolved
1194                       -- Lookup if we have solved this goal already
1195 {-
1196        ; let is_cached = {-# SCC "lookupFunEq" #-} 
1197                          lookupFunEq flat_ty fl fam_eqs
1198 -}
1199        ; let no_flattening = all isTcReflCo cos1
1200                       
1201        ; if no_flattening && isNothing is_cached then 
1202              canEqLeafFunEqLeft d fl eqv (fn,xis1) ty2
1203          else do
1204        { let (final_co, final_ty)
1205                  | no_flattening        -- Just in inerts
1206                  , Just (rhs_ty, ret_eq) <- is_cached
1207                  = (mkTcSymCo ret_eq, rhs_ty)
1208                  | Nothing <- is_cached -- Just flattening
1209                  = (mkTcTyConAppCo fn cos1, flat_ty)
1210                  | Just (rhs_ty, ret_eq) <- is_cached  -- Both
1211                  = (mkTcSymCo ret_eq `mkTcTransCo` mkTcTyConAppCo fn cos1, rhs_ty)
1212                  | otherwise = panic "No flattening and not cached!"
1213        ; delCachedEvVar eqv fl
1214        ; evc <- newEqVar fl final_ty ty2
1215        ; let new_eqv = evc_the_evvar evc
1216        ; fl' <- case fl of
1217            Wanted {}  -> setEqBind eqv 
1218                            (mkTcSymCo final_co `mkTcTransCo` (mkTcCoVarCo new_eqv)) fl
1219            Given {}   -> setEqBind new_eqv (final_co `mkTcTransCo` (mkTcCoVarCo eqv)) fl
1220            Derived {} -> return fl
1221        ; if isNewEvVar evc then
1222              if isNothing is_cached then
1223                  {-# SCC "canEqLeafFunEqLeft" #-}
1224                  canEqLeafFunEqLeft d fl' new_eqv (fn,xis1) ty2
1225              else
1226                  canEq (d+1) fl' new_eqv final_ty ty2
1227          else return Stop
1228        }
1229        }
1230
1231 lookupFunEq :: PredType -> CtFlavor -> TypeMap Ct -> Maybe (TcType, TcCoercion)
1232 lookupFunEq pty fl fam_eqs = lookup_funeq pty fam_eqs
1233   where lookup_funeq pty fam_eqs
1234           | Just ct <- lookupTM pty fam_eqs
1235           , cc_flavor ct `canRewrite` fl 
1236           = Just (cc_rhs ct, mkTcCoVarCo (cc_id ct))
1237           | otherwise 
1238           = Nothing
1239
1240 canEqLeafFunEqLeft :: SubGoalDepth -- Depth
1241                    -> CtFlavor -> EqVar -> (TyCon,[Xi]) 
1242                    -> TcType -> TcS StopOrContinue
1243 -- Precondition: No more flattening is needed for the LHS
1244 canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
1245  = {-# SCC "canEqLeafFunEqLeft" #-}
1246    do { traceTcS "canEqLeafFunEqLeft" $ pprEq (mkTyConApp fn xis1) s2
1247       ; (xi2,co2) <- 
1248           {-# SCC "flatten" #-} 
1249           flatten d fl s2 -- co2 :: xi2 ~ s2
1250       ; let no_flattening_happened = isTcReflCo co2
1251       ; if no_flattening_happened then 
1252             continueWith $ CFunEqCan { cc_id     = eqv
1253                                      , cc_flavor = fl
1254                                      , cc_fun    = fn
1255                                      , cc_tyargs = xis1 
1256                                      , cc_rhs    = xi2 
1257                                      , cc_depth  = d }
1258         else do { delCachedEvVar eqv fl
1259                 ; evc <- 
1260                     {-# SCC "newEqVar" #-}
1261                     newEqVar fl (mkTyConApp fn xis1) xi2
1262                 ; let new_eqv = evc_the_evvar evc -- F xis1 ~ xi2 
1263                       new_cv  = mkTcCoVarCo new_eqv
1264                       cv      = mkTcCoVarCo eqv    -- F xis1 ~ s2
1265                 ; fl' <- case fl of
1266                     Wanted {} -> setEqBind eqv (new_cv `mkTcTransCo` co2) fl 
1267                     Given {}  -> setEqBind new_eqv (cv `mkTcTransCo` mkTcSymCo co2) fl
1268                     Derived {} -> return fl
1269                 ; if isNewEvVar evc then 
1270                       do { continueWith $
1271                            CFunEqCan { cc_id = new_eqv
1272                                      , cc_flavor = fl'
1273                                      , cc_fun    = fn
1274                                      , cc_tyargs = xis1 
1275                                      , cc_rhs    = xi2 
1276                                      , cc_depth  = d } }
1277                   else return Stop }  }
1278
1279
1280 canEqLeafTyVarLeftRec :: SubGoalDepth
1281                       -> CtFlavor -> EqVar
1282                       -> TcTyVar -> TcType -> TcS StopOrContinue
1283 canEqLeafTyVarLeftRec d fl eqv tv s2              -- eqv :: tv ~ s2
1284   = do {  traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
1285        ; (xi1,co1) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv
1286        ; case isTcReflCo co1 of 
1287              True -- If reflco and variable, just go on
1288                | Just tv' <- getTyVar_maybe xi1 
1289                  -> canEqLeafTyVarLeft d fl eqv tv' s2
1290              _ -> -- If not a variable or not refl co, must rewrite and go on
1291                do { delCachedEvVar eqv fl
1292                   ; evc <- newEqVar fl xi1 s2  -- new_ev :: xi1 ~ s2
1293                   ; let new_ev = evc_the_evvar evc
1294                   ; fl' <- case fl of 
1295                     Wanted  {} -> setEqBind eqv 
1296                                     (mkTcSymCo co1 `mkTcTransCo` mkTcCoVarCo new_ev) fl
1297                     Given   {} -> setEqBind new_ev
1298                                     (co1 `mkTcTransCo` mkTcCoVarCo eqv) fl
1299                     Derived {} -> return fl
1300                   ; if isNewEvVar evc then
1301                       do { canEq d fl' new_ev xi1 s2 }
1302                     else return Stop
1303                   }
1304        }
1305
1306 canEqLeafTyVarLeft :: SubGoalDepth -- Depth
1307                    -> CtFlavor -> EqVar
1308                    -> TcTyVar -> TcType -> TcS StopOrContinue
1309 -- Precondition LHS is fully rewritten from inerts (but not RHS)
1310 canEqLeafTyVarLeft d fl eqv tv s2       -- eqv : tv ~ s2
1311   = do { traceTcS "canEqLeafTyVarLeft" (pprEq (mkTyVarTy tv) s2)
1312        ; (xi2, co) <- flatten d fl s2   -- Flatten RHS   co : xi2 ~ s2
1313                                                
1314        ; let no_flattening_happened = isTcReflCo co
1315              
1316        ; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv  =" <+> ppr tv
1317                                                      , text "s2  =" <+> ppr s2
1318                                                      , text "xi2 =" <+> ppr xi2]))
1319
1320                       -- Flattening the RHS may reveal an identity coercion, which should
1321                       -- not be reported as occurs check error! 
1322        ; let is_same_tv
1323                | Just tv' <- getTyVar_maybe xi2, tv' == tv
1324                = True
1325                | otherwise = False
1326        ; if is_same_tv then
1327              do { delCachedEvVar eqv fl
1328                 ; when (isWanted fl) $ 
1329                        do { _ <- setEqBind eqv co fl; return () }
1330                 ; return Stop }
1331          else
1332     do { -- Do an occurs check, and return a possibly
1333          -- unfolded version of the RHS, if we had to 
1334          -- unfold any type synonyms to get rid of tv.
1335          occ_check_result <- canOccursCheck fl tv xi2
1336
1337        ; let xi2'
1338               | Just xi2_unfolded <- occ_check_result
1339               = xi2_unfolded
1340               | otherwise = xi2
1341
1342
1343        ; if no_flattening_happened then
1344              if isNothing occ_check_result then 
1345                  canEqFailure d fl (setVarType eqv $ mkEqPred (mkTyVarTy tv, xi2'))
1346              else 
1347                  continueWith $ CTyEqCan { cc_id     = eqv
1348                                          , cc_flavor = fl
1349                                          , cc_tyvar  = tv
1350                                          , cc_rhs    = xi2'
1351                                          , cc_depth  = d }
1352          else -- Flattening happened, in any case we have to create new variable 
1353               -- even if we report an occurs check error
1354              do { delCachedEvVar eqv fl
1355                 ; evc <- newEqVar fl (mkTyVarTy tv) xi2' 
1356                 ; let eqv' = evc_the_evvar evc -- eqv' : tv ~ xi2'
1357                       cv   = mkTcCoVarCo eqv    -- cv : tv ~ s2
1358                       cv'  = mkTcCoVarCo eqv'   -- cv': tv ~ xi2'
1359                  ; fl' <- case fl of 
1360                      Wanted {}  -> setEqBind eqv (cv' `mkTcTransCo` co) fl         -- tv ~ xi2' ~ s2
1361                      Given {}   -> setEqBind eqv' (cv `mkTcTransCo` mkTcSymCo co) fl -- tv ~ s2 ~ xi2'
1362                      Derived {} -> return fl
1363
1364                  ; if isNewEvVar evc then 
1365                        if isNothing occ_check_result then 
1366                            canEqFailure d fl eqv'
1367                        else continueWith CTyEqCan { cc_id     = eqv'
1368                                                   , cc_flavor = fl'
1369                                                   , cc_tyvar  = tv
1370                                                   , cc_rhs    = xi2' 
1371                                                   , cc_depth  = d }
1372                    else 
1373                        return Stop } } }
1374
1375
1376 -- See Note [Type synonyms and canonicalization].
1377 -- Check whether the given variable occurs in the given type.  We may
1378 -- have needed to do some type synonym unfolding in order to get rid
1379 -- of the variable, so we also return the unfolded version of the
1380 -- type, which is guaranteed to be syntactically free of the given
1381 -- type variable.  If the type is already syntactically free of the
1382 -- variable, then the same type is returned.
1383 --
1384 -- Precondition: the two types are not equal (looking though synonyms)
1385 canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
1386 canOccursCheck _gw tv xi = return (expandAway tv xi)
1387 \end{code}
1388
1389 @expandAway tv xi@ expands synonyms in xi just enough to get rid of
1390 occurrences of tv, if that is possible; otherwise, it returns Nothing.
1391 For example, suppose we have
1392   type F a b = [a]
1393 Then
1394   expandAway b (F Int b) = Just [Int]
1395 but
1396   expandAway a (F a Int) = Nothing
1397
1398 We don't promise to do the absolute minimum amount of expanding
1399 necessary, but we try not to do expansions we don't need to.  We
1400 prefer doing inner expansions first.  For example,
1401   type F a b = (a, Int, a, [a])
1402   type G b   = Char
1403 We have
1404   expandAway b (F (G b)) = F Char
1405 even though we could also expand F to get rid of b.
1406
1407 \begin{code}
1408 expandAway :: TcTyVar -> Xi -> Maybe Xi
1409 expandAway tv t@(TyVarTy tv')
1410   | tv == tv' = Nothing
1411   | otherwise = Just t
1412 expandAway tv xi
1413   | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
1414 expandAway tv (AppTy ty1 ty2) 
1415   = do { ty1' <- expandAway tv ty1
1416        ; ty2' <- expandAway tv ty2 
1417        ; return (mkAppTy ty1' ty2') }
1418 -- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
1419 expandAway tv (FunTy ty1 ty2)
1420   = do { ty1' <- expandAway tv ty1 
1421        ; ty2' <- expandAway tv ty2 
1422        ; return (mkFunTy ty1' ty2') } 
1423 -- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
1424 expandAway tv ty@(ForAllTy {}) 
1425   = let (tvs,rho) = splitForAllTys ty
1426         tvs_knds  = map tyVarKind tvs 
1427     in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
1428        -- Can't expand away the kinds unless we create 
1429        -- fresh variables which we don't want to do at this point.
1430            Nothing 
1431        else do { rho' <- expandAway tv rho
1432                ; return (mkForAllTys tvs rho') }
1433 -- For a type constructor application, first try expanding away the
1434 -- offending variable from the arguments.  If that doesn't work, next
1435 -- see if the type constructor is a type synonym, and if so, expand
1436 -- it and try again.
1437 expandAway tv ty@(TyConApp tc tys)
1438   = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
1439
1440 \end{code}
1441
1442 Note [Type synonyms and canonicalization]
1443 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1444
1445 We treat type synonym applications as xi types, that is, they do not
1446 count as type function applications.  However, we do need to be a bit
1447 careful with type synonyms: like type functions they may not be
1448 generative or injective.  However, unlike type functions, they are
1449 parametric, so there is no problem in expanding them whenever we see
1450 them, since we do not need to know anything about their arguments in
1451 order to expand them; this is what justifies not having to treat them
1452 as specially as type function applications.  The thing that causes
1453 some subtleties is that we prefer to leave type synonym applications
1454 *unexpanded* whenever possible, in order to generate better error
1455 messages.
1456
1457 If we encounter an equality constraint with type synonym applications
1458 on both sides, or a type synonym application on one side and some sort
1459 of type application on the other, we simply must expand out the type
1460 synonyms in order to continue decomposing the equality constraint into
1461 primitive equality constraints.  For example, suppose we have
1462
1463   type F a = [Int]
1464
1465 and we encounter the equality
1466
1467   F a ~ [b]
1468
1469 In order to continue we must expand F a into [Int], giving us the
1470 equality
1471
1472   [Int] ~ [b]
1473
1474 which we can then decompose into the more primitive equality
1475 constraint
1476
1477   Int ~ b.
1478
1479 However, if we encounter an equality constraint with a type synonym
1480 application on one side and a variable on the other side, we should
1481 NOT (necessarily) expand the type synonym, since for the purpose of
1482 good error messages we want to leave type synonyms unexpanded as much
1483 as possible.
1484
1485 However, there is a subtle point with type synonyms and the occurs
1486 check that takes place for equality constraints of the form tv ~ xi.
1487 As an example, suppose we have
1488
1489   type F a = Int
1490
1491 and we come across the equality constraint
1492
1493   a ~ F a
1494
1495 This should not actually fail the occurs check, since expanding out
1496 the type synonym results in the legitimate equality constraint a ~
1497 Int.  We must actually do this expansion, because unifying a with F a
1498 will lead the type checker into infinite loops later.  Put another
1499 way, canonical equality constraints should never *syntactically*
1500 contain the LHS variable in the RHS type.  However, we don't always
1501 need to expand type synonyms when doing an occurs check; for example,
1502 the constraint
1503
1504   a ~ F b
1505
1506 is obviously fine no matter what F expands to. And in this case we
1507 would rather unify a with F b (rather than F b's expansion) in order
1508 to get better error messages later.
1509
1510 So, when doing an occurs check with a type synonym application on the
1511 RHS, we use some heuristics to find an expansion of the RHS which does
1512 not contain the variable from the LHS.  In particular, given
1513
1514   a ~ F t1 ... tn
1515
1516 we first try expanding each of the ti to types which no longer contain
1517 a.  If this turns out to be impossible, we next try expanding F
1518 itself, and so on.
1519