compiler/typecheck/TcTyFuns.lhs

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