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