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