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 #ifdef DEBUG
 107 import Control.Monad( when )
 108 #endif
 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 (mkTyVarTy tv, ty)
 210   ppr (CFunEqCan co fl tc tys ty)
 211       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (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 SDoc        -- Inferring type of a let-bound thing
 427   | SimplRuleLhs RuleName  -- Inferring type of a RULE lhs
 428   | SimplInteractive       -- Inferring type at GHCi prompt
 429   | SimplCheck SDoc        -- Checking a type signature or RULE rhs
 430
 431 instance Outputable SimplContext where
 432   ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
 433   ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
 434   ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
 435   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 436
 437 isInteractive :: SimplContext -> Bool
 438 isInteractive SimplInteractive = True
 439 isInteractive _                = False
 440
 441 simplEqsOnly :: SimplContext -> Bool
 442 -- Simplify equalities only, not dictionaries
 443 -- This is used for the LHS of rules; ee
 444 -- Note [Simplifying RULE lhs constraints] in TcSimplify
 445 simplEqsOnly (SimplRuleLhs {}) = True
 446 simplEqsOnly _                 = False
 447
 448 performDefaulting :: SimplContext -> Bool
 449 performDefaulting (SimplInfer {})   = False
 450 performDefaulting (SimplRuleLhs {}) = False
 451 performDefaulting SimplInteractive  = True
 452 performDefaulting (SimplCheck {})   = True
 453
 454 ---------------
 455 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
 456
 457 instance Functor TcS where
 458   fmap f m = TcS $ fmap f . unTcS m
 459
 460 instance Monad TcS where
 461   return x  = TcS (\_ -> return x)
 462   fail err  = TcS (\_ -> fail err)
 463   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 464
 465 -- Basic functionality
 466 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 467 wrapTcS :: TcM a -> TcS a
 468 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
 469 -- and TcS is supposed to have limited functionality
 470 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
 471
 472 wrapErrTcS :: TcM a -> TcS a
 473 -- The thing wrapped should just fail
 474 -- There's no static check; it's up to the user
 475 -- Having a variant for each error message is too painful
 476 wrapErrTcS = wrapTcS
 477
 478 wrapWarnTcS :: TcM a -> TcS a
 479 -- The thing wrapped should just add a warning, or no-op
 480 -- There's no static check; it's up to the user
 481 wrapWarnTcS = wrapTcS
 482
 483 failTcS, panicTcS :: SDoc -> TcS a
 484 failTcS      = wrapTcS . TcM.failWith
 485 panicTcS doc = pprPanic "TcCanonical" doc
 486
 487 traceTcS :: String -> SDoc -> TcS ()
 488 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 489
 490 bumpStepCountTcS :: TcS ()
 491 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
 492                                     ; n <- TcM.readTcRef ref
 493                                     ; TcM.writeTcRef ref (n+1) }
 494
 495 traceFireTcS :: Int -> SDoc -> TcS ()
 496 -- Dump a rule-firing trace
 497 traceFireTcS depth doc
 498   = TcS $ \env ->
 499     TcM.ifDOptM Opt_D_dump_cs_trace $
 500     do { n <- TcM.readTcRef (tcs_count env)
 501        ; let msg = int n
 502                 <> text (replicate (tcs_ic_depth env) '>')
 503                 <> brackets (int depth) <+> doc
 504        ; TcM.dumpTcRn msg }
 505
 506 runTcS :: SimplContext
 507        -> Untouchables         -- Untouchables
 508        -> TcS a                -- What to run
 509        -> TcM (a, Bag EvBind)
 510 runTcS context untouch tcs
 511   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 512        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 513        ; step_count <- TcM.newTcRef 0
 514        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
 515                           , tcs_ty_binds = ty_binds_var
 516                           , tcs_context  = context
 517                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
 518                           , tcs_count    = step_count
 519                           , tcs_ic_depth = 0
 520                           }
 521
 522              -- Run the computation
 523        ; res <- unTcS tcs env
 524              -- Perform the type unifications required
 525        ; ty_binds <- TcM.readTcRef ty_binds_var
 526        ; mapM_ do_unification (varEnvElts ty_binds)
 527
 528 #ifdef DEBUG
 529        ; count <- TcM.readTcRef step_count
 530        ; when (opt_PprStyle_Debug && count > 0) $
 531          TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
 532                             <+> int count <+> ppr context)
 533 #endif
 534              -- And return
 535        ; ev_binds      <- TcM.readTcRef evb_ref
 536        ; return (res, evBindMapBinds ev_binds) }
 537   where
 538     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 539
 540 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
 541 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
 542   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
 543                    , tcs_untch = (_outer_range, outer_tcs)
 544                    , tcs_count = count
 545                    , tcs_ic_depth = idepth
 546                    , tcs_context = ctxt } ->
 547     let
 548        inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
 549                    -- The inner_range should be narrower than the outer one
 550                    -- (thus increasing the set of untouchables) but
 551                    -- the inner Tcs-untouchables must be unioned with the
 552                    -- outer ones!
 553        nest_env = TcSEnv { tcs_ev_binds = ref
 554                          , tcs_ty_binds = ty_binds
 555                          , tcs_untch    = inner_untch
 556                          , tcs_count    = count
 557                          , tcs_ic_depth = idepth+1
 558                          , tcs_context  = ctxtUnderImplic ctxt }
 559     in
 560     thing_inside nest_env
 561
 562 recoverTcS :: TcS a -> TcS a -> TcS a
 563 recoverTcS (TcS recovery_code) (TcS thing_inside)
 564   = TcS $ \ env ->
 565     TcM.recoverM (recovery_code env) (thing_inside env)
 566
 567 ctxtUnderImplic :: SimplContext -> SimplContext
 568 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 569 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
 570                                                <+> doubleQuotes (ftext n))
 571 ctxtUnderImplic ctxt              = ctxt
 572
 573 tryTcS :: TcS a -> TcS a
 574 -- Like runTcS, but from within the TcS monad
 575 -- Ignore all the evidence generated, and do not affect caller's evidence!
 576 tryTcS tcs
 577   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 578                     ; ev_binds_var <- TcM.newTcEvBinds
 579                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 580                                      , tcs_ty_binds = ty_binds_var }
 581                     ; unTcS tcs env1 })
 582
 583 -- Update TcEvBinds
 584 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 585
 586 getDynFlags :: TcS DynFlags
 587 getDynFlags = wrapTcS TcM.getDOpts
 588
 589 getTcSContext :: TcS SimplContext
 590 getTcSContext = TcS (return . tcs_context)
 591
 592 getTcEvBinds :: TcS EvBindsVar
 593 getTcEvBinds = TcS (return . tcs_ev_binds)
 594
 595 getUntouchables :: TcS TcsUntouchables
 596 getUntouchables = TcS (return . tcs_untch)
 597
 598 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
 599 getTcSTyBinds = TcS (return . tcs_ty_binds)
 600
 601 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
 602 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
 603
 604
 605 getTcEvBindsBag :: TcS EvBindMap
 606 getTcEvBindsBag
 607   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 608        ; wrapTcS $ TcM.readTcRef ev_ref }
 609
 610 setCoBind :: CoVar -> Coercion -> TcS ()
 611 setCoBind cv co = setEvBind cv (EvCoercion co)
 612
 613 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 614 -- Add a type binding
 615 -- We never do this twice!
 616 setWantedTyBind tv ty
 617   = do { ref <- getTcSTyBinds
 618        ; wrapTcS $
 619          do { ty_binds <- TcM.readTcRef ref
 620 #ifdef DEBUG
 621             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
 622               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
 623                    , ppr tv <+> text ":=" <+> ppr ty
 624                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
 625 #endif
 626             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
 627
 628 setIPBind :: EvVar -> EvTerm -> TcS ()
 629 setIPBind = setEvBind
 630
 631 setDictBind :: EvVar -> EvTerm -> TcS ()
 632 setDictBind = setEvBind
 633
 634 setEvBind :: EvVar -> EvTerm -> TcS ()
 635 -- Internal
 636 setEvBind ev rhs
 637   = do { tc_evbinds <- getTcEvBinds
 638        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 639
 640 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 641 warnTcS loc warn_if doc
 642   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 643   | otherwise = return ()
 644
 645 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 646 getDefaultInfo
 647   = do { ctxt <- getTcSContext
 648        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 649        ; return (ctxt, tys, flags) }
 650
 651 -- Just get some environments needed for instance looking up and matching
 652 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 653
 654 getInstEnvs :: TcS (InstEnv, InstEnv)
 655 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 656
 657 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 658 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 659
 660 getTopEnv :: TcS HscEnv
 661 getTopEnv = wrapTcS $ TcM.getTopEnv
 662
 663 getGblEnv :: TcS TcGblEnv
 664 getGblEnv = wrapTcS $ TcM.getGblEnv
 665
 666 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 667 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 668
 669 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 670 checkWellStagedDFun pred dfun_id loc
 671   = wrapTcS $ TcM.setCtLoc loc $
 672     do { use_stage <- TcM.getStage
 673        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 674   where
 675     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 676     bind_lvl = TcM.topIdLvl dfun_id
 677
 678 pprEq :: TcType -> TcType -> SDoc
 679 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 680
 681 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 682 isTouchableMetaTyVar tv
 683   = do { untch <- getUntouchables
 684        ; return $ isTouchableMetaTyVar_InRange untch tv }
 685
 686 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
 687 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
 688   = case tcTyVarDetails tv of
 689       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
 690                         -- See Note [Touchable meta type variables]
 691       MetaTv {}      -> inTouchableRange untch tv
 692       _              -> False
 693
 694
 695 \end{code}
 696
 697
 698 Note [Touchable meta type variables]
 699 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 700 Meta type variables allocated *by the constraint solver itself* are always
 701 touchable.  Example:
 702    instance C a b => D [a] where...
 703 if we use this instance declaration we "make up" a fresh meta type
 704 variable for 'b', which we must later guess.  (Perhaps C has a
 705 functional dependency.)  But since we aren't in the constraint *generator*
 706 we can't allocate a Unique in the touchable range for this implication
 707 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 708
 709
 710 \begin{code}
 711 -- Flatten skolems
 712 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 713
 714 newFlattenSkolemTy :: TcType -> TcS TcType
 715 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 716
 717 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 718 newFlattenSkolemTyVar ty
 719   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
 720                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
 721                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 722        ; traceTcS "New Flatten Skolem Born" $
 723            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
 724        ; return tv }
 725
 726 -- Instantiations
 727 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 728
 729 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 730 instDFunTypes mb_inst_tys
 731   = mapM inst_tv mb_inst_tys
 732   where
 733     inst_tv :: Either TyVar TcType -> TcS Type
 734     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
 735     inst_tv (Right ty) = return ty
 736
 737 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 738 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 739
 740
 741 instFlexiTcS :: TyVar -> TcS TcTyVar
 742 -- Like TcM.instMetaTyVar but the variable that is created is always
 743 -- touchable; we are supposed to guess its instantiation.
 744 -- See Note [Touchable meta type variables]
 745 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
 746
 747 newFlexiTcSTy :: Kind -> TcS TcType
 748 newFlexiTcSTy knd
 749   = wrapTcS $
 750     do { uniq <- TcM.newUnique
 751        ; ref  <- TcM.newMutVar  Flexi
 752        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
 753        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
 754
 755 isFlexiTcsTv :: TyVar -> Bool
 756 isFlexiTcsTv tv
 757   | not (isTcTyVar tv)                  = False
 758   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
 759   | otherwise                           = False
 760
 761 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
 762 -- Create new wanted CoVar that constrains the type to have the specified kind.
 763 newKindConstraint tv knd
 764   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
 765        ; let ty_k = mkTyVarTy tv_k
 766        ; co_var <- newCoVar (mkTyVarTy tv) ty_k
 767        ; return co_var }
 768
 769 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
 770 instFlexiTcSHelper tvname tvkind
 771   = wrapTcS $
 772     do { uniq <- TcM.newUnique
 773        ; ref  <- TcM.newMutVar  Flexi
 774        ; let name = setNameUnique tvname uniq
 775              kind = tvkind
 776        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
 777
 778 -- Superclasses and recursive dictionaries
 779 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 780
 781 newEvVar :: TcPredType -> TcS EvVar
 782 newEvVar pty = wrapTcS $ TcM.newEvVar pty
 783
 784 newDerivedId :: TcPredType -> TcS EvVar
 785 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
 786
 787 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 788 -- Note we create immutable variables for given or derived, since we
 789 -- must bind them to TcEvBinds (because their evidence may involve
 790 -- superclasses). However we should be able to override existing
 791 -- 'derived' evidence, even in TcEvBinds
 792 newGivenCoVar ty1 ty2 co
 793   = do { cv <- newCoVar ty1 ty2
 794        ; setEvBind cv (EvCoercion co)
 795        ; return cv }
 796
 797 newCoVar :: TcType -> TcType -> TcS EvVar
 798 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 799
 800 newIPVar :: IPName Name -> TcType -> TcS EvVar
 801 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 802
 803 newDictVar :: Class -> [TcType] -> TcS EvVar
 804 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 805 \end{code}
 806
 807
 808 \begin{code}
 809 -- Matching and looking up classes and family instances
 810 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 811
 812 data MatchInstResult mi
 813   = MatchInstNo         -- No matching instance
 814   | MatchInstSingle mi  -- Single matching instance
 815   | MatchInstMany       -- Multiple matching instances
 816
 817
 818 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 819 -- Look up a class constraint in the instance environment
 820 matchClass clas tys
 821   = do  { let pred = mkClassPred clas tys
 822         ; instEnvs <- getInstEnvs
 823         ; case lookupInstEnv instEnvs clas tys of {
 824             ([], unifs)               -- Nothing matches
 825                 -> do { traceTcS "matchClass not matching"
 826                                  (vcat [ text "dict" <+> ppr pred,
 827                                          text "unifs" <+> ppr unifs ])
 828                       ; return MatchInstNo
 829                       } ;
 830             ([(ispec, inst_tys)], []) -- A single match
 831                 -> do   { let dfun_id = is_dfun ispec
 832                         ; traceTcS "matchClass success"
 833                                    (vcat [text "dict" <+> ppr pred,
 834                                           text "witness" <+> ppr dfun_id
 835                                            <+> ppr (idType dfun_id) ])
 836                                   -- Record that this dfun is needed
 837                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 838                         } ;
 839             (matches, unifs)          -- More than one matches
 840                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 841                                    (vcat [text "dict" <+> ppr pred,
 842                                           text "matches" <+> ppr matches,
 843                                           text "unifs" <+> ppr unifs])
 844                         ; return MatchInstMany
 845                         }
 846         }
 847         }
 848
 849 matchFam :: TyCon
 850          -> [Type]
 851          -> TcS (MatchInstResult (TyCon, [Type]))
 852 matchFam tycon args
 853   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 854        ; case mb of
 855            Nothing  -> return MatchInstNo
 856            Just res -> return $ MatchInstSingle res
 857        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 858        -- multiple matches. Check.
 859        }
 860 \end{code}