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