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