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