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