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