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 isTouchableMetaTyVar tv
 570   = case tcTyVarDetails tv of
 571       MetaTv TcsTv _ -> return True     -- See Note [Touchable meta type variables]
 572       MetaTv {}      -> do { untch <- getUntouchables
 573                            ; return (inTouchableRange untch tv) }
 574       _              -> return False
 575 \end{code}
 576
 577 Note [Touchable meta type variables]
 578 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 579 Meta type variables allocated *by the constraint solver itself* are always
 580 touchable.  Example:
 581    instance C a b => D [a] where...
 582 if we use this instance declaration we "make up" a fresh meta type
 583 variable for 'b', which we must later guess.  (Perhaps C has a
 584 functional dependency.)  But since we aren't in the constraint *generator*
 585 we can't allocate a Unique in the touchable range for this implication
 586 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 587
 588
 589 \begin{code}
 590 -- Flatten skolems
 591 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 592
 593 newFlattenSkolemTy :: TcType -> TcS TcType
 594 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 595
 596 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 597 newFlattenSkolemTyVar ty
 598   = wrapTcS $ do { uniq <- TcM.newUnique
 599                  ; let name = mkSysTvName uniq (fsLit "f")
 600                  ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 601
 602 -- Instantiations
 603 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 604
 605 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 606 instDFunTypes mb_inst_tys
 607   = mapM inst_tv mb_inst_tys
 608   where
 609     inst_tv :: Either TyVar TcType -> TcS Type
 610     inst_tv (Left tv)  = mkTyVarTy <$> newFlexiTcS tv
 611     inst_tv (Right ty) = return ty
 612
 613 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 614 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 615
 616 newFlexiTcS :: TyVar -> TcS TcTyVar
 617 -- Make a TcsTv meta tyvar; it is always touchable,
 618 -- but we are supposed to guess its instantiation
 619 -- See Note [Touchable meta type variables]
 620 newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
 621
 622 -- Superclasses and recursive dictionaries
 623 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 624
 625 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
 626 newGivOrDerEvVar pty evtrm
 627   = do { ev <- wrapTcS $ TcM.newEvVar pty
 628        ; setEvBind ev evtrm
 629        ; return ev }
 630
 631 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 632 -- Note we create immutable variables for given or derived, since we
 633 -- must bind them to TcEvBinds (because their evidence may involve
 634 -- superclasses). However we should be able to override existing
 635 -- 'derived' evidence, even in TcEvBinds
 636 newGivOrDerCoVar ty1 ty2 co
 637   = do { cv <- newCoVar ty1 ty2
 638        ; setEvBind cv (EvCoercion co)
 639        ; return cv }
 640
 641 newWantedCoVar :: TcType -> TcType -> TcS EvVar
 642 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2
 643
 644 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
 645 newKindConstraint ty kind =  wrapTcS $ TcM.newKindConstraint ty kind
 646
 647 newCoVar :: TcType -> TcType -> TcS EvVar
 648 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 649
 650 newIPVar :: IPName Name -> TcType -> TcS EvVar
 651 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 652
 653 newDictVar :: Class -> [TcType] -> TcS EvVar
 654 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 655 \end{code}
 656
 657
 658 \begin{code}
 659 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
 660 -- In a call (isGoodRecEv ev wv), we are considering solving wv
 661 -- using some term that involves ev, such as:
 662 -- by setting           wv = ev
 663 -- or                   wv = EvCast x |> ev
 664 -- etc.
 665 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
 666 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
 667 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
 668 --
 669 -- Guarded means: more instance calls than superclass selections. We
 670 -- compute this by chasing the evidence, adding +1 for every instance
 671 -- call (constructor) and -1 for every superclass selection (destructor).
 672 --
 673 -- See Note [Superclasses and recursive dictionaries] in TcInteract
 674 isGoodRecEv ev_var (WantedEvVar wv _)
 675   = do { tc_evbinds <- getTcEvBindsBag
 676        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
 677        ; return $ case mb of
 678                     Nothing -> True
 679                     Just min_guardedness -> min_guardedness > 0
 680        }
 681
 682   where chase_ev_var :: EvBindMap   -- Evidence binds
 683                  -> EvVar           -- Target variable whose gravity we want to return
 684                  -> Int             -- Current gravity
 685                  -> [EvVar]         -- Visited nodes
 686                  -> EvVar           -- Current node
 687                  -> TcS (Maybe Int)
 688         chase_ev_var assocs trg curr_grav visited orig
 689             | trg == orig         = return $ Just curr_grav
 690             | orig `elem` visited = return $ Nothing
 691             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
 692             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
 693
 694 {-  No longer needed: evidence is in the EvBinds
 695             | isTcTyVar orig && isMetaTyVar orig
 696             = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
 697                  ; case meta_details of
 698                      Flexi -> return Nothing
 699                      Indirect tyco -> chase_ev assocs trg curr_grav
 700                                              (orig:visited) (EvCoercion tyco)
 701                            }
 702 -}
 703             | otherwise = return Nothing
 704
 705         chase_ev assocs trg curr_grav visited (EvId v)
 706             = chase_ev_var assocs trg curr_grav visited v
 707         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
 708             = chase_ev_var assocs trg (curr_grav-1) visited d_id
 709         chase_ev assocs trg curr_grav visited (EvCast v co)
 710             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
 711                  ; m2 <- chase_co assocs trg curr_grav visited co
 712                  ; return (comb_chase_res Nothing [m1,m2]) }
 713
 714         chase_ev assocs trg curr_grav visited (EvCoercion co)
 715             = chase_co assocs trg curr_grav visited co
 716         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
 717             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
 718                  ; return (comb_chase_res Nothing chase_results) }
 719
 720         chase_co assocs trg curr_grav visited co
 721             = -- Look for all the coercion variables in the coercion
 722               -- chase them, and combine the results. This is OK since the
 723               -- coercion will not contain any superclass terms -- anything
 724               -- that involves dictionaries will be bound in assocs.
 725               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
 726                                              (tyVarsOfType co)
 727               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
 728                     ; return (comb_chase_res Nothing chase_results) }
 729
 730         comb_chase_res f []                   = f
 731         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest
 732         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
 733         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
 734
 735
 736 -- Matching and looking up classes and family instances
 737 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 738
 739 data MatchInstResult mi
 740   = MatchInstNo         -- No matching instance
 741   | MatchInstSingle mi  -- Single matching instance
 742   | MatchInstMany       -- Multiple matching instances
 743
 744
 745 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 746 -- Look up a class constraint in the instance environment
 747 matchClass clas tys
 748   = do  { let pred = mkClassPred clas tys
 749         ; instEnvs <- getInstEnvs
 750         ; case lookupInstEnv instEnvs clas tys of {
 751             ([], unifs)               -- Nothing matches
 752                 -> do { traceTcS "matchClass not matching"
 753                                  (vcat [ text "dict" <+> ppr pred,
 754                                          text "unifs" <+> ppr unifs ])
 755                       ; return MatchInstNo
 756                       } ;
 757             ([(ispec, inst_tys)], []) -- A single match
 758                 -> do   { let dfun_id = is_dfun ispec
 759                         ; traceTcS "matchClass success"
 760                                    (vcat [text "dict" <+> ppr pred,
 761                                           text "witness" <+> ppr dfun_id
 762                                            <+> ppr (idType dfun_id) ])
 763                                   -- Record that this dfun is needed
 764                         ; record_dfun_usage dfun_id
 765                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 766                         } ;
 767             (matches, unifs)          -- More than one matches
 768                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 769                                    (vcat [text "dict" <+> ppr pred,
 770                                           text "matches" <+> ppr matches,
 771                                           text "unifs" <+> ppr unifs])
 772                         ; return MatchInstMany
 773                         }
 774         }
 775         }
 776   where record_dfun_usage :: Id -> TcS ()
 777         record_dfun_usage dfun_id
 778           = do { hsc_env <- getTopEnv
 779                ; let  dfun_name = idName dfun_id
 780                       dfun_mod  = ASSERT( isExternalName dfun_name )
 781                                   nameModule dfun_name
 782                ; if isInternalName dfun_name ||    -- Internal name => defined in this module
 783                     modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
 784                  then return () -- internal, or in another package
 785                  else do updInstUses dfun_id
 786                }
 787
 788         updInstUses :: Id -> TcS ()
 789         updInstUses dfun_id
 790             = do { tcg_env <- getGblEnv
 791                  ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
 792                                             (`addOneToNameSet` idName dfun_id)
 793                  }
 794
 795 matchFam :: TyCon
 796          -> [Type]
 797          -> TcS (MatchInstResult (TyCon, [Type]))
 798 matchFam tycon args
 799   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 800        ; case mb of
 801            Nothing  -> return MatchInstNo
 802            Just res -> return $ MatchInstSingle res
 803        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 804        -- multiple matches. Check.
 805        }
 806
 807
 808 -- Functional dependencies, instantiation of equations
 809 -------------------------------------------------------
 810
 811 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
 812                    -> TcS [WantedEvVar]
 813 mkWantedFunDepEqns _   [] = return []
 814 mkWantedFunDepEqns loc eqns
 815   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
 816        ; wevvars <- mapM to_work_item eqns
 817        ; return $ concat wevvars }
 818   where
 819     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
 820     to_work_item ((qtvs, pairs), _, _)
 821       = do { let tvs = varSetElems qtvs
 822            ; tvs' <- mapM newFlexiTcS tvs
 823            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
 824            ; mapM (do_one subst) pairs }
 825
 826     do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
 827                                        sty2 = substTy subst ty2
 828                                 ; ev <- newWantedCoVar sty1 sty2
 829                                 ; return (WantedEvVar ev loc) }
 830
 831 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
 832 pprEquationDoc (eqn, (p1, _), (p2, _))
 833   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
 834 \end{code}