compiler/typecheck/TcSMonad.lhs

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