TcCanonical.lhs 55.4 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, occurCheckExpand, emitWorkNC,
11
    StopOrContinue (..)
12
13
14
15
16
17
 ) where

#include "HsVersions.h"

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

import VarSet
33
import TcSMonad
34
import FastString
35

36
import Util
37
import Maybes( catMaybes )
38
\end{code}
39
40
41
42


%************************************************************************
%*                                                                      *
43
%*                      The Canonicaliser                               *
44
45
46
%*                                                                      *
%************************************************************************

47
48
Note [Canonicalization]
~~~~~~~~~~~~~~~~~~~~~~~
49

50
51
52
53
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).
54

55
56
57
58
59
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. 
60

61
62
63
64
  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. 
65

66
67
  3) If no more decomposition is possible, we deeply apply the substitution
     from the inert_eqs and continue with flattening.
68

69
70
71
72
73
  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. 
74

75
76
77
78
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
79

80
\begin{code}
81

82
83
84
85
86
87
88
-- 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. 
89

90
91
92
instance Outputable StopOrContinue where
  ppr Stop             = ptext (sLit "Stop")
  ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
93
94


95
96
continueWith :: Ct -> TcS StopOrContinue
continueWith = return . ContinueWith
97

98
99
100
101
102
103
104
105
andWhenContinue :: TcS StopOrContinue 
                -> (Ct -> TcS StopOrContinue) 
                -> TcS StopOrContinue
andWhenContinue tcs1 tcs2
  = do { r <- tcs1
       ; case r of
           Stop            -> return Stop
           ContinueWith ct -> tcs2 ct }
106
107
108

\end{code}

109
110
Note [Caching for canonicals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
111
112
113
114
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:
115

116
117
InertSet = { [W] d1 : Num t } 
WorkList = { [W] d2 : Num t, [W] c : t ~ Int} 
118

Simon Peyton Jones's avatar
Simon Peyton Jones committed
119
120
121
122
123
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:
124
125
126
127
128
129
130
131
 
   - 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
132
133
134
   - 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:
135
136
137
        InertSet : { [G] c : t ~ Int }
        WorkList : { [W] d1 : Num t} 

Simon Peyton Jones's avatar
Simon Peyton Jones committed
138
139
   - Now we examine (d1), we observe that there is a binding for (Num
     t) in the evidence binds and we set:
140
141
142
             d1 := d2 
     and end up in a loop!

Simon Peyton Jones's avatar
Simon Peyton Jones committed
143
144
145
146
147
148
149
150
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.
151

Simon Peyton Jones's avatar
Simon Peyton Jones committed
152
153
154
155
156
157
158
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.
159

160
161


162
\begin{code}
163

164
165
166
167
-- Top-level canonicalization
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

canonicalize :: Ct -> TcS StopOrContinue
168
canonicalize ct@(CNonCanonical { cc_ev = ev, cc_loc  = d })
169
  = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
170
       ; {-# SCC "canEvVar" #-}
171
         canEvNC d ev }
172

173
174
canonicalize (CDictCan { cc_loc  = d
                       , cc_ev = ev
175
176
                       , cc_class  = cls
                       , cc_tyargs = xis })
177
  = {-# SCC "canClass" #-}
178
179
180
    canClass d ev cls xis -- Do not add any superclasses
canonicalize (CTyEqCan { cc_loc  = d
                       , cc_ev = ev
181
182
                       , cc_tyvar  = tv
                       , cc_rhs    = xi })
183
184
  = {-# SCC "canEqLeafTyVarEq" #-}
    canEqLeafTyVarEq d ev tv xi
185

186
187
canonicalize (CFunEqCan { cc_loc = d
                        , cc_ev = ev
188
189
190
                        , cc_fun    = fn
                        , cc_tyargs = xis1
                        , cc_rhs    = xi2 })
Simon Peyton Jones's avatar
Simon Peyton Jones committed
191
  = {-# SCC "canEqLeafFunEq" #-}
192
    canEqLeafFunEq d ev fn xis1 xi2
193

194
canonicalize (CIrredEvCan { cc_ev = ev
195
196
197
198
                          , cc_loc = d })
  = canIrred d ev
canonicalize (CHoleCan { cc_ev = ev, cc_loc = d })
  = canHole d ev
199

200
canEvNC :: CtLoc -> CtEvidence -> TcS StopOrContinue
201
-- Called only for non-canonical EvVars 
202
203
204
205
206
canEvNC d ev 
  = case classifyPredType (ctEvPred ev) of
      ClassPred cls tys -> canClassNC d ev cls tys 
      EqPred ty1 ty2    -> canEqNC    d ev ty1 ty2 
      TuplePred tys     -> canTuple   d ev tys
207
      IrredPred {}      -> canIrred   d ev 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
208
209
210
211
212
213
214
215
216
217
\end{code}


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

\begin{code}
218
219
canTuple :: CtLoc -> CtEvidence -> [PredType] -> TcS StopOrContinue
canTuple d ev tys
dimitris's avatar
dimitris committed
220
221
222
  = do { traceTcS "can_pred" (text "TuplePred!")
       ; let xcomp = EvTupleMk
             xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]             
223
       ; ctevs <- xCtFlavor ev tys (XEvTerm xcomp xdecomp)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
224
       ; canEvVarsCreated d ctevs }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
225
226
227
228
229
230
231
\end{code}

%************************************************************************
%*                                                                      *
%*                      Class Canonicalization
%*                                                                      *
%************************************************************************
232

Simon Peyton Jones's avatar
Simon Peyton Jones committed
233
234
\begin{code}
canClass, canClassNC 
235
   :: CtLoc
236
   -> CtEvidence  
Simon Peyton Jones's avatar
Simon Peyton Jones committed
237
   -> Class -> [Type] -> TcS StopOrContinue
238
-- Precondition: EvVar is class evidence 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
239
240
241
242
243
244

-- 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

245
246
canClassNC d ev cls tys 
  = canClass d ev cls tys 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
247
248
    `andWhenContinue` emitSuperclasses

249
canClass d ev cls tys
250
  = do { -- sctx <- getTcSContext
251
       ; (xis, cos) <- flattenMany d FMFullFlatten (ctEvFlavour ev) tys
252
       ; let co = mkTcTyConAppCo (classTyCon cls) cos 
253
             xi = mkClassPred cls xis
dimitris's avatar
dimitris committed
254
             
255
       ; mb <- rewriteCtFlavor ev xi co
256

dimitris's avatar
dimitris committed
257
       ; case mb of
258
259
           Just new_ev -> 
             let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_ev)
260
             in continueWith $ 
261
262
                CDictCan { cc_ev = new_ev, cc_loc = d
                         , cc_tyargs = xis_for_dict, cc_class = cls }
dimitris's avatar
dimitris committed
263
264
           Nothing -> return Stop }

Simon Peyton Jones's avatar
Simon Peyton Jones committed
265
emitSuperclasses :: Ct -> TcS StopOrContinue
266
emitSuperclasses ct@(CDictCan { cc_loc = d, cc_ev = ev
Simon Peyton Jones's avatar
Simon Peyton Jones committed
267
268
269
                              , 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. 
270
 = do { newSCWorkFromFlavored d ev cls xis_new
Simon Peyton Jones's avatar
Simon Peyton Jones committed
271
272
273
274
275
      -- 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!"
276
277
278
279
280
281
282
283
284
285
286
287
288
289
\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: 
290
291
       Generally speaking we want to be able to add superclasses of 
       wanteds for two reasons:
292

293
294
295
296
297
298
299
300
301
       (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. 
302

303
304
305
306
307
308
309
310
311
312
313
314
       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. 
315

316
       See also [New Wanted Superclass Work] in TcInteract. 
317

318
319
320

For Deriveds: 
       We do nothing.
321
322
323

Here's an example that demonstrates why we chose to NOT add
superclasses during simplification: [Comes from ticket #4497]
dimitris's avatar
dimitris committed
324
 
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
   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}
342
newSCWorkFromFlavored :: CtLoc -- Depth
343
                      -> CtEvidence -> Class -> [Xi] -> TcS ()
344
-- Returns superclasses, see Note [Adding superclasses]
dimitris's avatar
dimitris committed
345
newSCWorkFromFlavored d flavor cls xis 
batterseapower's avatar
batterseapower committed
346
  | isDerived flavor 
347
348
  = return ()  -- Deriveds don't yield more superclasses because we will
               -- add them transitively in the case of wanteds. 
dimitris's avatar
dimitris committed
349
350
351
    
  | isGiven flavor 
  = do { let sc_theta = immSuperClasses cls xis 
352
353
354
             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 }
355
       ; ctevs <- xCtFlavor flavor sc_theta xev
Simon Peyton Jones's avatar
Simon Peyton Jones committed
356
       ; emitWorkNC d ctevs }
dimitris's avatar
dimitris committed
357
358

  | isEmptyVarSet (tyVarsOfTypes xis)
359
  = return () -- Wanteds with no variables yield no deriveds.
360
              -- See Note [Improvement from Ground Wanteds]
361

362
  | otherwise -- Wanted case, just add those SC that can lead to improvement. 
363
  = do { let sc_rec_theta = transSuperClasses cls xis 
364
365
             impr_theta   = filter is_improvement_pty sc_rec_theta
       ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
366
       ; mb_der_evs <- mapM newDerived impr_theta
Simon Peyton Jones's avatar
Simon Peyton Jones committed
367
       ; emitWorkNC d (catMaybes mb_der_evs) }
368
369
370

is_improvement_pty :: PredType -> Bool 
-- Either it's an equality, or has some functional dependency
371
is_improvement_pty ty = go (classifyPredType ty)
batterseapower's avatar
batterseapower committed
372
373
  where
    go (EqPred {})         = True 
374
375
376
    go (ClassPred cls _tys) = not $ null fundeps
      where (_,fundeps) = classTvsFds cls
    go (TuplePred ts)      = any is_improvement_pty ts
batterseapower's avatar
batterseapower committed
377
    go (IrredPred {})      = True -- Might have equalities after reduction?
378
\end{code}
379
380


Simon Peyton Jones's avatar
Simon Peyton Jones committed
381
382
383
384
385
386
%************************************************************************
%*                                                                      *
%*                      Irreducibles canonicalization
%*                                                                      *
%************************************************************************

387

388
\begin{code}
389
canIrred :: CtLoc -> CtEvidence -> TcS StopOrContinue
390
-- Precondition: ty not a tuple and no other evidence form
391
392
393
canIrred d ev
  = do { let ty = ctEvPred ev
       ; traceTcS "can_pred" (text "IrredPred = " <+> ppr ty) 
394
       ; (xi,co) <- flatten d FMFullFlatten (ctEvFlavour ev) ty -- co :: xi ~ ty
395
       ; let no_flattening = xi `eqType` ty 
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
             -- We can't use isTcReflCo, because even if the coercion is
             -- Refl, the output type might have had a substitution 
             -- applied to it.  For example  'a' might now be 'C b'

       ; if no_flattening then
           continueWith $
           CIrredEvCan { cc_ev = ev, cc_loc = d }
         else do
       { mb <- rewriteCtFlavor ev xi co 
       ; case mb of
             Just new_ev -> canEvNC d new_ev  -- Re-classify and try again
             Nothing     -> return Stop } }   -- Found a cached copy

canHole :: CtLoc -> CtEvidence -> TcS StopOrContinue
canHole d ev 
  = do { let ty = ctEvPred ev
412
       ; (xi,co) <- flatten d FMFullFlatten (ctEvFlavour ev) ty -- co :: xi ~ ty
413
       ; mb <- rewriteCtFlavor ev xi co 
dimitris's avatar
dimitris committed
414
       ; case mb of
415
416
417
             Just new_ev -> emitInsoluble (CHoleCan { cc_ev = new_ev, cc_loc = d})
             Nothing     -> return ()   -- Found a cached copy; won't happen
       ; return Stop } 
418
\end{code}
419

420
421
422
423
424
425
426
427
428
429
%************************************************************************
%*                                                                      *
%*        Flattening (eliminating all function symbols)                 *
%*                                                                      *
%************************************************************************

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

432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
      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}

468
data FlattenMode = FMSubstOnly | FMFullFlatten
469

470
-- Flatten a bunch of types all at once.
471
flattenMany :: CtLoc -> FlattenMode
472
            -> CtFlavour -> [Type] -> TcS ([Xi], [TcCoercion])
473
-- Coercions :: Xi ~ Type 
474
-- Returns True iff (no flattening happened)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
475
476
477
-- NB: The EvVar inside the 'ctxt :: CtEvidence' is unused, 
--     we merely want (a) Given/Solved/Derived/Wanted info
--                    (b) the GivenLoc/WantedLoc for when we create new evidence
478
flattenMany d f ctxt tys 
479
480
  = -- pprTrace "flattenMany" empty $
    go tys 
481
  where go []       = return ([],[])
482
        go (ty:tys) = do { (xi,co)    <- flatten d f ctxt ty
483
484
                         ; (xis,cos)  <- go tys
                         ; return (xi:xis,co:cos) }
485
486
487
488

-- 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.
489
flatten :: CtLoc -> FlattenMode 
490
        -> CtFlavour -> TcType -> TcS (Xi, TcCoercion)
491
-- Postcondition: Coercion :: Xi ~ TcType
492
flatten loc f ctxt ty 
493
  | Just ty' <- tcView ty
494
  = do { (xi, co) <- flatten loc f ctxt ty'
495
496
       ; if eqType xi ty then return (ty,co) else return (xi,co) } 
       -- Small tweak for better error messages 
497

498
flatten _ _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
499

500
501
flatten loc f ctxt (TyVarTy tv)
  = flattenTyVar loc f ctxt tv
502

503
504
505
flatten loc f ctxt (AppTy ty1 ty2)
  = do { (xi1,co1) <- flatten loc f ctxt ty1
       ; (xi2,co2) <- flatten loc f ctxt ty2
506
       ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
507

508
509
510
flatten loc f ctxt (FunTy ty1 ty2)
  = do { (xi1,co1) <- flatten loc f ctxt ty1
       ; (xi2,co2) <- flatten loc f ctxt ty2
511
       ; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
512

513
flatten loc f ctxt (TyConApp tc tys)
514
515
516
  -- For a normal type constructor or data family application, we just
  -- recursively flatten the arguments.
  | not (isSynFamilyTyCon tc)
517
    = do { (xis,cos) <- flattenMany loc f ctxt tys
518
         ; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
519
520
521
522
523
524

  -- 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
525
      do { (xis, cos) <- flattenMany loc f ctxt tys
526
527
         ; let (xi_args,  xi_rest)  = splitAt (tyConArity tc) xis
               (cos_args, cos_rest) = splitAt (tyConArity tc) cos
528
529
530
531
	       	 -- 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
532
               
533
         ; (ret_co, rhs_xi) <-
534
535
             case f of 
               FMSubstOnly -> 
536
                 return (mkTcReflCo fam_ty, fam_ty)
537
               FMFullFlatten -> 
538
539
                 do { mb_ct <- lookupFlatEqn fam_ty
                    ; case mb_ct of
540
                        Just ct 
541
                          | let ctev = cc_ev ct
542
543
                                flav = ctEvFlavour ctev
                          , flav `canRewrite` ctxt 
544
545
546
547
548
549
550
551
552
553
                          -> -- 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
554
                               ; (flat_rhs_xi,co) <- flatten (cc_loc ct) f flav rhs_xi
555
556
                               ; let final_co = evTermCoercion (ctEvTerm ctev)
                                                `mkTcTransCo` mkTcSymCo co
557
                               ; return (final_co, flat_rhs_xi) }
dimitris's avatar
dimitris committed
558
                          
559
                        _ | Given <- ctxt -- Given: make new flatten skolem
560
                          -> do { traceTcS "flatten/flat-cache miss" $ empty 
561
562
                                ; rhs_ty <- newFlattenSkolemTy fam_ty
                                ; let co     = mkTcReflCo fam_ty
563
                                      new_ev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
564
                                                       , ctev_evtm = EvCoercion co }
565
                                      ct = CFunEqCan { cc_ev = new_ev
566
                                                     , cc_fun    = tc 
567
568
                            			     , cc_tyargs = xi_args    
                            			     , cc_rhs    = rhs_ty
569
                            			     , cc_loc  = loc }
570
571
572
                                ; updWorkListTcS $ extendWorkListEq ct
                                ; return (co, rhs_ty) }

573
574
575
                         | otherwise -- Wanted or Derived: make new unification variable
                         -> do { traceTcS "flatten/flat-cache miss" $ empty 
                               ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
576
                               ; let pred = mkTcEqPred fam_ty rhs_xi_var
577
                               ; mw <- newWantedEvVar pred
578
                               ; case mw of
579
580
                                   Fresh ctev -> 
                                     do { let ct = CFunEqCan { cc_ev = ctev
dimitris's avatar
dimitris committed
581
582
583
                                                             , cc_fun = tc
                                                             , cc_tyargs = xi_args
                                                             , cc_rhs    = rhs_xi_var 
584
                                                             , cc_loc    = loc }
585
586
                                        ; updWorkListTcS $ extendWorkListEq ct
                                        ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
dimitris's avatar
dimitris committed
587
                                   Cached {} -> panic "flatten TyConApp, var must be fresh!" } 
588
                    }
dimitris's avatar
dimitris committed
589
590
591
592
593
594
595
                  -- Emit the flat constraints
         ; 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
                  ) 
         }
596

597
flatten loc _f ctxt ty@(ForAllTy {})
598
599
600
-- 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
601
       ; (rho', co) <- flatten loc FMSubstOnly ctxt rho   
602
603
                         -- Substitute only under a forall
                         -- See Note [Flattening under a forall]
604
       ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
605
606
\end{code}

607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
Note [Flattening under a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Under a forall, we
  (a) MUST apply the inert subsitution
  (b) MUST NOT flatten type family applications
Hence FMSubstOnly.

For (a) consider   c ~ a, a ~ T (forall b. (b, [c])
If we don't apply the c~a substitution to the second constraint
we won't see the occurs-check error.

For (b) consider  (a ~ forall b. F a b), we don't want to flatten
to     (a ~ forall b.fsk, F a b ~ fsk)
because now the 'b' has escaped its scope.  We'd have to flatten to
       (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
and we have not begun to think about how to make that work!

Simon Peyton Jones's avatar
Simon Peyton Jones committed
624
\begin{code}
625
626
627
flattenTyVar, flattenFinalTyVar
        :: CtLoc -> FlattenMode 
        -> CtFlavour -> TcTyVar -> TcS (Xi, TcCoercion)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
628
-- "Flattening" a type variable means to apply the substitution to it
629
630
631
-- The substitution is actually the union of the substitution in the TyBinds
-- for the unification variables that have been unified already with the inert
-- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract.
632
flattenTyVar loc f ctxt tv
633
634
635
  | not (isTcTyVar tv)	              -- Happens when flatten under a (forall a. ty)
  = flattenFinalTyVar loc f ctxt tv   -- So ty contains referneces to the non-TcTyVar a
  | otherwise
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
  = do { mb_ty <- isFilledMetaTyVar_maybe tv
       ; case mb_ty of {
           Just ty -> flatten loc f ctxt ty ;
           Nothing -> 

    -- Try in ty_binds
    do { ty_binds <- getTcSTyBindsMap
       ; case lookupVarEnv ty_binds tv of {
           Just (_tv,ty) -> flatten loc f ctxt ty ;
                 -- NB: ty_binds coercions are all ReflCo,
                 -- so no need to transitively compose co' with another coercion,
                 -- unlike in 'flatten_from_inerts'
           Nothing -> 

    -- Try in the inert equalities
    do { ieqs <- getInertEqs
       ; let mco = tv_eq_subst ieqs tv  -- co : v ~ ty
       ; case mco of { 
           Just (co,ty) -> 
             do { (ty_final,co') <- flatten loc f ctxt ty
                ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } ;
       -- NB recursive call. 
       -- 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]

662
           Nothing -> flattenFinalTyVar loc f ctxt tv
663
    } } } } } } 
664
  where
665
666
667
    tv_eq_subst subst tv
       | Just ct <- lookupVarEnv subst tv
       , let ctev = cc_ev ct
668
       , ctEvFlavour ctev `canRewrite` ctxt
669
670
671
672
       = 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
673
674
675
676
677
678
679

flattenFinalTyVar loc f ctxt tv
  = -- Done, but make sure the kind is zonked
    do { let knd = tyVarKind tv
       ; (new_knd,_kind_co) <- flatten loc f ctxt knd
       ; let ty = mkTyVarTy (setVarType tv new_knd)
       ; return (ty, mkTcReflCo ty) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
680
681
682
683
684
685
686
687
688
\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
689
 [G] g1 : ta8 ~ ta4
Simon Peyton Jones's avatar
Simon Peyton Jones committed
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
 [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.
707

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
710
711
712
713
714
715
716
717

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

\begin{code}
718
719
canEvVarsCreated :: CtLoc -> [CtEvidence] -> TcS StopOrContinue
canEvVarsCreated _loc [] = return Stop
Simon Peyton Jones's avatar
Simon Peyton Jones committed
720
721
    -- Add all but one to the work list
    -- and return the first (if any) for futher processing
722
723
canEvVarsCreated loc (ev : evs) 
  = do { emitWorkNC loc evs; canEvNC loc ev }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
724
725
          -- Note the "NC": these are fresh goals, not necessarily canonical

726
727
emitWorkNC :: CtLoc -> [CtEvidence] -> TcS ()
emitWorkNC loc evs 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
728
729
730
  | null evs  = return ()
  | otherwise = updWorkListTcS (extendWorkListCts (map mk_nc evs))
  where
731
    mk_nc ev = CNonCanonical { cc_ev = ev, cc_loc = loc }
dimitris's avatar
dimitris committed
732

Simon Peyton Jones's avatar
Simon Peyton Jones committed
733
-------------------------
734
canEqNC, canEq :: CtLoc -> CtEvidence -> Type -> Type -> TcS StopOrContinue
Simon Peyton Jones's avatar
Simon Peyton Jones committed
735

736
737
canEqNC loc ev ty1 ty2
  = canEq loc ev ty1 ty2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
738
739
    `andWhenContinue` emitKindConstraint

740
canEq _loc ev ty1 ty2
741
  | eqType ty1 ty2	-- Dealing with equality here avoids
742
    	     	 	-- later spurious occurs checks for a~a
743
744
  = if isWanted ev then
      setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo ty1)) >> return Stop
dimitris's avatar
dimitris committed
745
746
    else
      return Stop
747

748
-- If one side is a variable, orient and flatten,
749
-- WITHOUT expanding type synonyms, so that we tend to 
750
-- substitute a ~ Age rather than a ~ Int when @type Age = Int@
751
752
753
754
canEq loc ev ty1@(TyVarTy {}) ty2 
  = canEqLeaf loc ev ty1 ty2
canEq loc ev ty1 ty2@(TyVarTy {})
  = canEqLeaf loc ev ty1 ty2
755

756
-- See Note [Naked given applications]
757
758
759
canEq loc ev ty1 ty2
  | Just ty1' <- tcView ty1 = canEq loc ev ty1' ty2
  | Just ty2' <- tcView ty2 = canEq loc ev ty1  ty2'
760

761
canEq loc ev ty1@(TyConApp fn tys) ty2
762
  | isSynFamilyTyCon fn, length tys == tyConArity fn
763
764
  = canEqLeaf loc ev ty1 ty2
canEq loc ev ty1 ty2@(TyConApp fn tys)
765
  | isSynFamilyTyCon fn, length tys == tyConArity fn
766
  = canEqLeaf loc ev ty1 ty2
767

768
canEq loc ev ty1 ty2
769
770
771
  | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
  , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
  , isDecomposableTyCon tc1 && isDecomposableTyCon tc2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
772
  = canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2 
773

774
canEq loc ev s1@(ForAllTy {}) s2@(ForAllTy {})
775
 | tcIsForAllTy s1, tcIsForAllTy s2
776
 , CtWanted { ctev_evar = orig_ev } <- ev 
777
778
779
 = do { let (tvs1,body1) = tcSplitForAllTys s1
            (tvs2,body2) = tcSplitForAllTys s2
      ; if not (equalLength tvs1 tvs2) then 
780
          canEqFailure loc ev s1 s2
781
        else
782
          do { traceTcS "Creating implication for polytype equality" $ ppr ev
783
784
             ; deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2) 
             ; return Stop } }
785
 | otherwise
786
 = do { traceTcS "Ommitting decomposition of given polytype equality" $ 
787
        pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
788
      ; return Stop }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
789
790
791
792
793
794
795
796
797
798
799
800
801
802

-- The last remaining source of success is an application
-- e.g.  F a b ~ Maybe c   where F has arity 1
-- See Note [Equality between type applications]
--     Note [Care with type applications] in TcUnify
canEq loc ev ty1 ty2 
 =  do { let flav = ctEvFlavour ev
       ; (s1, co1) <- flatten loc FMSubstOnly flav ty1
       ; (s2, co2) <- flatten loc FMSubstOnly flav ty2
       ; mb_ct <- rewriteCtFlavor ev (mkTcEqPred s1 s2) (mkHdEqPred s2 co1 co2)
       ; case mb_ct of
           Nothing     -> return Stop
           Just new_ev -> last_chance new_ev s1 s2 }
  where
803
    last_chance ev ty1 ty2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
804
805
806
      | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
      , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
      , isDecomposableTyCon tc1 && isDecomposableTyCon tc2
807
      = canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
808
809
810
811
812
813
814
815
816
817
818
    
      | Just (s1,t1) <- tcSplitAppTy_maybe ty1
      , Just (s2,t2) <- tcSplitAppTy_maybe ty2
      = do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
             	 xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
             	 xevdecomp x = let xco = evTermCoercion x 
       	                       in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
       	   ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
       	   ; canEvVarsCreated loc ctevs }

      | otherwise
819
      = do { emitInsoluble (CNonCanonical { cc_ev = ev, cc_loc = loc })
Simon Peyton Jones's avatar
Simon Peyton Jones committed
820
           ; return Stop }
821

Simon Peyton Jones's avatar
Simon Peyton Jones committed
822
------------------------
Simon Peyton Jones's avatar
Simon Peyton Jones committed
823
824
825
826
827
828
829
830
831
832
833
834
835
canDecomposableTyConApp :: CtLoc -> CtEvidence 
                        -> TyCon -> [TcType] 
                        -> TyCon -> [TcType] 
                        -> TcS StopOrContinue
canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
  | tc1 /= tc2 || length tys1 /= length tys2
    -- Fail straight away for better error messages
  = canEqFailure loc ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
  | otherwise
  = 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 ev (zipWith mkTcEqPred tys1 tys2) xev
836
       ; canEvVarsCreated loc ctevs }
837

838
839
840
841
842
843
844
845
846
847
848
canEqFailure :: CtLoc -> CtEvidence -> TcType -> TcType -> TcS StopOrContinue
-- See Note [Make sure that insolubles are fully rewritten]
canEqFailure loc ev ty1 ty2
  = do { let flav = ctEvFlavour ev
       ; (s1, co1) <- flatten loc FMSubstOnly flav ty1
       ; (s2, co2) <- flatten loc FMSubstOnly flav ty2
       ; mb_ct <- rewriteCtFlavor ev (mkTcEqPred s1 s2)
                                     (mkHdEqPred s2 co1 co2)
       ; case mb_ct of
           Just new_ev -> emitInsoluble (CNonCanonical { cc_ev = new_ev, cc_loc = loc }) 
           Nothing -> pprPanic "canEqFailure" (ppr ev $$ ppr ty1 $$ ppr ty2)
849
       ; return Stop }
dimitris's avatar
dimitris committed
850

Simon Peyton Jones's avatar
Simon Peyton Jones committed
851
852
------------------------
emitKindConstraint :: Ct -> TcS StopOrContinue
Simon Peyton Jones's avatar
Simon Peyton Jones committed
853
emitKindConstraint ct   -- By now ct is canonical
Simon Peyton Jones's avatar
Simon Peyton Jones committed
854
  = case ct of 
855
856
      CTyEqCan { cc_loc = loc
               , cc_ev = ev, cc_tyvar = tv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
857
               , cc_rhs = ty }
858
          -> emit_kind_constraint loc ev (mkTyVarTy tv) ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
859

860
861
      CFunEqCan { cc_loc = loc
                , cc_ev = ev
Simon Peyton Jones's avatar
Simon Peyton Jones committed
862
863
                , cc_fun = fn, cc_tyargs = xis1
                , cc_rhs = xi2 }
864
          -> emit_kind_constraint loc ev (mkTyConApp fn xis1) xi2
865

dimitris's avatar
dimitris committed
866
      _   -> continueWith ct
Simon Peyton Jones's avatar
Simon Peyton Jones committed
867
  where
868
    emit_kind_constraint loc _ev ty1 ty2 
869
870
871
       | 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
872
       | otherwise
873
       = ASSERT( isKind k1 && isKind k2 )
874
875
876
877
878
         do { mw <- newDerived (mkEqPred k1 k2) 
            ; case mw of
                Nothing  -> return ()
                Just kev -> emitWorkNC kind_co_loc [kev]
            ; continueWith ct }
879
       where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
880
881
         k1 = typeKind ty1
         k2 = typeKind ty2
882

Simon Peyton Jones's avatar
Simon Peyton Jones committed
883
884
         -- Always create a Wanted kind equality even if 
         -- you are decomposing a given constraint.
dimitris's avatar
dimitris committed
885
         -- NB: DV finds this reasonable for now. Maybe we have to revisit.
886
         kind_co_loc = setCtLocOrigin loc (KindEqOrigin ty1 ty2 (ctLocOrigin loc))
887
888
\end{code}

889
890
891
892
893
894
895
896
897
898
899
Note [Make sure that insolubles are fully rewritten]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When an equality fails, we still want to rewrite the equality 
all the way down, so that it accurately reflects 
 (a) the mutable reference substitution in force at start of solving
 (b) any ty-binds in force at this point in solving
See Note [Kick out insolubles] in TcInteract.
And if we don't do this there is a bad danger that 
TcSimplify.applyTyVarDefaulting will find a variable
that has in fact been substituted.

900
901
902
903
904
905
906
Note [Do not decompose given polytype equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider [G] (forall a. t1 ~ forall a. t2).  Can we decompose this?
No -- what would the evidence look like.  So instead we simply discard
this given evidence.   


907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
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.
   

922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
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


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
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
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 
1049
  = VarCls TcTyVar      -- ^ Type variable 
Ian Lynagh's avatar
Ian Lynagh committed
1050
1051
  | FunCls TyCon [Type] -- ^ Type function, exactly saturated
  | OtherCls TcType     -- ^ Neither of the above
1052
1053
1054


classify :: TcType -> TypeClassifier
1055

1056
classify (TyVarTy tv) = ASSERT2( isTcTyVar tv, ppr tv ) VarCls tv
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
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].
1068
reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool	
1069
1070
1071
1072
1073
-- (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
1074
1075
reOrient _ev (OtherCls {}) cls2 = ASSERT( case cls2 of { OtherCls {} -> False; _ -> True } )
                                  True  -- One must be Var/Fun
1076

1077
reOrient _ev (FunCls {}) _      = False             -- Fun/Other on rhs
1078
  -- But consider the following variation: isGiven ev && isMetaTyVar tv
1079
  -- See Note [No touchables as FunEq RHS] in TcSMonad
1080

1081
1082
reOrient _ev (VarCls {})   (FunCls {})      = True 
reOrient _ev (VarCls {})   (OtherCls {})   = False
1083
reOrient _ev (VarCls tv1)  (VarCls tv2)  
1084
1085
1086
  | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True 
  | otherwise                                = False 
  -- Just for efficiency, see CTyEqCan invariants 
1087
1088

------------------
1089

1090
canEqLeaf :: CtLoc -> CtEvidence 
1091
1092
          -> Type -> Type 
          -> TcS StopOrContinue
1093
1094
1095
1096
-- Canonicalizing "leaf" equality constraints which cannot be
-- decomposed further (ie one of the types is a variable or
-- saturated type function application).  

1097
-- Preconditions: 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1098
1099
--    * one of the two arguments is variable 
--      or an exactly-saturated family application
1100
--    * the two types are not equal (looking through synonyms)
1101
canEqLeaf loc ev s1 s2 
1102
  | cls1 `re_orient` cls2
1103
  = do { traceTcS "canEqLeaf (reorienting)" $ ppr ev <+> dcolon <+> pprEq s1 s2
1104
       ; let xcomp [x] = EvCoercion (mkTcSymCo (evTermCoercion x))
dimitris's avatar
dimitris committed
1105
             xcomp _ = panic "canEqLeaf: can't happen"
1106
             xdecomp x = [EvCoercion (mkTcSymCo (evTermCoercion x))]
dimitris's avatar
dimitris committed
1107
             xev = XEvTerm xcomp xdecomp
1108
       ; ctevs <- xCtFlavor ev [mkTcEqPred s2 s1] xev 
1109
1110
       ; case ctevs of
           []     -> return Stop
1111
           [ctev] -> canEqLeafOriented loc ctev cls2 s1
1112
1113
           _      -> panic "canEqLeaf" }

dimitris's avatar
dimitris committed
1114
1115
  | otherwise
  = do { traceTcS "canEqLeaf" $ ppr (mkTcEqPred s1 s2)
1116
       ; canEqLeafOriented loc ev cls1 s2 }
dimitris's avatar
dimitris committed
1117
  where
1118
    re_orient = reOrient ev 
dimitris's avatar
dimitris committed
1119
1120
1121
    cls1 = classify s1
    cls2 = classify s2

1122
canEqLeafOriented :: CtLoc -> CtEvidence
1123
                  -> TypeClassifier -> TcType -> TcS StopOrContinue
1124
-- By now s1 will either be a variable or a type family application
1125
1126
1127
canEqLeafOriented loc ev (FunCls fn tys1) s2 = canEqLeafFunEq loc ev fn tys1 s2
canEqLeafOriented loc ev (VarCls tv)      s2 = canEqLeafTyVarEq loc ev tv s2
canEqLeafOriented _   ev (OtherCls {})    _  = pprPanic "canEqLeafOriented" (ppr (ctEvPred ev))
1128

1129
canEqLeafFunEq :: CtLoc -> CtEvidence
1130
1131
               -> TyCon -> [TcType] -> TcType -> TcS StopOrContinue
canEqLeafFunEq loc ev fn tys1 ty2  -- ev :: F tys1 ~ ty2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1132
  = do { traceTcS "canEqLeafFunEq" $ pprEq (mkTyConApp fn tys1) ty2
1133
       ; let flav = ctEvFlavour ev
1134
1135
1136
1137
1138
1139

            -- Flatten type function arguments
            -- cos1 :: xis1 ~ tys1
            -- co2  :: xi2 ~ ty2
      ; (xis1,cos1) <- flattenMany loc FMFullFlatten flav tys1 
      ; (xi2, co2)  <- flatten     loc FMFullFlatten flav ty2
dimitris's avatar
dimitris committed
1140
           
1141
          -- Fancy higher-dimensional coercion between equalities!
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1142
         -- SPJ asks why?  Why not just co : F xis1 ~ F tys1?
1143
1144
       ; let fam_head = mkTyConApp fn xis1
             xco = mkHdEqPred ty2 (mkTcTyConAppCo fn cos1) co2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1145
             -- xco :: (F xis1 ~ xi2) ~ (F tys1 ~ ty2)
dimitris's avatar
dimitris committed
1146
             
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1147
1148
1149
1150
1151
1152
1153
       ; mb <- rewriteCtFlavor ev (mkTcEqPred fam_head xi2) xco
       ; case mb of {
           Nothing -> return Stop ;
           Just new_ev 
             | isTcReflCo xco -> continueWith new_ct
             | otherwise      -> do { updWorkListTcS (extendWorkListEq new_ct); return Stop }
             where
1154
               new_ct = CFunEqCan { cc_ev = new_ev, cc_loc = loc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1155
                                  , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } } } 
dimitris's avatar
dimitris committed
1156

1157

1158
canEqLeafTyVarEq :: CtLoc -> CtEvidence
1159
                   -> TcTyVar -> TcType -> TcS StopOrContinue
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
canEqLeafTyVarEq loc ev tv s2              -- ev :: tv ~ s2
  = do { traceTcS "canEqLeafTyVarEq" $ pprEq (mkTyVarTy tv) s2
       ; let flav = ctEvFlavour ev
       ; (xi1,co1) <- flattenTyVar loc FMFullFlatten flav tv -- co1 :: xi1 ~ tv
       ; (xi2,co2) <- flatten      loc FMFullFlatten flav s2 -- co2 :: xi2 ~ s2 
       ; let co = mkHdEqPred s2 co1 co2
             -- co :: (xi1 ~ xi2) ~ (tv ~ s2)
       
       ; traceTcS "canEqLeafTyVarEq2" $ empty 
       ; case (getTyVar_maybe xi1, getTyVar_maybe xi2) of {
           (Nothing,  _) -> -- Rewriting the LHS did not yield a type variable
                            -- so go around again to canEq
                            do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
                               ; case mb of
                                   Nothing     -> return Stop
                                   Just new_ev -> canEq loc new_ev xi1 xi2 } ;

           (Just tv1', Just tv2') | tv1' == tv2' 
              -> do { when (isWanted ev) $
                      setEvBind (ctev_evar ev) (mkEvCast (EvCoercion (mkTcReflCo xi1)) co)
                    ; return Stop } ;

           (Just tv1', _) ->

         -- LHS rewrote to a type variable, RHS to something else
         case occurCheckExpand tv1' xi2 of
           Nothing ->  -- Occurs check error
                       do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
                          ; case mb of
                              Nothing     -> return Stop
                              Just new_ev -> canEqFailure loc new_ev xi1 xi2 }

           Just xi2' -> -- No occurs check, so we can continue; but make sure
                        -- that the new goal has enough type synonyms expanded by 
                        -- by the occurCheckExpand
                        do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2') co
                           ; case mb of
                               Nothing     -> return Stop
                               Just new_ev -> continueWith $
                                              CTyEqCan { cc_ev = new_ev, cc_loc = loc
                                                       , cc_tyvar  = tv1', cc_rhs = xi2' } }
    } }
1202
1203
1204
1205
1206
1207

mkHdEqPred :: Type -> TcCoercion -> TcCoercion -> TcCoercion
-- Make a higher-dimensional equality
--    co1 :: s1~t1,  co2 :: s2~t2
-- Then (mkHdEqPred t2 co1 co2) :: (s1~s2) ~ (t1~t2)
mkHdEqPred t2 co1 co2 = mkTcTyConAppCo eqTyCon [mkTcReflCo (defaultKind (typeKind t2)), co1, co2]
1208
   -- Why defaultKind? Same reason as the comment on TcType/mkTcEqPred. I truly hate this (DV)
1209
1210
\end{code}

1211
1212
1213
1214
1215
1216
Note [Occurs check expansion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@occurCheckExpand tv xi@ expands synonyms in xi just enough to get rid
of occurrences of tv outside type function arguments, if that is
possible; otherwise, it returns Nothing.

1217
1218
1219
For example, suppose we have
  type F a b = [a]
Then
1220
  occurCheckExpand b (F Int b) = Just [Int]
1221
but
1222
  occurCheckExpand a (F a Int) = Nothing
1223
1224