compiler/typecheck/TcTyFuns.lhs

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