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