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
 599        -- One could be more conservative as well:
 600        -- ; flat_cache_var  <- TcM.newTcRef emptyFlatCache
 601
 602                             -- Consider copying the results the tcs_flat_map of the
 603                             -- incomping constraint, but we must make sure that we
 604                             -- have pushed everything in, which seems somewhat fragile
 605        ; let nest_env = TcSEnv { tcs_ev_binds = ref
 606                                , tcs_ty_binds = ty_binds
 607                                , tcs_untch    = inner_untch
 608                                , tcs_count    = count
 609                                , tcs_ic_depth = idepth+1
 610                                , tcs_context  = ctxtUnderImplic ctxt
 611                                , tcs_flat_map = flat_cache_var }
 612        ; thing_inside nest_env }
 613
 614 recoverTcS :: TcS a -> TcS a -> TcS a
 615 recoverTcS (TcS recovery_code) (TcS thing_inside)
 616   = TcS $ \ env ->
 617     TcM.recoverM (recovery_code env) (thing_inside env)
 618
 619 ctxtUnderImplic :: SimplContext -> SimplContext
 620 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 621 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
 622                                                <+> doubleQuotes (ftext n))
 623 ctxtUnderImplic ctxt              = ctxt
 624
 625 tryTcS :: TcS a -> TcS a
 626 -- Like runTcS, but from within the TcS monad
 627 -- Ignore all the evidence generated, and do not affect caller's evidence!
 628 tryTcS tcs
 629   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 630                     ; ev_binds_var <- TcM.newTcEvBinds
 631                     ; flat_cache_var <- TcM.newTcRef emptyFlatCache
 632                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 633                                      , tcs_ty_binds = ty_binds_var
 634                                      , tcs_flat_map = flat_cache_var }
 635                    ; unTcS tcs env1 })
 636
 637 -- Update TcEvBinds
 638 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 639
 640 getDynFlags :: TcS DynFlags
 641 getDynFlags = wrapTcS TcM.getDOpts
 642
 643 getTcSContext :: TcS SimplContext
 644 getTcSContext = TcS (return . tcs_context)
 645
 646 getTcEvBinds :: TcS EvBindsVar
 647 getTcEvBinds = TcS (return . tcs_ev_binds)
 648
 649 getUntouchables :: TcS TcsUntouchables
 650 getUntouchables = TcS (return . tcs_untch)
 651
 652 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
 653 getTcSTyBinds = TcS (return . tcs_ty_binds)
 654
 655 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
 656 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
 657
 658 getFlatCacheMapVar :: TcS (IORef FlatCache)
 659 getFlatCacheMapVar
 660   = TcS (return . tcs_flat_map)
 661
 662 lookupFlatCacheMap :: TyCon -> [Xi] -> CtFlavor
 663                    -> TcS (Maybe (TcType,Coercion,CtFlavor))
 664 -- For givens, we lookup in given flat cache
 665 lookupFlatCacheMap tc xis (Given {})
 666   = do { cache_ref <- getFlatCacheMapVar
 667        ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
 668        ; return $ Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) }
 669 -- For wanteds, we first lookup in givenFlatCache.
 670 -- If we get nothing back then we lookup in wantedFlatCache.
 671 lookupFlatCacheMap tc xis (Wanted {})
 672   = do { cache_ref <- getFlatCacheMapVar
 673        ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
 674        ; case Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) of
 675            Nothing -> return $ Map.lookup (FunEqHead (tc,xis)) (wantedFlatCache cache_map)
 676            other   -> return other }
 677 lookupFlatCacheMap _tc _xis (Derived {}) = return Nothing
 678
 679 updateFlatCacheMap :: TyCon -> [Xi]
 680                    -> TcType -> CtFlavor -> Coercion -> TcS ()
 681 updateFlatCacheMap _tc _xis _tv (Derived {}) _co
 682   = return () -- Not caching deriveds
 683 updateFlatCacheMap tc xis ty fl co
 684   = do { cache_ref <- getFlatCacheMapVar
 685        ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
 686        ; let new_cache_map
 687               | isGivenOrSolved fl
 688               = cache_map { givenFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
 689                                              givenFlatCache cache_map }
 690               | isWanted fl
 691               = cache_map { wantedFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
 692                                               wantedFlatCache cache_map }
 693               | otherwise = pprPanic "updateFlatCacheMap, met Derived!" $ empty
 694        ; wrapTcS $ TcM.writeTcRef cache_ref new_cache_map }
 695
 696
 697 getTcEvBindsBag :: TcS EvBindMap
 698 getTcEvBindsBag
 699   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 700        ; wrapTcS $ TcM.readTcRef ev_ref }
 701
 702
 703 setCoBind :: CoVar -> Coercion -> TcS ()
 704 setCoBind cv co = setEvBind cv (EvCoercion co)
 705
 706 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 707 -- Add a type binding
 708 -- We never do this twice!
 709 setWantedTyBind tv ty
 710   = do { ref <- getTcSTyBinds
 711        ; wrapTcS $
 712          do { ty_binds <- TcM.readTcRef ref
 713 #ifdef DEBUG
 714             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
 715               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
 716                    , ppr tv <+> text ":=" <+> ppr ty
 717                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
 718 #endif
 719             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
 720
 721 setIPBind :: EvVar -> EvTerm -> TcS ()
 722 setIPBind = setEvBind
 723
 724 setDictBind :: EvVar -> EvTerm -> TcS ()
 725 setDictBind = setEvBind
 726
 727 setEvBind :: EvVar -> EvTerm -> TcS ()
 728 -- Internal
 729 setEvBind ev rhs
 730   = do { tc_evbinds <- getTcEvBinds
 731        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 732
 733 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 734 warnTcS loc warn_if doc
 735   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 736   | otherwise = return ()
 737
 738 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 739 getDefaultInfo
 740   = do { ctxt <- getTcSContext
 741        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 742        ; return (ctxt, tys, flags) }
 743
 744 -- Just get some environments needed for instance looking up and matching
 745 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 746
 747 getInstEnvs :: TcS (InstEnv, InstEnv)
 748 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 749
 750 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 751 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 752
 753 getTopEnv :: TcS HscEnv
 754 getTopEnv = wrapTcS $ TcM.getTopEnv
 755
 756 getGblEnv :: TcS TcGblEnv
 757 getGblEnv = wrapTcS $ TcM.getGblEnv
 758
 759 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 760 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 761
 762 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 763 checkWellStagedDFun pred dfun_id loc
 764   = wrapTcS $ TcM.setCtLoc loc $
 765     do { use_stage <- TcM.getStage
 766        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 767   where
 768     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 769     bind_lvl = TcM.topIdLvl dfun_id
 770
 771 pprEq :: TcType -> TcType -> SDoc
 772 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 773
 774 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 775 isTouchableMetaTyVar tv
 776   = do { untch <- getUntouchables
 777        ; return $ isTouchableMetaTyVar_InRange untch tv }
 778
 779 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
 780 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
 781   = case tcTyVarDetails tv of
 782       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
 783                         -- See Note [Touchable meta type variables]
 784       MetaTv {}      -> inTouchableRange untch tv
 785       _              -> False
 786
 787
 788 \end{code}
 789
 790
 791 Note [Touchable meta type variables]
 792 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 793 Meta type variables allocated *by the constraint solver itself* are always
 794 touchable.  Example:
 795    instance C a b => D [a] where...
 796 if we use this instance declaration we "make up" a fresh meta type
 797 variable for 'b', which we must later guess.  (Perhaps C has a
 798 functional dependency.)  But since we aren't in the constraint *generator*
 799 we can't allocate a Unique in the touchable range for this implication
 800 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 801
 802
 803 \begin{code}
 804 -- Flatten skolems
 805 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 806
 807 newFlattenSkolemTy :: TcType -> TcS TcType
 808 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 809
 810 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 811 newFlattenSkolemTyVar ty
 812   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
 813                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
 814                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 815        ; traceTcS "New Flatten Skolem Born" $
 816            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
 817        ; return tv }
 818
 819 -- Instantiations
 820 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 821
 822 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 823 instDFunTypes mb_inst_tys
 824   = mapM inst_tv mb_inst_tys
 825   where
 826     inst_tv :: Either TyVar TcType -> TcS Type
 827     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
 828     inst_tv (Right ty) = return ty
 829
 830 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 831 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 832
 833
 834 instFlexiTcS :: TyVar -> TcS TcTyVar
 835 -- Like TcM.instMetaTyVar but the variable that is created is always
 836 -- touchable; we are supposed to guess its instantiation.
 837 -- See Note [Touchable meta type variables]
 838 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
 839
 840 newFlexiTcSTy :: Kind -> TcS TcType
 841 newFlexiTcSTy knd
 842   = wrapTcS $
 843     do { uniq <- TcM.newUnique
 844        ; ref  <- TcM.newMutVar  Flexi
 845        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
 846        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
 847
 848 isFlexiTcsTv :: TyVar -> Bool
 849 isFlexiTcsTv tv
 850   | not (isTcTyVar tv)                  = False
 851   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
 852   | otherwise                           = False
 853
 854 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
 855 -- Create new wanted CoVar that constrains the type to have the specified kind.
 856 newKindConstraint tv knd
 857   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
 858        ; let ty_k = mkTyVarTy tv_k
 859        ; co_var <- newCoVar (mkTyVarTy tv) ty_k
 860        ; return co_var }
 861
 862 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
 863 instFlexiTcSHelper tvname tvkind
 864   = wrapTcS $
 865     do { uniq <- TcM.newUnique
 866        ; ref  <- TcM.newMutVar  Flexi
 867        ; let name = setNameUnique tvname uniq
 868              kind = tvkind
 869        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
 870
 871 -- Superclasses and recursive dictionaries
 872 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 873
 874 newEvVar :: TcPredType -> TcS EvVar
 875 newEvVar pty = wrapTcS $ TcM.newEvVar pty
 876
 877 newDerivedId :: TcPredType -> TcS EvVar
 878 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
 879
 880 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 881 -- Note we create immutable variables for given or derived, since we
 882 -- must bind them to TcEvBinds (because their evidence may involve
 883 -- superclasses). However we should be able to override existing
 884 -- 'derived' evidence, even in TcEvBinds
 885 newGivenCoVar ty1 ty2 co
 886   = do { cv <- newCoVar ty1 ty2
 887        ; setEvBind cv (EvCoercion co)
 888        ; return cv }
 889
 890 newCoVar :: TcType -> TcType -> TcS EvVar
 891 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 892
 893 newIPVar :: IPName Name -> TcType -> TcS EvVar
 894 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 895
 896 newDictVar :: Class -> [TcType] -> TcS EvVar
 897 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 898 \end{code}
 899
 900
 901 \begin{code}
 902 -- Matching and looking up classes and family instances
 903 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 904
 905 data MatchInstResult mi
 906   = MatchInstNo         -- No matching instance
 907   | MatchInstSingle mi  -- Single matching instance
 908   | MatchInstMany       -- Multiple matching instances
 909
 910
 911 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 912 -- Look up a class constraint in the instance environment
 913 matchClass clas tys
 914   = do  { let pred = mkClassPred clas tys
 915         ; instEnvs <- getInstEnvs
 916         ; case lookupInstEnv instEnvs clas tys of {
 917             ([], unifs)               -- Nothing matches
 918                 -> do { traceTcS "matchClass not matching"
 919                                  (vcat [ text "dict" <+> ppr pred,
 920                                          text "unifs" <+> ppr unifs ])
 921                       ; return MatchInstNo
 922                       } ;
 923             ([(ispec, inst_tys)], []) -- A single match
 924                 -> do   { let dfun_id = is_dfun ispec
 925                         ; traceTcS "matchClass success"
 926                                    (vcat [text "dict" <+> ppr pred,
 927                                           text "witness" <+> ppr dfun_id
 928                                            <+> ppr (idType dfun_id) ])
 929                                   -- Record that this dfun is needed
 930                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 931                         } ;
 932             (matches, unifs)          -- More than one matches
 933                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 934                                    (vcat [text "dict" <+> ppr pred,
 935                                           text "matches" <+> ppr matches,
 936                                           text "unifs" <+> ppr unifs])
 937                         ; return MatchInstMany
 938                         }
 939         }
 940         }
 941
 942 matchFam :: TyCon
 943          -> [Type]
 944          -> TcS (MatchInstResult (TyCon, [Type]))
 945 matchFam tycon args
 946   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 947        ; case mb of
 948            Nothing  -> return MatchInstNo
 949            Just res -> return $ MatchInstSingle res
 950        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 951        -- multiple matches. Check.
 952        }
 953 \end{code}