TcCanonical.lhs 56 KB
Newer Older
1
\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
2
3
4
5
6
7
8
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

9
module TcCanonical(
10
    canonicalize, flatten, flattenMany, occurCheckExpand,
11
    FlattenMode (..),
12
    StopOrContinue (..)
13
14
15
16
17
18
 ) where

#include "HsVersions.h"

import TcRnTypes
import TcType
19
import Type
dreixel's avatar
dreixel committed
20
import Kind
21
import TcEvidence
22
23
24
25
import Class
import TyCon
import TypeRep
import Var
26
import VarEnv
27
import Outputable
28
import Control.Monad    ( when )
29
30
31
import MonadUtils
import Control.Applicative ( (<|>) )

32
import TrieMap
33
import VarSet
34
import TcSMonad
35
import FastString
36

37
import Util
38
39


dimitris's avatar
dimitris committed
40
41
42
43
import TysWiredIn ( eqTyCon )

import Data.Maybe ( isJust, fromMaybe )
-- import Data.List  ( zip4 )
44
\end{code}
45
46
47
48


%************************************************************************
%*                                                                      *
49
%*                      The Canonicaliser                               *
50
51
52
%*                                                                      *
%************************************************************************

53
54
Note [Canonicalization]
~~~~~~~~~~~~~~~~~~~~~~~
55

56
57
58
59
Canonicalization converts a flat constraint to a canonical form. It is
unary (i.e. treats individual constraints one at a time), does not do
any zonking, but lives in TcS monad because it needs to create fresh
variables (for flattening) and consult the inerts (for efficiency).
60

61
62
63
64
65
The execution plan for canonicalization is the following:
 
  1) Decomposition of equalities happens as necessary until we reach a 
     variable or type family in one side. There is no decomposition step
     for other forms of constraints. 
66

67
68
69
70
  2) If, when we decompose, we discover a variable on the head then we 
     look at inert_eqs from the current inert for a substitution for this 
     variable and contine decomposing. Hence we lazily apply the inert 
     substitution if it is needed. 
71

72
73
  3) If no more decomposition is possible, we deeply apply the substitution
     from the inert_eqs and continue with flattening.
74

75
76
77
78
79
  4) During flattening, we examine whether we have already flattened some 
     function application by looking at all the CTyFunEqs with the same 
     function in the inert set. The reason for deeply applying the inert 
     substitution at step (3) is to maximise our chances of matching an 
     already flattened family application in the inert. 
80

81
82
83
84
The net result is that a constraint coming out of the canonicalization 
phase cannot be rewritten any further from the inerts (but maybe /it/ can 
rewrite an inert or still interact with an inert in a further phase in the
simplifier.
dimitris's avatar
dimitris committed
85

86
\begin{code}
87

88
89
90
91
92
93
94
-- Informative results of canonicalization
data StopOrContinue 
  = ContinueWith Ct   -- Either no canonicalization happened, or if some did 
                      -- happen, it is still safe to just keep going with this 
                      -- work item. 
  | Stop              -- Some canonicalization happened, extra work is now in 
                      -- the TcS WorkList. 
95

96
97
98
instance Outputable StopOrContinue where
  ppr Stop             = ptext (sLit "Stop")
  ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
99
100


101
102
continueWith :: Ct -> TcS StopOrContinue
continueWith = return . ContinueWith
103

104
105
106
107
108
109
110
111
andWhenContinue :: TcS StopOrContinue 
                -> (Ct -> TcS StopOrContinue) 
                -> TcS StopOrContinue
andWhenContinue tcs1 tcs2
  = do { r <- tcs1
       ; case r of
           Stop            -> return Stop
           ContinueWith ct -> tcs2 ct }
112
113
114

\end{code}

115
116
Note [Caching for canonicals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
117
118
119
120
Our plan with pre-canonicalization is to be able to solve a constraint
really fast from existing bindings in TcEvBinds. So one may think that
the condition (isCNonCanonical) is not necessary.  However consider
the following setup:
121

122
123
InertSet = { [W] d1 : Num t } 
WorkList = { [W] d2 : Num t, [W] c : t ~ Int} 
124

Simon Peyton Jones's avatar
Simon Peyton Jones committed
125
126
127
128
129
Now, we prioritize equalities, but in our concrete example
(should_run/mc17.hs) the first (d2) constraint is dealt with first,
because (t ~ Int) is an equality that only later appears in the
worklist since it is pulled out from a nested implication
constraint. So, let's examine what happens:
130
131
132
133
134
135
136
137
 
   - We encounter work item (d2 : Num t)

   - Nothing is yet in EvBinds, so we reach the interaction with inerts 
     and set:
              d2 := d1 
    and we discard d2 from the worklist. The inert set remains unaffected.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
138
139
140
   - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
     (d1 : Num t) from the inerts.  Then that equation gets
     spontaneously solved, perhaps. We end up with:
141
142
143
        InertSet : { [G] c : t ~ Int }
        WorkList : { [W] d1 : Num t} 

Simon Peyton Jones's avatar
Simon Peyton Jones committed
144
145
   - Now we examine (d1), we observe that there is a binding for (Num
     t) in the evidence binds and we set:
146
147
148
             d1 := d2 
     and end up in a loop!

Simon Peyton Jones's avatar
Simon Peyton Jones committed
149
150
151
152
153
154
155
156
Now, the constraints that get kicked out from the inert set are always
Canonical, so by restricting the use of the pre-canonicalizer to
NonCanonical constraints we eliminate this danger. Moreover, for
canonical constraints we already have good caching mechanisms
(effectively the interaction solver) and we are interested in reducing
things like superclasses of the same non-canonical constraint being
generated hence I don't expect us to lose a lot by introducing the
(isCNonCanonical) restriction.
157

Simon Peyton Jones's avatar
Simon Peyton Jones committed
158
159
160
161
162
163
164
A similar situation can arise in TcSimplify, at the end of the
solve_wanteds function, where constraints from the inert set are
returned as new work -- our substCt ensures however that if they are
not rewritten by subst, they remain canonical and hence we will not
attempt to solve them from the EvBinds. If on the other hand they did
get rewritten and are now non-canonical they will still not match the
EvBinds, so we are again good.
165

166
167


168
\begin{code}
169

170
171
172
173
-- Top-level canonicalization
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

canonicalize :: Ct -> TcS StopOrContinue
174
canonicalize ct@(CNonCanonical { cc_ev = fl, cc_depth  = d })
175
  = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
176
       ; {-# SCC "canEvVar" #-}
dimitris's avatar
dimitris committed
177
         canEvVar d fl (classifyPredType (ctPred ct)) }
178

dimitris's avatar
dimitris committed
179
canonicalize (CDictCan { cc_depth  = d
180
                       , cc_ev = fl
181
182
                       , cc_class  = cls
                       , cc_tyargs = xis })
183
  = {-# SCC "canClass" #-}
dimitris's avatar
dimitris committed
184
185
    canClass d fl cls xis -- Do not add any superclasses
canonicalize (CTyEqCan { cc_depth  = d
186
                       , cc_ev = fl
187
188
                       , cc_tyvar  = tv
                       , cc_rhs    = xi })
189
  = {-# SCC "canEqLeafTyVarLeftRec" #-}
dimitris's avatar
dimitris committed
190
    canEqLeafTyVarLeftRec d fl tv xi
191

dimitris's avatar
dimitris committed
192
canonicalize (CFunEqCan { cc_depth = d
193
                        , cc_ev = fl
194
195
196
                        , cc_fun    = fn
                        , cc_tyargs = xis1
                        , cc_rhs    = xi2 })
197
  = {-# SCC "canEqLeafFunEqLeftRec" #-}
dimitris's avatar
dimitris committed
198
    canEqLeafFunEqLeftRec d fl (fn,xis1) xi2
199

200
canonicalize (CIrredEvCan { cc_ev = fl
201
202
                          , cc_depth = d
                          , cc_ty = xi })
dimitris's avatar
dimitris committed
203
  = canIrred d fl xi
204
205


dimitris's avatar
dimitris committed
206
canEvVar :: SubGoalDepth 
207
         -> CtEvidence 
dimitris's avatar
dimitris committed
208
209
         -> PredTree 
         -> TcS StopOrContinue
210
-- Called only for non-canonical EvVars 
dimitris's avatar
dimitris committed
211
canEvVar d fl pred_classifier 
212
  = case pred_classifier of
dimitris's avatar
dimitris committed
213
214
215
216
      ClassPred cls tys -> canClassNC d fl cls tys 
      EqPred ty1 ty2    -> canEqNC    d fl ty1 ty2 
      IrredPred ev_ty   -> canIrred   d fl ev_ty
      TuplePred tys     -> canTuple   d fl tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
217
218
219
220
221
222
223
224
225
226
\end{code}


%************************************************************************
%*                                                                      *
%*                      Tuple Canonicalization
%*                                                                      *
%************************************************************************

\begin{code}
227
canTuple :: SubGoalDepth -- Depth 
228
         -> CtEvidence -> [PredType] -> TcS StopOrContinue
dimitris's avatar
dimitris committed
229
230
231
232
canTuple d fl tys
  = do { traceTcS "can_pred" (text "TuplePred!")
       ; let xcomp = EvTupleMk
             xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]             
233
234
235
236
237
       ; ctevs <- xCtFlavor fl tys (XEvTerm xcomp xdecomp)
       ; mapM_ add_to_work ctevs
       ; return Stop }
  where
    add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctEvPred fl))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
238
239
240
241
242
243
244
245
\end{code}


%************************************************************************
%*                                                                      *
%*                      Class Canonicalization
%*                                                                      *
%************************************************************************
246

Simon Peyton Jones's avatar
Simon Peyton Jones committed
247
248
249
\begin{code}
canClass, canClassNC 
   :: SubGoalDepth -- Depth
250
   -> CtEvidence  
Simon Peyton Jones's avatar
Simon Peyton Jones committed
251
   -> Class -> [Type] -> TcS StopOrContinue
252
-- Precondition: EvVar is class evidence 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
253
254
255
256
257
258

-- The canClassNC version is used on non-canonical constraints
-- and adds superclasses.  The plain canClass version is used
-- for already-canonical class constraints (but which might have
-- been subsituted or somthing), and hence do not need superclasses

dimitris's avatar
dimitris committed
259
260
canClassNC d fl cls tys 
  = canClass d fl cls tys 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
261
262
    `andWhenContinue` emitSuperclasses

dimitris's avatar
dimitris committed
263
canClass d fl cls tys
264
  = do { -- sctx <- getTcSContext
265
       ; (xis, cos) <- flattenMany d FMFullFlatten fl tys
266
       ; let co = mkTcTyConAppCo (classTyCon cls) cos 
267
             xi = mkClassPred cls xis
dimitris's avatar
dimitris committed
268
269
             
       ; mb <- rewriteCtFlavor fl xi co
270

dimitris's avatar
dimitris committed
271
       ; case mb of
272
           Just new_fl -> 
273
             let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_fl)
274
             in continueWith $ 
275
                CDictCan { cc_ev = new_fl
276
                         , cc_tyargs = xis_for_dict, cc_class = cls, cc_depth = d }
dimitris's avatar
dimitris committed
277
278
           Nothing -> return Stop }

Simon Peyton Jones's avatar
Simon Peyton Jones committed
279
emitSuperclasses :: Ct -> TcS StopOrContinue
280
emitSuperclasses ct@(CDictCan { cc_depth = d, cc_ev = fl
Simon Peyton Jones's avatar
Simon Peyton Jones committed
281
282
283
                              , cc_tyargs = xis_new, cc_class = cls })
            -- Add superclasses of this one here, See Note [Adding superclasses]. 
            -- But only if we are not simplifying the LHS of a rule. 
284
 = do { newSCWorkFromFlavored d fl cls xis_new
Simon Peyton Jones's avatar
Simon Peyton Jones committed
285
286
287
288
289
      -- Arguably we should "seq" the coercions if they are derived, 
      -- as we do below for emit_kind_constraint, to allow errors in
      -- superclasses to be executed if deferred to runtime! 
      ; continueWith ct }
emitSuperclasses _ = panic "emit_superclasses of non-class!"
290
291
292
293
294
295
296
297
298
299
300
301
302
303
\end{code}

Note [Adding superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~ 
Since dictionaries are canonicalized only once in their lifetime, the
place to add their superclasses is canonicalisation (The alternative
would be to do it during constraint solving, but we'd have to be
extremely careful to not repeatedly introduced the same superclass in
our worklist). Here is what we do:

For Givens: 
       We add all their superclasses as Givens. 

For Wanteds: 
304
305
       Generally speaking we want to be able to add superclasses of 
       wanteds for two reasons:
306

307
308
309
310
311
312
313
314
315
       (1) Oportunities for improvement. Example: 
                  class (a ~ b) => C a b 
           Wanted constraint is: C alpha beta 
           We'd like to simply have C alpha alpha. Similar 
           situations arise in relation to functional dependencies. 
           
       (2) To have minimal constraints to quantify over: 
           For instance, if our wanted constraint is (Eq a, Ord a) 
           we'd only like to quantify over Ord a. 
316

317
318
319
320
321
322
323
324
325
326
327
328
       To deal with (1) above we only add the superclasses of wanteds
       which may lead to improvement, that is: equality superclasses or 
       superclasses with functional dependencies. 

       We deal with (2) completely independently in TcSimplify. See 
       Note [Minimize by SuperClasses] in TcSimplify. 


       Moreover, in all cases the extra improvement constraints are 
       Derived. Derived constraints have an identity (for now), but 
       we don't do anything with their evidence. For instance they 
       are never used to rewrite other constraints. 
329

330
       See also [New Wanted Superclass Work] in TcInteract. 
331

332
333
334

For Deriveds: 
       We do nothing.
335
336
337

Here's an example that demonstrates why we chose to NOT add
superclasses during simplification: [Comes from ticket #4497]
dimitris's avatar
dimitris committed
338
 
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
   class Num (RealOf t) => Normed t
   type family RealOf x

Assume the generated wanted constraint is: 
   RealOf e ~ e, Normed e 
If we were to be adding the superclasses during simplification we'd get: 
   Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf 
==> 
   e ~ uf, Num uf, Normed e, RealOf e ~ e 
==> [Spontaneous solve] 
   Num uf, Normed uf, RealOf uf ~ uf 

While looks exactly like our original constraint. If we add the superclass again we'd loop. 
By adding superclasses definitely only once, during canonicalisation, this situation can't 
happen.

\begin{code}
356

357
newSCWorkFromFlavored :: SubGoalDepth -- Depth
358
                      -> CtEvidence -> Class -> [Xi] -> TcS ()
359
-- Returns superclasses, see Note [Adding superclasses]
dimitris's avatar
dimitris committed
360
newSCWorkFromFlavored d flavor cls xis 
batterseapower's avatar
batterseapower committed
361
  | isDerived flavor 
362
363
  = return ()  -- Deriveds don't yield more superclasses because we will
               -- add them transitively in the case of wanteds. 
dimitris's avatar
dimitris committed
364
365
366
    
  | isGiven flavor 
  = do { let sc_theta = immSuperClasses cls xis 
367
368
369
             xev_decomp x = zipWith (\_ i -> EvSuperClass x i) sc_theta [0..] 
             xev = XEvTerm { ev_comp   = panic "Can't compose for given!" 
                           , ev_decomp = xev_decomp }
370
       ; ctevs <- xCtFlavor flavor sc_theta xev
371
372
373

       ; traceTcS "newSCWork/Given" $ ppr "ctevs =" <+> ppr ctevs 
       ; mapM_ emit_non_can ctevs }
dimitris's avatar
dimitris committed
374
375

  | isEmptyVarSet (tyVarsOfTypes xis)
376
  = return () -- Wanteds with no variables yield no deriveds.
377
              -- See Note [Improvement from Ground Wanteds]
378

379
  | otherwise -- Wanted case, just add those SC that can lead to improvement. 
380
  = do { let sc_rec_theta = transSuperClasses cls xis 
381
382
383
384
385
386
387
388
389
             impr_theta   = filter is_improvement_pty sc_rec_theta
       ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
       ; mapM_ emit_der impr_theta }

  where emit_der pty = newDerived (ctev_wloc flavor) pty >>= mb_emit
        mb_emit Nothing     = return ()
        mb_emit (Just ctev) = emit_non_can ctev 
        emit_non_can ctev   = updWorkListTcS $ 
                              extendWorkListCt (CNonCanonical ctev d)
390
391
392

is_improvement_pty :: PredType -> Bool 
-- Either it's an equality, or has some functional dependency
393
is_improvement_pty ty = go (classifyPredType ty)
batterseapower's avatar
batterseapower committed
394
395
  where
    go (EqPred {})         = True 
396
397
398
    go (ClassPred cls _tys) = not $ null fundeps
      where (_,fundeps) = classTvsFds cls
    go (TuplePred ts)      = any is_improvement_pty ts
batterseapower's avatar
batterseapower committed
399
    go (IrredPred {})      = True -- Might have equalities after reduction?
400
\end{code}
401
402


Simon Peyton Jones's avatar
Simon Peyton Jones committed
403
404
405
406
407
408
%************************************************************************
%*                                                                      *
%*                      Irreducibles canonicalization
%*                                                                      *
%************************************************************************

409

410
411
\begin{code}
canIrred :: SubGoalDepth -- Depth
412
         -> CtEvidence -> TcType -> TcS StopOrContinue
413
-- Precondition: ty not a tuple and no other evidence form
dimitris's avatar
dimitris committed
414
canIrred d fl ty 
415
  = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty) 
416
       ; (xi,co) <- flatten d FMFullFlatten fl ty -- co :: xi ~ ty
417
418
       ; let no_flattening = xi `eqType` ty 
                             -- In this particular case it is not safe to 
419
                             -- say 'isTcReflCo' because the new constraint may
420
                             -- be reducible!
dimitris's avatar
dimitris committed
421
422
423
424
425
       ; mb <- rewriteCtFlavor fl xi co 
       ; case mb of
             Just new_fl 
               | no_flattening
                 -> continueWith $
426
                    CIrredEvCan { cc_ev = new_fl, cc_ty = xi, cc_depth = d }
dimitris's avatar
dimitris committed
427
               | otherwise
428
                 -> canEvVar d new_fl (classifyPredType (ctEvPred new_fl))
dimitris's avatar
dimitris committed
429
430
             Nothing -> return Stop }

431
\end{code}
432

433
434
435
436
437
438
439
440
441
442
%************************************************************************
%*                                                                      *
%*        Flattening (eliminating all function symbols)                 *
%*                                                                      *
%************************************************************************

Note [Flattening]
~~~~~~~~~~~~~~~~~~~~
  flatten ty  ==>   (xi, cc)
    where
443
444
      xi has no type functions, unless they appear under ForAlls

445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
      cc = Auxiliary given (equality) constraints constraining
           the fresh type variables in xi.  Evidence for these 
           is always the identity coercion, because internally the
           fresh flattening skolem variables are actually identified
           with the types they have been generated to stand in for.

Note that it is flatten's job to flatten *every type function it sees*.
flatten is only called on *arguments* to type functions, by canEqGiven.

Recall that in comments we use alpha[flat = ty] to represent a
flattening skolem variable alpha which has been generated to stand in
for ty.

----- Example of flattening a constraint: ------
  flatten (List (F (G Int)))  ==>  (xi, cc)
    where
      xi  = List alpha
      cc  = { G Int ~ beta[flat = G Int],
              F beta ~ alpha[flat = F beta] }
Here
  * alpha and beta are 'flattening skolem variables'.
  * All the constraints in cc are 'given', and all their coercion terms 
    are the identity.

NB: Flattening Skolems only occur in canonical constraints, which
are never zonked, so we don't need to worry about zonking doing
accidental unflattening.

Note that we prefer to leave type synonyms unexpanded when possible,
so when the flattener encounters one, it first asks whether its
transitive expansion contains any type function applications.  If so,
it expands the synonym and proceeds; if not, it simply returns the
unexpanded synonym.

\begin{code}

481
482
483
data FlattenMode = FMSubstOnly 
                 | FMFullFlatten

484
485
-- Flatten a bunch of types all at once.
flattenMany :: SubGoalDepth -- Depth
486
            -> FlattenMode
487
            -> CtEvidence -> [Type] -> TcS ([Xi], [TcCoercion])
488
-- Coercions :: Xi ~ Type 
489
-- Returns True iff (no flattening happened)
dimitris's avatar
dimitris committed
490
-- NB: The EvVar inside the flavor is unused, we merely want Given/Solved/Derived/Wanted info
491
flattenMany d f ctxt tys 
492
493
  = -- pprTrace "flattenMany" empty $
    go tys 
494
  where go []       = return ([],[])
495
        go (ty:tys) = do { (xi,co)    <- flatten d f ctxt ty
496
497
                         ; (xis,cos)  <- go tys
                         ; return (xi:xis,co:cos) }
498
499
500
501
502

-- Flatten a type to get rid of type function applications, returning
-- the new type-function-free type, and a collection of new equality
-- constraints.  See Note [Flattening] for more detail.
flatten :: SubGoalDepth -- Depth
503
        -> FlattenMode 
504
        -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
505
-- Postcondition: Coercion :: Xi ~ TcType
506
flatten d f ctxt ty 
507
  | Just ty' <- tcView ty
508
  = do { (xi, co) <- flatten d f ctxt ty'
509
510
       ; if eqType xi ty then return (ty,co) else return (xi,co) } 
       -- Small tweak for better error messages 
511

512
flatten _ _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
513

514
515
flatten d f ctxt (TyVarTy tv)
  = flattenTyVar d f ctxt tv
516

517
518
519
flatten d f ctxt (AppTy ty1 ty2)
  = do { (xi1,co1) <- flatten d f ctxt ty1
       ; (xi2,co2) <- flatten d f ctxt ty2
520
       ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
521

522
523
524
flatten d f ctxt (FunTy ty1 ty2)
  = do { (xi1,co1) <- flatten d f ctxt ty1
       ; (xi2,co2) <- flatten d f ctxt ty2
525
       ; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
526

527
flatten d f fl (TyConApp tc tys)
528
529
530
  -- For a normal type constructor or data family application, we just
  -- recursively flatten the arguments.
  | not (isSynFamilyTyCon tc)
531
    = do { (xis,cos) <- flattenMany d f fl tys
532
         ; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
533
534
535
536
537
538

  -- Otherwise, it's a type function application, and we have to
  -- flatten it away as well, and generate a new given equality constraint
  -- between the application and a newly generated flattening skolem variable.
  | otherwise
  = ASSERT( tyConArity tc <= length tys )	-- Type functions are saturated
539
      do { (xis, cos) <- flattenMany d f fl tys
540
541
542
543
544
         ; let (xi_args, xi_rest)  = splitAt (tyConArity tc) xis
	       	 -- The type function might be *over* saturated
		 -- in which case the remaining arguments should
		 -- be dealt with by AppTys
               fam_ty = mkTyConApp tc xi_args
dimitris's avatar
dimitris committed
545
               
546
         ; (ret_co, rhs_xi, ct) <-
547
548
549
550
551
552
553
             case f of 
               FMSubstOnly -> 
                 return (mkTcReflCo fam_ty, fam_ty, [])
               FMFullFlatten -> 
                 do { flat_cache <- getFlatCache
                    ; case lookupTM fam_ty flat_cache of
                        Just ct 
554
555
                          | let ctev = cc_ev ct
                          , ctev `canRewrite` fl 
556
557
558
559
560
561
562
563
564
565
                          -> -- You may think that we can just return (cc_rhs ct) but not so. 
                             --            return (mkTcCoVarCo (ctId ct), cc_rhs ct, []) 
                             -- The cached constraint resides in the cache so we have to flatten 
                             -- the rhs to make sure we have applied any inert substitution to it.
                             -- Alternatively we could be applying the inert substitution to the 
                             -- cache as well when we interact an equality with the inert. 
                             -- The design choice is: do we keep the flat cache rewritten or not?
                             -- For now I say we don't keep it fully rewritten.
                            do { traceTcS "flatten/flat-cache hit" $ ppr ct
                               ; let rhs_xi = cc_rhs ct
566
567
568
                               ; (flat_rhs_xi,co) <- flatten (cc_depth ct) f ctev rhs_xi
                               ; let final_co = evTermCoercion (ctEvTerm ctev)
                                                `mkTcTransCo` mkTcSymCo co
569
                               ; return (final_co, flat_rhs_xi,[]) }
dimitris's avatar
dimitris committed
570
                          
571
                        _ | isGiven fl -- Given: make new flatten skolem
572
573
                          -> do { traceTcS "flatten/flat-cache miss" $ empty 
                                ; rhs_xi_var <- newFlattenSkolemTy fam_ty
574
575
576
577
578
579
580
581
582
583
584
585
                                ; let co = mkTcReflCo fam_ty
                                      new_fl = Given { ctev_gloc = ctev_gloc fl
                                                     , ctev_pred = mkTcEqPred fam_ty rhs_xi_var
                                                     , ctev_evtm = EvCoercion co }
                                      ct = CFunEqCan { cc_ev = new_fl
                                                     , cc_fun    = tc 
                                                     , cc_tyargs = xi_args 
                                                     , cc_rhs    = rhs_xi_var 
                                                     , cc_depth  = d }
                                      -- Update the flat cache
                                ; updFlatCache ct
                                ; return (co, rhs_xi_var, [ct]) }
586
587
588
                         | otherwise -- Wanted or Derived: make new unification variable
                         -> do { traceTcS "flatten/flat-cache miss" $ empty 
                               ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
589
590
591
                               ; let pred = mkTcEqPred fam_ty rhs_xi_var
                                     wloc = ctev_wloc fl
                               ; mw <- newWantedEvVar wloc pred
592
                               ; case mw of
593
594
                                   Fresh ctev -> 
                                     do { let ct = CFunEqCan { cc_ev = ctev
dimitris's avatar
dimitris committed
595
596
597
598
                                                             , cc_fun = tc
                                                             , cc_tyargs = xi_args
                                                             , cc_rhs    = rhs_xi_var 
                                                             , cc_depth  = d }
599
                                          -- Update the flat cache: just an optimisation!
dimitris's avatar
dimitris committed
600
                                        ; updFlatCache ct
601
                                        ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var, [ct]) }
dimitris's avatar
dimitris committed
602
                                   Cached {} -> panic "flatten TyConApp, var must be fresh!" } 
603
                    }
dimitris's avatar
dimitris committed
604
                  -- Emit the flat constraints
605
606
         ; updWorkListTcS $ appendWorkListEqs ct
         ; let (cos_args, cos_rest) = splitAt (tyConArity tc) cos
dimitris's avatar
dimitris committed
607
608
609
610
611
612
         ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
                                            --    cf Trac #5655
                  , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args) $
                    cos_rest
                  ) 
         }
613

614
flatten d _f ctxt ty@(ForAllTy {})
615
616
617
-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
  = do { let (tvs, rho) = splitForAllTys ty
618
619
620
       ; (rho', co) <- flatten d FMSubstOnly ctxt rho
       ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }

Simon Peyton Jones's avatar
Simon Peyton Jones committed
621
622
623
\end{code}

\begin{code}
624
625
flattenTyVar :: SubGoalDepth 
             -> FlattenMode 
626
             -> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
627
-- "Flattening" a type variable means to apply the substitution to it
628
flattenTyVar d f ctxt tv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
629
630
631
632
633
  = do { ieqs <- getInertEqs
       ; let mco = tv_eq_subst (fst ieqs) tv  -- co : v ~ ty
       ; case mco of -- Done, but make sure the kind is zonked
           Nothing -> 
               do { let knd = tyVarKind tv
634
                  ; (new_knd,_kind_co) <- flatten d f ctxt knd
Simon Peyton Jones's avatar
Simon Peyton Jones committed
635
636
637
                  ; let ty = mkTyVarTy (setVarType tv new_knd)
                  ; return (ty, mkTcReflCo ty) }
           -- NB recursive call. 
638
639
640
           -- Why? Because inert subst. non-idempotent, Note [Detailed InertCans Invariants]
           -- In fact, because of flavors, it couldn't possibly be idempotent,
           -- this is explained in Note [Non-idempotent inert substitution]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
641
           Just (co,ty) -> 
642
               do { (ty_final,co') <- flatten d f ctxt ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
643
                  ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } }  
644
645
646
647
648
649
650
651
652
  where 
    tv_eq_subst subst tv
       | Just ct <- lookupVarEnv subst tv
       , let ctev = cc_ev ct
       , ctev `canRewrite` ctxt
       = Just (evTermCoercion (ctEvTerm ctev), cc_rhs ct)
              -- NB: even if ct is Derived we are not going to 
              -- touch the actual coercion so we are fine. 
       | otherwise = Nothing
Simon Peyton Jones's avatar
Simon Peyton Jones committed
653
654
655
656
657
658
659
660
661
\end{code}

Note [Non-idempotent inert substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The inert substitution is not idempotent in the broad sense. It is only idempotent in 
that it cannot rewrite the RHS of other inert equalities any further. An example of such 
an inert substitution is:

dimitris's avatar
dimitris committed
662
 [G] g1 : ta8 ~ ta4
Simon Peyton Jones's avatar
Simon Peyton Jones committed
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
 [W] g2 : ta4 ~ a5Fj

Observe that the wanted cannot rewrite the solved goal, despite the fact that ta4 appears on
an RHS of an equality. Now, imagine a constraint:

 [W] g3: ta8 ~ Int 

coming in. If we simply apply once the inert substitution we will get: 

 [W] g3_1: ta4 ~ Int 

and because potentially ta4 is untouchable we will try to insert g3_1 in the inert set, 
getting a panic since the inert only allows ONE equation per LHS type variable (as it 
should).

For this reason, when we reach to flatten a type variable, we flatten it recursively, 
so that we can make sure that the inert substitution /is/ fully applied.
680

dimitris's avatar
dimitris committed
681
Insufficient (non-recursive) rewriting was the reason for #5668.
682

Simon Peyton Jones's avatar
Simon Peyton Jones committed
683
\begin{code}
dimitris's avatar
dimitris committed
684

685
686
687
688
689
690
-----------------
addToWork :: TcS StopOrContinue -> TcS ()
addToWork tcs_action = tcs_action >>= stop_or_emit
  where stop_or_emit Stop              = return ()
        stop_or_emit (ContinueWith ct) = updWorkListTcS $ 
                                         extendWorkListCt ct
Simon Peyton Jones's avatar
Simon Peyton Jones committed
691
\end{code}
692

Simon Peyton Jones's avatar
Simon Peyton Jones committed
693
694
695
696
697
698
699
700

%************************************************************************
%*                                                                      *
%*        Equalities
%*                                                                      *
%************************************************************************

\begin{code}
dimitris's avatar
dimitris committed
701
canEqEvVarsCreated :: SubGoalDepth
702
                   -> [CtEvidence] -> TcS StopOrContinue
dimitris's avatar
dimitris committed
703
704
705
706
707
canEqEvVarsCreated _d [] = return Stop
canEqEvVarsCreated d (quad:quads) 
  = mapM_ (addToWork . do_quad) quads >> do_quad quad
           -- Add all but one to the work list
           -- and return the first (if any) for futher processing
708
  where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctEvPred fl
dimitris's avatar
dimitris committed
709
710
711
712
                     in canEqNC d fl ty1 ty2
          -- Note the "NC": these are fresh equalities so we must be
          -- careful to add their kind constraints

Simon Peyton Jones's avatar
Simon Peyton Jones committed
713
714
715
-------------------------
canEqNC, canEq 
  :: SubGoalDepth 
716
  -> CtEvidence 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
717
718
  -> Type -> Type -> TcS StopOrContinue

dimitris's avatar
dimitris committed
719
720
canEqNC d fl ty1 ty2
  = canEq d fl ty1 ty2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
721
722
    `andWhenContinue` emitKindConstraint

dimitris's avatar
dimitris committed
723
canEq _d fl ty1 ty2
724
  | eqType ty1 ty2	-- Dealing with equality here avoids
725
    	     	 	-- later spurious occurs checks for a~a
dimitris's avatar
dimitris committed
726
  = if isWanted fl then
727
      setEvBind (ctev_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
dimitris's avatar
dimitris committed
728
729
    else
      return Stop
730

731
-- If one side is a variable, orient and flatten,
732
-- WITHOUT expanding type synonyms, so that we tend to 
733
-- substitute a ~ Age rather than a ~ Int when @type Age = Int@
dimitris's avatar
dimitris committed
734
735
736
737
canEq d fl ty1@(TyVarTy {}) ty2 
  = canEqLeaf d fl ty1 ty2
canEq d fl ty1 ty2@(TyVarTy {})
  = canEqLeaf d fl ty1 ty2
738

739
-- See Note [Naked given applications]
dimitris's avatar
dimitris committed
740
741
742
canEq d fl ty1 ty2
  | Just ty1' <- tcView ty1 = canEq d fl ty1' ty2
  | Just ty2' <- tcView ty2 = canEq d fl ty1  ty2'
743

dimitris's avatar
dimitris committed
744
canEq d fl ty1@(TyConApp fn tys) ty2
745
  | isSynFamilyTyCon fn, length tys == tyConArity fn
dimitris's avatar
dimitris committed
746
747
  = canEqLeaf d fl ty1 ty2
canEq d fl ty1 ty2@(TyConApp fn tys)
748
  | isSynFamilyTyCon fn, length tys == tyConArity fn
dimitris's avatar
dimitris committed
749
  = canEqLeaf d fl ty1 ty2
750

dimitris's avatar
dimitris committed
751
canEq d fl ty1 ty2
752
753
754
  | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
  , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
  , isDecomposableTyCon tc1 && isDecomposableTyCon tc2
755
  = -- Generate equalities for each of the corresponding arguments
756
757
    if (tc1 /= tc2 || length tys1 /= length tys2)
    -- Fail straight away for better error messages
dimitris's avatar
dimitris committed
758
759
    then canEqFailure d fl
    else
760
761
762
763
764
    do { let xcomp xs  = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
             xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
             xev = XEvTerm xcomp xdecomp
       ; ctevs <- xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev
       ; canEqEvVarsCreated d ctevs }
765
766
767

-- See Note [Equality between type applications]
--     Note [Care with type applications] in TcUnify
dimitris's avatar
dimitris committed
768
canEq d fl ty1 ty2    -- e.g.  F a b ~ Maybe c
769
770
                          -- where F has arity 1
  | Just (s1,t1) <- tcSplitAppTy_maybe ty1
771
  , Just (s2,t2) <- tcSplitAppTy_maybe ty2
dimitris's avatar
dimitris committed
772
  = canEqAppTy d fl s1 t1 s2 t2
773

dimitris's avatar
dimitris committed
774
canEq d fl s1@(ForAllTy {}) s2@(ForAllTy {})
775
 | tcIsForAllTy s1, tcIsForAllTy s2
776
 , Wanted { ctev_wloc = loc, ctev_evar = orig_ev } <- fl 
777
778
779
780
781
782
783
784
 = do { let (tvs1,body1) = tcSplitForAllTys s1
            (tvs2,body2) = tcSplitForAllTys s2
      ; if not (equalLength tvs1 tvs2) then 
          canEqFailure d fl
        else
          do { traceTcS "Creating implication for polytype equality" $ ppr fl
             ; deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2) 
             ; return Stop } }
785
 | otherwise
786
787
 = do { traceTcS "Ommitting decomposition of given polytype equality" $ 
        pprEq s1 s2
788
      ; return Stop }
dimitris's avatar
dimitris committed
789
canEq d fl _ _  = canEqFailure d fl
790

Simon Peyton Jones's avatar
Simon Peyton Jones committed
791
------------------------
792
793
-- Type application
canEqAppTy :: SubGoalDepth 
794
           -> CtEvidence 
dimitris's avatar
dimitris committed
795
           -> Type -> Type -> Type -> Type
796
           -> TcS StopOrContinue
dimitris's avatar
dimitris committed
797
canEqAppTy d fl s1 t1 s2 t2
798
  = ASSERT( not (isKind t1) && not (isKind t2) )
799
    if isGiven fl then 
800
        do { traceTcS "canEq (app case)" $
801
                text "Ommitting decomposition of given equality between: " 
802
                    <+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2)
803
804
805
                   -- We cannot decompose given applications
                   -- because we no longer have 'left' and 'right'
           ; return Stop }
dimitris's avatar
dimitris committed
806
    else 
807
808
809
810
811
812
813
814
    do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
             xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
             xev = XEvTerm { ev_comp = xevcomp
                           , ev_decomp = error "canEqAppTy: can't happen" }
       ; ctevs <- xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev 
       ; canEqEvVarsCreated d ctevs }

canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
dimitris's avatar
dimitris committed
815
816
canEqFailure d fl = emitFrozenError fl d >> return Stop

Simon Peyton Jones's avatar
Simon Peyton Jones committed
817
818
819
820
------------------------
emitKindConstraint :: Ct -> TcS StopOrContinue
emitKindConstraint ct
  = case ct of 
dimitris's avatar
dimitris committed
821
      CTyEqCan { cc_depth = d
822
               , cc_ev = fl, cc_tyvar = tv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
823
               , cc_rhs = ty }
dimitris's avatar
dimitris committed
824
          -> emit_kind_constraint d fl (mkTyVarTy tv) ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
825

dimitris's avatar
dimitris committed
826
      CFunEqCan { cc_depth = d
827
                , cc_ev = fl
Simon Peyton Jones's avatar
Simon Peyton Jones committed
828
829
                , cc_fun = fn, cc_tyargs = xis1
                , cc_rhs = xi2 }
dimitris's avatar
dimitris committed
830
          -> emit_kind_constraint d fl (mkTyConApp fn xis1) xi2
831

dimitris's avatar
dimitris committed
832
      _   -> continueWith ct
Simon Peyton Jones's avatar
Simon Peyton Jones committed
833
  where
dimitris's avatar
dimitris committed
834
    emit_kind_constraint d fl ty1 ty2 
835
836
837
       | compatKind k1 k2    -- True when ty1,ty2 are themselves kinds,
       = continueWith ct     -- because then k1, k2 are BOX
       
Simon Peyton Jones's avatar
Simon Peyton Jones committed
838
       | otherwise
839
       = ASSERT( isKind k1 && isKind k2 )
dimitris's avatar
dimitris committed
840
         do { kev <- 
841
                 do { mw <- newWantedEvVar kind_co_wloc (mkEqPred k1 k2) 
dimitris's avatar
dimitris committed
842
                    ; case mw of
843
844
845
846
847
                         Cached ev_tm -> return ev_tm
                         Fresh ctev   -> do { addToWork (canEq d ctev k1 k2) 
                                            ; return (ctEvTerm ctev) } }

            ; let xcomp [x] = mkEvKindCast x (evTermCoercion kev)
dimitris's avatar
dimitris committed
848
                  xcomp _   = panic "emit_kind_constraint:can't happen"
849
                  xdecomp x = [mkEvKindCast x (evTermCoercion kev)]
dimitris's avatar
dimitris committed
850
                  xev = XEvTerm xcomp xdecomp
851
852

            ; ctevs <- xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev 
853
854
855
856
857
858
                     -- Important: Do not cache original as Solved since we are supposed to 
                     -- solve /exactly/ the same constraint later! Example:
                     -- (alpha :: kappa0) 
                     -- (T :: *)
                     -- Equality is: (alpha ~ T), so we will emitConstraint (kappa0 ~ *) but
                     -- we don't want to say that (alpha ~ T) is now Solved!
dimitris's avatar
dimitris committed
859

860
861
862
863
864
            ; case ctevs of
                []         -> return Stop
                [new_ctev] -> continueWith (ct { cc_ev = new_ctev }) 
                _          -> panic "emitKindConstraint" }
       where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
865
866
867
         k1 = typeKind ty1
         k2 = typeKind ty2
         ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2
868

Simon Peyton Jones's avatar
Simon Peyton Jones committed
869
870
         -- Always create a Wanted kind equality even if 
         -- you are decomposing a given constraint.
dimitris's avatar
dimitris committed
871
         -- NB: DV finds this reasonable for now. Maybe we have to revisit.
872
873
874
875
876
877
         kind_co_wloc = pushErrCtxtSameOrigin ctxt wanted_loc
         wanted_loc = case fl of
                         Wanted  { ctev_wloc = wloc } -> wloc
                         Derived { ctev_wloc = wloc } -> wloc
                         Given { ctev_gloc = gloc }   -> setCtLocOrigin gloc orig
         orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
878
879
\end{code}

880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
Note [Combining insoluble constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As this point we have an insoluble constraint, like Int~Bool.

 * If it is Wanted, delete it from the cache, so that subsequent
   Int~Bool constraints give rise to separate error messages

 * But if it is Derived, DO NOT delete from cache.  A class constraint
   may get kicked out of the inert set, and then have its functional
   dependency Derived constraints generated a second time. In that
   case we don't want to get two (or more) error messages by
   generating two (or more) insoluble fundep constraints from the same
   class constraint.
   

895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
Note [Naked given applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider: 
   data A a 
   type T a = A a 
and the given equality:  
   [G] A a ~ T Int 
We will reach the case canEq where we do a tcSplitAppTy_maybe, but if
we dont have the guards (Nothing <- tcView ty1) (Nothing <- tcView
ty2) then the given equation is going to fall through and get
completely forgotten!

What we want instead is this clause to apply only when there is no
immediate top-level synonym; if there is one it will be later on
unfolded by the later stages of canEq.

Test-case is in typecheck/should_compile/GivenTypeSynonym.hs


914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
Note [Equality between type applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we see an equality of the form s1 t1 ~ s2 t2 we can always split
it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
functions (type functions use the TyConApp constructor, which never
shows up as the LHS of an AppTy).  Other than type functions, types
in Haskell are always 

  (1) generative: a b ~ c d implies a ~ c, since different type
      constructors always generate distinct types

  (2) injective: a b ~ a d implies b ~ d; we never generate the
      same type from different type arguments.


Note [Canonical ordering for equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Implemented as (<+=) below:

  - Type function applications always come before anything else.  
  - Variables always come before non-variables (other than type
      function applications).

Note that we don't need to unfold type synonyms on the RHS to check
the ordering; that is, in the rules above it's OK to consider only
whether something is *syntactically* a type function application or
not.  To illustrate why this is OK, suppose we have an equality of the
form 'tv ~ S a b c', where S is a type synonym which expands to a
top-level application of the type function F, something like

  type S a b c = F d e

Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
expansion contains type function applications the flattener will do
the expansion and then generate a skolem variable for the type
function application, so we end up with something like this:

  tv ~ x
  F d e ~ x

where x is the skolem variable.  This is one extra equation than
absolutely necessary (we could have gotten away with just 'F d e ~ tv'
if we had noticed that S expanded to a top-level type function
application and flipped it around in the first place) but this way
keeps the code simpler.

Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
ordering of tv ~ tv constraints.  There are several reasons why we
might:

  (1) In order to be able to extract a substitution that doesn't
      mention untouchable variables after we are done solving, we might
      prefer to put touchable variables on the left. However, in and
      of itself this isn't necessary; we can always re-orient equality
      constraints at the end if necessary when extracting a substitution.

  (2) To ensure termination we might think it necessary to put
      variables in lexicographic order. However, this isn't actually 
      necessary as outlined below.

While building up an inert set of canonical constraints, we maintain
the invariant that the equality constraints in the inert set form an
acyclic rewrite system when viewed as L-R rewrite rules.  Moreover,
the given constraints form an idempotent substitution (i.e. none of
the variables on the LHS occur in any of the RHS's, and type functions
never show up in the RHS at all), the wanted constraints also form an
idempotent substitution, and finally the LHS of a given constraint
never shows up on the RHS of a wanted constraint.  There may, however,
be a wanted LHS that shows up in a given RHS, since we do not rewrite
given constraints with wanted constraints.

Suppose we have an inert constraint set


  tg_1 ~ xig_1         -- givens
  tg_2 ~ xig_2
  ...
  tw_1 ~ xiw_1         -- wanteds
  tw_2 ~ xiw_2
  ...

where each t_i can be either a type variable or a type function
application. Now suppose we take a new canonical equality constraint,
t' ~ xi' (note among other things this means t' does not occur in xi')
and try to react it with the existing inert set.  We show by induction
on the number of t_i which occur in t' ~ xi' that this process will
terminate.

There are several ways t' ~ xi' could react with an existing constraint:

TODO: finish this proof.  The below was for the case where the entire
inert set is an idempotent subustitution...

(b) We could have t' = t_j for some j.  Then we obtain the new
    equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j.  We
    now canonicalize the new equality, which may involve decomposing it
    into several canonical equalities, and recurse on these.  However,
    none of the new equalities will contain t_j, so they have fewer
    occurrences of the t_i than the original equation.

(a) We could have t_j occurring in xi' for some j, with t' /=
    t_j. Then we substitute xi_j for t_j in xi' and continue.  However,
    since none of the t_i occur in xi_j, we have decreased the
    number of t_i that occur in xi', since we eliminated t_j and did not
    introduce any new ones.

\begin{code}
data TypeClassifier 
Ian Lynagh's avatar
Ian Lynagh committed
1022
  = FskCls TcTyVar      -- ^ Flatten skolem 
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1023
  | VarCls TcTyVar      -- ^ Non-flatten-skolem variable 
Ian Lynagh's avatar
Ian Lynagh committed
1024
1025
  | FunCls TyCon [Type] -- ^ Type function, exactly saturated
  | OtherCls TcType     -- ^ Neither of the above
1026
1027
1028


classify :: TcType -> TypeClassifier
1029
1030
1031
1032
1033

classify (TyVarTy tv) 
  | isTcTyVar tv, 
    FlatSkol {} <- tcTyVarDetails tv = FskCls tv
  | otherwise                        = VarCls tv
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
classify (TyConApp tc tys) | isSynFamilyTyCon tc
                           , tyConArity tc == length tys
                           = FunCls tc tys
classify ty                | Just ty' <- tcView ty
	                   = case classify ty' of
                               OtherCls {} -> OtherCls ty
                               var_or_fn   -> var_or_fn
                           | otherwise 
                           = OtherCls ty

-- See note [Canonical ordering for equality constraints].
1045
reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool	
1046
1047
1048
1049
1050
-- (t1 `reOrient` t2) responds True 
--   iff we should flip to (t2~t1)
-- We try to say False if possible, to minimise evidence generation
--
-- Postcondition: After re-orienting, first arg is not OTherCls
1051
1052
1053
1054
1055
1056
1057
reOrient _fl (OtherCls {}) (FunCls {})   = True
reOrient _fl (OtherCls {}) (FskCls {})   = True
reOrient _fl (OtherCls {}) (VarCls {})   = True
reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient"  -- One must be Var/Fun

reOrient _fl (FunCls {})   (VarCls _tv)  = False  
  -- But consider the following variation: isGiven fl && isMetaTyVar tv
1058
1059

  -- See Note [No touchables as FunEq RHS] in TcSMonad
1060
reOrient _fl (FunCls {}) _                = False             -- Fun/Other on rhs
1061

1062
reOrient _fl (VarCls {}) (FunCls {})      = True 
1063

1064
reOrient _fl (VarCls {}) (FskCls {})      = False
1065

1066
1067
reOrient _fl (VarCls {})  (OtherCls {})   = False
reOrient _fl (VarCls tv1)  (VarCls tv2)  
1068
1069
1070
  | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True 
  | otherwise                                = False 
  -- Just for efficiency, see CTyEqCan invariants 
1071

1072
reOrient _fl (FskCls {}) (VarCls tv2)     = isMetaTyVar tv2 
1073
  -- Just for efficiency, see CTyEqCan invariants
1074

1075
1076
1077
reOrient _fl (FskCls {}) (FskCls {})     = False
reOrient _fl (FskCls {}) (FunCls {})     = True 
reOrient _fl (FskCls {}) (OtherCls {})   = False 
1078
1079

------------------
1080
1081

canEqLeaf :: SubGoalDepth -- Depth
1082
          -> CtEvidence 
1083
1084
          -> Type -> Type 
          -> TcS StopOrContinue
1085
1086
1087
1088
-- Canonicalizing "leaf" equality constraints which cannot be
-- decomposed further (ie one of the types is a variable or
-- saturated type function application).  

1089
1090
1091
-- Preconditions: 
--    * one of the two arguments is variable or family applications
--    * the two types are not equal (looking through synonyms)
dimitris's avatar
dimitris committed
1092
canEqLeaf d fl s1 s2 
1093
  | cls1 `re_orient` cls2
dimitris's avatar
dimitris committed
1094
  = do { traceTcS "canEqLeaf (reorienting)" $ ppr fl <+> dcolon <+> pprEq s1 s2
1095
       ; let xcomp [x] = EvCoercion (mkTcSymCo (evTermCoercion x))
dimitris's avatar
dimitris committed
1096
             xcomp _ = panic "canEqLeaf: can't happen"
1097
             xdecomp x = [EvCoercion (mkTcSymCo (evTermCoercion x))]
dimitris's avatar
dimitris committed
1098
             xev = XEvTerm xcomp xdecomp
1099
1100
1101
1102
1103
1104
       ; ctevs <- xCtFlavor fl [mkTcEqPred s2 s1] xev 
       ; case ctevs of
           []     -> return Stop
           [ctev] -> canEqLeafOriented d ctev s2 s1
           _      -> panic "canEqLeaf" }

dimitris's avatar
dimitris committed
1105
1106
1107
1108
1109
1110
1111
1112
  | otherwise
  = do { traceTcS "canEqLeaf" $ ppr (mkTcEqPred s1 s2)
       ; canEqLeafOriented d fl s1 s2 }
  where
    re_orient = reOrient fl 
    cls1 = classify s1
    cls2 = classify s2

1113
canEqLeafOriented :: SubGoalDepth -- Depth
1114
                  -> CtEvidence
1115
1116
                  -> TcType -> TcType -> TcS StopOrContinue
-- By now s1 will either be a variable or a type family application
dimitris's avatar
dimitris committed
1117
1118
1119
canEqLeafOriented d fl s1 s2
  = can_eq_split_lhs d fl s1 s2
  where can_eq_split_lhs d fl s1 s2
1120
          | Just (fn,tys1) <- splitTyConApp_maybe s1
dimitris's avatar
dimitris committed
1121
          = canEqLeafFunEqLeftRec d fl (fn,tys1) s2
1122
          | Just tv <- getTyVar_maybe s1
dimitris's avatar
dimitris committed
1123
          = canEqLeafTyVarLeftRec d fl tv s2
1124
1125
          | otherwise
          = pprPanic "canEqLeafOriented" $
1126
            text "Non-variable or non-family equality LHS" <+> ppr (ctEvPred fl)
1127

1128
canEqLeafFunEqLeftRec :: SubGoalDepth
1129
                      -> CtEvidence
1130
                      -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
1131
canEqLeafFunEqLeftRec d fl (fn,tys1) ty2  -- fl :: F tys1 ~ ty2
1132
1133
  = do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
       ; (xis1,cos1) <- 
1134
           {-# SCC "flattenMany" #-}
1135
1136
           flattenMany d FMFullFlatten fl tys1 -- Flatten type function arguments
                                               -- cos1 :: xis1 ~ tys1
dimitris's avatar
dimitris committed
1137
1138
1139
1140
           
       ; let fam_head = mkTyConApp fn xis1
         -- Fancy higher-dimensional coercion between equalities!
       ; let co = mkTcTyConAppCo eqTyCon $ 
1141
1142
                  [mkTcReflCo (defaultKind $ typeKind ty2), mkTcTyConAppCo fn cos1, mkTcReflCo ty2]
             -- Why defaultKind? Same reason as the comment on TcType/mkTcEqPred. I trully hate this (DV)
dimitris's avatar
dimitris committed
1143
1144
1145
1146
1147
1148
1149
             -- co :: (F xis1 ~ ty2) ~ (F tys1 ~ ty2)
             
       ; mb <- rewriteCtFlavor fl (mkTcEqPred fam_head ty2) co
       ; case mb of 
           Nothing -> return Stop
           Just new_fl -> canEqLeafFunEqLeft d new_fl (fn,xis1) ty2 }

1150
1151

canEqLeafFunEqLeft :: SubGoalDepth -- Depth
1152
                   -> CtEvidence
dimitris's avatar
dimitris committed
1153
                   -> (TyCon,[Xi])
1154
1155
                   -> TcType -> TcS StopOrContinue
-- Precondition: No more flattening is needed for the LHS
dimitris's avatar
dimitris committed
1156
canEqLeafFunEqLeft d fl (fn,xis1) s2
1157
 = {-# SCC "canEqLeafFunEqLeft" #-}
1158
1159
   do { traceTcS "canEqLeafFunEqLeft" $ pprEq (mkTyConApp fn xis1) s2
      ; (xi2,co2) <- 
1160
          {-# SCC "flatten" #-} 
1161
          flatten d FMFullFlatten fl s2 -- co2 :: xi2 ~ s2
dimitris's avatar
dimitris committed
1162
1163
1164
          
      ; let fam_head = mkTyConApp fn xis1
      -- Fancy coercion between equalities! But it should just work! 
1165
1166
1167
      ; let co = mkTcTyConAppCo eqTyCon $ [ mkTcReflCo (defaultKind $ typeKind s2)
                                          , mkTcReflCo fam_head, co2 ]
            -- Why defaultKind? Same reason as the comment at TcType/mkTcEqPred
dimitris's avatar
dimitris committed
1168
1169
1170
1171
1172
1173
            -- co :: (F xis1 ~ xi2) ~ (F xis1 ~ s2)
            --           new pred         old pred
      ; mb <- rewriteCtFlavor fl (mkTcEqPred fam_head xi2) co
      ; case mb of
          Nothing -> return Stop
          Just new_fl -> continueWith $ 
1174
                         CFunEqCan { cc_ev = new_fl, cc_depth = d
dimitris's avatar
dimitris committed
1175
1176
                                   , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } }   

1177
1178

canEqLeafTyVarLeftRec :: SubGoalDepth
1179
                      -> CtEvidence
1180
                      -> TcTyVar -> TcType -> TcS StopOrContinue
dimitris's avatar
dimitris committed
1181
canEqLeafTyV