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