TcCanonical.lhs 55.1 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 { (xis, cos) <- flattenMany d FMFullFlatten (ctEvFlavour ev) tys
251
       ; let co = mkTcTyConAppCo (classTyCon cls) cos 
252
             xi = mkClassPred cls xis
253
       ; mb <- rewriteCtFlavor ev xi co
dimitris's avatar
dimitris committed
254
       ; case mb of
255 256 257 258
           Nothing -> return Stop
           Just new_ev -> continueWith $ 
                          CDictCan { cc_ev = new_ev, cc_loc = d
                                   , cc_tyargs = xis, cc_class = cls } }
dimitris's avatar
dimitris committed
259

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

288 289 290 291 292 293 294 295 296
       (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. 
297

298 299 300 301 302 303 304 305 306 307 308 309
       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. 
310

311
       See also [New Wanted Superclass Work] in TcInteract. 
312

313 314 315

For Deriveds: 
       We do nothing.
316 317 318

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

  | isEmptyVarSet (tyVarsOfTypes xis)
354
  = return () -- Wanteds with no variables yield no deriveds.
355
              -- See Note [Improvement from Ground Wanteds]
356

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

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


Simon Peyton Jones's avatar
Simon Peyton Jones committed
376 377 378 379 380 381
%************************************************************************
%*                                                                      *
%*                      Irreducibles canonicalization
%*                                                                      *
%************************************************************************

382

383
\begin{code}
384
canIrred :: CtLoc -> CtEvidence -> TcS StopOrContinue
385
-- Precondition: ty not a tuple and no other evidence form
386 387 388
canIrred d ev
  = do { let ty = ctEvPred ev
       ; traceTcS "can_pred" (text "IrredPred = " <+> ppr ty) 
389
       ; (xi,co) <- flatten d FMFullFlatten (ctEvFlavour ev) ty -- co :: xi ~ ty
390
       ; let no_flattening = xi `eqType` ty 
391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406
             -- 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
407
       ; (xi,co) <- flatten d FMFullFlatten (ctEvFlavour ev) ty -- co :: xi ~ ty
408
       ; mb <- rewriteCtFlavor ev xi co 
dimitris's avatar
dimitris committed
409
       ; case mb of
410 411 412
             Just new_ev -> emitInsoluble (CHoleCan { cc_ev = new_ev, cc_loc = d})
             Nothing     -> return ()   -- Found a cached copy; won't happen
       ; return Stop } 
413
\end{code}
414

415 416 417 418 419 420 421 422 423 424
%************************************************************************
%*                                                                      *
%*        Flattening (eliminating all function symbols)                 *
%*                                                                      *
%************************************************************************

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

427 428 429 430 431 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
      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}

463
data FlattenMode = FMSubstOnly | FMFullFlatten
464

465
-- Flatten a bunch of types all at once.
466
flattenMany :: CtLoc -> FlattenMode
467
            -> CtFlavour -> [Type] -> TcS ([Xi], [TcCoercion])
468
-- Coercions :: Xi ~ Type 
469
-- Returns True iff (no flattening happened)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
470 471 472
-- 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
473
flattenMany d f ctxt tys 
474 475
  = -- pprTrace "flattenMany" empty $
    go tys 
476
  where go []       = return ([],[])
477
        go (ty:tys) = do { (xi,co)    <- flatten d f ctxt ty
478 479
                         ; (xis,cos)  <- go tys
                         ; return (xi:xis,co:cos) }
480 481 482 483

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

493
flatten _ _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
494

495 496
flatten loc f ctxt (TyVarTy tv)
  = flattenTyVar loc f ctxt tv
497

498 499 500
flatten loc f ctxt (AppTy ty1 ty2)
  = do { (xi1,co1) <- flatten loc f ctxt ty1
       ; (xi2,co2) <- flatten loc f ctxt ty2
501
       ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
502

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

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

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

568 569 570
                         | otherwise -- Wanted or Derived: make new unification variable
                         -> do { traceTcS "flatten/flat-cache miss" $ empty 
                               ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
571 572 573 574 575 576 577 578 579 580
                               ; ctev <- newWantedEvVarNC (mkTcEqPred fam_ty rhs_xi_var)
                                   -- NC (no-cache) version because we've already
                                   -- looked in the solved goals an inerts (lookupFlatEqn)
                               ; let ct = CFunEqCan { cc_ev = ctev
                                                    , cc_fun = tc
                                                    , cc_tyargs = xi_args
                                                    , cc_rhs    = rhs_xi_var 
                                                    , cc_loc    = loc }
                               ; updWorkListTcS $ extendWorkListFunEq ct
                               ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
581
                    }
dimitris's avatar
dimitris committed
582 583 584 585 586 587 588
                  -- 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
                  ) 
         }
589

590
flatten loc _f ctxt ty@(ForAllTy {})
591 592 593
-- 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
594
       ; (rho', co) <- flatten loc FMSubstOnly ctxt rho   
595 596
                         -- Substitute only under a forall
                         -- See Note [Flattening under a forall]
597
       ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
598 599
\end{code}

600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616
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
617
\begin{code}
618 619 620
flattenTyVar, flattenFinalTyVar
        :: CtLoc -> FlattenMode 
        -> CtFlavour -> TcTyVar -> TcS (Xi, TcCoercion)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
621
-- "Flattening" a type variable means to apply the substitution to it
622 623 624
-- 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.
625
flattenTyVar loc f ctxt tv
626 627 628
  | 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
629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654
  = 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]

655
           Nothing -> flattenFinalTyVar loc f ctxt tv
656
    } } } } } } 
657
  where
658 659 660
    tv_eq_subst subst tv
       | Just ct <- lookupVarEnv subst tv
       , let ctev = cc_ev ct
661
       , ctEvFlavour ctev `canRewrite` ctxt
662 663 664 665
       = 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
666 667 668 669 670 671 672

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
673 674 675 676 677 678 679 680 681
\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
682
 [G] g1 : ta8 ~ ta4
Simon Peyton Jones's avatar
Simon Peyton Jones committed
683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699
 [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.
700

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
703 704 705 706 707 708 709 710

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

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

719 720
emitWorkNC :: CtLoc -> [CtEvidence] -> TcS ()
emitWorkNC loc evs 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
721 722 723
  | null evs  = return ()
  | otherwise = updWorkListTcS (extendWorkListCts (map mk_nc evs))
  where
724
    mk_nc ev = CNonCanonical { cc_ev = ev, cc_loc = loc }
dimitris's avatar
dimitris committed
725

Simon Peyton Jones's avatar
Simon Peyton Jones committed
726
-------------------------
727
canEqNC, canEq :: CtLoc -> CtEvidence -> Type -> Type -> TcS StopOrContinue
Simon Peyton Jones's avatar
Simon Peyton Jones committed
728

729 730
canEqNC loc ev ty1 ty2
  = canEq loc ev ty1 ty2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
731 732
    `andWhenContinue` emitKindConstraint

733
canEq _loc ev ty1 ty2
734
  | eqType ty1 ty2	-- Dealing with equality here avoids
735
    	     	 	-- later spurious occurs checks for a~a
736 737
  = if isWanted ev then
      setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo ty1)) >> return Stop
dimitris's avatar
dimitris committed
738 739
    else
      return Stop
740

741
-- If one side is a variable, orient and flatten,
742
-- WITHOUT expanding type synonyms, so that we tend to 
743
-- substitute a ~ Age rather than a ~ Int when @type Age = Int@
744 745 746 747
canEq loc ev ty1@(TyVarTy {}) ty2 
  = canEqLeaf loc ev ty1 ty2
canEq loc ev ty1 ty2@(TyVarTy {})
  = canEqLeaf loc ev ty1 ty2
748

749
-- See Note [Naked given applications]
750 751 752
canEq loc ev ty1 ty2
  | Just ty1' <- tcView ty1 = canEq loc ev ty1' ty2
  | Just ty2' <- tcView ty2 = canEq loc ev ty1  ty2'
753

754
canEq loc ev ty1@(TyConApp fn tys) ty2
755
  | isSynFamilyTyCon fn, length tys == tyConArity fn
756 757
  = canEqLeaf loc ev ty1 ty2
canEq loc ev ty1 ty2@(TyConApp fn tys)
758
  | isSynFamilyTyCon fn, length tys == tyConArity fn
759
  = canEqLeaf loc ev ty1 ty2
760

761
canEq loc ev ty1 ty2
762 763 764
  | 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
765
  = canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2 
766

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

-- 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
796
    last_chance ev ty1 ty2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
797 798 799
      | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
      , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
      , isDecomposableTyCon tc1 && isDecomposableTyCon tc2
800
      = canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
801 802 803 804 805 806 807 808 809 810 811
    
      | 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
812
      = do { emitInsoluble (CNonCanonical { cc_ev = ev, cc_loc = loc })
Simon Peyton Jones's avatar
Simon Peyton Jones committed
813
           ; return Stop }
814

Simon Peyton Jones's avatar
Simon Peyton Jones committed
815
------------------------
Simon Peyton Jones's avatar
Simon Peyton Jones committed
816 817 818 819 820 821 822 823 824 825 826 827 828
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
829
       ; canEvVarsCreated loc ctevs }
830

831 832 833 834 835 836 837 838 839 840 841
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)
842
       ; return Stop }
dimitris's avatar
dimitris committed
843

Simon Peyton Jones's avatar
Simon Peyton Jones committed
844 845
------------------------
emitKindConstraint :: Ct -> TcS StopOrContinue
Simon Peyton Jones's avatar
Simon Peyton Jones committed
846
emitKindConstraint ct   -- By now ct is canonical
Simon Peyton Jones's avatar
Simon Peyton Jones committed
847
  = case ct of 
848 849
      CTyEqCan { cc_loc = loc
               , cc_ev = ev, cc_tyvar = tv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
850
               , cc_rhs = ty }
851
          -> emit_kind_constraint loc ev (mkTyVarTy tv) ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
852

853 854
      CFunEqCan { cc_loc = loc
                , cc_ev = ev
Simon Peyton Jones's avatar
Simon Peyton Jones committed
855 856
                , cc_fun = fn, cc_tyargs = xis1
                , cc_rhs = xi2 }
857
          -> emit_kind_constraint loc ev (mkTyConApp fn xis1) xi2
858

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

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

882 883 884 885 886 887 888 889 890 891 892
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.

893 894 895 896 897 898 899
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.   


900 901 902 903 904 905 906 907 908 909 910 911 912 913 914
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.
   

915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933
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


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


classify :: TcType -> TypeClassifier
1048

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

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

1074 1075
reOrient _ev (VarCls {})   (FunCls {})      = True 
reOrient _ev (VarCls {})   (OtherCls {})   = False
1076
reOrient _ev (VarCls tv1)  (VarCls tv2)  
1077 1078 1079
  | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True 
  | otherwise                                = False 
  -- Just for efficiency, see CTyEqCan invariants 
1080 1081

------------------
1082

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