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