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 ctid =  not $ isGiven ctid || isWanted ctid
 287
 288 canRewrite :: CtFlavor -> CtFlavor -> Bool
 289 -- canRewrite ctid1 ctid2
 290 -- The constraint ctid1 can be used to rewrite ctid2
 291 canRewrite (Given {})   _            = True
 292 canRewrite (Derived {}) (Wanted {})  = True
 293 canRewrite (Derived {}) (Derived {}) = True
 294 canRewrite (Wanted {})  (Wanted {})  = True
 295 canRewrite _ _ = False
 296
 297 joinFlavors :: CtFlavor -> CtFlavor -> CtFlavor
 298 joinFlavors (Wanted loc) _  = Wanted loc
 299 joinFlavors _ (Wanted loc)  = Wanted loc
 300 joinFlavors (Derived loc) _ = Derived loc
 301 joinFlavors _ (Derived loc) = Derived loc
 302 joinFlavors (Given loc) _   = Given loc
 303
 304 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 305 mkGivenFlavor (Wanted  loc) sk = Given (setCtLocOrigin loc sk)
 306 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
 307 mkGivenFlavor (Given   loc) sk = Given (setCtLocOrigin loc sk)
 308 \end{code}
 309
 310
 311 %************************************************************************
 312 %*                                                                      *
 313 %*              The TcS solver monad                                    *
 314 %*                                                                      *
 315 %************************************************************************
 316
 317 Note [The TcS monad]
 318 ~~~~~~~~~~~~~~~~~~~~
 319 The TcS monad is a weak form of the main Tc monad
 320
 321 All you can do is
 322     * fail
 323     * allocate new variables
 324     * fill in evidence variables
 325
 326 Filling in a dictionary evidence variable means to create a binding
 327 for it, so TcS carries a mutable location where the binding can be
 328 added.  This is initialised from the innermost implication constraint.
 329
 330 \begin{code}
 331 data TcSEnv
 332   = TcSEnv {
 333       tcs_ev_binds :: EvBindsVar,
 334           -- Evidence bindings
 335
 336       tcs_ty_binds :: IORef (Bag (TcTyVar, TcType)),
 337           -- Global type bindings
 338
 339       tcs_context :: SimplContext
 340     }
 341
 342 data SimplContext
 343   = SimplInfer          -- Inferring type of a let-bound thing
 344   | SimplRuleLhs        -- Inferring type of a RULE lhs
 345   | SimplInteractive    -- Inferring type at GHCi prompt
 346   | SimplCheck          -- Checking a type signature or RULE rhs
 347
 348 instance Outputable SimplContext where
 349   ppr SimplInfer       = ptext (sLit "SimplInfer")
 350   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
 351   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 352   ppr SimplCheck       = ptext (sLit "SimplCheck")
 353
 354 isInteractive :: SimplContext -> Bool
 355 isInteractive SimplInteractive = True
 356 isInteractive _                = False
 357
 358 simplEqsOnly :: SimplContext -> Bool
 359 -- Simplify equalities only, not dictionaries
 360 -- This is used for the LHS of rules; ee
 361 -- Note [Simplifying RULE lhs constraints] in TcSimplify
 362 simplEqsOnly SimplRuleLhs = True
 363 simplEqsOnly _            = False
 364
 365 performDefaulting :: SimplContext -> Bool
 366 performDefaulting SimplInfer       = False
 367 performDefaulting SimplRuleLhs     = False
 368 performDefaulting SimplInteractive = True
 369 performDefaulting SimplCheck       = True
 370
 371 ---------------
 372 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
 373
 374 instance Functor TcS where
 375   fmap f m = TcS $ fmap f . unTcS m
 376
 377 instance Monad TcS where
 378   return x  = TcS (\_ -> return x)
 379   fail err  = TcS (\_ -> fail err)
 380   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 381
 382 -- Basic functionality
 383 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 384 wrapTcS :: TcM a -> TcS a
 385 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
 386 -- and TcS is supposed to have limited functionality
 387 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
 388
 389 wrapErrTcS :: TcM a -> TcS a
 390 -- The thing wrapped should just fail
 391 -- There's no static check; it's up to the user
 392 -- Having a variant for each error message is too painful
 393 wrapErrTcS = wrapTcS
 394
 395 wrapWarnTcS :: TcM a -> TcS a
 396 -- The thing wrapped should just add a warning, or no-op
 397 -- There's no static check; it's up to the user
 398 wrapWarnTcS = wrapTcS
 399
 400 failTcS, panicTcS :: SDoc -> TcS a
 401 failTcS      = wrapTcS . TcM.failWith
 402 panicTcS doc = pprPanic "TcCanonical" doc
 403
 404 traceTcS :: String -> SDoc -> TcS ()
 405 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 406
 407 traceTcS0 :: String -> SDoc -> TcS ()
 408 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
 409
 410 runTcS :: SimplContext
 411        -> TcTyVarSet           -- Untouchables
 412        -> TcS a                -- What to run
 413        -> TcM (a, Bag EvBind)
 414 runTcS context untouch tcs
 415   = do { ty_binds_var <- TcM.newTcRef emptyBag
 416        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 417        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
 418                           , tcs_ty_binds = ty_binds_var
 419                           , tcs_context = context }
 420
 421              -- Run the computation
 422        ; res <- TcM.setUntouchables untouch (unTcS tcs env)
 423
 424              -- Perform the type unifications required
 425        ; ty_binds <- TcM.readTcRef ty_binds_var
 426        ; mapBagM_ do_unification ty_binds
 427
 428              -- And return
 429        ; ev_binds <- TcM.readTcRef evb_ref
 430        ; return (res, evBindMapBinds ev_binds) }
 431   where
 432     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 433
 434 nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a
 435 nestImplicTcS ref untouch tcs
 436   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
 437     let
 438        nest_env = TcSEnv { tcs_ev_binds = ref
 439                          , tcs_ty_binds = ty_binds
 440                          , tcs_context = ctxtUnderImplic ctxt }
 441     in
 442     TcM.setUntouchables untouch (unTcS tcs nest_env)
 443
 444 ctxtUnderImplic :: SimplContext -> SimplContext
 445 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 446 ctxtUnderImplic SimplRuleLhs = SimplCheck
 447 ctxtUnderImplic ctxt         = ctxt
 448
 449 tryTcS :: TcTyVarSet -> TcS a -> TcS a
 450 -- Like runTcS, but from within the TcS monad
 451 -- Ignore all the evidence generated, and do not affect caller's evidence!
 452 tryTcS untch tcs
 453   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyBag
 454                     ; ev_binds_var <- TcM.newTcEvBinds
 455                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 456                                      , tcs_ty_binds = ty_binds_var }
 457                     ; TcM.setUntouchables untch (unTcS tcs env1) })
 458
 459 -- Update TcEvBinds
 460 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 461
 462 getDynFlags :: TcS DynFlags
 463 getDynFlags = wrapTcS TcM.getDOpts
 464
 465 getTcSContext :: TcS SimplContext
 466 getTcSContext = TcS (return . tcs_context)
 467
 468 getTcEvBinds :: TcS EvBindsVar
 469 getTcEvBinds = TcS (return . tcs_ev_binds)
 470
 471 getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType)))
 472 getTcSTyBinds = TcS (return . tcs_ty_binds)
 473
 474 getTcEvBindsBag :: TcS EvBindMap
 475 getTcEvBindsBag
 476   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 477        ; wrapTcS $ TcM.readTcRef ev_ref }
 478
 479 setWantedCoBind :: CoVar -> Coercion -> TcS ()
 480 setWantedCoBind cv co
 481   = setEvBind cv (EvCoercion co)
 482      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
 483
 484 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
 485 setDerivedCoBind cv co
 486   = setEvBind cv (EvCoercion co)
 487
 488 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 489 -- Add a type binding
 490 setWantedTyBind tv ty
 491   = do { ref <- getTcSTyBinds
 492        ; wrapTcS $
 493          do { ty_binds <- TcM.readTcRef ref
 494             ; TcM.writeTcRef ref (ty_binds `snocBag` (tv,ty)) } }
 495
 496 setIPBind :: EvVar -> EvTerm -> TcS ()
 497 setIPBind = setEvBind
 498
 499 setDictBind :: EvVar -> EvTerm -> TcS ()
 500 setDictBind = setEvBind
 501
 502 setEvBind :: EvVar -> EvTerm -> TcS ()
 503 -- Internal
 504 setEvBind ev rhs
 505   = do { tc_evbinds <- getTcEvBinds
 506        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 507
 508 newTcEvBindsTcS :: TcS EvBindsVar
 509 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
 510
 511 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 512 warnTcS loc warn_if doc
 513   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 514   | otherwise = return ()
 515
 516 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 517 getDefaultInfo
 518   = do { ctxt <- getTcSContext
 519        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 520        ; return (ctxt, tys, flags) }
 521
 522 -- Just get some environments needed for instance looking up and matching
 523 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 524
 525 getInstEnvs :: TcS (InstEnv, InstEnv)
 526 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 527
 528 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 529 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 530
 531 getTopEnv :: TcS HscEnv
 532 getTopEnv = wrapTcS $ TcM.getTopEnv
 533
 534 getGblEnv :: TcS TcGblEnv
 535 getGblEnv = wrapTcS $ TcM.getGblEnv
 536
 537 getUntouchablesTcS :: TcS TcTyVarSet
 538 getUntouchablesTcS = wrapTcS $ TcM.getUntouchables
 539
 540 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 541 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 542
 543 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 544 checkWellStagedDFun pred dfun_id loc
 545   = wrapTcS $ TcM.setCtLoc loc $
 546     do { use_stage <- TcM.getStage
 547        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 548   where
 549     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 550     bind_lvl = TcM.topIdLvl dfun_id
 551
 552 pprEq :: TcType -> TcType -> SDoc
 553 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 554
 555 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 556 -- is touchable variable!
 557 isTouchableMetaTyVar v
 558   | isMetaTyVar v = wrapTcS $ do { untch <- TcM.isUntouchable v;
 559                                  ; return (not untch) }
 560   | otherwise     = return False
 561
 562
 563 -- Flatten skolems
 564 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 565
 566 newFlattenSkolemTy :: TcType -> TcS TcType
 567 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 568   where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 569         newFlattenSkolemTyVar ty
 570             = wrapTcS $ do { uniq <- TcM.newUnique
 571                            ; let name = mkSysTvName uniq (fsLit "f")
 572                            ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty)
 573                            }
 574
 575 -- Instantiations
 576 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 577
 578 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 579 instDFunTypes mb_inst_tys =
 580   let inst_tv :: Either TyVar TcType -> TcS Type
 581       inst_tv (Left tv)  = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy
 582       inst_tv (Right ty) = return ty
 583   in mapM inst_tv mb_inst_tys
 584
 585
 586 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 587 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 588
 589
 590 -- Superclasses and recursive dictionaries
 591 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 592
 593 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
 594 newGivOrDerEvVar pty evtrm
 595   = do { ev <- wrapTcS $ TcM.newEvVar pty
 596        ; setEvBind ev evtrm
 597        ; return ev }
 598
 599 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 600 -- Note we create immutable variables for given or derived, since we
 601 -- must bind them to TcEvBinds (because their evidence may involve
 602 -- superclasses). However we should be able to override existing
 603 -- 'derived' evidence, even in TcEvBinds
 604 newGivOrDerCoVar ty1 ty2 co
 605   = do { cv <- newCoVar ty1 ty2
 606        ; setEvBind cv (EvCoercion co)
 607        ; return cv }
 608
 609 newWantedCoVar :: TcType -> TcType -> TcS EvVar
 610 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2
 611
 612 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
 613 newKindConstraint ty kind =  wrapTcS $ TcM.newKindConstraint ty kind
 614
 615 newCoVar :: TcType -> TcType -> TcS EvVar
 616 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 617
 618 newIPVar :: IPName Name -> TcType -> TcS EvVar
 619 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 620
 621 newDictVar :: Class -> [TcType] -> TcS EvVar
 622 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 623 \end{code}
 624
 625
 626 \begin{code}
 627 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
 628 -- In a call (isGoodRecEv ev wv), we are considering solving wv
 629 -- using some term that involves ev, such as:
 630 -- by setting           wv = ev
 631 -- or                   wv = EvCast x |> ev
 632 -- etc.
 633 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
 634 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
 635 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
 636 --
 637 -- Guarded means: more instance calls than superclass selections. We
 638 -- compute this by chasing the evidence, adding +1 for every instance
 639 -- call (constructor) and -1 for every superclass selection (destructor).
 640 --
 641 -- See Note [Superclasses and recursive dictionaries] in TcInteract
 642 isGoodRecEv ev_var (WantedEvVar wv _)
 643   = do { tc_evbinds <- getTcEvBindsBag
 644        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
 645        ; return $ case mb of
 646                     Nothing -> True
 647                     Just min_guardedness -> min_guardedness > 0
 648        }
 649
 650   where chase_ev_var :: EvBindMap   -- Evidence binds
 651                  -> EvVar           -- Target variable whose gravity we want to return
 652                  -> Int             -- Current gravity
 653                  -> [EvVar]         -- Visited nodes
 654                  -> EvVar           -- Current node
 655                  -> TcS (Maybe Int)
 656         chase_ev_var assocs trg curr_grav visited orig
 657             | trg == orig         = return $ Just curr_grav
 658             | orig `elem` visited = return $ Nothing
 659             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
 660             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
 661
 662 {-  No longer needed: evidence is in the EvBinds
 663             | isTcTyVar orig && isMetaTyVar orig
 664             = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
 665                  ; case meta_details of
 666                      Flexi -> return Nothing
 667                      Indirect tyco -> chase_ev assocs trg curr_grav
 668                                              (orig:visited) (EvCoercion tyco)
 669                            }
 670 -}
 671             | otherwise = return Nothing
 672
 673         chase_ev assocs trg curr_grav visited (EvId v)
 674             = chase_ev_var assocs trg curr_grav visited v
 675         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
 676             = chase_ev_var assocs trg (curr_grav-1) visited d_id
 677         chase_ev assocs trg curr_grav visited (EvCast v co)
 678             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
 679                  ; m2 <- chase_co assocs trg curr_grav visited co
 680                  ; return (comb_chase_res Nothing [m1,m2]) }
 681
 682         chase_ev assocs trg curr_grav visited (EvCoercion co)
 683             = chase_co assocs trg curr_grav visited co
 684         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
 685             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
 686                  ; return (comb_chase_res Nothing chase_results) }
 687
 688         chase_co assocs trg curr_grav visited co
 689             = -- Look for all the coercion variables in the coercion
 690               -- chase them, and combine the results. This is OK since the
 691               -- coercion will not contain any superclass terms -- anything
 692               -- that involves dictionaries will be bound in assocs.
 693               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
 694                                              (tyVarsOfType co)
 695               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
 696                     ; return (comb_chase_res Nothing chase_results) }
 697
 698         comb_chase_res f []                   = f
 699         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest
 700         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
 701         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
 702
 703
 704 -- Matching and looking up classes and family instances
 705 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 706
 707 data MatchInstResult mi
 708   = MatchInstNo         -- No matching instance
 709   | MatchInstSingle mi  -- Single matching instance
 710   | MatchInstMany       -- Multiple matching instances
 711
 712
 713 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 714 -- Look up a class constraint in the instance environment
 715 matchClass clas tys
 716   = do  { let pred = mkClassPred clas tys
 717         ; instEnvs <- getInstEnvs
 718         ; case lookupInstEnv instEnvs clas tys of {
 719             ([], unifs)               -- Nothing matches
 720                 -> do { traceTcS "matchClass not matching"
 721                                  (vcat [ text "dict" <+> ppr pred,
 722                                          text "unifs" <+> ppr unifs ])
 723                       ; return MatchInstNo
 724                       } ;
 725             ([(ispec, inst_tys)], []) -- A single match
 726                 -> do   { let dfun_id = is_dfun ispec
 727                         ; traceTcS "matchClass success"
 728                                    (vcat [text "dict" <+> ppr pred,
 729                                           text "witness" <+> ppr dfun_id
 730                                            <+> ppr (idType dfun_id) ])
 731                                   -- Record that this dfun is needed
 732                         ; record_dfun_usage dfun_id
 733                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 734                         } ;
 735             (matches, unifs)          -- More than one matches
 736                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 737                                    (vcat [text "dict" <+> ppr pred,
 738                                           text "matches" <+> ppr matches,
 739                                           text "unifs" <+> ppr unifs])
 740                         ; return MatchInstMany
 741                         }
 742         }
 743         }
 744   where record_dfun_usage :: Id -> TcS ()
 745         record_dfun_usage dfun_id
 746           = do { hsc_env <- getTopEnv
 747                ; let  dfun_name = idName dfun_id
 748                       dfun_mod  = ASSERT( isExternalName dfun_name )
 749                                   nameModule dfun_name
 750                ; if isInternalName dfun_name ||    -- Internal name => defined in this module
 751                     modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
 752                  then return () -- internal, or in another package
 753                  else do updInstUses dfun_id
 754                }
 755
 756         updInstUses :: Id -> TcS ()
 757         updInstUses dfun_id
 758             = do { tcg_env <- getGblEnv
 759                  ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
 760                                             (`addOneToNameSet` idName dfun_id)
 761                  }
 762
 763 matchFam :: TyCon
 764          -> [Type]
 765          -> TcS (MatchInstResult (TyCon, [Type]))
 766 matchFam tycon args
 767   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 768        ; case mb of
 769            Nothing  -> return MatchInstNo
 770            Just res -> return $ MatchInstSingle res
 771        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 772        -- multiple matches. Check.
 773        }
 774
 775
 776 -- Functional dependencies, instantiation of equations
 777 -------------------------------------------------------
 778
 779 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
 780                    -> TcS [WantedEvVar]
 781 mkWantedFunDepEqns _   [] = return []
 782 mkWantedFunDepEqns loc eqns
 783   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
 784        ; wevvars <- mapM to_work_item eqns
 785        ; return $ concat wevvars }
 786   where
 787     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
 788     to_work_item ((qtvs, pairs), _, _)
 789       = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs)
 790            ; mapM (do_one tenv) pairs }
 791
 792     do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1
 793                                       sty2 = substTy tenv ty2
 794                                 ; ev <- newWantedCoVar sty1 sty2
 795                                 ; return (WantedEvVar ev loc) }
 796
 797 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
 798 pprEquationDoc (eqn, (p1, _), (p2, _))
 799   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
 800 \end{code}