compiler/typecheck/TcCanonical.lhs

   1 \begin{code}
   2 module TcCanonical(
   3     mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
   4     canOccursCheck, canEqToWorkList,
   5     rewriteWithFunDeps
   6  ) where
   7
   8 #include "HsVersions.h"
   9
  10 import BasicTypes
  11 import Id       ( evVarPred )
  12 import TcErrors
  13 import TcRnTypes
  14 import FunDeps
  15 import qualified TcMType as TcM
  16 import TcType
  17 import Type
  18 import Coercion
  19 import Class
  20 import TyCon
  21 import TypeRep
  22 import Name
  23 import Var
  24 import VarEnv           ( TidyEnv )
  25 import Outputable
  26 import Control.Monad    ( unless, when, zipWithM, zipWithM_ )
  27 import MonadUtils
  28 import Control.Applicative ( (<|>) )
  29
  30 import VarSet
  31 import Bag
  32
  33 import HsBinds
  34 import TcSMonad
  35 import FastString
  36 \end{code}
  37
  38 Note [Canonicalisation]
  39 ~~~~~~~~~~~~~~~~~~~~~~~
  40 * Converts (Constraint f) _which_does_not_contain_proper_implications_ to CanonicalCts
  41 * Unary: treats individual constraints one at a time
  42 * Does not do any zonking
  43 * Lives in TcS monad so that it can create new skolem variables
  44
  45
  46 %************************************************************************
  47 %*                                                                      *
  48 %*        Flattening (eliminating all function symbols)                 *
  49 %*                                                                      *
  50 %************************************************************************
  51
  52 Note [Flattening]
  53 ~~~~~~~~~~~~~~~~~~~~
  54   flatten ty  ==>   (xi, cc)
  55     where
  56       xi has no type functions
  57       cc = Auxiliary given (equality) constraints constraining
  58            the fresh type variables in xi.  Evidence for these
  59            is always the identity coercion, because internally the
  60            fresh flattening skolem variables are actually identified
  61            with the types they have been generated to stand in for.
  62
  63 Note that it is flatten's job to flatten *every type function it sees*.
  64 flatten is only called on *arguments* to type functions, by canEqGiven.
  65
  66 Recall that in comments we use alpha[flat = ty] to represent a
  67 flattening skolem variable alpha which has been generated to stand in
  68 for ty.
  69
  70 ----- Example of flattening a constraint: ------
  71   flatten (List (F (G Int)))  ==>  (xi, cc)
  72     where
  73       xi  = List alpha
  74       cc  = { G Int ~ beta[flat = G Int],
  75               F beta ~ alpha[flat = F beta] }
  76 Here
  77   * alpha and beta are 'flattening skolem variables'.
  78   * All the constraints in cc are 'given', and all their coercion terms
  79     are the identity.
  80
  81 NB: Flattening Skolems only occur in canonical constraints, which
  82 are never zonked, so we don't need to worry about zonking doing
  83 accidental unflattening.
  84
  85 Note that we prefer to leave type synonyms unexpanded when possible,
  86 so when the flattener encounters one, it first asks whether its
  87 transitive expansion contains any type function applications.  If so,
  88 it expands the synonym and proceeds; if not, it simply returns the
  89 unexpanded synonym.
  90
  91 TODO: caching the information about whether transitive synonym
  92 expansions contain any type function applications would speed things
  93 up a bit; right now we waste a lot of energy traversing the same types
  94 multiple times.
  95
  96 \begin{code}
  97 -- Flatten a bunch of types all at once.
  98 flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts)
  99 -- Coercions :: Xi ~ Type
 100 flattenMany ctxt tys
 101   = do { (xis, cos, cts_s) <- mapAndUnzip3M (flatten ctxt) tys
 102        ; return (xis, cos, andCCans cts_s) }
 103
 104 -- Flatten a type to get rid of type function applications, returning
 105 -- the new type-function-free type, and a collection of new equality
 106 -- constraints.  See Note [Flattening] for more detail.
 107 flatten :: CtFlavor -> TcType -> TcS (Xi, Coercion, CanonicalCts)
 108 -- Postcondition: Coercion :: Xi ~ TcType
 109 flatten ctxt ty
 110   | Just ty' <- tcView ty
 111   = do { (xi, co, ccs) <- flatten ctxt ty'
 112         -- Preserve type synonyms if possible
 113         -- We can tell if ty' is function-free by
 114         -- whether there are any floated constraints
 115        ; if isEmptyCCan ccs then
 116              return (ty, mkReflCo ty, emptyCCan)
 117          else
 118              return (xi, co, ccs) }
 119
 120 flatten _ v@(TyVarTy _)
 121   = return (v, mkReflCo v, emptyCCan)
 122
 123 flatten ctxt (AppTy ty1 ty2)
 124   = do { (xi1,co1,c1) <- flatten ctxt ty1
 125        ; (xi2,co2,c2) <- flatten ctxt ty2
 126        ; return (mkAppTy xi1 xi2, mkAppCo co1 co2, c1 `andCCan` c2) }
 127
 128 flatten ctxt (FunTy ty1 ty2)
 129   = do { (xi1,co1,c1) <- flatten ctxt ty1
 130        ; (xi2,co2,c2) <- flatten ctxt ty2
 131        ; return (mkFunTy xi1 xi2, mkFunCo co1 co2, c1 `andCCan` c2) }
 132
 133 flatten fl (TyConApp tc tys)
 134   -- For a normal type constructor or data family application, we just
 135   -- recursively flatten the arguments.
 136   | not (isSynFamilyTyCon tc)
 137     = do { (xis,cos,ccs) <- flattenMany fl tys
 138          ; return (mkTyConApp tc xis, mkTyConAppCo tc cos, ccs) }
 139
 140   -- Otherwise, it's a type function application, and we have to
 141   -- flatten it away as well, and generate a new given equality constraint
 142   -- between the application and a newly generated flattening skolem variable.
 143   | otherwise
 144   = ASSERT( tyConArity tc <= length tys )       -- Type functions are saturated
 145       do { (xis, cos, ccs) <- flattenMany fl tys
 146          ; let (xi_args, xi_rest)  = splitAt (tyConArity tc) xis
 147                (cos_args, cos_rest) = splitAt (tyConArity tc) cos
 148                  -- The type function might be *over* saturated
 149                  -- in which case the remaining arguments should
 150                  -- be dealt with by AppTys
 151                fam_ty = mkTyConApp tc xi_args
 152                fam_co = mkReflCo fam_ty -- identity
 153
 154          ; (ret_co, rhs_var, ct) <-
 155              if isGiven fl then
 156                do { rhs_var <- newFlattenSkolemTy fam_ty
 157                   ; cv <- newGivenCoVar fam_ty rhs_var fam_co
 158                   ; let ct = CFunEqCan { cc_id     = cv
 159                                        , cc_flavor = fl -- Given
 160                                        , cc_fun    = tc
 161                                        , cc_tyargs = xi_args
 162                                        , cc_rhs    = rhs_var }
 163                   ; return $ (mkCoVarCo cv, rhs_var, ct) }
 164              else -- Derived or Wanted: make a new *unification* flatten variable
 165                do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
 166                   ; cv <- newCoVar fam_ty rhs_var
 167                   ; let ct = CFunEqCan { cc_id = cv
 168                                        , cc_flavor = mkWantedFlavor fl
 169                                            -- Always Wanted, not Derived
 170                                        , cc_fun = tc
 171                                        , cc_tyargs = xi_args
 172                                        , cc_rhs    = rhs_var }
 173                   ; return $ (mkCoVarCo cv, rhs_var, ct) }
 174
 175          ; return ( foldl AppTy rhs_var xi_rest
 176                   , foldl mkAppCo
 177                           (mkSymCo ret_co
 178                             `mkTransCo` mkTyConAppCo tc cos_args)
 179                           cos_rest
 180                   , ccs `extendCCans` ct) }
 181
 182
 183 flatten ctxt (PredTy pred)
 184   = do { (pred', co, ccs) <- flattenPred ctxt pred
 185        ; return (PredTy pred', co, ccs) }
 186
 187 flatten ctxt ty@(ForAllTy {})
 188 -- We allow for-alls when, but only when, no type function
 189 -- applications inside the forall involve the bound type variables
 190 -- TODO: What if it is a (t1 ~ t2) => t3
 191 --       Must revisit when the New Coercion API is here!
 192   = do { let (tvs, rho) = splitForAllTys ty
 193        ; (rho', co, ccs) <- flatten ctxt rho
 194        ; let bad_eqs  = filterBag is_bad ccs
 195              is_bad c = tyVarsOfCanonical c `intersectsVarSet` tv_set
 196              tv_set   = mkVarSet tvs
 197        ; unless (isEmptyBag bad_eqs)
 198                 (flattenForAllErrorTcS ctxt ty bad_eqs)
 199        ; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs, ccs)  }
 200
 201 ---------------
 202 flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, Coercion, CanonicalCts)
 203 flattenPred ctxt (ClassP cls tys)
 204   = do { (tys', cos, ccs) <- flattenMany ctxt tys
 205        ; return (ClassP cls tys', mkPredCo $ ClassP cls cos, ccs) }
 206 flattenPred ctxt (IParam nm ty)
 207   = do { (ty', co, ccs) <- flatten ctxt ty
 208        ; return (IParam nm ty', mkPredCo $ IParam nm co, ccs) }
 209 flattenPred ctxt (EqPred ty1 ty2)
 210   = do { (ty1', co1, ccs1) <- flatten ctxt ty1
 211        ; (ty2', co2, ccs2) <- flatten ctxt ty2
 212        ; return (EqPred ty1' ty2', mkPredCo $ EqPred co1 co2, ccs1 `andCCan` ccs2) }
 213 \end{code}
 214
 215 %************************************************************************
 216 %*                                                                      *
 217 %*                Canonicalising given constraints                      *
 218 %*                                                                      *
 219 %************************************************************************
 220
 221 \begin{code}
 222 canWanteds :: [WantedEvVar] -> TcS WorkList
 223 canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
 224
 225 canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
 226 canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens
 227                           ; return (unionWorkLists ccs) }
 228
 229 mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
 230 mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
 231
 232 mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
 233 mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
 234
 235 mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
 236 mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
 237   where         -- Preserves order (shouldn't be important, but curently
 238                 --                  is important for the vectoriser)
 239     canon_one fev wl = do { wl' <- mkCanonicalFEV fev
 240                           ; return (unionWorkList wl' wl) }
 241
 242 mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
 243 mkCanonical fl ev = case evVarPred ev of
 244                         ClassP clas tys -> canClassToWorkList fl ev clas tys
 245                         IParam ip ty    -> canIPToWorkList    fl ev ip ty
 246                         EqPred ty1 ty2  -> canEqToWorkList    fl ev ty1 ty2
 247
 248
 249 canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
 250 canClassToWorkList fl v cn tys
 251   = do { (xis,cos,ccs) <- flattenMany fl tys  -- cos :: xis ~ tys
 252        ; let no_flattening_happened = isEmptyCCan ccs
 253              dict_co = mkTyConAppCo (classTyCon cn) cos
 254        ; v_new <- if no_flattening_happened then return v
 255                   else if isGiven fl        then return v
 256                          -- The cos are all identities if fl=Given,
 257                          -- hence nothing to do
 258                   else do { v' <- newDictVar cn xis  -- D xis
 259                           ; when (isWanted fl) $ setDictBind v  (EvCast v' dict_co)
 260                           ; when (isGiven fl)  $ setDictBind v' (EvCast v (mkSymCo dict_co))
 261                                  -- NB: No more setting evidence for derived now
 262                           ; return v' }
 263
 264        -- Add the superclasses of this one here, See Note [Adding superclasses].
 265        -- But only if we are not simplifying the LHS of a rule.
 266        ; sctx <- getTcSContext
 267        ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
 268                    else newSCWorkFromFlavored v_new fl cn xis
 269
 270        ; return (sc_cts `unionWorkList`
 271                  workListFromEqs ccs `unionWorkList`
 272                  workListFromNonEq CDictCan { cc_id     = v_new
 273                                            , cc_flavor = fl
 274                                            , cc_class  = cn
 275                                            , cc_tyargs = xis }) }
 276 \end{code}
 277
 278 Note [Adding superclasses]
 279 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 280 Since dictionaries are canonicalized only once in their lifetime, the
 281 place to add their superclasses is canonicalisation (The alternative
 282 would be to do it during constraint solving, but we'd have to be
 283 extremely careful to not repeatedly introduced the same superclass in
 284 our worklist). Here is what we do:
 285
 286 For Givens:
 287        We add all their superclasses as Givens.
 288
 289 For Wanteds:
 290        Generally speaking we want to be able to add superclasses of
 291        wanteds for two reasons:
 292
 293        (1) Oportunities for improvement. Example:
 294                   class (a ~ b) => C a b
 295            Wanted constraint is: C alpha beta
 296            We'd like to simply have C alpha alpha. Similar
 297            situations arise in relation to functional dependencies.
 298
 299        (2) To have minimal constraints to quantify over:
 300            For instance, if our wanted constraint is (Eq a, Ord a)
 301            we'd only like to quantify over Ord a.
 302
 303        To deal with (1) above we only add the superclasses of wanteds
 304        which may lead to improvement, that is: equality superclasses or
 305        superclasses with functional dependencies.
 306
 307        We deal with (2) completely independently in TcSimplify. See
 308        Note [Minimize by SuperClasses] in TcSimplify.
 309
 310
 311        Moreover, in all cases the extra improvement constraints are
 312        Derived. Derived constraints have an identity (for now), but
 313        we don't do anything with their evidence. For instance they
 314        are never used to rewrite other constraints.
 315
 316        See also [New Wanted Superclass Work] in TcInteract.
 317
 318
 319 For Deriveds:
 320        We do nothing.
 321
 322 Here's an example that demonstrates why we chose to NOT add
 323 superclasses during simplification: [Comes from ticket #4497]
 324
 325    class Num (RealOf t) => Normed t
 326    type family RealOf x
 327
 328 Assume the generated wanted constraint is:
 329    RealOf e ~ e, Normed e
 330 If we were to be adding the superclasses during simplification we'd get:
 331    Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
 332 ==>
 333    e ~ uf, Num uf, Normed e, RealOf e ~ e
 334 ==> [Spontaneous solve]
 335    Num uf, Normed uf, RealOf uf ~ uf
 336
 337 While looks exactly like our original constraint. If we add the superclass again we'd loop.
 338 By adding superclasses definitely only once, during canonicalisation, this situation can't
 339 happen.
 340
 341 \begin{code}
 342
 343 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
 344 -- Returns superclasses, see Note [Adding superclasses]
 345 newSCWorkFromFlavored ev orig_flavor cls xis
 346   | isDerived orig_flavor
 347   = return emptyWorkList  -- Deriveds don't yield more superclasses because we will
 348                           -- add them transitively in the case of wanteds.
 349
 350   | isGiven orig_flavor
 351   = do { let sc_theta = immSuperClasses cls xis
 352              flavor   = orig_flavor
 353        ; sc_vars <- mapM newEvVar sc_theta
 354        ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
 355        ; mkCanonicals flavor sc_vars }
 356
 357   | isEmptyVarSet (tyVarsOfTypes xis)
 358   = return emptyWorkList -- Wanteds with no variables yield no deriveds.
 359                          -- See Note [Improvement from Ground Wanteds]
 360
 361   | otherwise -- Wanted case, just add those SC that can lead to improvement.
 362   = do { let sc_rec_theta = transSuperClasses cls xis
 363              impr_theta   = filter is_improvement_pty sc_rec_theta
 364              Wanted wloc  = orig_flavor
 365        ; der_ids <- mapM newDerivedId impr_theta
 366        ; mkCanonicals (Derived wloc) der_ids }
 367
 368
 369 is_improvement_pty :: PredType -> Bool
 370 -- Either it's an equality, or has some functional dependency
 371 is_improvement_pty (EqPred {})      = True
 372 is_improvement_pty (ClassP cls _ty) = not $ null fundeps
 373  where (_,fundeps,_,_,_,_) = classExtraBigSig cls
 374 is_improvement_pty _ = False
 375
 376
 377
 378
 379 canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
 380 -- See Note [Canonical implicit parameter constraints] to see why we don't
 381 -- immediately canonicalize (flatten) IP constraints.
 382 canIPToWorkList fl v nm ty
 383   = return $ workListFromNonEq (CIPCan { cc_id = v
 384                                       , cc_flavor = fl
 385                                       , cc_ip_nm = nm
 386                                       , cc_ip_ty = ty })
 387
 388 -----------------
 389 canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
 390 canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2
 391                          ; return $ workListFromEqs cts }
 392
 393 canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
 394 canEq fl cv ty1 ty2
 395   | eqType ty1 ty2      -- Dealing with equality here avoids
 396                         -- later spurious occurs checks for a~a
 397   = do { when (isWanted fl) (setCoBind cv (mkReflCo ty1))
 398        ; return emptyCCan }
 399
 400 -- If one side is a variable, orient and flatten,
 401 -- WITHOUT expanding type synonyms, so that we tend to
 402 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@
 403 canEq fl cv ty1@(TyVarTy {}) ty2
 404   = do { untch <- getUntouchables
 405        ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
 406 canEq fl cv ty1 ty2@(TyVarTy {})
 407   = do { untch <- getUntouchables
 408        ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
 409       -- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
 410
 411 -- Split up an equality between function types into two equalities.
 412 canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
 413   = do { (argv, resv) <-
 414              if isWanted fl then
 415                  do { argv <- newCoVar s1 s2
 416                     ; resv <- newCoVar t1 t2
 417                     ; setCoBind cv $
 418                       mkFunCo (mkCoVarCo argv) (mkCoVarCo resv)
 419                     ; return (argv,resv) }
 420
 421              else if isGiven fl then
 422                       let [arg,res] = decomposeCo 2 (mkCoVarCo cv)
 423                       in do { argv <- newGivenCoVar s1 s2 arg
 424                             ; resv <- newGivenCoVar t1 t2 res
 425                             ; return (argv,resv) }
 426
 427              else -- Derived
 428                  do { argv <- newDerivedId (EqPred s1 s2)
 429                     ; resv <- newDerivedId (EqPred t1 t2)
 430                     ; return (argv,resv) }
 431
 432        ; cc1 <- canEq fl argv s1 s2 -- inherit original kinds and locations
 433        ; cc2 <- canEq fl resv t1 t2
 434        ; return (cc1 `andCCan` cc2) }
 435
 436 canEq fl cv (TyConApp fn tys) ty2
 437   | isSynFamilyTyCon fn, length tys == tyConArity fn
 438   = do { untch <- getUntouchables
 439        ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
 440 canEq fl cv ty1 (TyConApp fn tys)
 441   | isSynFamilyTyCon fn, length tys == tyConArity fn
 442   = do { untch <- getUntouchables
 443        ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
 444
 445 canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 446   | isDecomposableTyCon tc1 && isDecomposableTyCon tc2
 447   , tc1 == tc2
 448   , length tys1 == length tys2
 449   = -- Generate equalities for each of the corresponding arguments
 450     do { argsv
 451              <- if isWanted fl then
 452                     do { argsv <- zipWithM newCoVar tys1 tys2
 453                        ; setCoBind cv $
 454                          mkTyConAppCo tc1 (map mkCoVarCo argsv)
 455                        ; return argsv }
 456
 457                 else if isGiven fl then
 458                     let cos = decomposeCo (length tys1) (mkCoVarCo cv)
 459                     in zipWith3M newGivenCoVar tys1 tys2 cos
 460
 461                 else -- Derived
 462                     zipWithM (\t1 t2 -> newDerivedId (EqPred t1 t2)) tys1 tys2
 463
 464        ; andCCans <$> zipWith3M (canEq fl) argsv tys1 tys2 }
 465
 466 -- See Note [Equality between type applications]
 467 --     Note [Care with type applications] in TcUnify
 468 canEq fl cv ty1 ty2
 469   | Just (s1,t1) <- tcSplitAppTy_maybe ty1
 470   , Just (s2,t2) <- tcSplitAppTy_maybe ty2
 471     = if isWanted fl
 472       then do { cv1 <- newCoVar s1 s2
 473               ; cv2 <- newCoVar t1 t2
 474               ; setCoBind cv $
 475                 mkAppCo (mkCoVarCo cv1) (mkCoVarCo cv2)
 476               ; cc1 <- canEq fl cv1 s1 s2
 477               ; cc2 <- canEq fl cv2 t1 t2
 478               ; return (cc1 `andCCan` cc2) }
 479
 480       else if isDerived fl
 481       then do { cv1 <- newDerivedId (EqPred s1 s2)
 482               ; cv2 <- newDerivedId (EqPred t1 t2)
 483               ; cc1 <- canEq fl cv1 s1 s2
 484               ; cc2 <- canEq fl cv2 t1 t2
 485               ; return (cc1 `andCCan` cc2) }
 486
 487       else return emptyCCan    -- We cannot decompose given applications
 488                                -- because we no longer have 'left' and 'right'
 489
 490 canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {})
 491  | tcIsForAllTy s1, tcIsForAllTy s2,
 492    Wanted {} <- fl
 493  = canEqFailure fl cv
 494  | otherwise
 495  = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
 496       ; return emptyCCan }
 497
 498 -- Finally expand any type synonym applications.
 499 canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2
 500 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2'
 501 canEq fl cv _ _                               = canEqFailure fl cv
 502
 503 canEqFailure :: CtFlavor -> EvVar -> TcS CanonicalCts
 504 canEqFailure fl cv = return (singleCCan (mkFrozenError fl cv))
 505 \end{code}
 506
 507 Note [Equality between type applications]
 508 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 509 If we see an equality of the form s1 t1 ~ s2 t2 we can always split
 510 it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
 511 functions (type functions use the TyConApp constructor, which never
 512 shows up as the LHS of an AppTy).  Other than type functions, types
 513 in Haskell are always
 514
 515   (1) generative: a b ~ c d implies a ~ c, since different type
 516       constructors always generate distinct types
 517
 518   (2) injective: a b ~ a d implies b ~ d; we never generate the
 519       same type from different type arguments.
 520
 521
 522 Note [Canonical ordering for equality constraints]
 523 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 524 Implemented as (<+=) below:
 525
 526   - Type function applications always come before anything else.
 527   - Variables always come before non-variables (other than type
 528       function applications).
 529
 530 Note that we don't need to unfold type synonyms on the RHS to check
 531 the ordering; that is, in the rules above it's OK to consider only
 532 whether something is *syntactically* a type function application or
 533 not.  To illustrate why this is OK, suppose we have an equality of the
 534 form 'tv ~ S a b c', where S is a type synonym which expands to a
 535 top-level application of the type function F, something like
 536
 537   type S a b c = F d e
 538
 539 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
 540 expansion contains type function applications the flattener will do
 541 the expansion and then generate a skolem variable for the type
 542 function application, so we end up with something like this:
 543
 544   tv ~ x
 545   F d e ~ x
 546
 547 where x is the skolem variable.  This is one extra equation than
 548 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
 549 if we had noticed that S expanded to a top-level type function
 550 application and flipped it around in the first place) but this way
 551 keeps the code simpler.
 552
 553 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
 554 ordering of tv ~ tv constraints.  There are several reasons why we
 555 might:
 556
 557   (1) In order to be able to extract a substitution that doesn't
 558       mention untouchable variables after we are done solving, we might
 559       prefer to put touchable variables on the left. However, in and
 560       of itself this isn't necessary; we can always re-orient equality
 561       constraints at the end if necessary when extracting a substitution.
 562
 563   (2) To ensure termination we might think it necessary to put
 564       variables in lexicographic order. However, this isn't actually
 565       necessary as outlined below.
 566
 567 While building up an inert set of canonical constraints, we maintain
 568 the invariant that the equality constraints in the inert set form an
 569 acyclic rewrite system when viewed as L-R rewrite rules.  Moreover,
 570 the given constraints form an idempotent substitution (i.e. none of
 571 the variables on the LHS occur in any of the RHS's, and type functions
 572 never show up in the RHS at all), the wanted constraints also form an
 573 idempotent substitution, and finally the LHS of a given constraint
 574 never shows up on the RHS of a wanted constraint.  There may, however,
 575 be a wanted LHS that shows up in a given RHS, since we do not rewrite
 576 given constraints with wanted constraints.
 577
 578 Suppose we have an inert constraint set
 579
 580
 581   tg_1 ~ xig_1         -- givens
 582   tg_2 ~ xig_2
 583   ...
 584   tw_1 ~ xiw_1         -- wanteds
 585   tw_2 ~ xiw_2
 586   ...
 587
 588 where each t_i can be either a type variable or a type function
 589 application. Now suppose we take a new canonical equality constraint,
 590 t' ~ xi' (note among other things this means t' does not occur in xi')
 591 and try to react it with the existing inert set.  We show by induction
 592 on the number of t_i which occur in t' ~ xi' that this process will
 593 terminate.
 594
 595 There are several ways t' ~ xi' could react with an existing constraint:
 596
 597 TODO: finish this proof.  The below was for the case where the entire
 598 inert set is an idempotent subustitution...
 599
 600 (b) We could have t' = t_j for some j.  Then we obtain the new
 601     equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j.  We
 602     now canonicalize the new equality, which may involve decomposing it
 603     into several canonical equalities, and recurse on these.  However,
 604     none of the new equalities will contain t_j, so they have fewer
 605     occurrences of the t_i than the original equation.
 606
 607 (a) We could have t_j occurring in xi' for some j, with t' /=
 608     t_j. Then we substitute xi_j for t_j in xi' and continue.  However,
 609     since none of the t_i occur in xi_j, we have decreased the
 610     number of t_i that occur in xi', since we eliminated t_j and did not
 611     introduce any new ones.
 612
 613 \begin{code}
 614 data TypeClassifier
 615   = FskCls TcTyVar      -- ^ Flatten skolem
 616   | VarCls TcTyVar      -- ^ Non-flatten-skolem variable
 617   | FunCls TyCon [Type] -- ^ Type function, exactly saturated
 618   | OtherCls TcType     -- ^ Neither of the above
 619
 620 unClassify :: TypeClassifier -> TcType
 621 unClassify (VarCls tv)      = TyVarTy tv
 622 unClassify (FskCls tv) = TyVarTy tv
 623 unClassify (FunCls fn tys)  = TyConApp fn tys
 624 unClassify (OtherCls ty)    = ty
 625
 626 classify :: TcType -> TypeClassifier
 627
 628 classify (TyVarTy tv)
 629   | isTcTyVar tv,
 630     FlatSkol {} <- tcTyVarDetails tv = FskCls tv
 631   | otherwise                        = VarCls tv
 632 classify (TyConApp tc tys) | isSynFamilyTyCon tc
 633                            , tyConArity tc == length tys
 634                            = FunCls tc tys
 635 classify ty                | Just ty' <- tcView ty
 636                            = case classify ty' of
 637                                OtherCls {} -> OtherCls ty
 638                                var_or_fn   -> var_or_fn
 639                            | otherwise
 640                            = OtherCls ty
 641
 642 -- See note [Canonical ordering for equality constraints].
 643 reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool
 644 -- (t1 `reOrient` t2) responds True
 645 --   iff we should flip to (t2~t1)
 646 -- We try to say False if possible, to minimise evidence generation
 647 --
 648 -- Postcondition: After re-orienting, first arg is not OTherCls
 649 reOrient _fl (OtherCls {}) (FunCls {})   = True
 650 reOrient _fl (OtherCls {}) (FskCls {})   = True
 651 reOrient _fl (OtherCls {}) (VarCls {})   = True
 652 reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient"  -- One must be Var/Fun
 653
 654 reOrient _fl (FunCls {})   (VarCls _tv)  = False
 655   -- But consider the following variation: isGiven fl && isMetaTyVar tv
 656
 657   -- See Note [No touchables as FunEq RHS] in TcSMonad
 658 reOrient _fl (FunCls {}) _                = False             -- Fun/Other on rhs
 659
 660 reOrient _fl (VarCls {}) (FunCls {})      = True
 661
 662 reOrient _fl (VarCls {}) (FskCls {})      = False
 663
 664 reOrient _fl (VarCls {})  (OtherCls {})   = False
 665 reOrient _fl (VarCls tv1)  (VarCls tv2)
 666   | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True
 667   | otherwise                                = False
 668   -- Just for efficiency, see CTyEqCan invariants
 669
 670 reOrient _fl (FskCls {}) (VarCls tv2)     = isMetaTyVar tv2
 671   -- Just for efficiency, see CTyEqCan invariants
 672
 673 reOrient _fl (FskCls {}) (FskCls {})     = False
 674 reOrient _fl (FskCls {}) (FunCls {})     = True
 675 reOrient _fl (FskCls {}) (OtherCls {})   = False
 676
 677 ------------------
 678 canEqLeaf :: TcsUntouchables
 679           -> CtFlavor -> CoVar
 680           -> TypeClassifier -> TypeClassifier -> TcS CanonicalCts
 681 -- Canonicalizing "leaf" equality constraints which cannot be
 682 -- decomposed further (ie one of the types is a variable or
 683 -- saturated type function application).
 684
 685   -- Preconditions:
 686   --    * one of the two arguments is not OtherCls
 687   --    * the two types are not equal (looking through synonyms)
 688 canEqLeaf _untch fl cv cls1 cls2
 689   | cls1 `re_orient` cls2
 690   = do { cv' <- if isWanted fl
 691                 then do { cv' <- newCoVar s2 s1
 692                         ; setCoBind cv $ mkSymCo (mkCoVarCo cv')
 693                         ; return cv' }
 694                 else if isGiven fl then
 695                          newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv))
 696                 else -- Derived
 697                     newDerivedId (EqPred s2 s1)
 698        ; canEqLeafOriented fl cv' cls2 s1 }
 699
 700   | otherwise
 701   = do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2))
 702        ; canEqLeafOriented fl cv cls1 s2 }
 703   where
 704     re_orient = reOrient fl
 705     s1 = unClassify cls1
 706     s2 = unClassify cls2
 707
 708 ------------------
 709 canEqLeafOriented :: CtFlavor -> CoVar
 710                   -> TypeClassifier -> TcType -> TcS CanonicalCts
 711 -- First argument is not OtherCls
 712 canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2         -- cv : F tys1
 713   | let k1 = kindAppResult (tyConKind fn) tys1,
 714     let k2 = typeKind s2,
 715     not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan
 716   = canEqFailure fl cv
 717     -- Eagerly fails, see Note [Kind errors] in TcInteract
 718
 719   | otherwise
 720   = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
 721     do { (xis1,cos1,ccs1) <- flattenMany fl tys1 -- Flatten type function arguments
 722                                                  -- cos1 :: xis1 ~ tys1
 723        ; (xi2, co2, ccs2) <- flatten fl s2       -- Flatten entire RHS
 724                                                  -- co2  :: xi2 ~ s2
 725        ; let ccs = ccs1 `andCCan` ccs2
 726              no_flattening_happened = isEmptyCCan ccs
 727        ; cv_new <- if no_flattening_happened then return cv
 728                    else if isGiven fl        then return cv
 729                    else if isWanted fl then
 730                          do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
 731                                  -- cv' : F xis ~ xi2
 732                             ; let -- fun_co :: F xis1 ~ F tys1
 733                                  fun_co = mkTyConAppCo fn cos1
 734                                  -- want_co :: F tys1 ~ s2
 735                                  want_co = mkSymCo fun_co
 736                                            `mkTransCo` mkCoVarCo cv'
 737                                            `mkTransCo` co2
 738                             ; setCoBind cv  want_co
 739                             ; return cv' }
 740                    else -- Derived
 741                        newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
 742
 743        ; let final_cc = CFunEqCan { cc_id     = cv_new
 744                                   , cc_flavor = fl
 745                                   , cc_fun    = fn
 746                                   , cc_tyargs = xis1
 747                                   , cc_rhs    = xi2 }
 748        ; return $ ccs `extendCCans` final_cc }
 749
 750 -- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft
 751 canEqLeafOriented fl cv (FskCls tv) s2
 752   = canEqLeafTyVarLeft fl cv tv s2
 753 canEqLeafOriented fl cv (VarCls tv) s2
 754   = canEqLeafTyVarLeft fl cv tv s2
 755 canEqLeafOriented _ cv (OtherCls ty1) ty2
 756   = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
 757
 758 canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts
 759 -- Establish invariants of CTyEqCans
 760 canEqLeafTyVarLeft fl cv tv s2       -- cv : tv ~ s2
 761   | not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan
 762   = canEqFailure fl cv
 763        -- Eagerly fails, see Note [Kind errors] in TcInteract
 764   | otherwise
 765   = do { (xi2, co, ccs2) <- flatten fl s2  -- Flatten RHS   co : xi2 ~ s2
 766        ; mxi2' <- canOccursCheck fl tv xi2 -- Do an occurs check, and return a possibly
 767                                            -- unfolded version of the RHS, if we had to
 768                                            -- unfold any type synonyms to get rid of tv.
 769        ; case mxi2' of {
 770            Nothing   -> canEqFailure fl cv ;
 771            Just xi2' ->
 772     do { let no_flattening_happened = isEmptyCCan ccs2
 773        ; cv_new <- if no_flattening_happened then return cv
 774                    else if isGiven fl        then return cv
 775                    else if isWanted fl then
 776                          do { cv' <- newCoVar (mkTyVarTy tv) xi2'  -- cv' : tv ~ xi2
 777                             ; setCoBind cv  (mkCoVarCo cv' `mkTransCo` co)
 778                             ; return cv' }
 779                    else -- Derived
 780                        newDerivedId (EqPred (mkTyVarTy tv) xi2')
 781
 782        ; return $ ccs2 `extendCCans` CTyEqCan { cc_id     = cv_new
 783                                               , cc_flavor = fl
 784                                               , cc_tyvar  = tv
 785                                               , cc_rhs    = xi2' } } } }
 786   where
 787     k1 = tyVarKind tv
 788     k2 = typeKind s2
 789
 790 -- See Note [Type synonyms and canonicalization].
 791 -- Check whether the given variable occurs in the given type.  We may
 792 -- have needed to do some type synonym unfolding in order to get rid
 793 -- of the variable, so we also return the unfolded version of the
 794 -- type, which is guaranteed to be syntactically free of the given
 795 -- type variable.  If the type is already syntactically free of the
 796 -- variable, then the same type is returned.
 797 --
 798 -- Precondition: the two types are not equal (looking though synonyms)
 799 canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
 800 canOccursCheck _gw tv xi = return (expandAway tv xi)
 801 \end{code}
 802
 803 @expandAway tv xi@ expands synonyms in xi just enough to get rid of
 804 occurrences of tv, if that is possible; otherwise, it returns Nothing.
 805 For example, suppose we have
 806   type F a b = [a]
 807 Then
 808   expandAway b (F Int b) = Just [Int]
 809 but
 810   expandAway a (F a Int) = Nothing
 811
 812 We don't promise to do the absolute minimum amount of expanding
 813 necessary, but we try not to do expansions we don't need to.  We
 814 prefer doing inner expansions first.  For example,
 815   type F a b = (a, Int, a, [a])
 816   type G b   = Char
 817 We have
 818   expandAway b (F (G b)) = F Char
 819 even though we could also expand F to get rid of b.
 820
 821 \begin{code}
 822 expandAway :: TcTyVar -> Xi -> Maybe Xi
 823 expandAway tv t@(TyVarTy tv')
 824   | tv == tv' = Nothing
 825   | otherwise = Just t
 826 expandAway tv xi
 827   | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
 828 expandAway tv (AppTy ty1 ty2)
 829   = do { ty1' <- expandAway tv ty1
 830        ; ty2' <- expandAway tv ty2
 831        ; return (mkAppTy ty1' ty2') }
 832 -- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
 833 expandAway tv (FunTy ty1 ty2)
 834   = do { ty1' <- expandAway tv ty1
 835        ; ty2' <- expandAway tv ty2
 836        ; return (mkFunTy ty1' ty2') }
 837 -- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
 838 expandAway tv ty@(ForAllTy {})
 839   = let (tvs,rho) = splitForAllTys ty
 840         tvs_knds  = map tyVarKind tvs
 841     in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
 842        -- Can't expand away the kinds unless we create
 843        -- fresh variables which we don't want to do at this point.
 844            Nothing
 845        else do { rho' <- expandAway tv rho
 846                ; return (mkForAllTys tvs rho') }
 847 expandAway tv (PredTy pred)
 848   = do { pred' <- expandAwayPred tv pred
 849        ; return (PredTy pred') }
 850 -- For a type constructor application, first try expanding away the
 851 -- offending variable from the arguments.  If that doesn't work, next
 852 -- see if the type constructor is a type synonym, and if so, expand
 853 -- it and try again.
 854 expandAway tv ty@(TyConApp tc tys)
 855   = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
 856
 857 expandAwayPred :: TcTyVar -> TcPredType -> Maybe TcPredType
 858 expandAwayPred tv (ClassP cls tys)
 859   = do { tys' <- mapM (expandAway tv) tys; return (ClassP cls tys') }
 860 expandAwayPred tv (EqPred ty1 ty2)
 861   = do { ty1' <- expandAway tv ty1
 862        ; ty2' <- expandAway tv ty2
 863        ; return (EqPred ty1' ty2') }
 864 expandAwayPred tv (IParam nm ty)
 865   = do { ty' <- expandAway tv ty
 866        ; return (IParam nm ty') }
 867
 868
 869
 870 \end{code}
 871
 872 Note [Type synonyms and canonicalization]
 873 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 874
 875 We treat type synonym applications as xi types, that is, they do not
 876 count as type function applications.  However, we do need to be a bit
 877 careful with type synonyms: like type functions they may not be
 878 generative or injective.  However, unlike type functions, they are
 879 parametric, so there is no problem in expanding them whenever we see
 880 them, since we do not need to know anything about their arguments in
 881 order to expand them; this is what justifies not having to treat them
 882 as specially as type function applications.  The thing that causes
 883 some subtleties is that we prefer to leave type synonym applications
 884 *unexpanded* whenever possible, in order to generate better error
 885 messages.
 886
 887 If we encounter an equality constraint with type synonym applications
 888 on both sides, or a type synonym application on one side and some sort
 889 of type application on the other, we simply must expand out the type
 890 synonyms in order to continue decomposing the equality constraint into
 891 primitive equality constraints.  For example, suppose we have
 892
 893   type F a = [Int]
 894
 895 and we encounter the equality
 896
 897   F a ~ [b]
 898
 899 In order to continue we must expand F a into [Int], giving us the
 900 equality
 901
 902   [Int] ~ [b]
 903
 904 which we can then decompose into the more primitive equality
 905 constraint
 906
 907   Int ~ b.
 908
 909 However, if we encounter an equality constraint with a type synonym
 910 application on one side and a variable on the other side, we should
 911 NOT (necessarily) expand the type synonym, since for the purpose of
 912 good error messages we want to leave type synonyms unexpanded as much
 913 as possible.
 914
 915 However, there is a subtle point with type synonyms and the occurs
 916 check that takes place for equality constraints of the form tv ~ xi.
 917 As an example, suppose we have
 918
 919   type F a = Int
 920
 921 and we come across the equality constraint
 922
 923   a ~ F a
 924
 925 This should not actually fail the occurs check, since expanding out
 926 the type synonym results in the legitimate equality constraint a ~
 927 Int.  We must actually do this expansion, because unifying a with F a
 928 will lead the type checker into infinite loops later.  Put another
 929 way, canonical equality constraints should never *syntactically*
 930 contain the LHS variable in the RHS type.  However, we don't always
 931 need to expand type synonyms when doing an occurs check; for example,
 932 the constraint
 933
 934   a ~ F b
 935
 936 is obviously fine no matter what F expands to. And in this case we
 937 would rather unify a with F b (rather than F b's expansion) in order
 938 to get better error messages later.
 939
 940 So, when doing an occurs check with a type synonym application on the
 941 RHS, we use some heuristics to find an expansion of the RHS which does
 942 not contain the variable from the LHS.  In particular, given
 943
 944   a ~ F t1 ... tn
 945
 946 we first try expanding each of the ti to types which no longer contain
 947 a.  If this turns out to be impossible, we next try expanding F
 948 itself, and so on.
 949
 950
 951 %************************************************************************
 952 %*                                                                      *
 953 %*          Functional dependencies, instantiation of equations
 954 %*                                                                      *
 955 %************************************************************************
 956
 957 When we spot an equality arising from a functional dependency,
 958 we now use that equality (a "wanted") to rewrite the work-item
 959 constraint right away.  This avoids two dangers
 960
 961  Danger 1: If we send the original constraint on down the pipeline
 962            it may react with an instance declaration, and in delicate
 963            situations (when a Given overlaps with an instance) that
 964            may produce new insoluble goals: see Trac #4952
 965
 966  Danger 2: If we don't rewrite the constraint, it may re-react
 967            with the same thing later, and produce the same equality
 968            again --> termination worries.
 969
 970 To achieve this required some refactoring of FunDeps.lhs (nicer
 971 now!).
 972
 973 \begin{code}
 974 rewriteWithFunDeps :: [Equation]
 975                    -> [Xi] -> CtFlavor
 976                    -> TcS (Maybe ([Xi], [Coercion], WorkList))
 977 rewriteWithFunDeps eqn_pred_locs xis fl
 978  = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
 979       ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
 980             fd_ev_pos = concat fd_ev_poss
 981             (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
 982       ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
 983       ; let fd_work = unionWorkLists fds
 984       ; if isEmptyWorkList fd_work
 985         then return Nothing
 986         else return (Just (rewritten_xis, cos, fd_work)) }
 987
 988 instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
 989               -> Equation
 990               -> TcS [(Int, FlavoredEvVar)]
 991 -- Post: Returns the position index as well as the corresponding FunDep equality
 992 instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
 993                         , fd_pred1 = d1, fd_pred2 = d2 })
 994   = do { let tvs = varSetElems qtvs
 995        ; tvs' <- mapM instFlexiTcS tvs
 996        ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
 997        ; mapM (do_one subst) eqs }
 998   where
 999     fl' = case fl of
1000              Given _     -> panic "mkFunDepEqns"
1001              Wanted  loc -> Wanted  (push_ctx loc)
1002              Derived loc -> Derived (push_ctx loc)
1003
1004     push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1005
1006     do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
1007        = do { let sty1 = Type.substTy subst ty1
1008                   sty2 = Type.substTy subst ty2
1009             ; ev <- newCoVar sty1 sty2
1010             ; return (i, mkEvVarX ev fl') }
1011
1012 rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
1013                   -> [Type]                -- A sequence of types: tys
1014                   -> [(Type,Coercion)]     -- Returns            : [(ty', co : ty' ~ ty)]
1015 rewriteDictParams param_eqs tys
1016   = zipWith do_one tys [0..]
1017   where
1018     do_one :: Type -> Int -> (Type,Coercion)
1019     do_one ty n = case lookup n param_eqs of
1020                     Just wev -> (get_fst_ty wev, mkCoVarCo (evVarOf wev))
1021                     Nothing  -> (ty,             mkReflCo ty)   -- Identity
1022
1023     get_fst_ty wev = case evVarOfPred wev of
1024                           EqPred ty1 _ -> ty1
1025                           _ -> panic "rewriteDictParams: non equality fundep"
1026
1027 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1028          -> TcM (TidyEnv, SDoc)
1029 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1030   = do  { zpred1 <- TcM.zonkTcPredType pred1
1031         ; zpred2 <- TcM.zonkTcPredType pred2
1032         ; let { tpred1 = tidyPred tidy_env zpred1
1033               ; tpred2 = tidyPred tidy_env zpred2 }
1034         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1035                           nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
1036                           nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1037         ; return (tidy_env, msg) }
1038 \end{code}