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