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