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