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         tcNormaliseFamInst,
   7
   8         normaliseGivenEqs, normaliseGivenDicts,
   9         normaliseWantedEqs, normaliseWantedDicts,
  10         solveWantedEqs,
  11         substEqInDictInsts,
  12
  13         -- errors
  14         eqInstMisMatch, misMatchMsg,
  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 Var
  35 import Name
  36 import Bag
  37 import Outputable
  38 import SrcLoc   ( Located(..) )
  39 import Maybes
  40
  41 -- standard
  42 import Data.List
  43 import Control.Monad (liftM)
  44 \end{code}
  45
  46
  47 %************************************************************************
  48 %*                                                                      *
  49                 Normalisation of types
  50 %*                                                                      *
  51 %************************************************************************
  52
  53 Unfold a single synonym family instance and yield the witnessing coercion.
  54 Return 'Nothing' if the given type is either not synonym family instance
  55 or is a synonym family instance that has no matching instance declaration.
  56 (Applies only if the type family application is outermost.)
  57
  58 For example, if we have
  59
  60   :Co:R42T a :: T [a] ~ :R42T a
  61
  62 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
  63
  64 \begin{code}
  65 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
  66 tcUnfoldSynFamInst (TyConApp tycon tys)
  67   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
  68   = return Nothing
  69   | otherwise
  70   = do { -- we only use the indexing arguments for matching,
  71          -- not the additional ones
  72        ; maybeFamInst <- tcLookupFamInst tycon idxTys
  73        ; case maybeFamInst of
  74            Nothing                -> return Nothing
  75            Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
  76                                                     mkTyConApp coe_tc tys')
  77              where
  78                tys'   = rep_tys ++ restTys
  79                coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
  80                                    (tyConFamilyCoercion_maybe rep_tc)
  81        }
  82     where
  83         n                = tyConArity tycon
  84         (idxTys, restTys) = splitAt n tys
  85 tcUnfoldSynFamInst _other = return Nothing
  86 \end{code}
  87
  88 Normalise 'Type's and 'PredType's by unfolding type family applications where
  89 possible (ie, we treat family instances as a TRS).  Also zonk meta variables.
  90
  91         tcNormaliseFamInst ty = (co, ty')
  92         then   co : ty ~ ty'
  93
  94 \begin{code}
  95 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
  96 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
  97
  98 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
  99 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
 100 \end{code}
 101
 102 Normalise a type relative to the rewrite rule implied by one EqInst or an
 103 already unpacked EqInst (ie, an equality rewrite rule).
 104
 105 \begin{code}
 106 -- Rewrite by EqInst
 107 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, Type)
 108 tcEqInstNormaliseFamInst inst =
 109   ASSERT( isEqInst inst )
 110   tcEqRuleNormaliseFamInst (pat, rhs, co)
 111   where
 112     pat = eqInstLeftTy  inst
 113     rhs = eqInstRightTy inst
 114     co  = eqInstType    inst
 115
 116 -- Rewrite by equality rewrite rule
 117 tcEqRuleNormaliseFamInst :: (TcType,   -- rewrite rule lhs
 118                              TcType,   -- rewrite rule rhs
 119                              TcType)   -- coercion witnessing the rewrite rule
 120                           -> TcType    -- type to rewrite
 121                           -> TcM (CoercionI, Type)
 122 tcEqRuleNormaliseFamInst (pat, rhs, co) ty
 123   = tcGenericNormaliseFamInst matchEqRule ty
 124   where
 125     matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
 126                     | otherwise          = return $ Nothing
 127 \end{code}
 128
 129 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
 130 apply the normalisation function gives as the first argument to every TyConApp
 131 and every TyVarTy subterm.
 132
 133         tcGenericNormaliseFamInst fun ty = (co, ty')
 134         then   co : ty ~ ty'
 135
 136 This function is (by way of using smart constructors) careful to ensure that
 137 the returned coercion is exactly IdCo (and not some semantically equivalent,
 138 but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
 139 makes it easy for the caller to determine whether the type changed.  BUT
 140 even if we return IdCo, ty' may be *syntactically* different from ty due to
 141 unfolded closed type synonyms (by way of tcCoreView).  In the interest of
 142 good error messages, callers should discard ty' in favour of ty in this case.
 143
 144 \begin{code}
 145 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
 146                              -- what to do with type functions and tyvars
 147                            -> TcType                    -- old type
 148                            -> TcM (CoercionI, TcType)   -- (coercion, new type)
 149 tcGenericNormaliseFamInst fun ty
 150   | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
 151 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
 152   = do  { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 153         ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
 154         ; maybe_ty_co <- fun (mkTyConApp tyCon ntys)     -- use normalised args!
 155         ; case maybe_ty_co of
 156             -- a matching family instance exists
 157             Just (ty', co) ->
 158               do { let first_coi = mkTransCoI tycon_coi (ACo co)
 159                  ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
 160                  ; let fix_coi = mkTransCoI first_coi rest_coi
 161                  ; return (fix_coi, nty)
 162                  }
 163             -- no matching family instance exists
 164             -- we do not do anything
 165             Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
 166         }
 167 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
 168   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 169         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
 170         ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
 171         }
 172 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
 173   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 174         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
 175         ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
 176         }
 177 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
 178   = do  { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
 179         ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
 180         }
 181 tcGenericNormaliseFamInst fun (NoteTy note ty1)
 182   = do  { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
 183         ; return (mkNoteTyCoI note coi, NoteTy note nty1)
 184         }
 185 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
 186   | isTcTyVar tv
 187   = do  { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
 188         ; res <- lookupTcTyVar tv
 189         ; case res of
 190             DoneTv _ ->
 191               do { maybe_ty' <- fun ty
 192                  ; case maybe_ty' of
 193                      Nothing         -> return (IdCo, ty)
 194                      Just (ty', co1) ->
 195                        do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
 196                           ; return (ACo co1 `mkTransCoI` coi2, ty'')
 197                           }
 198                  }
 199             IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
 200         }
 201   | otherwise
 202   = return (IdCo, ty)
 203 tcGenericNormaliseFamInst fun (PredTy predty)
 204   = do  { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
 205         ; return (coi, PredTy pred') }
 206
 207 ---------------------------------
 208 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
 209                               -> TcPredType
 210                               -> TcM (CoercionI, TcPredType)
 211
 212 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
 213   = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 214        ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
 215        }
 216 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
 217   = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
 218        ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
 219        }
 220 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
 221   = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
 222        ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
 223        ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
 224 \end{code}
 225
 226
 227 %************************************************************************
 228 %*                                                                      *
 229 \section{Normalisation of equality constraints}
 230 %*                                                                      *
 231 %************************************************************************
 232
 233 Note [Inconsistencies in equality constraints]
 234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 235 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
 236 equalities that if presented to the unifer in TcUnify would result in an
 237 error) during normalisation of wanted constraints.  This is especially so that
 238 we don't solve wanted constraints under an inconsistent given set.  In
 239 particular, we don't want to permit signatures, such as
 240
 241   bad :: (Int ~ Bool => Int) -> a -> a
 242
 243 \begin{code}
 244 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
 245 normaliseGivenEqs givens
 246  = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
 247       ; (result, deSkolem) <-
 248           rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
 249             [ ("(ZONK)",    dontRerun $ zonkInsts)
 250             , ("(TRIVIAL)", dontRerun $ trivialRule)
 251             , ("(DECOMP)",  decompRule)
 252             , ("(TOP)",     topRule)
 253             , ("(SUBST)",   substRule)                   -- incl. occurs check
 254             ] givens
 255       ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
 256       ; return (result, deSkolem)
 257       }
 258 \end{code}
 259
 260 \begin{code}
 261 normaliseWantedEqs :: [Inst] -> TcM [Inst]
 262 normaliseWantedEqs insts
 263   = do { traceTc (text "normaliseWantedEqs <-" <+> ppr insts)
 264        ; result <- liftM fst $ rewriteToFixedPoint Nothing
 265                      [ ("(ZONK)",    dontRerun $ zonkInsts)
 266                      , ("(TRIVIAL)", dontRerun $ trivialRule)
 267                      , ("(DECOMP)",  decompRule)
 268                      , ("(TOP)",     topRule)
 269                      , ("(UNIFY)",   unifyMetaRule)      -- incl. occurs check
 270                      , ("(SUBST)",   substRule)          -- incl. occurs check
 271                      ] insts
 272        ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
 273        ; return result
 274        }
 275 \end{code}
 276
 277
 278 %************************************************************************
 279 %*                                                                      *
 280 \section{Solving of wanted constraints with respect to a given set}
 281 %*                                                                      *
 282 %************************************************************************
 283
 284 The set of given equalities must have been normalised already.
 285
 286 \begin{code}
 287 solveWantedEqs :: [Inst]        -- givens
 288              -> [Inst]          -- wanteds
 289              -> TcM [Inst]      -- irreducible wanteds
 290 solveWantedEqs givens wanteds
 291   = do { traceTc $ text "solveWantedEqs <-" <+> ppr wanteds <+> text "with" <+>
 292                    ppr givens
 293        ; result <- liftM fst $ rewriteToFixedPoint Nothing
 294                      [ ("(ZONK)",    dontRerun $ zonkInsts)
 295                      , ("(TRIVIAL)", dontRerun $ trivialRule)
 296                      , ("(DECOMP)",  decompRule)
 297                      , ("(TOP)",     topRule)
 298                      , ("(GIVEN)",   substGivens givens) -- incl. occurs check
 299                      , ("(UNIFY)",   unifyMetaRule)      -- incl. occurs check
 300                      ] wanteds
 301        ; traceTc (text "solveWantedEqs ->" <+> ppr result)
 302        ; return result
 303        }
 304   where
 305     -- Use `substInst' with every given on all the wanteds.
 306     substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
 307     substGivens []     wanteds = return (wanteds, False)
 308     substGivens (g:gs) wanteds
 309       = do { (wanteds1, changed1) <- substGivens gs wanteds
 310            ; (wanteds2, changed2) <- substInst g wanteds1
 311            ; return (wanteds2, changed1 || changed2)
 312            }
 313 \end{code}
 314
 315
 316 %************************************************************************
 317 %*                                                                      *
 318 \section{Normalisation of non-equality dictionaries}
 319 %*                                                                      *
 320 %************************************************************************
 321
 322 \begin{code}
 323 normaliseGivenDicts, normaliseWantedDicts
 324         :: [Inst]               -- given equations
 325         -> [Inst]               -- dictionaries
 326         -> TcM ([Inst],TcDictBinds)
 327
 328 normaliseGivenDicts  eqs dicts = normalise_dicts eqs dicts False
 329 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
 330
 331 normalise_dicts
 332         :: [Inst]       -- given equations
 333         -> [Inst]       -- dictionaries
 334         -> Bool         -- True <=> the dicts are wanted
 335                         -- Fals <=> they are given
 336         -> TcM ([Inst],TcDictBinds)
 337 normalise_dicts given_eqs dicts is_wanted
 338   = do  { traceTc $ text "normalise???Dicts <-" <+> ppr dicts <+>
 339                     text "with" <+> ppr given_eqs
 340         ; (dicts0, binds0)  <- normaliseInsts is_wanted dicts
 341         ; (dicts1, binds1)  <- substEqInDictInsts given_eqs dicts0
 342         ; let binds01 = binds0 `unionBags` binds1
 343         ; if isEmptyBag binds1
 344           then return (dicts1, binds01)
 345           else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
 346                   ; return (dicts2, binds01 `unionBags` binds2) } }
 347 \end{code}
 348
 349
 350 %************************************************************************
 351 %*                                                                      *
 352 \section{Normalisation rules and iterative rule application}
 353 %*                                                                      *
 354 %************************************************************************
 355
 356 We have three kinds of normalising rewrite rules:
 357
 358 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
 359     whether any changes occurred during rewriting that necessitate re-running
 360     the current rule set.
 361
 362 (2) Precondition rules that rewrite a set of insts and return a monadic action
 363     that reverts the effect of preconditioning.
 364
 365 (3) Idempotent normalisation rules that never require re-running the rule set.
 366
 367 \begin{code}
 368 type RewriteRule     = [Inst] -> TcM ([Inst], Bool)   -- rewrite, maybe re-run
 369 type PrecondRule     = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
 370 type IdemRewriteRule = [Inst] -> TcM [Inst]           -- rewrite, don't re-run
 371
 372 type NamedRule       = (String, RewriteRule)          -- rule with description
 373 type NamedPreRule    = (String, PrecondRule)          -- precond with desc
 374 \end{code}
 375
 376 Template lifting idempotent rules to full rules (which can be put into a rule
 377 set).
 378
 379 \begin{code}
 380 dontRerun :: IdemRewriteRule -> RewriteRule
 381 dontRerun rule insts = liftM addFalse $ rule insts
 382   where
 383     addFalse x = (x, False)
 384 \end{code}
 385
 386 The following function applies a set of rewrite rules until a fixed point is
 387 reached; i.e., none of the `RewriteRule's require re-running the rule set.
 388 Optionally, there may be a pre-conditing rule that is applied before any other
 389 rules are applied and before the rule set is re-run.
 390
 391 The result is the set of rewritten (i.e., normalised) insts and, in case of a
 392 pre-conditing rule, a monadic action that reverts the effects of
 393 pre-conditioning - specifically, this is removing introduced skolems.
 394
 395 \begin{code}
 396 rewriteToFixedPoint :: Maybe NamedPreRule   -- optional preconditioning rule
 397                     -> [NamedRule]          -- rule set
 398                     -> [Inst]               -- insts to rewrite
 399                     -> TcM ([Inst], TcM ())
 400 rewriteToFixedPoint precondRule rules insts
 401   = completeRewrite (return ()) precondRule insts
 402   where
 403     completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
 404                     -> TcM ([Inst], TcM ())
 405     completeRewrite dePrecond (Just (precondName, precond)) insts
 406       = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
 407            ; (insts', dePrecond') <- precond insts
 408            ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
 409            ; tryRules (dePrecond >> dePrecond') rules insts'
 410            }
 411     completeRewrite dePrecond Nothing insts
 412       = tryRules dePrecond rules insts
 413
 414     tryRules dePrecond _                    []    = return ([]   , dePrecond)
 415     tryRules dePrecond []                   insts = return (insts, dePrecond)
 416     tryRules dePrecond ((name, rule):rules) insts
 417       = do { traceTc $ text name <+> text " <- " <+> ppr insts
 418            ; (insts', rerun) <- rule insts
 419            ; traceTc $ text name <+> text " -> " <+> ppr insts'
 420            ; if rerun then completeRewrite dePrecond precondRule insts'
 421                       else tryRules dePrecond rules insts'
 422            }
 423 \end{code}
 424
 425
 426 %************************************************************************
 427 %*                                                                      *
 428 \section{Different forms of Inst rewrite rules}
 429 %*                                                                      *
 430 %************************************************************************
 431
 432 Splitting of non-terminating given constraints: skolemOccurs
 433 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 434 This is a preconditioning rule exclusively applied to given constraints.
 435 Moreover, its rewriting is only temporary, as it is undone by way of
 436 side-effecting mutable type variables after simplification and constraint
 437 entailment has been completed.
 438
 439 This version is an (attempt at, yet unproven, an) *unflattened* version of
 440 the SubstL-Ev completion rule.
 441
 442 The above rule is essential to catch non-terminating rules that cannot be
 443 oriented properly, like
 444
 445      F a ~ [G (F a)]
 446  or even
 447      a ~ [G a]
 448
 449 The left-to-right orientiation is not suitable because it does not
 450 terminate. The right-to-left orientation is not suitable because it
 451 does not have a type-function on the left. This is undesirable because
 452 it would hide information. E.g. assume
 453
 454         instance C [x]
 455
 456 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
 457 see that the C [x] instance applies.
 458
 459 The rule also caters for badly-oriented rules of the form:
 460
 461      F a ~ G (F a)
 462
 463 for which other solutions are possible, but this one will do too.
 464
 465 It's behavior is:
 466
 467   co : ty1 ~ ty2{F ty1}
 468      >-->
 469   co         : ty1 ~ ty2{b}
 470   sym (F co) : F ty2{b} ~ b
 471         where b is a fresh skolem variable
 472
 473 We also cater for the symmetric situation *if* the rule cannot be used as a
 474 left-to-right rewrite rule.
 475
 476 We also return an action (b := ty1) which is used to eliminate b
 477 after the dust of normalisation with the completed rewrite system
 478 has settled.
 479
 480 A subtle point of this transformation is that both coercions in the results
 481 are strictly speaking incorrect.  However, they are correct again after the
 482 action {B := ty1} has removed the skolem again.  This happens immediately
 483 after constraint entailment has been checked; ie, code outside of the
 484 simplification and entailment checking framework will never see these
 485 temporarily incorrect coercions.
 486
 487 NB: We perform this transformation for multiple occurences of ty1 under one
 488     or multiple family applications on the left-hand side at once (ie, the
 489     rule doesn't need to be applied multiple times at a single inst).  As a
 490     result we can get two or more insts back.
 491
 492 \begin{code}
 493 skolemOccurs :: PrecondRule
 494 skolemOccurs insts
 495   = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
 496        ; return (concat instss, sequence_ undoSkolems)
 497        }
 498   where
 499     oneSkolemOccurs inst
 500       = ASSERT( isEqInst inst )
 501         isRewriteRule (eqInstLeftTy inst) (eqInstRightTy inst)
 502       where
 503
 504         -- look through synonyms
 505         isRewriteRule ty1 ty2 | Just ty1' <- tcView ty1 = isRewriteRule ty1' ty2
 506         isRewriteRule ty1 ty2 | Just ty2' <- tcView ty2 = isRewriteRule ty1 ty2'
 507
 508         -- left-to-right rule with type family head
 509         isRewriteRule ty1@(TyConApp con _) ty2
 510           | isOpenSynTyCon con
 511           = breakRecursion ty1 ty2 False    -- not swapped
 512
 513         -- left-to-right rule with type variable head
 514         isRewriteRule ty1@(TyVarTy _) ty2
 515           = breakRecursion ty1 ty2 False    -- not swapped
 516
 517         -- right-to-left rule with type family head
 518         isRewriteRule ty1 ty2@(TyConApp con _)
 519           | isOpenSynTyCon con
 520           = breakRecursion ty2 ty1 True     -- swapped
 521
 522         -- right-to-left rule with type variable head
 523         isRewriteRule ty1 ty2@(TyVarTy _)
 524           = breakRecursion ty2 ty1 True     -- swapped
 525
 526         -- this equality is not a rewrite rule => ignore
 527         isRewriteRule _ _ = return ([inst], return ())
 528
 529
 530         breakRecursion pat body swapped
 531           | null tysToLiftOut
 532           = return ([inst], return ())
 533           | otherwise
 534           = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
 535                ; let skTvs_tysTLO   = zip skTvs tysToLiftOut
 536                      insertSkolems = return . replace skTvs_tysTLO
 537                ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
 538                ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
 539                                      else mkEqInst (EqPred pat body') co
 540                                      -- ensure to reconstruct the inst in the
 541                                      -- original orientation
 542                ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
 543                                                  skTvs_tysTLO
 544                ; return (inst':insts, sequence_ undoSk)
 545                }
 546           where
 547             co  = eqInstCoercion inst
 548
 549             -- all subtypes that are (1) type family instances and (2) contain
 550             -- the lhs type as part of the type arguments of the type family
 551             -- constructor
 552             tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
 553                                               , any (pat `tcPartOfType`) tys]
 554
 555             replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
 556             replace []                   _  = Nothing
 557             replace ((skTv, tyTLO):rest) ty
 558               | tyTLO `tcEqType` ty         = Just (mkTyVarTy skTv, undefined)
 559               | otherwise                   = replace rest ty
 560
 561             -- create the EqInst for the equality determining the skolem and a
 562             -- TcM action undoing the skolem introduction
 563             mkSkolemInst inst' (skTv, tyTLO)
 564               = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
 565                    ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
 566                                       (mkGivenCo $ mkSymCoercion (fromACo co))
 567                    ; return (inst, writeMetaTyVar skTv tyTLO)
 568                    }
 569 \end{code}
 570
 571
 572 Removal of trivial equalities: trivialRule
 573 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 574 The following rules exploits the reflexivity of equality:
 575
 576   (Trivial)
 577     g1 : t ~ t
 578       >-->
 579     g1 := t
 580
 581 \begin{code}
 582 trivialRule :: IdemRewriteRule
 583 trivialRule insts
 584   = liftM catMaybes $ mappM trivial insts
 585   where
 586     trivial inst
 587       | ASSERT( isEqInst inst )
 588         ty1 `tcEqType` ty2
 589       = do { eitherEqInst inst
 590                (\cotv -> writeMetaTyVar cotv ty1)
 591                (\_    -> return ())
 592            ; return Nothing
 593            }
 594       | otherwise
 595       = return $ Just inst
 596       where
 597          ty1 = eqInstLeftTy  inst
 598          ty2 = eqInstRightTy inst
 599 \end{code}
 600
 601
 602 Decomposition of data type constructors: decompRule
 603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 604 Whenever, the same *data* constructors occurs on both sides of an equality, we
 605 can decompose as in standard unification.
 606
 607   (Decomp)
 608     g1 : T cs ~ T ds
 609       >-->
 610     g21 : c1 ~ d1, ..., g2n : cn ~ dn
 611     g1 := T g2s
 612
 613 Works also for the case where T is actually an application of a type family
 614 constructor to a set of types, provided the applications on both sides of the
 615 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
 616
 617 We guarantee to raise an error for any inconsistent equalities;
 618 cf Note [Inconsistencies in equality constraints].
 619
 620 \begin{code}
 621 decompRule :: RewriteRule
 622 decompRule insts
 623   = do { (insts, changed) <- mapAndUnzipM decomp insts
 624        ; return (concat insts, or changed)
 625        }
 626   where
 627     decomp inst
 628       = ASSERT( isEqInst inst )
 629         go (eqInstLeftTy inst) (eqInstRightTy inst)
 630       where
 631         go ty1 ty2
 632           | Just ty1' <- tcView ty1 = go ty1' ty2
 633           | Just ty2' <- tcView ty2 = go ty1 ty2'
 634
 635         go (TyConApp con1 tys1) (TyConApp con2 tys2)
 636           | con1 == con2 && identicalHead
 637           = mkArgInsts (mkTyConApp con1) tys1 tys2
 638
 639           | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
 640             -- not matching data constructors (of any flavour) are bad news
 641           = eqInstMisMatch inst
 642           where
 643             n             = tyConArity con1
 644             (idxTys1, _)  = splitAt n tys1
 645             (idxTys2, _)  = splitAt n tys2
 646             identicalHead = not (isOpenSynTyCon con1) ||
 647                             idxTys1 `tcEqTypes` idxTys2
 648
 649         go (FunTy fun1 arg1) (FunTy fun2 arg2)
 650           = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
 651                                                                 [fun2, arg2]
 652
 653         -- Applications need a bit of care!
 654         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 655         go (AppTy s1 t1) ty2
 656           | Just (s2, t2) <- tcSplitAppTy_maybe ty2
 657           = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
 658
 659         -- Symmetric case
 660         go ty1 (AppTy s2 t2)
 661           | Just (s1, t1) <- tcSplitAppTy_maybe ty1
 662           = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
 663
 664         -- We already covered all the consistent cases of rigid types on both
 665         -- sides; so, if we see two rigid types here, we discovered an
 666         -- inconsistency.
 667         go ty1 ty2
 668           | isRigid ty1 && isRigid ty2
 669           = eqInstMisMatch inst
 670
 671         -- We can neither assert consistency nor inconsistency => defer
 672         go _ _ = return ([inst], False)
 673
 674         isRigid (TyConApp con _) = not (isOpenSynTyCon con)
 675         isRigid (FunTy _ _)      = True
 676         isRigid (AppTy _ _)      = True
 677         isRigid _                = False
 678
 679         -- Create insts for matching argument positions (ie, the bit after
 680         -- '>-->' in the rule description above)
 681         mkArgInsts con tys1 tys2
 682           = do { cos <- eitherEqInst inst
 683                           -- old_co := Con1 cos
 684                           (\old_covar ->
 685                             do { cotvs <- zipWithM newMetaCoVar tys1 tys2
 686                                ; let cos = map mkTyVarTy cotvs
 687                                ; writeMetaTyVar old_covar (con cos)
 688                                ; return $ map mkWantedCo cotvs
 689                                })
 690                           -- co_i := Con_i old_co
 691                           (\old_co ->
 692                             return $ map mkGivenCo $
 693                                          mkRightCoercions (length tys1) old_co)
 694                ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
 695                ; traceTc (text "decomp identicalHead" <+> ppr insts)
 696                ; return (insts, not $ null insts)
 697                }
 698 \end{code}
 699
 700
 701 Rewriting with type instances: topRule
 702 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 703 We use (toplevel) type instances to normalise both sides of equalities.
 704
 705   (Top)
 706     g1 : t ~ s
 707       >--> co1 :: t ~ t' / co2 :: s ~ s'
 708     g2 : t' ~ s'
 709     g1 := co1 * g2 * sym co2
 710
 711 \begin{code}
 712 topRule :: RewriteRule
 713 topRule insts
 714   =  do { (insts, changed) <- mapAndUnzipM top insts
 715         ; return (insts, or changed)
 716         }
 717   where
 718     top inst
 719       = ASSERT( isEqInst inst )
 720         do { (coi1, ty1') <- tcNormaliseFamInst ty1
 721            ; (coi2, ty2') <- tcNormaliseFamInst ty2
 722            ; case (coi1, coi2) of
 723                (IdCo, IdCo) -> return (inst, False)
 724                _            ->
 725                  do { wg_co <-
 726                        eitherEqInst inst
 727                          -- old_co = co1 * new_co * sym co2
 728                          (\old_covar ->
 729                            do { new_cotv <- newMetaCoVar ty1' ty2'
 730                               ; let new_co  = mkTyVarTy new_cotv
 731                                     old_coi = coi1 `mkTransCoI`
 732                                               ACo new_co `mkTransCoI`
 733                                               (mkSymCoI coi2)
 734                               ; writeMetaTyVar old_covar (fromACo old_coi)
 735                               ; return $ mkWantedCo new_cotv
 736                               })
 737                          -- new_co = sym co1 * old_co * co2
 738                          (\old_co ->
 739                            return $
 740                              mkGivenCo $
 741                                fromACo $
 742                                  mkSymCoI coi1 `mkTransCoI`
 743                                  ACo old_co `mkTransCoI` coi2)
 744                    ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
 745                    ; return (new_inst, True)
 746                    }
 747              }
 748       where
 749         ty1 = eqInstLeftTy  inst
 750         ty2 = eqInstRightTy inst
 751 \end{code}
 752
 753
 754 Rewriting with equalities: substRule
 755 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 756 From a set of insts, use all insts that can be read as rewrite rules to
 757 rewrite the types in all other insts.
 758
 759   (Subst)
 760     g : F c ~ t,
 761     forall g1 : s1{F c} ~ s2{F c}
 762       >-->
 763     g2 : s1{t} ~ s2{t}
 764     g1 := s1{g} * g2  * sym s2{g}  <=>  g2 := sym s1{g} * g1 * s2{g}
 765
 766 Alternatively, the rewrite rule may have the form (g : a ~ t).
 767
 768 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
 769 where t is neither a variable nor a type family application, we use them for
 770 rewriting from right-to-left.  However, it is crucial to only apply rules
 771 from right-to-left if they cannot be used left-to-right.
 772
 773 The workhorse is substInst, which performs an occurs check before actually
 774 using an equality for rewriting.  If the type pattern occurs in the type we
 775 substitute for the pattern, normalisation would diverge.
 776
 777 \begin{code}
 778 substRule :: RewriteRule
 779 substRule insts = tryAllInsts insts []
 780   where
 781     -- for every inst check whether it can be used to rewrite the others
 782     -- (we make an effort to keep the insts in order; it makes debugging
 783     -- easier)
 784     tryAllInsts []           triedInsts = return (reverse triedInsts, False)
 785     tryAllInsts (inst:insts) triedInsts
 786       = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
 787            ; if changed then return (insertAt (length triedInsts) inst insts',
 788                                      True)
 789                         else tryAllInsts insts (inst:triedInsts)
 790            }
 791       where
 792         insertAt n x xs = let (xs1, xs2) = splitAt n xs
 793                           in xs1 ++ [x] ++ xs2
 794
 795 -- Use the given inst as a rewrite rule to normalise the insts in the second
 796 -- argument.  Don't do anything if the inst cannot be used as a rewrite rule,
 797 -- but do apply it right-to-left, if possible, and if it cannot be used
 798 -- left-to-right.
 799 --
 800 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
 801 substInst inst insts
 802   = ASSERT( isEqInst inst )
 803     go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
 804   where
 805     -- look through synonyms
 806     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
 807     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
 808
 809     -- rewrite type family applications
 810     go ty1@(TyConApp con _) ty2 co
 811       | isOpenSynTyCon con
 812       = substEquality (ty1, ty2, co) insts
 813
 814     -- rewrite skolems
 815     go ty1@(TyVarTy tv) ty2 co
 816       | isSkolemTyVar tv
 817       = substEquality (ty1, ty2, co) insts
 818
 819     -- rewrite type family applications from right-to-left, only after
 820     -- having checked whether we can work left-to-right
 821     go ty1 ty2@(TyConApp con _) co
 822       | isOpenSynTyCon con
 823       = substEquality (ty2, ty1, mkSymCoercion co) insts
 824
 825     -- rewrite skolems from right-to-left, only after having checked
 826     -- whether we can work left-to-right
 827     go ty1 ty2@(TyVarTy tv) co
 828       | isSkolemTyVar tv
 829       = substEquality (ty2, ty1, mkSymCoercion co) insts
 830
 831     go _ _ _ = return (insts, False)
 832
 833     substEquality :: (TcType,   -- rewrite rule lhs
 834                       TcType,   -- rewrite rule rhs
 835                       TcType)   -- coercion witnessing the rewrite rule
 836                   -> [Inst]     -- insts to rewrite
 837                   -> TcM ([Inst], Bool)
 838     substEquality eqRule@(pat, rhs, _) insts
 839       | pat `tcPartOfType` rhs      -- occurs check!
 840       = occurCheckErr pat rhs
 841       | otherwise
 842       = do { (insts', changed) <- mapAndUnzipM substOne insts
 843            ; return (insts', or changed)
 844            }
 845       where
 846         substOne inst
 847           = ASSERT( isEqInst inst )
 848             do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
 849                ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
 850                ; case (coi1, coi2) of
 851                 (IdCo, IdCo) -> return (inst, False)
 852                 _            ->
 853                   do { gw_co <-
 854                          eitherEqInst inst
 855                            -- old_co := co1 * new_co * sym co2
 856                            (\old_covar ->
 857                              do { new_cotv <- newMetaCoVar ty1' ty2'
 858                                 ; let new_co  = mkTyVarTy new_cotv
 859                                       old_coi = coi1 `mkTransCoI`
 860                                                 ACo new_co `mkTransCoI`
 861                                                 (mkSymCoI coi2)
 862                                 ; writeMetaTyVar old_covar (fromACo old_coi)
 863                                 ; return $ mkWantedCo new_cotv
 864                                 })
 865                            -- new_co := sym co1 * old_co * co2
 866                            (\old_co ->
 867                              return $
 868                                mkGivenCo $
 869                                  fromACo $
 870                                    mkSymCoI coi1 `mkTransCoI`
 871                                    ACo old_co `mkTransCoI` coi2)
 872                      ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
 873                      ; return (new_inst, True)
 874                      }
 875                }
 876           where
 877             ty1 = eqInstLeftTy  inst
 878             ty2 = eqInstRightTy inst
 879 \end{code}
 880
 881
 882 Instantiate meta variables: unifyMetaRule
 883 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 884 If an equality equates a meta type variable with a type, we simply instantiate
 885 the meta variable.
 886
 887   (UnifyMeta)
 888     g : alpha ~ t
 889       >-->
 890     alpha := t
 891     g     := t
 892
 893 Meta variables can only appear in wanted constraints, and this rule should
 894 only be applied to wanted constraints.  We also know that t definitely is
 895 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
 896
 897 NB: We cannot assume that meta tyvars are empty.  They may have been updated
 898 by another inst in the currently processed wanted list.  We need to be very
 899 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
 900 we know that we have no boxes.  It's unclear that it would be an advantage to
 901 common up the code in TcUnify and the code below.  Firstly, we don't want
 902 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
 903 current module, so we would have to move everything here (Yuk!) or to
 904 TcMType.  Besides, the code here is much simpler due to the lack of boxes.
 905
 906 \begin{code}
 907 unifyMetaRule :: RewriteRule
 908 unifyMetaRule insts
 909   = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
 910        ; return (concat insts', or changed)
 911        }
 912   where
 913     unifyMeta inst
 914       = ASSERT( isEqInst inst )
 915         go (eqInstLeftTy inst) (eqInstRightTy inst)
 916            (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
 917       where
 918         go ty1 ty2 cotv
 919           | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
 920           | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
 921
 922           | TyVarTy tv1 <- ty1
 923           , isMetaTyVar tv1         = do { lookupTV <- lookupTcTyVar tv1
 924                                          ; uMeta False tv1 lookupTV ty2 cotv
 925                                          }
 926           | TyVarTy tv2 <- ty2
 927           , isMetaTyVar tv2         = do { lookupTV <- lookupTcTyVar tv2
 928                                          ; uMeta True tv2 lookupTV ty1 cotv
 929                                          }
 930           | otherwise               = return ([inst], False)
 931
 932         -- meta variable has been filled already
 933         -- => ignore this inst (we'll come around again, after zonking)
 934         uMeta _swapped _tv (IndirectTv _) _ty _cotv
 935           = return ([inst], False)
 936
 937         -- signature skolem meets non-variable type
 938         -- => cannot update!
 939         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) ty _cotv
 940           | not $ isTyVarTy ty
 941           = return ([inst], False)
 942
 943         -- type variable meets type variable
 944         -- => check that tv2 hasn't been updated yet and choose which to update
 945         uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
 946           = do { lookupTV2 <- lookupTcTyVar tv2
 947                ; case lookupTV2 of
 948                    IndirectTv ty  -> uMeta swapped tv1 (DoneTv details1) ty cotv
 949                    DoneTv details2 ->
 950                      uMetaVar swapped tv1 details1 tv2 details2 cotv
 951                }
 952
 953         -- updatable meta variable meets non-variable type
 954         -- => occurs check, monotype check, and kinds match check, then update
 955         uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv
 956           = do { mb_ty' <- checkTauTvUpdate tv ty    -- occurs + monotype check
 957                ; case mb_ty' of
 958                    Nothing  -> return ([inst], False)  -- tv occurs in faminst
 959                    Just ty' ->
 960                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
 961                         ; writeMetaTyVar cotv ty'             -- update co var
 962                         ; return ([], True)
 963                         }
 964                }
 965
 966         uMeta _ _ _ _ _ = panic "uMeta"
 967
 968         -- meta variable meets skolem
 969         -- => just update
 970         uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
 971           = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
 972                ; writeMetaTyVar cotv (mkTyVarTy tv2)
 973                ; return ([], True)
 974                }
 975
 976         -- meta variable meets meta variable
 977         -- => be clever about which of the two to update
 978         --   (from TcUnify.uUnfilledVars minus boxy stuff)
 979         uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
 980           = do { case (info1, info2) of
 981                    -- Avoid SigTvs if poss
 982                    (SigTv _, _      ) | k1_sub_k2 -> update_tv2
 983                    (_,       SigTv _) | k2_sub_k1 -> update_tv1
 984
 985                    (_,   _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
 986                                            then update_tv1      -- Same kinds
 987                                            else update_tv2
 988                             | k2_sub_k1 -> update_tv1
 989                             | otherwise -> kind_err
 990               -- Update the variable with least kind info
 991               -- See notes on type inference in Kind.lhs
 992               -- The "nicer to" part only applies if the two kinds are the same,
 993               -- so we can choose which to do.
 994
 995                ; writeMetaTyVar cotv (mkTyVarTy tv2)
 996                ; return ([], True)
 997                }
 998           where
 999                 -- Kinds should be guaranteed ok at this point
1000             update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1001             update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1002
1003             kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1004                        unifyKindMisMatch k1 k2
1005
1006             k1 = tyVarKind tv1
1007             k2 = tyVarKind tv2
1008             k1_sub_k2 = k1 `isSubKind` k2
1009             k2_sub_k1 = k2 `isSubKind` k1
1010
1011             nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1012                 -- Try to update sys-y type variables in preference to ones
1013                 -- gotten (say) by instantiating a polymorphic function with
1014                 -- a user-written type sig
1015
1016         uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1017 \end{code}
1018
1019
1020 %************************************************************************
1021 %*                                                                      *
1022 \section{Normalisation of Insts}
1023 %*                                                                      *
1024 %************************************************************************
1025
1026 Normalises a set of dictionaries relative to a set of given equalities (which
1027 are interpreted as rewrite rules).  We only consider given equalities of the
1028 form
1029
1030   F ts ~ t    or    a ~ t
1031
1032 where F is a type family.
1033
1034 \begin{code}
1035 substEqInDictInsts :: [Inst]    -- given equalities (used as rewrite rules)
1036                    -> [Inst]    -- dictinaries to be normalised
1037                    -> TcM ([Inst], TcDictBinds)
1038 substEqInDictInsts eqInsts dictInsts
1039   = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1040        ; dictInsts' <-
1041            foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1042        ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1043        ; return dictInsts'
1044        }
1045   where
1046       -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1047     rewriteWithOneEquality (dictInsts, dictBinds)
1048                            eqInst@(EqInst {tci_left  = pattern,
1049                                            tci_right = target})
1050       | isOpenSynTyConApp pattern || isTyVarTy pattern
1051       = do { (dictInsts', moreDictBinds) <-
1052                genericNormaliseInsts True {- wanted -} applyThisEq dictInsts
1053            ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1054            }
1055       where
1056         applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1057
1058         -- rewrite in case of an exact match
1059         matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1060                        | otherwise           = Nothing
1061
1062       -- (2) Given equality has the wrong form: ignore
1063     rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1064       = return (dictInsts, dictBinds)
1065 \end{code}
1066
1067
1068 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1069 type-function equations, where
1070
1071         (norm_insts, binds) = normaliseInsts is_wanted insts
1072
1073 If 'is_wanted'
1074   = True,  (binds + norm_insts) defines insts       (wanteds)
1075   = False, (binds + insts)      defines norm_insts  (givens)
1076
1077 Ie, in the case of normalising wanted dictionaries, we use the normalised
1078 dictionaries to define the originally wanted ones.  However, in the case of
1079 given dictionaries, we use the originally given ones to define the normalised
1080 ones.
1081
1082 \begin{code}
1083 normaliseInsts :: Bool                          -- True <=> wanted insts
1084                -> [Inst]                        -- wanted or given insts
1085                -> TcM ([Inst], TcDictBinds)     -- normalised insts and bindings
1086 normaliseInsts isWanted insts
1087   = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1088
1089 genericNormaliseInsts  :: Bool                      -- True <=> wanted insts
1090                        -> (TcPredType -> TcM (CoercionI, TcPredType))
1091                                                     -- how to normalise
1092                        -> [Inst]                    -- wanted or given insts
1093                        -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1094 genericNormaliseInsts isWanted fun insts
1095   = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1096        ; return (insts', unionManyBags binds)
1097        }
1098   where
1099     normaliseOneInst isWanted fun
1100                      dict@(Dict {tci_pred = pred,
1101                                  tci_loc  = loc})
1102       = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1103            ; (coi, pred') <- fun pred
1104
1105            ; case coi of
1106                IdCo   ->
1107                  do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1108                     ; return (dict, emptyBag)
1109                     }
1110                          -- don't use pred' in this case; otherwise, we get
1111                          -- more unfolded closed type synonyms in error messages
1112                ACo co ->
1113                  do { -- an inst for the new pred
1114                     ; dict' <- newDictBndr loc pred'
1115                       -- relate the old inst to the new one
1116                       -- target_dict = source_dict `cast` st_co
1117                     ; let (target_dict, source_dict, st_co)
1118                             | isWanted  = (dict,  dict', mkSymCoercion co)
1119                             | otherwise = (dict', dict,  co)
1120                               -- we have
1121                               --   co :: dict ~ dict'
1122                               -- hence, if isWanted
1123                               --          dict  = dict' `cast` sym co
1124                               --        else
1125                               --          dict' = dict  `cast` co
1126                           expr      = HsVar $ instToId source_dict
1127                           cast_expr = HsWrap (WpCo st_co) expr
1128                           rhs       = L (instLocSpan loc) cast_expr
1129                           binds     = instToDictBind target_dict rhs
1130                       -- return the new inst
1131                     ; traceTc $ text "genericNormaliseInst ->" <+> ppr dict'
1132                     ; return (dict', binds)
1133                     }
1134            }
1135
1136         -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1137     normaliseOneInst _isWanted _fun inst
1138       = do { inst' <- zonkInst inst
1139            ; return (inst', emptyBag)
1140            }
1141 \end{code}
1142
1143
1144 %************************************************************************
1145 %*                                                                      *
1146 \section{Errors}
1147 %*                                                                      *
1148 %************************************************************************
1149
1150 The infamous couldn't match expected type soandso against inferred type
1151 somethingdifferent message.
1152
1153 \begin{code}
1154 eqInstMisMatch :: Inst -> TcM a
1155 eqInstMisMatch inst
1156   = ASSERT( isEqInst inst )
1157     do { (env, msg) <- misMatchMsg ty_act ty_exp
1158        ; setErrCtxt ctxt $
1159            failWithTcM (env, msg)
1160        }
1161   where
1162     ty_act           = eqInstLeftTy  inst
1163     ty_exp           = eqInstRightTy inst
1164     InstLoc _ _ ctxt = instLoc       inst
1165
1166 -----------------------
1167 misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
1168 -- Generate the message when two types fail to match,
1169 -- going to some trouble to make it helpful.
1170 -- The argument order is: actual type, expected type
1171 misMatchMsg ty_act ty_exp
1172   = do  { env0 <- tcInitTidyEnv
1173         ; ty_exp <- zonkTcType ty_exp
1174         ; ty_act <- zonkTcType ty_act
1175         ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
1176         ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
1177         ; return (env2,
1178                   sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1179                             nest 7 $
1180                               ptext SLIT("against inferred type") <+> pp_act],
1181                        nest 2 (extra_exp $$ extra_act)]) }
1182
1183 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1184 ppr_ty env ty
1185   = do  { let (env1, tidy_ty) = tidyOpenType env ty
1186         ; (env2, extra) <- ppr_extra env1 tidy_ty
1187         ; return (env2, quotes (ppr tidy_ty), extra) }
1188
1189 -- (ppr_extra env ty) shows extra info about 'ty'
1190 ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
1191 ppr_extra env (TyVarTy tv)
1192   | isSkolemTyVar tv || isSigTyVar tv
1193   = return (env1, pprSkolTvBinding tv1)
1194   where
1195     (env1, tv1) = tidySkolemTyVar env tv
1196
1197 ppr_extra env _ty = return (env, empty)         -- Normal case
1198 \end{code}