compiler/typecheck/TcTyFuns.lhs

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