compiler/typecheck/Inst.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 The @Inst@ type: dictionaries or method instances
   7
   8 \begin{code}
   9 module Inst (
  10        deeplySkolemise,
  11        deeplyInstantiate, instCall, instStupidTheta,
  12        emitWanted, emitWanteds,
  13
  14        newOverloadedLit, mkOverLit,
  15
  16        tcGetInstEnvs, getOverlapFlag, tcExtendLocalInstEnv,
  17        instCallConstraints, newMethodFromName,
  18        tcSyntaxName,
  19
  20        -- Simple functions over evidence variables
  21        hasEqualities, unitImplication,
  22
  23        tyVarsOfWC, tyVarsOfBag, tyVarsOfEvVarXs, tyVarsOfEvVarX,
  24        tyVarsOfEvVar, tyVarsOfEvVars, tyVarsOfImplication,
  25
  26        tidyWantedEvVar, tidyWantedEvVars, tidyWC,
  27        tidyEvVar, tidyImplication, tidyFlavoredEvVar,
  28
  29        substWantedEvVar, substWantedEvVars, substFlavoredEvVar,
  30        substEvVar, substImplication
  31     ) where
  32
  33 #include "HsVersions.h"
  34
  35 import {-# SOURCE #-}   TcExpr( tcPolyExpr, tcSyntaxOp )
  36 import {-# SOURCE #-}   TcUnify( unifyType )
  37
  38 import FastString
  39 import HsSyn
  40 import TcHsSyn
  41 import TcRnMonad
  42 import TcEnv
  43 import InstEnv
  44 import FunDeps
  45 import TcMType
  46 import TcType
  47 import Class
  48 import Unify
  49 import Coercion
  50 import HscTypes
  51 import Id
  52 import Name
  53 import Var
  54 import VarEnv
  55 import VarSet
  56 import PrelNames
  57 import SrcLoc
  58 import DynFlags
  59 import Bag
  60 import Maybes
  61 import Util
  62 import Outputable
  63 import Data.List( mapAccumL )
  64 \end{code}
  65
  66
  67
  68 %************************************************************************
  69 %*                                                                      *
  70                 Emitting constraints
  71 %*                                                                      *
  72 %************************************************************************
  73
  74 \begin{code}
  75 emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
  76 emitWanteds origin theta = mapM (emitWanted origin) theta
  77
  78 emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
  79 emitWanted origin pred = do { loc <- getCtLoc origin
  80                             ; ev  <- newWantedEvVar pred
  81                             ; emitFlat (mkEvVarX ev loc)
  82                             ; return ev }
  83
  84 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
  85 -- Used when Name is the wired-in name for a wired-in class method,
  86 -- so the caller knows its type for sure, which should be of form
  87 --    forall a. C a => <blah>
  88 -- newMethodFromName is supposed to instantiate just the outer
  89 -- type variable and constraint
  90
  91 newMethodFromName origin name inst_ty
  92   = do { id <- tcLookupId name
  93               -- Use tcLookupId not tcLookupGlobalId; the method is almost
  94               -- always a class op, but with -XRebindableSyntax GHC is
  95               -- meant to find whatever thing is in scope, and that may
  96               -- be an ordinary function.
  97
  98        ; let (tvs, theta, _caller_knows_this) = tcSplitSigmaTy (idType id)
  99              (the_tv:rest) = tvs
 100              subst = zipOpenTvSubst [the_tv] [inst_ty]
 101
 102        ; wrap <- ASSERT( null rest && isSingleton theta )
 103                  instCall origin [inst_ty] (substTheta subst theta)
 104        ; return (mkHsWrap wrap (HsVar id)) }
 105 \end{code}
 106
 107
 108 %************************************************************************
 109 %*                                                                      *
 110         Deep instantiation and skolemisation
 111 %*                                                                      *
 112 %************************************************************************
 113
 114 Note [Deep skolemisation]
 115 ~~~~~~~~~~~~~~~~~~~~~~~~~
 116 deeplySkolemise decomposes and skolemises a type, returning a type
 117 with all its arrows visible (ie not buried under foralls)
 118
 119 Examples:
 120
 121   deeplySkolemise (Int -> forall a. Ord a => blah)
 122     =  ( wp, [a], [d:Ord a], Int -> blah )
 123     where wp = \x:Int. /\a. \(d:Ord a). <hole> x
 124
 125   deeplySkolemise  (forall a. Ord a => Maybe a -> forall b. Eq b => blah)
 126     =  ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
 127     where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
 128
 129 In general,
 130   if      deeplySkolemise ty = (wrap, tvs, evs, rho)
 131     and   e :: rho
 132   then    wrap e :: ty
 133     and   'wrap' binds tvs, evs
 134
 135 ToDo: this eta-abstraction plays fast and loose with termination,
 136       because it can introduce extra lambdas.  Maybe add a `seq` to
 137       fix this
 138
 139
 140 \begin{code}
 141 deeplySkolemise
 142   :: TcSigmaType
 143   -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType)
 144
 145 deeplySkolemise ty
 146   | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
 147   = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
 148        ; tvs1 <- tcInstSkolTyVars tvs
 149        ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs1)
 150        ; ev_vars1 <- newEvVars (substTheta subst theta)
 151        ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
 152        ; return ( mkWpLams ids1
 153                    <.> mkWpTyLams tvs1
 154                    <.> mkWpLams ev_vars1
 155                    <.> wrap
 156                    <.> mkWpEvVarApps ids1
 157                 , tvs1     ++ tvs2
 158                 , ev_vars1 ++ ev_vars2
 159                 , mkFunTys arg_tys rho ) }
 160
 161   | otherwise
 162   = return (idHsWrapper, [], [], ty)
 163
 164 deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 165 --   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
 166 -- In general if
 167 -- if    deeplyInstantiate ty = (wrap, rho)
 168 -- and   e :: ty
 169 -- then  wrap e :: rho
 170
 171 deeplyInstantiate orig ty
 172   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
 173   = do { (_, tys, subst) <- tcInstTyVars tvs
 174        ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
 175        ; wrap1 <- instCall orig tys (substTheta subst theta)
 176        ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
 177        ; return (mkWpLams ids1
 178                     <.> wrap2
 179                     <.> wrap1
 180                     <.> mkWpEvVarApps ids1,
 181                  mkFunTys arg_tys rho2) }
 182
 183   | otherwise = return (idHsWrapper, ty)
 184 \end{code}
 185
 186
 187 %************************************************************************
 188 %*                                                                      *
 189             Instantiating a call
 190 %*                                                                      *
 191 %************************************************************************
 192
 193 \begin{code}
 194 ----------------
 195 instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
 196 -- Instantiate the constraints of a call
 197 --      (instCall o tys theta)
 198 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
 199 -- (b) Throws these dictionaries into the LIE
 200 -- (c) Returns an HsWrapper ([.] tys dicts)
 201
 202 instCall orig tys theta
 203   = do  { dict_app <- instCallConstraints orig theta
 204         ; return (dict_app <.> mkWpTyApps tys) }
 205
 206 ----------------
 207 instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
 208 -- Instantiates the TcTheta, puts all constraints thereby generated
 209 -- into the LIE, and returns a HsWrapper to enclose the call site.
 210
 211 instCallConstraints _ [] = return idHsWrapper
 212
 213 instCallConstraints origin (EqPred ty1 ty2 : preds)     -- Try short-cut
 214   = do  { traceTc "instCallConstraints" $ ppr (EqPred ty1 ty2)
 215         ; coi   <- unifyType ty1 ty2
 216         ; co_fn <- instCallConstraints origin preds
 217         ; let co = case coi of
 218                        IdCo ty -> ty
 219                        ACo  co -> co
 220         ; return (co_fn <.> WpEvApp (EvCoercion co)) }
 221
 222 instCallConstraints origin (pred : preds)
 223   = do  { ev_var <- emitWanted origin pred
 224         ; co_fn <- instCallConstraints origin preds
 225         ; return (co_fn <.> WpEvApp (EvId ev_var)) }
 226
 227 ----------------
 228 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
 229 -- Similar to instCall, but only emit the constraints in the LIE
 230 -- Used exclusively for the 'stupid theta' of a data constructor
 231 instStupidTheta orig theta
 232   = do  { _co <- instCallConstraints orig theta -- Discard the coercion
 233         ; return () }
 234 \end{code}
 235
 236 %************************************************************************
 237 %*                                                                      *
 238                 Literals
 239 %*                                                                      *
 240 %************************************************************************
 241
 242 In newOverloadedLit we convert directly to an Int or Integer if we
 243 know that's what we want.  This may save some time, by not
 244 temporarily generating overloaded literals, but it won't catch all
 245 cases (the rest are caught in lookupInst).
 246
 247 \begin{code}
 248 newOverloadedLit :: CtOrigin
 249                  -> HsOverLit Name
 250                  -> TcRhoType
 251                  -> TcM (HsOverLit TcId)
 252 newOverloadedLit orig
 253   lit@(OverLit { ol_val = val, ol_rebindable = rebindable
 254                , ol_witness = meth_name }) res_ty
 255
 256   | not rebindable
 257   , Just expr <- shortCutLit val res_ty
 258         -- Do not generate a LitInst for rebindable syntax.
 259         -- Reason: If we do, tcSimplify will call lookupInst, which
 260         --         will call tcSyntaxName, which does unification,
 261         --         which tcSimplify doesn't like
 262   = return (lit { ol_witness = expr, ol_type = res_ty })
 263
 264   | otherwise
 265   = do  { hs_lit <- mkOverLit val
 266         ; let lit_ty = hsLitType hs_lit
 267         ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
 268                 -- Overloaded literals must have liftedTypeKind, because
 269                 -- we're instantiating an overloaded function here,
 270                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
 271                 -- However this'll be picked up by tcSyntaxOp if necessary
 272         ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
 273         ; return (lit { ol_witness = witness, ol_type = res_ty }) }
 274
 275 ------------
 276 mkOverLit :: OverLitVal -> TcM HsLit
 277 mkOverLit (HsIntegral i)
 278   = do  { integer_ty <- tcMetaTy integerTyConName
 279         ; return (HsInteger i integer_ty) }
 280
 281 mkOverLit (HsFractional r)
 282   = do  { rat_ty <- tcMetaTy rationalTyConName
 283         ; return (HsRat r rat_ty) }
 284
 285 mkOverLit (HsIsString s) = return (HsString s)
 286 \end{code}
 287
 288
 289
 290
 291 %************************************************************************
 292 %*                                                                      *
 293                 Re-mappable syntax
 294
 295      Used only for arrow syntax -- find a way to nuke this
 296 %*                                                                      *
 297 %************************************************************************
 298
 299 Suppose we are doing the -XRebindableSyntax thing, and we encounter
 300 a do-expression.  We have to find (>>) in the current environment, which is
 301 done by the rename. Then we have to check that it has the same type as
 302 Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
 303 this:
 304
 305   (>>) :: HB m n mn => m a -> n b -> mn b
 306
 307 So the idea is to generate a local binding for (>>), thus:
 308
 309         let then72 :: forall a b. m a -> m b -> m b
 310             then72 = ...something involving the user's (>>)...
 311         in
 312         ...the do-expression...
 313
 314 Now the do-expression can proceed using then72, which has exactly
 315 the expected type.
 316
 317 In fact tcSyntaxName just generates the RHS for then72, because we only
 318 want an actual binding in the do-expression case. For literals, we can
 319 just use the expression inline.
 320
 321 \begin{code}
 322 tcSyntaxName :: CtOrigin
 323              -> TcType                  -- Type to instantiate it at
 324              -> (Name, HsExpr Name)     -- (Standard name, user name)
 325              -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
 326 --      *** NOW USED ONLY FOR CmdTop (sigh) ***
 327 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
 328 -- So we do not call it from lookupInst, which is called from tcSimplify
 329
 330 tcSyntaxName orig ty (std_nm, HsVar user_nm)
 331   | std_nm == user_nm
 332   = do rhs <- newMethodFromName orig std_nm ty
 333        return (std_nm, rhs)
 334
 335 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
 336     std_id <- tcLookupId std_nm
 337     let
 338         -- C.f. newMethodAtLoc
 339         ([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
 340         sigma1          = substTyWith [tv] [ty] tau
 341         -- Actually, the "tau-type" might be a sigma-type in the
 342         -- case of locally-polymorphic methods.
 343
 344     addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
 345
 346         -- Check that the user-supplied thing has the
 347         -- same type as the standard one.
 348         -- Tiresome jiggling because tcCheckSigma takes a located expression
 349      span <- getSrcSpanM
 350      expr <- tcPolyExpr (L span user_nm_expr) sigma1
 351      return (std_nm, unLoc expr)
 352
 353 syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
 354                -> TcRn (TidyEnv, SDoc)
 355 syntaxNameCtxt name orig ty tidy_env = do
 356     inst_loc <- getCtLoc orig
 357     let
 358         msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+>
 359                                 ptext (sLit "(needed by a syntactic construct)"),
 360                     nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
 361                     nest 2 (pprArisingAt inst_loc)]
 362     return (tidy_env, msg)
 363 \end{code}
 364
 365
 366 %************************************************************************
 367 %*                                                                      *
 368                 Instances
 369 %*                                                                      *
 370 %************************************************************************
 371
 372 \begin{code}
 373 getOverlapFlag :: TcM OverlapFlag
 374 getOverlapFlag
 375   = do  { dflags <- getDOpts
 376         ; let overlap_ok    = xopt Opt_OverlappingInstances dflags
 377               incoherent_ok = xopt Opt_IncoherentInstances  dflags
 378               overlap_flag | incoherent_ok = Incoherent
 379                            | overlap_ok    = OverlapOk
 380                            | otherwise     = NoOverlap
 381
 382         ; return overlap_flag }
 383
 384 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
 385 -- Gets both the external-package inst-env
 386 -- and the home-pkg inst env (includes module being compiled)
 387 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
 388                      return (eps_inst_env eps, tcg_inst_env env) }
 389
 390 tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
 391   -- Add new locally-defined instances
 392 tcExtendLocalInstEnv dfuns thing_inside
 393  = do { traceDFuns dfuns
 394       ; env <- getGblEnv
 395       ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
 396       ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
 397                          tcg_inst_env = inst_env' }
 398       ; setGblEnv env' thing_inside }
 399
 400 addLocalInst :: InstEnv -> Instance -> TcM InstEnv
 401 -- Check that the proposed new instance is OK,
 402 -- and then add it to the home inst env
 403 addLocalInst home_ie ispec
 404   = do  {       -- Instantiate the dfun type so that we extend the instance
 405                 -- envt with completely fresh template variables
 406                 -- This is important because the template variables must
 407                 -- not overlap with anything in the things being looked up
 408                 -- (since we do unification).
 409                 --
 410                 -- We use tcInstSkolType because we don't want to allocate fresh
 411                 --  *meta* type variables.
 412                 --
 413                 -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
 414                 -- these variables must be bindable by tcUnifyTys.  See
 415                 -- the call to tcUnifyTys in InstEnv, and the special
 416                 -- treatment that instanceBindFun gives to isOverlappableTyVar
 417                 -- This is absurdly delicate.
 418
 419           let dfun = instanceDFunId ispec
 420         ; (tvs', theta', tau') <- tcInstSkolType (idType dfun)
 421         ; let   (cls, tys') = tcSplitDFunHead tau'
 422                 dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')
 423                 ispec'      = setInstanceDFunId ispec dfun'
 424
 425                 -- Load imported instances, so that we report
 426                 -- duplicates correctly
 427         ; eps <- getEps
 428         ; let inst_envs = (eps_inst_env eps, home_ie)
 429
 430                 -- Check functional dependencies
 431         ; case checkFunDeps inst_envs ispec' of
 432                 Just specs -> funDepErr ispec' specs
 433                 Nothing    -> return ()
 434
 435                 -- Check for duplicate instance decls
 436         ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
 437               ; dup_ispecs = [ dup_ispec
 438                              | (dup_ispec, _) <- matches
 439                              , let (_,_,_,dup_tys) = instanceHead dup_ispec
 440                              , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
 441                 -- Find memebers of the match list which ispec itself matches.
 442                 -- If the match is 2-way, it's a duplicate
 443         ; case dup_ispecs of
 444             dup_ispec : _ -> dupInstErr ispec' dup_ispec
 445             []            -> return ()
 446
 447                 -- OK, now extend the envt
 448         ; return (extendInstEnv home_ie ispec') }
 449
 450 traceDFuns :: [Instance] -> TcRn ()
 451 traceDFuns ispecs
 452   = traceTc "Adding instances:" (vcat (map pp ispecs))
 453   where
 454     pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
 455         -- Print the dfun name itself too
 456
 457 funDepErr :: Instance -> [Instance] -> TcRn ()
 458 funDepErr ispec ispecs
 459   = addDictLoc ispec $
 460     addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
 461                2 (pprInstances (ispec:ispecs)))
 462 dupInstErr :: Instance -> Instance -> TcRn ()
 463 dupInstErr ispec dup_ispec
 464   = addDictLoc ispec $
 465     addErr (hang (ptext (sLit "Duplicate instance declarations:"))
 466                2 (pprInstances [ispec, dup_ispec]))
 467
 468 addDictLoc :: Instance -> TcRn a -> TcRn a
 469 addDictLoc ispec thing_inside
 470   = setSrcSpan (mkSrcSpan loc loc) thing_inside
 471   where
 472    loc = getSrcLoc ispec
 473 \end{code}
 474
 475 %************************************************************************
 476 %*                                                                      *
 477         Simple functions over evidence variables
 478 %*                                                                      *
 479 %************************************************************************
 480
 481 \begin{code}
 482 unitImplication :: Implication -> Bag Implication
 483 unitImplication implic
 484   | isEmptyWC (ic_wanted implic) = emptyBag
 485   | otherwise                    = unitBag implic
 486
 487 hasEqualities :: [EvVar] -> Bool
 488 -- Has a bunch of canonical constraints (all givens) got any equalities in it?
 489 hasEqualities givens = any (has_eq . evVarPred) givens
 490   where
 491     has_eq (EqPred {})       = True
 492     has_eq (IParam {})       = False
 493     has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls)
 494
 495 ---------------- Getting free tyvars -------------------------
 496 tyVarsOfWC :: WantedConstraints -> TyVarSet
 497 tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
 498   = tyVarsOfEvVarXs flat `unionVarSet`
 499     tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
 500     tyVarsOfEvVarXs insol
 501
 502 tyVarsOfImplication :: Implication -> TyVarSet
 503 tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
 504   = tyVarsOfWC wanted `minusVarSet` skols
 505
 506 tyVarsOfEvVarX :: EvVarX a -> TyVarSet
 507 tyVarsOfEvVarX (EvVarX ev _) = tyVarsOfEvVar ev
 508
 509 tyVarsOfEvVarXs :: Bag (EvVarX a) -> TyVarSet
 510 tyVarsOfEvVarXs = tyVarsOfBag tyVarsOfEvVarX
 511
 512 tyVarsOfEvVar :: EvVar -> TyVarSet
 513 tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev
 514
 515 tyVarsOfEvVars :: [EvVar] -> TyVarSet
 516 tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
 517
 518 tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
 519 tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
 520
 521 ---------------- Tidying -------------------------
 522 tidyWC :: TidyEnv -> WantedConstraints -> WantedConstraints
 523 tidyWC env (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
 524   = WC { wc_flat  = tidyWantedEvVars env flat
 525        , wc_impl  = mapBag (tidyImplication env) implic
 526        , wc_insol = mapBag (tidyFlavoredEvVar env) insol }
 527
 528 tidyImplication :: TidyEnv -> Implication -> Implication
 529 tidyImplication env implic@(Implic { ic_skols = tvs
 530                                    , ic_given = given
 531                                    , ic_wanted = wanted
 532                                    , ic_loc = loc })
 533   = implic { ic_skols = mkVarSet tvs'
 534            , ic_given = map (tidyEvVar env1) given
 535            , ic_wanted = tidyWC env1 wanted
 536            , ic_loc = tidyGivenLoc env1 loc }
 537   where
 538    (env1, tvs') = mapAccumL tidyTyVarBndr env (varSetElems tvs)
 539
 540 tidyEvVar :: TidyEnv -> EvVar -> EvVar
 541 tidyEvVar env var = setVarType var (tidyType env (varType var))
 542
 543 tidyWantedEvVar :: TidyEnv -> WantedEvVar -> WantedEvVar
 544 tidyWantedEvVar env (EvVarX v l) = EvVarX (tidyEvVar env v) l
 545
 546 tidyWantedEvVars :: TidyEnv -> Bag WantedEvVar -> Bag WantedEvVar
 547 tidyWantedEvVars env = mapBag (tidyWantedEvVar env)
 548
 549 tidyFlavoredEvVar :: TidyEnv -> FlavoredEvVar -> FlavoredEvVar
 550 tidyFlavoredEvVar env (EvVarX v fl)
 551   = EvVarX (tidyEvVar env v) (tidyFlavor env fl)
 552
 553 tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
 554 tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc)
 555 tidyFlavor _   fl          = fl
 556
 557 tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
 558 tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt
 559
 560 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
 561 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
 562 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
 563 tidySkolemInfo _   info            = info
 564
 565 ---------------- Substitution -------------------------
 566 substWC :: TvSubst -> WantedConstraints -> WantedConstraints
 567 substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
 568   = WC { wc_flat = substWantedEvVars subst flat
 569        , wc_impl = mapBag (substImplication subst) implic
 570        , wc_insol = mapBag (substFlavoredEvVar subst) insol }
 571
 572 substImplication :: TvSubst -> Implication -> Implication
 573 substImplication subst implic@(Implic { ic_skols = tvs
 574                                       , ic_given = given
 575                                       , ic_wanted = wanted
 576                                       , ic_loc = loc })
 577   = implic { ic_skols  = mkVarSet tvs'
 578            , ic_given  = map (substEvVar subst1) given
 579            , ic_wanted = substWC subst1 wanted
 580            , ic_loc    = substGivenLoc subst1 loc }
 581   where
 582    (subst1, tvs') = mapAccumL substTyVarBndr subst (varSetElems tvs)
 583
 584 substEvVar :: TvSubst -> EvVar -> EvVar
 585 substEvVar subst var = setVarType var (substTy subst (varType var))
 586
 587 substWantedEvVars :: TvSubst -> Bag WantedEvVar -> Bag WantedEvVar
 588 substWantedEvVars subst = mapBag (substWantedEvVar subst)
 589
 590 substWantedEvVar :: TvSubst -> WantedEvVar -> WantedEvVar
 591 substWantedEvVar subst (EvVarX v l) = EvVarX (substEvVar subst v) l
 592
 593 substFlavoredEvVar :: TvSubst -> FlavoredEvVar -> FlavoredEvVar
 594 substFlavoredEvVar subst (EvVarX v fl)
 595   = EvVarX (substEvVar subst v) (substFlavor subst fl)
 596
 597 substFlavor :: TvSubst -> CtFlavor -> CtFlavor
 598 substFlavor subst (Given loc) = Given (substGivenLoc subst loc)
 599 substFlavor _     fl          = fl
 600
 601 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
 602 substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
 603
 604 substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
 605 substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
 606 substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
 607 substSkolemInfo _     info            = info
 608 \end{code}