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