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