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