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