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