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