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