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