compiler/typecheck/TcTyFuns.lhs

   1 Normalisation of type terms relative to type instances as well as
   2 normalisation and entailment checking of equality constraints.
   3
   4 \begin{code}
   5 module TcTyFuns (
   6   -- type normalisation wrt to toplevel equalities only
   7   tcNormaliseFamInst,
   8
   9   -- instance normalisation wrt to equalities
  10   tcReduceEqs,
  11
  12   -- errors
  13   misMatchMsg, failWithMisMatch,
  14
  15 ) where
  16
  17
  18 #include "HsVersions.h"
  19
  20 --friends
  21 import TcRnMonad
  22 import TcEnv
  23 import Inst
  24 import TcType
  25 import TcMType
  26
  27 -- GHC
  28 import Coercion
  29 import Type
  30 import TypeRep  ( Type(..) )
  31 import TyCon
  32 import HsSyn
  33 import VarEnv
  34 import VarSet
  35 import Var
  36 import Name
  37 import Bag
  38 import Outputable
  39 import SrcLoc   ( Located(..) )
  40 import Maybes
  41 import MonadUtils
  42 import FastString
  43
  44 -- standard
  45 import Data.List
  46 import Control.Monad
  47 \end{code}
  48
  49
  50 %************************************************************************
  51 %*                                                                      *
  52                 Normalisation of types wrt toplevel equality schemata
  53 %*                                                                      *
  54 %************************************************************************
  55
  56 Unfold a single synonym family instance and yield the witnessing coercion.
  57 Return 'Nothing' if the given type is either not synonym family instance
  58 or is a synonym family instance that has no matching instance declaration.
  59 (Applies only if the type family application is outermost.)
  60
  61 For example, if we have
  62
  63   :Co:R42T a :: T [a] ~ :R42T a
  64
  65 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
  66
  67 \begin{code}
  68 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
  69 tcUnfoldSynFamInst (TyConApp tycon tys)
  70   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
  71   = return Nothing
  72   | otherwise
  73   = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
  74        ; maybeFamInst <- tcLookupFamInst tycon tys
  75        ; case maybeFamInst of
  76            Nothing                -> return Nothing
  77            Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
  78                                                     mkTyConApp coe_tc rep_tys)
  79              where
  80                coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
  81                                    (tyConFamilyCoercion_maybe rep_tc)
  82        }
  83 tcUnfoldSynFamInst _other = return Nothing
  84 \end{code}
  85
  86 Normalise 'Type's and 'PredType's by unfolding type family applications where
  87 possible (ie, we treat family instances as a TRS).  Also zonk meta variables.
  88
  89         tcNormaliseFamInst ty = (co, ty')
  90         then   co : ty ~ ty'
  91
  92 \begin{code}
  93 -- |Normalise the given type as far as possible with toplevel equalities.
  94 -- This results in a coercion witnessing the type equality, in addition to the
  95 -- normalised type.
  96 --
  97 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
  98 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
  99 \end{code}
 100
 101 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
 102 apply the normalisation function gives as the first argument to every TyConApp
 103 and every TyVarTy subterm.
 104
 105         tcGenericNormaliseFamInst fun ty = (co, ty')
 106         then   co : ty ~ ty'
 107
 108 This function is (by way of using smart constructors) careful to ensure that
 109 the returned coercion is exactly IdCo (and not some semantically equivalent,
 110 but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
 111 makes it easy for the caller to determine whether the type changed.  BUT
 112 even if we return IdCo, ty' may be *syntactically* different from ty due to
 113 unfolded closed type synonyms (by way of tcCoreView).  In the interest of
 114 good error messages, callers should discard ty' in favour of ty in this case.
 115
 116 \begin{code}
 117 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
 118                              -- what to do with type functions and tyvars
 119                            -> TcType                    -- old type
 120                            -> TcM (CoercionI, TcType)   -- (coercion, new type)
 121 tcGenericNormaliseFamInst fun ty
 122   | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
 123 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
 124   = do  { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 125         ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
 126         ; maybe_ty_co <- fun (mkTyConApp tyCon ntys)     -- use normalised args!
 127         ; case maybe_ty_co of
 128             -- a matching family instance exists
 129             Just (ty', co) ->
 130               do { let first_coi = mkTransCoI tycon_coi (ACo co)
 131                  ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
 132                  ; let fix_coi = mkTransCoI first_coi rest_coi
 133                  ; return (fix_coi, nty)
 134                  }
 135             -- no matching family instance exists
 136             -- we do not do anything
 137             Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
 138         }
 139 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
 140   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 141         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
 142         ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
 143         }
 144 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
 145   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 146         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
 147         ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
 148         }
 149 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
 150   = do  { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
 151         ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
 152         }
 153 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
 154   | isTcTyVar tv
 155   = do  { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
 156         ; res <- lookupTcTyVar tv
 157         ; case res of
 158             DoneTv _ ->
 159               do { maybe_ty' <- fun ty
 160                  ; case maybe_ty' of
 161                      Nothing         -> return (IdCo, ty)
 162                      Just (ty', co1) ->
 163                        do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
 164                           ; return (ACo co1 `mkTransCoI` coi2, ty'')
 165                           }
 166                  }
 167             IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
 168         }
 169   | otherwise
 170   = return (IdCo, ty)
 171 tcGenericNormaliseFamInst fun (PredTy predty)
 172   = do  { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
 173         ; return (coi, PredTy pred') }
 174
 175 ---------------------------------
 176 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
 177                               -> TcPredType
 178                               -> TcM (CoercionI, TcPredType)
 179
 180 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
 181   = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 182        ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
 183        }
 184 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
 185   = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
 186        ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
 187        }
 188 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
 189   = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
 190        ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
 191        ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
 192 \end{code}
 193
 194
 195 %************************************************************************
 196 %*                                                                      *
 197                 Normalisation of instances wrt to equalities
 198 %*                                                                      *
 199 %************************************************************************
 200
 201 Given a set of given, local constraints and a set of wanted constraints,
 202 simplify the wanted equalities as far as possible and normalise both local and
 203 wanted dictionaries with respect to the equalities.
 204
 205 In addition to the normalised local dictionaries and simplified wanteds, the
 206 function yields bindings for instantiated meta variables (due to solving
 207 equality constraints) and dictionary bindings (due to simplifying class
 208 constraints).  The bag of type variable bindings only contains bindings for
 209 non-local variables - i.e., type variables other than those newly created by
 210 the present function.  Consequently, type improvement took place iff the bag
 211 of bindings contains any bindings for proper type variables (not just covars).
 212 The solver does not instantiate any non-local variables; i.e., the bindings
 213 must be executed by the caller.
 214
 215 All incoming constraints are assumed to be zonked already.  All outgoing
 216 constraints will be zonked again.
 217
 218 NB: The solver only has local effects that cannot be observed from outside.
 219     In particular, it can be executed twice on the same constraint set with
 220     the same result (modulo generated variables names).
 221
 222 \begin{code}
 223 tcReduceEqs :: [Inst]             -- locals
 224             -> [Inst]             -- wanteds
 225             -> TcM ([Inst],       -- normalised locals (w/o equalities)
 226                     [Inst],       -- normalised wanteds (including equalities)
 227                     TcTyVarBinds, -- bindings for meta type variables
 228                     TcDictBinds)  -- bindings for all simplified dictionaries
 229 tcReduceEqs locals wanteds
 230   = do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $
 231            do { let (local_eqs  , local_dicts)   = partition isEqInst locals
 232                     (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
 233               ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
 234               ; eqCfg2 <- normaliseDicts False local_dicts
 235               ; eqCfg3 <- normaliseDicts True  wanteds_dicts
 236               ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig`
 237                                        eqCfg2 `unionEqConfig`
 238                                        eqCfg3)
 239               ; finaliseEqsAndDicts freeFlexibles eqCfg
 240               }
 241          -- execute type bindings of skolem flexibles...
 242        ; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles
 243          -- ...and zonk the constraints to propagate the bindings
 244        ; locals_z  <- zonkInsts locals
 245        ; wanteds_z <- zonkInsts wanteds
 246        ; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds)
 247        }
 248    where
 249      -- unification variables that appear in the environment and may not be
 250      -- instantiated - this includes coercion variables
 251      freeFlexibles = tcTyVarsOfInsts locals `unionVarSet`
 252                      tcTyVarsOfInsts wanteds
 253
 254      pruneTyBinds tybinds freeFlexibles
 255        = do { let tybinds'                      = bagToList tybinds
 256                   (skolem_tybinds, env_tybinds) = partition isSkolem tybinds'
 257             ; execTcTyVarBinds (listToBag skolem_tybinds)
 258             ; return $ listToBag env_tybinds
 259             }
 260        where
 261          isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles)
 262 \end{code}
 263
 264
 265 %************************************************************************
 266 %*                                                                      *
 267                 Equality Configurations
 268 %*                                                                      *
 269 %************************************************************************
 270
 271 We maintain normalised equalities together with the skolems introduced as
 272 intermediates during flattening of equalities as well as
 273
 274 \begin{code}
 275 -- |Configuration of normalised equalities used during solving.
 276 --
 277 data EqConfig = EqConfig { eqs     :: [RewriteInst]     -- all equalities
 278                          , locals  :: [Inst]            -- given dicts
 279                          , wanteds :: [Inst]            -- wanted dicts
 280                          , binds   :: TcDictBinds       -- bindings
 281                          }
 282
 283 addEq :: EqConfig -> RewriteInst -> EqConfig
 284 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
 285
 286 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
 287 unionEqConfig eqc1 eqc2 = EqConfig
 288                           { eqs     = eqs eqc1 ++ eqs eqc2
 289                           , locals  = locals eqc1 ++ locals eqc2
 290                           , wanteds = wanteds eqc1 ++ wanteds eqc2
 291                           , binds   = binds eqc1 `unionBags` binds eqc2
 292                           }
 293
 294 emptyEqConfig :: EqConfig
 295 emptyEqConfig = EqConfig
 296                 { eqs     = []
 297                 , locals  = []
 298                 , wanteds = []
 299                 , binds   = emptyBag
 300                 }
 301
 302 instance Outputable EqConfig where
 303   ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
 304     = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
 305 \end{code}
 306
 307 The set of operations on an equality configuration.  We obtain the initialise
 308 configuration by normalisation ('normaliseEqs'), solve the equalities by
 309 propagation ('propagateEqs'), and eventually finalise the configuration when
 310 no further propoagation is possible.
 311
 312 \begin{code}
 313 -- |Turn a set of equalities into an equality configuration for solving.
 314 --
 315 -- Precondition: The Insts are zonked.
 316 --
 317 normaliseEqs :: [Inst] -> TcM EqConfig
 318 normaliseEqs eqs
 319   = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs )
 320        ; traceTc $ ptext (sLit "Entering normaliseEqs")
 321
 322        ; eqss <- mapM normEqInst eqs
 323        ; return $ emptyEqConfig { eqs = concat eqss }
 324        }
 325
 326 -- |Flatten the type arguments of all dictionaries, returning the result as a
 327 -- equality configuration.  The dictionaries go into the 'wanted' component if
 328 -- the second argument is 'True'.
 329 --
 330 -- Precondition: The Insts are zonked.
 331 --
 332 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
 333 normaliseDicts isWanted insts
 334   = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
 335                          ptext (if isWanted then sLit "[Wanted] for"
 336                                             else sLit "[Local] for"))
 337                      4 (ppr insts)
 338
 339        ; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts
 340
 341        ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
 342                      4 (ppr insts' $$ ppr eqss)
 343        ; return $ emptyEqConfig { eqs     = concat eqss
 344                                 , locals  = if isWanted then [] else insts'
 345                                 , wanteds = if isWanted then insts' else []
 346                                 , binds   = unionManyBags bindss
 347                                 }
 348        }
 349
 350 -- |Solves the equalities as far as possible by applying propagation rules.
 351 --
 352 propagateEqs :: EqConfig -> TcM EqConfig
 353 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
 354   = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
 355                      4 (ppr eqCfg)
 356
 357        ; propagate todoEqs (eqCfg {eqs = []})
 358        }
 359
 360 -- |Finalise a set of equalities and associated dictionaries after
 361 -- propagation.  The first returned set of instances are the locals (without
 362 -- equalities) and the second set are all residual wanteds, including
 363 -- equalities.  In addition, we return all generated dictionary bindings.
 364 --
 365 finaliseEqsAndDicts :: TcTyVarSet -> EqConfig
 366                     -> TcM ([Inst], [Inst], TcDictBinds)
 367 finaliseEqsAndDicts freeFlexibles (EqConfig { eqs     = eqs
 368                                             , locals  = locals
 369                                             , wanteds = wanteds
 370                                             , binds   = binds
 371                                             })
 372   = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
 373
 374        ; (eqs', subst_binds, locals', wanteds')
 375            <- substitute eqs locals wanteds checkingMode freeFlexibles
 376        ; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles
 377        ; let final_binds = subst_binds `unionBags` binds
 378
 379          -- Assert that all cotvs of wanted equalities are still unfilled, and
 380          -- zonk all final insts, to make any improvement visible
 381        ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
 382        ; zonked_locals  <- zonkInsts locals'
 383        ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
 384        ; return (zonked_locals, zonked_wanteds, final_binds)
 385        }
 386   where
 387     checkingMode = length eqs > length wanteds || not (null locals)
 388                      -- no local equalities or dicts => checking mode
 389 \end{code}
 390
 391
 392 %************************************************************************
 393 %*                                                                      *
 394                 Normalisation of equalities
 395 %*                                                                      *
 396 %************************************************************************
 397
 398 A normal equality is a properly oriented equality with associated coercion
 399 that contains at most one family equality (in its left-hand side) is oriented
 400 such that it may be used as a rewrite rule.  It has one of the following two
 401 forms:
 402
 403 (1) co :: F t1..tn ~ t  (family equalities)
 404 (2) co :: x ~ t         (variable equalities)
 405
 406 Variable equalities fall again in two classes:
 407
 408 (2a) co :: x ~ t, where t is *not* a variable, or
 409 (2b) co :: x ~ y, where x > y.
 410
 411 The types t, t1, ..., tn may not contain any occurrences of synonym
 412 families.  Moreover, in Forms (2) & (3), the left-hand side may not occur in
 413 the right-hand side, and the relation x > y is an (nearly) arbitrary, but
 414 total order on type variables.  The only restriction that we impose on that
 415 order is that for x > y, we are happy to instantiate x with y taking into
 416 account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
 417
 418 \begin{code}
 419 data RewriteInst
 420   = RewriteVar  -- Form (2) above
 421     { rwi_var     :: TyVar    -- may be rigid or flexible
 422     , rwi_right   :: TcType   -- contains no synonym family applications
 423     , rwi_co      :: EqInstCo -- the wanted or given coercion
 424     , rwi_loc     :: InstLoc
 425     , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
 426     , rwi_swapped :: Bool     -- swapped orientation of original EqInst
 427     }
 428   | RewriteFam  -- Forms (1) above
 429     { rwi_fam     :: TyCon    -- synonym family tycon
 430     , rwi_args    :: [Type]   -- contain no synonym family applications
 431     , rwi_right   :: TcType   -- contains no synonym family applications
 432     , rwi_co      :: EqInstCo -- the wanted or given coercion
 433     , rwi_loc     :: InstLoc
 434     , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
 435     , rwi_swapped :: Bool     -- swapped orientation of original EqInst
 436     }
 437
 438 isWantedRewriteInst :: RewriteInst -> Bool
 439 isWantedRewriteInst = isWantedCo . rwi_co
 440
 441 isRewriteVar :: RewriteInst -> Bool
 442 isRewriteVar (RewriteVar {}) = True
 443 isRewriteVar _               = False
 444
 445 tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
 446 tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
 447   = unitVarSet tv `unionVarSet` tyVarsOfType ty
 448 tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
 449   = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty
 450
 451 rewriteInstToInst :: RewriteInst -> TcM Inst
 452 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
 453   = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
 454 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
 455   = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
 456
 457 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
 458 -- around.
 459 --
 460 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
 461 deriveEqInst rewrite ty1 ty2 co
 462   = do { co_adjusted <- if not swapped then return co
 463                                        else mkSymEqInstCo co (ty2, ty1)
 464        ; return $ EqInst
 465                   { tci_left  = left
 466                   , tci_right = right
 467                   , tci_co    = co_adjusted
 468                   , tci_loc   = rwi_loc rewrite
 469                   , tci_name  = rwi_name rewrite
 470                   }
 471        }
 472   where
 473     swapped       = rwi_swapped rewrite
 474     (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
 475
 476 instance Outputable RewriteInst where
 477   ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
 478     = hsep [ pprEqInstCo co <+> text "::"
 479            , ppr (mkTyConApp fam args)
 480            , text "~>"
 481            , ppr rhs
 482            ]
 483   ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
 484     = hsep [ pprEqInstCo co <+> text "::"
 485            , ppr tv
 486            , text "~>"
 487            , ppr rhs
 488            ]
 489
 490 pprEqInstCo :: EqInstCo -> SDoc
 491 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
 492 pprEqInstCo (Right co)  = ptext (sLit "Local") <+> ppr co
 493 \end{code}
 494
 495 The following functions turn an arbitrary equality into a set of normal
 496 equalities.  This implements the WFlat and LFlat rules of the paper in one
 497 sweep.  However, we use flexible variables for both locals and wanteds, and
 498 avoid to carry around the unflattening substitution \Sigma (for locals) by
 499 already updating the skolems for locals with the family application that they
 500 represent - i.e., they will turn into that family application on the next
 501 zonking (which only happens after finalisation).
 502
 503 In a corresponding manner, normDict normalises class dictionaries by
 504 extracting any synonym family applications and generation appropriate normal
 505 equalities.
 506
 507 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
 508 we drop that equality and raise an error if it is a wanted or a warning if it
 509 is a local.
 510
 511 \begin{code}
 512 normEqInst :: Inst -> TcM [RewriteInst]
 513 -- Normalise one equality.
 514 normEqInst inst
 515   = ASSERT( isEqInst inst )
 516     do { traceTc $ ptext (sLit "normEqInst of ") <+>
 517                    pprEqInstCo co <+> text "::" <+>
 518                    ppr ty1 <+> text "~" <+> ppr ty2
 519        ; res <- go ty1 ty2 co
 520
 521        ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
 522        ; return res
 523        }
 524   where
 525     (ty1, ty2) = eqInstTys inst
 526     co         = eqInstCoercion inst
 527
 528       -- look through synonyms
 529     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
 530     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
 531
 532       -- left-to-right rule with type family head
 533     go ty1@(TyConApp con args) ty2 co
 534       | isOpenSynTyConApp ty1           -- only if not oversaturated
 535       = mkRewriteFam False con args ty2 co
 536
 537       -- right-to-left rule with type family head
 538     go ty1 ty2@(TyConApp con args) co
 539       | isOpenSynTyConApp ty2           -- only if not oversaturated
 540       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 541            ; mkRewriteFam True con args ty1 co'
 542            }
 543
 544       -- no outermost family
 545     go ty1 ty2 co
 546       = do { (ty1', co1, ty1_eqs) <- flattenType inst ty1
 547            ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
 548            ; let ty12_eqs  = ty1_eqs ++ ty2_eqs
 549                  sym_co2   = mkSymCoercion co2
 550                  eqTys     = (ty1', ty2')
 551            ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
 552            ; eqs <- checkOrientation ty1' ty2' co' inst
 553            ; if isLoopyEquality eqs ty12_eqs'
 554              then do { if isWantedCo (tci_co inst)
 555                        then
 556                           addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
 557                             eqInstMisMatch inst
 558                        else
 559                          warnDroppingLoopyEquality ty1 ty2
 560                      ; return ([])                 -- drop the equality
 561                      }
 562              else
 563                return (eqs ++ ty12_eqs')
 564            }
 565
 566     mkRewriteFam swapped con args ty2 co
 567       = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
 568            ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
 569            ; let co1       = mkTyConApp con cargs
 570                  sym_co2   = mkSymCoercion co2
 571                  all_eqs   = concat args_eqss ++ ty2_eqs
 572                  eqTys     = (mkTyConApp con args', ty2')
 573            ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
 574            ; let thisRewriteFam = RewriteFam
 575                                   { rwi_fam     = con
 576                                   , rwi_args    = args'
 577                                   , rwi_right   = ty2'
 578                                   , rwi_co      = co'
 579                                   , rwi_loc     = tci_loc inst
 580                                   , rwi_name    = tci_name inst
 581                                   , rwi_swapped = swapped
 582                                   }
 583            ; return $ thisRewriteFam : all_eqs'
 584            }
 585
 586     -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
 587     -- have a variable equality with 'a' on the lhs as the first equality.
 588     -- Then, check whether 'a' occurs in the lhs of any family equality
 589     -- generated by flattening.
 590     isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs
 591       where
 592         inRewriteFam (RewriteFam {rwi_args = args})
 593           = tv `elemVarSet` tyVarsOfTypes args
 594         inRewriteFam _ = False
 595     isLoopyEquality _ _ = False
 596
 597 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds)
 598 -- Normalise one dictionary or IP constraint.
 599 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
 600   = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
 601        ; let rewriteCo = PredTy $ ClassP clas cargs
 602              eqs       = concat args_eqss
 603              pred'     = ClassP clas args'
 604        ; if null eqs
 605          then  -- don't generate a binding if there is nothing to flatten
 606            return (inst, [], emptyBag)
 607          else do {
 608        ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
 609        ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
 610        ; return (inst', eqs', bind)
 611        }}
 612 normDict _isWanted inst
 613   = return (inst, [], emptyBag)
 614 -- !!!TODO: Still need to normalise IP constraints.
 615
 616 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
 617 -- Performs the occurs check, decomposition, and proper orientation
 618 -- (returns a singleton, or an empty list in case of a trivial equality)
 619 -- NB: We cannot assume that the two types already have outermost type
 620 --     synonyms expanded due to the recursion in the case of type applications.
 621 checkOrientation ty1 ty2 co inst
 622   = go ty1 ty2
 623   where
 624       -- look through synonyms
 625     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
 626     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 627
 628       -- identical types => trivial
 629     go ty1 ty2
 630       | ty1 `tcEqType` ty2
 631       = do { mkIdEqInstCo co ty1
 632            ; return []
 633            }
 634
 635       -- two tvs (distinct tvs, due to previous equation)
 636     go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
 637       = do { isBigger <- tv1 `tvIsBigger` tv2
 638            ; if isBigger                                      -- left greater
 639                then mkRewriteVar False tv1 ty2 co             --   => unchanged
 640                else do { co' <- mkSymEqInstCo co (ty2, ty1)   -- right greater
 641                        ; mkRewriteVar True tv2 ty1 co'        --   => swap
 642                        }
 643            }
 644
 645       -- only lhs is a tv => unchanged
 646     go ty1@(TyVarTy tv1) ty2
 647       | ty1 `tcPartOfType` ty2      -- occurs check!
 648       = occurCheckErr ty1 ty2
 649       | otherwise
 650       = mkRewriteVar False tv1 ty2 co
 651
 652       -- only rhs is a tv => swap
 653     go ty1 ty2@(TyVarTy tv2)
 654       | ty2 `tcPartOfType` ty1      -- occurs check!
 655       = occurCheckErr ty2 ty1
 656       | otherwise
 657       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 658            ; mkRewriteVar True tv2 ty1 co'
 659            }
 660
 661       -- data type constructor application => decompose
 662       -- NB: Special cased for efficiency - could be handled as type application
 663     go (TyConApp con1 args1) (TyConApp con2 args2)
 664       |  con1 == con2
 665       && isInjectiveTyCon con1   -- don't match family synonym apps
 666       = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
 667            ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
 668                      args1 args2 co_args
 669            ; return $ concat eqss
 670            }
 671
 672       -- function type => decompose
 673       -- NB: Special cased for efficiency - could be handled as type application
 674     go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
 675       = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
 676            ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
 677            ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
 678            ; return $ eqs_l ++ eqs_r
 679            }
 680
 681       -- type applications => decompose
 682     go ty1 ty2
 683       | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1   -- won't split fam apps
 684       , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
 685       = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
 686            ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
 687            ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
 688            ; return $ eqs_l ++ eqs_r
 689            }
 690
 691       -- inconsistency => type error
 692     go ty1 ty2
 693       = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
 694         eqInstMisMatch inst
 695
 696     mkRewriteVar swapped tv ty co = return [RewriteVar
 697                                             { rwi_var     = tv
 698                                             , rwi_right   = ty
 699                                             , rwi_co      = co
 700                                             , rwi_loc     = tci_loc inst
 701                                             , rwi_name    = tci_name inst
 702                                             , rwi_swapped = swapped
 703                                             }]
 704
 705     -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
 706     tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
 707     tvIsBigger tv1 tv2
 708       = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
 709       where
 710         isBigger tv1 (SkolemTv _)     tv2 (SkolemTv _)
 711           = return $ tv1 > tv2
 712         isBigger _   (MetaTv _ _)     _   (SkolemTv _)
 713           = return True
 714         isBigger _   (SkolemTv _)     _   (MetaTv _ _)
 715           = return False
 716         isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
 717           -- meta variable meets meta variable
 718           -- => be clever about which of the two to update
 719           --   (from TcUnify.uUnfilledVars minus boxy stuff)
 720           = case (info1, info2) of
 721               -- Avoid SigTvs if poss
 722               (SigTv _, SigTv _)             -> return $ tv1 > tv2
 723               (SigTv _, _      ) | k1_sub_k2 -> return False
 724               (_,       SigTv _) | k2_sub_k1 -> return True
 725
 726               (_, _)
 727                 | k1_sub_k2 &&
 728                   k2_sub_k1
 729                   -> case (nicer_to_update tv1, nicer_to_update tv2) of
 730                        (True, False) -> return True
 731                        (False, True) -> return False
 732                        _             -> return $ tv1 > tv2
 733                 | k1_sub_k2    -> return False
 734                 | k2_sub_k1    -> return True
 735                 | otherwise    -> kind_err >> return True
 736               -- Update the variable with least kind info
 737               -- See notes on type inference in Kind.lhs
 738               -- The "nicer to" part only applies if the two kinds are the same,
 739               -- so we can choose which to do.
 740           where
 741             kind_err = addErrCtxtM (unifyKindCtxt False tv1 (mkTyVarTy tv2)) $
 742                        unifyKindMisMatch k1 k2
 743
 744             k1 = tyVarKind tv1
 745             k2 = tyVarKind tv2
 746             k1_sub_k2 = k1 `isSubKind` k2
 747             k2_sub_k1 = k2 `isSubKind` k1
 748
 749             nicer_to_update tv = isSystemName (Var.varName tv)
 750                 -- Try to update sys-y type variables in preference to ones
 751                 -- gotten (say) by instantiating a polymorphic function with
 752                 -- a user-written type sig
 753
 754 flattenType :: Inst     -- context to get location  & name
 755             -> Type     -- the type to flatten
 756             -> TcM (Type,           -- the flattened type
 757                     Coercion,       -- coercion witness of flattening wanteds
 758                     [RewriteInst])  -- extra equalities
 759 -- Removes all family synonyms from a type by moving them into extra equalities
 760 flattenType inst ty = go ty
 761   where
 762       -- look through synonyms
 763     go ty | Just ty' <- tcView ty
 764       = do { (ty_flat, co, eqs) <- go ty'
 765            ; if null eqs
 766              then     -- unchanged, keep the old type with folded synonyms
 767                return (ty, ty, [])
 768              else
 769                return (ty_flat, co, eqs)
 770            }
 771
 772       -- type variable => nothing to do
 773     go ty@(TyVarTy _)
 774       = return (ty, ty, [])
 775
 776       -- type family application & family arity matches number of args
 777       -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
 778     go ty@(TyConApp con args)
 779       | isOpenSynTyConApp ty   -- only if not oversaturated
 780       = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
 781            ; alpha <- newFlexiTyVar (typeKind ty)
 782            ; let alphaTy = mkTyVarTy alpha
 783            ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
 784            ; let thisRewriteFam = RewriteFam
 785                                   { rwi_fam     = con
 786                                   , rwi_args    = args'
 787                                   , rwi_right   = alphaTy
 788                                   , rwi_co      = mkWantedCo cotv
 789                                   , rwi_loc     = tci_loc inst
 790                                   , rwi_name    = tci_name inst
 791                                   , rwi_swapped = True
 792                                   }
 793            ; return (alphaTy,
 794                      mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
 795                      thisRewriteFam : concat args_eqss)
 796            }
 797
 798       -- data constructor application => flatten subtypes
 799       -- NB: Special cased for efficiency - could be handled as type application
 800     go ty@(TyConApp con args)
 801       | not (isOpenSynTyCon con)   -- don't match oversaturated family apps
 802       = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
 803            ; if null args_eqss
 804              then     -- unchanged, keep the old type with folded synonyms
 805                return (ty, ty, [])
 806              else
 807                return (mkTyConApp con args',
 808                        mkTyConApp con cargs,
 809                        concat args_eqss)
 810            }
 811
 812       -- function type => flatten subtypes
 813       -- NB: Special cased for efficiency - could be handled as type application
 814     go ty@(FunTy ty_l ty_r)
 815       = do { (ty_l', co_l, eqs_l) <- go ty_l
 816            ; (ty_r', co_r, eqs_r) <- go ty_r
 817            ; if null eqs_l && null eqs_r
 818              then     -- unchanged, keep the old type with folded synonyms
 819                return (ty, ty, [])
 820              else
 821                return (mkFunTy ty_l' ty_r',
 822                        mkFunTy co_l co_r,
 823                        eqs_l ++ eqs_r)
 824            }
 825
 826       -- type application => flatten subtypes
 827     go ty
 828       | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
 829                              -- need to use the smart split as ty may be an
 830                              -- oversaturated family application
 831       = do { (ty_l', co_l, eqs_l) <- go ty_l
 832            ; (ty_r', co_r, eqs_r) <- go ty_r
 833            ; if null eqs_l && null eqs_r
 834              then     -- unchanged, keep the old type with folded synonyms
 835                return (ty, ty, [])
 836              else
 837                return (mkAppTy ty_l' ty_r',
 838                        mkAppTy co_l co_r,
 839                        eqs_l ++ eqs_r)
 840            }
 841
 842       -- forall type => panic if the body contains a type family
 843       -- !!!TODO: As long as the family does not contain a quantified variable
 844       --          we might pull it out, but what if it does contain a quantified
 845       --          variable???
 846     go ty@(ForAllTy _ body)
 847       | null (tyFamInsts body)
 848       = return (ty, ty, [])
 849       | otherwise
 850       = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
 851
 852       -- we should never see a predicate type
 853     go (PredTy _)
 854       = panic "TcTyFuns.flattenType: unexpected PredType"
 855
 856     go _ = panic "TcTyFuns: suppress bogus warning"
 857
 858 adjustCoercions :: EqInstCo            -- coercion of original equality
 859                 -> Coercion            -- coercion witnessing the left rewrite
 860                 -> Coercion            -- coercion witnessing the right rewrite
 861                 -> (Type, Type)        -- types of flattened equality
 862                 -> [RewriteInst]       -- equalities from flattening
 863                 -> TcM (EqInstCo,      -- coercion for flattened equality
 864                         [RewriteInst]) -- final equalities from flattening
 865 -- Depending on whether we flattened a local or wanted equality, that equality's
 866 -- coercion and that of the new equalities produced during flattening are
 867 -- adjusted .
 868 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
 869     -- wanted => generate a fresh coercion variable for the flattened equality
 870   = do { cotv' <- newMetaCoVar ty_l ty_r
 871        ; bindMetaTyVar cotv $
 872            (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
 873        ; return (Left cotv', all_eqs)
 874        }
 875
 876 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
 877     -- local => turn all new equalities into locals and update (but not zonk)
 878     --          the skolem
 879   = do { all_eqs' <- mapM wantedToLocal all_eqs
 880        ; return (co, all_eqs')
 881        }
 882
 883 mkDictBind :: Inst                 -- original instance
 884            -> Bool                 -- is this a wanted contraint?
 885            -> Coercion             -- coercion witnessing the rewrite
 886            -> PredType             -- coerced predicate
 887            -> TcM (Inst,           -- new inst
 888                    TcDictBinds)    -- binding for coerced dictionary
 889 mkDictBind dict isWanted rewriteCo pred
 890   = do { dict' <- newDictBndr loc pred
 891          -- relate the old inst to the new one
 892          -- target_dict = source_dict `cast` st_co
 893        ; let (target_dict, source_dict, st_co)
 894                | isWanted  = (dict,  dict', mkSymCoercion rewriteCo)
 895                | otherwise = (dict', dict,  rewriteCo)
 896                  -- we have
 897                  --   co :: dict ~ dict'
 898                  -- hence, if isWanted
 899                  --       dict  = dict' `cast` sym co
 900                  --        else
 901                  --       dict' = dict  `cast` co
 902              expr      = HsVar $ instToId source_dict
 903              cast_expr = HsWrap (WpCast st_co) expr
 904              rhs       = L (instLocSpan loc) cast_expr
 905              binds     = instToDictBind target_dict rhs
 906        ; return (dict', binds)
 907        }
 908   where
 909     loc = tci_loc dict
 910
 911 -- gamma ::^l Fam args ~ alpha
 912 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
 913 --    (the update of alpha will not be apparent during propagation, as we
 914 --    never follow the indirections of meta variables; it will be revealed
 915 --    when the equality is zonked)
 916 --
 917 --  NB: It's crucial to update *both* alpha and gamma, as gamma may already
 918 --      have escaped into some other coercions during normalisation.
 919 --
 920 --      We do actually update alpha and gamma by side effect (instead of
 921 --      only remembering the binding with `bindMetaTyVar', as we do for all
 922 --      other tyvars).  We can do this as the side effects are strictly
 923 --      *local*; we know that both alpha and gamma were just a moment ago
 924 --      introduced by normalisation.
 925 --
 926 wantedToLocal :: RewriteInst -> TcM RewriteInst
 927 wantedToLocal eq@(RewriteFam {rwi_fam   = fam,
 928                               rwi_args  = args,
 929                               rwi_right = TyVarTy alpha,
 930                               rwi_co    = Left gamma})
 931   = do { writeMetaTyVar alpha (mkTyConApp fam args)
 932        ; writeMetaTyVar gamma (mkTyConApp fam args)
 933        ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
 934        }
 935 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
 936 \end{code}
 937
 938
 939 %************************************************************************
 940 %*                                                                      *
 941                 Propagation of equalities
 942 %*                                                                      *
 943 %************************************************************************
 944
 945 Apply the propagation rules exhaustively.
 946
 947 \begin{code}
 948 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
 949 propagate []       eqCfg = return eqCfg
 950 propagate (eq:eqs) eqCfg
 951   = do { optEqs <- applyTop eq
 952        ; case optEqs of
 953
 954               -- Top applied to 'eq' => retry with new equalities
 955            Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
 956
 957               -- Top doesn't apply => try subst rules with all other
 958               --   equalities, after that 'eq' can go into the residual list
 959            Nothing   -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
 960                            ; propagate eqs' (eqCfg' `addEq` eq)
 961                            }
 962        }
 963
 964 applySubstRules :: RewriteInst                    -- currently considered eq
 965                 -> [RewriteInst]                  -- todo eqs list
 966                 -> EqConfig                       -- residual
 967                 -> TcM ([RewriteInst], EqConfig)  -- new todo & residual
 968 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
 969   = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
 970        ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
 971        ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
 972                  eqConfig {eqs = unchangedEqs_r})
 973        }
 974
 975 mapSubstRules :: RewriteInst     -- try substituting this equality
 976               -> [RewriteInst]   -- into these equalities
 977               -> TcM ([RewriteInst], [RewriteInst])
 978 mapSubstRules eq eqs
 979   = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
 980        ; return (concat newEqss, concat unchangedEqss)
 981        }
 982   where
 983     substRules eq1 eq2
 984       = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
 985                         4 (ppr eq1 $$ ppr eq2)
 986
 987                -- try the SubstFam rule
 988            ; optEqs <- applySubstFam eq1 eq2
 989            ; case optEqs of
 990                Just eqs -> return (eqs, [])
 991                Nothing  -> do
 992            {   -- try the SubstVarVar rule
 993              optEqs <- applySubstVarVar eq1 eq2
 994            ; case optEqs of
 995                Just eqs -> return (eqs, [])
 996                Nothing  -> do
 997            {   -- try the SubstVarFam rule
 998              optEqs <- applySubstVarFam eq1 eq2
 999            ; case optEqs of
1000                Just eq -> return ([eq], [])
1001                Nothing -> return ([], [eq2])
1002                  -- if no rule matches, we return the equlity we tried to
1003                  -- substitute into unchanged
1004            }}}
1005 \end{code}
1006
1007 Attempt to apply the Top rule.  The rule is
1008
1009   co :: F t1..tn ~ t
1010   =(Top)=>
1011   co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
1012
1013 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
1014
1015 Returns Nothing if the rule could not be applied.  Otherwise, the resulting
1016 equality is normalised and a list of the normal equalities is returned.
1017
1018 \begin{code}
1019 applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
1020
1021 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
1022   = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
1023        ; case optTyCo of
1024            Nothing                -> return Nothing
1025            Just (lhs, rewrite_co)
1026              -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
1027                    ; eq' <- deriveEqInst eq lhs rhs co'
1028                    ; liftM Just $ normEqInst eq'
1029                    }
1030        }
1031   where
1032     co  = rwi_co eq
1033     rhs = rwi_right eq
1034
1035 applyTop _ = return Nothing
1036 \end{code}
1037
1038 Attempt to apply the SubstFam rule.  The rule is
1039
1040   co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s
1041   =(SubstFam)=>
1042   co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
1043
1044 where co1 may be a wanted only if co2 is a wanted, too.
1045
1046 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1047 co2' is normalised and a list of the normal equalities is returned.  (The
1048 equality co1 is not returned as it remain unaltered.)
1049
1050 \begin{code}
1051 applySubstFam :: RewriteInst
1052               -> RewriteInst
1053               -> TcM (Maybe ([RewriteInst]))
1054 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
1055               eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1056
1057     -- rule matches => rewrite
1058   | fam1 == fam2 && tcEqTypes args1 args2 &&
1059     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1060   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1061        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1062        ; liftM Just $ normEqInst eq2'
1063        }
1064
1065     -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1066   | fam1 == fam2 && tcEqTypes args1 args2 &&
1067     (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1068   = return $ Just [eq2]
1069
1070   where
1071     lhs = rwi_right eq1
1072     rhs = rwi_right eq2
1073     co1 = eqInstCoType (rwi_co eq1)
1074     co2 = rwi_co eq2
1075
1076 applySubstFam _ _ = return Nothing
1077 \end{code}
1078
1079 Attempt to apply the SubstVarVar rule.  The rule is
1080
1081   co1 :: x ~ t  &  co2 :: x ~ s
1082   =(SubstVarVar)=>
1083   co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
1084
1085 where co1 may be a wanted only if co2 is a wanted, too.
1086
1087 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1088 co2' is normalised and a list of the normal equalities is returned.  (The
1089 equality co1 is not returned as it remain unaltered.)
1090
1091 \begin{code}
1092 applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
1093 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
1094                  eq2@(RewriteVar {rwi_var = tv2})
1095
1096     -- rule matches => rewrite
1097   | tv1 == tv2 &&
1098     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1099   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1100        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1101        ; liftM Just $ normEqInst eq2'
1102        }
1103
1104     -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1105   | tv1 == tv2 &&
1106     (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1107   = return $ Just [eq2]
1108
1109   where
1110     lhs = rwi_right eq1
1111     rhs = rwi_right eq2
1112     co1 = eqInstCoType (rwi_co eq1)
1113     co2 = rwi_co eq2
1114
1115 applySubstVarVar _ _ = return Nothing
1116 \end{code}
1117
1118 Attempt to apply the SubstVarFam rule.  The rule is
1119
1120   co1 :: x ~ t  &  co2 :: F s1..sn ~ s
1121   =(SubstVarFam)=>
1122   co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s
1123     with co2 = [co1/x](F s1..sn) |> co2'
1124
1125 where x occurs in F s1..sn. (co1 may be local or wanted.)
1126
1127 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1128 co2' is returned.  (The equality co1 is not returned as it remain unaltered.)
1129
1130 \begin{code}
1131 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1132
1133   -- rule matches => rewrite
1134 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1135                  eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1136   | tv1 `elemVarSet` tyVarsOfTypes args2
1137   = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1138              args2'   = substTysWith [tv1] [rhs1] args2
1139              lhs2     = mkTyConApp fam2 args2'
1140        ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1141        ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1142        }
1143   where
1144     rhs1 = rwi_right eq1
1145     rhs2 = rwi_right eq2
1146     co1  = eqInstCoType (rwi_co eq1)
1147     co2  = rwi_co eq2
1148
1149   -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1150 applySubstVarFam (RewriteFam {rwi_args = args1})
1151                  eq2@(RewriteVar {rwi_var = tv2})
1152   | tv2 `elemVarSet` tyVarsOfTypes args1
1153   = return $ Just eq2
1154
1155 applySubstVarFam _ _ = return Nothing
1156 \end{code}
1157
1158
1159 %************************************************************************
1160 %*                                                                      *
1161                 Finalisation of equalities
1162 %*                                                                      *
1163 %************************************************************************
1164
1165 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1166 (both local and wanted) into the right-hand sides of all other equalities and
1167 of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
1168 other *family* equalities.  This may lead to recursive equalities; i.e., (1)
1169 we need to apply the substitution implied by one equality exhaustively before
1170 turning to the next and (2) we need an occurs check.
1171
1172 We also apply the same substitutions to the local and wanted class and IP
1173 dictionaries.
1174
1175 We perform the substitutions in two steps:
1176
1177   Step A: Substitute variable equalities into the right-hand sides of all
1178           other equalities (but wanted only into wanteds) and into class and IP
1179           constraints (again wanteds only into wanteds).
1180
1181   Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
1182           'alpha' is a skolem flexible (i.e., not free in the environment),
1183           into the right-hand sides of all wanted variable equalities and into
1184           both sides of all wanted family equalities.
1185
1186   Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
1187           alpha' into the right-hand sides of all wanted variable equalities
1188           and into both sides of all wanted family equalities.
1189
1190 In inference mode, we do not substitute into variable equalities in Steps B & C.
1191
1192 The treatment of flexibles in wanteds is quite subtle.  We absolutely want to
1193 substitute variable equalities first; e.g., consider
1194
1195   F s ~ alpha, alpha ~ t
1196
1197 If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
1198 This would be bad as `F s' is less useful, eg, as an argument to a class
1199 constraint.
1200
1201 The restriction on substituting locals is necessary due to examples, such as
1202
1203   F delta ~ alpha, F alpha ~ delta,
1204
1205 where `alpha' is a skolem flexible and `delta' a environment flexible. We need
1206 to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
1207 we may wrongly claim to having performed an improvement, which can lead to
1208 non-termination of the combined class-family solver.
1209
1210 We do also substitute flexibles, as in `alpha ~ t' into class constraints.
1211 When `alpha' is later instantiated, we'd get the same effect, but in the
1212 meantime the class constraint would miss some information, which would be a
1213 problem in an integrated equality-class solver.
1214
1215 NB:
1216 * Given that we apply the substitution corresponding to a single equality
1217   exhaustively, before turning to the next, and because we eliminate recursive
1218   equalities, all opportunities for subtitution will have been exhausted after
1219   we have considered each equality once.
1220
1221 \begin{code}
1222 substitute :: [RewriteInst]       -- equalities
1223            -> [Inst]              -- local class dictionaries
1224            -> [Inst]              -- wanted class dictionaries
1225            -> Bool                -- True ~ checking mode; False ~ inference
1226            -> TyVarSet            -- flexibles free in the environment
1227            -> TcM ([RewriteInst], -- equalities after substitution
1228                    TcDictBinds,   -- all newly generated dictionary bindings
1229                    [Inst],        -- local dictionaries after substitution
1230                    [Inst])        -- wanted dictionaries after substitution
1231 substitute eqs locals wanteds checkingMode freeFlexibles
1232   = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
1233     -- sorting the equalities appropriately: first all variable, then all
1234     -- family/skolem, and then the remaining family equalities.
1235     let (var_eqs, fam_eqs)             = partition isRewriteVar eqs
1236         (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
1237     in
1238     subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
1239   where
1240     isFamSkolemEq (RewriteFam {rwi_right = ty})
1241       | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
1242     isFamSkolemEq _ = False
1243
1244     subst [] res binds locals wanteds
1245       = return (res, binds, locals, wanteds)
1246
1247     -- co :: x ~ t
1248     subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1249           res binds locals wanteds
1250       = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+>
1251                        ppr eq
1252
1253              -- create the substitution
1254            ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1255                  tySubst = zipOpenTvSubst [tv] [ty]
1256
1257              -- substitute into all other equalities
1258            ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1259            ; res' <- mapM (substEq eq coSubst tySubst) res
1260
1261              -- only substitute local equalities into local dictionaries
1262            ; (lbinds, locals')  <- if not (isWantedCo co)
1263                                    then
1264                                      mapAndUnzipM
1265                                        (substDict eq coSubst tySubst False)
1266                                        locals
1267                                    else
1268                                      return ([], locals)
1269
1270               -- substitute all equalities into wanteds dictionaries
1271            ; (wbinds, wanteds') <- mapAndUnzipM
1272                                      (substDict eq coSubst tySubst True)
1273                                      wanteds
1274
1275            ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1276            ; subst eqs' (eq:res') binds' locals' wanteds'
1277            }
1278
1279     -- co ::^w F t1..tn ~ alpha
1280     subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty,
1281                            rwi_co = co}):eqs)
1282           res binds locals wanteds
1283       | Just tv <- tcGetTyVar_maybe ty
1284       , isMetaTyVar tv
1285       , isWantedCo co
1286       = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+>
1287                        ppr eq
1288
1289              -- create the substitution
1290            ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
1291                  tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]
1292
1293              -- substitute into other wanted equalities (`substEq' makes sure
1294              -- that we only substitute into wanteds)
1295            ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1296            ; res' <- mapM (substEq eq coSubst tySubst) res
1297
1298            ; subst eqs' (eq:res') binds locals wanteds
1299            }
1300
1301     subst (eq:eqs) res binds locals wanteds
1302       = subst eqs (eq:res) binds locals wanteds
1303
1304       -- We have, co :: tv ~ ty
1305       -- => apply [ty/tv] to right-hand side of eq2
1306       --    (but only if tv actually occurs in the right-hand side of eq2
1307       --    and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
1308     substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
1309             coSubst tySubst eq2
1310       |  tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1311       && (isWantedRewriteInst eq2 || not (isWantedCo co))
1312       = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1313                  right2'  = substTy tySubst (rwi_right eq2)
1314                  left2    = case eq2 of
1315                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
1316                               RewriteFam {rwi_fam = fam,
1317                                           rwi_args = args} ->mkTyConApp fam args
1318            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1319            ; case eq2 of
1320                RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1321                  -> occurCheckErr left2 right2'
1322                _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1323            }
1324
1325       -- We have, co ::^w F t1..tn ~ tv
1326       -- => apply [F t1..tn/tv] to eq2
1327       --    (but only if tv actually occurs in eq2
1328       --    and eq2 is a wanted equality
1329       --    and we are either in checking mode or eq2 is a family equality)
1330     substEq (RewriteFam {rwi_args = args, rwi_right = ty})
1331             coSubst tySubst eq2
1332       | Just tv <- tcGetTyVar_maybe ty
1333       , tv `elemVarSet` tyVarsOfRewriteInst eq2
1334       , isWantedRewriteInst eq2
1335       , checkingMode || not (isRewriteVar eq2)
1336       = do { -- substitute into the right-hand side
1337            ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1338                  right2'  = substTy tySubst (rwi_right eq2)
1339                  left2    = case eq2 of
1340                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
1341                               RewriteFam {rwi_fam = fam,
1342                                           rwi_args = args} -> mkTyConApp fam args
1343            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1344            ; case eq2 of
1345                RewriteVar {rwi_var = tv2}
1346                  -- variable equality: perform an occurs check
1347                  | tv2 `elemVarSet` tyVarsOfTypes args
1348                  -> occurCheckErr left2 right2'
1349                  | otherwise
1350                  -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1351                RewriteFam {rwi_fam = fam}
1352                  -- family equality: substitute also into the left-hand side
1353                  -> do { let co1Subst = substTy coSubst left2
1354                              args2'   = substTys tySubst (rwi_args  eq2)
1355                              left2'   = mkTyConApp fam args2'
1356                        ; co2'' <- mkRightTransEqInstCo co2' co1Subst
1357                                                        (left2', right2')
1358                        ; return $ eq2 {rwi_args = args2', rwi_right = right2',
1359                                        rwi_co = co2''}
1360                        }
1361            }
1362
1363       -- unchanged
1364     substEq _ _ _ eq2
1365       = return eq2
1366
1367       -- We have, co :: tv ~ ty
1368       -- => apply [ty/tv] to dictionary predicate
1369       --    (but only if tv actually occurs in the predicate)
1370     substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1371       | isClassDict dict
1372       , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1373       = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1374                  pred'    = substPred tySubst (tci_pred dict)
1375            ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1376            ; return (binds, dict')
1377            }
1378
1379       -- unchanged
1380     substDict _ _ _ _ dict
1381       = return (emptyBag, dict)
1382 -- !!!TODO: Still need to substitute into IP constraints.
1383 \end{code}
1384
1385 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1386 alpha, we record a binding of alpha with t or a, respectively, and for co :=
1387 id.  We do the same for equalities of the form co :: F t1..tn ~ alpha unless
1388 we are in inference mode and alpha appears in the environment - i.e., it is
1389 not a flexible introduced by flattening locals or it is local, but was
1390 propagated into the environment by the instantiation of a variable equality.
1391
1392 We proceed in two phases: (1) first we consider all variable equalities and then
1393 (2) we consider all family equalities.  The two phase structure is required as
1394 the recorded variable equalities determine which skolems flexibles escape, and
1395 hence, which family equalities may be recorded as bindings.
1396
1397 We return all wanted equalities for which we did not generate a binding.
1398 (These can be skolem variable equalities, cyclic variable equalities, and
1399 family equalities.)
1400
1401 We don't update any meta variables.  Instead, instantiation simply implies
1402 putting a type variable binding into the binding pool of TcM.
1403
1404 NB:
1405  * We may encounter filled flexibles due to the instant filling of local
1406    skolems in local-given constraints during flattening.
1407  * Be careful with SigTVs.  They can only be instantiated with other SigTVs or
1408    rigid skolems.
1409
1410 \begin{code}
1411 bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
1412 bindAndExtract eqs checkingMode freeFlexibles
1413   = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
1414                      4 (ppr eqs $$ ppr freeFlexibles)
1415        ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
1416        ; escapingSkolems <- getEscapingSkolems
1417        ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
1418        ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
1419        ; mapM rewriteInstToInst residuals2
1420        }
1421   where
1422     -- NB: we don't have to transitively chase the relation as the substitution
1423     --     process applied before generating the bindings was exhaustive
1424     getEscapingSkolems
1425       = do { tybinds_rel <- getTcTyVarBindsRelation
1426            ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
1427            }
1428       where
1429         isFree (tv, _) = tv `elemVarSet` freeFlexibles
1430
1431         -- co :: alpha ~ t or co :: a ~ alpha
1432     instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1433       = do { flexi_tv1       <- isFlexible   tv1
1434            ; maybe_flexi_tv2 <- isFlexibleTy ty2
1435            ; case (flexi_tv1, maybe_flexi_tv2) of
1436                (True, Just tv2)
1437                  | isSigTyVar tv1 && isSigTyVar tv2
1438                  -> -- co :: alpha ~ beta, where both a SigTvs
1439                     doInst (rwi_swapped eq) tv1 ty2 co eq
1440                (True, Nothing)
1441                  | Just tv2 <- tcGetTyVar_maybe ty2
1442                  , isSigTyVar tv1
1443                  , isSkolemTyVar tv2
1444                  -> -- co :: alpha ~ a, where alpha is a SigTv
1445                     doInst (rwi_swapped eq) tv1 ty2 co eq
1446                (True, _)
1447                  | not (isSigTyVar tv1)
1448                  -> -- co :: alpha ~ t, where alpha is not a SigTv
1449                     doInst (rwi_swapped eq) tv1 ty2 co eq
1450                (False, Just tv2)
1451                  | isSigTyVar tv2
1452                  , isSkolemTyVar tv1
1453                  -> -- co :: a ~ alpha, where alpha is a SigTv
1454                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1455                  | not (isSigTyVar tv2)
1456                  -> -- co :: a ~ alpha, where alpha is not a SigTv
1457                     --                        ('a' may be filled)
1458                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1459                _ -> return $ Just eq
1460            }
1461     instVarEq eq = return $ Just eq
1462
1463         -- co :: F args ~ alpha,
1464         -- and we are either in checking mode or alpha is a skolem flexible that
1465         --     doesn't escape
1466     instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1467                                                rwi_right = ty2, rwi_co = co})
1468       | Just tv2 <- tcGetTyVar_maybe ty2
1469       , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
1470       = do { flexi_tv2 <- isFlexible tv2
1471            ; if flexi_tv2
1472              then
1473                doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1474              else
1475                return $ Just eq
1476            }
1477     instFamEq _ eq = return $ Just eq
1478
1479     -- tv is a meta var, but not a SigTV and not filled
1480     isFlexible tv
1481       | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
1482       | otherwise      = return False
1483
1484     -- type is a tv that is a meta var, but not a SigTV and not filled
1485     isFlexibleTy ty
1486       | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
1487                                             ; if flexi then return $ Just tv
1488                                                        else return Nothing
1489                                             }
1490       | otherwise                      = return Nothing
1491
1492     doInst _swapped _tv _ty (Right ty) _eq
1493       = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1494     doInst swapped tv ty (Left cotv) eq
1495       = do { lookupTV <- lookupTcTyVar tv
1496            ; bMeta swapped tv lookupTV ty cotv
1497            }
1498       where
1499         -- Try to create a binding for a meta variable.  There is *no* need to
1500         -- consider reorienting the underlying equality; `checkOrientation'
1501         -- makes sure that we get variable-variable equalities only in the
1502         -- appropriate orientation.
1503         --
1504         bMeta :: Bool                    -- is this a swapped equality?
1505               -> TcTyVar                 -- tyvar to instantiate
1506               -> LookupTyVarResult       -- lookup result of that tyvar
1507               -> TcType                  -- to to instantiate tyvar with
1508               -> TcTyVar                 -- coercion tyvar of current equality
1509               -> TcM (Maybe RewriteInst) -- returns the original equality if
1510                                          -- the tyvar could not be instantiated,
1511                                          -- and hence, the equality must be kept
1512
1513         -- meta variable has been filled already
1514         -- => this should never happen due to the use of `isFlexible' above
1515         bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1516           = pprPanic "TcTyFuns.bMeta" $
1517               ptext (sLit "flexible") <+> ppr tv <+>
1518               ptext (sLit "already filled with") <+> ppr fill_ty <+>
1519               ptext (sLit "meant to fill with") <+> ppr ty
1520
1521         -- type variable meets type variable
1522         -- => `checkOrientation' already ensures that it is fine to instantiate
1523         --    tv1 with tv2, but chase tv2's instantiations if necessary, so that
1524         --    we eventually can perform a kinds check in bMetaInst
1525         -- NB: tv's instantiations won't alter the orientation in which we
1526         --     want to instantiate as they either constitute a family
1527         --     application or are themselves due to a properly oriented
1528         --     instantiation
1529         bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
1530           = do { lookupTV2 <- lookupTcTyVar tv2
1531                ; case lookupTV2 of
1532                    IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
1533                    DoneTv _       -> bMetaInst swapped tv1 ty cotv
1534                }
1535
1536         -- updatable meta variable meets non-variable type
1537         -- => occurs check, monotype check, and kinds match check, then bind
1538         bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
1539           = bMetaInst swapped tv non_tv_ty cotv
1540
1541         bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
1542
1543         -- We know `tv' can be instantiated; check that `ty' is alright for
1544         -- instantiating `tv' with and then record a binding; we return the
1545         -- original equality if it is cyclic through a synonym family
1546         bMetaInst swapped tv ty cotv
1547           = do {   -- occurs + monotype check
1548                ; mb_ty' <- checkTauTvUpdate tv ty
1549
1550                ; case mb_ty' of
1551                    Nothing  ->
1552                      -- there may be a family in non_tv_ty due to an unzonked,
1553                      -- but updated skolem for a local equality
1554                      -- (cf `wantedToLocal')
1555                      return $ Just eq
1556                    Just ty' ->
1557                      do { checkKinds swapped tv ty'
1558                         ; bindMetaTyVar tv ty'          -- bind meta var
1559                         ; bindMetaTyVar cotv ty'        -- bind co var
1560                         ; return Nothing
1561                         }
1562                }
1563 \end{code}
1564
1565
1566 %************************************************************************
1567 %*                                                                      *
1568 \section{Errors}
1569 %*                                                                      *
1570 %************************************************************************
1571
1572 The infamous couldn't match expected type soandso against inferred type
1573 somethingdifferent message.
1574
1575 \begin{code}
1576 eqInstMisMatch :: Inst -> TcM a
1577 eqInstMisMatch inst
1578   = ASSERT( isEqInst inst )
1579     setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1580   where
1581     (ty_act, ty_exp) = eqInstTys inst
1582     InstLoc _ _ ctxt = instLoc   inst
1583
1584 -----------------------
1585 failWithMisMatch :: TcType -> TcType -> TcM a
1586 -- Generate the message when two types fail to match,
1587 -- going to some trouble to make it helpful.
1588 -- The argument order is: actual type, expected type
1589 failWithMisMatch ty_act ty_exp
1590   = do  { env0 <- tcInitTidyEnv
1591         ; ty_exp <- zonkTcType ty_exp
1592         ; ty_act <- zonkTcType ty_act
1593         ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1594         }
1595
1596 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1597 misMatchMsg env0 (ty_act, ty_exp)
1598   = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1599         (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1600         msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1601                         nest 7 $
1602                               ptext (sLit "against inferred type") <+> pp_act],
1603                    nest 2 (extra_exp $$ extra_act),
1604                    nest 2 (vcat (map pp_open_tc (nub open_tcs)))]
1605                         -- See Note [Non-injective type functions]
1606     in
1607     (env2, msg)
1608
1609   where
1610     open_tcs = [tc | TyConApp tc _ <- [ty_act, ty_exp]
1611                    , isOpenTyCon tc ]
1612     pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc)
1613                     <+> ptext (sLit "is a type function") <> pp_inj
1614         where
1615           pp_inj | isInjectiveTyCon tc = empty
1616                  | otherwise = ptext (sLit (", and may not be injective"))
1617
1618     ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1619     ppr_ty env ty
1620       = let (env1, tidy_ty) = tidyOpenType env ty
1621             (env2, extra)  = ppr_extra env1 tidy_ty
1622         in
1623         (env2, quotes (ppr tidy_ty), extra)
1624
1625     -- (ppr_extra env ty) shows extra info about 'ty'
1626     ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1627     ppr_extra env (TyVarTy tv)
1628       | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1629       = (env1, pprSkolTvBinding tv1)
1630       where
1631         (env1, tv1) = tidySkolemTyVar env tv
1632
1633     ppr_extra env _ty = (env, empty)            -- Normal case
1634 \end{code}
1635
1636 Note [Non-injective type functions]
1637 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1638 It's very confusing to get a message like
1639      Couldn't match expected type `Depend s'
1640             against inferred type `Depend s1'
1641 so pp_open_tc adds:
1642        NB: `Depend' is type function, and hence may not be injective
1643
1644 Currently we add this independently for each argument, so we also get
1645      Couldn't match expected type `a'
1646             against inferred type `Dual (Dual a)'
1647        NB: `Dual' is a (non-injective) type function
1648 which is arguably redundant.  But on the other hand, it's probably
1649 a good idea for the programmer to know the error involves type functions
1650 so I've left it in for now.  The obvious alternative is to only add
1651 this NB in the case of matching (T ...) ~ (T ...).
1652
1653
1654 Warn of loopy local equalities that were dropped.
1655
1656 \begin{code}
1657 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1658 warnDroppingLoopyEquality ty1 ty2
1659   = do { env0 <- tcInitTidyEnv
1660        ; ty1 <- zonkTcType ty1
1661        ; ty2 <- zonkTcType ty2
1662        ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1663              (_env2, tidy_ty2) = tidyOpenType env1 ty2
1664        ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1665                        2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))
1666        }
1667 \end{code}