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