compiler/typecheck/TcSMonad.lhs

   1 \begin{code}
   2 -- Type definitions for the constraint solver
   3 module TcSMonad (
   4
   5        -- Canonical constraints
   6     CanonicalCts, emptyCCan, andCCan, andCCans,
   7     singleCCan, extendCCans, isEmptyCCan,
   8     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals,
   9     mkWantedConstraints, deCanonicaliseWanted,
  10     makeGivens, makeSolved,
  11
  12     CtFlavor (..), isWanted, isGiven, isDerived, canRewrite,
  13     joinFlavors, mkGivenFlavor,
  14
  15     TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality
  16     tryTcS, nestImplicTcS, wrapErrTcS, wrapWarnTcS,
  17     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
  18
  19        -- Creation of evidence variables
  20
  21     newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
  22     newIPVar, newDictVar, newKindConstraint,
  23
  24        -- Setting evidence variables
  25     setWantedCoBind, setDerivedCoBind,
  26     setIPBind, setDictBind, setEvBind,
  27
  28     setWantedTyBind,
  29
  30     newTcEvBindsTcS,
  31
  32     getInstEnvs, getFamInstEnvs,                -- Getting the environments
  33     getTopEnv, getGblEnv, getTcEvBinds, getUntouchablesTcS,
  34     getTcEvBindsBag, getTcSContext, getTcSTyBinds,
  35
  36
  37     newFlattenSkolemTy,                         -- Flatten skolems
  38
  39     instDFunTypes,                              -- Instantiation
  40     instDFunConstraints,
  41
  42     isGoodRecEv,
  43
  44     isTouchableMetaTyVar,
  45
  46     getDefaultInfo, getDynFlags,
  47
  48     matchClass, matchFam, MatchInstResult (..),
  49     checkWellStagedDFun,
  50     warnTcS,
  51     pprEq,                                   -- Smaller utils, re-exported from TcM
  52                                              -- TODO (DV): these are only really used in the
  53                                              -- instance matcher in TcSimplify. I am wondering
  54                                              -- if the whole instance matcher simply belongs
  55                                              -- here
  56
  57
  58     mkWantedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
  59
  60 ) where
  61
  62 #include "HsVersions.h"
  63
  64 import HscTypes
  65 import BasicTypes
  66 import Type
  67
  68 import Inst
  69 import InstEnv
  70 import FamInst
  71 import FamInstEnv
  72
  73 import NameSet ( addOneToNameSet )
  74
  75 import qualified TcRnMonad as TcM
  76 import qualified TcMType as TcM
  77 import qualified TcEnv as TcM
  78        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
  79 import TcType
  80 import Module
  81 import DynFlags
  82
  83 import Coercion
  84 import Class
  85 import TyCon
  86 import Name
  87 import Var
  88 import Outputable
  89 import Bag
  90 import MonadUtils
  91 import VarSet
  92 import FastString
  93
  94 import HsBinds               -- for TcEvBinds stuff
  95 import Id
  96 import FunDeps
  97
  98 import TcRnTypes
  99
 100 import Control.Monad
 101 import Data.IORef
 102 \end{code}
 103
 104
 105 %************************************************************************
 106 %*                                                                      *
 107 %*                       Canonical constraints                          *
 108 %*                                                                      *
 109 %*   These are the constraints the low-level simplifier works with      *
 110 %*                                                                      *
 111 %************************************************************************
 112
 113 \begin{code}
 114 -- Types without any type functions inside.  However, note that xi
 115 -- types CAN contain unexpanded type synonyms; however, the
 116 -- (transitive) expansions of those type synonyms will not contain any
 117 -- type functions.
 118 type Xi = Type       -- In many comments, "xi" ranges over Xi
 119
 120 type CanonicalCts = Bag CanonicalCt
 121
 122 data CanonicalCt
 123   -- Atomic canonical constraints
 124   = CDictCan {  -- e.g.  Num xi
 125       cc_id     :: EvVar,
 126       cc_flavor :: CtFlavor,
 127       cc_class  :: Class,
 128       cc_tyargs :: [Xi]
 129     }
 130
 131   | CIPCan {    -- ?x::tau
 132       -- See note [Canonical implicit parameter constraints].
 133       cc_id     :: EvVar,
 134       cc_flavor :: CtFlavor,
 135       cc_ip_nm  :: IPName Name,
 136       cc_ip_ty  :: TcTauType
 137     }
 138
 139   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
 140        -- Invariant:
 141        --   * tv not in tvs(xi)   (occurs check)
 142        --   * If tv is a MetaTyVar, then typeKind xi <: typeKind tv
 143        --              a skolem,    then typeKind xi =  typeKind tv
 144       cc_id     :: EvVar,
 145       cc_flavor :: CtFlavor,
 146       cc_tyvar :: TcTyVar,
 147       cc_rhs   :: Xi
 148     }
 149
 150   | CFunEqCan {  -- F xis ~ xi
 151                  -- Invariant: * isSynFamilyTyCon cc_fun
 152                  --            * cc_rhs is not a touchable unification variable
 153                  --                   See Note [No touchables as FunEq RHS]
 154                  --            * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
 155       cc_id     :: EvVar,
 156       cc_flavor :: CtFlavor,
 157       cc_fun    :: TyCon,       -- A type function
 158       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
 159       cc_rhs    :: Xi           --    *never* over-saturated (because if so
 160                                 --    we should have decomposed)
 161
 162     }
 163
 164 makeGivens :: CanonicalCts -> CanonicalCts
 165 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
 166            -- The UnkSkol doesn't matter because these givens are
 167            -- not contradictory (else we'd have rejected them already)
 168
 169 makeSolved :: CanonicalCt -> CanonicalCt
 170 -- Record that a constraint is now solved
 171 --        Wanted         -> Derived
 172 --        Given, Derived -> no-op
 173 makeSolved ct
 174   | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc }
 175   | otherwise                  = ct
 176
 177 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
 178 mkWantedConstraints flats implics
 179   = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
 180
 181 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
 182 deCanonicaliseWanted ct
 183   = WARN( not (isWanted $ cc_flavor ct), ppr ct )
 184     let Wanted loc = cc_flavor ct
 185     in WantedEvVar (cc_id ct) loc
 186
 187 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
 188 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
 189 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
 190 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
 191 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
 192
 193 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
 194 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
 195
 196 instance Outputable CanonicalCt where
 197   ppr (CDictCan d fl cls tys)
 198       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
 199   ppr (CIPCan ip fl ip_nm ty)
 200       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
 201   ppr (CTyEqCan co fl tv ty)
 202       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
 203   ppr (CFunEqCan co fl tc tys ty)
 204       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
 205 \end{code}
 206
 207
 208 Note [No touchables as FunEq RHS]
 209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 210 Notice that (F xis ~ beta), where beta is an touchable unification
 211 variable, is not canonical.  Why?
 212   * If (F xis ~ beta) was the only wanted constraint, we'd
 213     definitely want to spontaneously-unify it
 214
 215   * But suppose we had an earlier wanted (beta ~ Int), and
 216     have already spontaneously unified it.  Then we have an
 217     identity given (id : beta ~ Int) in the inert set.
 218
 219   * But (F xis ~ beta) does not react with that given (because we
 220     don't subsitute on the RHS of a function equality).  So there's a
 221     serious danger that we'd spontaneously unify it a second time.
 222
 223 Hence the invariant.
 224
 225 Note [Canonical implicit parameter constraints]
 226 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 227 The type in a canonical implicit parameter constraint doesn't need to
 228 be a xi (type-function-free type) since we can defer the flattening
 229 until checking this type for equality with another type.  If we
 230 encounter two IP constraints with the same name, they MUST have the
 231 same type, and at that point we can generate a flattened equality
 232 constraint between the types.  (On the other hand, the types in two
 233 class constraints for the same class MAY be equal, so they need to be
 234 flattened in the first place to facilitate comparing them.)
 235
 236 \begin{code}
 237 singleCCan :: CanonicalCt -> CanonicalCts
 238 singleCCan = unitBag
 239
 240 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
 241 andCCan = unionBags
 242
 243 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
 244 extendCCans = snocBag
 245
 246 andCCans :: [CanonicalCts] -> CanonicalCts
 247 andCCans = unionManyBags
 248
 249 emptyCCan :: CanonicalCts
 250 emptyCCan = emptyBag
 251
 252 isEmptyCCan :: CanonicalCts -> Bool
 253 isEmptyCCan = isEmptyBag
 254 \end{code}
 255
 256 %************************************************************************
 257 %*                                                                      *
 258                     CtFlavor
 259          The "flavor" of a canonical constraint
 260 %*                                                                      *
 261 %************************************************************************
 262
 263 \begin{code}
 264 data CtFlavor
 265   = Given   GivenLoc  -- We have evidence for this constraint in TcEvBinds
 266   | Derived WantedLoc -- We have evidence for this constraint in TcEvBinds;
 267                       --   *however* this evidence can contain wanteds, so
 268                       --   it's valid only provisionally to the solution of
 269                       --   these wanteds
 270   | Wanted WantedLoc  -- We have no evidence bindings for this constraint.
 271
 272 instance Outputable CtFlavor where
 273   ppr (Given _)   = ptext (sLit "[Given]")
 274   ppr (Wanted _)  = ptext (sLit "[Wanted]")
 275   ppr (Derived _) = ptext (sLit "[Derived]")
 276
 277 isWanted :: CtFlavor -> Bool
 278 isWanted (Wanted {}) = True
 279 isWanted _           = False
 280
 281 isGiven :: CtFlavor -> Bool
 282 isGiven (Given {}) = True
 283 isGiven _          = False
 284
 285 isDerived :: CtFlavor -> Bool
 286 isDerived (Derived {}) = True
 287 isDerived _            = False
 288
 289 canRewrite :: CtFlavor -> CtFlavor -> Bool
 290 -- canRewrite ctid1 ctid2
 291 -- The constraint ctid1 can be used to rewrite ctid2
 292 canRewrite (Given {})   _            = True
 293 canRewrite (Derived {}) (Wanted {})  = True
 294 canRewrite (Derived {}) (Derived {}) = True
 295 canRewrite (Wanted {})  (Wanted {})  = True
 296 canRewrite _ _ = False
 297
 298 joinFlavors :: CtFlavor -> CtFlavor -> CtFlavor
 299 joinFlavors (Wanted loc) _  = Wanted loc
 300 joinFlavors _ (Wanted loc)  = Wanted loc
 301 joinFlavors (Derived loc) _ = Derived loc
 302 joinFlavors _ (Derived loc) = Derived loc
 303 joinFlavors (Given loc) _   = Given loc
 304
 305 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 306 mkGivenFlavor (Wanted  loc) sk = Given (setCtLocOrigin loc sk)
 307 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
 308 mkGivenFlavor (Given   loc) sk = Given (setCtLocOrigin loc sk)
 309 \end{code}
 310
 311
 312 %************************************************************************
 313 %*                                                                      *
 314 %*              The TcS solver monad                                    *
 315 %*                                                                      *
 316 %************************************************************************
 317
 318 Note [The TcS monad]
 319 ~~~~~~~~~~~~~~~~~~~~
 320 The TcS monad is a weak form of the main Tc monad
 321
 322 All you can do is
 323     * fail
 324     * allocate new variables
 325     * fill in evidence variables
 326
 327 Filling in a dictionary evidence variable means to create a binding
 328 for it, so TcS carries a mutable location where the binding can be
 329 added.  This is initialised from the innermost implication constraint.
 330
 331 \begin{code}
 332 data TcSEnv
 333   = TcSEnv {
 334       tcs_ev_binds :: EvBindsVar,
 335           -- Evidence bindings
 336
 337       tcs_ty_binds :: IORef (Bag (TcTyVar, TcType)),
 338           -- Global type bindings
 339
 340       tcs_context :: SimplContext
 341     }
 342
 343 data SimplContext
 344   = SimplInfer          -- Inferring type of a let-bound thing
 345   | SimplRuleLhs        -- Inferring type of a RULE lhs
 346   | SimplInteractive    -- Inferring type at GHCi prompt
 347   | SimplCheck          -- Checking a type signature or RULE rhs
 348
 349 instance Outputable SimplContext where
 350   ppr SimplInfer       = ptext (sLit "SimplInfer")
 351   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
 352   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 353   ppr SimplCheck       = ptext (sLit "SimplCheck")
 354
 355 isInteractive :: SimplContext -> Bool
 356 isInteractive SimplInteractive = True
 357 isInteractive _                = False
 358
 359 simplEqsOnly :: SimplContext -> Bool
 360 -- Simplify equalities only, not dictionaries
 361 -- This is used for the LHS of rules; ee
 362 -- Note [Simplifying RULE lhs constraints] in TcSimplify
 363 simplEqsOnly SimplRuleLhs = True
 364 simplEqsOnly _            = False
 365
 366 performDefaulting :: SimplContext -> Bool
 367 performDefaulting SimplInfer       = False
 368 performDefaulting SimplRuleLhs     = False
 369 performDefaulting SimplInteractive = True
 370 performDefaulting SimplCheck       = True
 371
 372 ---------------
 373 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
 374
 375 instance Functor TcS where
 376   fmap f m = TcS $ fmap f . unTcS m
 377
 378 instance Monad TcS where
 379   return x  = TcS (\_ -> return x)
 380   fail err  = TcS (\_ -> fail err)
 381   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 382
 383 -- Basic functionality
 384 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 385 wrapTcS :: TcM a -> TcS a
 386 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
 387 -- and TcS is supposed to have limited functionality
 388 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
 389
 390 wrapErrTcS :: TcM a -> TcS a
 391 -- The thing wrapped should just fail
 392 -- There's no static check; it's up to the user
 393 -- Having a variant for each error message is too painful
 394 wrapErrTcS = wrapTcS
 395
 396 wrapWarnTcS :: TcM a -> TcS a
 397 -- The thing wrapped should just add a warning, or no-op
 398 -- There's no static check; it's up to the user
 399 wrapWarnTcS = wrapTcS
 400
 401 failTcS, panicTcS :: SDoc -> TcS a
 402 failTcS      = wrapTcS . TcM.failWith
 403 panicTcS doc = pprPanic "TcCanonical" doc
 404
 405 traceTcS :: String -> SDoc -> TcS ()
 406 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 407
 408 traceTcS0 :: String -> SDoc -> TcS ()
 409 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
 410
 411 runTcS :: SimplContext
 412        -> TcTyVarSet           -- Untouchables
 413        -> TcS a                -- What to run
 414        -> TcM (a, Bag EvBind)
 415 runTcS context untouch tcs
 416   = do { ty_binds_var <- TcM.newTcRef emptyBag
 417        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 418        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
 419                           , tcs_ty_binds = ty_binds_var
 420                           , tcs_context = context }
 421
 422              -- Run the computation
 423        ; res <- TcM.setUntouchables untouch (unTcS tcs env)
 424
 425              -- Perform the type unifications required
 426        ; ty_binds <- TcM.readTcRef ty_binds_var
 427        ; mapBagM_ do_unification ty_binds
 428
 429              -- And return
 430        ; ev_binds <- TcM.readTcRef evb_ref
 431        ; return (res, evBindMapBinds ev_binds) }
 432   where
 433     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 434
 435 nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a
 436 nestImplicTcS ref untouch tcs
 437   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
 438     let
 439        nest_env = TcSEnv { tcs_ev_binds = ref
 440                          , tcs_ty_binds = ty_binds
 441                          , tcs_context = ctxtUnderImplic ctxt }
 442     in
 443     TcM.setUntouchables untouch (unTcS tcs nest_env)
 444
 445 ctxtUnderImplic :: SimplContext -> SimplContext
 446 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 447 ctxtUnderImplic SimplRuleLhs = SimplCheck
 448 ctxtUnderImplic ctxt         = ctxt
 449
 450 tryTcS :: TcTyVarSet -> TcS a -> TcS a
 451 -- Like runTcS, but from within the TcS monad
 452 -- Ignore all the evidence generated, and do not affect caller's evidence!
 453 tryTcS untch tcs
 454   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyBag
 455                     ; ev_binds_var <- TcM.newTcEvBinds
 456                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 457                                      , tcs_ty_binds = ty_binds_var }
 458                     ; TcM.setUntouchables untch (unTcS tcs env1) })
 459
 460 -- Update TcEvBinds
 461 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 462
 463 getDynFlags :: TcS DynFlags
 464 getDynFlags = wrapTcS TcM.getDOpts
 465
 466 getTcSContext :: TcS SimplContext
 467 getTcSContext = TcS (return . tcs_context)
 468
 469 getTcEvBinds :: TcS EvBindsVar
 470 getTcEvBinds = TcS (return . tcs_ev_binds)
 471
 472 getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType)))
 473 getTcSTyBinds = TcS (return . tcs_ty_binds)
 474
 475 getTcEvBindsBag :: TcS EvBindMap
 476 getTcEvBindsBag
 477   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 478        ; wrapTcS $ TcM.readTcRef ev_ref }
 479
 480 setWantedCoBind :: CoVar -> Coercion -> TcS ()
 481 setWantedCoBind cv co
 482   = setEvBind cv (EvCoercion co)
 483      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
 484
 485 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
 486 setDerivedCoBind cv co
 487   = setEvBind cv (EvCoercion co)
 488
 489 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 490 -- Add a type binding
 491 setWantedTyBind tv ty
 492   = do { ref <- getTcSTyBinds
 493        ; wrapTcS $
 494          do { ty_binds <- TcM.readTcRef ref
 495             ; TcM.writeTcRef ref (ty_binds `snocBag` (tv,ty)) } }
 496
 497 setIPBind :: EvVar -> EvTerm -> TcS ()
 498 setIPBind = setEvBind
 499
 500 setDictBind :: EvVar -> EvTerm -> TcS ()
 501 setDictBind = setEvBind
 502
 503 setEvBind :: EvVar -> EvTerm -> TcS ()
 504 -- Internal
 505 setEvBind ev rhs
 506   = do { tc_evbinds <- getTcEvBinds
 507        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 508
 509 newTcEvBindsTcS :: TcS EvBindsVar
 510 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
 511
 512 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 513 warnTcS loc warn_if doc
 514   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 515   | otherwise = return ()
 516
 517 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 518 getDefaultInfo
 519   = do { ctxt <- getTcSContext
 520        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 521        ; return (ctxt, tys, flags) }
 522
 523 -- Just get some environments needed for instance looking up and matching
 524 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 525
 526 getInstEnvs :: TcS (InstEnv, InstEnv)
 527 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 528
 529 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 530 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 531
 532 getTopEnv :: TcS HscEnv
 533 getTopEnv = wrapTcS $ TcM.getTopEnv
 534
 535 getGblEnv :: TcS TcGblEnv
 536 getGblEnv = wrapTcS $ TcM.getGblEnv
 537
 538 getUntouchablesTcS :: TcS TcTyVarSet
 539 getUntouchablesTcS = wrapTcS $ TcM.getUntouchables
 540
 541 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 542 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 543
 544 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 545 checkWellStagedDFun pred dfun_id loc
 546   = wrapTcS $ TcM.setCtLoc loc $
 547     do { use_stage <- TcM.getStage
 548        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 549   where
 550     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 551     bind_lvl = TcM.topIdLvl dfun_id
 552
 553 pprEq :: TcType -> TcType -> SDoc
 554 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 555
 556 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 557 -- is touchable variable!
 558 isTouchableMetaTyVar v
 559   | isMetaTyVar v = wrapTcS $ do { untch <- TcM.isUntouchable v;
 560                                  ; return (not untch) }
 561   | otherwise     = return False
 562
 563
 564 -- Flatten skolems
 565 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 566
 567 newFlattenSkolemTy :: TcType -> TcS TcType
 568 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 569   where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 570         newFlattenSkolemTyVar ty
 571             = wrapTcS $ do { uniq <- TcM.newUnique
 572                            ; let name = mkSysTvName uniq (fsLit "f")
 573                            ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty)
 574                            }
 575
 576 -- Instantiations
 577 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 578
 579 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 580 instDFunTypes mb_inst_tys =
 581   let inst_tv :: Either TyVar TcType -> TcS Type
 582       inst_tv (Left tv)  = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy
 583       inst_tv (Right ty) = return ty
 584   in mapM inst_tv mb_inst_tys
 585
 586
 587 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 588 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 589
 590
 591 -- Superclasses and recursive dictionaries
 592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 593
 594 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
 595 newGivOrDerEvVar pty evtrm
 596   = do { ev <- wrapTcS $ TcM.newEvVar pty
 597        ; setEvBind ev evtrm
 598        ; return ev }
 599
 600 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 601 -- Note we create immutable variables for given or derived, since we
 602 -- must bind them to TcEvBinds (because their evidence may involve
 603 -- superclasses). However we should be able to override existing
 604 -- 'derived' evidence, even in TcEvBinds
 605 newGivOrDerCoVar ty1 ty2 co
 606   = do { cv <- newCoVar ty1 ty2
 607        ; setEvBind cv (EvCoercion co)
 608        ; return cv }
 609
 610 newWantedCoVar :: TcType -> TcType -> TcS EvVar
 611 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2
 612
 613 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
 614 newKindConstraint ty kind =  wrapTcS $ TcM.newKindConstraint ty kind
 615
 616 newCoVar :: TcType -> TcType -> TcS EvVar
 617 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 618
 619 newIPVar :: IPName Name -> TcType -> TcS EvVar
 620 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 621
 622 newDictVar :: Class -> [TcType] -> TcS EvVar
 623 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 624 \end{code}
 625
 626
 627 \begin{code}
 628 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
 629 -- In a call (isGoodRecEv ev wv), we are considering solving wv
 630 -- using some term that involves ev, such as:
 631 -- by setting           wv = ev
 632 -- or                   wv = EvCast x |> ev
 633 -- etc.
 634 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
 635 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
 636 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
 637 --
 638 -- Guarded means: more instance calls than superclass selections. We
 639 -- compute this by chasing the evidence, adding +1 for every instance
 640 -- call (constructor) and -1 for every superclass selection (destructor).
 641 --
 642 -- See Note [Superclasses and recursive dictionaries] in TcInteract
 643 isGoodRecEv ev_var (WantedEvVar wv _)
 644   = do { tc_evbinds <- getTcEvBindsBag
 645        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
 646        ; return $ case mb of
 647                     Nothing -> True
 648                     Just min_guardedness -> min_guardedness > 0
 649        }
 650
 651   where chase_ev_var :: EvBindMap   -- Evidence binds
 652                  -> EvVar           -- Target variable whose gravity we want to return
 653                  -> Int             -- Current gravity
 654                  -> [EvVar]         -- Visited nodes
 655                  -> EvVar           -- Current node
 656                  -> TcS (Maybe Int)
 657         chase_ev_var assocs trg curr_grav visited orig
 658             | trg == orig         = return $ Just curr_grav
 659             | orig `elem` visited = return $ Nothing
 660             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
 661             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
 662
 663 {-  No longer needed: evidence is in the EvBinds
 664             | isTcTyVar orig && isMetaTyVar orig
 665             = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
 666                  ; case meta_details of
 667                      Flexi -> return Nothing
 668                      Indirect tyco -> chase_ev assocs trg curr_grav
 669                                              (orig:visited) (EvCoercion tyco)
 670                            }
 671 -}
 672             | otherwise = return Nothing
 673
 674         chase_ev assocs trg curr_grav visited (EvId v)
 675             = chase_ev_var assocs trg curr_grav visited v
 676         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
 677             = chase_ev_var assocs trg (curr_grav-1) visited d_id
 678         chase_ev assocs trg curr_grav visited (EvCast v co)
 679             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
 680                  ; m2 <- chase_co assocs trg curr_grav visited co
 681                  ; return (comb_chase_res Nothing [m1,m2]) }
 682
 683         chase_ev assocs trg curr_grav visited (EvCoercion co)
 684             = chase_co assocs trg curr_grav visited co
 685         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
 686             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
 687                  ; return (comb_chase_res Nothing chase_results) }
 688
 689         chase_co assocs trg curr_grav visited co
 690             = -- Look for all the coercion variables in the coercion
 691               -- chase them, and combine the results. This is OK since the
 692               -- coercion will not contain any superclass terms -- anything
 693               -- that involves dictionaries will be bound in assocs.
 694               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
 695                                              (tyVarsOfType co)
 696               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
 697                     ; return (comb_chase_res Nothing chase_results) }
 698
 699         comb_chase_res f []                   = f
 700         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest
 701         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
 702         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
 703
 704
 705 -- Matching and looking up classes and family instances
 706 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 707
 708 data MatchInstResult mi
 709   = MatchInstNo         -- No matching instance
 710   | MatchInstSingle mi  -- Single matching instance
 711   | MatchInstMany       -- Multiple matching instances
 712
 713
 714 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 715 -- Look up a class constraint in the instance environment
 716 matchClass clas tys
 717   = do  { let pred = mkClassPred clas tys
 718         ; instEnvs <- getInstEnvs
 719         ; case lookupInstEnv instEnvs clas tys of {
 720             ([], unifs)               -- Nothing matches
 721                 -> do { traceTcS "matchClass not matching"
 722                                  (vcat [ text "dict" <+> ppr pred,
 723                                          text "unifs" <+> ppr unifs ])
 724                       ; return MatchInstNo
 725                       } ;
 726             ([(ispec, inst_tys)], []) -- A single match
 727                 -> do   { let dfun_id = is_dfun ispec
 728                         ; traceTcS "matchClass success"
 729                                    (vcat [text "dict" <+> ppr pred,
 730                                           text "witness" <+> ppr dfun_id
 731                                            <+> ppr (idType dfun_id) ])
 732                                   -- Record that this dfun is needed
 733                         ; record_dfun_usage dfun_id
 734                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 735                         } ;
 736             (matches, unifs)          -- More than one matches
 737                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 738                                    (vcat [text "dict" <+> ppr pred,
 739                                           text "matches" <+> ppr matches,
 740                                           text "unifs" <+> ppr unifs])
 741                         ; return MatchInstMany
 742                         }
 743         }
 744         }
 745   where record_dfun_usage :: Id -> TcS ()
 746         record_dfun_usage dfun_id
 747           = do { hsc_env <- getTopEnv
 748                ; let  dfun_name = idName dfun_id
 749                       dfun_mod  = ASSERT( isExternalName dfun_name )
 750                                   nameModule dfun_name
 751                ; if isInternalName dfun_name ||    -- Internal name => defined in this module
 752                     modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
 753                  then return () -- internal, or in another package
 754                  else do updInstUses dfun_id
 755                }
 756
 757         updInstUses :: Id -> TcS ()
 758         updInstUses dfun_id
 759             = do { tcg_env <- getGblEnv
 760                  ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
 761                                             (`addOneToNameSet` idName dfun_id)
 762                  }
 763
 764 matchFam :: TyCon
 765          -> [Type]
 766          -> TcS (MatchInstResult (TyCon, [Type]))
 767 matchFam tycon args
 768   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 769        ; case mb of
 770            Nothing  -> return MatchInstNo
 771            Just res -> return $ MatchInstSingle res
 772        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 773        -- multiple matches. Check.
 774        }
 775
 776
 777 -- Functional dependencies, instantiation of equations
 778 -------------------------------------------------------
 779
 780 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
 781                    -> TcS [WantedEvVar]
 782 mkWantedFunDepEqns _   [] = return []
 783 mkWantedFunDepEqns loc eqns
 784   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
 785        ; wevvars <- mapM to_work_item eqns
 786        ; return $ concat wevvars }
 787   where
 788     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
 789     to_work_item ((qtvs, pairs), _, _)
 790       = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs)
 791            ; mapM (do_one tenv) pairs }
 792
 793     do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1
 794                                       sty2 = substTy tenv ty2
 795                                 ; ev <- newWantedCoVar sty1 sty2
 796                                 ; return (WantedEvVar ev loc) }
 797
 798 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
 799 pprEquationDoc (eqn, (p1, _), (p2, _))
 800   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
 801 \end{code}