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
  10     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
  11     mkWantedConstraints, deCanonicaliseWanted,
  12     makeGivens, makeSolvedByInst,
  13
  14     CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst,
  15     isGivenCt, isWantedCt,
  16
  17     DerivedOrig (..),
  18     canRewrite, canSolve,
  19     combineCtLoc, mkGivenFlavor,
  20
  21     TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality
  22     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
  23     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
  24
  25        -- Creation of evidence variables
  26
  27     newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
  28     newIPVar, newDictVar, newKindConstraint,
  29
  30        -- Setting evidence variables
  31     setWantedCoBind, setDerivedCoBind,
  32     setIPBind, setDictBind, setEvBind,
  33
  34     setWantedTyBind,
  35
  36     newTcEvBindsTcS,
  37
  38     getInstEnvs, getFamInstEnvs,                -- Getting the environments
  39     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
  40     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
  41
  42
  43     newFlattenSkolemTy,                         -- Flatten skolems
  44
  45
  46     instDFunTypes,                              -- Instantiation
  47     instDFunConstraints,
  48
  49     isGoodRecEv,
  50
  51     zonkTcTypeTcS,                              -- Zonk through the TyBinds of the Tcs Monad
  52     compatKind,
  53
  54
  55     isTouchableMetaTyVar,
  56     isTouchableMetaTyVar_InRange,
  57
  58     getDefaultInfo, getDynFlags,
  59
  60     matchClass, matchFam, MatchInstResult (..),
  61     checkWellStagedDFun,
  62     warnTcS,
  63     pprEq,                                   -- Smaller utils, re-exported from TcM
  64                                              -- TODO (DV): these are only really used in the
  65                                              -- instance matcher in TcSimplify. I am wondering
  66                                              -- if the whole instance matcher simply belongs
  67                                              -- here
  68
  69
  70     mkWantedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
  71
  72 ) where
  73
  74 #include "HsVersions.h"
  75
  76 import HscTypes
  77 import BasicTypes
  78
  79 import Inst
  80 import InstEnv
  81 import FamInst
  82 import FamInstEnv
  83
  84 import NameSet ( addOneToNameSet )
  85
  86 import qualified TcRnMonad as TcM
  87 import qualified TcMType as TcM
  88 import qualified TcEnv as TcM
  89        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
  90 import TcType
  91 import Module
  92 import DynFlags
  93
  94 import Coercion
  95 import Class
  96 import TyCon
  97 import TypeRep
  98
  99 import Name
 100 import Var
 101 import VarEnv
 102 import Outputable
 103 import Bag
 104 import MonadUtils
 105 import VarSet
 106 import FastString
 107
 108 import HsBinds               -- for TcEvBinds stuff
 109 import Id
 110 import FunDeps
 111
 112 import TcRnTypes
 113
 114 import Data.IORef
 115 \end{code}
 116
 117
 118 %************************************************************************
 119 %*                                                                      *
 120 %*                       Canonical constraints                          *
 121 %*                                                                      *
 122 %*   These are the constraints the low-level simplifier works with      *
 123 %*                                                                      *
 124 %************************************************************************
 125
 126 \begin{code}
 127 -- Types without any type functions inside.  However, note that xi
 128 -- types CAN contain unexpanded type synonyms; however, the
 129 -- (transitive) expansions of those type synonyms will not contain any
 130 -- type functions.
 131 type Xi = Type       -- In many comments, "xi" ranges over Xi
 132
 133 type CanonicalCts = Bag CanonicalCt
 134
 135 data CanonicalCt
 136   -- Atomic canonical constraints
 137   = CDictCan {  -- e.g.  Num xi
 138       cc_id     :: EvVar,
 139       cc_flavor :: CtFlavor,
 140       cc_class  :: Class,
 141       cc_tyargs :: [Xi]
 142     }
 143
 144   | CIPCan {    -- ?x::tau
 145       -- See note [Canonical implicit parameter constraints].
 146       cc_id     :: EvVar,
 147       cc_flavor :: CtFlavor,
 148       cc_ip_nm  :: IPName Name,
 149       cc_ip_ty  :: TcTauType
 150     }
 151
 152   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
 153        -- Invariant:
 154        --   * tv not in tvs(xi)   (occurs check)
 155        --   * If constraint is given then typeKind xi `compatKind` typeKind tv
 156        --                See Note [Spontaneous solving and kind compatibility]
 157        --   * If 'xi' is a flatten skolem then 'tv' can only be:
 158        --              - a flatten skolem or a unification variable
 159        --     i.e. equalities prefer flatten skolems in their LHS
 160        --     See Note [Loopy Spontaneous Solving, Example 4]
 161        --     Also related to [Flatten Skolem Equivalence Classes]
 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                  --            * cc_rhs is not a touchable unification variable
 171                  --                   See Note [No touchables as FunEq RHS]
 172                  --            * If constraint is given then
 173                  --                 typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs
 174       cc_id     :: EvVar,
 175       cc_flavor :: CtFlavor,
 176       cc_fun    :: TyCon,       -- A type function
 177       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
 178       cc_rhs    :: Xi           --    *never* over-saturated (because if so
 179                                 --    we should have decomposed)
 180
 181     }
 182
 183 compatKind :: Kind -> Kind -> Bool
 184 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
 185
 186 makeGivens :: CanonicalCts -> CanonicalCts
 187 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
 188            -- The UnkSkol doesn't matter because these givens are
 189            -- not contradictory (else we'd have rejected them already)
 190
 191 makeSolvedByInst :: CanonicalCt -> CanonicalCt
 192 -- Record that a constraint is now solved
 193 --        Wanted         -> Derived
 194 --        Given, Derived -> no-op
 195 makeSolvedByInst ct
 196   | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
 197   | otherwise                  = ct
 198
 199 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
 200 mkWantedConstraints flats implics
 201   = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
 202
 203 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
 204 deCanonicaliseWanted ct
 205   = WARN( not (isWanted $ cc_flavor ct), ppr ct )
 206     let Wanted loc = cc_flavor ct
 207     in WantedEvVar (cc_id ct) loc
 208
 209 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
 210 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
 211 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
 212 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
 213 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
 214
 215 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
 216 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
 217 tyVarsOfCDict _ct                            = emptyVarSet
 218
 219 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
 220 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
 221
 222 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
 223 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
 224
 225 instance Outputable CanonicalCt where
 226   ppr (CDictCan d fl cls tys)
 227       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
 228   ppr (CIPCan ip fl ip_nm ty)
 229       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
 230   ppr (CTyEqCan co fl tv ty)
 231       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
 232   ppr (CFunEqCan co fl tc tys ty)
 233       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
 234 \end{code}
 235
 236
 237 Note [No touchables as FunEq RHS]
 238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 239 Notice that (F xis ~ beta), where beta is an touchable unification
 240 variable, is not canonical.  Why?
 241   * If (F xis ~ beta) was the only wanted constraint, we'd
 242     definitely want to spontaneously-unify it
 243
 244   * But suppose we had an earlier wanted (beta ~ Int), and
 245     have already spontaneously unified it.  Then we have an
 246     identity given (id : beta ~ Int) in the inert set.
 247
 248   * But (F xis ~ beta) does not react with that given (because we
 249     don't subsitute on the RHS of a function equality).  So there's a
 250     serious danger that we'd spontaneously unify it a second time.
 251
 252 Hence the invariant.
 253
 254 The invariant is
 255
 256 Note [Canonical implicit parameter constraints]
 257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 258 The type in a canonical implicit parameter constraint doesn't need to
 259 be a xi (type-function-free type) since we can defer the flattening
 260 until checking this type for equality with another type.  If we
 261 encounter two IP constraints with the same name, they MUST have the
 262 same type, and at that point we can generate a flattened equality
 263 constraint between the types.  (On the other hand, the types in two
 264 class constraints for the same class MAY be equal, so they need to be
 265 flattened in the first place to facilitate comparing them.)
 266
 267 \begin{code}
 268 singleCCan :: CanonicalCt -> CanonicalCts
 269 singleCCan = unitBag
 270
 271 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
 272 andCCan = unionBags
 273
 274 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
 275 extendCCans = snocBag
 276
 277 andCCans :: [CanonicalCts] -> CanonicalCts
 278 andCCans = unionManyBags
 279
 280 emptyCCan :: CanonicalCts
 281 emptyCCan = emptyBag
 282
 283 isEmptyCCan :: CanonicalCts -> Bool
 284 isEmptyCCan = isEmptyBag
 285
 286 isCTyEqCan :: CanonicalCt -> Bool
 287 isCTyEqCan (CTyEqCan {})  = True
 288 isCTyEqCan (CFunEqCan {}) = False
 289 isCTyEqCan _              = False
 290
 291 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
 292 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
 293 isCDictCan_Maybe _              = Nothing
 294
 295 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
 296 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
 297 isCIPCan_Maybe _                = Nothing
 298
 299 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
 300 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
 301 isCFunEqCan_Maybe _ = Nothing
 302
 303 \end{code}
 304
 305 %************************************************************************
 306 %*                                                                      *
 307                     CtFlavor
 308          The "flavor" of a canonical constraint
 309 %*                                                                      *
 310 %************************************************************************
 311
 312 \begin{code}
 313 data CtFlavor
 314   = Given   GivenLoc  -- We have evidence for this constraint in TcEvBinds
 315   | Derived WantedLoc DerivedOrig
 316                       -- We have evidence for this constraint in TcEvBinds;
 317                       --   *however* this evidence can contain wanteds, so
 318                       --   it's valid only provisionally to the solution of
 319                       --   these wanteds
 320   | Wanted WantedLoc  -- We have no evidence bindings for this constraint.
 321
 322 data DerivedOrig = DerSC | DerInst
 323 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
 324 -- solved wanteds from instances.
 325
 326 instance Outputable CtFlavor where
 327   ppr (Given _)    = ptext (sLit "[Given]")
 328   ppr (Wanted _)   = ptext (sLit "[Wanted]")
 329   ppr (Derived {}) = ptext (sLit "[Derived]")
 330
 331 isWanted :: CtFlavor -> Bool
 332 isWanted (Wanted {}) = True
 333 isWanted _           = False
 334
 335 isGiven :: CtFlavor -> Bool
 336 isGiven (Given {}) = True
 337 isGiven _          = False
 338
 339 isDerived :: CtFlavor -> Bool
 340 isDerived (Derived {}) = True
 341 isDerived _            = False
 342
 343 isDerivedSC :: CtFlavor -> Bool
 344 isDerivedSC (Derived _ DerSC) = True
 345 isDerivedSC _                 = False
 346
 347 isDerivedByInst :: CtFlavor -> Bool
 348 isDerivedByInst (Derived _ DerInst) = True
 349 isDerivedByInst _                   = False
 350
 351 isWantedCt :: CanonicalCt -> Bool
 352 isWantedCt ct = isWanted (cc_flavor ct)
 353 isGivenCt :: CanonicalCt -> Bool
 354 isGivenCt ct = isGiven (cc_flavor ct)
 355
 356 canSolve :: CtFlavor -> CtFlavor -> Bool
 357 -- canSolve ctid1 ctid2
 358 -- The constraint ctid1 can be used to solve ctid2
 359 -- "to solve" means a reaction where the active parts of the two constraints match.
 360 --  active(F xis ~ xi) = F xis
 361 --  active(tv ~ xi)    = tv
 362 --  active(D xis)      = D xis
 363 --  active(IP nm ty)   = nm
 364 -----------------------------------------
 365 canSolve (Given {})   _            = True
 366 canSolve (Derived {}) (Wanted {})  = True
 367 canSolve (Derived {}) (Derived {}) = True
 368 canSolve (Wanted {})  (Wanted {})  = True
 369 canSolve _ _ = False
 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 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 385 mkGivenFlavor (Wanted  loc)   sk = Given (setCtLocOrigin loc sk)
 386 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
 387 mkGivenFlavor (Given   loc)   sk = Given (setCtLocOrigin loc sk)
 388 \end{code}
 389
 390
 391 %************************************************************************
 392 %*                                                                      *
 393 %*              The TcS solver monad                                    *
 394 %*                                                                      *
 395 %************************************************************************
 396
 397 Note [The TcS monad]
 398 ~~~~~~~~~~~~~~~~~~~~
 399 The TcS monad is a weak form of the main Tc monad
 400
 401 All you can do is
 402     * fail
 403     * allocate new variables
 404     * fill in evidence variables
 405
 406 Filling in a dictionary evidence variable means to create a binding
 407 for it, so TcS carries a mutable location where the binding can be
 408 added.  This is initialised from the innermost implication constraint.
 409
 410 \begin{code}
 411 data TcSEnv
 412   = TcSEnv {
 413       tcs_ev_binds :: EvBindsVar,
 414           -- Evidence bindings
 415
 416       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
 417           -- Global type bindings
 418
 419       tcs_context :: SimplContext,
 420
 421       tcs_untch :: Untouchables
 422     }
 423
 424 data SimplContext
 425   = SimplInfer          -- Inferring type of a let-bound thing
 426   | SimplRuleLhs        -- Inferring type of a RULE lhs
 427   | SimplInteractive    -- Inferring type at GHCi prompt
 428   | SimplCheck          -- Checking a type signature or RULE rhs
 429
 430 instance Outputable SimplContext where
 431   ppr SimplInfer       = ptext (sLit "SimplInfer")
 432   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
 433   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 434   ppr SimplCheck       = ptext (sLit "SimplCheck")
 435
 436 isInteractive :: SimplContext -> Bool
 437 isInteractive SimplInteractive = True
 438 isInteractive _                = False
 439
 440 simplEqsOnly :: SimplContext -> Bool
 441 -- Simplify equalities only, not dictionaries
 442 -- This is used for the LHS of rules; ee
 443 -- Note [Simplifying RULE lhs constraints] in TcSimplify
 444 simplEqsOnly SimplRuleLhs = True
 445 simplEqsOnly _            = False
 446
 447 performDefaulting :: SimplContext -> Bool
 448 performDefaulting SimplInfer       = False
 449 performDefaulting SimplRuleLhs     = False
 450 performDefaulting SimplInteractive = True
 451 performDefaulting SimplCheck       = True
 452
 453 ---------------
 454 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
 455
 456 instance Functor TcS where
 457   fmap f m = TcS $ fmap f . unTcS m
 458
 459 instance Monad TcS where
 460   return x  = TcS (\_ -> return x)
 461   fail err  = TcS (\_ -> fail err)
 462   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 463
 464 -- Basic functionality
 465 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 466 wrapTcS :: TcM a -> TcS a
 467 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
 468 -- and TcS is supposed to have limited functionality
 469 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
 470
 471 wrapErrTcS :: TcM a -> TcS a
 472 -- The thing wrapped should just fail
 473 -- There's no static check; it's up to the user
 474 -- Having a variant for each error message is too painful
 475 wrapErrTcS = wrapTcS
 476
 477 wrapWarnTcS :: TcM a -> TcS a
 478 -- The thing wrapped should just add a warning, or no-op
 479 -- There's no static check; it's up to the user
 480 wrapWarnTcS = wrapTcS
 481
 482 failTcS, panicTcS :: SDoc -> TcS a
 483 failTcS      = wrapTcS . TcM.failWith
 484 panicTcS doc = pprPanic "TcCanonical" doc
 485
 486 traceTcS :: String -> SDoc -> TcS ()
 487 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 488
 489 traceTcS0 :: String -> SDoc -> TcS ()
 490 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
 491
 492 runTcS :: SimplContext
 493        -> Untouchables         -- Untouchables
 494        -> TcS a                -- What to run
 495        -> TcM (a, Bag EvBind)
 496 runTcS context untouch tcs
 497   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 498        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 499        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
 500                           , tcs_ty_binds = ty_binds_var
 501                           , tcs_context = context
 502                           , tcs_untch   = untouch }
 503
 504              -- Run the computation
 505        ; res <- unTcS tcs env
 506
 507              -- Perform the type unifications required
 508        ; ty_binds <- TcM.readTcRef ty_binds_var
 509        ; mapM_ do_unification (varEnvElts ty_binds)
 510
 511              -- And return
 512        ; ev_binds <- TcM.readTcRef evb_ref
 513        ; return (res, evBindMapBinds ev_binds) }
 514   where
 515     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 516
 517
 518 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
 519 nestImplicTcS ref untch (TcS thing_inside)
 520   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
 521     let
 522        nest_env = TcSEnv { tcs_ev_binds = ref
 523                          , tcs_ty_binds = ty_binds
 524                          , tcs_untch    = untch
 525                          , tcs_context  = ctxtUnderImplic ctxt }
 526     in
 527     thing_inside nest_env
 528
 529 recoverTcS :: TcS a -> TcS a -> TcS a
 530 recoverTcS (TcS recovery_code) (TcS thing_inside)
 531   = TcS $ \ env ->
 532     TcM.recoverM (recovery_code env) (thing_inside env)
 533
 534 ctxtUnderImplic :: SimplContext -> SimplContext
 535 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 536 ctxtUnderImplic SimplRuleLhs = SimplCheck
 537 ctxtUnderImplic ctxt         = ctxt
 538
 539 tryTcS :: TcS a -> TcS a
 540 -- Like runTcS, but from within the TcS monad
 541 -- Ignore all the evidence generated, and do not affect caller's evidence!
 542 tryTcS tcs
 543   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 544                     ; ev_binds_var <- TcM.newTcEvBinds
 545                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 546                                      , tcs_ty_binds = ty_binds_var }
 547                     ; unTcS tcs env1 })
 548
 549 -- Update TcEvBinds
 550 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 551
 552 getDynFlags :: TcS DynFlags
 553 getDynFlags = wrapTcS TcM.getDOpts
 554
 555 getTcSContext :: TcS SimplContext
 556 getTcSContext = TcS (return . tcs_context)
 557
 558 getTcEvBinds :: TcS EvBindsVar
 559 getTcEvBinds = TcS (return . tcs_ev_binds)
 560
 561 getUntouchables :: TcS Untouchables
 562 getUntouchables = TcS (return . tcs_untch)
 563
 564 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
 565 getTcSTyBinds = TcS (return . tcs_ty_binds)
 566
 567 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
 568 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
 569
 570
 571 getTcEvBindsBag :: TcS EvBindMap
 572 getTcEvBindsBag
 573   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 574        ; wrapTcS $ TcM.readTcRef ev_ref }
 575
 576 setWantedCoBind :: CoVar -> Coercion -> TcS ()
 577 setWantedCoBind cv co
 578   = setEvBind cv (EvCoercion co)
 579      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
 580
 581 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
 582 setDerivedCoBind cv co
 583   = setEvBind cv (EvCoercion co)
 584
 585 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 586 -- Add a type binding
 587 setWantedTyBind tv ty
 588   = do { ref <- getTcSTyBinds
 589        ; wrapTcS $
 590          do { ty_binds <- TcM.readTcRef ref
 591             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
 592
 593 setIPBind :: EvVar -> EvTerm -> TcS ()
 594 setIPBind = setEvBind
 595
 596 setDictBind :: EvVar -> EvTerm -> TcS ()
 597 setDictBind = setEvBind
 598
 599 setEvBind :: EvVar -> EvTerm -> TcS ()
 600 -- Internal
 601 setEvBind ev rhs
 602   = do { tc_evbinds <- getTcEvBinds
 603        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 604
 605 newTcEvBindsTcS :: TcS EvBindsVar
 606 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
 607
 608 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 609 warnTcS loc warn_if doc
 610   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 611   | otherwise = return ()
 612
 613 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 614 getDefaultInfo
 615   = do { ctxt <- getTcSContext
 616        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 617        ; return (ctxt, tys, flags) }
 618
 619 -- Just get some environments needed for instance looking up and matching
 620 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 621
 622 getInstEnvs :: TcS (InstEnv, InstEnv)
 623 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 624
 625 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 626 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 627
 628 getTopEnv :: TcS HscEnv
 629 getTopEnv = wrapTcS $ TcM.getTopEnv
 630
 631 getGblEnv :: TcS TcGblEnv
 632 getGblEnv = wrapTcS $ TcM.getGblEnv
 633
 634 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 635 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 636
 637 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 638 checkWellStagedDFun pred dfun_id loc
 639   = wrapTcS $ TcM.setCtLoc loc $
 640     do { use_stage <- TcM.getStage
 641        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 642   where
 643     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 644     bind_lvl = TcM.topIdLvl dfun_id
 645
 646 pprEq :: TcType -> TcType -> SDoc
 647 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 648
 649 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 650 isTouchableMetaTyVar tv
 651   = do { untch <- getUntouchables
 652        ; return $ isTouchableMetaTyVar_InRange untch tv }
 653
 654 isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool
 655 isTouchableMetaTyVar_InRange untch tv
 656   = case tcTyVarDetails tv of
 657       MetaTv TcsTv _ -> True    -- See Note [Touchable meta type variables]
 658       MetaTv {}      -> inTouchableRange untch tv
 659       _              -> False
 660
 661
 662 \end{code}
 663
 664
 665 Note [Touchable meta type variables]
 666 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 667 Meta type variables allocated *by the constraint solver itself* are always
 668 touchable.  Example:
 669    instance C a b => D [a] where...
 670 if we use this instance declaration we "make up" a fresh meta type
 671 variable for 'b', which we must later guess.  (Perhaps C has a
 672 functional dependency.)  But since we aren't in the constraint *generator*
 673 we can't allocate a Unique in the touchable range for this implication
 674 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 675
 676
 677 \begin{code}
 678 -- Flatten skolems
 679 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 680
 681 newFlattenSkolemTy :: TcType -> TcS TcType
 682 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 683
 684 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 685 newFlattenSkolemTyVar ty
 686   = wrapTcS $ do { uniq <- TcM.newUnique
 687                  ; let name = mkSysTvName uniq (fsLit "f")
 688                  ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 689
 690 -- Instantiations
 691 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 692
 693 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 694 instDFunTypes mb_inst_tys
 695   = mapM inst_tv mb_inst_tys
 696   where
 697     inst_tv :: Either TyVar TcType -> TcS Type
 698     inst_tv (Left tv)  = mkTyVarTy <$> newFlexiTcS tv
 699     inst_tv (Right ty) = return ty
 700
 701 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 702 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 703
 704
 705 -- newFlexiTcS :: TyVar -> TcS TcTyVar
 706 -- -- Make a TcsTv meta tyvar; it is always touchable,
 707 -- -- but we are supposed to guess its instantiation
 708 -- -- See Note [Touchable meta type variables]
 709 -- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
 710
 711 newFlexiTcS :: TyVar -> TcS TcTyVar
 712 -- Like TcM.instMetaTyVar but the variable that is created is always
 713 -- touchable; we are supposed to guess its instantiation.
 714 -- See Note [Touchable meta type variables]
 715 newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
 716
 717 newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)
 718 -- Create new wanted CoVar that constrains the type to have the specified kind.
 719 newKindConstraint tv knd
 720   = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd
 721        ; let ty_k = mkTyVarTy tv_k
 722        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
 723        ; return (co_var, ty_k) }
 724
 725 newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
 726 newFlexiTcSHelper tvname tvkind
 727   = wrapTcS $
 728     do { uniq <- TcM.newUnique
 729        ; ref  <- TcM.newMutVar  Flexi
 730        ; let name = setNameUnique tvname uniq
 731              kind = tvkind
 732        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
 733
 734 -- Superclasses and recursive dictionaries
 735 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 736
 737 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
 738 newGivOrDerEvVar pty evtrm
 739   = do { ev <- wrapTcS $ TcM.newEvVar pty
 740        ; setEvBind ev evtrm
 741        ; return ev }
 742
 743 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 744 -- Note we create immutable variables for given or derived, since we
 745 -- must bind them to TcEvBinds (because their evidence may involve
 746 -- superclasses). However we should be able to override existing
 747 -- 'derived' evidence, even in TcEvBinds
 748 newGivOrDerCoVar ty1 ty2 co
 749   = do { cv <- newCoVar ty1 ty2
 750        ; setEvBind cv (EvCoercion co)
 751        ; return cv }
 752
 753 newWantedCoVar :: TcType -> TcType -> TcS EvVar
 754 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2
 755
 756
 757 newCoVar :: TcType -> TcType -> TcS EvVar
 758 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 759
 760 newIPVar :: IPName Name -> TcType -> TcS EvVar
 761 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 762
 763 newDictVar :: Class -> [TcType] -> TcS EvVar
 764 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 765 \end{code}
 766
 767
 768 \begin{code}
 769 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
 770 -- In a call (isGoodRecEv ev wv), we are considering solving wv
 771 -- using some term that involves ev, such as:
 772 -- by setting           wv = ev
 773 -- or                   wv = EvCast x |> ev
 774 -- etc.
 775 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
 776 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
 777 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
 778 --
 779 -- Guarded means: more instance calls than superclass selections. We
 780 -- compute this by chasing the evidence, adding +1 for every instance
 781 -- call (constructor) and -1 for every superclass selection (destructor).
 782 --
 783 -- See Note [Superclasses and recursive dictionaries] in TcInteract
 784 isGoodRecEv ev_var (WantedEvVar wv _)
 785   = do { tc_evbinds <- getTcEvBindsBag
 786        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
 787        ; return $ case mb of
 788                     Nothing -> True
 789                     Just min_guardedness -> min_guardedness > 0
 790        }
 791
 792   where chase_ev_var :: EvBindMap   -- Evidence binds
 793                  -> EvVar           -- Target variable whose gravity we want to return
 794                  -> Int             -- Current gravity
 795                  -> [EvVar]         -- Visited nodes
 796                  -> EvVar           -- Current node
 797                  -> TcS (Maybe Int)
 798         chase_ev_var assocs trg curr_grav visited orig
 799             | trg == orig         = return $ Just curr_grav
 800             | orig `elem` visited = return $ Nothing
 801             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
 802             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
 803
 804 {-  No longer needed: evidence is in the EvBinds
 805             | isTcTyVar orig && isMetaTyVar orig
 806             = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
 807                  ; case meta_details of
 808                      Flexi -> return Nothing
 809                      Indirect tyco -> chase_ev assocs trg curr_grav
 810                                              (orig:visited) (EvCoercion tyco)
 811                            }
 812 -}
 813             | otherwise = return Nothing
 814
 815         chase_ev assocs trg curr_grav visited (EvId v)
 816             = chase_ev_var assocs trg curr_grav visited v
 817         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
 818             = chase_ev_var assocs trg (curr_grav-1) visited d_id
 819         chase_ev assocs trg curr_grav visited (EvCast v co)
 820             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
 821                  ; m2 <- chase_co assocs trg curr_grav visited co
 822                  ; return (comb_chase_res Nothing [m1,m2]) }
 823
 824         chase_ev assocs trg curr_grav visited (EvCoercion co)
 825             = chase_co assocs trg curr_grav visited co
 826         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
 827             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
 828                  ; return (comb_chase_res Nothing chase_results) }
 829
 830         chase_co assocs trg curr_grav visited co
 831             = -- Look for all the coercion variables in the coercion
 832               -- chase them, and combine the results. This is OK since the
 833               -- coercion will not contain any superclass terms -- anything
 834               -- that involves dictionaries will be bound in assocs.
 835               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
 836                                              (tyVarsOfType co)
 837               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
 838                     ; return (comb_chase_res Nothing chase_results) }
 839
 840         comb_chase_res f []                   = f
 841         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest
 842         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
 843         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
 844
 845
 846 -- Matching and looking up classes and family instances
 847 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 848
 849 data MatchInstResult mi
 850   = MatchInstNo         -- No matching instance
 851   | MatchInstSingle mi  -- Single matching instance
 852   | MatchInstMany       -- Multiple matching instances
 853
 854
 855 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 856 -- Look up a class constraint in the instance environment
 857 matchClass clas tys
 858   = do  { let pred = mkClassPred clas tys
 859         ; instEnvs <- getInstEnvs
 860         ; case lookupInstEnv instEnvs clas tys of {
 861             ([], unifs)               -- Nothing matches
 862                 -> do { traceTcS "matchClass not matching"
 863                                  (vcat [ text "dict" <+> ppr pred,
 864                                          text "unifs" <+> ppr unifs ])
 865                       ; return MatchInstNo
 866                       } ;
 867             ([(ispec, inst_tys)], []) -- A single match
 868                 -> do   { let dfun_id = is_dfun ispec
 869                         ; traceTcS "matchClass success"
 870                                    (vcat [text "dict" <+> ppr pred,
 871                                           text "witness" <+> ppr dfun_id
 872                                            <+> ppr (idType dfun_id) ])
 873                                   -- Record that this dfun is needed
 874                         ; record_dfun_usage dfun_id
 875                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 876                         } ;
 877             (matches, unifs)          -- More than one matches
 878                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 879                                    (vcat [text "dict" <+> ppr pred,
 880                                           text "matches" <+> ppr matches,
 881                                           text "unifs" <+> ppr unifs])
 882                         ; return MatchInstMany
 883                         }
 884         }
 885         }
 886   where record_dfun_usage :: Id -> TcS ()
 887         record_dfun_usage dfun_id
 888           = do { hsc_env <- getTopEnv
 889                ; let  dfun_name = idName dfun_id
 890                       dfun_mod  = ASSERT( isExternalName dfun_name )
 891                                   nameModule dfun_name
 892                ; if isInternalName dfun_name ||    -- Internal name => defined in this module
 893                     modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
 894                  then return () -- internal, or in another package
 895                  else do updInstUses dfun_id
 896                }
 897
 898         updInstUses :: Id -> TcS ()
 899         updInstUses dfun_id
 900             = do { tcg_env <- getGblEnv
 901                  ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
 902                                             (`addOneToNameSet` idName dfun_id)
 903                  }
 904
 905 matchFam :: TyCon
 906          -> [Type]
 907          -> TcS (MatchInstResult (TyCon, [Type]))
 908 matchFam tycon args
 909   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 910        ; case mb of
 911            Nothing  -> return MatchInstNo
 912            Just res -> return $ MatchInstSingle res
 913        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 914        -- multiple matches. Check.
 915        }
 916
 917
 918 zonkTcTypeTcS :: TcType -> TcS TcType
 919 -- Zonk through the TyBinds of the Tcs Monad
 920 zonkTcTypeTcS ty
 921   = do { subst <- getTcSTyBindsMap >>= return . varEnvElts
 922        ; let (dom,rng)  = unzip subst
 923              apply_once = substTyWith dom rng
 924        ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ]
 925        ; return (substTyWith dom rng_idemp ty) }
 926
 927
 928
 929
 930
 931
 932 -- Functional dependencies, instantiation of equations
 933 -------------------------------------------------------
 934
 935 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
 936                    -> TcS [WantedEvVar]
 937 mkWantedFunDepEqns _   [] = return []
 938 mkWantedFunDepEqns loc eqns
 939   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
 940        ; wevvars <- mapM to_work_item eqns
 941        ; return $ concat wevvars }
 942   where
 943     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
 944     to_work_item ((qtvs, pairs), _, _)
 945       = do { let tvs = varSetElems qtvs
 946            ; tvs' <- mapM newFlexiTcS tvs
 947            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
 948            ; mapM (do_one subst) pairs }
 949
 950     do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
 951                                        sty2 = substTy subst ty2
 952                                 ; ev <- newWantedCoVar sty1 sty2
 953                                 ; return (WantedEvVar ev loc) }
 954
 955 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
 956 pprEquationDoc (eqn, (p1, _), (p2, _))
 957   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
 958 \end{code}