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