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, isCTyEqCan,
   8     isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
   9     isCFrozenErr,
  10
  11     WorkList, unionWorkList, unionWorkLists, isEmptyWorkList, emptyWorkList,
  12     workListFromEq, workListFromNonEq,
  13     workListFromEqs, workListFromNonEqs, foldrWorkListM,
  14
  15     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
  16     deCanonicalise, mkFrozenError,
  17
  18     isWanted, isGivenOrSolved, isDerived,
  19     isGivenOrSolvedCt, isGivenCt_maybe,
  20     isWantedCt, isDerivedCt, pprFlavorArising,
  21
  22     isFlexiTcsTv,
  23
  24     canRewrite, canSolve,
  25     combineCtLoc, mkSolvedFlavor, mkGivenFlavor,
  26     mkWantedFlavor,
  27     getWantedLoc,
  28
  29     TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
  30     traceFireTcS, bumpStepCountTcS,
  31     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
  32     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
  33
  34        -- Creation of evidence variables
  35     newEvVar, newCoVar, newGivenCoVar,
  36     newDerivedId,
  37     newIPVar, newDictVar, newKindConstraint,
  38
  39        -- Setting evidence variables
  40     setCoBind, setIPBind, setDictBind, setEvBind,
  41
  42     setWantedTyBind,
  43
  44     lookupFlatCacheMap, updateFlatCacheMap,
  45
  46     getInstEnvs, getFamInstEnvs,                -- Getting the environments
  47     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
  48     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
  49
  50     newFlattenSkolemTy,                         -- Flatten skolems
  51
  52
  53     instDFunTypes,                              -- Instantiation
  54     instDFunConstraints,
  55     newFlexiTcSTy, instFlexiTcS,
  56
  57     compatKind,
  58
  59     TcsUntouchables,
  60     isTouchableMetaTyVar,
  61     isTouchableMetaTyVar_InRange,
  62
  63     getDefaultInfo, getDynFlags,
  64
  65     matchClass, matchFam, MatchInstResult (..),
  66     checkWellStagedDFun,
  67     warnTcS,
  68     pprEq                                   -- Smaller utils, re-exported from TcM
  69                                              -- TODO (DV): these are only really used in the
  70                                              -- instance matcher in TcSimplify. I am wondering
  71                                              -- if the whole instance matcher simply belongs
  72                                              -- here
  73 ) where
  74
  75 #include "HsVersions.h"
  76
  77 import HscTypes
  78 import BasicTypes
  79
  80 import Inst
  81 import InstEnv
  82 import FamInst
  83 import FamInstEnv
  84
  85 import qualified TcRnMonad as TcM
  86 import qualified TcMType as TcM
  87 import qualified TcEnv as TcM
  88        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
  89 import TcType
  90 import DynFlags
  91
  92 import Coercion
  93 import Class
  94 import TyCon
  95 import TypeRep
  96
  97 import Name
  98 import Var
  99 import VarEnv
 100 import Outputable
 101 import Bag
 102 import MonadUtils
 103 import VarSet
 104 import FastString
 105
 106 import HsBinds               -- for TcEvBinds stuff
 107 import Id
 108 import TcRnTypes
 109 import Data.IORef
 110
 111 import qualified Data.Map as Map
 112
 113 #ifdef DEBUG
 114 import StaticFlags( opt_PprStyle_Debug )
 115 import Control.Monad( when )
 116 #endif
 117 \end{code}
 118
 119
 120 %************************************************************************
 121 %*                                                                      *
 122 %*                       Canonical constraints                          *
 123 %*                                                                      *
 124 %*   These are the constraints the low-level simplifier works with      *
 125 %*                                                                      *
 126 %************************************************************************
 127
 128 \begin{code}
 129 -- Types without any type functions inside.  However, note that xi
 130 -- types CAN contain unexpanded type synonyms; however, the
 131 -- (transitive) expansions of those type synonyms will not contain any
 132 -- type functions.
 133 type Xi = Type       -- In many comments, "xi" ranges over Xi
 134
 135 type CanonicalCts = Bag CanonicalCt
 136
 137 data CanonicalCt
 138   -- Atomic canonical constraints
 139   = CDictCan {  -- e.g.  Num xi
 140       cc_id     :: EvVar,
 141       cc_flavor :: CtFlavor,
 142       cc_class  :: Class,
 143       cc_tyargs :: [Xi]
 144     }
 145
 146   | CIPCan {    -- ?x::tau
 147       -- See note [Canonical implicit parameter constraints].
 148       cc_id     :: EvVar,
 149       cc_flavor :: CtFlavor,
 150       cc_ip_nm  :: IPName Name,
 151       cc_ip_ty  :: TcTauType
 152     }
 153
 154   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
 155        -- Invariant:
 156        --   * tv not in tvs(xi)   (occurs check)
 157        --   * typeKind xi `compatKind` typeKind tv
 158        --       See Note [Spontaneous solving and kind compatibility]
 159        --   * We prefer unification variables on the left *JUST* for efficiency
 160       cc_id     :: EvVar,
 161       cc_flavor :: CtFlavor,
 162       cc_tyvar  :: TcTyVar,
 163       cc_rhs    :: Xi
 164     }
 165
 166   | CFunEqCan {  -- F xis ~ xi
 167                  -- Invariant: * isSynFamilyTyCon cc_fun
 168                  --            * typeKind (F xis) `compatKind` typeKind xi
 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   | CFrozenErr {      -- A "frozen error" does not interact with anything
 179                       -- See Note [Frozen Errors]
 180       cc_id     :: EvVar,
 181       cc_flavor :: CtFlavor
 182     }
 183
 184 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
 185 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
 186
 187 compatKind :: Kind -> Kind -> Bool
 188 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
 189
 190 deCanonicalise :: CanonicalCt -> FlavoredEvVar
 191 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
 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 tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
 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   ppr (CFrozenErr co fl)
 220       = ppr fl <+> pprEvVarWithType co
 221 \end{code}
 222
 223 Note [Canonical implicit parameter constraints]
 224 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 225 The type in a canonical implicit parameter constraint doesn't need to
 226 be a xi (type-function-free type) since we can defer the flattening
 227 until checking this type for equality with another type.  If we
 228 encounter two IP constraints with the same name, they MUST have the
 229 same type, and at that point we can generate a flattened equality
 230 constraint between the types.  (On the other hand, the types in two
 231 class constraints for the same class MAY be equal, so they need to be
 232 flattened in the first place to facilitate comparing them.)
 233
 234 \begin{code}
 235 singleCCan :: CanonicalCt -> CanonicalCts
 236 singleCCan = unitBag
 237
 238 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
 239 andCCan = unionBags
 240
 241 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
 242 extendCCans = snocBag
 243
 244 andCCans :: [CanonicalCts] -> CanonicalCts
 245 andCCans = unionManyBags
 246
 247 emptyCCan :: CanonicalCts
 248 emptyCCan = emptyBag
 249
 250 isEmptyCCan :: CanonicalCts -> Bool
 251 isEmptyCCan = isEmptyBag
 252
 253 isCTyEqCan :: CanonicalCt -> Bool
 254 isCTyEqCan (CTyEqCan {})  = True
 255 isCTyEqCan (CFunEqCan {}) = False
 256 isCTyEqCan _              = False
 257
 258 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
 259 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
 260 isCDictCan_Maybe _              = Nothing
 261
 262 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
 263 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
 264 isCIPCan_Maybe _                = Nothing
 265
 266 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
 267 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
 268 isCFunEqCan_Maybe _ = Nothing
 269
 270 isCFrozenErr :: CanonicalCt -> Bool
 271 isCFrozenErr (CFrozenErr {}) = True
 272 isCFrozenErr _               = False
 273
 274
 275 -- A mixture of Given, Wanted, and Derived constraints.
 276 -- We split between equalities and the rest to process equalities first.
 277 data WorkList = WorkList { weqs  :: CanonicalCts
 278                                  -- NB: weqs includes equalities /and/ family equalities
 279                          , wrest :: CanonicalCts }
 280
 281 unionWorkList :: WorkList -> WorkList -> WorkList
 282 unionWorkList wl1 wl2
 283   = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
 284              , wrest = wrest wl1 `andCCan` wrest wl2 }
 285
 286 unionWorkLists :: [WorkList] -> WorkList
 287 unionWorkLists = foldr unionWorkList emptyWorkList
 288
 289 isEmptyWorkList :: WorkList -> Bool
 290 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
 291
 292 emptyWorkList :: WorkList
 293 emptyWorkList
 294   = WorkList { weqs = emptyBag, wrest = emptyBag }
 295
 296 workListFromEq :: CanonicalCt -> WorkList
 297 workListFromEq = workListFromEqs . singleCCan
 298
 299 workListFromNonEq :: CanonicalCt -> WorkList
 300 workListFromNonEq = workListFromNonEqs . singleCCan
 301
 302 workListFromNonEqs :: CanonicalCts -> WorkList
 303 workListFromNonEqs cts
 304   = WorkList { weqs = emptyCCan, wrest = cts }
 305
 306 workListFromEqs :: CanonicalCts -> WorkList
 307 workListFromEqs cts
 308   = WorkList { weqs = cts, wrest = emptyCCan }
 309
 310 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
 311                            -> r -> WorkList -> m r
 312 -- Prioritizes equalities
 313 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
 314   = do { r1 <- foldrBagM on_ct r eqs
 315        ; foldrBagM on_ct r1 rest }
 316
 317 instance Outputable WorkList where
 318   ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
 319                 , text "WorkList (Other)      = " <+> ppr (wrest wl) ]
 320
 321 \end{code}
 322
 323
 324
 325 %************************************************************************
 326 %*                                                                      *
 327                     CtFlavor
 328          The "flavor" of a canonical constraint
 329 %*                                                                      *
 330 %************************************************************************
 331
 332 \begin{code}
 333 getWantedLoc :: CanonicalCt -> WantedLoc
 334 getWantedLoc ct
 335   = ASSERT (isWanted (cc_flavor ct))
 336     case cc_flavor ct of
 337       Wanted wl -> wl
 338       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
 339
 340 isWantedCt :: CanonicalCt -> Bool
 341 isWantedCt ct = isWanted (cc_flavor ct)
 342 isDerivedCt :: CanonicalCt -> Bool
 343 isDerivedCt ct = isDerived (cc_flavor ct)
 344
 345 isGivenCt_maybe :: CanonicalCt -> Maybe GivenKind
 346 isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct)
 347
 348 isGivenOrSolvedCt :: CanonicalCt -> Bool
 349 isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct)
 350
 351
 352 canSolve :: CtFlavor -> CtFlavor -> Bool
 353 -- canSolve ctid1 ctid2
 354 -- The constraint ctid1 can be used to solve ctid2
 355 -- "to solve" means a reaction where the active parts of the two constraints match.
 356 --  active(F xis ~ xi) = F xis
 357 --  active(tv ~ xi)    = tv
 358 --  active(D xis)      = D xis
 359 --  active(IP nm ty)   = nm
 360 --
 361 -- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
 362 -----------------------------------------
 363 canSolve (Given {})   _            = True
 364 canSolve (Wanted {})  (Derived {}) = True
 365 canSolve (Wanted {})  (Wanted {})  = True
 366 canSolve (Derived {}) (Derived {}) = True  -- Important: derived can't solve wanted/given
 367 canSolve _ _ = False                       -- (There is no *evidence* for a derived.)
 368
 369 canRewrite :: CtFlavor -> CtFlavor -> Bool
 370 -- canRewrite ctid1 ctid2
 371 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
 372 canRewrite = canSolve
 373
 374 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
 375 -- Precondition: At least one of them should be wanted
 376 combineCtLoc (Wanted loc) _    = loc
 377 combineCtLoc _ (Wanted loc)    = loc
 378 combineCtLoc (Derived loc ) _  = loc
 379 combineCtLoc _ (Derived loc )  = loc
 380 combineCtLoc _ _ = panic "combineCtLoc: both given"
 381
 382 mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 383 -- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
 384 mkSolvedFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk) GivenSolved
 385 mkSolvedFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk) GivenSolved
 386 mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
 387
 388 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 389 mkGivenFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk) GivenOrig
 390 mkGivenFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk) GivenOrig
 391 mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
 392
 393 mkWantedFlavor :: CtFlavor -> CtFlavor
 394 mkWantedFlavor (Wanted  loc) = Wanted loc
 395 mkWantedFlavor (Derived loc) = Wanted loc
 396 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl)
 397 \end{code}
 398
 399 %************************************************************************
 400 %*                                                                      *
 401 %*              The TcS solver monad                                    *
 402 %*                                                                      *
 403 %************************************************************************
 404
 405 Note [The TcS monad]
 406 ~~~~~~~~~~~~~~~~~~~~
 407 The TcS monad is a weak form of the main Tc monad
 408
 409 All you can do is
 410     * fail
 411     * allocate new variables
 412     * fill in evidence variables
 413
 414 Filling in a dictionary evidence variable means to create a binding
 415 for it, so TcS carries a mutable location where the binding can be
 416 added.  This is initialised from the innermost implication constraint.
 417
 418 \begin{code}
 419 data TcSEnv
 420   = TcSEnv {
 421       tcs_ev_binds :: EvBindsVar,
 422           -- Evidence bindings
 423
 424       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
 425           -- Global type bindings
 426
 427       tcs_context :: SimplContext,
 428
 429       tcs_untch :: TcsUntouchables,
 430
 431       tcs_ic_depth   :: Int,       -- Implication nesting depth
 432       tcs_count      :: IORef Int, -- Global step count
 433
 434       tcs_flat_map   :: IORef FlatCache
 435     }
 436
 437 data FlatCache
 438   = FlatCache { givenFlatCache  :: Map.Map FunEqHead (TcType,Coercion,CtFlavor)
 439                 -- Invariant: all CtFlavors here satisfy isGiven
 440               , wantedFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor) }
 441                 -- Invariant: all CtFlavors here satisfy isWanted
 442
 443 emptyFlatCache :: FlatCache
 444 emptyFlatCache
 445  = FlatCache { givenFlatCache  = Map.empty, wantedFlatCache = Map.empty }
 446
 447 newtype FunEqHead = FunEqHead (TyCon,[Xi])
 448
 449 instance Eq FunEqHead where
 450   FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && tcEqTypes xis1 xis2
 451
 452 instance Ord FunEqHead where
 453   FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2)
 454     = case compare tc1 tc2 of
 455         EQ    -> tcCmpTypes xis1 xis2
 456         other -> other
 457
 458 type TcsUntouchables = (Untouchables,TcTyVarSet)
 459 -- Like the TcM Untouchables,
 460 -- but records extra TcsTv variables generated during simplification
 461 -- See Note [Extra TcsTv untouchables] in TcSimplify
 462 \end{code}
 463
 464 \begin{code}
 465 data SimplContext
 466   = SimplInfer SDoc        -- Inferring type of a let-bound thing
 467   | SimplRuleLhs RuleName  -- Inferring type of a RULE lhs
 468   | SimplInteractive       -- Inferring type at GHCi prompt
 469   | SimplCheck SDoc        -- Checking a type signature or RULE rhs
 470
 471 instance Outputable SimplContext where
 472   ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
 473   ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
 474   ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
 475   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 476
 477 isInteractive :: SimplContext -> Bool
 478 isInteractive SimplInteractive = True
 479 isInteractive _                = False
 480
 481 simplEqsOnly :: SimplContext -> Bool
 482 -- Simplify equalities only, not dictionaries
 483 -- This is used for the LHS of rules; ee
 484 -- Note [Simplifying RULE lhs constraints] in TcSimplify
 485 simplEqsOnly (SimplRuleLhs {}) = True
 486 simplEqsOnly _                 = False
 487
 488 performDefaulting :: SimplContext -> Bool
 489 performDefaulting (SimplInfer {})   = False
 490 performDefaulting (SimplRuleLhs {}) = False
 491 performDefaulting SimplInteractive  = True
 492 performDefaulting (SimplCheck {})   = True
 493
 494 ---------------
 495 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
 496
 497 instance Functor TcS where
 498   fmap f m = TcS $ fmap f . unTcS m
 499
 500 instance Monad TcS where
 501   return x  = TcS (\_ -> return x)
 502   fail err  = TcS (\_ -> fail err)
 503   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 504
 505 -- Basic functionality
 506 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 507 wrapTcS :: TcM a -> TcS a
 508 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
 509 -- and TcS is supposed to have limited functionality
 510 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
 511
 512 wrapErrTcS :: TcM a -> TcS a
 513 -- The thing wrapped should just fail
 514 -- There's no static check; it's up to the user
 515 -- Having a variant for each error message is too painful
 516 wrapErrTcS = wrapTcS
 517
 518 wrapWarnTcS :: TcM a -> TcS a
 519 -- The thing wrapped should just add a warning, or no-op
 520 -- There's no static check; it's up to the user
 521 wrapWarnTcS = wrapTcS
 522
 523 failTcS, panicTcS :: SDoc -> TcS a
 524 failTcS      = wrapTcS . TcM.failWith
 525 panicTcS doc = pprPanic "TcCanonical" doc
 526
 527 traceTcS :: String -> SDoc -> TcS ()
 528 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 529
 530 bumpStepCountTcS :: TcS ()
 531 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
 532                                     ; n <- TcM.readTcRef ref
 533                                     ; TcM.writeTcRef ref (n+1) }
 534
 535 traceFireTcS :: Int -> SDoc -> TcS ()
 536 -- Dump a rule-firing trace
 537 traceFireTcS depth doc
 538   = TcS $ \env ->
 539     TcM.ifDOptM Opt_D_dump_cs_trace $
 540     do { n <- TcM.readTcRef (tcs_count env)
 541        ; let msg = int n
 542                 <> text (replicate (tcs_ic_depth env) '>')
 543                 <> brackets (int depth) <+> doc
 544        ; TcM.dumpTcRn msg }
 545
 546 runTcS :: SimplContext
 547        -> Untouchables         -- Untouchables
 548        -> TcS a                -- What to run
 549        -> TcM (a, Bag EvBind)
 550 runTcS context untouch tcs
 551   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 552        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 553        ; step_count <- TcM.newTcRef 0
 554        ; flat_cache_var <- TcM.newTcRef emptyFlatCache
 555        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
 556                           , tcs_ty_binds = ty_binds_var
 557                           , tcs_context  = context
 558                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
 559                           , tcs_count    = step_count
 560                           , tcs_ic_depth = 0
 561                           , tcs_flat_map = flat_cache_var
 562                           }
 563
 564              -- Run the computation
 565        ; res <- unTcS tcs env
 566              -- Perform the type unifications required
 567        ; ty_binds <- TcM.readTcRef ty_binds_var
 568        ; mapM_ do_unification (varEnvElts ty_binds)
 569
 570 #ifdef DEBUG
 571        ; count <- TcM.readTcRef step_count
 572        ; when (opt_PprStyle_Debug && count > 0) $
 573          TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
 574                             <+> int count <+> ppr context)
 575 #endif
 576              -- And return
 577        ; ev_binds      <- TcM.readTcRef evb_ref
 578        ; return (res, evBindMapBinds ev_binds) }
 579   where
 580     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 581
 582 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
 583 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
 584   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
 585                    , tcs_untch = (_outer_range, outer_tcs)
 586                    , tcs_count = count
 587                    , tcs_ic_depth = idepth
 588                    , tcs_context = ctxt
 589                    , tcs_flat_map = orig_flat_cache_var
 590                    } ->
 591     do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
 592                    -- The inner_range should be narrower than the outer one
 593                    -- (thus increasing the set of untouchables) but
 594                    -- the inner Tcs-untouchables must be unioned with the
 595                    -- outer ones!
 596
 597        ; orig_flat_cache <- TcM.readTcRef orig_flat_cache_var
 598        ; flat_cache_var  <- TcM.newTcRef orig_flat_cache -- emptyFlatCache
 599
 600                             -- Consider copying the results the tcs_flat_map of the
 601                             -- incomping constraint, but we must make sure that we
 602                             -- have pushed everything in, which seems somewhat fragile
 603        ; let nest_env = TcSEnv { tcs_ev_binds = ref
 604                                , tcs_ty_binds = ty_binds
 605                                , tcs_untch    = inner_untch
 606                                , tcs_count    = count
 607                                , tcs_ic_depth = idepth+1
 608                                , tcs_context  = ctxtUnderImplic ctxt
 609                                , tcs_flat_map = flat_cache_var }
 610        ; thing_inside nest_env }
 611
 612 recoverTcS :: TcS a -> TcS a -> TcS a
 613 recoverTcS (TcS recovery_code) (TcS thing_inside)
 614   = TcS $ \ env ->
 615     TcM.recoverM (recovery_code env) (thing_inside env)
 616
 617 ctxtUnderImplic :: SimplContext -> SimplContext
 618 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 619 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
 620                                                <+> doubleQuotes (ftext n))
 621 ctxtUnderImplic ctxt              = ctxt
 622
 623 tryTcS :: TcS a -> TcS a
 624 -- Like runTcS, but from within the TcS monad
 625 -- Ignore all the evidence generated, and do not affect caller's evidence!
 626 tryTcS tcs
 627   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 628                     ; ev_binds_var <- TcM.newTcEvBinds
 629                     ; flat_cache_var <- TcM.newTcRef emptyFlatCache
 630                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 631                                      , tcs_ty_binds = ty_binds_var
 632                                      , tcs_flat_map = flat_cache_var }
 633                    ; unTcS tcs env1 })
 634
 635 -- Update TcEvBinds
 636 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 637
 638 getDynFlags :: TcS DynFlags
 639 getDynFlags = wrapTcS TcM.getDOpts
 640
 641 getTcSContext :: TcS SimplContext
 642 getTcSContext = TcS (return . tcs_context)
 643
 644 getTcEvBinds :: TcS EvBindsVar
 645 getTcEvBinds = TcS (return . tcs_ev_binds)
 646
 647 getUntouchables :: TcS TcsUntouchables
 648 getUntouchables = TcS (return . tcs_untch)
 649
 650 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
 651 getTcSTyBinds = TcS (return . tcs_ty_binds)
 652
 653 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
 654 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
 655
 656 getFlatCacheMapVar :: TcS (IORef FlatCache)
 657 getFlatCacheMapVar
 658   = TcS (return . tcs_flat_map)
 659
 660 lookupFlatCacheMap :: TyCon -> [Xi] -> CtFlavor
 661                    -> TcS (Maybe (TcType,Coercion,CtFlavor))
 662 -- For givens, we lookup in given flat cache
 663 lookupFlatCacheMap tc xis (Given {})
 664   = do { cache_ref <- getFlatCacheMapVar
 665        ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
 666        ; return $ Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) }
 667 -- For wanteds, we first lookup in givenFlatCache.
 668 -- If we get nothing back then we lookup in wantedFlatCache.
 669 lookupFlatCacheMap tc xis (Wanted {})
 670   = do { cache_ref <- getFlatCacheMapVar
 671        ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
 672        ; case Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) of
 673            Nothing -> return $ Map.lookup (FunEqHead (tc,xis)) (wantedFlatCache cache_map)
 674            other   -> return other }
 675 lookupFlatCacheMap _tc _xis (Derived {}) = return Nothing
 676
 677 updateFlatCacheMap :: TyCon -> [Xi]
 678                    -> TcType -> CtFlavor -> Coercion -> TcS ()
 679 updateFlatCacheMap _tc _xis _tv (Derived {}) _co
 680   = return () -- Not caching deriveds
 681 updateFlatCacheMap tc xis ty fl co
 682   = do { cache_ref <- getFlatCacheMapVar
 683        ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
 684        ; let new_cache_map
 685               | isGivenOrSolved fl
 686               = cache_map { givenFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
 687                                              givenFlatCache cache_map }
 688               | isWanted fl
 689               = cache_map { wantedFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
 690                                               wantedFlatCache cache_map }
 691               | otherwise = pprPanic "updateFlatCacheMap, met Derived!" $ empty
 692        ; wrapTcS $ TcM.writeTcRef cache_ref new_cache_map }
 693
 694
 695 getTcEvBindsBag :: TcS EvBindMap
 696 getTcEvBindsBag
 697   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 698        ; wrapTcS $ TcM.readTcRef ev_ref }
 699
 700
 701 setCoBind :: CoVar -> Coercion -> TcS ()
 702 setCoBind cv co = setEvBind cv (EvCoercion co)
 703
 704 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 705 -- Add a type binding
 706 -- We never do this twice!
 707 setWantedTyBind tv ty
 708   = do { ref <- getTcSTyBinds
 709        ; wrapTcS $
 710          do { ty_binds <- TcM.readTcRef ref
 711 #ifdef DEBUG
 712             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
 713               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
 714                    , ppr tv <+> text ":=" <+> ppr ty
 715                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
 716 #endif
 717             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
 718
 719 setIPBind :: EvVar -> EvTerm -> TcS ()
 720 setIPBind = setEvBind
 721
 722 setDictBind :: EvVar -> EvTerm -> TcS ()
 723 setDictBind = setEvBind
 724
 725 setEvBind :: EvVar -> EvTerm -> TcS ()
 726 -- Internal
 727 setEvBind ev rhs
 728   = do { tc_evbinds <- getTcEvBinds
 729        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 730
 731 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 732 warnTcS loc warn_if doc
 733   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 734   | otherwise = return ()
 735
 736 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 737 getDefaultInfo
 738   = do { ctxt <- getTcSContext
 739        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 740        ; return (ctxt, tys, flags) }
 741
 742 -- Just get some environments needed for instance looking up and matching
 743 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 744
 745 getInstEnvs :: TcS (InstEnv, InstEnv)
 746 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 747
 748 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 749 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 750
 751 getTopEnv :: TcS HscEnv
 752 getTopEnv = wrapTcS $ TcM.getTopEnv
 753
 754 getGblEnv :: TcS TcGblEnv
 755 getGblEnv = wrapTcS $ TcM.getGblEnv
 756
 757 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 758 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 759
 760 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 761 checkWellStagedDFun pred dfun_id loc
 762   = wrapTcS $ TcM.setCtLoc loc $
 763     do { use_stage <- TcM.getStage
 764        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 765   where
 766     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 767     bind_lvl = TcM.topIdLvl dfun_id
 768
 769 pprEq :: TcType -> TcType -> SDoc
 770 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 771
 772 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 773 isTouchableMetaTyVar tv
 774   = do { untch <- getUntouchables
 775        ; return $ isTouchableMetaTyVar_InRange untch tv }
 776
 777 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
 778 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
 779   = case tcTyVarDetails tv of
 780       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
 781                         -- See Note [Touchable meta type variables]
 782       MetaTv {}      -> inTouchableRange untch tv
 783       _              -> False
 784
 785
 786 \end{code}
 787
 788
 789 Note [Touchable meta type variables]
 790 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 791 Meta type variables allocated *by the constraint solver itself* are always
 792 touchable.  Example:
 793    instance C a b => D [a] where...
 794 if we use this instance declaration we "make up" a fresh meta type
 795 variable for 'b', which we must later guess.  (Perhaps C has a
 796 functional dependency.)  But since we aren't in the constraint *generator*
 797 we can't allocate a Unique in the touchable range for this implication
 798 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 799
 800
 801 \begin{code}
 802 -- Flatten skolems
 803 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 804
 805 newFlattenSkolemTy :: TcType -> TcS TcType
 806 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 807
 808 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 809 newFlattenSkolemTyVar ty
 810   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
 811                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
 812                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 813        ; traceTcS "New Flatten Skolem Born" $
 814            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
 815        ; return tv }
 816
 817 -- Instantiations
 818 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 819
 820 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 821 instDFunTypes mb_inst_tys
 822   = mapM inst_tv mb_inst_tys
 823   where
 824     inst_tv :: Either TyVar TcType -> TcS Type
 825     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
 826     inst_tv (Right ty) = return ty
 827
 828 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 829 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 830
 831
 832 instFlexiTcS :: TyVar -> TcS TcTyVar
 833 -- Like TcM.instMetaTyVar but the variable that is created is always
 834 -- touchable; we are supposed to guess its instantiation.
 835 -- See Note [Touchable meta type variables]
 836 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
 837
 838 newFlexiTcSTy :: Kind -> TcS TcType
 839 newFlexiTcSTy knd
 840   = wrapTcS $
 841     do { uniq <- TcM.newUnique
 842        ; ref  <- TcM.newMutVar  Flexi
 843        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
 844        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
 845
 846 isFlexiTcsTv :: TyVar -> Bool
 847 isFlexiTcsTv tv
 848   | not (isTcTyVar tv)                  = False
 849   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
 850   | otherwise                           = False
 851
 852 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
 853 -- Create new wanted CoVar that constrains the type to have the specified kind.
 854 newKindConstraint tv knd
 855   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
 856        ; let ty_k = mkTyVarTy tv_k
 857        ; co_var <- newCoVar (mkTyVarTy tv) ty_k
 858        ; return co_var }
 859
 860 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
 861 instFlexiTcSHelper tvname tvkind
 862   = wrapTcS $
 863     do { uniq <- TcM.newUnique
 864        ; ref  <- TcM.newMutVar  Flexi
 865        ; let name = setNameUnique tvname uniq
 866              kind = tvkind
 867        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
 868
 869 -- Superclasses and recursive dictionaries
 870 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 871
 872 newEvVar :: TcPredType -> TcS EvVar
 873 newEvVar pty = wrapTcS $ TcM.newEvVar pty
 874
 875 newDerivedId :: TcPredType -> TcS EvVar
 876 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
 877
 878 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 879 -- Note we create immutable variables for given or derived, since we
 880 -- must bind them to TcEvBinds (because their evidence may involve
 881 -- superclasses). However we should be able to override existing
 882 -- 'derived' evidence, even in TcEvBinds
 883 newGivenCoVar ty1 ty2 co
 884   = do { cv <- newCoVar ty1 ty2
 885        ; setEvBind cv (EvCoercion co)
 886        ; return cv }
 887
 888 newCoVar :: TcType -> TcType -> TcS EvVar
 889 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 890
 891 newIPVar :: IPName Name -> TcType -> TcS EvVar
 892 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 893
 894 newDictVar :: Class -> [TcType] -> TcS EvVar
 895 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 896 \end{code}
 897
 898
 899 \begin{code}
 900 -- Matching and looking up classes and family instances
 901 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 902
 903 data MatchInstResult mi
 904   = MatchInstNo         -- No matching instance
 905   | MatchInstSingle mi  -- Single matching instance
 906   | MatchInstMany       -- Multiple matching instances
 907
 908
 909 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 910 -- Look up a class constraint in the instance environment
 911 matchClass clas tys
 912   = do  { let pred = mkClassPred clas tys
 913         ; instEnvs <- getInstEnvs
 914         ; case lookupInstEnv instEnvs clas tys of {
 915             ([], unifs)               -- Nothing matches
 916                 -> do { traceTcS "matchClass not matching"
 917                                  (vcat [ text "dict" <+> ppr pred,
 918                                          text "unifs" <+> ppr unifs ])
 919                       ; return MatchInstNo
 920                       } ;
 921             ([(ispec, inst_tys)], []) -- A single match
 922                 -> do   { let dfun_id = is_dfun ispec
 923                         ; traceTcS "matchClass success"
 924                                    (vcat [text "dict" <+> ppr pred,
 925                                           text "witness" <+> ppr dfun_id
 926                                            <+> ppr (idType dfun_id) ])
 927                                   -- Record that this dfun is needed
 928                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 929                         } ;
 930             (matches, unifs)          -- More than one matches
 931                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 932                                    (vcat [text "dict" <+> ppr pred,
 933                                           text "matches" <+> ppr matches,
 934                                           text "unifs" <+> ppr unifs])
 935                         ; return MatchInstMany
 936                         }
 937         }
 938         }
 939
 940 matchFam :: TyCon
 941          -> [Type]
 942          -> TcS (MatchInstResult (TyCon, [Type]))
 943 matchFam tycon args
 944   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 945        ; case mb of
 946            Nothing  -> return MatchInstNo
 947            Just res -> return $ MatchInstSingle res
 948        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 949        -- multiple matches. Check.
 950        }
 951 \end{code}