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