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     joinFlavors, 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, getUntouchablesTcS,
  34     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsBag,
  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 Outputable
  91 import Bag
  92 import MonadUtils
  93 import VarSet
  94 import FastString
  95
  96 import HsBinds               -- for TcEvBinds stuff
  97 import Id
  98 import FunDeps
  99
 100 import TcRnTypes
 101
 102 import Control.Monad
 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 joinFlavors :: CtFlavor -> CtFlavor -> CtFlavor
 301 joinFlavors (Wanted loc) _  = Wanted loc
 302 joinFlavors _ (Wanted loc)  = Wanted loc
 303 joinFlavors (Derived loc) _ = Derived loc
 304 joinFlavors _ (Derived loc) = Derived loc
 305 joinFlavors (Given loc) _   = Given loc
 306
 307 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 308 mkGivenFlavor (Wanted  loc) sk = Given (setCtLocOrigin loc sk)
 309 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
 310 mkGivenFlavor (Given   loc) sk = Given (setCtLocOrigin loc sk)
 311 \end{code}
 312
 313
 314 %************************************************************************
 315 %*                                                                      *
 316 %*              The TcS solver monad                                    *
 317 %*                                                                      *
 318 %************************************************************************
 319
 320 Note [The TcS monad]
 321 ~~~~~~~~~~~~~~~~~~~~
 322 The TcS monad is a weak form of the main Tc monad
 323
 324 All you can do is
 325     * fail
 326     * allocate new variables
 327     * fill in evidence variables
 328
 329 Filling in a dictionary evidence variable means to create a binding
 330 for it, so TcS carries a mutable location where the binding can be
 331 added.  This is initialised from the innermost implication constraint.
 332
 333 \begin{code}
 334 data TcSEnv
 335   = TcSEnv {
 336       tcs_ev_binds :: EvBindsVar,
 337           -- Evidence bindings
 338
 339       tcs_ty_binds :: IORef (Bag (TcTyVar, TcType)),
 340           -- Global type bindings
 341
 342       tcs_context :: SimplContext
 343     }
 344
 345 data SimplContext
 346   = SimplInfer          -- Inferring type of a let-bound thing
 347   | SimplRuleLhs        -- Inferring type of a RULE lhs
 348   | SimplInteractive    -- Inferring type at GHCi prompt
 349   | SimplCheck          -- Checking a type signature or RULE rhs
 350
 351 instance Outputable SimplContext where
 352   ppr SimplInfer       = ptext (sLit "SimplInfer")
 353   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
 354   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 355   ppr SimplCheck       = ptext (sLit "SimplCheck")
 356
 357 isInteractive :: SimplContext -> Bool
 358 isInteractive SimplInteractive = True
 359 isInteractive _                = False
 360
 361 simplEqsOnly :: SimplContext -> Bool
 362 -- Simplify equalities only, not dictionaries
 363 -- This is used for the LHS of rules; ee
 364 -- Note [Simplifying RULE lhs constraints] in TcSimplify
 365 simplEqsOnly SimplRuleLhs = True
 366 simplEqsOnly _            = False
 367
 368 performDefaulting :: SimplContext -> Bool
 369 performDefaulting SimplInfer       = False
 370 performDefaulting SimplRuleLhs     = False
 371 performDefaulting SimplInteractive = True
 372 performDefaulting SimplCheck       = True
 373
 374 ---------------
 375 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
 376
 377 instance Functor TcS where
 378   fmap f m = TcS $ fmap f . unTcS m
 379
 380 instance Monad TcS where
 381   return x  = TcS (\_ -> return x)
 382   fail err  = TcS (\_ -> fail err)
 383   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 384
 385 -- Basic functionality
 386 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 387 wrapTcS :: TcM a -> TcS a
 388 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
 389 -- and TcS is supposed to have limited functionality
 390 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
 391
 392 wrapErrTcS :: TcM a -> TcS a
 393 -- The thing wrapped should just fail
 394 -- There's no static check; it's up to the user
 395 -- Having a variant for each error message is too painful
 396 wrapErrTcS = wrapTcS
 397
 398 wrapWarnTcS :: TcM a -> TcS a
 399 -- The thing wrapped should just add a warning, or no-op
 400 -- There's no static check; it's up to the user
 401 wrapWarnTcS = wrapTcS
 402
 403 failTcS, panicTcS :: SDoc -> TcS a
 404 failTcS      = wrapTcS . TcM.failWith
 405 panicTcS doc = pprPanic "TcCanonical" doc
 406
 407 traceTcS :: String -> SDoc -> TcS ()
 408 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 409
 410 traceTcS0 :: String -> SDoc -> TcS ()
 411 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
 412
 413 runTcS :: SimplContext
 414        -> TcTyVarSet           -- Untouchables
 415        -> TcS a                -- What to run
 416        -> TcM (a, Bag EvBind)
 417 runTcS context untouch tcs
 418   = do { ty_binds_var <- TcM.newTcRef emptyBag
 419        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 420        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
 421                           , tcs_ty_binds = ty_binds_var
 422                           , tcs_context = context }
 423
 424              -- Run the computation
 425        ; res <- TcM.setUntouchables untouch (unTcS tcs env)
 426
 427              -- Perform the type unifications required
 428        ; ty_binds <- TcM.readTcRef ty_binds_var
 429        ; mapBagM_ do_unification ty_binds
 430
 431              -- And return
 432        ; ev_binds <- TcM.readTcRef evb_ref
 433        ; return (res, evBindMapBinds ev_binds) }
 434   where
 435     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 436
 437
 438 nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a
 439 nestImplicTcS ref untouch tcs
 440   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
 441     let
 442        nest_env = TcSEnv { tcs_ev_binds = ref
 443                          , tcs_ty_binds = ty_binds
 444                          , tcs_context = ctxtUnderImplic ctxt }
 445     in
 446     TcM.setUntouchables untouch (unTcS tcs nest_env)
 447
 448 ctxtUnderImplic :: SimplContext -> SimplContext
 449 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 450 ctxtUnderImplic SimplRuleLhs = SimplCheck
 451 ctxtUnderImplic ctxt         = ctxt
 452
 453 tryTcS :: TcTyVarSet -> TcS a -> TcS a
 454 -- Like runTcS, but from within the TcS monad
 455 -- Ignore all the evidence generated, and do not affect caller's evidence!
 456 tryTcS untch tcs
 457   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyBag
 458                     ; ev_binds_var <- TcM.newTcEvBinds
 459                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 460                                      , tcs_ty_binds = ty_binds_var }
 461                     ; TcM.setUntouchables untch (unTcS tcs env1) })
 462
 463 -- Update TcEvBinds
 464 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 465
 466 getDynFlags :: TcS DynFlags
 467 getDynFlags = wrapTcS TcM.getDOpts
 468
 469 getTcSContext :: TcS SimplContext
 470 getTcSContext = TcS (return . tcs_context)
 471
 472 getTcEvBinds :: TcS EvBindsVar
 473 getTcEvBinds = TcS (return . tcs_ev_binds)
 474
 475 getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType)))
 476 getTcSTyBinds = TcS (return . tcs_ty_binds)
 477
 478 getTcSTyBindsBag :: TcS (Bag (TcTyVar, TcType))
 479 getTcSTyBindsBag = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
 480
 481
 482 getTcEvBindsBag :: TcS EvBindMap
 483 getTcEvBindsBag
 484   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 485        ; wrapTcS $ TcM.readTcRef ev_ref }
 486
 487 setWantedCoBind :: CoVar -> Coercion -> TcS ()
 488 setWantedCoBind cv co
 489   = setEvBind cv (EvCoercion co)
 490      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
 491
 492 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
 493 setDerivedCoBind cv co
 494   = setEvBind cv (EvCoercion co)
 495
 496 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 497 -- Add a type binding
 498 setWantedTyBind tv ty
 499   = do { ref <- getTcSTyBinds
 500        ; wrapTcS $
 501          do { ty_binds <- TcM.readTcRef ref
 502             ; TcM.writeTcRef ref (ty_binds `snocBag` (tv,ty)) } }
 503
 504 setIPBind :: EvVar -> EvTerm -> TcS ()
 505 setIPBind = setEvBind
 506
 507 setDictBind :: EvVar -> EvTerm -> TcS ()
 508 setDictBind = setEvBind
 509
 510 setEvBind :: EvVar -> EvTerm -> TcS ()
 511 -- Internal
 512 setEvBind ev rhs
 513   = do { tc_evbinds <- getTcEvBinds
 514        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 515
 516 newTcEvBindsTcS :: TcS EvBindsVar
 517 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
 518
 519 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 520 warnTcS loc warn_if doc
 521   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 522   | otherwise = return ()
 523
 524 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 525 getDefaultInfo
 526   = do { ctxt <- getTcSContext
 527        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 528        ; return (ctxt, tys, flags) }
 529
 530 -- Just get some environments needed for instance looking up and matching
 531 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 532
 533 getInstEnvs :: TcS (InstEnv, InstEnv)
 534 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 535
 536 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 537 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 538
 539 getTopEnv :: TcS HscEnv
 540 getTopEnv = wrapTcS $ TcM.getTopEnv
 541
 542 getGblEnv :: TcS TcGblEnv
 543 getGblEnv = wrapTcS $ TcM.getGblEnv
 544
 545 getUntouchablesTcS :: TcS TcTyVarSet
 546 getUntouchablesTcS = wrapTcS $ TcM.getUntouchables
 547
 548 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 549 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 550
 551 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 552 checkWellStagedDFun pred dfun_id loc
 553   = wrapTcS $ TcM.setCtLoc loc $
 554     do { use_stage <- TcM.getStage
 555        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 556   where
 557     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 558     bind_lvl = TcM.topIdLvl dfun_id
 559
 560 pprEq :: TcType -> TcType -> SDoc
 561 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 562
 563 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 564 -- is touchable variable!
 565 isTouchableMetaTyVar v
 566   | isMetaTyVar v = wrapTcS $ do { untch <- TcM.isUntouchable v;
 567                                  ; return (not untch) }
 568   | otherwise     = return False
 569
 570
 571 -- Flatten skolems
 572 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 573
 574 newFlattenSkolemTy :: TcType -> TcS TcType
 575 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 576   where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 577         newFlattenSkolemTyVar ty
 578             = wrapTcS $ do { uniq <- TcM.newUnique
 579                            ; let name = mkSysTvName uniq (fsLit "f")
 580                            ; return $
 581                              mkTcTyVar name (typeKind ty) (FlatSkol ty)
 582                            }
 583
 584 -- Instantiations
 585 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 586
 587 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 588 instDFunTypes mb_inst_tys =
 589   let inst_tv :: Either TyVar TcType -> TcS Type
 590       inst_tv (Left tv)  = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy
 591       inst_tv (Right ty) = return ty
 592   in mapM inst_tv mb_inst_tys
 593
 594
 595 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 596 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 597
 598
 599 -- Superclasses and recursive dictionaries
 600 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 601
 602 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
 603 newGivOrDerEvVar pty evtrm
 604   = do { ev <- wrapTcS $ TcM.newEvVar pty
 605        ; setEvBind ev evtrm
 606        ; return ev }
 607
 608 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 609 -- Note we create immutable variables for given or derived, since we
 610 -- must bind them to TcEvBinds (because their evidence may involve
 611 -- superclasses). However we should be able to override existing
 612 -- 'derived' evidence, even in TcEvBinds
 613 newGivOrDerCoVar ty1 ty2 co
 614   = do { cv <- newCoVar ty1 ty2
 615        ; setEvBind cv (EvCoercion co)
 616        ; return cv }
 617
 618 newWantedCoVar :: TcType -> TcType -> TcS EvVar
 619 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2
 620
 621 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
 622 newKindConstraint ty kind =  wrapTcS $ TcM.newKindConstraint ty kind
 623
 624 newCoVar :: TcType -> TcType -> TcS EvVar
 625 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 626
 627 newIPVar :: IPName Name -> TcType -> TcS EvVar
 628 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 629
 630 newDictVar :: Class -> [TcType] -> TcS EvVar
 631 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 632 \end{code}
 633
 634
 635 \begin{code}
 636 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
 637 -- In a call (isGoodRecEv ev wv), we are considering solving wv
 638 -- using some term that involves ev, such as:
 639 -- by setting           wv = ev
 640 -- or                   wv = EvCast x |> ev
 641 -- etc.
 642 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
 643 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
 644 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
 645 --
 646 -- Guarded means: more instance calls than superclass selections. We
 647 -- compute this by chasing the evidence, adding +1 for every instance
 648 -- call (constructor) and -1 for every superclass selection (destructor).
 649 --
 650 -- See Note [Superclasses and recursive dictionaries] in TcInteract
 651 isGoodRecEv ev_var (WantedEvVar wv _)
 652   = do { tc_evbinds <- getTcEvBindsBag
 653        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
 654        ; return $ case mb of
 655                     Nothing -> True
 656                     Just min_guardedness -> min_guardedness > 0
 657        }
 658
 659   where chase_ev_var :: EvBindMap   -- Evidence binds
 660                  -> EvVar           -- Target variable whose gravity we want to return
 661                  -> Int             -- Current gravity
 662                  -> [EvVar]         -- Visited nodes
 663                  -> EvVar           -- Current node
 664                  -> TcS (Maybe Int)
 665         chase_ev_var assocs trg curr_grav visited orig
 666             | trg == orig         = return $ Just curr_grav
 667             | orig `elem` visited = return $ Nothing
 668             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
 669             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
 670
 671 {-  No longer needed: evidence is in the EvBinds
 672             | isTcTyVar orig && isMetaTyVar orig
 673             = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
 674                  ; case meta_details of
 675                      Flexi -> return Nothing
 676                      Indirect tyco -> chase_ev assocs trg curr_grav
 677                                              (orig:visited) (EvCoercion tyco)
 678                            }
 679 -}
 680             | otherwise = return Nothing
 681
 682         chase_ev assocs trg curr_grav visited (EvId v)
 683             = chase_ev_var assocs trg curr_grav visited v
 684         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
 685             = chase_ev_var assocs trg (curr_grav-1) visited d_id
 686         chase_ev assocs trg curr_grav visited (EvCast v co)
 687             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
 688                  ; m2 <- chase_co assocs trg curr_grav visited co
 689                  ; return (comb_chase_res Nothing [m1,m2]) }
 690
 691         chase_ev assocs trg curr_grav visited (EvCoercion co)
 692             = chase_co assocs trg curr_grav visited co
 693         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
 694             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
 695                  ; return (comb_chase_res Nothing chase_results) }
 696
 697         chase_co assocs trg curr_grav visited co
 698             = -- Look for all the coercion variables in the coercion
 699               -- chase them, and combine the results. This is OK since the
 700               -- coercion will not contain any superclass terms -- anything
 701               -- that involves dictionaries will be bound in assocs.
 702               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
 703                                              (tyVarsOfType co)
 704               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
 705                     ; return (comb_chase_res Nothing chase_results) }
 706
 707         comb_chase_res f []                   = f
 708         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest
 709         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
 710         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
 711
 712
 713 -- Matching and looking up classes and family instances
 714 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 715
 716 data MatchInstResult mi
 717   = MatchInstNo         -- No matching instance
 718   | MatchInstSingle mi  -- Single matching instance
 719   | MatchInstMany       -- Multiple matching instances
 720
 721
 722 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 723 -- Look up a class constraint in the instance environment
 724 matchClass clas tys
 725   = do  { let pred = mkClassPred clas tys
 726         ; instEnvs <- getInstEnvs
 727         ; case lookupInstEnv instEnvs clas tys of {
 728             ([], unifs)               -- Nothing matches
 729                 -> do { traceTcS "matchClass not matching"
 730                                  (vcat [ text "dict" <+> ppr pred,
 731                                          text "unifs" <+> ppr unifs ])
 732                       ; return MatchInstNo
 733                       } ;
 734             ([(ispec, inst_tys)], []) -- A single match
 735                 -> do   { let dfun_id = is_dfun ispec
 736                         ; traceTcS "matchClass success"
 737                                    (vcat [text "dict" <+> ppr pred,
 738                                           text "witness" <+> ppr dfun_id
 739                                            <+> ppr (idType dfun_id) ])
 740                                   -- Record that this dfun is needed
 741                         ; record_dfun_usage dfun_id
 742                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 743                         } ;
 744             (matches, unifs)          -- More than one matches
 745                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 746                                    (vcat [text "dict" <+> ppr pred,
 747                                           text "matches" <+> ppr matches,
 748                                           text "unifs" <+> ppr unifs])
 749                         ; return MatchInstMany
 750                         }
 751         }
 752         }
 753   where record_dfun_usage :: Id -> TcS ()
 754         record_dfun_usage dfun_id
 755           = do { hsc_env <- getTopEnv
 756                ; let  dfun_name = idName dfun_id
 757                       dfun_mod  = ASSERT( isExternalName dfun_name )
 758                                   nameModule dfun_name
 759                ; if isInternalName dfun_name ||    -- Internal name => defined in this module
 760                     modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
 761                  then return () -- internal, or in another package
 762                  else do updInstUses dfun_id
 763                }
 764
 765         updInstUses :: Id -> TcS ()
 766         updInstUses dfun_id
 767             = do { tcg_env <- getGblEnv
 768                  ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
 769                                             (`addOneToNameSet` idName dfun_id)
 770                  }
 771
 772 matchFam :: TyCon
 773          -> [Type]
 774          -> TcS (MatchInstResult (TyCon, [Type]))
 775 matchFam tycon args
 776   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 777        ; case mb of
 778            Nothing  -> return MatchInstNo
 779            Just res -> return $ MatchInstSingle res
 780        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 781        -- multiple matches. Check.
 782        }
 783
 784
 785 -- Functional dependencies, instantiation of equations
 786 -------------------------------------------------------
 787
 788 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
 789                    -> TcS [WantedEvVar]
 790 mkWantedFunDepEqns _   [] = return []
 791 mkWantedFunDepEqns loc eqns
 792   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
 793        ; wevvars <- mapM to_work_item eqns
 794        ; return $ concat wevvars }
 795   where
 796     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
 797     to_work_item ((qtvs, pairs), _, _)
 798       = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs)
 799            ; mapM (do_one tenv) pairs }
 800
 801     do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1
 802                                       sty2 = substTy tenv ty2
 803                                 ; ev <- newWantedCoVar sty1 sty2
 804                                 ; return (WantedEvVar ev loc) }
 805
 806 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
 807 pprEquationDoc (eqn, (p1, _), (p2, _))
 808   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
 809 \end{code}