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