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