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