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